awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X A₁ A₂ : C
i₁ : A₁ ⟶ X
i₂ : A₂ ⟶ X
inst_1 : Mono i₁
inst_2 : Mono i₂
f : A₁ ⟶ A₂
fac : f ≫ i₂ = i₁
hf : ¬IsIso f
h : mk i₁ = mk i₂
h₁ : f ≫ i₂ = (isoOfMkEqMk i₁ i₂ h).hom ≫ i₂
h₂ : f ≫ i₂ = ofMkLEMk i₁ i₂ ⋯ ≫ i₂
h₃ : f ≫ i₂ = i₁
⊢ f = (isoOfMkEqMk i₁ i₂ h).hom
have h₄ : i₁ = i₁
Tactic: rw [← cancel_mono i₂, isoOfMkEqMk_hom, ofMkLEMk_comp, fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P Q : MonoOver.{v₁, u₁} X
f : P ⟶ Q
⊢ IsIso f ↔ Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
have rw : IsIso (Over.Hom.left f.hom) ↔ Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
Tactic: rw [isIso_iff_isIso_hom_left, isIso_hom_left_iff_subobjectMk_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
P Q : MonoOver.{v₁, u₁} X
f : P ⟶ Q
rw :
  IsIso (Over.Hom.left f.hom) ↔
    Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
⊢ IsIso f ↔ Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
have rw₁ : Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom ↔
  Subobject.mk P.obj (P := Over.isMono X).hom = Subobject.mk Q.obj (P := Over.isMono X).hom
Tactic: rw [isIso_iff_isIso_hom_left, isIso_hom_left_iff_subobjectMk_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ 𝟭 (Subobject.{v₁, u₁} A) ≅ lower e.functor ⋙ lower e.inverse
have p : 𝟭 (Subobject.{v₁, u₁} A) = lower e.functor ⋙ lower e.inverse
Tactic: apply eqToIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ 𝟭 (Subobject.{v₁, u₁} A) = lower e.functor ⋙ lower e.inverse
have h : Eq (α := Subobject.{v₁, u₁} A ⥤ Subobject.{v₁, u₁} A) (𝟭 (Subobject.{v₁, u₁} A))
  (ThinSkeleton.map (𝟭 (MonoOver.{v₁, u₁} A)))
Tactic: convert! ThinSkeleton.map_iso_eq e.unitIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
h :
  Eq (α := Subobject.{v₁, u₁} A ⥤ Subobject.{v₁, u₁} A) (𝟭 (Subobject.{v₁, u₁} A))
    (ThinSkeleton.map (𝟭 (MonoOver.{v₁, u₁} A)))
⊢ 𝟭 (Subobject.{v₁, u₁} A) = lower e.functor ⋙ lower e.inverse
have h₁ : lower e.functor ⋙ lower e.inverse = ThinSkeleton.map (e.functor ⋙ e.inverse)
Tactic: convert! ThinSkeleton.map_iso_eq e.unitIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ lower e.inverse ⋙ lower e.functor ≅ 𝟭 (Subobject.{v₂, u₂} B)
have p : lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject.{v₂, u₂} B)
Tactic: apply eqToIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
⊢ lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject.{v₂, u₂} B)
have h : lower e.inverse ⋙ lower e.functor = ThinSkeleton.map (e.inverse ⋙ e.functor)
Tactic: convert! ThinSkeleton.map_iso_eq e.counitIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
A : C
B : D
e : MonoOver.{v₁, u₁} A ≌ MonoOver.{v₂, u₂} B
h : lower e.inverse ⋙ lower e.functor = ThinSkeleton.map (e.inverse ⋙ e.functor)
⊢ lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject.{v₂, u₂} B)
have h₁ : Eq (α := Subobject.{v₂, u₂} B ⥤ Subobject.{v₂, u₂} B) (𝟭 (Subobject.{v₂, u₂} B))
  (ThinSkeleton.map (𝟭 (MonoOver.{v₂, u₂} B)))
Tactic: convert! ThinSkeleton.map_iso_eq e.counitIso
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
inst_1 : HasPullbacks.{v₁, u₁} C
x : Subobject.{v₁, u₁} X
⊢ Functor.obj (pullback (𝟙 X)) x = x
have h : ∀ (f : MonoOver.{v₁, u₁} X), Functor.obj (pullback (𝟙 X)) (Quotient.mk'' f) = Quotient.mk'' f
Tactic: induction x using Quotient.inductionOn' with | _ f
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
g : Y ⟶ Z
x : Subobject.{v₁, u₁} Z
⊢ (pullback (f ≫ g)).obj x = (pullback f).obj ((pullback g).obj x)
have h : ∀ (t : MonoOver.{v₁, u₁} Z),
  (pullback (f ≫ g)).obj (Quotient.mk'' t) = (pullback f).obj ((pullback g).obj (Quotient.mk'' t))
