Having trouble applying lemma due to metavariable

Stream: new members

[Daniel Fabian]

I'm trying to apply the lemma eq_zero_of_mul_eq_self_left (copied here for convenience),

lemma eq_zero_of_mul_eq_self_left_local {a b : ℤ} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 := sorry

example : (∀ f : ℤ → ℤ, 2 * f 0 = f 0 → f(0) = 0) :=
begin
    intros,
    apply eq_zero_of_mul_eq_self_left_local,
end

However, once I apply the lemma it wants me to show ?m1 ≠ 1 vs 2 ≠ 1. And even if I introduce 2 ≠ 1 into the context using a have, it still won't unify. I think, I probably need to show it that 2 : ℤ, but not sure how. (or perhaps I'm doing something really stupid)

[Kevin Buzzard]

import tactic

lemma eq_zero_of_mul_eq_self_left_local {a b : ℤ} (h₁ : b ≠ 1) (h₂ : b * a = a) : a = 0 := sorry

example : (∀ f : ℤ → ℤ, 2 * f 0 = f 0 → f(0) = 0) :=
begin
    intros,
    apply eq_zero_of_mul_eq_self_left_local (show (2 : ℤ) ≠ 1, by norm_num),
end

[Kevin Buzzard]

Or

example : (∀ f : ℤ → ℤ, 2 * f 0 = f 0 → f(0) = 0) :=
begin
    intros,
    have h : (2 : ℤ) ≠ 1,
    { norm_num},
    apply eq_zero_of_mul_eq_self_left_local h,
end

but now you have an h clogging up your local context

[Daniel Fabian]

fantastic, this moved my prove forward! either option would be fine in my case as this concludes the subproof.

I'm trying to formalise the math olympiad problem and lean is somehow really neat for exploring properties.

[Kevin Buzzard]

Other people have formalised various Olympiad problems, e.g. https://github.com/jsm28/bmo2-2020-lean and https://github.com/leanprover-community/mathlib/blob/master/archive/imo1988_q6.lean

[Oliver Nash]

Since this has come up, I can’t help shamelessly promoting my own effort (in Coq 😱) http://olivernash.org/2019/07/06/coq-imo/index.html