Theorem: exists_iff (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∀ (T : Sort u_1) (P Q : T → Prop), (∀ (t : T), Q t ↔ P t) → (∃ t, P t) → ∃ t, Q t
Tactic:
intros T P Q equiv ex_t
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
⊢ ∃ t, Q t

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
⊢ ∃ t, Q t
Tactic:
match ex_t with
 | Exists.intro w h =>
   exists w
   simp [equiv]
   exact h
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ ∃ t, Q t
Tactic:
exists w
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ Q w

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ Q w
Tactic:
simp [equiv]
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ P w

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
T : Sort u_1
P Q : T → Prop
equiv : ∀ (t : T), Q t ↔ P t
ex_t : ∃ t, P t
w : T
h : (fun t => P t) w
⊢ P w
Tactic:
exact h
State after:
no goals