awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
X Y : MorphismProperty.Comma L R P Q W
i : X.toComma (P := P) (Q := Q) (W := W) ⟶ Y.toComma (P := P) (Q := Q) (W := W)
inst_7 : IsIso i
⊢ Eq (α := Y ⟶ Y)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) (𝟙 Y)
have h : Hom.hom (P := P) (Q := Q) (W := W)
    (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (inv i) ≫ homFromCommaOfIsIso (P := P) (Q := Q) (W := W) i) =
  Hom.hom (P := P) (Q := Q) (W := W) (𝟙 Y)
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst_5 : IsIso f
⊢ Hom.hom (P := P) (Q := Q) (W := W) (inv f) = inv (Hom.hom (P := P) (Q := Q) (W := W) f)
have hom_inv_id : Hom.hom (P := P) (Q := Q) (W := W) f ≫ Hom.hom (P := P) (Q := Q) (W := W) (inv f) =
  𝟙 (X.toComma (P := P) (Q := Q) (W := W))
Tactic: apply IsIso.eq_inv_of_hom_inv_id
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst_5 : IsIso f
⊢ Hom.hom (P := P) (Q := Q) (W := W) f ≫ Hom.hom (P := P) (Q := Q) (W := W) (inv f) =
    𝟙 (X.toComma (P := P) (Q := Q) (W := W))
have hom_inv_id : Hom.hom (P := P) (Q := Q) (W := W) (f ≫ inv f) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
Tactic: rw [← comp_hom, IsIso.hom_inv_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst_5 : IsIso f
hom_inv_id : Hom.hom (P := P) (Q := Q) (W := W) (f ≫ inv f) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
⊢ Hom.hom (P := P) (Q := Q) (W := W) f ≫ Hom.hom (P := P) (Q := Q) (W := W) (inv f) =
    𝟙 (X.toComma (P := P) (Q := Q) (W := W))
have hom_inv_id₁ : Hom.hom (P := P) (Q := Q) (W := W) (𝟙 X) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
Tactic: rw [← comp_hom, IsIso.hom_inv_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f : X ⟶ Y
inst_5 : IsIso f
hom_inv_id : Hom.hom (P := P) (Q := Q) (W := W) (f ≫ inv f) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
hom_inv_id₁ : Hom.hom (P := P) (Q := Q) (W := W) (𝟙 X) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
⊢ Hom.hom (P := P) (Q := Q) (W := W) f ≫ Hom.hom (P := P) (Q := Q) (W := W) (inv f) =
    𝟙 (X.toComma (P := P) (Q := Q) (W := W))
have hom_inv_id₂ : 𝟙 (X.toComma (P := P) (Q := Q) (W := W)) = 𝟙 (X.toComma (P := P) (Q := Q) (W := W))
Tactic: rw [← comp_hom, IsIso.hom_inv_id, id_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
inst_5 : Q.RespectsIso
inst_6 : W.RespectsIso
A_1 B_1 : MorphismProperty.Comma L R P Q W
f : A_1 ⟶ B_1
hf : IsIso (Hom.hom (P := P) (Q := Q) (W := W) f)
⊢ IsIso f
have rw : IsIso (homFromCommaOfIsIso (P := P) (Q := Q) (W := W) (Hom.hom (P := P) (Q := Q) (W := W) f))
Tactic: rw [← hom_homFromCommaOfIsIso f]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.toComma (P := P) (Q := Q) (W := W).left = Y.toComma (P := P) (Q := Q) (W := W).left
have rw : Y.toComma (P := P) (Q := Q) (W := W).left = Y.toComma (P := P) (Q := Q) (W := W).left
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ CommaMorphism.left (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom h)) = eqToHom ⋯
have subst : CommaMorphism.left (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom sorry)) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.toComma (P := P) (Q := Q) (W := W).right = Y.toComma (P := P) (Q := Q) (W := W).right
have rw : Y.toComma (P := P) (Q := Q) (W := W).right = Y.toComma (P := P) (Q := Q) (W := W).right
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P : MorphismProperty.{v_3, u_3} T
Q : MorphismProperty.{v_1, u_1} A
W : MorphismProperty.{v_2, u_2} B
inst_3 : Q.IsMultiplicative
inst_4 : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ CommaMorphism.right (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom h)) = eqToHom ⋯
have subst : CommaMorphism.right (Hom.toCommaMorphism (P := P) (Q := Q) (W := W) (eqToHom sorry)) = eqToHom sorry
Tactic: subst h
Cleared hypotheses: Y, h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
B : Type u_2
inst_1 : Category.{v_2, u_2} B
T : Type u_3
inst_2 : Category.{v_3, u_3} T
L : Functor.{v_1, v_3, u_1, u_3} A T
R : Functor.{v_2, v_3, u_2, u_3} B T
P_1 : MorphismProperty.{v_3, u_3} T
Q_1 : MorphismProperty.{v_1, u_1} A
W_1 : MorphismProperty.{v_2, u_2} B
inst_3 : Q_1.IsMultiplicative
inst_4 : W_1.IsMultiplicative
P P' : MorphismProperty.{v_3, u_3} T
Q Q' : MorphismProperty.{v_1, u_1} A
W W' : MorphismProperty.{v_2, u_2} B
hP : P ≤ P'
hQ : Q ≤ Q'
hW : W ≤ W'
inst_5 : Q.IsMultiplicative
inst_6 : Q'.IsMultiplicative
inst_7 : W.IsMultiplicative
inst_8 : W'.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
f g : X ⟶ Y
h :
  Eq (α :=
    Functor.obj (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) X ⟶
      Functor.obj (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) Y)
    (Functor.map (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) f)
    (Functor.map (changeProp L R (P := P) (P' := P') (Q := Q) (Q' := Q') (W := W) (W' := W') hP hQ hW) g)
