mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ π.cycleType = π.cycleType + σ.cycleType - σ'.cycleType

pp: case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ' ∈ τ.cycleFactorsFinset

Tactic:
hs,

Goal state after:
case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ π.cycleType = π.cycleType + σ'.cycleType - σ'.cycleType

case induction_disjoint.refine_1
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
hd : σ.Disjoint π
hc : σ.IsCycle
hσ : ∀ {τ : Perm α}, σ.cycleType = τ.cycleType → IsConj σ τ
hπ : ∀ {τ : Perm α}, π.cycleType = τ.cycleType → IsConj π τ
τ : Perm α
h : σ.cycleType + π.cycleType = τ.cycleType
h' : #σ.support ∈ τ.cycleType
σ' : Perm α
hσ'l : σ' ∈ τ.cycleFactorsFinset.val
hσ' : (Finset.card ∘ support) σ' = #σ.support
key : IsConj (σ' * τ * σ'⁻¹) τ
hs : σ.cycleType = σ'.cycleType
⊢ σ' ∈ τ.cycleFactorsFinset
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ

Tactic:
have : castSucc (j + 1) = j.succ := by
      ext
      rw [val_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]

Goal state after:
case succ.inl
n✝ : ℕ
i j : Fin (n✝ + 1)
hlt : j < i
this : (j + 1).castSucc = j.succ
⊢ i.succ.succAbove (i.cycleRange j) = (swap 0 i.succ) j.succ
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: case mp.refine_3
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hn : l.Nodup
l' : List (Perm α)
hp' : l'.prod = σ
hc' : ∀ g ∈ l', g.IsCycle
hd' : List.Pairwise Disjoint l'
hl : Trunc.mk ⟨l', ⋯⟩ = σ.truncCycleFactors
ht : σ.cycleFactorsFinset = l'.toFinset
h : l'.toFinset = l.toFinset
hn' : l'.Nodup
hperm : l ~ l'
⊢ List.Pairwise Commute l'

Tactic:
exact hd'.imp Disjoint.commute

Goal state after:
Module: Mathlib.GroupTheory.Perm.Fin

Goal state before:
pp: n : ℕ
i j k : Fin n
inst✝ : NeZero n
hij : i ≤ j
hjk : j ≤ k
⊢ ⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k) = ⇑(i.cycleIcc k)

Tactic:
ext x
  rcases lt_or_ge x i with ch | ch
  · simp [cycleIcc_of_lt (lt_of_lt_of_le ch hij), cycleIcc_of_lt ch]
  rcases lt_or_ge k x with ch | ch1
  · simp [cycleIcc_of_gt (lt_of_le_of_lt hjk ch), cycleIcc_of_gt ch]
  rcases lt_or_ge x j with ch2 | ch2
  · simp [cycleIcc_of_lt ch2, cycleIcc_of_le_of_le ch ch1, cycleIcc_of_le_of_le ch (le_of_lt ch2)]
    split_ifs
    repeat lia
  · simp only [Function.comp_apply, cycleIcc_of_le_of_le ch2 ch1, cycleIcc_of_le_of_le ch ch1]
    split_ifs with h
    · exact val_eq_of_eq (cycleIcc_of_last hij)
    · simp [cycleIcc_of_gt (lt_of_le_of_lt ch2 (lt_add_one_of_succ_lt (by lia)))]

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
hn : n ∈ σ.cycleType + Multiset.replicate (Fintype.card α - #σ.support) 1
⊢ 0 < n

Tactic:
by
    rcases mem_add.mp hn with hn | hn
    · exact zero_lt_one.trans (one_lt_of_mem_cycleType hn)
    · exact lt_of_lt_of_le zero_lt_one (ge_of_eq (Multiset.eq_of_mem_replicate hn))

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
this : f = g → (g.IsCycle ↔ f.IsCycle)
⊢ f.cycleFactorsFinset = {g} ↔ f.IsCycle ∧ f = g

Tactic:
rw [cycleFactorsFinset_eq_finset]
    simpa [eq_comm]

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
S : Type uS
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)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) (N p)
dec : DecidableEq ι
m : (i : ι) → Π₀ (j : κ i), M i j
i : ι
x y : Π₀ (j : κ i), M i j
p : (i : ι) → κ i
⊢ ((f p) fun i_1 ↦ Function.update (fun k ↦ (m k) (p k)) i (x (p i) + y (p i)) i_1) =
    ((f p) fun i_1 ↦ Function.update (fun k ↦ (m k) (p k)) i (x (p i)) i_1) +
      (f p) fun i_1 ↦ Function.update (fun k ↦ (m k) (p k)) i (y (p i)) i_1

