a b c : ℕ,
h₁ : a = b,
h₂ : b = c
⊢ a = b
2 goals
a : ℕ
⊢ ?m_1 = a

a : ℕ
⊢ ℕ
a : ℕ
⊢ ?m_1 = a
2 goals
a : ℕ
⊢ ℕ

a : ℕ
⊢ ?m_1 = a
a : ℕ
⊢ a = a
apply_tac.lean:62:0: warning: declaration 'my_div_self' uses sorry
