Number theory · hard

Statement, exactly as the model and Lean see it

theorem lg_target {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] (hΓ : ∃ h ∈ Γ.strictPeriods, 0 < h) {a b : ℤ} {f : ModularForm Γ a} {g : ModularForm Γ b} (hf : f ≠ 0) (hg : g ≠ 0) : f.mul g ≠ 0 := by

Mathlib declaration: ModularForm.mul_ne_zero
Held-out module: Mathlib.NumberTheory.ModularForms.QExpansion
Banned modules (itself + downstream): 19
Reference proof premises (reachable / held-out): 4 / 2

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00009

Attempts

sample 0 · round 0Lean 3 syntax3.3 s model time

Proof

intro hfg
contrapose! hfg
assume hfg_eq_zero : f.mul g = 0
have hfg_eq_zero' : f.mul g = 0 := hfg_eq_zero
have hf_ne_zero : f ≠ 0 := hf
have hg_ne_zero : g ≠ 0 := hg
have hmul_zero : f.mul g = 0 := hfg_eq_zero'
rw [mul_zero_iff_left hf_ne_zero] at hmul_zero
exact hmul_zero hg_ne_zero

What Lean printed (this is all the model sees on repair)

6:9: error: Unknown identifier `hfg_eq_zero`
6:21: error: unexpected token ':'; expected command

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

/-- The product of two non-zero modular forms is non-zero. -/
protected lemma mul_ne_zero [Γ.HasDetPlusMinusOne] (hΓ : ∃ h ∈ Γ.strictPeriods, 0 < h)
    {a b : ℤ} {f : ModularForm Γ a} {g : ModularForm Γ b} (hf : f ≠ 0) (hg : g ≠ 0) :
    f.mul g ≠ 0 := by
  obtain ⟨h, hΓ, hh⟩ := hΓ
  simp only [ne_eq, ← ModularForm.qExpansion_eq_zero_iff hh hΓ,
    ModularForm.qExpansion_mul hh hΓ] at hf hg ⊢
  exact mul_ne_zero hf hg