Tactic:
(f p).map_update_add

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

Goal state before:
pp: ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
N : Type u_1
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) N
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ (((dfinsuppFamilyₗ f) x).sum fun x ↦ ⇑((fun x ↦ LinearMap.id) x).toAddMonoidHom) =
    ∑ p ∈ Fintype.piFinset fun i ↦ (x i).support, (f p) fun i ↦ (x i) (p i)

Tactic:
refine Finset.sum_subset (MultilinearMap.support_dfinsuppFamily_subset _ _) ?_

Goal state after:
ι : Type uι
κ : ι → Type uκ
R : Type uR
M : (i : ι) → κ i → Type uM
inst✝⁸ : DecidableEq ι
inst✝⁷ : Fintype ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
N : Type u_1
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : (i : ι) → (j : κ i) → (x : M i j) → Decidable (x ≠ 0)
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i ↦ M i (p i)) N
x : (i : ι) → Π₀ (j : κ i), M i j
⊢ ∀ x_1 ∈ Fintype.piFinset fun i ↦ (x i).support,
    x_1 ∉ ((dfinsuppFamilyₗ f) x).support →
      (fun x ↦ ⇑((fun x ↦ LinearMap.id) x).toAddMonoidHom) x_1 (((dfinsuppFamilyₗ f) x) x_1) = 0
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommMonoid (M₁ i)
inst✝³ : AddCommMonoid M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : DecidableEq ι
m : (i : ι) → M₁ i
t✝ : Finset ι
i : ι
t : Finset ι
hit : i ∉ t
Hrec : ∀ (m' : (i : ι) → M₁ i), f (t.piecewise (m + m') m') = ∑ s ∈ t.powerset, f (s.piecewise m m')
m' : (i : ι) → M₁ i
A : (insert i t).piecewise (m + m') m' = update (t.piecewise (m + m') m') i (m i + m' i)
B : update (t.piecewise (m + m') m') i (m' i) = t.piecewise (m + m') m'
m'' : (a : ι) → M₁ a := update m' i (m i)
j : ι
h : ¬j = i
⊢ update (t.piecewise (m + m') m') i (m i) j = t.piecewise (m + m'') m'' j

Tactic:
· by_cases h' : j ∈ t <;> simp [m'', h, h']

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)

Tactic:
apply Relation.map

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s ((x.add y).mul z) = descFunLift F s ((x.mul z).add (y.mul z))

Tactic:
| right_distrib x y z =>

Goal state after:
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
j j' : J
f : j ⟶ j'
x✝ : ↑(F.obj j)
⊢ (colimitSetoid F) (Prequotient.of j' ((F.map f).hom' x✝)) (Prequotient.of j x✝)

Tactic:
apply Relation.map

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

Goal state before:
pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)

Tactic:
have B_subset_A : ∀ i, B i ⊆ A i := by
    intro i
    by_cases hi : i = i₀
    · rw [hi]
      simp only [B, Finset.sdiff_subset, update_self]
    · simp only [B, hi, update_of_ne, Ne, not_false_iff, Finset.Subset.refl]

Goal state after:
case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁶ : Semiring R
inst✝⁵ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f : MultilinearMap R M₁ M₂
α : ι → Type u_1
g : (i : ι) → α i → M₁ i
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
this : (i : ι) → DecidableEq (α i) := fun i ↦ Classical.decEq (α i)
n : ℕ
IH :
  ∀ m < n,
    ∀ (A : (i : ι) → Finset (α i)),
      ∑ i, #(A i) = m → (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
A : (i : ι) → Finset (α i)
h : ∑ i, #(A i) = n
Ai_empty : ∀ (i : ι), (A i).Nonempty
i₀ : ι
hi₀ : 1 < #(A i₀)
j₁ j₂ : α i₀
left✝ : j₁ ∈ A i₀
hj₂ : j₂ ∈ A i₀
right✝ : j₁ ≠ j₂
B : (a : ι) → Finset (α a) := update A i₀ (A i₀ \ {j₂})
C : (a : ι) → Finset (α a) := update A i₀ {j₂}
B_subset_A : ∀ (i : ι), B i ⊆ A i
⊢ (f fun i ↦ ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i ↦ g i (r i)
Module: Mathlib.Algebra.Category.Ring.Colimits

Goal state before:
pp: case a.right_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s ((x.add y).mul z) = descFunLift F s ((x.mul z).add (y.mul z))

Tactic:
| right_distrib x y z =>

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

Goal state before:
pp: n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ A.det = 0

Tactic:
rw [← det_transpose]

Goal state after:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ Aᵀ.det = 0
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ ∀ (a b : (j : J) × F.obj j),
    F.ColimitTypeRel a b →
      (match a with
        | ⟨j, x⟩ => c.ι j x) =
        match b with
        | ⟨j, x⟩ => c.ι j x

Tactic:
rintro _ _ ⟨_, _⟩

Goal state after:
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
a✝ b✝ : (j : J) × F.obj j
w✝ : a✝.fst ⟶ b✝.fst
h✝ : b✝.snd = (ConcreteCategory.hom (F.map w✝)) a✝.snd
⊢ (match a✝ with
    | ⟨j, x⟩ => c.ι j x) =
    match b✝ with
    | ⟨j, x⟩ => c.ι j x
Module: Mathlib.CategoryTheory.Limits.Types.ColimitType

Goal state before:
pp: case mp
J : Type u
inst✝ : Category.{v, u} J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Surjective (F.descColimitType c) → ∀ (z : c.pt), ∃ i x, c.ι i x = z

Tactic:
intro h z
    obtain ⟨⟨i, x⟩, rfl⟩ := h z
    exact ⟨i, x, rfl⟩

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

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : HasColimit F
j j' : J
x : F.obj j
x' : F.obj j'
f : j ⟶ j'
w : (hom (F.map f)) x = x'
⊢ (hom (colimit.ι F j)) x = (hom (colimit.ι F j')) x'

Tactic:
rw [← w, colimit.w_apply]

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

Goal state before:
pp: R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ).det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det

Tactic:
rw [← det_transpose]

Goal state after:
R : Type v
inst✝ : CommRing R
n : ℕ
A : Matrix (Fin n.succ) (Fin n.succ) R
i : Fin n.succ
x✝ : i ∈ univ
⊢ (-1) ^ ↑i * Aᵀ i 0 * (Aᵀ.submatrix i.succAbove Fin.succ)ᵀ.det =
    (-1) ^ ↑i * A 0 i * (A.submatrix Fin.succ i.succAbove).det
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case neg
R : Type uR
ι : Type uι
M₁ : ι → Type v₁
M₂ : Type v₂
inst✝⁵ : Semiring R
inst✝⁴ : (i : ι) → AddCommGroup (M₁ i)
inst✝³ : AddCommGroup M₂
inst✝² : (i : ι) → Module R (M₁ i)
inst✝¹ : Module R M₂
f : MultilinearMap R M₁ M₂
inst✝ : LinearOrder ι
a b : (i : ι) → M₁ i
k : ι
s : Finset ι
hk : ∀ x ∈ s, k < x
ih : f a - f (s.piecewise b a) = ∑ i ∈ s, f fun j ↦ if j ∈ s → j < i then a j else if i = j then a j - b j else b j
i : ι
h₁ : ¬(i = k ∨ i ∈ s → i < k)
h₂ : ¬k = i
⊢ update (s.piecewise b a) k (s.piecewise b a k - b k) i = b i

Tactic:
· push Not at h₁
      rw [update_of_ne (Ne.symm h₂), s.piecewise_eq_of_mem _ _ (h₁.1.resolve_left <| Ne.symm h₂)]

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ RingCat
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      ofHom
        (SemiRingCat.Hom.hom
          ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRingCat)).ι.app x✝)) =
    ofHom
        (SemiRingCat.Hom.hom
          ((SemiRingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ RingCat SemiRingCat)).ι.app x✝¹)) ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
