awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X : C
φ : X ⟶ 𝒞.Ω
⊢ 𝒞.χ ((pullback φ).obj 𝒞.truth_as_subobject).arrow = φ
have obtain : ∀ (Z : C) (i : Z ⟶ X) (w : Mono i), 𝒞.χ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow = 𝒞.χ i
Tactic: obtain ⟨Z, i, _, rfl⟩ := 𝒞.surjective_χ φ
Cleared hypotheses: φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
⊢ 𝒞.χ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow = 𝒞.χ i
have refine : IsPullback ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
  (𝒞.χ₀ (obj underlying ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject))) (𝒞.χ i) 𝒞.truth
Tactic: refine (𝒞.uniq _ (?_ : IsPullback _ (𝒞.χ₀ _) _ _)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
⊢ IsPullback ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
    (𝒞.χ₀ (obj underlying ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject))) (𝒞.χ i) 𝒞.truth
have refine : pullback.snd 𝒞.truth (𝒞.χ i) ≫ Iso.hom (Iso.refl X) =
  Iso.hom (Iso.symm (underlyingIso (pullback.snd (obj (MonoOver.forget 𝒞.Ω) (MonoOver.mk 𝒞.truth)).hom (𝒞.χ i)))) ≫
    ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
Tactic: refine (IsPullback.of_hasPullback 𝒞.truth (𝒞.χ i)).flip.of_iso
    (underlyingIso _).symm (Iso.refl _) (Iso.refl _) (Iso.refl _)
    ?_ (𝒞.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (underlyingIso (pullback.snd (obj (MonoOver.forget 𝒞.Ω) (MonoOver.mk 𝒞.truth)).hom (𝒞.χ i)))) ≫
      ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
have dsimp : pullback.snd 𝒞.truth (𝒞.χ i) ≫ 𝟙 X =
  Iso.inv (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))) ≫ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
𝒞 : Classifier.{v, u} C
X Z : C
i : Z ⟶ X
w : Mono i
⊢ pullback.snd 𝒞.truth (𝒞.χ i) ≫ 𝟙 X =
    Iso.inv (underlyingIso (pullback.snd 𝒞.truth (𝒞.χ i))) ≫ ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
have rw : (Subobject.mk (A := Limits.pullback 𝒞.truth (𝒞.χ i)) (pullback.snd 𝒞.truth (𝒞.χ i))).arrow =
  ((pullback (𝒞.χ i)).obj 𝒞.truth_as_subobject).arrow
Tactic: rw [Iso.eq_inv_comp, comp_id, underlyingIso_hom_comp_eq_mk]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
x : Subobject.{v, u} X
⊢ obj (Subobject.pullback ((Equiv.symm h.homEquiv : (a : (Subobject.presheaf C).obj (Opposite.op X)) → X ⟶ Ω) x)) h.Ω₀ =
    x
have rw : (h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X))
    ((Equiv.symm h.homEquiv : (a : (Subobject.presheaf C).obj (Opposite.op X)) → X ⟶ Ω) x) =
  x
Tactic: rw [← homEquiv_eq, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
x : Subobject.{v, u} X
rw :
  (h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X))
      ((Equiv.symm h.homEquiv : (a : (Subobject.presheaf C).obj (Opposite.op X)) → X ⟶ Ω) x) =
    x
⊢ obj (Subobject.pullback ((Equiv.symm h.homEquiv : (a : (Subobject.presheaf C).obj (Opposite.op X)) → X ⟶ Ω) x)) h.Ω₀ =
    x
have rw₁ : x = x
Tactic: rw [← homEquiv_eq, Equiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m))) ≫ h.π m = pullbackπ (h.χ m) h.Ω₀
have dsimp : Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m))) ≫
    Over.Hom.left (InducedCategory.Hom.hom (Iso.hom (h.iso m))) ≫ pullbackπ (h.χ m) h.Ω₀ =
  pullbackπ (h.χ m) h.Ω₀
Tactic: dsimp only [π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m))) ≫
      Over.Hom.left (InducedCategory.Hom.hom (Iso.hom (h.iso m))) ≫ pullbackπ (h.χ m) h.Ω₀ =
    pullbackπ (h.χ m) h.Ω₀
have rw : Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m)) ≫ InducedCategory.Hom.hom (Iso.hom (h.iso m))) ≫
    pullbackπ (h.χ m) h.Ω₀ =
  pullbackπ (h.χ m) h.Ω₀
Tactic: rw [← Over.comp_left_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m)) ≫ InducedCategory.Hom.hom (Iso.hom (h.iso m))) ≫
      pullbackπ (h.χ m) h.Ω₀ =
    pullbackπ (h.χ m) h.Ω₀
