awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (pre L (𝟭 T) (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ (F := sA.inverse) ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (F := sT.functor) (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
⊢ Final (C := CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
    (pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b))
have apply : F'' ≅ pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)
Tactic: apply final_of_natIso (F := F'')
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (hypothesis)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (pre L (𝟭 T) (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
b : AsSmall B
x : AsSmall T := (sB.inverse ⋙ R ⋙ sT.functor).obj b
F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 (AsSmall T)) x :=
  map₂ (F := sA.inverse) ((sA.inverse ⋙ L).whiskerLeft sT.unit) (𝟙 (sT.inverse.obj x)) ⋙
    pre L (𝟭 T) (R.obj (sB.inverse.obj b)) ⋙
      map₂ (F := sT.functor) (𝟙 (sT.functor ⋙ 𝟭 (AsSmall T))) (𝟙 (sT.functor.obj (R.obj (sB.inverse.obj b))))
⊢ F'' ≅ pre (sA.inverse ⋙ L ⋙ sT.functor) (𝟭 (AsSmall T)) ((sB.inverse ⋙ R ⋙ sT.functor).obj b)
have hsT : ∀ (X : AsSmall T), sT.counitInv.app X = 𝟙 (obj (𝟭 (AsSmall T)) X)
Tactic: have hsT (X) : sT.counitInv.app X = 𝟙 _ := rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (hypothesis)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
⊢ L.Final
have this : ∀ (b : AsSmall B), Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))
Tactic: have (b : _) : (CostructuredArrow.toOver L' (R'.obj b)).Final := by
    dsimp only [L', R', CostructuredArrow.toOver] at hB ⊢
    let x := (sB.inverse ⋙ R ⋙ sT.functor).obj b
    let F'' : CostructuredArrow (sA.inverse ⋙ L ⋙ sT.functor) x ⥤ CostructuredArrow (𝟭 _) x :=
      map₂ (F := sA.inverse) (G := sT.inverse) (whiskerLeft (sA.inverse ⋙ L) sT.unit) (𝟙 _) ⋙
      pre L (𝟭 T) (R.obj _) ⋙ map₂ (F := sT.functor) (G := sT.functor) (𝟙 _) (𝟙 _)
    apply final_of_natIso (F := F'')
    have hsT (X) : sT.counitInv.app X = 𝟙 _ := rfl
    exact NatIso.ofComponents (fun X => CostructuredArrow.isoMk (Iso.refl _) (by simp [F'', hsT]))
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (hypothesis)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
this : ∀ (b : AsSmall B), Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))
⊢ L.Final
have this₁ : L'.Final
Tactic: have := final_of_final_costructuredArrowToOver_small L' R'
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Final (goal)
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
T : Type u₃
inst_2 : Category.{v₃, u₃} T
L : Functor.{v₁, v₃, u₁, u₃} A T
R : Functor.{v₂, v₃, u₂, u₃} B T
inst_3 : R.Final
hB : ∀ (b : B), Final (C := CostructuredArrow L (R.obj b)) (CostructuredArrow.toOver L (R.obj b))
sA : A ≌ AsSmall A := AsSmall.equiv
sB : B ≌ AsSmall B := AsSmall.equiv
sT : T ≌ AsSmall T := AsSmall.equiv
L' : AsSmall A ⥤ AsSmall T := sA.inverse ⋙ L ⋙ sT.functor
R' : AsSmall B ⥤ AsSmall T := sB.inverse ⋙ R ⋙ sT.functor
this_1 : ∀ (b : AsSmall B), Final (C := CostructuredArrow L' (R'.obj b)) (CostructuredArrow.toOver L' (R'.obj b))
this : L'.Final
⊢ L.Final
have apply : sA.functor ⋙ L' ⋙ sT.inverse ≅ L
Tactic: apply final_of_natIso (F := (sA.functor ⋙ L' ⋙ sT.inverse))
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
d : Dᵒᵖ
⊢ Functor.toCatHom (map (Quiver.Hom.unop (𝟙 d))) = 𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T))
have h : Cat.Hom.toFunctor (Functor.toCatHom (map (Quiver.Hom.unop (𝟙 d)))) =
  Cat.Hom.toFunctor (𝟙 (Cat.of (StructuredArrow (Opposite.unop d) T)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : Dᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Cat.of (StructuredArrow (Opposite.unop X) T) ⟶ Cat.of (StructuredArrow (Opposite.unop Z) T))
    (Functor.toCatHom (map (f ≫ g).unop)) (Functor.toCatHom (map f.unop) ≫ Functor.toCatHom (map g.unop))
have h : Eq (α :=
  (↑(Cat.of (StructuredArrow (Opposite.unop X) T)) : Type (max u₁ v₂)) ⥤
    (↑(Cat.of (StructuredArrow (Opposite.unop Z) T)) : Type (max u₁ v₂)))
  (Cat.Hom.toFunctor (Functor.toCatHom (map (f ≫ g).unop)))
  (Cat.Hom.toFunctor (Functor.toCatHom (map f.unop) ≫ Functor.toCatHom (map g.unop)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
d : D
⊢ Functor.toCatHom (map (𝟙 d)) = 𝟙 (Cat.of (CostructuredArrow T d))
have h : Cat.Hom.toFunctor (Functor.toCatHom (map (𝟙 d))) = Cat.Hom.toFunctor (𝟙 (Cat.of (CostructuredArrow T d)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Functor (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
T : Functor.{v₁, v₂, u₁, u₂} C D
X Y Z : D
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := Cat.of (CostructuredArrow T X) ⟶ Cat.of (CostructuredArrow T Z)) (Functor.toCatHom (map (f ≫ g)))
    (Functor.toCatHom (map f) ≫ Functor.toCatHom (map g))
have h : Eq (α :=
  (↑(Cat.of (CostructuredArrow T X)) : Type (max u₁ v₂)) ⥤ (↑(Cat.of (CostructuredArrow T Z)) : Type (max u₁ v₂)))
  (Cat.Hom.toFunctor (Functor.toCatHom (map (f ≫ g))))
  (Cat.Hom.toFunctor (Functor.toCatHom (map f) ≫ Functor.toCatHom (map g)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : Small.{w, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
f : StructuredArrow S T
⊢ ∃ (a : (X : C) × (S ⟶ T.obj X)),
    (fun (f : (X : C) × (S ⟶ T.obj X)) ↦ mk (f.snd (β := fun (X : C) ↦ S ⟶ T.obj X))) a = f
have obtain : ∀ (X : C) (f : S ⟶ T.obj X),
  ∃ (a : (X : C) × (S ⟶ T.obj X)),
    (fun (f : (X : C) × (S ⟶ T.obj X)) ↦ mk (f.snd (β := fun (X : C) ↦ S ⟶ T.obj X))) a = mk f
Tactic: obtain ⟨X, f, rfl⟩ := f.mk_surjective
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
this :
  P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))
have rw : ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (C := StructuredArrow S T)
  (ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
    mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C))))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))
have suffices : P.inverseImage (proj S T) =
  ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
    mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))
