Theorems / mh_alge_8f6995

Mathlib held-out

Algebra · hard

Statement, exactly as the model and Lean see it
theorem lg_target {A : Type u_1} [AddMonoid A] [StarAddMonoid A] {r : A → A → Prop} (hr : ∀ (a b : A), r a b → r (star a) (star b)) ⦃a b : A⦄ : AddConGen.Rel r a b → AddConGen.Rel r (star a) (star b) := by
Mathlib declaration
AddConGen.Rel.star
Held-out module
Mathlib.GroupTheory.Congruence.Star
Banned modules (itself + downstream)
1
Reference proof premises (reachable / held-out)
2 / 0

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

Attempts

  1. sample 0 · round 0Syntax error2.0 s model time
    Proof
    intros H; induction H using AddConGen.Rel.induction with h₁ h₂; constructor; apply hr; assumption
    What Lean printed (this is all the model sees on repair)
    4:60: error: unknown tactic

Reference proof

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

theorem AddConGen.Rel.star (hr : ∀ a b, r a b → r (star a) (star b))
    ⦃a b : A⦄ : Rel r a b → Rel r (star a) (star b)
  | refl _ => .refl _
  | symm h => .symm <| h.star hr
  | trans h1 h2 => .trans  (h1.star hr) (h2.star hr)
  | of _ _ h => .of _ _ (hr _ _ h)
  | add h1 h2 => by
    rw [star_add, star_add]
    exact (h1.star hr).add (h2.star hr)