Theorem: test_faq_have (lean/main/09_tactics.lean)

State before:
⊢ True
Tactic:
custom_let n : Nat := 5
State after:
n : Nat := 5
⊢ True

State before:
n : Nat := 5
⊢ True
Tactic:
custom_have h : n = n := rfl
State after:
n : Nat := 5
h : n = n
⊢ True

State before:
n : Nat := 5
h : n = n
⊢ True
Tactic:
trivial
State after:
no goals