ext
        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget RingCat)).ι.naturality_apply f _

Goal state after:
Module: Mathlib.Algebra.Category.Ring.FilteredColimits

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ CommRingCat
x✝¹ x✝ : J
f : x✝¹ ⟶ x✝
⊢ F.map f ≫
      ofHom (RingCat.Hom.hom ((RingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommRingCat RingCat)).ι.app x✝)) =
    ofHom (RingCat.Hom.hom ((RingCat.FilteredColimits.colimitCocone (F ⋙ forget₂ CommRingCat RingCat)).ι.app x✝¹)) ≫
      ((Functor.const J).obj (colimit F)).map f

Tactic:
ext
        simpa using! (Types.TypeMax.colimitCocone (F ⋙ forget CommRingCat)).ι.naturality_apply f _

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 t
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
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
k : J
f : i ⟶ k
g : j ⟶ k
hfg : (ConcreteCategory.hom ((F ⋙ forget C).map f)) x = (ConcreteCategory.hom (F.map g)) y
h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g
⊢ (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y

Tactic:
change E.ι.app i x = E.ι.app j y

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
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
D : Cocone F
i j : J
x : ToType (F.obj i)
y : ToType (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
k : J
f : i ⟶ k
g : j ⟶ k
hfg : (ConcreteCategory.hom ((F ⋙ forget C).map f)) x = (ConcreteCategory.hom (F.map g)) y
h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g
⊢ (ConcreteCategory.hom (E.ι.app i)) x = (ConcreteCategory.hom (E.ι.app j)) y
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X X' : C
Y : Cᵒᵖ
f : unop Y ⟶ X
g : X ⟶ X'
⊢ (ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map g).app Y)) (shrinkYonedaObjObjEquiv.symm f) =
    shrinkYonedaObjObjEquiv.symm (f ≫ g)

