mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
P : Extension R S
R' : Type ?u.16
S' : Type ?u.18
inst✝¹¹ : CommRing R'
inst✝¹⁰ : CommRing S'
inst✝⁹ : Algebra R' S'
P' : Extension R' S'
R'' : Type ?u.29
S'' : Type ?u.31
inst✝⁸ : CommRing R''
inst✝⁷ : CommRing S''
inst✝⁶ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R' R''
inst✝³ : Algebra R R''
inst✝² : Algebra S S'
inst✝¹ : Algebra S' S''
inst✝ : Algebra S S''
f : P.Hom P'
alg : Algebra P.Ring P'.Ring
halg : algebraMap P.Ring P'.Ring = f.toRingHom
x : ↥P.ker
⊢ f.toRingHom ↑x ∈ P'.ker

Tactic:
simp [show algebraMap P.Ring S x = 0 from x.2]

Goal state after:
Module: Mathlib.Algebra.Module.Presentation.DirectSum

Goal state before:
pp: A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A fun g ↦ s.var ⟨i, g⟩) ((relations i).relation r) =
    (Finsupp.linearCombination A s.var) ((directSum relations).relation ⟨i, r⟩)

Tactic:
symm

Goal state after:
A : Type u
inst✝⁵ : Ring A
ι : Type w
inst✝⁴ : DecidableEq ι
relations : ι → Relations A
M : ι → Type v
inst✝³ : (i : ι) → AddCommGroup (M i)
inst✝² : (i : ι) → Module A (M i)
N : Type v
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ (Finsupp.linearCombination A s.var) ((directSum relations).relation ⟨i, r⟩) =
    (Finsupp.linearCombination A fun g ↦ s.var ⟨i, g⟩) ((relations i).relation r)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 ↦ (Q.ofComp P).val x1 ^ x2) =
    C ((aeval P.val) ((monomial v₂) a)) * v₁.prod fun n e ↦ X n ^ e

Tactic:
simp only [ofComp_val, aeval_monomial]

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
v₁ : ι' →₀ ℕ
v₂ : ι →₀ ℕ
a : R
⊢ (a • (v₁.sumElim v₂).prod fun x1 x2 ↦ Sum.elim X (⇑C ∘ P.val) x1 ^ x2) =
    C ((algebraMap R S) a * v₂.prod fun i k ↦ P.val i ^ k) * v₁.prod fun n e ↦ X n ^ e
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
m₁ m₂ : M
⊢ s.var (m₁ + m₂) = s.var m₁ + s.var m₂

Tactic:
symm

Goal state after:
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
m₁ m₂ : M
⊢ s.var m₁ + s.var m₂ = s.var (m₁ + m₂)
Module: Mathlib.Algebra.Module.Presentation.Tautological

Goal state before:
pp: A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
a : A
m : M
⊢ s.var (a • m) = (RingHom.id A) a • s.var m

Tactic:
symm

Goal state after:
A : Type u
inst✝⁴ : Ring A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
N : Type w
inst✝¹ : AddCommGroup N
inst✝ : Module A N
s : (tautologicalRelations A M).Solution N
a : A
m : M
⊢ (RingHom.id A) a • s.var m = s.var (a • m)
Module: Mathlib.RingTheory.Extension.Generators

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x✝ : (Q.comp P).Ring
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
x : (Q.comp P).Ring
j : (ι' →₀ ℕ) × (ι →₀ ℕ)
⊢ j ∈ (↑(Finset.map (↑e).toEmbedding (support x)))ᶜ →
    j ∈ (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0)ᶜ

Tactic:
obtain ⟨j, rfl⟩ := e.surjective j

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
ι' : Type u_3
T : Type u_7
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T ι'
P : Generators R S ι
this : DecidableEq (ι' →₀ ℕ) := Classical.decEq (ι' →₀ ℕ)
x✝ : (Q.comp P).Ring
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
x : (Q.comp P).Ring
j : ι' ⊕ ι →₀ ℕ
⊢ e j ∈ (↑(Finset.map (↑e).toEmbedding (support x)))ᶜ →
    e j ∈ (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0)ᶜ
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case e'_2
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card ↥s)), (fun i ↦ (↑(e i)).2) i = ∑ j, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i, a i j • (fun i ↦ ↑(↑(e i)).1) i = 0
x✝² : ℕ
x✝¹ : Fin (Fintype.card ↥s) → Fin x✝² → R
x✝ : Fin x✝² → N
a✝ : Fin x✝²
⊢ ∑ i, x✝¹ i a✝ • ((fun i ↦ (↑i).1) ∘ ⇑e) i = 0 ↔ ∑ i, x✝¹ i a✝ • (fun i ↦ ↑(↑(e i)).1) i = 0