have h₁ : Over.Hom.left (InducedCategory.Hom.hom (Iso.inv (h.iso m)) ≫ InducedCategory.Hom.hom (Iso.hom (h.iso m))) =
  𝟙 (obj representative ((Subobject.pullback (h.χ m)).obj h.Ω₀)).obj (P := Over.isMono X).left
Tactic: convert! Category.id_comp _ using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
⊢ IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow
have commfst : ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow ≫ Iso.hom (Iso.refl X) =
  Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ m
Tactic: fapply (Subobject.isPullback (h.χ m) h.Ω₀).flip.of_iso
    (((MonoOver.forget _ ⋙ Over.forget _).mapIso (h.iso m)).symm) (Iso.refl _)
    (Iso.refl _) (Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
commfst :
  ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ m
⊢ IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow
have commsnd : Eq (α := obj underlying ((Subobject.pullback (h.χ m)).obj h.Ω₀) ⟶ obj underlying h.Ω₀)
  (pullbackπ (h.χ m) h.Ω₀ ≫ Iso.hom (Iso.refl (obj underlying h.Ω₀)))
  (Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ h.π m)
Tactic: fapply (Subobject.isPullback (h.χ m) h.Ω₀).flip.of_iso
    (((MonoOver.forget _ ⋙ Over.forget _).mapIso (h.iso m)).symm) (Iso.refl _)
    (Iso.refl _) (Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
commfst :
  ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ m
commsnd :
  Eq (α := obj underlying ((Subobject.pullback (h.χ m)).obj h.Ω₀) ⟶ obj underlying h.Ω₀)
    (pullbackπ (h.χ m) h.Ω₀ ≫ Iso.hom (Iso.refl (obj underlying h.Ω₀)))
    (Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ h.π m)
⊢ IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow
have commf : h.χ m ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl X) ≫ h.χ m
Tactic: fapply (Subobject.isPullback (h.χ m) h.Ω₀).flip.of_iso
    (((MonoOver.forget _ ⋙ Over.forget _).mapIso (h.iso m)).symm) (Iso.refl _)
    (Iso.refl _) (Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
commfst :
  ((Subobject.pullback (h.χ m)).obj h.Ω₀).arrow ≫ Iso.hom (Iso.refl X) =
    Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ m
commsnd :
  Eq (α := obj underlying ((Subobject.pullback (h.χ m)).obj h.Ω₀) ⟶ obj underlying h.Ω₀)
    (pullbackπ (h.χ m) h.Ω₀ ≫ Iso.hom (Iso.refl (obj underlying h.Ω₀)))
    (Iso.hom (Iso.symm (Functor.mapIso (MonoOver.forget X ⋙ Over.forget X) (h.iso m))) ≫ h.π m)
commf : h.χ m ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl X) ≫ h.χ m
⊢ IsPullback m (h.π m) (h.χ m) h.Ω₀.arrow
have commg : h.Ω₀.arrow ≫ Iso.hom (Iso.refl Ω) = Iso.hom (Iso.refl (obj underlying h.Ω₀)) ≫ h.Ω₀.arrow
Tactic: fapply (Subobject.isPullback (h.χ m) h.Ω₀).flip.of_iso
    (((MonoOver.forget _ ⋙ Over.forget _).mapIso (h.iso m)).symm) (Iso.refl _)
    (Iso.refl _) (Iso.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
χ' : X ⟶ Ω
π : U ⟶ obj underlying h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
⊢ χ' = h.χ m
have a : Eq (α := obj (Subobject.presheaf C) (Opposite.op X))
  ((h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) χ' :
    obj (Subobject.presheaf C) (Opposite.op X))
  ((h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) (h.χ m) :
    obj (Subobject.presheaf C) (Opposite.op X))
Tactic: apply h.homEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
U X : C
m : U ⟶ X
inst_2 : Mono m
χ' : X ⟶ Ω
π : U ⟶ obj underlying h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
⊢ Eq (α := obj (Subobject.presheaf C) (Opposite.op X))
    ((h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) χ' :
      obj (Subobject.presheaf C) (Opposite.op X))
    ((h.homEquiv : (a : X ⟶ Ω) → (Subobject.presheaf C).obj (Opposite.op X)) (h.χ m) :
      obj (Subobject.presheaf C) (Opposite.op X))
have a : (Subobject.pullback χ').obj h.Ω₀ = Subobject.mk m
Tactic: simp only [χ, Equiv.apply_symm_apply, homEquiv_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
⊢ (fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π' = s.snd
have rw : ((fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π') ≫ h.Ω₀.arrow = s.snd ≫ h.Ω₀.arrow
Tactic: rw [← cancel_mono h.Ω₀.arrow, ← s.condition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
rw : ((fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π') ≫ h.Ω₀.arrow = s.snd ≫ h.Ω₀.arrow
⊢ (fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π' = s.snd
have rw₁ : ((fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π') ≫ h.Ω₀.arrow = s.fst ≫ π' ≫ h.Ω₀.arrow
Tactic: rw [← cancel_mono h.Ω₀.arrow, ← s.condition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
rw : ((fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π') ≫ h.Ω₀.arrow = s.snd ≫ h.Ω₀.arrow
rw₁ : ((fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π') ≫ h.Ω₀.arrow = s.fst ≫ π' ≫ h.Ω₀.arrow
⊢ (fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π' = s.snd
have rw₂ : (fun (s : PullbackCone (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow) ↦ s.fst) s ≫ π' ≫ h.Ω₀.arrow = s.fst ≫ π' ≫ h.Ω₀.arrow
Tactic: rw [← cancel_mono h.Ω₀.arrow, ← s.condition, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (hypothesis)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
⊢ π' = (fun (X : C) ↦ h.π (𝟙 X)) X
have this : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
Tactic: have : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow :=
      { isLimit' := ⟨PullbackCone.IsLimit.mk _ (fun s ↦ s.fst) (by simp)
          (fun s ↦ by rw [← cancel_mono h.Ω₀.arrow, ← s.condition, Category.assoc])
          (fun s m hm _ ↦ by simpa using hm) ⟩ }
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
this : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
⊢ π' = (fun (X : C) ↦ h.π (𝟙 X)) X
have rw : π' ≫ h.Ω₀.arrow = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
Tactic: rw [← cancel_mono h.Ω₀.arrow, h.uniq this,
      ← (h.isPullback (𝟙 X)).w, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
this : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
rw : π' ≫ h.Ω₀.arrow = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
⊢ π' = (fun (X : C) ↦ h.π (𝟙 X)) X
have rw₁ : h.χ (𝟙 X) = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
Tactic: rw [← cancel_mono h.Ω₀.arrow, h.uniq this,
      ← (h.isPullback (𝟙 X)).w, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
this : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
rw : π' ≫ h.Ω₀.arrow = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
rw₁ : h.χ (𝟙 X) = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
⊢ π' = (fun (X : C) ↦ h.π (𝟙 X)) X
have rw₂ : h.χ (𝟙 X) = 𝟙 X ≫ h.χ (𝟙 X)
Tactic: rw [← cancel_mono h.Ω₀.arrow, h.uniq this,
      ← (h.isPullback (𝟙 X)).w, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
X : C
π' : X ⟶ obj underlying h.Ω₀
this : IsPullback (𝟙 X) π' (π' ≫ h.Ω₀.arrow) h.Ω₀.arrow
rw : π' ≫ h.Ω₀.arrow = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
rw₁ : h.χ (𝟙 X) = (fun (X : C) ↦ h.π (𝟙 X)) X ≫ h.Ω₀.arrow
rw₂ : h.χ (𝟙 X) = 𝟙 X ≫ h.χ (𝟙 X)
⊢ π' = (fun (X : C) ↦ h.π (𝟙 X)) X
have rw₃ : h.χ (𝟙 X) = h.χ (𝟙 X)
Tactic: rw [← cancel_mono h.Ω₀.arrow, h.uniq this,
      ← (h.isPullback (𝟙 X)).w, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (hypothesis)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : SubobjectRepresentableBy.{v, u} Ω
inst_3 : HasTerminal.{v, u} C
U X : C
m : U ⟶ X
h_1 : Mono m
χ₀ : U ⟶ terminal.{v, u} C
χ' : X ⟶ Ω
sq : IsPullback m χ₀ χ' (Iso.inv h.isoΩ₀ ≫ h.Ω₀.arrow)
⊢ χ' = h.χ m
have this : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow
Tactic: have : IsPullback m (h.χ₀ U) χ' h.Ω₀.arrow :=
      sq.of_iso (Iso.refl _) (Iso.refl _) (h.isoΩ₀.symm) (Iso.refl _)
        (by simp) (h.isTerminalΩ₀.hom_ext _ _) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
⊢ HasSubobjectClassifier.{v, u} C ↔ IsRepresentable (Subobject.presheaf C)
have mp : HasSubobjectClassifier.{v, u} C → IsRepresentable (Subobject.presheaf C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
mp : HasSubobjectClassifier.{v, u} C → IsRepresentable (Subobject.presheaf C)
⊢ HasSubobjectClassifier.{v, u} C ↔ IsRepresentable (Subobject.presheaf C)
have mpr : IsRepresentable (Subobject.presheaf C) → HasSubobjectClassifier.{v, u} C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
h : HasSubobjectClassifier.{v, u} C
⊢ IsRepresentable (Subobject.presheaf C)
have mp : ∀ (𝒞 : Subobject.Classifier.{v, u} C), IsRepresentable (Subobject.presheaf C)
Tactic: obtain ⟨⟨𝒞⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
𝒞 : Subobject.Classifier.{v, u} C
⊢ IsRepresentable (Subobject.presheaf C)
have mp : RepresentableBy (Subobject.presheaf C) 𝒞.Ω
Tactic: apply RepresentableBy.isRepresentable
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
𝒞 : Subobject.Classifier.{v, u} C
mp : RepresentableBy (Subobject.presheaf C) 𝒞.Ω
⊢ IsRepresentable (Subobject.presheaf C)
have mp₁ : C
Tactic: apply RepresentableBy.isRepresentable
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
h : IsRepresentable (Subobject.presheaf C)
⊢ HasSubobjectClassifier.{v, u} C
have mpr : ∀ (Ω : C) (h : RepresentableBy (Subobject.presheaf C) Ω), HasSubobjectClassifier.{v, u} C
Tactic: obtain ⟨Ω, ⟨h⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : RepresentableBy (Subobject.presheaf C) Ω
⊢ HasSubobjectClassifier.{v, u} C
have mpr : Nonempty (Subobject.Classifier.{v, u} C)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasTerminal.{v, u} C
inst_2 : HasPullbacks.{v, u} C
Ω : C
h : RepresentableBy (Subobject.presheaf C) Ω
⊢ Nonempty (Subobject.Classifier.{v, u} C)
have mpr : Subobject.Classifier.{v, u} C
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
⊢ IsPullback m (from' F) (𝒞.χ m ≫ eΩ.hom) t
have rw : IsPullback m (𝒞.χ₀ F ≫ eΩ₀.hom) (𝒞.χ m ≫ eΩ.hom) t
Tactic: rw [eΩ₀.comp_inv_eq.mp (Subsingleton.elim (from' F ≫ eΩ₀.inv) (𝒞.χ₀ F))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ χ' ≫ eΩ.inv = 𝒞.χ m
have apply : IsPullback m (χ₀' ≫ eΩ₀.inv) (χ' ≫ eΩ.inv) 𝒞.truth
Tactic: apply 𝒞.uniq m (χ₀' := χ₀' ≫ eΩ₀.inv)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
𝒞 : Classifier.{v, u} C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
h : Mono m
χ₀' : F ⟶ Ω₀
χ' : G ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
⊢ χ' = 𝒞.χ m ≫ eΩ.hom
have this : χ' ≫ eΩ.inv = 𝒞.χ m
Tactic: have : χ' ≫ eΩ.inv = 𝒞.χ m := by
      apply 𝒞.uniq m (χ₀' := χ₀' ≫ eΩ₀.inv)
      exact hχ'.paste_vert (IsPullback.of_vert_isIso_mono (by simp [ht]))
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
⊢ IsPullback m (e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)))
    (e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))) (e.functor.map 𝒞₁.truth)
have commfst : e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m
Tactic: apply ((𝒞₁.isPullback (e.inverse.map m)).map e.functor).of_iso (e.counitIso.app _)
      (e.counitIso.app _) (.refl _) (.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
commfst : e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m
⊢ IsPullback m (e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)))
    (e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))) (e.functor.map 𝒞₁.truth)
have commsnd : e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω₀)) =
  (e.counitIso.app F).hom ≫ e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F))
Tactic: apply ((𝒞₁.isPullback (e.inverse.map m)).map e.functor).of_iso (e.counitIso.app _)
      (e.counitIso.app _) (.refl _) (.refl _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Classifier.Defs (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u_1
inst_1 : Category.{v_1, u_1} D
𝒞₁ : Classifier.{v, u} C
e : Equivalence.{v, v_1, u, u_1} C D
F G : D
m : F ⟶ G
h : Mono m
commfst : e.functor.map (e.inverse.map m) ≫ (e.counitIso.app G).hom = (e.counitIso.app F).hom ≫ m
commsnd :
  e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω₀)) =
    (e.counitIso.app F).hom ≫ e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F))
⊢ IsPullback m (e.counitInv.app F ≫ e.functor.map (𝒞₁.χ₀ (e.inverse.obj F)))
    (e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))) (e.functor.map 𝒞₁.truth)
have commf : e.functor.map (𝒞₁.χ (e.inverse.map m)) ≫ Iso.hom (Iso.refl (e.functor.obj 𝒞₁.Ω)) =
  (e.counitIso.app G).hom ≫ e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))
Tactic: apply ((𝒞₁.isPullback (e.inverse.map m)).map e.functor).of_iso (e.counitIso.app _)
      (e.counitIso.app _) (.refl _) (.refl _)