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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
v : ↥(Subgroup.zpowers ↑c)
m : ℤ
hm : (fun x ↦ ↑c ^ x) m = ↑v
⊢ (↑v).support ⊆ g.support

Tactic:
simp only [← hm]

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
c : ↥g.cycleFactorsFinset
v : ↥(Subgroup.zpowers ↑c)
m : ℤ
hm : (fun x ↦ ↑c ^ x) m = ↑v
⊢ (↑c ^ m).support ⊆ g.support
Module: Mathlib.GroupTheory.Perm.Cycle.Type

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
⊢ σ.IsThreeCycle

Tactic:
by_cases h1 : σ.cycleType.erase n = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle

case neg
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
h : #σ.support = 3
h0 : ¬σ.cycleType = 0
n : ℕ
hn : n ∈ σ.cycleType
h1 : ¬σ.cycleType.erase n = 0
⊢ σ.IsThreeCycle
Module: Mathlib.GroupTheory.Perm.Cycle.Factors

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f c : Perm α
a : α
ha : a ∈ c.support
hc : c ∈ f.cycleFactorsFinset
this : f.cycleOf a = c.cycleOf a
⊢ c = f.cycleOf a

Tactic:
by
    rw [this]
    apply symm
    exact
      Equiv.Perm.IsCycle.cycleOf_eq (Equiv.Perm.mem_cycleFactorsFinset_iff.mp hc).left
        (Equiv.Perm.mem_support.mp ha)

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

Goal state before:
pp: case e_a.inl
ι : Type uι
κ : ι → Type uκ
R : Type uR
ι' : Type u_1
inst✝⁵ : DecidableEq ι
inst✝⁴ : Fintype ι
inst✝³ : CommSemiring R
inst✝² : (i : ι) → Fintype (κ i)
inst✝¹ : (i : ι) → DecidableEq (κ i)
inst✝ : DecidableEq ι'
r : R
x : (i : ι) → Π₀ (x : κ i), R
p : (i : ι) → κ i
j : ι'
⊢ ((freeDFinsuppEquiv (DFinsupp.single (p, j) 1)) x) j = (DFinsupp.single (p, j).2 (∏ i, (x i) ((p, j).1 i))) j

Tactic:
suffices ∀ (l : ι), (x l) (p l) = 0 → 0 = ∏ i, (x i) (p i) by
      simpa [freeDFinsuppEquiv_def, MultilinearMap.piRingEquiv, DFinsupp.sigmaCurryEquiv,
        fromDFinsuppEquiv_apply]
    exact fun i h ↦ (Finset.prod_eq_zero (Finset.mem_univ i) h).symm

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

Goal state before:
pp: ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ f v = 0

Tactic:
suffices f (update v i (g i • v i)) = 0 by
    rw [f.map_update_smul, Function.update_eq_self, smul_eq_zero] at this
    exact Or.resolve_left this hz

Goal state after:
ι : Type u_7
K : Type u_12
M : Type u_13
N : Type u_14
inst✝⁶ : Ring K
inst✝⁵ : IsDomain K
inst✝⁴ : AddCommGroup M
inst✝³ : Module K M
inst✝² : AddCommGroup N
inst✝¹ : Module K N
inst✝ : IsTorsionFree K N
f : M [⋀^ι]→ₗ[K] N
v : ι → M
h✝ : ¬LinearIndependent K v
s : Finset ι
g : ι → K
h : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
hz : g i ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ f (update v i (g i • v i)) = 0
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
mul_add

Goal state after:
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ RingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
Module: Mathlib.Algebra.Category.Ring.Colimits

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

Tactic:
mul_add

Goal state after:
case a.left_distrib
J : Type v
inst✝ : SmallCategory J
F : J ⥤ CommRingCat
s : Cocone F
x✝ y✝ x y z : Prequotient F
⊢ descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z =
    descFunLift F s x * descFunLift F s y + descFunLift F s x * descFunLift F s z
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case pos
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
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
⊢ ∑ j ∈ A i₀, g i₀ j = update (fun i ↦ ∑ j ∈ A i, g i j) i₀ (∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j) i₀

Tactic:
update_self

Goal state after:
case pos
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
C_subset_A : ∀ (i : ι), C i ⊆ A i
i : ι
hi : i = i₀
⊢ ∑ j ∈ A i₀, g i₀ j = ∑ j ∈ B i₀, g i₀ j + ∑ j ∈ C i₀, g i₀ j
Module: Mathlib.LinearAlgebra.Matrix.SemiringInverse