Tactic:
symm

Goal state after:
case e'_2
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this :
  ∃ k a y,
    (∀ (i : Fin (Fintype.card ↥s)), (fun i ↦ (↑(e i)).2) i = ∑ j, a i j • y j) ∧
      ∀ (j : Fin k), ∑ i, a i j • (fun i ↦ ↑(↑(e i)).1) i = 0
x✝² : ℕ
x✝¹ : Fin (Fintype.card ↥s) → Fin x✝² → R
x✝ : Fin x✝² → N
a✝ : Fin x✝²
⊢ ∑ i, x✝¹ i a✝ • (fun i ↦ ↑(↑(e i)).1) i = 0 ↔ ∑ i, x✝¹ i a✝ • ((fun i ↦ (↑i).1) ∘ ⇑e) i = 0
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
R' : Type u_3
inst✝⁵ : CommSemiring R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Subalgebra.toSubmodule (Algebra.adjoin R' s)
⊢ ∃ t, t • x ∈ Subalgebra.toSubmodule (Algebra.adjoin R s)

Tactic:
Algebra.adjoin_eq_span

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
R' : Type u_3
inst✝⁵ : CommSemiring R'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra R' S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R R' S
inst✝ : IsLocalization M R'
s : Set S
x : S
hx : x ∈ Submodule.span R' ↑(Submonoid.closure s)
⊢ ∃ t, t • x ∈ Submodule.span R ↑(Submonoid.closure s)
Module: Mathlib.RingTheory.Support

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
this : { asIdeal := p, isPrime := ⋯ } ∈ (Module.support R M)ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)

Tactic:
Module.support_eq_zeroLocus,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Module.Finite R M
p : Ideal R
inst✝¹ : p.IsPrime
inst✝ : Subsingleton (LocalizedModule p.primeCompl M)
this : { asIdeal := p, isPrime := ⋯ } ∈ (zeroLocus ↑(Module.annihilator R M))ᶜ
⊢ ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
t : Set R
ht : span t = ⊤
H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG
⊢ I.FG

Tactic:
apply Module.Finite.iff_fg.mp

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
t : Set R
ht : span t = ⊤
H : ∀ (g : ↑t), (map (algebraMap R (Localization.Away ↑g)) I).FG
⊢ Module.Finite R ↥I
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: case e_a.e_a.e_a.e_6
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth v j = v j.succ
H₂ : j.succ.removeNth v i = v i.castSucc
⊢ i.removeNth (j.succ.removeNth v) = j.removeNth (i.castSucc.removeNth v)

Tactic:
rw [removeNth_removeNth_eq_swap]

Goal state after:
case e_a.e_a.e_a.e_6
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
H₁ : i.castSucc.removeNth v j = v j.succ
H₂ : j.succ.removeNth v i = v i.castSucc
⊢ (i.predAbove j.succ).removeNth ((j.succ.succAbove i).removeNth v) = j.removeNth (i.castSucc.removeNth v)
Module: Mathlib.LinearAlgebra.ExteriorPower.Pairing

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → Module.Dual R M
i j : Fin n
hf : f i = f j
hij : i ≠ j
v : Fin n → M
⊢ (LinearMap.compAlternatingMap
        (((toTensorPower R M n).dualMap.compMultilinearMap (TensorPower.multilinearMapToDual R M n)).toFun f)
        (ιMulti R n))
      v =
    (LinearMap.compAlternatingMap 0 (ιMulti R n)) v

Tactic:
suffices Matrix.det (n := Fin n) (.of (fun i j ↦ f j (v i))) = 0 by
      simpa [Matrix.det_apply] using this

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
f : Fin n → Module.Dual R M
i j : Fin n
hf : f i = f j
hij : i ≠ j
v : Fin n → M
⊢ (Matrix.of fun i j ↦ (f j) (v i)).det = 0
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
n : ↥N
m : ↥M
⊢ (N.mulMap M) (n ⊗ₜ[R] m) = (M.mulMap N) (m ⊗ₜ[R] n)

