mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (eqToHom ⋯ ≫ f) ≫ g = ((eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f) ≫ eqToHom ⋯) ≫ g

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
F : C ⥤ Cat
G : C ⥤ Type w
E : Type u_1
inst✝ : Category.{v_1, u_1} E
c : C
X✝ Y✝ Z✝ : ↑(F.obj c)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ eqToHom ⋯ ≫ f = (eqToHom ⋯ ≫ (F.map (𝟙 c)).toFunctor.map f) ≫ eqToHom ⋯
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : f p + 0 = 0
this :
  (MvPolynomial.map (algebraMap R A)) p + q ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
⊢ (MvPolynomial.map (algebraMap R A)) p + q ∈ Ideal.span s₀

Tactic:
add_zero

Goal state after:
case refine_2
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R B
inst✝ : FiniteType R A
n : ℕ
f : MvPolynomial (Fin n) R →ₐ[R] B
hf : Surjective ⇑f
s : Finset (MvPolynomial (Fin n) R)
hs : Ideal.span ↑s = RingHom.ker f.toRingHom
RX : Type (max w₁ 0) := MvPolynomial (Fin n) R
AX : Type (max w₂ 0) := MvPolynomial (Fin n) A
t : Finset A
ht : adjoin R ↑t = ⊤
t' : ↥t → MvPolynomial (Fin n) R
ht' : ∀ (i : ↥t), f (t' i) = (algebraMap A B) ↑i
ht'' : adjoin R (⇑(algebraMap A AX) '' ↑t ∪ Set.range MvPolynomial.X) = ⊤
g : ↥t → AX := fun x ↦ MvPolynomial.C ↑x - (MvPolynomial.map (algebraMap R A)) (t' x)
s₀✝ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
I : Ideal (MvPolynomial (Fin n) A) := RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
leI :
  Ideal.span (⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g) ≤
    RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X))
s₀ : Set (MvPolynomial (Fin n) A) := ⇑(MvPolynomial.map (algebraMap R A)) '' ↑s ∪ Set.range g
p : MvPolynomial (Fin n) R
q : MvPolynomial (Fin n) A
hq : q ∈ (Ideal.span s₀).toAddSubmonoid
hx : f p = 0
this :
  (MvPolynomial.map (algebraMap R A)) p + q ∈
    (MvPolynomial.map (algebraMap R A)).range.toAddSubmonoid ⊔ (Ideal.span s₀).toAddSubmonoid
⊢ (MvPolynomial.map (algebraMap R A)) p + q ∈ Ideal.span s₀
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithTerminal C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (incl.map f ≫ starTerminal.from (of y)) = F.map (starTerminal.from (of x))

Tactic:
congr 1

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
j : J
⊢ limit.π ((Functor.const J).obj c.pt) j ≫ c.π.app j =
    ((limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt)).hom ≫ c.π.app j

Tactic:
congr 1

Goal state after:
case e_a
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
X : C
inst✝² : IsConnected J
F : J ⥤ C
inst✝¹ : HasLimit F
c : Cone F
inst✝ : IsIso (limMap c.π)
j : J
⊢ limit.π ((Functor.const J).obj c.pt) j =
    ((limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt)).hom
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
hc : IsLimit c
j : J
⊢ limit.π ((Functor.const J).obj c.pt) j ≫ c.π.app j =
    ((limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt)).hom ≫ c.π.app j

Tactic:
congr 1

Goal state after:
case e_a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasLimit F
c : Cone F
hc : IsLimit c
j : J
⊢ limit.π ((Functor.const J).obj c.pt) j =
    ((limit.isLimit ((Functor.const J).obj c.pt)).conePointUniqueUpToIso (isLimitConstCone J c.pt)).hom
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
hc : IsColimit c
j : J
⊢ c.ι.app j ≫ colimit.ι ((Functor.const J).obj c.pt) j =
    c.ι.app j ≫
      ((isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit ((Functor.const J).obj c.pt))).hom

Tactic:
congr 1

Goal state after:
case e_a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
C : Type u₂
inst✝² : Category.{v₂, u₂} C
inst✝¹ : IsConnected J
F : J ⥤ C
inst✝ : HasColimit F
c : Cocone F
hc : IsColimit c
j : J
⊢ colimit.ι ((Functor.const J).obj c.pt) j =
    ((isColimitConstCocone J c.pt).coconePointUniqueUpToIso (colimit.isColimit ((Functor.const J).obj c.pt))).hom
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
⊢ H.mapCocone (Cocone.whisker F (liftColimit ((isColimitExtendCoconeEquiv F c).symm hc))) ≅ c

