Theorem: Lean4Axiomatic.Logic.or_distribL_and (Lean4Axiomatic/Logic.lean)

State before:
p q r : Prop
⊢ p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)
Tactic:
apply Iff.intro
State after:
case mp
p q r : Prop
⊢ p ∨ q ∧ r → (p ∨ q) ∧ (p ∨ r)

case mpr
p q r : Prop
⊢ (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r

State before:
p q r : Prop
⊢ p ∨ q ∧ r → (p ∨ q) ∧ (p ∨ r)
Tactic:
case mp =>
  intro (_ : p ∨ (q ∧ r))
  show (p ∨ q) ∧ (p ∨ r)
  match ‹p ∨ (q ∧ r)› with
  | Or.inl (_ : p) =>
    have : p ∨ q := Or.inl ‹p›
    have : p ∨ r := Or.inl ‹p›
    exact And.intro ‹p ∨ q› ‹p ∨ r›
  | Or.inr (And.intro (_ : q) (_ : r)) =>
    have : p ∨ q := Or.inr ‹q›
    have : p ∨ r := Or.inr ‹r›
    exact And.intro ‹p ∨ q› ‹p ∨ r›
State after:
no goals

State before:
p q r : Prop
⊢ (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r
Tactic:
case mpr =>
  intro (And.intro (_ : p ∨ q) (_ : p ∨ r))
  show p ∨ (q ∧ r)
  match ‹p ∨ q› with
  | Or.inl (_ : p) =>
    exact Or.inl ‹p›
  | Or.inr (_ : q) =>
    match ‹p ∨ r› with
    | Or.inl (_ : p) =>
      exact Or.inl ‹p›
    | Or.inr (_ : r) =>
      have : q ∧ r := And.intro ‹q› ‹r›
      exact Or.inr ‹q ∧ r›
State after:
no goals

State before:
p q r : Prop
⊢ p ∨ q ∧ r → (p ∨ q) ∧ (p ∨ r)
Tactic:
intro (_ : p ∨ (q ∧ r))
State after:
p q r : Prop
x✝ : p ∨ q ∧ r
⊢ (p ∨ q) ∧ (p ∨ r)

State before:
p q r : Prop
x✝ : p ∨ q ∧ r
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
match ‹p ∨ (q ∧ r)› with
| Or.inl (_ : p) =>
  have : p ∨ q := Or.inl ‹p›
  have : p ∨ r := Or.inl ‹p›
  exact And.intro ‹p ∨ q› ‹p ∨ r›
| Or.inr (And.intro (_ : q) (_ : r)) =>
  have : p ∨ q := Or.inr ‹q›
  have : p ∨ r := Or.inr ‹r›
  exact And.intro ‹p ∨ q› ‹p ∨ r›
State after:
no goals

State before:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
have : p ∨ q := Or.inl ‹p›
State after:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)

State before:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
have : p ∨ r := Or.inl ‹p›
State after:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)

State before:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
exact And.intro ‹p ∨ q› ‹p ∨ r›
State after:
no goals

State before:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
have : p ∨ q := Or.inr ‹q›
State after:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)

State before:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
have : p ∨ r := Or.inr ‹r›
State after:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)

State before:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
exact And.intro ‹p ∨ q› ‹p ∨ r›
State after:
no goals

State before:
p q r : Prop
⊢ (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r
Tactic:
intro (And.intro (_ : p ∨ q) (_ : p ∨ r))
State after:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
⊢ p ∨ q ∧ r

State before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
⊢ p ∨ q ∧ r
Tactic:
match ‹p ∨ q› with
| Or.inl (_ : p) =>
  exact Or.inl ‹p›
| Or.inr (_ : q) =>
  match ‹p ∨ r› with
  | Or.inl (_ : p) =>
    exact Or.inl ‹p›
  | Or.inr (_ : r) =>
    have : q ∧ r := And.intro ‹q› ‹r›
    exact Or.inr ‹q ∧ r›
State after:
no goals

State before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝ : p
⊢ p ∨ q ∧ r
Tactic:
exact Or.inl ‹p›
State after:
no goals

State before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝ : q
⊢ p ∨ q ∧ r
Tactic:
match ‹p ∨ r› with
| Or.inl (_ : p) =>
  exact Or.inl ‹p›
| Or.inr (_ : r) =>
  have : q ∧ r := And.intro ‹q› ‹r›
  exact Or.inr ‹q ∧ r›
State after:
no goals

State before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝¹ : q
h✝ : p
⊢ p ∨ q ∧ r
Tactic:
exact Or.inl ‹p›
State after:
no goals

State before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝¹ : q
h✝ : r
⊢ p ∨ q ∧ r
Tactic:
have : q ∧ r := And.intro ‹q› ‹r›
State after:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝¹ : q
h✝ : r
this : q ∧ r
⊢ p ∨ q ∧ r

State before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝¹ : q
h✝ : r
this : q ∧ r
⊢ p ∨ q ∧ r
Tactic:
exact Or.inr ‹q ∧ r›
State after:
no goals