Tactic:
mulMap_tmul

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
hc : ∀ (m : ↥M) (n : ↥N), Commute ↑m ↑n
n : ↥N
m : ↥M
⊢ ↑n * ↑m = ↑m * ↑n
Module: Mathlib.LinearAlgebra.TensorProduct.Submodule

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
⊢ (M.mulMap N).range = M * N

Tactic:
refine le_antisymm ?_ (mul_le.2 fun m hm n hn ↦ ⟨⟨m, hm⟩ ⊗ₜ[R] ⟨n, hn⟩, rfl⟩)
  rintro _ ⟨x, rfl⟩
  induction x with
  | zero => rw [map_zero]; exact zero_mem _
  | tmul a b => exact mul_mem_mul a.2 b.2
  | add a b ha hb => rw [map_add]; exact add_mem ha hb

Goal state after:
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v)) = ⊤
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)

Tactic:
eq_top_iff,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : FinitePresentation R M
H : Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype 𝔪))
ι : Type u
v : ι → M
hv : Submodule.span R (Set.range v) = ⊤
this : ⊤ ≤ Submodule.span R (Set.range (⇑((TensorProduct.mk R k M) 1) ∘ v))
⊢ ∃ κ a b, ∀ (i : κ), b i = v (a i)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹⁴ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹³ : (i : ι) → AddCommMonoid (s i)
inst✝¹² : (i : ι) → Module R (s i)
M : Type u_8
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
E : Type u_9
inst✝⁹ : AddCommMonoid E
inst✝⁸ : Module R E
F : Type u_10
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Monoid R₁
inst✝⁵ : DistribMulAction R₁ R
inst✝⁴ : SMulCommClass R₁ R R
inst✝³ : Monoid R₂
inst✝² : DistribMulAction R₂ R
inst✝¹ : SMulCommClass R₂ R R
inst✝ : SMulCommClass R₁ R₂ R
r' : R₁
r'' : R₂
x : ⨂[R] (i : ι), s i
xr : R
xf : (i : ι) → s i
⊢ r' • r'' • tprodCoeff R xr xf = r'' • r' • tprodCoeff R xr xf

Tactic:
simp only [smul_tprodCoeff', smul_comm]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)

Tactic:
have rhs_eq : ∀ a b c, rhs a b c = a ₜ* (b ₜ* c) := fun _ _ _ => rfl

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb nc : ℕ
a : ⨂[R]^na M
b : ⨂[R]^nb M
c : ⨂[R]^nc M
mul : (n m : ℕ) → ⨂[R]^n M →ₗ[R] ⨂[R]^m M →ₗ[R] ⨂[R]^(n + m) M :=
  fun n m ↦ (TensorProduct.mk R (⨂[R]^n M) (⨂[R]^m M)).compr₂ ↑mulEquiv
e : ⨂[R]^(na + nb + nc) M ≃ₗ[R] ⨂[R]^(na + (nb + nc)) M := cast R M ⋯
lhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^(na + nb) M) (⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
      ((mul (na + nb) nc).compr₂ ↑e) ∘ₗ
    mul na nb
lhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M),
    ((lhs a) b) c = e (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c)
