awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ g = s.snd

Tactic:
have H₂ : s.fst ≫ g = s.snd := by simpa using congr($s.condition ≫ prod.snd)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
H₂ : s.fst ≫ g = s.snd
⊢ s.fst ≫ f = s.fst ≫ g

Tactic:
H₁.trans H₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
H₂ : s.fst ≫ g = s.snd
⊢ s.fst ≫ f = s.fst ≫ g

Tactic:
exact H₁.trans H₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g) = s.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
    CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g) = s.fst

Tactic:
exact fun s ↦ by simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g ≫ f) = s.snd

Tactic:
simpa using congr($s.condition ≫ prod.fst)

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.Limits.prod.fst
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))),
    CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g ≫ f) = s.snd

Tactic:
exact fun s ↦ by simpa using congr($s.condition ≫ prod.fst)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
m : s.pt ⟶ equalizer f g
hm : m ≫ equalizer.ι f g = s.fst
h_1 : m ≫ equalizer.ι f g ≫ f = s.snd
h : m ≫ equalizer.ι f g = CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g)
⊢ m = equalizer.lift s.fst ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
m : s.pt ⟶ equalizer f g
hm : m ≫ equalizer.ι f g = s.fst
h : m ≫ equalizer.ι f g ≫ f = s.snd
⊢ m ≫ equalizer.ι f g = CategoryStruct.comp (Y := equalizer f g) (equalizer.lift s.fst ⋯) (equalizer.ι f g)

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasEqualizer f g
inst_2 : HasBinaryProduct.{v, u} Y Y
⊢ ∀ (s : PullbackCone (Z := prod.{v, u} Y Y) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) (m : s.pt ⟶ equalizer f g),
    m ≫ equalizer.ι f g = s.fst → m ≫ equalizer.ι f g ≫ f = s.snd → m = equalizer.lift s.fst ⋯

Tactic:
exact fun s m hm _ ↦ by ext; simp [*]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
h₁ :
  Eq (α := X ⟶ coequalizer f g)
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc f g ≫ coequalizer.π f g))
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g))
h₂ :
  Eq (α := X ⟶ coequalizer f g)
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc f g ≫ coequalizer.π f g))
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g))
⊢ Eq (α := coprod.{v, u} X X ⟶ coequalizer f g) (coprod.desc f g ≫ coequalizer.π f g)
    (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
⊢ Eq (α := X ⟶ coequalizer f g)
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc f g ≫ coequalizer.π f g))
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inl (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g))

Tactic:
simp [coequalizer.condition f g]

Premises used: CategoryTheory.Limits.coequalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
⊢ Eq (α := X ⟶ coequalizer f g)
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc f g ≫ coequalizer.π f g))
    (CategoryStruct.comp (Y := coprod.{v, u} X X) coprod.inr (coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g))

Tactic:
simp [coequalizer.condition f g]

Premises used: CategoryTheory.Limits.coequalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
refine_1 :
  (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt
refine_2 :
  ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inl
refine_3 :
  ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    CategoryStruct.comp (Y := coequalizer f g) (f ≫ coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inr
refine_4 :
  ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X)))
    (m : coequalizer f g ⟶ s.pt),
    coequalizer.π f g ≫ m = s.inl → (f ≫ coequalizer.π f g) ≫ m = s.inr → m = coequalizer.desc s.inl ⋯
⊢ IsPushout (Z := coprod.{v, u} X X) (P := coequalizer f g) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
    (coequalizer.π f g) (f ≫ coequalizer.π f g)

Tactic:
refine ⟨⟨by ext <;> simp [coequalizer.condition f g]⟩, ⟨PushoutCocone.IsColimit.mk _ ?_ ?_ ?_ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
refine_1 :
  ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))), f ≫ s.inl = g ≫ s.inl
⊢ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt

Tactic:
refine fun s ↦ coequalizer.desc s.inl ?_

Premises used: CategoryTheory.Limits.coequalizer.desc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = s.inr

Tactic:
simpa using congr(coprod.inl ≫ $s.condition)

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.Limits.coprod.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = s.inr

Tactic:
have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
⊢ g ≫ s.inl = s.inr

Tactic:
simpa using congr(coprod.inr ≫ $s.condition)

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.Limits.coprod.inr
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
⊢ g ≫ s.inl = s.inr

Tactic:
have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
H₂ : g ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl

Tactic:
H₁.trans H₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
H₂ : g ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl

Tactic:
exact H₁.trans H₂.symm

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
⊢ ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inl

