mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.Ring.Constructions

Goal state before:
pp: A B : CommRingCat
s : BinaryCofan A B
x✝¹ : ↑((pair A B).obj { as := WalkingPair.left })
x✝ : ↑((pair A B).obj { as := WalkingPair.right })
⊢ Commute ((Hom.hom s.inl).toIntAlgHom x✝¹) ((Hom.hom s.inr).toIntAlgHom x✝)

Tactic:
apply Commute.all

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ (G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.mapComp f✝ g)) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)

Tactic:
assoc,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f✝ f'✝ : a✝ ⟶ b✝
η : f✝ ⟶ f'✝
g : b✝ ⟶ c✝
⊢ G.mapComp (F.map f✝) (F.map g) ≫ G.map₂ (F.mapComp f✝ g) ≫ G.map₂ (F.map₂ (η ▷ g)) =
    G.map₂ (F.map₂ η) ▷ G.map (F.map g) ≫ G.mapComp (F.map f'✝) (F.map g) ≫ G.map₂ (F.mapComp f'✝ g)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ (G.mapComp (F.map f) (F.map x✝¹) ≫ G.map₂ (F.mapComp f x✝¹)) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)

Tactic:
assoc,

Goal state after:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ : B
f : a✝ ⟶ b✝
x✝¹ x✝ : b✝ ⟶ c✝
η : x✝¹ ⟶ x✝
⊢ G.mapComp (F.map f) (F.map x✝¹) ≫ G.map₂ (F.mapComp f x✝¹) ≫ G.map₂ (F.map₂ (f ◁ η)) =
    G.map (F.map f) ◁ G.map₂ (F.map₂ η) ≫ G.mapComp (F.map f) (F.map x✝) ≫ G.map₂ (F.mapComp f x✝)
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom ≫
    (G.map (F.map f) ◁ G.mapComp (F.map g) (F.map h) ≫ G.map (F.map f) ◁ G.map₂ (F.mapComp g h)) ≫
      G.mapComp (F.map f) (F.map (g ≫ h))

pp: case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.mapComp f (g ≫ h))

Tactic:
assoc,

Goal state after:
case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| (α_ (G.map (F.map f)) (G.map (F.map g)) (G.map (F.map h))).hom ≫
    G.map (F.map f) ◁ G.mapComp (F.map g) (F.map h) ≫
      G.map (F.map f) ◁ G.map₂ (F.mapComp g h) ≫ G.mapComp (F.map f) (F.map (g ≫ h))

case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.mapComp f (g ≫ h))
Module: Mathlib.CategoryTheory.Bicategory.Functor.Lax

Goal state before:
pp: case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| (G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫ G.map₂ (F.mapComp f g) ▷ G.map (F.map h)) ≫
    G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)

pp: case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.map₂ (α_ f g h).hom)

Tactic:
assoc,

Goal state after:
case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.mapComp (F.map f) (F.map g) ▷ G.map (F.map h) ≫
    G.map₂ (F.mapComp f g) ▷ G.map (F.map h) ≫ G.mapComp (F.map (f ≫ g)) (F.map h) ≫ G.map₂ (F.mapComp (f ≫ g) h)

case a
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F✝ : B ⥤ᴸ C
D : Type u₃
inst✝ : Bicategory D
F : B ⥤ᴸ C
G : C ⥤ᴸ D
a✝ b✝ c✝ d✝ : B
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
| G.map₂ (F.map₂ (α_ f g h).hom)
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inl
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))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ (MvPolynomial.map (algebraMap R A)) x ∈ ↑(RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)))

Tactic:
rw [SetLike.mem_coe, RingHom.mem_ker]

Goal state after:
case inl
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))
x : MvPolynomial (Fin n) R
hx : x ∈ ↑s
⊢ (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) ((MvPolynomial.map (algebraMap R A)) x) = 0
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case inr
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))
x : A
hx : x ∈ t
⊢ g ⟨x, hx⟩ ∈ ↑(RingHom.ker (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)))

Tactic:
rw [SetLike.mem_coe, RingHom.mem_ker]

Goal state after:
case inr
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))
x : A
hx : x ∈ t
⊢ (MvPolynomial.aeval (⇑f ∘ MvPolynomial.X)) (g ⟨x, hx⟩) = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
F : C ⥤ Cat
H : Type u₂
inst✝¹ : Category.{v₂, u₂} H
G : Grothendieck F ⥤ H
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), HasColimit ((F.map f).toFunctor ⋙ Grothendieck.ι F Y ⋙ G)
c : Cocone G
hc : IsColimit c
s : Cocone (fiberwiseColimit G)
m : (coconeFiberwiseColimitOfCocone c).pt ⟶ s.pt
hm : ∀ (j : C), (coconeFiberwiseColimitOfCocone c).ι.app j ≫ m = s.ι.app j
X : Grothendieck F
⊢ c.ι.app X ≫ m =
    c.ι.app X ≫
      hc.desc { pt := s.pt, ι := natTransIntoForgetCompFiberwiseColimit G ≫ (Grothendieck.forget F).whiskerLeft s.ι }