Goal state before:
pp: n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
⊢ ∑ x, ∑ i_1 ∈ ofSign s with i_1 i = x, A i x * ∏ k ∈ {i}ᶜ, A k (i_1 k) =
    ∑ j, ∑ σ ∈ ofSign s with σ i = j, ∏ k, A k (σ k)

Tactic:
refine sum_congr rfl fun x hx ↦ sum_congr rfl fun σ hσ ↦ ?_

Goal state after:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
s : ℤˣ
A : Matrix n n R
i : n
key : ∑ j, ∑ i ∈ ofSign s with i i = j, ∏ k, A k (i k) = ∑ i ∈ ofSign s, ∏ k, A k (i k)
x : n
hx : x ∈ univ
σ : Perm n
hσ : σ ∈ {i_1 ∈ ofSign s | i_1 i = x}
⊢ A i x * ∏ k ∈ {i}ᶜ, A k (σ k) = ∏ k, A k (σ k)
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Basic

Goal state before:
pp: case insert
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i : n
s : Finset n
_hi : i ∉ s
ih :
  ∀ {B : Matrix n n R} (c : n → R),
    (∀ i ∉ s, c i = 0) → ∀ k ∉ s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det
B : Matrix n n R
⊢ ∀ (c : n → R),
    (∀ i_1 ∉ insert i s, c i_1 = 0) → ∀ k ∉ insert i s, (∀ (i j : n), A i j = B i j + c i * B k j) → A.det = B.det