rhs : ⨂[R]^na M →ₗ[R] ⨂[R]^nb M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M :=
  (((LinearMap.llcomp R (⨂[R]^nb M) (⨂[R]^nc M →ₗ[R] ⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M)
          (⨂[R]^na M →ₗ[R] ⨂[R]^nc M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
        ↑LinearMap.lflip)
      ((LinearMap.llcomp R (⨂[R]^nc M) (⨂[R]^(nb + nc) M) (⨂[R]^na M →ₗ[R] ⨂[R]^(na + (nb + nc)) M))
          (mul na (nb + nc)).flip ∘ₗ
        mul nb nc)).flip
rhs_eq :
  ∀ (a : ⨂[R]^na M) (b : ⨂[R]^nb M) (c : ⨂[R]^nc M), ((rhs a) b) c = GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
⊢ (cast R M ⋯) (GradedMonoid.GMul.mul (GradedMonoid.GMul.mul a b) c) =
    GradedMonoid.GMul.mul a (GradedMonoid.GMul.mul b c)
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n * a n j + ∑ i ∈ s, f i * a' i = ∑ x, f ↑x * a x j

Tactic:
a_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n * a' ↑n + ∑ i ∈ s, f i * a' i = ∑ x, f ↑x * a' ↑x
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsLocalRing R
inst✝ : Flat R M
ι : Type u
f : ι → R
n✝ : ι
s : Finset ι
hn : n✝ ∉ s
ih : ∀ (v : ι → M), LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v) → ∑ i ∈ s, f i • v i = 0 → ∀ i ∈ s, f i = 0
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
hfv : ∑ i, f ↑i • v ↑i = 0
i : ι
hi : i ∈ insert n✝ s
l : ℕ
a : ↥(insert n✝ s) → Fin l → R
y : Fin l → M
hay : ∀ (i : ↥(insert n✝ s)), (fun i ↦ v ↑i) i = ∑ j, a i j • y j
hfa : ∀ (j : Fin l), ∑ i, (fun i ↦ f ↑i) i * a i j = 0
this : v n✝ ∉ 𝔪 • ⊤
n : ↥(insert n✝ s) := ⟨n✝, ⋯⟩
n_def : n = ⟨n✝, ⋯⟩
j : Fin l
hj : IsUnit (a n j)
a' : ι → R := fun i ↦ if hi : i ∈ insert n✝ s then a ⟨i, hi⟩ j else 0
a_eq : ∀ (i : ↥(insert n✝ s)), a i j = a' ↑i
⊢ f ↑n * a' ↑n + ∑ i ∈ s, f i * a' i = f n✝ * a' n✝ + ∑ i ∈ s, f i * a' i

Tactic:
n_def

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

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (r • (tprod R) f)
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
⊢ motive z

Tactic:
simp_rw [← tprodCoeff_eq_smul_tprod] at smul_tprod

Goal state after:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
motive : (⨂[R] (i : ι), s i) → Prop
z : ⨂[R] (i : ι), s i
add : ∀ (x y : ⨂[R] (i : ι), s i), motive x → motive y → motive (x + y)
smul_tprod : ∀ (r : R) (f : (i : ι) → s i), motive (tprodCoeff R r f)
⊢ motive z
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁶ : CommSemiring R
s : ι → Type u_7
inst✝⁵ : (i : ι) → AddCommMonoid (s i)
inst✝⁴ : (i : ι) → Module R (s i)
t : ι → Type u_11
t' : ι → Type u_12
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
inst✝¹ : (i : ι) → AddCommMonoid (t' i)
inst✝ : (i : ι) → Module R (t' i)
r : R
φ : ⨂[R] (i : ι), s i →ₗ[R] t i →ₗ[R] t' i
x✝¹ : (i : ι) → s i
x✝ : (i : ι) → t i
⊢ ((((lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) (r • φ)))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝ =
    ((((r • lift (piTensorHomMap.compMultilinearMap ((lift (piLinearMap (tprod R))) φ))).compMultilinearMap (tprod R))
            x✝¹).compMultilinearMap
        (tprod R))
      x✝

Tactic:
simp only [map_smul, LinearMap.compMultilinearMap_apply,
    lift.tprod, smul_apply, LinearMap.smul_apply]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ ClassGroup.mk0 (⟨I, ⋯⟩ ^ n) = 1

Tactic:
SubmonoidClass.mk_pow

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI0 : ¬I = 0
hI : ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
⊢ ClassGroup.mk0 ⟨I ^ n, ⋯⟩ = 1
Module: Mathlib.RingTheory.LocalRing.ResidueField.Fiber

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        (r •
          (IsLocalRing.residue (Localization.AtPrime p))
            ((fun x ↦
                match x with
                | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p))
        ((fun x ↦
            match x with
            | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ includeRight ((algebraMap R p.ResidueField) (r * y)) * x = a ⊗ₜ[R] (y • 1)

Tactic:
← Algebra.algebraMap_eq_smul_one,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
inst✝ : p.IsPrime
x : S ⊗[R] p.ResidueField
r : R
a : S
y : R
t : ↥p.primeCompl
e :
  1 ⊗ₜ[R]
        (r •
          (IsLocalRing.residue (Localization.AtPrime p))
            ((fun x ↦
                match x with
                | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
              (y, t))) *
      x =
    a ⊗ₜ[R]
      (IsLocalRing.residue (Localization.AtPrime p))
        ((fun x ↦
            match x with
            | (r, m) => IsLocalization.mk' (Localization.AtPrime p) r m)
          (y, t))
hrt : r ∉ p ∧ y ∉ p
⊢ includeRight ((algebraMap R p.ResidueField) (r * y)) * x = a ⊗ₜ[R] (algebraMap R p.ResidueField) y