Algebra · easy

Statement, exactly as the model and Lean see it

theorem lg_target {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) : ∏ x ∈ s, f x ≡ ∏ x ∈ s, g x [MOD n] := by

Mathlib declaration: Nat.ModEq.prod
Held-out module: Mathlib.Algebra.BigOperators.ModEq
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 0 / 1

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.00008

Attempts

sample 0 · round 0Syntax error2.6 s model time

Proof

induction s with x xs IH using Finset.induction_on
· rw [Finset.prod_empty, Finset.prod_empty]
  exact Mod.eq_self_mod _
· rw [Finset.prod_insert, Finset.prod_insert]
  have hfx : f x ≡ g x [MOD n] := h x (Finset.mem_insert x xs)
  rw [hfx, IH]
  exact Mod.mul_mod_mod _

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

4:20: error: unknown tactic
4:14: error: Invalid syntax for induction tactic: The `with` keyword must be followed by a tactic or by an alternative (e.g. `| zero =>`), but here it is followed by the identifier `x`.

Reference proof

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

@[gcongr]
protected theorem prod {s : Finset α} (h : ∀ x ∈ s, f x ≡ g x [MOD n]) :
    (∏ x ∈ s, f x) ≡ ∏ x ∈ s, g x [MOD n] :=
  .multisetProd_map (s := s.1) h