mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ ((dfinsuppFamily f) x).support ⊆ Fintype.piFinset fun i ↦ (x i).support

Tactic:
intro p hp

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁹ : DecidableEq ι
inst✝⁸ : Fintype ι
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : (i : ι) → DecidableEq (κ i)
inst✝¹ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
inst✝ : (i : (i : ι) → κ i) → (x : N i) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
p : (i : ι) → κ i
hp : p ∈ ((dfinsuppFamily f) x).support
⊢ p ∈ Fintype.piFinset fun i ↦ (x i).support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a b : α
ab : a ≠ b
c d : α
cd : c ≠ d
ac : a = c
⊢ swap a b * swap c d ∈ closure {σ | σ.IsThreeCycle}

Tactic:
subst ac
    exact swap_mul_swap_same_mem_closure_three_cycles ab cd

Goal state after:
Module: Mathlib.LinearAlgebra.Multilinear.DFinsupp

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝³ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝² : (i : ι) → (k : κ i) → Module R (M i k)
inst✝¹ : (p : (i : ι) → κ i) → Module R (N p)
inst✝ : (i : ι) → DecidableEq (κ i)
p : (i : ι) → κ i
f : MultilinearMap R (fun i ↦ M i (p i)) (N p)
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ (dfinsuppFamily (Pi.single p f)) x = DFinsupp.single p (f fun i ↦ (x i) (p i))

Tactic:
ext p'
  obtain rfl | hp := eq_or_ne p p'
  · simp
  · simp [hp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : (hom (F.map f)) x = (hom (F.map g)) y
| (hom (F.map (f ≫ IsFiltered.coeqHom f g))) y

Tactic:
rw [IsFiltered.coeq_condition]

Goal state after:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
k : J
f g : i ⟶ k
h : (hom (F.map f)) x = (hom (F.map g)) y
| (hom (F.map (g ≫ IsFiltered.coeqHom f g))) y
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: case mpr
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
i : J
x y : F.obj i
⊢ (∃ j f, (hom (F.map f)) x = (hom (F.map f)) y) → ∃ k f g, (hom (F.map f)) x = (hom (F.map g)) y

Tactic:
· rintro ⟨j, f, h⟩
    exact ⟨j, f, f, h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Filtered

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : IsFilteredOrEmpty J
t : Cocone F
ht : IsColimit t
x₁ x₂ : t.pt
⊢ ∃ j x₁' x₂', (hom (t.ι.app j)) x₁' = x₁ ∧ (hom (t.ι.app j)) x₂' = x₂

Tactic:
by
  obtain ⟨j₁, x₁, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₁
  obtain ⟨j₂, x₂, rfl⟩ := Types.jointly_surjective_of_isColimit ht x₂
  exact ⟨max j₁ j₂, F.map (leftToMax _ _) x₁, F.map (rightToMax _ _) x₂,
    congr_hom (t.w (leftToMax j₁ j₂)) x₁, congr_hom (t.w (rightToMax j₁ j₂)) x₂⟩

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ ∀ (a : Perm m) (b : Perm n),
    (↑↑(sign a) * ∏ x, A (a x) x) * (↑↑(sign b) * ∏ x, D (b x) x) =
      ↑↑(sign (a.sumCongr b)) * ∏ x, fromBlocks A B 0 D ((a.sumCongr b) x) x

Tactic:
intro σ₁ σ₂

Goal state after:
case e'_3.refine_4
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
σ₁ : Perm m
σ₂ : Perm n
⊢ (↑↑(sign σ₁) * ∏ x, A (σ₁ x) x) * (↑↑(sign σ₂) * ∏ x, D (σ₂ x) x) =
    ↑↑(sign (σ₁.sumCongr σ₂)) * ∏ x, fromBlocks A B 0 D ((σ₁.sumCongr σ₂) x) x
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case e'_3
m : Type u_1
n : Type u_2
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
R : Type v
inst✝ : CommRing R
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
⊢ (∑ σ, ↑↑(sign σ) * ∏ i, A (σ i) i) * ∑ σ, ↑↑(sign σ) * ∏ i, D (σ i) i =
    ∑ x ∈ (↑(sumCongrHom m n).range).toFinset, ↑↑(sign x) * ∏ i, fromBlocks A B 0 D (x i) i

Tactic:
simp_rw [sum_mul_sum, ← sum_product', univ_product_univ]
      refine sum_nbij (fun σ ↦ σ.fst.sumCongr σ.snd) ?_ ?_ ?_ ?_
      · intro σ₁₂ _
        simp
      · intro σ₁ _ σ₂ _
        dsimp only
        intro h
        have h2 : ∀ x, Perm.sumCongr σ₁.fst σ₁.snd x = Perm.sumCongr σ₂.fst σ₂.snd x :=
          DFunLike.congr_fun h
        simp only [Sum.map_inr, Sum.map_inl, Perm.sumCongr_apply, Sum.forall, Sum.inl.injEq,
          Sum.inr.injEq] at h2
        ext x
        · exact h2.left x
        · exact h2.right x
      · intro σ hσ
        rw [mem_coe, Set.mem_toFinset] at hσ
        obtain ⟨σ₁₂, hσ₁₂⟩ := hσ
        use σ₁₂
        rw [← hσ₁₂]
        simp
      · simp only [forall_prop_of_true, Prod.forall, mem_univ]
        intro σ₁ σ₂
        rw [Fintype.prod_sum_type]
        simp_rw [Equiv.sumCongr_apply, Sum.map_inr, Sum.map_inl, fromBlocks_apply₁₁,
          fromBlocks_apply₂₂]
        rw [mul_mul_mul_comm]
        congr
        rw [sign_sumCongr, Units.val_mul, Int.cast_mul]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (X✝.map f.1).app X.2 ≫ (T.app Y.1).app X.2

pp: case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.1).map f.2

Tactic:
rw [← NatTrans.comp_app, NatTrans.naturality, NatTrans.comp_app]

Goal state after:
case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (T.app X.1).app X.2 ≫ (Y✝.map f.1).app X.2

case a
B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
X✝ Y✝ : C ⥤ D ⥤ E
T : X✝ ⟶ Y✝
X Y : C × D
f : X ⟶ Y
| (Y✝.obj Y.1).map f.2
Module: Mathlib.CategoryTheory.Functor.Currying

Goal state before:
pp: B : Type u₁
inst✝⁴ : Category.{v₁, u₁} B
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
D : Type u₃
inst✝² : Category.{v₃, u₃} D
E : Type u₄
inst✝¹ : Category.{v₄, u₄} E
H : Type u₅
inst✝ : Category.{v₅, u₅} H
F : C × D ⥤ E
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { app := fun Y ↦ F.map (f ≫ g ×ₘ 𝟙 Y), naturality := ⋯ } =
    { app := fun Y ↦ F.map (f ×ₘ 𝟙 Y), naturality := ⋯ } ≫ { app := fun Y ↦ F.map (g ×ₘ 𝟙 Y), naturality := ⋯ }

Tactic:
ext Y; simp [← F.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Yoneda

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
F : J ⥤ C
X : C
s : ↑(F ⋙ coyoneda.obj (op X)).sections
j j' : J
f : j ⟶ j'
⊢ ↑s j' = ↑s j ≫ F.map f

Tactic:
exact (s.property f).symm

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} coyoneda

Tactic:
apply preservesLimits_of_evaluation
  intro K
  change PreservesLimitsOfSize (yoneda.obj K)
  infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
J : Type w
inst✝² : Category.{r, w} J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : ToType (F.obj i)
y : ToType (F.obj j)
h : (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ k f g, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y

Tactic:
exact (Types.FilteredColimit.isColimit_eq_iff (F ⋙ forget C) hE).mp h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F G : J ⥤ K ⥤ C
η : F ⟶ G
⊢ colim.map η ≫ (colimitIsoFlipCompColim G).hom =
    (colimitIsoFlipCompColim F).hom ≫ (flipFunctor J K C ⋙ (whiskeringRight K (J ⥤ C) C).obj colim).map η

Tactic:
ext k
    apply colimit_obj_ext
    intro j
    simp [comp_evaluation, ← NatTrans.comp_app_assoc _ (colimMap η)]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.FullyFaithful

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
inst✝¹ : R.Faithful
inst✝ : R.Full
Y : C
⊢ IsIso (h.unit.app Y) ↔ R.essImage Y

Tactic:
constructor
  · intro
    exact ⟨L.obj Y, ⟨(asIso (h.unit.app Y)).symm⟩⟩
  · rintro ⟨_, ⟨i⟩⟩
    rw [NatTrans.isIso_app_iff_of_iso _ i.symm]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (X ◁ (ρ_ Y).hom) ▷ 𝟙_ C = ((α_ X Y (𝟙_ C)).inv ≫ (ρ_ (X ⊗ Y)).hom) ▷ 𝟙_ C

Tactic:
comp_whiskerRight,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (X ◁ (ρ_ Y).hom) ▷ 𝟙_ C = (α_ X Y (𝟙_ C)).inv ▷ 𝟙_ C ≫ (ρ_ (X ⊗ Y)).hom ▷ 𝟙_ C
Module: Mathlib.CategoryTheory.Monoidal.Discrete

Goal state before:
pp: M : Type u
inst✝ : Monoid M
X₁✝ Y₁✝ X₂✝ Y₂✝ : Discrete M
f : X₁✝ ⟶ Y₁✝
g : X₂✝ ⟶ Y₂✝
⊢ { as := X₁✝.as * X₂✝.as } = { as := Y₁✝.as * Y₂✝.as }

Tactic:
rw [eq_of_hom f, eq_of_hom g]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ≫ G.map (μ F x✝² x✝¹)) ▷ G.obj (F.obj x✝) ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

Tactic:
comp_whiskerRight,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ (μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫ G.map (μ F x✝² x✝¹) ▷ G.obj (F.obj x✝)) ≫
      (μ G (F.obj (x✝² ⊗ x✝¹)) (F.obj x✝) ≫ G.map (μ F (x✝² ⊗ x✝¹) x✝)) ≫ G.map (F.map (α_ x✝² x✝¹ x✝).hom) =
    (α_ (G.obj (F.obj x✝²)) (G.obj (F.obj x✝¹)) (G.obj (F.obj x✝))).hom ≫
      G.obj (F.obj x✝²) ◁ (μ G (F.obj x✝¹) (F.obj x✝) ≫ G.map (μ F x✝¹ x✝)) ≫
        μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ (G.map (δ F (X ⊗ Y) Z) ≫ δ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
      (G.map (δ F X Y) ≫ δ G (F.obj X) (F.obj Y)) ▷ G.obj (F.obj Z) ≫
        (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom =
    G.map (F.map (α_ X Y Z).hom) ≫
      (G.map (δ F X (Y ⊗ Z)) ≫ δ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))

Tactic:
comp_whiskerRight,

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ (G.map (δ F (X ⊗ Y) Z) ≫ δ G (F.obj (X ⊗ Y)) (F.obj Z)) ≫
      (G.map (δ F X Y) ▷ G.obj (F.obj Z) ≫ δ G (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z)) ≫
        (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom =
    G.map (F.map (α_ X Y Z).hom) ≫
      (G.map (δ F X (Y ⊗ Z)) ≫ δ G (F.obj X) (F.obj (Y ⊗ Z))) ≫
        G.obj (F.obj X) ◁ (G.map (δ F Y Z) ≫ δ G (F.obj Y) (F.obj Z))
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        G.map (F.obj X ◁ δ F Y Z) ≫ δ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z) =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        δ G (F.obj X) (F.obj (Y ⊗ Z)) ≫ G.obj (F.obj X) ◁ G.map (δ F Y Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z)

Tactic:
δ_natural_right_assoc

Goal state after:
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
inst✝⁷ : MonoidalCategory C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : MonoidalCategory D
E : Type u₃
inst✝⁴ : Category.{v₃, u₃} E
inst✝³ : MonoidalCategory E
C' : Type u₁'
inst✝² : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ E
inst✝¹ : F.OplaxMonoidal
inst✝ : G.OplaxMonoidal
X Y Z : C
⊢ G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        G.map (F.obj X ◁ δ F Y Z) ≫ δ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z) =
    G.map (F.map (α_ X Y Z).hom) ≫
      G.map (δ F X (Y ⊗ Z)) ≫
        G.map (F.obj X ◁ δ F Y Z) ≫ δ G (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ δ G (F.obj Y) (F.obj Z)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ IsLimit (G.mapCone (PullbackCone.mk (c.π.app WalkingCospan.right) (c.π.app WalkingCospan.left) ?m.108))

pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ c.π.app WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
    c.π.app WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl

Tactic:
· refine @isLimitOfPreserves _ _ _ _ _ _ _ _ _ ?_ ?_
      · apply PullbackCone.isLimitOfFlip
        apply IsLimit.ofIsoLimit _ (PullbackCone.isoMk _)
        exact (IsLimit.postcomposeHomEquiv (diagramIsoCospan.{v₁} _) _).invFun hc
      · dsimp
        infer_instance

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : PreservesLimit (cospan f g) G
c : Cone (cospan g f)
hc : IsLimit c
⊢ c.π.app WalkingCospan.right ≫ (cospan g f).map WalkingCospan.Hom.inr =
    c.π.app WalkingCospan.left ≫ (cospan g f).map WalkingCospan.Hom.inl
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).inv ≫ G.map (pullback.fst f g) = pullback.fst (G.map f) (G.map g)

Tactic:
by
  simp [PreservesPullback.iso, Iso.inv_comp_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).inv ≫ G.map (pullback.snd f g) = pullback.snd (G.map f) (G.map g)

Tactic:
by
  simp [PreservesPullback.iso, Iso.inv_comp_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Functor

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map
        ((adj.unit.app (𝟙_ C) ≫ G.map (η F)) ▷ G.obj X ≫
          (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
            G.map (λ_ X).hom) ≫
      adj.counit.app X

Tactic:
comp_whiskerRight,

Goal state after:
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : MonoidalCategory C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : MonoidalCategory D
E : Type u₃
inst✝³ : Category.{v₃, u₃} E
inst✝² : MonoidalCategory E
C' : Type u₁'
inst✝¹ : Category.{v₁', u₁'} C'
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X : D
⊢ F.map (λ_ (G.obj X)).hom ≫ adj.counit.app X =
    F.map
        ((adj.unit.app (𝟙_ C) ▷ G.obj X ≫ G.map (η F) ▷ G.obj X) ≫
          (adj.unit.app (G.obj (𝟙_ D) ⊗ G.obj X) ≫
              G.map (δ F (G.obj (𝟙_ D)) (G.obj X) ≫ (adj.counit.app (𝟙_ D) ⊗ₘ adj.counit.app X))) ≫
            G.map (λ_ X).hom) ≫
      adj.counit.app X
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsMultiplicative
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : W.multiplicativeClosure f✝
hg : W g✝
hf : W f✝
⊢ W (f✝ ≫ g✝)

Tactic:
| comp_of _ _ _ hg hf =>

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Composition

Goal state before:
pp: case comp_of
C : Type u
inst✝¹ : Category.{v, u} C
W W' : MorphismProperty C
inst✝ : W'.IsMultiplicative
h : W ≤ W'
X✝ Y✝ : C
f✝¹ : X✝ ⟶ Y✝
x✝ y✝ z✝ : C
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : W.multiplicativeClosure f✝
hg : W g✝
hf : W' f✝
⊢ W' (f✝ ≫ g✝)

Tactic:
| comp_of _ _ _ hg hf =>

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks

Goal state before:
pp: case g
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u₂
inst✝ : Category.{v₂, u₂} J
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
⊢ IsLimit c.op → IsColimit c

Tactic:
intro h
    exact (IsColimit.equivIsoColimit c.opUnopIso).toFun
      (((IsLimit.postcomposeHomEquiv _ _).invFun
        ((IsLimit.whiskerEquivalenceEquiv _).toFun h)).unop)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ ((β_ X (𝟙_ C)).hom ≫ (λ_ X).hom) ▷ 𝟙_ C = (ρ_ X).hom ▷ 𝟙_ C

Tactic:
comp_whiskerRight,

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom ▷ 𝟙_ C ≫ (λ_ X).hom ▷ 𝟙_ C = (ρ_ X).hom ▷ 𝟙_ C
Module: Mathlib.Algebra.TrivSqZeroExt.Basic

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : DivisionRing R
inst✝² : AddCommGroup M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : Module R M
x : tsze R M
⊢ (-x)⁻¹ = -x⁻¹

Tactic:
by
  ext <;> simp [inv_neg]

Goal state after:
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
x : Π₀ (i : n), A i
⊢ (counit ∘ₗ DFinsupp.coeFnLinearMap R) x = counit x

Tactic:
have (i : n) (x : A i) : Decidable (x ≠ 0) := Classical.propDecidable _

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
x : Π₀ (i : n), A i
this : (i : n) → (x : A i) → Decidable (x ≠ 0)
⊢ (counit ∘ₗ DFinsupp.coeFnLinearMap R) x = counit x
Module: Mathlib.RingTheory.Coalgebra.Basic

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
x : Π₀ (i : n), A i
⊢ (comul ∘ₗ coeFnLinearMap R) x = (map (coeFnLinearMap R) (coeFnLinearMap R) ∘ₗ comul) x

Tactic:
have (i : n) (x : A i) : Decidable (x ≠ 0) := Classical.propDecidable _

Goal state after:
R : Type u_1
n : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
A : n → Type u_3
inst✝² : (i : n) → AddCommMonoid (A i)
inst✝¹ : (i : n) → Module R (A i)
inst✝ : (i : n) → CoalgebraStruct R (A i)
x : Π₀ (i : n), A i
this : (i : n) → (x : A i) → Decidable (x ≠ 0)
⊢ (comul ∘ₗ coeFnLinearMap R) x = (map (coeFnLinearMap R) (coeFnLinearMap R) ∘ₗ comul) x