Lean4 tutorials : Need help trying to prove distributive pro

Stream: new members

[Shubham Kumar]

  theorem and_distrib_or : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r)

in the above equation I am trying to first prove p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r)
but I am unable to extract q and r from (q ∨ r) which makes sense because q -> (q ∨ r) and r -> (q ∨ r) is possible but you can make a case for the other way.

Is there a hint or am I missing something because I feel stuck at this point, getting p is easy with And.left but extracting properties from q ∨ r is not the right way to go I think

[Matthew Ballard]

You want to give proofs in both cases. You can use apply Or.elim h where h : p \or r or you can use

cases h with
| inl g => sorry
| inr g => sorry

[Shubham Kumar]

is there a way of doing things with functions only? I am more comfortable doing something like the following

  theorem or_assoc : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
  Iff.intro
    (λ h =>
      Or.elim h
        (λ hpq =>
          Or.elim hpq
              (λ hp : p => Or.intro_left (q ∨ r) hp)
              (λ hq : q => Or.intro_right p (Or.intro_left r hq)))
        (λ hr : r => Or.intro_right p (Or.intro_right q hr)))
    (λ h : p ∨ (q ∨ r) =>
      Or.elim h
        (λ hp : p => Or.intro_left r (Or.intro_left q hp))
        (λ hqr : (q ∨ r) =>
          Or.elim hqr
            (λ hq : q => Or.intro_left r (Or.intro_right p hq))
            (λ hr : r => Or.intro_right (p ∨ q) hr)))

[Shubham Kumar]

sorry if it's too much to ask, but I am ok with long solutions as long as they are using first principles.

I am trying to practice from first principles then move onto using other ways.

[Shubham Kumar]

also I try to be explicit and not implicit

[Matthew Ballard]

Just checking: you only want a term proof and not a tactic one? Is that correct?