⊢ f = g
have h₁ : Hom.hom (P := P) (Q := Q) (W := W) f = Hom.hom (P := P) (Q := Q) (W := W) g
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.toCommaMorphism (P := P) (Q := Q) (W := W).left = g.toCommaMorphism (P := P) (Q := Q) (W := W).left
hr : f.toCommaMorphism (P := P) (Q := Q) (W := W).right = g.toCommaMorphism (P := P) (Q := Q) (W := W).right
⊢ f = g
have h : (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).left
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q W : MorphismProperty.{v_1, u_1} T
inst_1 : Q.IsMultiplicative
inst_2 : W.IsMultiplicative
A B : P.Arrow Q W
f g : A ⟶ B
hl : f.toCommaMorphism (P := P) (Q := Q) (W := W).left = g.toCommaMorphism (P := P) (Q := Q) (W := W).left
hr : f.toCommaMorphism (P := P) (Q := Q) (W := W).right = g.toCommaMorphism (P := P) (Q := Q) (W := W).right
h : (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).left
⊢ f = g
have h₁ : (Comma.Hom.hom (P := P) (Q := Q) (W := W) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := W) g).right
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
⊢ f = g
have h₁ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
h₁ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left
⊢ f = g
have h₂ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).right
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right = g.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right
⊢ f = g
have h₁ : (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) f).left = (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) g).left
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
P Q : MorphismProperty.{v_1, u_1} T
X : T
inst_1 : Q.IsMultiplicative
A B : P.Under Q X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right = g.toCommaMorphism (P := P) (Q := ⊤) (W := Q).right
h₁ : (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) f).left = (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) g).left
⊢ f = g
have h₂ : (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) f).right = (Comma.Hom.hom (P := P) (Q := ⊤) (W := Q) g).right
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
⊢ f = g
have h₁ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
A B : P.CostructuredArrow Q F X
f g : A ⟶ B
h : f.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left = g.toCommaMorphism (P := P) (Q := Q) (W := ⊤).left
h₁ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).left = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).left
⊢ f = g
have h₂ : (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) f).right = (Comma.Hom.hom (P := P) (Q := Q) (W := ⊤) g).right
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Faithful
⊢ (CostructuredArrow.toOver P F X).Faithful
have map_injective : autoParam
  (∀ {X_1 Y : P.CostructuredArrow ⊤ F X}, Function.Injective (α := X_1 ⟶ Y) (CostructuredArrow.toOver P F X).map)
  Functor.Faithful.map_injective._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
⊢ (CostructuredArrow.toOver P F X).Full
have map_surjective : ∀ {X_1 Y : P.CostructuredArrow ⊤ F X}, Function.Surjective (α := X_1 ⟶ Y) (CostructuredArrow.toOver P F X).map
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ ∃ (a : A ⟶ B), (CostructuredArrow.toOver P F X).map a = f
have map_surjective : F.map (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left) ≫ B.toComma (P := P) (Q := ⊤) (W := ⊤).hom =
  A.toComma (P := P) (Q := ⊤) (W := ⊤).hom
Tactic: refine ⟨CostructuredArrow.homMk (F.preimage f.left) trivial ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
map_surjective :
  F.map (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left) ≫ B.toComma (P := P) (Q := ⊤) (W := ⊤).hom =
    A.toComma (P := P) (Q := ⊤) (W := ⊤).hom
⊢ ∃ (a : A ⟶ B), (CostructuredArrow.toOver P F X).map a = f
have map_surjective₁ : (CostructuredArrow.toOver P F X).map
    (CostructuredArrow.homMk (P := P) (Q := ⊤) (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left) trivial
      sorry) =
  f
Tactic: refine ⟨CostructuredArrow.homMk (F.preimage f.left) trivial ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Comma (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_3, u_1} C
inst_1 : Category.{u_4, u_2} D
P : MorphismProperty.{u_4, u_2} D
Q : MorphismProperty.{u_3, u_1} C
inst_2 : Q.IsMultiplicative
F : Functor.{u_3, u_4, u_1, u_2} C D
X : D
inst_3 : F.Full
A B : P.CostructuredArrow ⊤ F X
f : (CostructuredArrow.toOver P F X).obj A ⟶ (CostructuredArrow.toOver P F X).obj B
⊢ (CostructuredArrow.toOver P F X).map
      (CostructuredArrow.homMk (P := P) (Q := ⊤) (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left) trivial
        ⋯) =
    f