Tactic: suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S ⟶ T.obj G => mk f.2 by
    rw [this]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
⊢ P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))
have h : ∀ (X : StructuredArrow S T),
  P.inverseImage (proj S T) X ↔
    ObjectProperty.ofObj
      (fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦ mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
X : StructuredArrow S T
⊢ P.inverseImage (proj S T) X ↔
    ObjectProperty.ofObj
      (fun (f : (G : Subtype P) × (S ⟶ T.obj (↑G : C))) ↦ mk (f.snd (β := fun (G : Subtype P) ↦ S ⟶ T.obj (↑G : C)))) X
have h : P X.right ↔ ∃ (a : C), P a ∧ ∃ (b : S ⟶ T.obj a), mk b = X
Tactic: simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
    Sigma.exists, Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (StructuredArrow S T)
have rw : EssentiallySmall.{w, w, max v₂ w}
  (StructuredArrow.{w, v₂, w, u₂} (C := SmallModel.{w, v₁, u₁} C) S (Equivalence.inverse (equivSmallModel C) ⋙ T))
Tactic: rw [← essentiallySmall_congr
    (StructuredArrow.pre S (equivSmallModel.{w} C).inverse T).asEquivalence]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : Small.{w, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
f : CostructuredArrow S T
⊢ ∃ (a : (X : C) × (S.obj X ⟶ T)),
    (fun (f : (X : C) × (S.obj X ⟶ T)) ↦ mk (f.snd (β := fun (X : C) ↦ S.obj X ⟶ T))) a = f
have obtain : ∀ (X : C) (f : S.obj X ⟶ T),
  ∃ (a : (X : C) × (S.obj X ⟶ T)),
    (fun (f : (X : C) × (S.obj X ⟶ T)) ↦ mk (f.snd (β := fun (X : C) ↦ S.obj X ⟶ T))) a = mk f
Tactic: obtain ⟨X, f, rfl⟩ := f.mk_surjective
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
this :
  P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))