Tactic:
let i := liftedColimitMapsToOriginal ((isColimitExtendCoconeEquiv F (G := G ⋙ H) _).symm hc)

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Final
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : CreatesColimit G H
c : Cocone ((F ⋙ G) ⋙ H)
hc : IsColimit c
i : H.mapCocone (liftColimit ((isColimitExtendCoconeEquiv F c).symm hc)) ≅ extendCocone.obj c :=
  liftedColimitMapsToOriginal ((isColimitExtendCoconeEquiv F c).symm hc)
⊢ H.mapCocone (Cocone.whisker F (liftColimit ((isColimitExtendCoconeEquiv F c).symm hc))) ≅ c
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of y)) = F.map (starInitial.to (of x) ≫ incl.map f)

Tactic:
congr 1

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
c c' : Comma (Functor.const C) (𝟭 (C ⥤ D))
φ : c ⟶ c'
x y : WithInitial C
f : x ⟶ y
a : C
x✝ : star ⟶ of a
⊢ ((ofCommaObject c).map x✝ ≫
      match of a with
      | of x => φ.right.app x
      | star => φ.left) =
    (match star with
      | of x => φ.right.app x
      | star => φ.left) ≫
      (ofCommaObject c').map x✝

Tactic:
by simpa [-CommaMorphism.w] using (congrArg (fun f ↦ f.app a) φ.w).symm

Goal state after:
Module: Mathlib.CategoryTheory.WithTerminal.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : WithInitial C ⥤ D
x y : C
f : x ⟶ y
⊢ F.map (starInitial.to (of x) ≫ incl.map f) = F.map (starInitial.to (of y))

Tactic:
congr 1

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y P Q R S : C
f : P ⟶ Q
g : P ⟶ R
h : Q ⟶ S
k : R ⟶ S
hr : RegularMono h
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
⊢ IsLimit (Fork.ofι g ⋯)

Tactic:
apply Fork.IsLimit.mk' _ _
    intro s
    have l₁ : (Fork.ι s ≫ k) ≫ hr.left = (Fork.ι s ≫ k) ≫ hr.right := by
      rw [Category.assoc, s.condition, Category.assoc]
    obtain ⟨l, hl⟩ := Fork.IsLimit.lift' hr.isLimit _ l₁
    obtain ⟨p, _, hp₂⟩ := PullbackCone.IsLimit.lift' t _ _ hl
    refine ⟨p, hp₂, ?_⟩
    intro m w
    have z : m ≫ g = p ≫ g := w.trans hp₂.symm
    apply t.hom_ext
    have := hr.mono
    apply (PullbackCone.mk f g comm).equalizer_ext
    · simp only [PullbackCone.mk_π_app, ← cancel_mono h]
      grind [Fork.ofι, PullbackCone.mk]
    · exact z

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: case refine_3
C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
comm : a ≫ f₁ = b ≫ f₁
big_k : IsKernelPair (f₁ ≫ f₂) a b
s : PullbackCone f₁ f₁
s' : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂) := PullbackCone.mk s.fst s.snd ⋯
m✝ : s.pt ⟶ (PullbackCone.mk a b comm).pt
m₁ : m✝ ≫ (PullbackCone.mk a b comm).fst = s.fst
m₂ : m✝ ≫ (PullbackCone.mk a b comm).snd = s.snd
⊢ m✝ ≫ (PullbackCone.mk a b ⋯).snd = (IsPullback.isLimit big_k).lift s' ≫ (PullbackCone.mk a b ⋯).snd

Tactic:
· apply m₂.trans (big_k.isLimit.fac s' WalkingCospan.right).symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ ((pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄) ≫ pullback.fst f₁ f₂ =
    pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯ ≫
      pullback.fst f₁ f₂

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).inv ≫ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ =
    pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ ((pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ≫ pullback.fst f₃ f₄ =
    pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫
      pullback.fst f₃ f₄

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) =
    pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
      (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ ((pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ≫ pullback.snd f₃ f₄ =
    pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯ ≫
      pullback.snd f₃ f₄

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst✝³ : HasPullback f₁ f₂
inst✝² : HasPullback f₃ f₄
inst✝¹ : HasPullback (pullback.snd f₁ f₂ ≫ f₃) f₄
inst✝ : HasPullback f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ (pullbackAssoc f₁ f₂ f₃ f₄).hom ≫ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) =
    pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
      (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.inl g₁ g₂ ≫
      pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
      ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.inr g₁ g₂ ≫
      pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄))
        (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄)) ⋯

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄ ≫ (pushoutAssoc g₁ g₂ g₃ g₄).hom =
    pushout.desc (pushout.inl g₁ (g₂ ≫ pushout.inl g₃ g₄)) (pushout.inl g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄))
      ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
⊢ ∀ (g h : Z ⟶ X), g ≫ f = h ≫ f → g = h

Tactic:
g₁

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : IsIso a
l : X ⟶ (IsPullback.cone h).pt
h₁ : l = inv a
h₂ : (IsPullback.cone h).snd = a
Z : C
g₁ : Z ⟶ X
⊢ ∀ (h : Z ⟶ X), g₁ ≫ f = h ≫ f → g₁ = h
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr g₃ g₄ ≫ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.inr g₃ g₄ ≫
      pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄)
        (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄) ⋯

Tactic:
congr 1

Goal state after:
case e_a
C : Type u
inst✝⁴ : Category.{v, u} C
X₁ X₂ X₃ Z₁ Z₂ : C
g₁ : Z₁ ⟶ X₁
g₂ : Z₁ ⟶ X₂
g₃ : Z₂ ⟶ X₂
g₄ : Z₂ ⟶ X₃
inst✝³ : HasPushout g₁ g₂
inst✝² : HasPushout g₃ g₄
inst✝¹ : HasPushout (g₃ ≫ pushout.inr g₁ g₂) g₄
inst✝ : HasPushout g₁ (g₂ ≫ pushout.inl g₃ g₄)
⊢ pushout.inr g₁ (g₂ ≫ pushout.inl g₃ g₄) ≫ (pushoutAssoc g₁ g₂ g₃ g₄).inv =
    pushout.desc (pushout.inr g₁ g₂ ≫ pushout.inl (g₃ ≫ pushout.inr g₁ g₂) g₄) (pushout.inr (g₃ ≫ pushout.inr g₁ g₂) g₄)
      ⋯
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
⊢ P
      ((CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
        (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            {
              toFun := fun x ↦
                (CommRingCat.Hom.hom
                    (CommRingCat.ofHom
                      {
                        toFun :=
                          (↑((IsLocalization.toLocalizationMap (Submonoid.powers r) (Localization.Away r)).lift₀
                                ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                        map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))
                  ((CommRingCat.Hom.hom e₁.toCommRingCatIso.hom) x),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))) =
    P (IsLocalization.Away.map R' S' f r)

Tactic:
congr 1

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
⊢ (CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
      (CommRingCat.Hom.hom
        (CommRingCat.ofHom
          {
            toFun := fun x ↦
              (CommRingCat.Hom.hom
                  (CommRingCat.ofHom
                    {
                      toFun :=
                        (↑((IsLocalization.toLocalizationMap (Submonoid.powers r) (Localization.Away r)).lift₀
                              ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                      map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))
                ((CommRingCat.Hom.hom e₁.toCommRingCatIso.hom) x),
            map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })) =
    IsLocalization.Away.map R' S' f r
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.limitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
⊢ ∀ (c₁ : Cone X₁) (c₂ : Cone X₂) (x : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ

Tactic:
c₁

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.limitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
c₁ : Cone X₁
⊢ ∀ (c₂ : Cone X₂) (x : IsLimit c₁) (h₂ : IsLimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
⊢ ∀ (c₁ : Cocone X₁) (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₁ : IsColimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ

Tactic:
c₁

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
h : W.colimitsOfShape J ≤ W
X₁ X₂ : J ⥤ C
c₁ : Cocone X₁
⊢ ∀ (c₂ : Cocone X₂) (h₁ : IsColimit c₁) (h₁ : IsColimit c₂) (f : X₁ ⟶ X₂),
    W.functorCategory J f → ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ
Module: Mathlib.CategoryTheory.MorphismProperty.Limits

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
X Y : C
f : X ⟶ Y
J : Type w'
hf : W.colimitsOfShape (Discrete J) f
inst✝ : Small.{w, w'} J
⊢ W.colimitsOfShape (Discrete (Shrink.{w, w'} J)) f

Tactic:
rwa [← W.colimitsOfShape_eq_of_equivalence (Discrete.equivalence (equivShrink.{w} J))]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesColimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteCoproducts C
n : ℕ
⊢ ∀ (f : Fin (n + 1) → C), PreservesColimit (Discrete.functor f) F

Tactic:
by
    have := preserves_fin_of_preserves_binary_and_initial n
    intro f
    apply
      preservesColimit_of_preserves_colimit_cocone
        (extendCofanIsColimit f (colimit.isColimit _) (colimit.isColimit _)) _
    apply (isColimitMapCoconeCofanMkEquiv _ _ _).symm _
    let :=
      extendCofanIsColimit (fun i => F.obj (f i))
        (isColimitOfHasCoproductOfPreservesColimit F _)
        (isColimitOfHasBinaryCoproductOfPreservesColimit F _ _)
    refine IsColimit.ofIsoColimit this ?_
    apply Cocone.ext _ _
    · apply Iso.refl _
    rintro ⟨j⟩
    refine Fin.inductionOn j ?_ ?_
    · apply Category.comp_id
    · rintro i _
      dsimp [extendCofan_ι_app, Iso.refl_hom, Cofan.mk_ι_app]
      rw [comp_id, ← F.map_comp]
      rfl

Goal state after: