Theorem: LoVe.ForwardProofs.prop_comp_tactical (LoVe/Lectures/LoVe04_ForwardProofs_Demo.lean)

State before:
a b c : Prop
hab : a → b
hbc : b → c
⊢ a → c
Tactic:
intro ha
State after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ c

State before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
⊢ c
Tactic:
have hb : b :=
  hab ha
State after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
⊢ c

State before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
⊢ c
Tactic:
let c' := c
State after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
c' : Prop := c
⊢ c

State before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
c' : Prop := c
⊢ c
Tactic:
have hc : c' :=
  hbc hb
State after:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
c' : Prop := c
hc : c'
⊢ c

State before:
a b c : Prop
hab : a → b
hbc : b → c
ha : a
hb : b
c' : Prop := c
hc : c'
⊢ c
Tactic:
exact hc
State after:
no goals