lean - 如何证明精益的例子？

Question

下面是我的错误尝试。关于如何进行的任何建议？

def le(f g : ℕ) : Prop := ∃ a : ℕ , a + f = g

local notation a ≤ b := le a b

    example : ∀ f g : ℕ , f ≤ g → g ≤ f → f = g :=
    begin
      assume f g fg gf,
      dsimp[le.nat] at fg,
      dsimp[le.nat] at gf,
      cases fg with a b,
      cases gf with c d,
      rewrite←  b at d,
      rewrite← d at b,
      induction f with f' ih,
      rewrite← d,
      ring,
      ring at d,
      rewrite← b,
      ring,
      ring at b,
      rewrite d,
      ring,
      cases a,
      refl,
      rewrite← d,
      cases c,
      ring,
      contradiction,
      cases c,
      ring at d,
      rewrite← d,
      cases a,
      ring,
      ring at d,
      ring at b,
      exact b,
    
    end

Answer 1

如果你import tactic那时

example : ∀ f g : ℕ , f ≤ g → g ≤ f → f = g :=
begin
  rintro f g ⟨a, rfl⟩ ⟨b, hb⟩,
  omega
end

Answer 2

如果出于教学原因您想避免omega：

example : ∀ f g : ℕ , f ≤ g → g ≤ f → f = g :=
begin
  rintro f g ⟨a, rfl⟩ ⟨b, hb⟩,
  rw ←add_assoc at hb,
  conv_rhs at hb {rw ←zero_add f},
  obtain ⟨-, rfl⟩ := nat.eq_zero_of_add_eq_zero (nat.add_right_cancel hb),
  rw zero_add,
end