Tactic: induction x using Quotient.inductionOn' with | _ t
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
f : Y ⟶ X
x : Subobject.{v₁, u₁} X
⊢ (pullback f).obj x = mk (A := Limits.pullback x.arrow f) (pullback.snd x.arrow f)
have obtain : ∀ (Z : C) (i : Z ⟶ X) (w : Mono i),
  (pullback f).obj (mk i) = mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)
Tactic: obtain ⟨Z, i, _, rfl⟩ := mk_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w : Mono i
⊢ (pullback f).obj (mk i) = mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)
have rw : mk (A := Limits.pullback i f) (pullback.snd i f) =
  mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)
Tactic: rw [pullback_obj_mk (IsPullback.of_hasPullback i f)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
y : Subobject.{v₁, u₁} Y
⊢ ∃ (φ : Functor.obj underlying ((pullback f).obj y) ⟶ Functor.obj underlying y),
    IsPullback φ ((pullback f).obj y).arrow y.arrow f
have obtain : ∀ (A : C) (i : A ⟶ Y) (w : Mono i),
  ∃ (φ : Functor.obj underlying ((pullback f).obj (mk i)) ⟶ Functor.obj underlying (mk i)),
    IsPullback φ ((pullback f).obj (mk i)).arrow (mk i).arrow f
Tactic: obtain ⟨A, i, ⟨_, rfl⟩⟩ := mk_surjective y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
A : C
i : A ⟶ Y
w : Mono i
⊢ ∃ (φ : Functor.obj underlying ((pullback f).obj (mk i)) ⟶ Functor.obj underlying (mk i)),
    IsPullback φ ((pullback f).obj (mk i)).arrow (mk i).arrow f
have rw : ∃ (φ :
  Functor.obj underlying (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)) ⟶
    Functor.obj underlying (mk i)),
  IsPullback φ (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f
Tactic: rw [pullback_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
A : C
i : A ⟶ Y
w : Mono i
⊢ ∃ (φ :
    Functor.obj underlying (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)) ⟶
      Functor.obj underlying (mk i)),
    IsPullback φ (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f
have exists : IsPullback (Iso.hom (underlyingIso (pullback.snd (mk i).arrow f)) ≫ pullback.fst (mk i).arrow f)
  (mk (A := Limits.pullback (mk i).arrow f) (pullback.snd (mk i).arrow f)).arrow (mk i).arrow f
Tactic: exists (underlyingIso (pullback.snd (mk i).arrow f)).hom ≫ pullback.fst (mk i).arrow f
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
x : Subobject.{v₁, u₁} X
⊢ Functor.obj (map (𝟙 X)) x = x
have h : ∀ (f : MonoOver.{v₁, u₁} X), Functor.obj (map (𝟙 X)) (Quotient.mk'' f) = Quotient.mk'' f
Tactic: induction x using Quotient.inductionOn' with | _ f
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : Mono f
inst_2 : Mono g
x : Subobject.{v₁, u₁} X
⊢ (map (f ≫ g)).obj x = (map g).obj ((map f).obj x)
have h : ∀ (t : MonoOver.{v₁, u₁} X), (map (f ≫ g)).obj (Quotient.mk'' t) = (map g).obj ((map f).obj (Quotient.mk'' t))
Tactic: induction x using Quotient.inductionOn' with | _ t
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
X₁ X₂ : Subobject.{v₁, u₁} X
h : (map f).obj X₁ = (map f).obj X₂
⊢ X₁ = X₂
have h₁ : ∀ ⦃A : C⦄ (f_1 : A ⟶ X) [inst_2 : Mono f_1] (h : (map f).obj (mk f_1) = (map f).obj X₂), mk f_1 = X₂
Tactic: induction X₁ using Subobject.ind
Cleared hypotheses: X₁, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst_1 : Mono f
X₂ : Subobject.{v₁, u₁} X
A : C
f_1 : A ⟶ X
inst_2 : Mono f_1
h : (map f).obj (mk f_1) = (map f).obj X₂
⊢ mk f_1 = X₂
have h₁ : ∀ ⦃A_1 : C⦄ (f_2 : A_1 ⟶ X) [inst_3 : Mono f_2] (h : (map f).obj (mk f_1) = (map f).obj (mk f_2)), mk f_1 = mk f_2
Tactic: induction X₂ using Subobject.ind
Cleared hypotheses: X₂, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject.{v₁, u₁} X
⊢ (map e.inv).obj ((map e.hom).obj g) = g
have simp_rw : (map (e.hom ≫ e.inv)).obj g = g
Tactic: simp_rw [← map_comp, e.hom_inv_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject.{v₁, u₁} X
simp_rw : (map (e.hom ≫ e.inv)).obj g = g
⊢ (map e.inv).obj ((map e.hom).obj g) = g
have simp_rw₁ : Functor.obj (map (𝟙 X)) g = g
Tactic: simp_rw [← map_comp, e.hom_inv_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject.{v₁, u₁} Y
⊢ (map e.hom).obj ((map e.inv).obj g) = g
have simp_rw : (map (e.inv ≫ e.hom)).obj g = g
Tactic: simp_rw [← map_comp, e.inv_hom_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
g : Subobject.{v₁, u₁} Y
simp_rw : (map (e.inv ≫ e.hom)).obj g = g
⊢ (map e.hom).obj ((map e.inv).obj g) = g
have simp_rw₁ : Functor.obj (map (𝟙 Y)) g = g
Tactic: simp_rw [← map_comp, e.inv_hom_id, map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
⊢ LE.le (α := Subobject.{v₁, u₁} Y)
      (({ toFun := (map e.hom).obj, invFun := (map e.inv).obj, left_inv := ⋯, right_inv := ⋯ :
              Subobject.{v₁, u₁} X ≃ Subobject.{v₁, u₁} Y } :
            (a : Subobject X) → Subobject Y)
          A :
        Subobject.{v₁, u₁} Y)
      (({ toFun := (map e.hom).obj, invFun := (map e.inv).obj, left_inv := ⋯, right_inv := ⋯ :
              Subobject.{v₁, u₁} X ≃ Subobject.{v₁, u₁} Y } :
            (a : Subobject X) → Subobject Y)
          B :
        Subobject.{v₁, u₁} Y) ↔
    A ≤ B
have dsimp : (map e.hom).obj A ≤ (map e.hom).obj B ↔ A ≤ B
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
⊢ (map e.hom).obj A ≤ (map e.hom).obj B ↔ A ≤ B
have mp : (map e.hom).obj A ≤ (map e.hom).obj B → A ≤ B
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
mp : (map e.hom).obj A ≤ (map e.hom).obj B → A ≤ B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B ↔ A ≤ B
have mpr : A ≤ B → (map e.hom).obj A ≤ (map e.hom).obj B
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : (map e.hom).obj A ≤ (map e.hom).obj B
⊢ A ≤ B
have mp : ∀ (h : (map e.inv).obj ((map e.hom).obj A) ≤ (map e.inv).obj ((map e.hom).obj B)), A ≤ B
Tactic: apply_fun (map e.inv).obj at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : (map e.hom).obj A ≤ (map e.hom).obj B
mp : ∀ (h : (map e.inv).obj ((map e.hom).obj A) ≤ (map e.inv).obj ((map e.hom).obj B)), A ≤ B
⊢ A ≤ B
have apply_fun : Monotone (map e.inv).obj
Tactic: apply_fun (map e.inv).obj at h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : A ≤ B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B
have mpr : ∀ (h : (map e.hom).obj A ≤ (map e.hom).obj B), (map e.hom).obj A ≤ (map e.hom).obj B
Tactic: apply_fun (map e.hom).obj at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
e : X ≅ Y
A B : Subobject.{v₁, u₁} X
h : A ≤ B
mpr : ∀ (h : (map e.hom).obj A ≤ (map e.hom).obj B), (map e.hom).obj A ≤ (map e.hom).obj B
⊢ (map e.hom).obj A ≤ (map e.hom).obj B
have apply_fun : Monotone (map e.hom).obj
Tactic: apply_fun (map e.hom).obj at h
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
inst_1 : HasPullbacks.{v₁, u₁} C
f : X ⟶ Y
inst_2 : Mono f
g : Subobject.{v₁, u₁} X
⊢ (pullback f).obj ((map f).obj g) = g
have revert : ∀ (g : Subobject.{v₁, u₁} X), (pullback f).obj ((map f).obj g) = g
Tactic: revert g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
p : Subobject.{v₁, u₁} Y
⊢ (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
have revert : ∀ (p : Subobject.{v₁, u₁} Y), (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
Tactic: revert p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ ∀ (p : Subobject.{v₁, u₁} Y), (map g).obj ((pullback f).obj p) = (pullback k).obj ((map h).obj p)
have h₁ : ∀ (a : MonoOver.{v₁, u₁} Y),
  (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
Tactic: apply Quotient.ind'
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ (map g).obj ((pullback f).obj (Quotient.mk'' a)) = (pullback k).obj ((map h).obj (Quotient.mk'' a))
have h₁ : (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
Tactic: apply Quotient.sound
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
have h₁ : (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
Tactic: apply ThinSkeleton.equiv_of_both_ways
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ : (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ≈ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
have h₂ : (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)
Tactic: apply ThinSkeleton.equiv_of_both_ways
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ (MonoOver.map g).obj ((MonoOver.pullback f).obj a) ⟶ (MonoOver.pullback k).obj ((MonoOver.map h).obj a)
have h₁ : pullback.fst (Functor.obj (MonoOver.forget Y) a).hom f ≫
    (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom =
  ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow ≫ k
Tactic: refine MonoOver.homMk (pullback.lift (pullback.fst _ _) _ ?_) (pullback.lift_snd _ _ _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)
have h₁ : Eq (α := ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).obj (P := Over.isMono Z).left ⟶ W)
  ((pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
      (Functor.obj (MonoOver.forget Y) a).hom) ≫
    h)
  (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ k)
Tactic: refine MonoOver.homMk (pullback.lift (pullback.fst _ _)
      (PullbackCone.IsLimit.lift t (pullback.fst _ _ ≫ a.arrow) (pullback.snd _ _) _)
      (PullbackCone.IsLimit.lift_fst _ _ _ ?_).symm) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
h₁ :
  Eq (α := ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).obj (P := Over.isMono Z).left ⟶ W)
    ((pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
        (Functor.obj (MonoOver.forget Y) a).hom) ≫
      h)
    (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ k)
⊢ (MonoOver.pullback k).obj ((MonoOver.map h).obj a) ⟶ (MonoOver.map g).obj ((MonoOver.pullback f).obj a)
have h₂ : pullback.lift (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k)
      (PullbackCone.IsLimit.lift t
        (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ a.arrow)
        (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k) sorry)
      sorry ≫
    ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow =
  ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).arrow
Tactic: refine MonoOver.homMk (pullback.lift (pullback.fst _ _)
      (PullbackCone.IsLimit.lift t (pullback.fst _ _ ≫ a.arrow) (pullback.snd _ _) _)
      (PullbackCone.IsLimit.lift_fst _ _ _ ?_).symm) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ Eq (α := ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).obj (P := Over.isMono Z).left ⟶ W)
    ((pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
        (Functor.obj (MonoOver.forget Y) a).hom) ≫
      h)
    (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ k)
have h₁ : Eq (α := ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).obj (P := Over.isMono Z).left ⟶ W)
  (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
    (Functor.obj (MonoOver.forget Y) a).hom ≫ h)
  (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫
    (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom)
Tactic: rw [← pullback.condition, assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ pullback.lift (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k)
        (PullbackCone.IsLimit.lift t
          (pullback.fst (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k ≫ a.arrow)
          (pullback.snd (Functor.obj (MonoOver.forget W) ((MonoOver.map h).obj a)).hom k) ⋯)
        ⋯ ≫
      ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow =
    ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).arrow
have h₁ : Eq (α := Limits.pullback (a.arrow ≫ h) k ⟶ Z)
  (CategoryStruct.comp (Y := Limits.pullback a.arrow f)
    (pullback.lift (pullback.fst (a.arrow ≫ h) k)
      (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) sorry) sorry)
    (pullback.snd a.obj (P := Over.isMono Y).hom f ≫ g))
  (pullback.snd (a.arrow ≫ h) k)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Subobject.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst_2 : Mono h
inst_3 : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver.{v₁, u₁} Y
⊢ Eq (α := Limits.pullback (a.arrow ≫ h) k ⟶ Z)
    (CategoryStruct.comp (Y := Limits.pullback a.arrow f)
      (pullback.lift (pullback.fst (a.arrow ≫ h) k)
        (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯) ⋯)
      (pullback.snd a.obj (P := Over.isMono Y).hom f ≫ g))
    (pullback.snd (a.arrow ≫ h) k)
have h₁ : Eq (α := Limits.pullback (a.arrow ≫ h) k ⟶ Z)
  (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) sorry ≫ g)
  (pullback.snd (a.arrow ≫ h) k)
Tactic: rw [pullback.lift_snd_assoc]