Tactic:
intro c hs k hk A_eq
    have hAi : A i = B i + c i • B k := funext (A_eq i)
    rw [@ih (updateRow B i (A i)) (Function.update c i 0), hAi, det_updateRow_add_smul_self]
    · exact mt (fun h => show k ∈ insert i s from h ▸ Finset.mem_insert_self _ _) hk
    · intro i' hi'
      rw [Function.update_apply]
      split_ifs with hi'i
      · rfl
      · exact hs i' fun h => hi' ((Finset.mem_insert.mp h).resolve_left hi'i)
    · exact k
    · exact fun h => hk (Finset.mem_insert_of_mem h)
    · intro i' j'
      rw [updateRow_apply, Function.update_apply]
      split_ifs with hi'i
      · simp [hi'i]
      rw [A_eq, updateRow_ne fun h : k = i => hk <| h ▸ Finset.mem_insert_self k s]

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

Goal state before:
pp: case neg
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := M.updateRow k.succ (N k.succ)
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
⊢ i.castSucc ≠ k.succ

Tactic:
apply ne_of_lt

Goal state after:
case neg
R : Type v
inst✝ : CommRing R
n : ℕ
k✝ : Fin (n + 1)
k : Fin n
ih :
  ∀ (c : Fin n → R),
    (∀ (i : Fin n), k.castSucc < i.succ → c i = 0) →
      ∀ {M N : Matrix (Fin n.succ) (Fin n.succ) R},
        (∀ (j : Fin n.succ), M 0 j = N 0 j) →
          (∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j) → M.det = N.det
c : Fin n → R
hc : ∀ (i : Fin n), k.succ < i.succ → c i = 0
M N : Matrix (Fin n.succ) (Fin n.succ) R
h0 : ∀ (j : Fin n.succ), M 0 j = N 0 j
hsucc : ∀ (i : Fin n) (j : Fin n.succ), M i.succ j = N i.succ j + c i * M i.castSucc j
M' : Matrix (Fin n.succ) (Fin n.succ) R := ⋯
hM' : M' = M.updateRow k.succ (N k.succ)
hM : M = M'.updateRow k.succ (M' k.succ + c k • M k.castSucc)
k_ne_succ : k.castSucc ≠ k.succ
M_k : M k.castSucc = M' k.castSucc
i : Fin n
j : Fin n.succ
hik : ¬i = k
hik2 : ¬k < i
⊢ i.castSucc < k.succ
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case inl
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
z : (i : ι) → M₁ i
i : ↑s
⊢ z ↑i = update (fun j ↦ m (e.symm j) ↑j) i (z ↑i) i

Tactic:
update_self

Goal state after:
case inl
ι : Type u_3
M₁ : ι → Type u_1
α : Type u_2
inst✝¹ : DecidableEq α
s : Set ι
inst✝ : DecidableEq { x // x ∈ s }
e : α ≃ ↑s
m : α → (i : ι) → M₁ i
z : (i : ι) → M₁ i
i : ↑s
⊢ z ↑i = z ↑i
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case e'_3.e'_6
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁹ : CommSemiring R
inst✝⁸ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁷ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : (i : Fin n.succ) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
f✝ f' : MultilinearMap R M₁ M₂
inst✝² : (i : ι) → AddCommMonoid (M₁' i)
inst✝¹ : (i : ι) → Module R (M₁' i)
inst✝ : DecidableEq ι
f : (i : ι) → M₁ i →ₗ[R] M₁' i
i : ι
f₁ f₂ : M₁ i →ₗ[R] M₁' i
g : MultilinearMap R M₁' M₂
x : (i : ι) → M₁ i
c : (i : ι) → (M₁ i →ₗ[R] M₁' i) → M₁' i := fun i f ↦ f (x i)
j : ι
⊢ (update f i f₂ j) (x j) = update (fun j ↦ (f j) (x j)) i (f₂ (x i)) j

Tactic:
· exact Function.apply_update c f i f₂ j

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

Goal state before:
pp: J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ SemiRingCat
inst✝ : IsFiltered J
x y z : ↑(R F)
⊢ x * (y + z) = x * y + x * z

Tactic:
by
      refine Quot.induction_on₃ x y z ?_; clear x y z; intro x y z
      obtain ⟨j₁, x⟩ := x; obtain ⟨j₂, y⟩ := y; obtain ⟨j₃, z⟩ := z
      let k := IsFiltered.max₃ j₁ j₂ j₃
      let f := IsFiltered.firstToMax₃ j₁ j₂ j₃
      let g := IsFiltered.secondToMax₃ j₁ j₂ j₃
      let h := IsFiltered.thirdToMax₃ j₁ j₂ j₃
      erw [colimit_add_mk_eq _ ⟨j₂, _⟩ ⟨j₃, _⟩ k g h, colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨k, _⟩ k f (𝟙 k),
        colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₂, _⟩ k f g, colimit_mul_mk_eq _ ⟨j₁, _⟩ ⟨j₃, _⟩ k f h,
        colimit_add_mk_eq _ ⟨k, _⟩ ⟨k, _⟩ k (𝟙 k) (𝟙 k)]
      simp only [CategoryTheory.Functor.map_id]
      erw [left_distrib (F.map f x) (F.map g y) (F.map h z)]
      rfl

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

Goal state before:
pp: case pos
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 v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j

Tactic:
by_cases hji : j < i

Goal state after:
case pos
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 v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : j < i
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j

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 v : (i : ι) → M₁ i
s : Finset ι
i : ι
hi : i ∈ s
j : ι
hjs : j ∈ s
hji : ¬j < i
⊢ (if j ∈ s → j < i then s.piecewise a v j else if i = j then s.piecewise a v j - b j else b j) =
    if j < i then a j else if j = i then a j - b j else b j
Module: Mathlib.LinearAlgebra.Multilinear.Basic

Goal state before:
pp: case refine_1
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : j = i
⊢ update x i (c • x i) i ∈ p i

Tactic:
update_self

Goal state after:
case refine_1
R : Type uR
S : Type uS
ι : Type uι
n : ℕ
M : Fin n.succ → Type v
M₁ : ι → Type v₁
M₁' : ι → Type v₁'
M₁'' : ι → Type v₁''
M₂ : Type v₂
M₃ : Type v₃
M₄ : Type v₄
M' : Type v'
inst✝⁷ : Ring R
inst✝⁶ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M₂
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M'
inst✝¹ : Module R M₂
inst✝ : Nonempty ι
f : MultilinearMap R M₁ M₂
p : (i : ι) → Submodule R (M₁ i)
c : R
x✝¹ : M₂
x✝ : x✝¹ ∈ ⇑f '' {v | ∀ (i : ι), v i ∈ p i}
x : (i : ι) → M₁ i
hx : x ∈ {v | ∀ (i : ι), v i ∈ p i}
hf : f x = x✝¹
i : ι
this : DecidableEq ι := Classical.decEq ι
j : ι
hij : j = i
⊢ c • x i ∈ p i
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
F : J ⥤ K ⥤ C
c : (k : K) → LimitCone (F.flip.obj k)
j₁ j₂ : J
g : j₁ ⟶ j₂
⊢ ((const J).obj
            { obj := fun k ↦ (c k).cone.pt,
              map := fun {k₁ k₂} f ↦ (c k₂).isLimit.lift { pt := (c k₁).cone.pt, π := (c k₁).cone.π ≫ F.flip.map f },
              map_id := ⋯, map_comp := ⋯ }).map
        g ≫
      { app := fun k ↦ (c k).cone.π.app j₂, naturality := ⋯ } =
    { app := fun k ↦ (c k).cone.π.app j₁, naturality := ⋯ } ≫ F.map g

Tactic:
by ext k; exact (c k).cone.π.naturality g

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) 1 = 1

Tactic:
simp; rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget MonCat)).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) (x✝¹ * x✝) =
    (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) x✝¹ *
      (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget MonCat)).π.app j)) x✝

