# How to introduce assumption in lean4

This is probably a trivial question, but I've been googling for hours and can't find the syntax I'm looking for.

I'm trying to write a proof of

example (A B C : Prop) (h : A → (B ∨ C)) : (A → B) ∨ (A → C) := by
<logic goes here>


The logic I'm trying to replicate is something like:

• Assume A

• From h we have B ∨ C

• if B, then A → B, which implies (A → B) ∨ (A → C)

• conversely, if ¬B, then C, so A → C, which again implies (A → B) ∨ (A → C)

• Finally, if ¬A, then A → B, which implies (A → B) ∨ (A → C)

I assume this is what cases is for, but when I try cases h I'm told: "tactic 'induction' failed, major premise type is not an inductive type"

• You seem to be doing classical reasoning. Commented Nov 8, 2023 at 22:33
• @AgnishomChattopadhyay Correct. Since posting my question, I've figured out that I can introduce a tautology via "have hemA : A ∨ ¬A := em A" and then do cases on that. I think I have it mostly figured out, now. Will post my answer when I'm done. Commented Nov 8, 2023 at 23:08

I figured it out!

This might not be the most elegant solution, but it works.

open Classical

example (A B C : Prop) (h : A → (B ∨ C)) : ((A → B) ∨ (A → C)) := by
have hemA : A ∨ ¬A := em A
cases hemA
{
have hBC : B ∨ C := by
apply h
assumption
cases hBC
{
apply Or.inl
intro
assumption
}
{
apply Or.inr
intro
assumption
}
}
{
have hAB : A → B := by
intro
apply Or.inl
exact hAB
}


More elegant solutions are of course welcome.

Note that lean has good support for structured proofs:

open Classical

example (A B C : Prop) (h : A → (B ∨ C)) : ((A → B) ∨ (A → C)) := by
cases em A with
| inl ha =>
cases h ha with
| inl hb =>
left
intro
exact hb
| inr hc =>
right
intro
exact hc
| inr na =>
apply Or.inl
intro
$$$$
`