Theorems / novel_alg_10

Authored

Algebra · easy

Statement, exactly as the model and Lean see it
theorem lg_target {G : Type*} [Group G] (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
Source
Written for LeanGraph, reference proof certified
Premises used by the reference proof
1

Traces

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

Verified1 model calls · 1 Lean checks · $0.00010

Retrieved lemmas

  1. 1. conj_commutatorElement_left_commutatorElement_mul
  2. 2. conj_commutatorElement_right_commutatorElement_mul
  3. 3. SemiconjBy.conj_iff
  4. 4. Commute.inv
  5. 5. mul_inv_rev
  6. 6. Commute.mul_inv
  7. 7. DivisionMonoid.mul_inv_rev
  8. 8. Commute.conj

Attempts

  1. sample 0 · round 0Verified12.4 s model time
    Proof
    rw [mul_inv_rev]

Verified proof

theorem lg_target {G : Type*} [Group G] (a b : G) : (a * b)⁻¹ = b⁻¹ * a⁻¹ := by
  rw [mul_inv_rev]

Axioms used: propext

Reference proof

The proof we wrote and certified before any model ran.

simp