Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₁, u₂} D] {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G) (A : adj.toMonad.Algebra) : G.IsSplitPair (F.map A.a) (adj.counit.app (F.obj A.A)) := by

Mathlib declaration: CategoryTheory.Monad.MonadicityInternal.main_pair_G_split
Held-out module: Mathlib.CategoryTheory.Monad.Monadicity
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 0 / 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.00011

Attempts

sample 0 · round 0Syntax error3.9 s model time

Proof

intro A
obtain ⟨a, h₁, h₂⟩ := A
constructor
· exact (adj.counit.app (F.obj A.A))
· exact (adj.unit.app (G.obj A.A))
· exact (adj.counit naturality at (F.obj A.A))
· exact (adj.unit naturality at (G.obj A.A))
· refine (adj.counit.associates (F.obj A.A) (F.obj A.A) _)
  exact (adj.unit.associates (G.obj A.A) (G.obj A.A) _)
· exact (adj.counit.is_right_inverse (F.obj A.A))
· exact (adj.unit.is_left_inverse (G.obj A.A))

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

9:32: error: unexpected token 'at'; expected ')', ',' or ':'

Reference proof

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

/-- The "main pair" for an algebra `(A, α)` is the pair of morphisms `(F α, ε_FA)`. It is always a
`G`-split pair, and will be used to construct the left adjoint to the comparison functor and show it
is an equivalence.
-/
instance main_pair_G_split (A : adj.toMonad.Algebra) :
    G.IsSplitPair (F.map A.a)
      (adj.counit.app (F.obj A.A)) where
  splittable := ⟨_, _, ⟨beckSplitCoequalizer A⟩⟩