have map_surjective : ((CostructuredArrow.toOver P F X).map
          (CostructuredArrow.homMk (P := P) (Q := ⊤) (F.preimage f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left)
            trivial sorry)).toCommaMorphism
      (P := P) (Q := ⊤) (W := ⊤).left =
  f.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve (Functor.obj (Over.forget P ⊤ S) X)
hR :
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) X)))
    ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) X)) R
⊢ ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = R
have hR₁ : ∃ (𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)),
  R = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: rw [Precoverage.mem_iff_exists_zeroHypercover] at hR
Cleared hypotheses: hR
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
R : Presieve (Functor.obj (Over.forget P ⊤ S) X)
hR :
  ∃ (𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)),
    R = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = R
have obtain : ∀ (𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)),
  ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: obtain ⟨𝒰, rfl⟩ := hR
Cleared hypotheses: R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
refine_2 : ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f
⊢ ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f
have refine_1 : ∀ (i : 𝒰.I₀), P (𝒰.X i).hom
Tactic: let 𝒱 : PreZeroHypercover X :=
    ⟨𝒰.I₀, fun i ↦ Over.mk _ (𝒰.X i).hom ?_, fun i ↦ Over.homMk (𝒰.f i).left (by simp) trivial⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
𝒱 : PreZeroHypercover X :=
  { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ Over.mk (P := P) ⊤ (𝒰.X i).hom ⋯,
    f := fun (i : 𝒰.I₀) ↦ Over.homMk (P := P) (Q := ⊤) (Over.Hom.left (𝒰.f i)) ⋯ trivial }
⊢ ∃ (T : Presieve X), Presieve.map (Over.forget P ⊤ S) T = Presieve.ofArrows 𝒰.X 𝒰.f
have h : Presieve.map (Over.forget P ⊤ S) 𝒱.presieve₀ = Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: use 𝒱.presieve₀
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
𝒱 : PreZeroHypercover X :=
  { I₀ := 𝒰.I₀, X := fun (i : 𝒰.I₀) ↦ Over.mk (P := P) ⊤ (𝒰.X i).hom ⋯,
    f := fun (i : 𝒰.I₀) ↦ Over.homMk (P := P) (Q := ⊤) (Over.Hom.left (𝒰.f i)) ⋯ trivial }
⊢ Presieve.map (Over.forget P ⊤ S) 𝒱.presieve₀ = Presieve.ofArrows 𝒰.X 𝒰.f
have h : (Presieve.ofArrows (fun (i : 𝒱.I₀) ↦ Functor.obj (Over.forget P ⊤ S) (𝒱.X i)) fun (i : 𝒱.I₀) ↦
    Functor.map (Over.forget P ⊤ S) (𝒱.f i)) =
  Presieve.ofArrows 𝒰.X 𝒰.f
Tactic: rw [Presieve.map_ofArrows]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
H : K ≤ P.precoverage
X : P.Over ⊤ S
𝒰 : (Precoverage.comap (CategoryTheory.Over.forget S) K).ZeroHypercover (Functor.obj (Over.forget P ⊤ S) X)
i : 𝒰.I₀
⊢ P (𝒰.X i).hom
have refine_1 : P (Over.Hom.left (𝒰.f i) ≫ (Functor.obj (Over.forget P ⊤ S) X).hom)
Tactic: rw [← CategoryTheory.Over.w (𝒰.f i)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S) (K.toGrothendieck.over S)
have rw : Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
  (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
Tactic: rw [over_toGrothendieck_eq_toGrothendieck_comap_forget]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.CommaSites (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : MorphismProperty.{v_1, u_1} C
S : C
inst_1 : P.IsStableUnderComposition
K : Precoverage.{v_1, u_1} C
inst_2 : K.HasIsos
inst_3 : K.IsStableUnderBaseChange
inst_4 : K.IsStableUnderComposition
inst_5 : K.HasPullbacks
H : K ≤ P.precoverage
⊢ Functor.LocallyCoverDense (C := P.Over ⊤ S) (Over.forget P ⊤ S)
    (Precoverage.comap (CategoryTheory.Over.forget S) K).toGrothendieck
have H₁ : ∀ {S_1 : P.Over ⊤ S} {R : Presieve (Functor.obj (Over.forget P ⊤ S) S_1)},
  Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) S_1)))
      ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) S_1)) R →
    Membership.mem (γ := Set (Presieve (Functor.obj (Over.forget P ⊤ S) S_1)))
      ((Precoverage.comap (CategoryTheory.Over.forget S) K).coverings (Functor.obj (Over.forget P ⊤ S) S_1))
      (Presieve.map (Over.forget P ⊤ S) (Presieve.functorPullback (Over.forget P ⊤ S) R))
Tactic: apply Precoverage.locallyCoverDense_of_map_functorPullback_mem