mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Module.LocalizedModule.Exact

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
x : M₀
hx : g x = a • m
⊢ mk (a • m) (⟨a, aS⟩ * s) = mk (⟨a, aS⟩ • m) (⟨a, aS⟩ * s)

Tactic:
mk_smul

Goal state after:
case h
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M₀ : Type u_2
inst✝⁵ : AddCommMonoid M₀
inst✝⁴ : Module R M₀
M₁ : Type u_3
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
M₂ : Type u_4
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
g : M₀ →ₗ[R] M₁
h : M₁ →ₗ[R] M₂
ex : Exact ⇑g ⇑h
y : LocalizedModule S M₁
m : M₁
s : ↥S
hy : ∃ u, u • h m = u • 0
a : R
aS : a ∈ S
x : M₀
hx : g x = a • m
⊢ mk (a • m) (⟨a, aS⟩ * s) = mk (a • m) (⟨a, aS⟩ * s)
Module: Mathlib.Algebra.Homology.LeftResolution.Basic

Goal state before:
pp: A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ n + 1 + 1 = n + 2

Tactic:
;

Goal state after:
A : Type u_1
C : Type u_2
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} A
ι : C ⥤ A
Λ : LeftResolution ι
X : A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : HasZeroMorphisms C
inst✝ : Abelian A
n : ℕ
⊢ n + 1 + 1 = n + 2
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
r : R
i : ℕ
hi : i < 0
⊢ M

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
r : R
i : ℕ
hi : i < 0
⊢ M
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
x✝ y✝ : R
⊢ ((x✝ + y✝) • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) =
    (x✝ • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) +
      y✝ • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
x✝ y✝ : R
⊢ ((x✝ + y✝) • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) =
    (x✝ • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) +
      y✝ • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
m✝ x✝ : R
⊢ ((m✝ • x✝) • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) =
    (RingHom.id R) m✝ • x✝ • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
m✝ x✝ : R
⊢ ((m✝ • x✝) • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim) =
    (RingHom.id R) m✝ • x✝ • (ιMulti R 0) fun a ↦ Fin.casesOn a fun i hi ↦ ⋯.elim
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = ((ιMulti R 1) fun x ↦ m₁) + (ιMulti R 1) fun x ↦ m₂
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = (ιMulti R 1) (update (fun x ↦ 0) 0 m₁) + (ιMulti R 1) fun x ↦ m₂

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
m₁ m₂ : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (m₁ + m₂)) = (ιMulti R 1) (update (fun x ↦ 0) 0 m₁) + (ιMulti R 1) fun x ↦ m₂
Module: Mathlib.LinearAlgebra.ExteriorPower.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (r • m)) = r • (ιMulti R 1) fun x ↦ m

Tactic:
;

