Category theory · medium

Statement, exactly as the model and Lean see it

theorem lg_target {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {X Y : C} (i : X ≅ Y) : Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj := by

Mathlib declaration: CategoryTheory.PreGaloisCategory.card_fiber_eq_of_iso
Held-out module: Mathlib.CategoryTheory.Galois.Basic
Banned modules (itself + downstream): 11
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

sample 0 · round 0Hallucinated theorem2.0 s model time

Proof

rw [Nat.card_eq, CategoryTheory.nat_trans_obj_map_eq, CategoryTheory.isomorphic_map]

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

4:19: error: Unknown identifier `CategoryTheory.nat_trans_obj_map_eq`
3:186: error: unsolved goals
C : Type u₁
inst✝ : CategoryTheory.Category.{u₂, u₁} C
F : CategoryTheory.Functor C FintypeCat
X Y : C
i : X ≅ Y
⊢ (if x : Finite (F.obj X).obj then Fintype.card (F.obj X).obj else 0) = Nat.card (F.obj Y).obj

Reference proof

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

/-- The cardinality of the fiber is preserved under isomorphisms. -/
lemma card_fiber_eq_of_iso {X Y : C} (i : X ≅ Y) : Nat.card (F.obj X) = Nat.card (F.obj Y) := by
  have e : F.obj X ≃ F.obj Y := Iso.toEquiv (mapIso (F ⋙ FintypeCat.incl) i)
  exact Nat.card_eq_of_bijective e (Equiv.bijective e)