have rw : ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (C := CostructuredArrow S T)
  (ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
    mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))
have suffices : P.inverseImage (proj S T) =
  ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
    mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))
Tactic: suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S.obj G ⟶ T => mk f.2 by
    rw [this]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
⊢ P.inverseImage (proj S T) =
    ObjectProperty.ofObj fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦
      mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))
have h : ∀ (X : CostructuredArrow S T),
  P.inverseImage (proj S T) X ↔
    ObjectProperty.ofObj
      (fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦ mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))) X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{v₁, v₁, u₁} P
inst_3 : LocallySmall.{v₁, v₂, u₂} D
X : CostructuredArrow S T
⊢ P.inverseImage (proj S T) X ↔
    ObjectProperty.ofObj
      (fun (f : (G : Subtype P) × (S.obj (↑G : C) ⟶ T)) ↦ mk (f.snd (β := fun (G : Subtype P) ↦ S.obj (↑G : C) ⟶ T))) X
have h : P X.left ↔ ∃ (a : C), P a ∧ ∃ (b : S.obj a ⟶ T), mk b = X
Tactic: simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
    Sigma.exists, Subtype.exists, exists_prop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Comma.StructuredArrow.Small (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
inst_2 : EssentiallySmall.{w, v₁, u₁} C
inst_3 : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (CostructuredArrow S T)
have rw : EssentiallySmall.{w, w, max v₂ w}
  (CostructuredArrow.{w, v₂, w, u₂} (C := SmallModel.{w, v₁, u₁} C) (Equivalence.inverse (equivSmallModel C) ⋙ S) T)
Tactic: rw [← essentiallySmall_congr
    (CostructuredArrow.pre (equivSmallModel.{w} C).inverse S T).asEquivalence]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j k : Fin 2
hij : i ≤ j
hjk : j ≤ k
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk
have inl : ∀ (hij : i ≤ i) (hjk : i ≤ k), map f i k sorry = map f i i hij ≫ map f i k hjk
Tactic: obtain rfl | rfl : i = j ∨ j = k := by lia
Cleared hypotheses: j, hij, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j k : Fin 2
hij : i ≤ j
hjk : j ≤ k
inl : ∀ (hij : i ≤ i) (hjk : i ≤ k), map f i k ⋯ = map f i i hij ≫ map f i k hjk
⊢ map f i k ⋯ = map f i j hij ≫ map f j k hjk
have inr : ∀ (hjk : j ≤ j), map f i j sorry = map f i j hij ≫ map f j j hjk
Tactic: obtain rfl | rfl : i = j ∨ j = k := by lia
Cleared hypotheses: k, hjk
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i k : Fin 2
hij : i ≤ i
hjk : i ≤ k
⊢ map f i k ⋯ = map f i i hij ≫ map f i k hjk
have inl : map f i k sorry = 𝟙 (obj X₀ X₁ i) ≫ map f i k hjk
Tactic: rw [map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i k : Fin 2
hij : i ≤ i
hjk : i ≤ k
inl : map f i k ⋯ = 𝟙 (obj X₀ X₁ i) ≫ map f i k hjk
⊢ map f i k ⋯ = map f i i hij ≫ map f i k hjk
have inl₁ : map f i k sorry = map f i k hjk
Tactic: rw [map_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j : Fin 2
hij : i ≤ j
hjk : j ≤ j
⊢ map f i j ⋯ = map f i j hij ≫ map f j j hjk
have inr : map f i j sorry = map f i j hij ≫ 𝟙 (obj X₀ X₁ j)
Tactic: rw [map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
i j : Fin 2
hij : i ≤ j
hjk : j ≤ j
inr : map f i j ⋯ = map f i j hij ≫ 𝟙 (obj X₀ X₁ j)
⊢ map f i j ⋯ = map f i j hij ≫ map f j j hjk
have inr₁ : map f i j sorry = map f i j hij
Tactic: rw [map_id, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this :
  ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : (⟨i, hi⟩ : Fin (n + 1)) ⟶ ⟨j, hj⟩
⊢ F.map hij ≫ app (⟨j, hj⟩ : Fin (n + 1)) = app ⟨i, hi⟩ ≫ G.map hij
have hij' : (⟨i, hi⟩ : Fin (n + 1)) ≤ ⟨j, hj⟩
Tactic: have hij' := leOfHom hij
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this :
  ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : (⟨i, hi⟩ : Fin (n + 1)) ⟶ ⟨j, hj⟩
hij' : (⟨i, hi⟩ : Fin (n + 1)) ≤ ⟨j, hj⟩
⊢ F.map hij ≫ app (⟨j, hj⟩ : Fin (n + 1)) = app ⟨i, hi⟩ ≫ G.map hij
have hij'₁ : i ≤ j
Tactic: simp only [Fin.mk_le_mk] at hij'
Cleared hypotheses: hij'
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
this :
  ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
    Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
      (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 1
hij : (⟨i, hi⟩ : Fin (n + 1)) ⟶ ⟨j, hj⟩
hij' : i ≤ j
⊢ F.map hij ≫ app (⟨j, hj⟩ : Fin (n + 1)) = app ⟨i, hi⟩ ≫ G.map hij
have obtain : ∀ (k : ℕ) (hk : i + k = j), F.map hij ≫ app (⟨j, hj⟩ : Fin (n + 1)) = app ⟨i, hi⟩ ≫ G.map hij
Tactic: obtain ⟨k, hk⟩ := Nat.le.dest hij'
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
⊢ ∀ ⦃X Y : Fin (n + 1)⦄ (f : X ⟶ Y), F.map f ≫ app Y = app X ≫ G.map f
have suffices : ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
  Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
    (F.map' i j sorry hj' ≫ app ⟨j, sorry⟩ : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
    (app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i j sorry hj' : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, sorry⟩)
Tactic: suffices ∀ (k i j : ℕ) (hj : i + k = j) (hj' : j ≤ n),
        F.map' i j ≫ app _ = app _ ≫ G.map' i j by
      rintro ⟨i, hi⟩ ⟨j, hj⟩ hij
      have hij' := leOfHom hij
      simp only [Fin.mk_le_mk] at hij'
      obtain ⟨k, hk⟩ := Nat.le.dest hij'
      exact this k i j hk (by valid)
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i j : ℕ
hj : i + 0 = j
hj' : j ≤ n
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
have hj₁ : i = j
Tactic: simp only [add_zero] at hj
-- Lean 4 proof step from Mathlib.CategoryTheory.ComposableArrows.Basic (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
n m : ℕ
F_1 G_1 F G : ComposableArrows.{v_1, u_1} C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app (⟨i + 1, ⋯⟩ : Fin (n + 1)) = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i j : ℕ
hj_1 : i + 0 = j
hj' : j ≤ n
hj : i = j
⊢ Eq (α := F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
    (app (⟨i, ⋯⟩ : Fin (n + 1)) ≫ G.map' i j ⋯ hj' : F.obj (⟨i, ⋯⟩ : Fin (n + 1)) ⟶ G.obj ⟨j, ⋯⟩)
have zero : ∀ (hj : i + 0 = i) (hj' : i ≤ n),
  Eq (α := F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, sorry⟩)
    (F.map' i i sorry hj' ≫ app ⟨i, sorry⟩ : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, sorry⟩)
    (app (⟨i, sorry⟩ : Fin (n + 1)) ≫ G.map' i i sorry hj' : F.obj (⟨i, sorry⟩ : Fin (n + 1)) ⟶ G.obj ⟨i, sorry⟩)
Tactic: obtain rfl := hj
Cleared hypotheses: j, hj_1, hj', hj