mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
h : RegularMono f
this : Mono f
A B : C
z : A ⟶ B
hz : Epi z
u : A ⟶ X
v : B ⟶ Y
sq : CommSq u z f v
⊢ (u ≫ f) ≫ h.left = (u ≫ f) ≫ h.right
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: 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
f : A →ₐ[R] B
hf : Surjective ⇑f
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation R B
n : ℕ
g : MvPolynomial (Fin n) R →ₐ[R] A
hg : Surjective ⇑g
right✝ : (RingHom.ker g.toRingHom).FG
⊢ Ideal.comap ↑f ⊥ = Ideal.comap ↑f ⊥

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : Algebra A B
⊢ Algebra.FinitePresentation A B ↔ Algebra.FinitePresentation A B

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y X' Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
e : Arrow.mk f ≅ Arrow.mk g
h : RegularEpi f
⊢ h.right ≫ f ≫ Arrow.Hom.right e.hom = h.right ≫ f ≫ Arrow.Hom.right e.hom

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
hker : (ker f).FG
⊢ (f.comp (RingHom.id A)).FinitePresentation

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
hker : (ker f).FG
⊢ (f.comp (RingHom.id A)).FinitePresentation
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
⊢ Function.Injective ⇑f

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
⊢ Function.Injective ⇑f
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
this : ker f = ⊥
⊢ ⊥.FG

Tactic:
]

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Function.Bijective ⇑f
this : ker f = ⊥
⊢ ⊥.FG
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
inst✝¹ : F.Final
inst✝ : IsFilteredOrEmpty C
X Y : D
f g : X ⟶ Y
P : StructuredArrow X F → Prop := fun h ↦ ∃ Z q₁ q₂, h.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
h₀ : P (StructuredArrow.mk (f ≫ Final.homToLift F Y))
U V : StructuredArrow X F
h : U ⟶ V
Z : C
q₁ : U.right ⟶ Z
q₂ : Final.lift F Y ⟶ Z
hq : U.hom ≫ F.map q₁ = f ≫ Final.homToLift F Y ≫ F.map q₂
W : C
q₃ : Z ⟶ W
q₄ : V.right ⟶ W
hq' : q₁ ≫ q₃ = StructuredArrow.Hom.right h ≫ q₄
⊢ V.hom ≫ F.map q₄ = V.hom ≫ F.map q₄

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst✝¹ : HasPullback f f
inst✝ : Epi f
h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, pullback.fst f f ≫ g = pullback.snd f f ≫ g → ∃ u, f ≫ u = g
s : Cofork (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
m✝ : (Cofork.ofπ f ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ f ⋯).π ≫ m✝ = s.π
⊢ f ≫ m✝ = s.π

Tactic:
]

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst✝¹ : HasPullback f f
inst✝ : Epi f
h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, pullback.fst f f ≫ g = pullback.snd f f ≫ g → ∃ u, f ≫ u = g
s : Cofork (pullback.fst f f) (pullback.snd f f)
g : B ⟶ s.pt
hg : f ≫ g = s.π
m✝ : (Cofork.ofπ f ⋯).pt ⟶ s.pt
hm : (Cofork.ofπ f ⋯).π ≫ m✝ = s.π
⊢ f ≫ m✝ = s.π
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
big_k : IsKernelPair (f₁ ≫ f₂) a b
⊢ b ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂

Tactic:
]