Goal state after:
R : Type u
inst✝⁶ : CommRing R
n : ℕ
M : Type u_1
N : Type u_2
N' : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup N'
inst✝ : Module R N'
h : ∀ (m : M), (fun x ↦ m) = update (fun x ↦ 0) 0 m
r : R
m : M
⊢ (ιMulti R 1) (update (fun x ↦ 0) 0 (r • m)) = r • (ιMulti R 1) fun x ↦ m
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y) = (α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f)

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G F' G' : C ⥤ D
α : F ⟶ G
β : F' ⟶ G'
X Y : C
f : X ⟶ Y
⊢ (F.map f ⊗ₘ F'.map f) ≫ (α.app Y ⊗ₘ β.app Y) = (α.app X ⊗ₘ β.app X) ≫ (G.map f ⊗ₘ G'.map f)
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X₁✝ Y₁✝ X₂✝ Y₂✝ : C ⥤ D
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X₁✝ Y₁✝ X₂✝ Y₂✝ : C ⥤ D
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ f✝ ⊗ₘ g✝ = f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X₁✝ Y₁✝ X₂✝ Y₂✝ : C ⥤ D
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
x✝ : C
⊢ (f✝ ⊗ₘ g✝).app x✝ = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).app x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
X₁✝ Y₁✝ X₂✝ Y₂✝ : C ⥤ D
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
x✝ : C
⊢ (f✝ ⊗ₘ g✝).app x✝ = (f✝ ▷ X₂✝ ≫ Y₁✝ ◁ g✝).app x✝
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ ((α_ F G H).hom ▷ K ≫ (α_ F (G ⊗ H) K).hom ≫ F ◁ (α_ G H K).hom).app X =
    ((α_ (F ⊗ G) H K).hom ≫ (α_ F G (H ⊗ K)).hom).app X

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ ((α_ F G H).hom ▷ K ≫ (α_ F (G ⊗ H) K).hom ≫ F ◁ (α_ G H K).hom).app X =
    ((α_ (F ⊗ G) H K).hom ≫ (α_ F G (H ⊗ K)).hom).app X
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ (α_ (F.obj X) (G.obj X) (H.obj X)).hom ▷ K.obj X ≫
      (α_ (F.obj X) (G.obj X ⊗ H.obj X) (K.obj X)).hom ≫ F.obj X ◁ (α_ (G.obj X) (H.obj X) (K.obj X)).hom =
    (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom

Tactic:
;

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F G H K : C ⥤ D
X : C
⊢ (α_ (F.obj X) (G.obj X) (H.obj X)).hom ▷ K.obj X ≫
      (α_ (F.obj X) (G.obj X ⊗ H.obj X) (K.obj X)).hom ≫ F.obj X ◁ (α_ (G.obj X) (H.obj X) (K.obj X)).hom =
    (α_ (F.obj X ⊗ G.obj X) (H.obj X) (K.obj X)).hom ≫ (α_ (F.obj X) (G.obj X) (H.obj X ⊗ K.obj X)).hom
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ ((α_ F G H).hom ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) ((G ⊗ H).obj x)) ⋯).hom ≫ (α_ G H F).hom).app X =
    ((NatIso.ofComponents (fun x ↦ β_ (F.obj x) (G.obj x)) ⋯).hom ▷ H ≫
          (α_ G F H).hom ≫ G ◁ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom).app
      X

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ ((α_ F G H).hom ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) ((G ⊗ H).obj x)) ⋯).hom ≫ (α_ G H F).hom).app X =
    ((NatIso.ofComponents (fun x ↦ β_ (F.obj x) (G.obj x)) ⋯).hom ▷ H ≫
          (α_ G F H).hom ≫ G ◁ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom).app
      X
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ ((α_ F G H).inv ≫ (NatIso.ofComponents (fun x ↦ β_ ((F ⊗ G).obj x) (H.obj x)) ⋯).hom ≫ (α_ H F G).inv).app X =
    (F ◁ (NatIso.ofComponents (fun x ↦ β_ (G.obj x) (H.obj x)) ⋯).hom ≫
          (α_ F H G).inv ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom ▷ G).app
      X

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : BraidedCategory D
F G H : C ⥤ D
X : C
⊢ ((α_ F G H).inv ≫ (NatIso.ofComponents (fun x ↦ β_ ((F ⊗ G).obj x) (H.obj x)) ⋯).hom ≫ (α_ H F G).inv).app X =
    (F ◁ (NatIso.ofComponents (fun x ↦ β_ (G.obj x) (H.obj x)) ⋯).hom ≫
          (α_ F H G).inv ≫ (NatIso.ofComponents (fun x ↦ β_ (F.obj x) (H.obj x)) ⋯).hom ▷ G).app
      X
Module: Mathlib.CategoryTheory.Monoidal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : SymmetricCategory D
F G : C ⥤ D
X : C
⊢ ((β_ F G).hom ≫ (β_ G F).hom).app X = (𝟙 (F ⊗ G)).app X

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
inst✝ : SymmetricCategory D
F G : C ⥤ D
X : C
⊢ ((β_ F G).hom ≫ (β_ G F).hom).app X = (𝟙 (F ⊗ G)).app X
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y) =
    CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))

Tactic:
;

Goal state after:
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁶ : Category.{v_1, u_1} J
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} D
inst✝³ : Category.{v_4, u_4} E
inst✝² : CartesianMonoidalCategory C
inst✝¹ : CartesianMonoidalCategory E
F G : D ⥤ C
H : C ⥤ E
inst✝ : PreservesFiniteProducts H
X Y : D
f : X ⟶ Y
⊢ H.map (F.map f ⊗ₘ G.map f) ≫ CartesianMonoidalCategory.prodComparison H (F.obj Y) (G.obj Y) =
    CartesianMonoidalCategory.prodComparison H (F.obj X) (G.obj X) ≫ (H.map (F.map f) ⊗ₘ H.map (G.map f))
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} J₁
inst✝² : Category.{v₂, u₂} J₂
inst✝¹ : Category.{v₃, u₃} C
inst✝ : MonoidalCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₁ ⥤ C)
x✝¹ : X✝ ⟶ Y✝
x✝ : J₁
⊢ ((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).map x✝¹ ≫
          (NatIso.ofComponents
              (fun x ↦
                Iso.refl
                  (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj Y✝).obj x))
              ⋯).hom).app
      x✝ =
    ((NatIso.ofComponents
              (fun x ↦
                Iso.refl
                  (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj X✝).obj x))
              ⋯).hom ≫
          (tensor (J₁ ⥤ C)).map x✝¹).app
      x✝

Tactic:
;

Goal state after:
J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} J₁
inst✝² : Category.{v₂, u₂} J₂
inst✝¹ : Category.{v₃, u₃} C
inst✝ : MonoidalCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₁ ⥤ C)
x✝¹ : X✝ ⟶ Y✝
x✝ : J₁
⊢ ((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).map x✝¹ ≫
          (NatIso.ofComponents
              (fun x ↦
                Iso.refl
                  (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj Y✝).obj x))
              ⋯).hom).app
      x✝ =
    ((NatIso.ofComponents
              (fun x ↦
                Iso.refl
                  (((externalProductBifunctor J₁ J₁ C ⋙ (whiskeringLeft J₁ (J₁ × J₁) C).obj (diag J₁)).obj X✝).obj x))
              ⋯).hom ≫
          (tensor (J₁ ⥤ C)).map x✝¹).app
      x✝
Module: Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic

