awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f g : X ⟶ Y
h : Relation.EqvGen homRel f g
rel : ∀ (x y : X ⟶ Y) (h : homRel x y), W x ↔ W y
refl : ∀ (x : X ⟶ Y), W x ↔ W x
symm : ∀ (x y : X ⟶ Y), Relation.EqvGen homRel x y → ∀ (h : W x ↔ W y), W y ↔ W x
⊢ W f ↔ W g
have trans : ∀ (x y z : X ⟶ Y),
  Relation.EqvGen homRel x y → Relation.EqvGen homRel y z → ∀ (h₁ : W x ↔ W y) (h₂ : W y ↔ W z), W x ↔ W z
Tactic: induction h with
  | rel _ _ h => exact iff W h
  | refl => rfl
  | symm _ _ _ h => exact h.symm
  | trans _ _ _ _ _ h₁ h₂ => exact h₁.trans h₂
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
⊢ W.quotient homRel ((Quotient.functor homRel).map f) ↔ W f
have refine : W.quotient homRel ((Quotient.functor homRel).map f) →
  ∀
    (f' :
      Quiver.Hom.{v_1, u_1} (V := C) (Quotient.as (r := homRel) ((Quotient.functor homRel).1 X))
        (Quotient.as (r := homRel) ((Quotient.functor homRel).1 Y)))
    (hf' : W f') (h : (Quotient.functor homRel).map f = (Quotient.functor homRel).map f'), W f
Tactic: refine ⟨fun ⟨f', hf', h⟩ ↦ ?_, fun hf ↦ ⟨f, hf, rfl⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Quotient (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
h_1 : W.quotient homRel ((Quotient.functor homRel).map f)
f' :
  Quiver.Hom.{v_1, u_1} (V := C) (Quotient.as (r := homRel) ((Quotient.functor homRel).1 X))
    (Quotient.as (r := homRel) ((Quotient.functor homRel).1 Y))
hf' : W f'
h : (Quotient.functor homRel).map f = (Quotient.functor homRel).map f'
⊢ W f
have h₁ : Relation.EqvGen homRel f f'
Tactic: rw [← Functor.homRel_iff, Quotient.functor_homRel_eq_compClosure_eqvGen,
    HomRel.compClosure_eq_self homRel] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Quotient (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
homRel : HomRel.{u_1, v_1} C
inst_1 : HomRel.IsStableUnderPrecomp homRel
inst_2 : HomRel.IsStableUnderPostcomp homRel
inst_3 : W.HasQuotient homRel
⊢ W = (W.quotient homRel).inverseImage (Quotient.functor homRel)
have h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ (W.quotient homRel).inverseImage (Quotient.functor homRel) f
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : HasPullbacks.{v₁, u₁} C
a b : C
f : a ⟶ b
inst_4 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : F.obj c ⟶ F.obj b
⊢ ∃ (b_1 : C) (snd : b_1 ⟶ c) (fst : F.obj b_1 ⟶ F.obj a), IsPullback fst (F.map snd) (F.map f) g
have obtain : ∀ (g : c ⟶ b), ∃ (b_1 : C) (snd : b_1 ⟶ c) (fst : F.obj b_1 ⟶ F.obj a), IsPullback fst (F.map snd) (F.map f) (F.map g)
Tactic: obtain ⟨g, rfl⟩ := F.map_surjective g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
inst_3 : HasPullbacks.{v₁, u₁} C
a b : C
f : a ⟶ b
inst_4 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
c : C
g : c ⟶ b
⊢ ∃ (b_1 : C) (snd : b_1 ⟶ c) (fst : F.obj b_1 ⟶ F.obj a), IsPullback fst (F.map snd) (F.map f) (F.map g)
have refine : IsPullback (P := F.obj (Limits.pullback f g)) (F.map (pullback.fst f g)) (F.map (pullback.snd f g)) (F.map f) (F.map g)
Tactic: refine ⟨Limits.pullback f g, Limits.pullback.snd f g, F.map (Limits.pullback.fst f g), ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ Y'), IsPullback fst (F.map snd) g' h
have refine_1 : F.obj (hg.pullback (h ≫ f)) ⟶ Y'
Tactic: refine ⟨hg.pullback (h ≫ f), hg.snd (h ≫ f), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y Y' X' : D
f : X ⟶ X'
g : Y ⟶ X'
f' : Y' ⟶ Y
g' : Y' ⟶ X
P₁ : IsPullback f' g' g f
hg : F.relativelyRepresentable g
a : C
h : F.obj a ⟶ X
refine_1 : F.obj (hg.pullback (h ≫ f)) ⟶ Y'
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ Y'), IsPullback fst (F.map snd) g' h
have refine_2 : IsPullback (P₁.lift (hg.fst (h ≫ f)) (F.map (hg.snd (h ≫ f)) ≫ h) sorry) (F.map (hg.snd (h ≫ f))) g' h
Tactic: refine ⟨hg.pullback (h ≫ f), hg.snd (h ≫ f), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
⊢ relative F P f
have refine_1 : ∀ (a : C) (g : F.obj a ⟶ Y), ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g
Tactic: refine ⟨fun a g ↦ ?_, fun a b g fst snd h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
refine_1 : ∀ (a : C) (g : F.obj a ⟶ Y), ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g
⊢ relative F P f
have refine_2 : ∀ (a b : C) (g : F.obj a ⟶ Y) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (h : IsPullback fst (F.map snd) f g), P snd
Tactic: refine ⟨fun a g ↦ ?_, fun a b g fst snd h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a : C
g : F.obj a ⟶ Y
⊢ ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g
have refine_1 : ∀ (c : C) (g_fst : F.obj c ⟶ X) (g_snd : c ⟶ a) (BC : IsPullback g_fst (F.map g_snd) f g) (H : P g_snd),
  ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), IsPullback fst (F.map snd) f g
Tactic: obtain ⟨c, g_fst, g_snd, BC, H⟩ := h₀ g
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
⊢ P snd
have refine_2 : ∀ (c : C) (g_fst : F.obj c ⟶ X) (g_snd : c ⟶ a) (BC : IsPullback g_fst (F.map g_snd) f g) (H : P g_snd), P snd
Tactic: obtain ⟨c, g_fst, g_snd, BC, H⟩ := h₀ g
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : P.RespectsIso
f : X ⟶ Y
h₀ :
  ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (fst : F.obj b ⟶ X) (snd : b ⟶ a) (_ : IsPullback fst (F.map snd) f g), P snd
a b : C
g : F.obj a ⟶ Y
fst : F.obj b ⟶ X
snd : b ⟶ a
h : IsPullback fst (F.map snd) f g
c : C
g_fst : F.obj c ⟶ X
g_snd : c ⟶ a
BC : IsPullback g_fst (F.map g_snd) f g
H : P g_snd
⊢ P snd
have refine_2 : Arrow.mk snd ≅ Arrow.mk g_snd
Tactic: refine (P.arrow_mk_iso_iff ?_).2 H
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst_6 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
⊢ relative F P (F.map f)
have h₀ : ∀ ⦃a_1 : C⦄ (g : F.obj a_1 ⟶ F.obj b),
  ∃ (b_1 : C) (fst : F.obj b_1 ⟶ F.obj a) (snd : b_1 ⟶ a_1) (_ : IsPullback fst (F.map snd) (F.map f) g), P snd
Tactic: apply relative.of_exists
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F.Faithful
inst_3 : F.Full
inst_4 : HasPullbacks.{v₁, u₁} C
inst_5 : P.IsStableUnderBaseChange
a b : C
f : a ⟶ b
inst_6 : ∀ (c : C) (g : c ⟶ b), PreservesLimit (cospan f g) F
hf : P f
Y' : C
g : F.obj Y' ⟶ F.obj b
⊢ ∃ (b_1 : C) (fst : F.obj b_1 ⟶ F.obj a) (snd : b_1 ⟶ Y') (_ : IsPullback fst (F.map snd) (F.map f) g), P snd
have h₀ : ∀ (g : Y' ⟶ b),
  ∃ (b_1 : C) (fst : F.obj b_1 ⟶ F.obj a) (snd : b_1 ⟶ Y') (_ : IsPullback fst (F.map snd) (F.map f) (F.map g)), P snd
Tactic: obtain ⟨g, rfl⟩ := F.map_surjective g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
⊢ relative F_1 P (f ≫ g)
have refine : ∀ (Z X : C) (p : F_1.obj Z ⟶ H) (fst : F_1.obj X ⟶ F) (snd : X ⟶ Z) (h : IsPullback fst (F_1.map snd) (f ≫ g) p), P snd
Tactic: refine ⟨comp_mem _ _ _ hf.1 hg.1, fun Z X p fst snd h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
⊢ P snd
have rw : P (sorry.lift (fst ≫ f) snd sorry ≫ sorry.snd p)
Tactic: rw [← hg.1.lift_snd (fst ≫ f) snd (by simpa using h.w)]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
⊢ P (⋯.lift (fst ≫ f) snd ⋯ ≫ ⋯.snd p)
have refine_1 : IsPullback fst (F_1.map (sorry.lift (fst ≫ f) snd sorry) ≫ F_1.map (sorry.snd p)) (f ≫ g) p
Tactic: refine comp_mem _ _ _ (hf.property (hg.1.fst p) fst _
      (IsPullback.of_bot ?_ ?_ (hg.1.isPullback p))) (hg.property_snd p)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
refine_1 : IsPullback fst (F_1.map (⋯.lift (fst ≫ f) snd ⋯) ≫ F_1.map (⋯.snd p)) (f ≫ g) p
⊢ P (⋯.lift (fst ≫ f) snd ⋯ ≫ ⋯.snd p)
have refine_2 : fst ≫ f = F_1.map (sorry.lift (fst ≫ f) snd sorry) ≫ sorry.fst p
Tactic: refine comp_mem _ _ _ (hf.property (hg.1.fst p) fst _
      (IsPullback.of_bot ?_ ?_ (hg.1.isPullback p))) (hg.property_snd p)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
X_1 Y : D
P : MorphismProperty.{v₁, u₁} C
inst_2 : F_1.Faithful
inst_3 : F_1.Full
inst_4 : P.IsStableUnderComposition
F G H : D
f : F ⟶ G
g : G ⟶ H
hf : relative F_1 P f
hg : relative F_1 P g
Z X : C
p : F_1.obj Z ⟶ H
fst : F_1.obj X ⟶ F
snd : X ⟶ Z
h : IsPullback fst (F_1.map snd) (f ≫ g) p
⊢ fst ≫ f = F_1.map (⋯.lift (fst ≫ f) snd ⋯) ≫ ⋯.fst p
have refine_2 : F_1.map (sorry.lift (fst ≫ f) snd sorry) ≫ sorry.fst p = fst ≫ f
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
⊢ monomorphisms (Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) f
have suffices : ∀ {X : C} {a b : Functor.obj yoneda X ⟶ F}, a ≫ f = b ≫ f → a = b
Tactic: suffices ∀ {X : C} {a b : yoneda.obj X ⟶ F}, a ≫ f = b ≫ f → a = b from
    ⟨fun _ _ h ↦ hom_ext_yoneda (fun _ _ ↦ this (by simp only [assoc, h]))⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
X : C
a b : Functor.obj yoneda X ⟶ F
h : a ≫ f = b ≫ f
⊢ a = b
have suffices : sorry.lift a (𝟙 X) sorry = sorry.lift b (𝟙 X) sorry
Tactic: suffices hf.rep.lift (g := a ≫ f) a (𝟙 X) (by simp) =
      hf.rep.lift b (𝟙 X) (by simp [← h]) by
    simpa using yoneda.congr_map this =≫ (hf.rep.fst (a ≫ f))
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
F G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
f : F ⟶ G
hf : presheaf (monomorphisms C) f
X : C
a b : Functor.obj yoneda X ⟶ F
h : a ≫ f = b ≫ f
⊢ ⋯.lift a (𝟙 X) ⋯ = ⋯.lift b (𝟙 X) ⋯
have this : Mono (sorry.snd (a ≫ f))
Tactic: have : Mono (hf.rep.snd (a ≫ f)) := hf.property_snd (a ≫ f)
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
⊢ ⋯.fst' f = ⋯.snd f
have this : Mono f
Tactic: have := P.presheaf_mono_of_le hP hf
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
this : Mono f
⊢ ⋯.fst' f = ⋯.snd f
have a : Eq (α :=
  Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Functor.obj yoneda (sorry.pullback f))
    (Functor.obj yoneda X))
  (Functor.map yoneda (sorry.fst' f)) (Functor.map yoneda (sorry.snd f))
Tactic: apply yoneda.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
this : Mono f
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Functor.obj yoneda (⋯.pullback f))
      (Functor.obj yoneda X))
    (Functor.map yoneda (⋯.fst' f)) (Functor.map yoneda (⋯.snd f))
have a : Functor.map yoneda (sorry.fst' f) ≫ f = Functor.map yoneda (sorry.snd f) ≫ f
Tactic: rw [← cancel_mono f, (hf.rep.isPullback' f).w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : MorphismProperty.{v₁, u₁} C
G : Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)
hP : P ≤ monomorphisms C
X : C
f : Functor.obj yoneda X ⟶ G
hf : P.presheaf f
this : Mono f
a : Functor.map yoneda (⋯.fst' f) ≫ f = Functor.map yoneda (⋯.snd f) ≫ f
⊢ Eq (α :=
    Quiver.Hom (V := Functor.{v₁, v₁, u₁, v₁ + 1} Cᵒᵖ (Type v₁)) (Functor.obj yoneda (⋯.pullback f))
      (Functor.obj yoneda X))
    (Functor.map yoneda (⋯.fst' f)) (Functor.map yoneda (⋯.snd f))
have a₁ : Functor.map yoneda (sorry.snd f) ≫ f = Functor.map yoneda (sorry.snd f) ≫ f
Tactic: rw [← cancel_mono f, (hf.rep.isPullback' f).w]
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ = φ'
have h₀ : φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
h₀ : φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)
⊢ φ = φ'
have h₄ : φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)
have h₀ : (φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₂ =
  (φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
h₀ :
  (φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₂ =
    (φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₂
⊢ φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)
have h₄ : (φ ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₂ =
  (φ' ≫ pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₂
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
⊢ φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)
have h₄ : (φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₃ =
  (φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : F.Full
A₁ A₂ A₃ : C
X : D
f₁ : F.obj A₁ ⟶ X
hf₁ : F.relativelyRepresentable f₁
f₂ : F.obj A₂ ⟶ X
f₃ : F.obj A₃ ⟶ X
inst_3 : HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)
inst_4 : F.Faithful
Z : C
φ φ' : Z ⟶ hf₁.pullback₃ f₂ f₃
h₁ : φ ≫ p₁ hf₁ f₂ f₃ = φ' ≫ p₁ hf₁ f₂ f₃
h₂ : φ ≫ p₂ hf₁ f₂ f₃ = φ' ≫ p₂ hf₁ f₂ f₃
h₃ : φ ≫ p₃ hf₁ f₂ f₃ = φ' ≫ p₃ hf₁ f₂ f₃
h₄ :
  (φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₃ =
    (φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.fst' f₃
⊢ φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃) = φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)
have h₅ : (φ ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₃ =
  (φ' ≫ pullback.snd (hf₁.fst' f₂) (hf₁.fst' f₃)) ≫ hf₁.snd f₃
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.MorphismProperty.Representable (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasBinaryProducts.{v₁, u₁} C
inst_3 : HasPullbacks.{v₂, u₂} D
inst_4 : HasBinaryProducts.{v₂, u₂} D
inst_5 : HasTerminal.{v₂, u₂} D
inst_6 : F.Full
inst_7 : PreservesLimitsOfShape (Discrete WalkingPair) F
X : D
h : F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X) (Limits.diag X)
a : C
g : F.obj a ⟶ X
⊢ F.relativelyRepresentable g
have rw : ∀
  (h :
    F.relativelyRepresentable (Y := Limits.prod.{v₂, u₂} X X)
      (CategoryStruct.comp (Y :=
        Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
        (pullback.lift (𝟙 X) (𝟙 X) sorry :
          X ⟶ Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X))
        (Iso.inv (prodIsoPullback X X) :
          Limits.pullback.{v₂, u₂} (Z := terminal.{v₂, u₂} D) (terminal.from X) (terminal.from X) ⟶
            Limits.prod.{v₂, u₂} X X)))
  ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
Tactic: rw [(by cat_disch : Limits.diag X = pullback.lift (𝟙 X) (𝟙 X) ≫ (prodIsoPullback X X).inv)] at h
Cleared hypotheses: h, a, g