Theorem: MotivatedTree.imp_exists_iff (MotivatedMoves/Moves/TreeRewrite.lean)

State before:
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) ↔ ∃ a, p → q a
Tactic:
apply Iff.intro
State after:
case mp
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)

State before:
case mp
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)
Tactic:
by_cases p
State after:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case neg
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : ¬p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a

case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)

State before:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a
Tactic:
intro g
State after:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
g : Imp p (_root_.Exists q)
⊢ ∃ a, p → q a

State before:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
g : Imp p (_root_.Exists q)
⊢ ∃ a, p → q a
Tactic:
have ⟨a, g⟩ := g ‹p›
State after:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
g✝ : Imp p (_root_.Exists q)
a : α
g : q a
⊢ ∃ a, p → q a

State before:
case pos
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : p
g✝ : Imp p (_root_.Exists q)
a : α
g : q a
⊢ ∃ a, p → q a
Tactic:
exact ⟨a, fun _ => g⟩
State after:
no goals

State before:
case neg
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : ¬p
⊢ Imp p (_root_.Exists q) → ∃ a, p → q a
Tactic:
intro _
State after:
case neg
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
h✝ : ¬p
a✝ : Imp p (_root_.Exists q)
⊢ ∃ a, p → q a

State before:
case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
⊢ (∃ a, p → q a) → Imp p (_root_.Exists q)
Tactic:
intro ⟨a, h⟩ g
State after:
case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
a : α
h : p → q a
g : p
⊢ _root_.Exists q

State before:
case mpr
α : Sort u_1
inst : Nonempty α
p : Prop
q : α → Prop
a : α
h : p → q a
g : p
⊢ _root_.Exists q
Tactic:
exact ⟨a, h g⟩
State after:
no goals