Theorem: LoVe.BackwardProofs.forall_and (LoVe/Labs/Lab2Solution.lean)

State before:
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) ↔ (∀ (x : α), p x) ∧ ∀ (x : α), q x
Tactic:
apply Iff.intro
State after:
case mp
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x

case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x

State before:
case mp
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x

case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x
Tactic:
{ intro h
  apply And.intro
  { intro x
    apply And.left
    apply h }
  { intro x
    apply And.right
    apply h } }
State after:
case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x

State before:
case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x
Tactic:
{ intro h x
  apply And.intro
  { apply And.left h }
  { apply And.right h } }
State after:
no goals

State before:
case mp
α : Type
p q : α → Prop
⊢ (∀ (x : α), p x ∧ q x) → (∀ (x : α), p x) ∧ ∀ (x : α), q x
Tactic:
intro h
State after:
case mp
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ (∀ (x : α), p x) ∧ ∀ (x : α), q x

State before:
case mp
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ (∀ (x : α), p x) ∧ ∀ (x : α), q x
Tactic:
apply And.intro
State after:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), p x

case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x

State before:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), p x

case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x
Tactic:
{ intro x
  apply And.left
  apply h }
State after:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x

State before:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x
Tactic:
{ intro x
  apply And.right
  apply h }
State after:
no goals

State before:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), p x
Tactic:
intro x
State after:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x

State before:
case mp.left
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x
Tactic:
apply And.left
State after:
case mp.left.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x ∧ ?mp.left.b

case mp.left.b
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop

State before:
case mp.left.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ p x ∧ ?mp.left.b

case mp.left.b
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop
Tactic:
apply h
State after:
no goals

State before:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
⊢ ∀ (x : α), q x
Tactic:
intro x
State after:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ q x

State before:
case mp.right
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ q x
Tactic:
apply And.right
State after:
case mp.right.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ ?mp.right.a ∧ q x

case mp.right.a
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop

State before:
case mp.right.self
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ ?mp.right.a ∧ q x

case mp.right.a
α : Type
p q : α → Prop
h : ∀ (x : α), p x ∧ q x
x : α
⊢ Prop
Tactic:
apply h
State after:
no goals

State before:
case mpr
α : Type
p q : α → Prop
⊢ ((∀ (x : α), p x) ∧ ∀ (x : α), q x) → ∀ (x : α), p x ∧ q x
Tactic:
intro h x
State after:
case mpr
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x ∧ q x

State before:
case mpr
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x ∧ q x
Tactic:
apply And.intro
State after:
case mpr.left
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x

case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x

State before:
case mpr.left
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x

case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
Tactic:
{ apply And.left h }
State after:
case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x

State before:
case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
Tactic:
{ apply And.right h }
State after:
no goals

State before:
case mpr.left
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ p x
Tactic:
apply And.left h
State after:
no goals

State before:
case mpr.right
α : Type
p q : α → Prop
h : (∀ (x : α), p x) ∧ ∀ (x : α), q x
x : α
⊢ q x
Tactic:
apply And.right h
State after:
no goals