Theorem: MyNat.and_or_distrib_left (TheoremProvingLean/inductive_types.lean)

State before:
P Q R : Prop
⊢ P ∧ (Q ∨ R) ↔ P ∧ Q ∨ P ∧ R
Tactic:
constructor
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 h
  have _ : P := h.left
  cases h.right with
  | inl hq => apply Or.inl; constructor <;> assumption
  | inr rq => apply Or.inr; constructor <;> assumption
State after:
no goals

State before:
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
Tactic:
case mpr =>
  intro h
  cases h with
  | inl hpq =>
    constructor
    exact hpq.1
    apply Or.inl
    exact hpq.2
    | inr hpr =>
    constructor
    exact hpr.1
    apply Or.inr
    exact hpr.2
State after:
no goals

State before:
P Q R : Prop
⊢ P ∧ (Q ∨ R) → P ∧ Q ∨ P ∧ R
Tactic:
intro h
State after:
P Q R : Prop
h : P ∧ (Q ∨ R)
⊢ P ∧ Q ∨ P ∧ R

State before:
P Q R : Prop
h : P ∧ (Q ∨ R)
⊢ P ∧ Q ∨ P ∧ R
Tactic:
have _ : P := h.left
State after:
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
⊢ P ∧ Q ∨ P ∧ R

State before:
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
⊢ P ∧ Q ∨ P ∧ R
Tactic:
cases h.right with
| inl hq => apply Or.inl; constructor <;> assumption
| inr rq => apply Or.inr; constructor <;> assumption
State after:
no goals

State before:
case inl
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
hq : Q
⊢ P ∧ Q ∨ P ∧ R
Tactic:
apply Or.inl
State after:
case inl.h
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
hq : Q
⊢ P ∧ Q

State before:
case inl.h
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
hq : Q
⊢ P ∧ Q
Tactic:
constructor <;> assumption
State after:
no goals

State before:
case inr
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
rq : R
⊢ P ∧ Q ∨ P ∧ R
Tactic:
apply Or.inr
State after:
case inr.h
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
rq : R
⊢ P ∧ R

State before:
case inr.h
P Q R : Prop
h : P ∧ (Q ∨ R)
x✝ : P
rq : R
⊢ P ∧ R
Tactic:
constructor <;> assumption
State after:
no goals

State before:
P Q R : Prop
⊢ P ∧ Q ∨ P ∧ R → P ∧ (Q ∨ R)
Tactic:
intro h
State after:
P Q R : Prop
h : P ∧ Q ∨ P ∧ R
⊢ P ∧ (Q ∨ R)

State before:
P Q R : Prop
h : P ∧ Q ∨ P ∧ R
⊢ P ∧ (Q ∨ R)
Tactic:
cases h with
| inl hpq =>
  constructor
  exact hpq.1
  apply Or.inl
  exact hpq.2
  | inr hpr =>
  constructor
  exact hpr.1
  apply Or.inr
  exact hpr.2
State after:
no goals

State before:
case inl
P Q R : Prop
hpq : P ∧ Q
⊢ P ∧ (Q ∨ R)
Tactic:
constructor
State after:
case inl.left
P Q R : Prop
hpq : P ∧ Q
⊢ P

case inl.right
P Q R : Prop
hpq : P ∧ Q
⊢ Q ∨ R

State before:
case inl.left
P Q R : Prop
hpq : P ∧ Q
⊢ P

case inl.right
P Q R : Prop
hpq : P ∧ Q
⊢ Q ∨ R
Tactic:
exact hpq.1
State after:
case inl.right
P Q R : Prop
hpq : P ∧ Q
⊢ Q ∨ R

State before:
case inl.right
P Q R : Prop
hpq : P ∧ Q
⊢ Q ∨ R
Tactic:
apply Or.inl
State after:
case inl.right.h
P Q R : Prop
hpq : P ∧ Q
⊢ Q

State before:
case inl.right.h
P Q R : Prop
hpq : P ∧ Q
⊢ Q
Tactic:
exact hpq.2
State after:
no goals

State before:
case inr
P Q R : Prop
hpr : P ∧ R
⊢ P ∧ (Q ∨ R)
Tactic:
constructor
State after:
case inr.left
P Q R : Prop
hpr : P ∧ R
⊢ P

case inr.right
P Q R : Prop
hpr : P ∧ R
⊢ Q ∨ R

State before:
case inr.left
P Q R : Prop
hpr : P ∧ R
⊢ P

case inr.right
P Q R : Prop
hpr : P ∧ R
⊢ Q ∨ R
Tactic:
exact hpr.1
State after:
case inr.right
P Q R : Prop
hpr : P ∧ R
⊢ Q ∨ R

State before:
case inr.right
P Q R : Prop
hpr : P ∧ R
⊢ Q ∨ R
Tactic:
apply Or.inr
State after:
case inr.right.h
P Q R : Prop
hpr : P ∧ R
⊢ R

State before:
case inr.right.h
P Q R : Prop
hpr : P ∧ R
⊢ R
Tactic:
exact hpr.2
State after:
no goals