Tactic:
by
  simp [shrinkYoneda, shrinkYonedaObjObjEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.ShrinkYoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X X' : C
Y : Cᵒᵖ
f : (shrinkYoneda.{w, v, u}.obj X).obj Y
g : X ⟶ X'
⊢ shrinkYonedaObjObjEquiv ((ConcreteCategory.hom ((shrinkYoneda.{w, v, u}.map g).app Y)) f) =
    shrinkYonedaObjObjEquiv f ≫ g

Tactic:
by
  simp [shrinkYoneda, shrinkYonedaObjObjEquiv]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f =
    ((limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))) ≫
      (limitObjIsoLimitCompEvaluation F j).inv

Tactic:
Iso.eq_comp_inv,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasLimitsOfShape J C
i j : K
F : J ⥤ K ⥤ C
f : i ⟶ j
⊢ (limit F).map f ≫ (limitObjIsoLimitCompEvaluation F j).hom =
    (limitObjIsoLimitCompEvaluation F i).hom ≫ limMap (F.whiskerLeft ((evaluation K C).map f))
Module: Mathlib.CategoryTheory.Functor.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} C₄
inst✝¹ : Category.{v_5, u_5} C₁₂
inst✝ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ G₂₃' : C₂ ⥤ C₃ ⥤ C₂₃
φ : G₂₃ ⟶ G₂₃'
X₁ : C₁
X₂ Y₂ : C₂
f : X₂ ⟶ Y₂
X₃ : C₃
⊢ (F.obj X₁).map ((G₂₃.map f).app X₃) ≫ (F.obj X₁).map ((φ.app Y₂).app X₃) =
    (F.obj X₁).map ((φ.app X₂).app X₃) ≫ (F.obj X₁).map ((G₂₃'.map f).app X₃)

Tactic:
simp only [← NatTrans.comp_app, ← Functor.map_comp, NatTrans.naturality]

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 Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ₘ f = (α_ X Y Z).hom ≫ (𝟙 X ⊗ₘ 𝟙 Y ⊗ₘ f) ≫ (α_ X Y Z').inv

Tactic:
rw [← assoc, ← associator_naturality]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z Z' : C
f : Z ⟶ Z'
⊢ 𝟙 (X ⊗ Y) ⊗ₘ f = (((𝟙 X ⊗ₘ 𝟙 Y) ⊗ₘ f) ≫ (α_ X Y Z').hom) ≫ (α_ X Y Z').inv
Module: Mathlib.CategoryTheory.Monoidal.Category

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
W X Y : C
f : W ⟶ X
g : X ⟶ Y
Z : C
⊢ (f ≫ g) ▷ Z = f ▷ Z ≫ g ▷ Z

Tactic:
simp [← tensorHom_id]

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 Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z = (α_ X Y Z).hom ≫ (𝟙 X ⊗ₘ f ⊗ₘ 𝟙 Z) ≫ (α_ X Y' Z).inv

Tactic:
rw [← assoc, ← associator_naturality]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Y' : C
f : Y ⟶ Y'
Z : C
⊢ (𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z = (((𝟙 X ⊗ₘ f) ⊗ₘ 𝟙 Z) ≫ (α_ X Y' Z).hom) ≫ (α_ X Y' Z).inv
Module: Mathlib.CategoryTheory.Monoidal.NaturalTransformation

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
E' : Type u₄
inst✝⁶ : Category.{v₄, u₄} E'
inst✝⁵ : MonoidalCategory E'
F₁ F₂ F₃ : C ⥤ D
τ : F₁ ⟶ F₂
inst✝⁴ : F₁.LaxMonoidal
inst✝³ : F₂.LaxMonoidal
inst✝² : F₃.LaxMonoidal
G₁ : D ⥤ E
inst✝¹ : G₁.LaxMonoidal
inst✝ : IsMonoidal τ
⊢ IsMonoidal (Functor.whiskerRight τ G₁)

Tactic:
by
  rw [← Functor.hcomp_id]
  infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X₁ X₂ : D
⊢ F.map (𝟙 X₁ ⊗ₘ 𝟙 X₂) = F.map (𝟙 (X₁ ⊗ X₂))

Tactic:
cases fData; cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
g₁ : Y₁✝ ⟶ Z₁✝
g₂ : Y₂✝ ⟶ Z₂✝
⊢ F.map ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂)) = F.map (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)

Tactic:
cases fData; cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategoryStruct D
F : D ⥤ C
inst✝ : F.Faithful
fData : InducingFunctorData F
X Y : D
⊢ F.map ((α_ X (𝟙_ D) Y).hom ≫ X ◁ (λ_ Y).hom) = F.map ((ρ_ X).hom ▷ Y)

Tactic:
cases fData; cat_disch

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

Goal state before:
pp: case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ δ F x✝¹ x✝ = μ F x✝¹ x✝ ≫ δ F x✝¹ x✝

Tactic:
← μIso_inv

Goal state after:
case μ
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : MonoidalCategory D
F : C ⥤ D
a b : F.Monoidal
eq : a.toOplaxMonoidal = b.toOplaxMonoidal
x✝¹ x✝ : C
⊢ μ F x✝¹ x✝ ≫ (μIso F x✝¹ x✝).inv = μ F x✝¹ x✝ ≫ δ F 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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod' G)).2 = ε G

Tactic:
change _ ≫ G.map (𝟙 _) = _

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
F : C ⥤ D
G : C ⥤ E
inst✝¹ : F.LaxMonoidal
inst✝ : G.LaxMonoidal
⊢ (ε (F.prod G)).2 ≫ G.map (𝟙 (𝟙_ (C × C)).2) = ε G