Goal state before:
pp: J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} J₁
inst✝³ : Category.{v₂, u₂} J₂
inst✝² : Category.{v₃, u₃} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₂ ⥤ C)
x✝¹ : X✝ ⟶ Y✝
x✝ : J₂ × J₁
⊢ ((externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)).map x✝¹ ≫
          (NatIso.ofComponents
              (fun x ↦ β_ (Y✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (Y✝.2.obj ((Prod.swap J₂ J₁).obj x).2)) ⋯).hom).app
      x✝ =
    ((NatIso.ofComponents (fun x ↦ β_ (X✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (X✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
              ⋯).hom ≫
          (Prod.swap (J₁ ⥤ C) (J₂ ⥤ C) ⋙ externalProductBifunctor J₂ J₁ C).map x✝¹).app
      x✝

Tactic:
;

Goal state after:
J₁ : Type u₁
J₂ : Type u₂
C : Type u₃
inst✝⁴ : Category.{v₁, u₁} J₁
inst✝³ : Category.{v₂, u₂} J₂
inst✝² : Category.{v₃, u₃} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X✝ Y✝ : (J₁ ⥤ C) × (J₂ ⥤ C)
x✝¹ : X✝ ⟶ Y✝
x✝ : J₂ × J₁
⊢ ((externalProductBifunctor J₁ J₂ C ⋙ (whiskeringLeft (J₂ × J₁) (J₁ × J₂) C).obj (Prod.swap J₂ J₁)).map x✝¹ ≫
          (NatIso.ofComponents
              (fun x ↦ β_ (Y✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (Y✝.2.obj ((Prod.swap J₂ J₁).obj x).2)) ⋯).hom).app
      x✝ =
    ((NatIso.ofComponents (fun x ↦ β_ (X✝.1.obj ((Prod.swap J₂ J₁).obj x).1) (X✝.2.obj ((Prod.swap J₂ J₁).obj x).2))
              ⋯).hom ≫
          (Prod.swap (J₁ ⥤ C) (J₂ ⥤ C) ⋙ externalProductBifunctor J₂ J₁ C).map x✝¹).app
      x✝
Module: Mathlib.CategoryTheory.Filtered.FinallySmall

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this✝ : IsFiltered P.FullSubcategory
G : FinalModel C₀ ⥤ P.FullSubcategory :=
  { obj := fun X ↦ { obj := (fromFinalModel C₀).obj X, property := ⋯ },
    map := fun {X Y} f ↦ ObjectProperty.homMk ((fromFinalModel C₀).map f), map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
Y : FinalModel C₀
⊢ ∃ a, G.obj a = { obj := (fromFinalModel C₀).obj Y, property := ⋯ }

Tactic:
;

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : IsFiltered C
inst✝⁴ : LocallySmall.{w, v, u} C
inst✝³ : FinallySmall C
C₀ : Type u
inst✝² : Category.{w, u} C₀
inst✝¹ : IsFiltered C₀
inst✝ : FinallySmall C₀
P : ObjectProperty C₀ := ⊤.strictMap (fromFinalModel C₀)
hP : ∀ (X : C₀), ∃ Y, ∃ (_ : P Y), Nonempty (X ⟶ Y)
this✝ : IsFiltered P.FullSubcategory
G : FinalModel C₀ ⥤ P.FullSubcategory :=
  { obj := fun X ↦ { obj := (fromFinalModel C₀).obj X, property := ⋯ },
    map := fun {X Y} f ↦ ObjectProperty.homMk ((fromFinalModel C₀).map f), map_id := ⋯, map_comp := ⋯ }
this : (G ⋙ P.ι).Final
Y : FinalModel C₀
⊢ ∃ a, G.obj a = { obj := (fromFinalModel C₀).obj Y, property := ⋯ }
Module: Mathlib.CategoryTheory.Filtered.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✝ : IsFilteredOrEmpty C
⊢ F.Final ↔ ∀ (d : D), IsFiltered (StructuredArrow d F)

Tactic:
by
  refine ⟨?_, fun h => final_of_isFiltered_structuredArrow F⟩
  rw [final_iff_of_isFiltered]
  exact fun h d => isFiltered_structuredArrow_of_isFiltered_of_exists F d (h.1 d) h.2

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

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ t, x✝¹ ≫ F.map t = x✝ ≫ F.map t

Tactic:
;

Goal state after:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsFiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : x✝² ⟶ F.obj c
⊢ ∃ t, x✝¹ ≫ F.map t = x✝ ≫ F.map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ t, F.map t ≫ x✝¹ = F.map t ≫ x✝

Tactic:
;

Goal state after:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : IsCofiltered C
F : C ⥤ Discrete PUnit.{u_1 + 1}
x✝² : Discrete PUnit.{u_1 + 1}
c : C
x✝¹ x✝ : F.obj c ⟶ x✝²
⊢ ∃ t, F.map t ≫ x✝¹ = F.map t ≫ x✝
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ (F.obj j).map f ≫ c.ι.app (j, k') = c.ι.app (j, k) ≫ 𝟙 c.pt

Tactic:
;

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
⊢ (F.obj j).map f ≫ c.ι.app (j, k') = c.ι.app (j, k) ≫ 𝟙 c.pt
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
| (F.obj j).map f

Tactic:
;

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
| (F.obj j).map f
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
| (F.map (𝟙 j)).app k ≫ (F.obj j).map f

Tactic:
;

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j : J
k k' : K
f : k ⟶ k'
| (F.map (𝟙 j)).app k ≫ (F.obj j).map f
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ (Pi.eval I s).obj c
⊢ ∃ c' t, f ≫ (Pi.eval I s).map t = g ≫ (Pi.eval I s).map t

Tactic:
let c't : (∀ s, (c' : I s) × (c s ⟶ c')) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨coeq f g, coeqHom f g⟩

Goal state after:
case h₂
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
F : C ⥤ D
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
d : I s
c : (i : α) → I i
f g : d ⟶ (Pi.eval I s).obj c
c't : (s : α) → (c' : I s) × (c s ⟶ c') := Function.update (fun t ↦ ⟨c t, 𝟙 (c t)⟩) s ⟨coeq f g, coeqHom f g⟩
⊢ ∃ c' t, f ≫ (Pi.eval I s).map t = g ≫ (Pi.eval I s).map t
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
⊢ (F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)

Tactic:
have := @NatTrans.naturality _ _ _ _ _ _ c.ι (j, k) (j', k) (f, 𝟙 k)

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
this : (uncurry.obj F).map (f, 𝟙 k) ≫ c.ι.app (j', k) = c.ι.app (j, k) ≫ ((const (J × K)).obj c.pt).map (f, 𝟙 k)
⊢ (F.map f).app k ≫ c.ι.app (j', k) = c.ι.app (j, k)