Theorem: HTPI.Example_3_2_5_simple (HTPILib/IntroLean.lean)

State before:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∉ B \ C
⊢ a ∈ C
Tactic:
define at h2
State after:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : ¬(a ∈ B ∧ a ∉ C)
⊢ a ∈ C

State before:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : ¬(a ∈ B ∧ a ∉ C)
⊢ a ∈ C
Tactic:
demorgan at h2
State after:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∉ B ∨ a ∈ C
⊢ a ∈ C

State before:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∉ B ∨ a ∈ C
⊢ a ∈ C
Tactic:
conditional at h2
State after:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∈ B → a ∈ C
⊢ a ∈ C

State before:
B C : Set ℕ
a : ℕ
h1 : a ∈ B
h2 : a ∈ B → a ∈ C
⊢ a ∈ C
Tactic:
show a ∈ C from h2 h1
State after:
no goals