Theorem: exercise2_1 (LeanCourse/Assignments/Solutions/Solutions2.lean)

State before:
α : Type u_1
p q : α → Prop
⊢ (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x
Tactic:
constructor
State after:
case mp
α : Type u_1
p q : α → Prop
⊢ (∃ x, p x ∨ q x) → (∃ x, p x) ∨ ∃ x, q x

case mpr
α : Type u_1
p q : α → Prop
⊢ ((∃ x, p x) ∨ ∃ x, q x) → ∃ x, p x ∨ q x

State before:
case mp
α : Type u_1
p q : α → Prop
⊢ (∃ x, p x ∨ q x) → (∃ x, p x) ∨ ∃ x, q x
Tactic:
rintro ⟨x, hpx|hqx⟩
State after:
case mp.intro.inl
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ (∃ x, p x) ∨ ∃ x, q x

case mp.intro.inr
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ (∃ x, p x) ∨ ∃ x, q x

State before:
case mp.intro.inl
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ (∃ x, p x) ∨ ∃ x, q x
Tactic:
left
State after:
case mp.intro.inl.h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ ∃ x, p x

State before:
case mp.intro.inl.h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ ∃ x, p x
Tactic:
use x
State after:
no goals

State before:
case mp.intro.inr
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ (∃ x, p x) ∨ ∃ x, q x
Tactic:
right
State after:
case mp.intro.inr.h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ ∃ x, q x

State before:
case mp.intro.inr.h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ ∃ x, q x
Tactic:
use x
State after:
no goals

State before:
case mpr
α : Type u_1
p q : α → Prop
⊢ ((∃ x, p x) ∨ ∃ x, q x) → ∃ x, p x ∨ q x
Tactic:
rintro (⟨x, hpx⟩|⟨x, hqx⟩)
State after:
case mpr.inl.intro
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ ∃ x, p x ∨ q x

case mpr.inr.intro
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ ∃ x, p x ∨ q x

State before:
case mpr.inl.intro
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ ∃ x, p x ∨ q x
Tactic:
use x
State after:
case h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ p x ∨ q x

State before:
case h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ p x ∨ q x
Tactic:
left
State after:
case h.h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ p x

State before:
case h.h
α : Type u_1
p q : α → Prop
x : α
hpx : p x
⊢ p x
Tactic:
assumption
State after:
no goals

State before:
case mpr.inr.intro
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ ∃ x, p x ∨ q x
Tactic:
use x
State after:
case h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ p x ∨ q x

State before:
case h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ p x ∨ q x
Tactic:
right
State after:
case h.h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ q x

State before:
case h.h
α : Type u_1
p q : α → Prop
x : α
hqx : q x
⊢ q x
Tactic:
assumption
State after:
no goals