Tactic:
simp; rfl

Goal state after:
Module: Mathlib.Algebra.Category.MonCat.Limits

Goal state before:
pp: J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ MonCat
inst✝ : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
c : Cone (F ⋙ forget MonCat)
t : IsLimit c
this : Small.{u, max u v} ↑(F ⋙ forget MonCat).sections
s✝ : Cone F
⊢ (ConcreteCategory.hom ((Types.Small.limitConeIsLimit (F ⋙ forget MonCat)).lift ((forget MonCat).mapCone s✝))) 1 = 1

Tactic:
simp; rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
j : J
x✝¹ x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) (x✝¹ + x✝) =
    (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝¹ +
      (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝

Tactic:
simp; rfl

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Limits

Goal state before:
pp: R : Type u
inst✝² : Ring R
J : Type v
inst✝¹ : Category.{t, v} J
F : J ⥤ ModuleCat R
inst✝ : Small.{w, max v w} ↑(F ⋙ forget (ModuleCat R)).sections
j : J
x✝¹ : R
x✝ : (Types.Small.limitCone (F ⋙ forget (ModuleCat R))).pt
⊢ (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) (x✝¹ • x✝) =
    (RingHom.id R) x✝¹ • (ConcreteCategory.hom ((Types.Small.limitCone (F ⋙ forget (ModuleCat R))).π.app j)) x✝

Tactic:
simp; rfl

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ f ⊗ₘ g ⊗ₘ h = (α_ X Y Z).inv ≫ ((f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X' Y' Z').hom

Tactic:
associator_naturality,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X X' Y Y' Z Z' : C
f : X ⟶ X'
g : Y ⟶ Y'
h : Z ⟶ Z'
⊢ f ⊗ₘ g ⊗ₘ h = (α_ X Y Z).inv ≫ (α_ X Y Z).hom ≫ (f ⊗ₘ g ⊗ₘ h)
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✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ G.obj (F.obj x✝¹) ◁ G.map (F.map x✝) ≫ μ G (F.obj x✝¹) (F.obj Y✝) ≫ G.map (μ F x✝¹ Y✝) =
    (μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝)) ≫ G.map (F.map (x✝¹ ◁ x✝))

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.LaxMonoidal
inst✝ : G.LaxMonoidal
X✝ Y✝ x✝¹ : C
x✝ : X✝ ⟶ Y✝
⊢ μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (F.obj x✝¹ ◁ F.map x✝) ≫ G.map (μ F x✝¹ Y✝) =
    (μ G (F.obj x✝¹) (F.obj X✝) ≫ G.map (μ F x✝¹ X✝)) ≫ G.map (F.map (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.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (μ F 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.obj (F.obj x✝²) ◁ G.map (μ F x✝¹ x✝) ≫ μ G (F.obj x✝²) (F.obj (x✝¹ ⊗ x✝)) ≫ G.map (μ F x✝² (x✝¹ ⊗ x✝))

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.LaxMonoidal
inst✝ : G.LaxMonoidal
x✝² x✝¹ x✝ : C
⊢ μ G (F.obj x✝²) (F.obj x✝¹) ▷ G.obj (F.obj x✝) ≫
      μ G (F.obj x✝² ⊗ F.obj x✝¹) (F.obj x✝) ≫
        G.map (μ F 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 (F.obj x✝²) (F.obj x✝¹ ⊗ F.obj x✝) ≫ G.map (F.obj x✝² ◁ μ F 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 ⥤ C
adj : F ⊣ G
inst✝ : F.OplaxMonoidal
X Y : D
f : X ⟶ Y
X' : D
⊢ adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X')) =
    adj.unit.app (G.obj X ⊗ G.obj X') ≫
      G.map (δ F (G.obj X) (G.obj X') ≫ (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X')

Tactic:
suffices F.map (G.map f) ▷ F.obj (G.obj X') ≫ _ =
      (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ _ by rw [this]

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 Y : D
f : X ⟶ Y
X' : D
⊢ F.map (G.map f) ▷ F.obj (G.obj X') ≫ (adj.counit.app Y ⊗ₘ adj.counit.app X') =
    (adj.counit.app X ⊗ₘ adj.counit.app X') ≫ f ▷ X'