Tactic:
exact fun s ↦ by simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ CategoryStruct.comp (Y := coequalizer f g) (f ≫ coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inr

Tactic:
simpa using congr(coprod.inl ≫ $s.condition)

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.Limits.coprod.inl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
⊢ ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    CategoryStruct.comp (Y := coequalizer f g) (f ≫ coequalizer.π f g) (coequalizer.desc s.inl ⋯) = s.inr

Tactic:
exact fun s ↦ by simpa using congr(coprod.inl ≫ $s.condition)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
m : coequalizer f g ⟶ s.pt
hm : coequalizer.π f g ≫ m = s.inl
h_1 : (f ≫ coequalizer.π f g) ≫ m = s.inr
h : coequalizer.π f g ≫ m = CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl ⋯)
⊢ m = coequalizer.desc s.inl ⋯

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
m : coequalizer f g ⟶ s.pt
hm : coequalizer.π f g ≫ m = s.inl
h : (f ≫ coequalizer.π f g) ≫ m = s.inr
⊢ coequalizer.π f g ≫ m = CategoryStruct.comp (Y := coequalizer f g) (coequalizer.π f g) (coequalizer.desc s.inl ⋯)

Tactic:
simp [*]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst_1 : HasCoequalizer f g
inst_2 : HasBinaryCoproduct.{v, u} X X
⊢ ∀ (s : PushoutCocone (X := coprod.{v, u} X X) (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X)))
    (m : coequalizer f g ⟶ s.pt),
    coequalizer.π f g ≫ m = s.inl → (f ≫ coequalizer.π f g) ≫ m = s.inr → m = coequalizer.desc s.inl ⋯

Tactic:
exact fun s m hm _ ↦ by ext; simp [*]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ s ≫ 𝟙 S = f ≫ t

Tactic:
simp [hf]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ s ≫ 𝟙 S = g ≫ t

Tactic:
simp [hg]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ v ≫ 𝟙 S = 𝟙 T ≫ v

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
⊢ pullback.fst s v ≫ f = lhs ≫ pullback.fst t v

Tactic:
simp [lhs]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
⊢ pullback.fst s v ≫ g = rhs ≫ pullback.fst t v

Tactic:
simp [rhs]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ Eq (α := equalizer lhs rhs ⟶ Y) ((equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ f)
    ((equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ g)

Tactic:
simp [hl, hr, equalizer.condition_assoc lhs rhs]

Premises used: CategoryTheory.Limits.equalizer.condition_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ Eq (α := equalizer lhs rhs ⟶ S) ((equalizer.ι lhs rhs ≫ pullback.fst s v) ≫ s)
    ((equalizer.ι lhs rhs ≫ pullback.snd s v) ≫ v)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ Eq (α := equalizer lhs rhs ⟶ X)
    (CategoryStruct.comp (Y := equalizer f g) (equalizer.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) ⋯)
      (equalizer.ι f g))
    (CategoryStruct.comp (Y := pullback s v)
      (pullback.lift (equalizer.ι lhs rhs ≫ pullback.fst s v) (equalizer.ι lhs rhs ≫ pullback.snd s v) ⋯)
      (pullback.fst s v))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ Eq (α := pullback s v ⟶ S) (pullback.fst s v ≫ s) (pullback.snd s v ≫ v)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
h₀ :
  Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ Y)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.fst t v)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.fst t v)
h₁ :
  Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.snd t v)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.snd t v)
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ pullback t v)
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs)
    (pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ Y)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.fst t v)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.fst t v)

Tactic:
simp [lhs, rhs, equalizer.condition f g]

Premises used: CategoryTheory.Limits.equalizer.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 : C
f_1 g_1 : X_1 ⟶ Y_1
inst_1 : HasEqualizers.{v, u} C
inst_2 : HasPullbacks.{v, u} C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
lhs : pullback s v ⟶ pullback t v := pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯
rhs : pullback s v ⟶ pullback t v := pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯
hl : pullback.fst s v ≫ f = lhs ≫ pullback.fst t v
hr : pullback.fst s v ≫ g = rhs ≫ pullback.fst t v
⊢ Eq (α := pullback (X := equalizer f g) (Y := pullback s v) (equalizer.ι f g) (pullback.fst s v) ⟶ T)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ lhs) ≫
      pullback.snd t v)
    ((pullback.map (equalizer.ι f g) (pullback.fst s v) s v (equalizer.ι f g) (pullback.snd s v) s ⋯ ⋯ ≫ rhs) ≫
      pullback.snd t v)

Tactic:
simp [lhs, rhs, equalizer.condition f g]

Premises used: CategoryTheory.Limits.equalizer.condition