Goal state after:
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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Final
S : D ⥤ E
X : E
f : StructuredArrow X S
⊢ IsConnected (StructuredArrow f.right T)

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Final
S : D ⥤ E
X : E
f : StructuredArrow X S
⊢ IsConnected (StructuredArrow f.right T)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case zero
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ (Ideal.comap MvPolynomial.C (ker g')).FG

Tactic:
]

Goal state after:
case zero
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ (Ideal.comap MvPolynomial.C (ker g')).FG
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
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Initial
S : D ⥤ E
X : E
f : CostructuredArrow S X
⊢ IsConnected (CostructuredArrow T f.left)

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
T : C ⥤ D
inst✝ : T.Initial
S : D ⥤ E
X : E
f : CostructuredArrow S X
⊢ IsConnected (CostructuredArrow T f.left)
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
⊢ b ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z✝ : C
g₁ g₂ : Z✝ ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ Cofork.π s = PullbackCone.IsLimit.lift hc g₁ g₂ hg ≫ s.ι.app WalkingParallelPair.zero

Tactic:
]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y B X : C
f : X ⟶ B
inst✝ : EffectiveEpi f
c : PullbackCone f f
hc : IsLimit c
s : Cocone (parallelPair c.fst c.snd)
Z✝ : C
g₁ g₂ : Z✝ ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ ≫ Cofork.π s = PullbackCone.IsLimit.lift hc g₁ g₂ hg ≫ s.ι.app WalkingParallelPair.zero
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
R X Y Z : C
a b : R ⟶ X
f₁ : X ⟶ Y
f₂ : Y ⟶ Z
inst✝ : Mono f₂
small_k : IsKernelPair f₁ a b
s : PullbackCone (f₁ ≫ f₂) (f₁ ≫ f₂)
⊢ s.snd ≫ f₁ ≫ f₂ = s.snd ≫ f₁ ≫ f₂

Tactic:
]

Goal state after:
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 : D ⥤ Cat
G : C ⥤ D
d : D
f : ↑(F.obj d)
X✝ Y✝ : StructuredArrow d G
g : X✝ ⟶ Y✝
⊢ (F.map (G.map (StructuredArrow.Hom.right g))).toFunctor.obj ((F.map X✝.hom).toFunctor.obj f) =
    (F.map (G.map (StructuredArrow.Hom.right g))).toFunctor.obj ((F.map X✝.hom).toFunctor.obj f)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
⊢ (Ideal.comap (↑e.symm) (ker g')).FG

Tactic:
]

Goal state after:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
⊢ (Ideal.comap (↑e.symm) (ker g')).FG
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ gr.left ≫ g ≫ k = gr.right ≫ g ≫ k

Tactic:
]

Goal state after:
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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
⊢ gr.left ≫ g ≫ k = gr.right ≫ g ≫ k
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R X Y Z : C
f : X ⟶ Y
a b : R ⟶ X
k : IsKernelPair f a b
r : RegularEpi f
t : (PullbackCone.mk r.left r.right ⋯).pt ⟶ (IsPullback.cone k).pt :=
  (IsPullback.isLimit k).lift (PullbackCone.mk r.left r.right ⋯)
ht : t ≫ a = r.left
kt : t ≫ b = r.right
s : Cofork a b
⊢ r.right ≫ s.π = r.right ≫ s.π

Tactic:
]

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
gr : RegularEpi g
comm : f ≫ h = g ≫ k
t : IsColimit (PushoutCocone.mk h k comm)
s : Cofork (gr.left ≫ f) (gr.right ≫ f)
⊢ (gr.right ≫ f) ≫ s.π = (gr.right ≫ f) ≫ s.π

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this✝ : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
he : (ker (g'.comp ↑e.symm)).FG
this : Q R[X] S ((g'.comp ↑e.symm).comp MvPolynomial.C)
⊢ g'.comp MvPolynomial.C = g'.comp ((↑e.symm).comp (MvPolynomial.C.comp C))

Tactic:
]

Goal state after:
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
n : ℕ
IH :
  ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (g' : MvPolynomial (Fin n) R →+* S),
    Surjective ⇑g' →
      (ker g').FG →
        let this := (g'.comp MvPolynomial.C).toAlgebra;
        Q R S (g'.comp MvPolynomial.C)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin (n + 1)) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this✝ : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
e : MvPolynomial (Fin (n + 1)) R ≃ₐ[R] MvPolynomial (Fin n) R[X] :=
  (MvPolynomial.renameEquiv R (finSuccEquiv n)).trans (MvPolynomial.optionEquivRight R (Fin n))
he : (ker (g'.comp ↑e.symm)).FG
this : Q R[X] S ((g'.comp ↑e.symm).comp MvPolynomial.C)
⊢ g'.comp MvPolynomial.C = g'.comp ((↑e.symm).comp (MvPolynomial.C.comp C))
Module: Mathlib.CategoryTheory.Limits.Shapes.KernelPair

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z A : C
g : Y ⟶ Z
a₁ a₂ : A ⟶ Y
h : IsKernelPair g a₁ a₂
f : X ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPullback f (a₁ ≫ g)
⊢ pullback.fst f (a₁ ≫ g) ≫ 𝟙 X = pullback.fst f (a₁ ≫ g) ≫ 𝟙 X

Tactic:
]

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₄
⊢ pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂ =
    pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂

Tactic:
]

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 f₁ (pullback.fst f₃ f₄ ≫ f₂)
⊢ pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ ≫ f₄ =
    pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.snd f₃ f₄ ≫ f₄

Tactic:
]

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:
]

Goal state after:
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₂
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
⊢ ∀ (G_1 : Grothendieck G ⥤ Type u₁), IsIso (colimit.pre G_1 (map α))

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : SmallCategory C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
⊢ ∀ (G_1 : Grothendieck G ⥤ Type u₁), IsIso (colimit.pre G_1 (map α))
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₂)
⊢ pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂) = pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂)

Tactic:
]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this✝ : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
this : (map α).Final
⊢ (map α).Final

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this✝ : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
this : (map α).Final
⊢ (map α).Final
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F G : C ⥤ Cat
α : F ⟶ G
hα : ∀ (X : C), (α.app X).toFunctor.Final
sC : C ≌ AsSmall C := AsSmall.equiv
F' : AsSmall C ⥤ Cat := sC.inverse ⋙ F ⋙ Cat.asSmallFunctor
G' : AsSmall C ⥤ Cat := sC.inverse ⋙ G ⋙ Cat.asSmallFunctor
α' : F' ⟶ G' := sC.inverse.whiskerLeft (whiskerRight α Cat.asSmallFunctor)
this✝ : ∀ (X : AsSmall C), (α'.app X).toFunctor.Final
hα' : (map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor))).Final
i :
  map (sC.symm.functor.whiskerLeft (whiskerRight α Cat.asSmallFunctor)) ≅
    (preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse
this :
  ((preEquivalence (F ⋙ Cat.asSmallFunctor) sC.symm).functor ⋙
      ((compAsSmallFunctorEquivalence F).functor ⋙ map α ⋙ (compAsSmallFunctorEquivalence G).inverse) ⋙
        (preEquivalence (G ⋙ Cat.asSmallFunctor) sC.symm).inverse).Final
⊢ (map α).Final

Tactic:
rwa [← final_iff_equivalence_comp, ← final_iff_comp_equivalence,
    ← final_iff_equivalence_comp, ← final_iff_comp_equivalence] at this

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₄).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:
]

Goal state after:
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₄