-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equalizer.lean
/-- The equalizer of `f g : X ⟶ Y` is the pullback of the diagonal map `Y ⟶ Y × Y`
along the map `(f, g) : X ⟶ Y × Y`. -/
lemma isPullback_equalizer_prod [HasEqualizer f g] [HasBinaryProduct Y Y] :
    IsPullback (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g) (prod.lift (𝟙 _) (𝟙 _))

Proof state:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g

Tactic:
refine fun s ↦ equalizer.lift s.fst ?_

Result:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ s.fst ≫ f = s.fst ≫ g

Proof state:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ s.fst ≫ f = s.fst ≫ g

Tactic:
have H₁ : s.fst ≫ f = s.snd := by simpa using congr($s.condition ≫ prod.fst)

Result:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ f = s.fst ≫ g

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
m : s.pt ⟶ equalizer f g
hm : m ≫ equalizer.ι f g = s.fst
x✝ : m ≫ equalizer.ι f g ≫ f = s.snd
⊢ m ≫ equalizer.ι f g = equalizer.lift s.fst ⋯ ≫ equalizer.ι f g

Tactic:
simp [*]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ equalizer.lift s.fst ⋯ ≫ equalizer.ι f g ≫ f = s.snd

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

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ g = s.snd

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

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
H₁ : s.fst ≫ f = s.snd
⊢ s.fst ≫ f = s.fst ≫ g

Tactic:
have H₂ : s.fst ≫ g = s.snd := by simpa using congr($s.condition ≫ prod.snd)

Result:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (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

Proof state:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), equalizer.lift s.fst ⋯ ≫ equalizer.ι f g ≫ f = s.snd

Tactic:
exact fun s ↦ by simpa using congr($s.condition ≫ prod.fst)

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
m : s.pt ⟶ equalizer f g
hm : m ≫ equalizer.ι f g = s.fst
x✝ : m ≫ equalizer.ι f g ≫ f = s.snd
⊢ m = equalizer.lift s.fst ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
m : s.pt ⟶ equalizer f g
hm : m ≫ equalizer.ι f g = s.fst
x✝ : m ≫ equalizer.ι f g ≫ f = s.snd
⊢ m ≫ equalizer.ι f g = equalizer.lift s.fst ⋯ ≫ equalizer.ι f g

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ IsPullback (equalizer.ι f g) (equalizer.ι f g ≫ f) (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))

Tactic:
refine ⟨⟨by ext <;> simp [equalizer.condition f g]⟩, ⟨PullbackCone.IsLimit.mk _ ?_ ?_ ?_ ?_⟩⟩

Result:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))) → s.pt ⟶ equalizer f g

case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), ?refine_1 s ≫ equalizer.ι f g = s.fst

case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), ?refine_1 s ≫ equalizer.ι f g ≫ f = s.snd

case refine_4
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (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 = ?refine_1 s

Proof state:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))), equalizer.lift s.fst ⋯ ≫ equalizer.ι f g = s.fst

Tactic:
exact fun s ↦ by simp

Result:
no goals

Proof state:
case refine_4
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ ∀ (s : PullbackCone (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 [*]

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (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

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
⊢ equalizer.ι f g ≫ prod.lift f g = (equalizer.ι f g ≫ f) ≫ prod.lift (𝟙 Y) (𝟙 Y)

Tactic:
ext <;> simp [equalizer.condition f g]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ s.fst ≫ f = s.snd

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

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasEqualizer f g
inst✝ : HasBinaryProduct Y Y
s : PullbackCone (prod.lift f g) (prod.lift (𝟙 Y) (𝟙 Y))
⊢ equalizer.lift s.fst ⋯ ≫ equalizer.ι f g = s.fst

Tactic:
simp

Result:
no goals