-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equalizer.lean
/-- The coequalizer of `f g : X ⟶ Y` is the pushout of the diagonal map `X ⨿ X ⟶ X`
along the map `(f, g) : X ⨿ X ⟶ Y`. -/
lemma isPushout_coequalizer_coprod [HasCoequalizer f g] [HasBinaryCoproduct X X] :
    IsPushout (coprod.desc f g) (coprod.desc (𝟙 _) (𝟙 _))
      (coequalizer.π f g) (f ≫ coequalizer.π f g)

Proof state:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ ∀ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    coequalizer.π f g ≫ coequalizer.desc s.inl ⋯ = s.inl

Tactic:
exact fun s ↦ by 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✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt

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

Result:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = g ≫ s.inl

Proof state:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = g ≫ s.inl

Tactic:
have H₁ : f ≫ s.inl = s.inr := by simpa using congr(coprod.inl ≫ $s.condition)

Result:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
m : coequalizer f g ⟶ s.pt
hm : coequalizer.π f g ≫ m = s.inl
x✝ : (f ≫ coequalizer.π f g) ≫ m = s.inr
⊢ m = coequalizer.desc s.inl ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
m : coequalizer f g ⟶ s.pt
hm : coequalizer.π f g ≫ m = s.inl
x✝ : (f ≫ coequalizer.π f g) ≫ m = s.inr
⊢ coequalizer.π f g ≫ m = coequalizer.π f g ≫ coequalizer.desc s.inl ⋯

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ IsPushout (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 _ ?_ ?_ ?_ ?_⟩⟩

Result:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))) → coequalizer f g ⟶ s.pt

case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ ∀ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))), coequalizer.π f g ≫ ?refine_1 s = s.inl

case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ ∀ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))), (f ≫ coequalizer.π f g) ≫ ?refine_1 s = s.inr

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

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ coprod.desc f g ≫ coequalizer.π f g = coprod.desc (𝟙 X) (𝟙 X) ≫ f ≫ coequalizer.π f g

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

Result:
no goals

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

Result:
no goals

Proof state:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
H₁ : f ≫ s.inl = s.inr
⊢ f ≫ s.inl = g ≫ s.inl

Tactic:
have H₂ : g ≫ s.inl = s.inr := by simpa using congr(coprod.inr ≫ $s.condition)

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

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ f ≫ s.inl = s.inr

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

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ (f ≫ coequalizer.π f g) ≫ coequalizer.desc s.inl ⋯ = s.inr

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

Result:
no goals

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

Result:
no goals

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
m : coequalizer f g ⟶ s.pt
hm : coequalizer.π f g ≫ m = s.inl
x✝ : (f ≫ coequalizer.π f g) ≫ m = s.inr
⊢ coequalizer.π f g ≫ m = coequalizer.π f g ≫ coequalizer.desc s.inl ⋯

Tactic:
simp [*]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))
⊢ coequalizer.π f g ≫ coequalizer.desc s.inl ⋯ = s.inl

Tactic:
simp

Result:
no goals

Proof state:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
⊢ ∀ (s : PushoutCocone (coprod.desc f g) (coprod.desc (𝟙 X) (𝟙 X))),
    (f ≫ coequalizer.π f g) ≫ coequalizer.desc s.inl ⋯ = s.inr

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

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
inst✝ : HasBinaryCoproduct X X
s : PushoutCocone (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)

Result:
no goals