Theorem: HTPI.Like_Example_3_2_5 (HTPILib/Chap3.lean)

State before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A \ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ C
Tactic:
apply h3 _
State after:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A \ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B

State before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A \ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Tactic:
define at h2
State after:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : ¬(a ∈ A ∧ a ∉ B)
h3 : a ∈ B → a ∈ C
⊢ a ∈ B

State before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : ¬(a ∈ A ∧ a ∉ B)
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Tactic:
demorgan at h2
State after:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A ∨ a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B

State before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∉ A ∨ a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Tactic:
conditional at h2
State after:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∈ A → a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B

State before:
U : Type
A B C : Set U
a : U
h1 : a ∈ A
h2 : a ∈ A → a ∈ B
h3 : a ∈ B → a ∈ C
⊢ a ∈ B
Tactic:
show a ∈ B from h2 h1
State after:
no goals