Tactic:
have := hm X.base
    simp only [Functor.const_obj_obj, IsColimit.fac, NatTrans.comp_app, Functor.comp_obj,
      Grothendieck.forget_obj, natTransIntoForgetCompFiberwiseColimit_app,
      whiskerLeft_app]
    simp only [coconeFiberwiseColimitOfCocone_pt, coconeFiberwiseColimitOfCocone_ι_app] at this
    simp [← this]

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

Goal state before:
pp: case h.some
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
val✝ : J
⊢ some val✝ ∈ p

Tactic:
← t (WidePushoutShape.Hom.init _)

Goal state after:
case h.some
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
val✝ : J
⊢ none ∈ p
Module: Mathlib.CategoryTheory.Limits.Connected

Goal state before:
pp: case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
        ((prod.functor.obj X).mapCone c).π.app j) ≫
      prod.fst =
    s.π.app j ≫ prod.fst

Tactic:
assoc,

Goal state after:
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ prod.lift (s.π.app (Classical.arbitrary J) ≫ prod.fst) (l.lift (forgetCone s)) ≫
      ((prod.functor.obj X).mapCone c).π.app j ≫ prod.fst =
    s.π.app j ≫ prod.fst
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
⊢ (a ≫ f₁) ≫ f₂ = (b ≫ f₁) ≫ f₂

Tactic:
assoc,

Goal state after:
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
⊢ a ≫ f₁ ≫ f₂ = (b ≫ f₁) ≫ f₂
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
⊢ a ≫ f₁ ≫ f₂ = (b ≫ f₁) ≫ f₂

Tactic:
assoc,

Goal state after:
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
⊢ a ≫ f₁ ≫ f₂ = b ≫ f₁ ≫ f₂
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.fst ≫ f₁) ≫ f₂ = (s.snd ≫ f₁) ≫ f₂

Tactic:
assoc,

Goal state after:
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.fst ≫ f₁ ≫ f₂ = (s.snd ≫ f₁) ≫ f₂
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
⊢ (t ≫ a) ≫ s.π = r.right ≫ s.π

Tactic:
assoc,

Goal state after:
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
⊢ t ≫ a ≫ s.π = r.right ≫ s.π
Module: Mathlib.CategoryTheory.Limits.Final

Goal state before:
pp: case pos.refine_1
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ j₁ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj { obj := d, property := hd }))

pp: case pos.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ j₂ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj { obj := d, property := hd }))

Tactic:
· exact CostructuredArrow.homMk (InducedCategory.homMk j₁.hom)

Goal state after:
case pos.refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
h : ∀ (d : C), ¬P d → IsConnected (CostructuredArrow P.ι d)
d : C
hd : P d
this : Nonempty (CostructuredArrow P.ι d)
j₁ j₂ : CostructuredArrow P.ι d
⊢ j₂ ⟶ CostructuredArrow.mk (𝟙 (P.ι.obj { obj := d, property := hd }))
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₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
⊢ ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ

Tactic:
φ

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₂
h₁ : IsLimit c₁
h₂ : IsLimit c₂
f : X₁ ⟶ X₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
⊢ (∀ (j : J), φ ≫ c₂.π.app j = c₁.π.app j ≫ f.app j) → W φ
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) ≫ f =
    (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ≫ g

Tactic:
← cancel_mono i₃,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ ((fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) ≫ f) ≫ i₃ =
    ((snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ≫ g) ≫ i₃
Module: Mathlib.CategoryTheory.ObjectProperty.ContainsZero

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
P Q : ObjectProperty C
inst✝² : P.ContainsZero
inst✝¹ : Q.ContainsZero
inst✝ : Q.IsClosedUnderIsomorphisms
Z : C
hZ : IsZero Z
hP : P Z
⊢ ∃ Z, IsZero Z ∧ (P ⊓ Q) Z

Tactic:
exact ⟨Z, hZ, hP, Q.prop_of_isZero hZ⟩

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

Goal state before:
pp: case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ (c₁.ι.app { as := i } ≫ c₂.inr) ≫
      ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
          (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
    s.ι.app { as := i.succ }

Tactic:
assoc,

Goal state after:
case refine_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
n : ℕ
f : Fin (n + 1) → C
c₁ : Cofan fun i ↦ f i.succ
c₂ : BinaryCofan (f 0) c₁.pt
t₁ : IsColimit c₁
t₂ : IsColimit c₂
s : Cocone (Discrete.functor f)
j : Fin (n + 1)
i : Fin n
⊢ c₁.ι.app { as := i } ≫
      c₂.inr ≫
        ↑(BinaryCofan.IsColimit.desc' t₂ (s.ι.app { as := 0 })
            (t₁.desc { pt := s.pt, ι := Discrete.natTrans fun i ↦ s.ι.app { as := i.as.succ } })) =
    s.ι.app { as := i.succ }
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 : ℕ
this : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
⊢ IsColimit
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
      F.map
        (Fin.cases
          (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
          (fun i ↦
            (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).ι.app { as := i } ≫
              BinaryCofan.inr (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
          j))

Tactic:
let :=
      extendCofanIsColimit (fun i => F.obj (f i))
        (isColimitOfHasCoproductOfPreservesColimit F _)
        (isColimitOfHasBinaryCoproductOfPreservesColimit F _ _)

Goal state after:
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 : ℕ
this✝ : ∀ (f : Fin n → C), PreservesColimit (Discrete.functor f) F
f : Fin (n + 1) → C
this : IsColimit
  (extendCofan (Cofan.mk (F.obj (∐ fun i ↦ f i.succ)) fun j ↦ F.map (Sigma.ι (fun i ↦ f i.succ) j))
    (BinaryCofan.mk (F.map coprod.inl) (F.map coprod.inr))) :=
  extendCofanIsColimit (fun i ↦ F.obj (f i)) (isColimitOfHasCoproductOfPreservesColimit F fun i ↦ f i.succ)
    (isColimitOfHasBinaryCoproductOfPreservesColimit F (f 0) (∐ fun i ↦ f i.succ))
⊢ IsColimit
    (Cofan.mk (F.obj (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)).pt) fun j ↦
      F.map
        (Fin.cases
          (BinaryCofan.inl (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
          (fun i ↦
            (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).ι.app { as := i } ≫
              BinaryCofan.inr (colimit.cocone (pair (f 0) (colimit.cocone (Discrete.functor fun i ↦ f i.succ)).pt)))
          j))
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₂
hf : W.functorCategory J f
⊢ ∀ (φ : c₁.pt ⟶ c₂.pt), (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ

Tactic:
φ

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₂
hf : W.functorCategory J f
φ : c₁.pt ⟶ c₂.pt
⊢ (∀ (j : J), c₁.ι.app j ≫ φ = f.app j ≫ c₂.ι.app j) → W φ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂) f₃ ≫ μ ▷ M ≫ μ

Tactic:
← tensorHom_id,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f₁ f₂ f₃ : X ⟶ M
⊢ lift (lift f₁ f₂ ≫ μ) f₃ ≫ μ = lift (lift f₁ f₂) f₃ ≫ (μ ⊗ₘ 𝟙 M) ≫ μ
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mon

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift f (toUnit X) ≫ (𝟙 M ⊗ₘ η) ≫ μ = f ≫ 𝟙 M

Tactic:
id_tensorHom,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : CartesianMonoidalCategory C
inst✝⁴ : Category.{w, u_2} D
inst✝³ : CartesianMonoidalCategory D
M N O X Y : C
inst✝² : MonObj M
inst✝¹ : MonObj N
inst✝ : MonObj O
f : X ⟶ M
⊢ lift f (toUnit X) ≫ M ◁ η ≫ μ = f ≫ 𝟙 M
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : (lift (𝟙 A) ι ≫ μ) ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η

Tactic:
assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift (𝟙 A) ι ≫ μ ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift (𝟙 A) ι ≫ (f ⊗ₘ f) ≫ μ = (toUnit A ≫ η) ≫ f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η

Tactic:
assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift (𝟙 A) ι ≫ (f ⊗ₘ f) ≫ μ = toUnit A ≫ η ≫ f
⊢ lift f (ι ≫ f) ≫ μ = toUnit A ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : (lift ι (𝟙 A) ≫ μ) ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η

Tactic:
assoc,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : CartesianMonoidalCategory C
A B : C
inst✝² : GrpObj A
inst✝¹ : GrpObj B
f : A ⟶ B
inst✝ : IsMonHom f
this : lift ι (𝟙 A) ≫ μ ≫ f = (toUnit A ≫ η) ≫ f
⊢ lift (ι ≫ f) f ≫ μ = toUnit A ≫ η