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

Goal state before:
pp: case a.convert_4
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
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ j ∈ Finset.map e.toEmbedding (support x) with j.1 = i, (monomial j.2) (coeff (e.symm j) x) ∈ P.ker

Tactic:
simp only [ker_eq_ker_aeval_val, AddEquiv.toEquiv_eq_coe, RingHom.mem_ker, map_sum]

Goal state after:
case a.convert_4
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
h₂ : (Q.ofComp P).toAlgHom x = 0
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
hi : i ∈ Finset.image Prod.fst (Finset.map (↑e).toEmbedding (support x))
⊢ ∑ x_1 ∈ Finset.map (↑e).toEmbedding (support x) with x_1.1 = i,
      (aeval P.val) ((monomial x_1.2) (coeff (e.symm x_1) x)) =
    0
Module: Mathlib.Algebra.Module.Presentation.Tensor

Goal state before:
pp: case inr
A : Type u
inst✝⁴ : CommRing A
M₁ : Type v₁
M₂ : Type v₂
inst✝³ : AddCommGroup M₁
inst✝² : AddCommGroup M₂
inst✝¹ : Module A M₁
inst✝ : Module A M₂
relations₁ : Relations A
relations₂ : Relations A
solution₁ : relations₁.Solution M₁
solution₂ : relations₂.Solution M₂
g₁ : relations₁.G
r₂ : relations₂.R
⊢ (Finsupp.linearCombination A fun x ↦
        match x with
        | (g₁, g₂) => solution₁.var g₁ ⊗ₜ[A] solution₂.var g₂)
      ((relations₁.tensor relations₂).relation (Sum.inr (g₁, r₂))) =
    0

Tactic:
· dsimp
      rw [Finsupp.linearCombination_embDomain]
      exact (solution₂.postcomp (curry .id (solution₁.var g₁))).linearCombination_var_relation r₂

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case e'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
x' : S
hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx'' : (algebraMap S S') x' = (Algebra.linearMap S S') (y' • x)
a : R
ha₁ : a ∈ ↑M
ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
⊢ (⟨a, ha₁⟩ * ⟨y', hy'⟩) • x = (algebraMap R S) a * y' • x

Tactic:
Submonoid.smul_def,

Goal state after:
case e'_2
R : Type u_1
S : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
M : Submonoid R
S' : Type u_4
inst✝⁵ : CommSemiring S'
inst✝⁴ : Algebra S S'
inst✝³ : Algebra R S
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsLocalization (Submonoid.map (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), g x = (algebraMap S S') x
y : ↥(Submonoid.map (algebraMap R S) M) := commonDenomOfFinset (Submonoid.map (algebraMap R S) M) s
y' : R
hy' : y' ∈ ↑M
e : (algebraMap R S) y' = ↑y
this : (algebraMap R S) y' • ↑s = y' • ↑s
hx₁ : y' • Submodule.span R ↑s = Submodule.span R (⇑g '' ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
x' : S
hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s))
hx'' : (algebraMap S S') x' = (Algebra.linearMap S S') (y' • x)
a : R
ha₁ : a ∈ ↑M
ha₂ : ↑⟨(algebraMap R S) a, ⋯⟩ * x' = ↑⟨(algebraMap R S) a, ⋯⟩ * y' • x
⊢ ↑(⟨a, ha₁⟩ * ⟨y', hy'⟩) • x = (algebraMap R S) a * y' • x
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
f : R
⊢ Subsingleton (LocalizedModule.Away f M) ↔ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}

Tactic:
rw [LocalizedModule.subsingleton_iff]
  constructor
  · rintro H x hx' f rfl
    obtain ⟨m, hm⟩ := Module.mem_support_iff_exists_annihilator.mp hx'
    obtain ⟨_, ⟨n, rfl⟩, e⟩ := H m
    exact Ideal.IsPrime.mem_of_pow_mem inferInstance n
      (hm ((Submodule.mem_annihilator_span_singleton _ _).mpr e))
  · intro H m
    by_cases h : (Submodule.span R {m}).annihilator = ⊤
    · rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h
      exact ⟨1, one_mem _, by simpa using h⟩
    obtain ⟨n, hn⟩ : f ∈ (Submodule.span R {m}).annihilator.radical := by
      rw [Ideal.radical_eq_sInf, Ideal.mem_sInf]
      rintro p ⟨hp, hp'⟩
      simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)
    exact ⟨_, ⟨n, rfl⟩, (Submodule.mem_annihilator_span_singleton _ _).mp hn⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: R : Type u
inst✝¹¹ : CommSemiring R
S : Submonoid R
Rₚ : Type v
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization S Rₚ
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
Mₚ : Type t
inst✝⁵ : AddCommMonoid Mₚ
inst✝⁴ : Module R Mₚ
inst✝³ : Module Rₚ Mₚ
inst✝² : IsScalarTower R Rₚ Mₚ
f : M →ₗ[R] Mₚ
inst✝¹ : IsLocalizedModule S f
inst✝ : Module.Finite R M
⊢ Module.Finite Rₚ Mₚ

Tactic:
obtain ⟨T, hT⟩ := ‹Module.Finite R M›

Goal state after:
R : Type u
inst✝¹¹ : CommSemiring R
S : Submonoid R
Rₚ : Type v
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : Algebra R Rₚ
inst✝⁸ : IsLocalization S Rₚ
M : Type w
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
Mₚ : Type t
inst✝⁵ : AddCommMonoid Mₚ
inst✝⁴ : Module R Mₚ
inst✝³ : Module Rₚ Mₚ
inst✝² : IsScalarTower R Rₚ Mₚ
f : M →ₗ[R] Mₚ
inst✝¹ : IsLocalizedModule S f
inst✝ : Module.Finite R M
T : Finset M
hT : Submodule.span R ↑T = ⊤
⊢ Module.Finite Rₚ Mₚ
Module: Mathlib.RingTheory.Flat.EquationalCriterion

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
inst✝⁷ : Flat R M
K : Type u_3
N : Type u_4
inst✝⁶ : AddCommGroup K
inst✝⁵ : Module R K
inst✝⁴ : Module.Finite R K
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Free R N
inst✝ : Module.Finite R N
f : K →ₗ[R] N
x : N →ₗ[R] M
h : x ∘ₗ f = 0
e : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) ≃ₗ[R] N
k : ℕ
a : (Fin (Fintype.card (Free.ChooseBasisIndex R N)) →₀ R) →ₗ[R] Fin k →₀ R
y : (Fin k →₀ R) →ₗ[R] M
hya : x ∘ₗ ↑e = y ∘ₗ a
haf : a ∘ₗ ↑e.symm ∘ₗ f = 0
⊢ (a ∘ₗ ↑e.symm) ∘ₗ f = 0

Tactic:
by
    rwa [comp_assoc]

Goal state after:
Module: Mathlib.RingTheory.Localization.Finiteness

Goal state before:
pp: case h
R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤
sf : ↥t → Finset M := fun x ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)
x : M
r : ↑↑t
S : Submonoid R := Submonoid.powers ↑r
n₁ : ℕ
hn₁ : ⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ • IsLocalizedModule.mk' (f r) x 1 ∈ Submodule.span R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)

Tactic:
Submonoid.smul_def,

Goal state after:
case h
R : Type u
inst✝¹⁰ : CommSemiring R
M : Type w
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
t : Finset R
ht : Ideal.span ↑t = ⊤
Mₚ : ↥t → Type u_1
inst✝⁷ : (g : ↥t) → AddCommMonoid (Mₚ g)
inst✝⁶ : (g : ↥t) → Module R (Mₚ g)
Rₚ : ↥t → Type u_2
inst✝⁵ : (g : ↥t) → CommSemiring (Rₚ g)
inst✝⁴ : (g : ↥t) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↥t), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↥t) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↥t), IsScalarTower R (Rₚ g) (Mₚ g)
f : (g : ↥t) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↥t), IsLocalizedModule.Away (↑g) (f g)
H : ∀ (g : ↥t), Module.Finite (Rₚ g) (Mₚ g)
s₁ : (g : ↥t) → Finset (Mₚ g)
s₂ : ∀ (g : ↥t), Submodule.span (Rₚ g) ↑(s₁ g) = ⊤
sf : ↥t → Finset M := fun x ↦ IsLocalizedModule.finsetIntegerMultiple (Submonoid.powers ↑x) (f x) (s₁ x)
x : M
r : ↑↑t
S : Submonoid R := Submonoid.powers ↑r
n₁ : ℕ
hn₁ : ↑⟨(fun x ↦ ↑r ^ x) n₁, ⋯⟩ • IsLocalizedModule.mk' (f r) x 1 ∈ Submodule.span R ↑(s₁ r)
⊢ ∃ n, ↑r ^ n • x ∈ ⨆ x, Submodule.span R ↑(sf x)
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m✝ : (i : ι₁ ⊕ ι₂) → N i
val✝ : ι₁
x✝ y✝ : N (Sum.inl val✝)
⊢ ((a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inr i₂)) =
    ((a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) x✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) x✝ (Sum.inr i₂)) +
      (a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) y✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) y✝ (Sum.inr i₂)

Tactic:
let := Classical.decEq ι₁

Goal state after:
case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m✝ : (i : ι₁ ⊕ ι₂) → N i
val✝ : ι₁
x✝ y✝ : N (Sum.inl val✝)
this : DecidableEq ι₁ := Classical.decEq ι₁
⊢ ((a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inl i₁)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) (x✝ + y✝) (Sum.inr i₂)) =
    ((a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) x✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) x✝ (Sum.inr i₂)) +
      (a fun i₁ ↦ Function.update m✝ (Sum.inl val✝) y✝ (Sum.inl i₁)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m✝ (Sum.inl val✝) y✝ (Sum.inr i₂)
Module: Mathlib.LinearAlgebra.Alternating.Uncurry.Fin

Goal state before:
pp: 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
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ (-1) ^ (↑(j.succAbove i) + ↑(i.predAbove j)) • (-1) ^ ↑i • f (j.removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0

pp: 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
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i

Tactic:
neg_one_pow_succAbove_add_predAbove,

Goal state after:
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
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ -(-1) ^ (↑j + ↑i) • (-1) ^ ↑i • f (j.removeNth v) + (-1) ^ ↑j • f (j.removeNth v) = 0

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
m : ℕ
f : M [⋀^Fin (m + 1)]→ₗ[R] N
v : Fin (m + 1 + 1) → M
j : Fin (m + 1 + 1)
i : Fin (m + 1)
hvij : v (j.succAbove i) = v j
hij : j.succAbove i ≠ j
⊢ v j = j.removeNth v i
Module: Mathlib.LinearAlgebra.Multilinear.TensorProduct

Goal state before:
pp: case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₁ : ι₁
p : R
q : N (Sum.inl i₁)
⊢ ((a fun i₁_1 ↦ Function.update m (Sum.inl i₁) (p • q) (Sum.inl i₁_1)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m (Sum.inl i₁) (p • q) (Sum.inr i₂)) =
    p •
      (a fun i₁_1 ↦ Function.update m (Sum.inl i₁) q (Sum.inl i₁_1)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m (Sum.inl i₁) q (Sum.inr i₂)

Tactic:
let := Classical.decEq ι₁

Goal state after:
case inl
R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
ι₃ : Type u_4
ι₄ : Type u_5
inst✝⁷ : CommSemiring R
N₁ : Type u_6
inst✝⁶ : AddCommMonoid N₁
inst✝⁵ : Module R N₁
N₂ : Type u_7
inst✝⁴ : AddCommMonoid N₂
inst✝³ : Module R N₂
N : ι₁ ⊕ ι₂ → Type u_8
inst✝² : (i : ι₁ ⊕ ι₂) → AddCommMonoid (N i)
inst✝¹ : (i : ι₁ ⊕ ι₂) → Module R (N i)
a : MultilinearMap R (fun i₁ ↦ N (Sum.inl i₁)) N₁
b : MultilinearMap R (fun i₂ ↦ N (Sum.inr i₂)) N₂
inst✝ : DecidableEq (ι₁ ⊕ ι₂)
m : (i : ι₁ ⊕ ι₂) → N i
i₁ : ι₁
p : R
q : N (Sum.inl i₁)
this : DecidableEq ι₁ := Classical.decEq ι₁
⊢ ((a fun i₁_1 ↦ Function.update m (Sum.inl i₁) (p • q) (Sum.inl i₁_1)) ⊗ₜ[R]
      b fun i₂ ↦ Function.update m (Sum.inl i₁) (p • q) (Sum.inr i₂)) =
    p •
      (a fun i₁_1 ↦ Function.update m (Sum.inl i₁) q (Sum.inl i₁_1)) ⊗ₜ[R]
        b fun i₂ ↦ Function.update m (Sum.inl i₁) q (Sum.inr i₂)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ (Basis.exteriorPower n b).coord s = ιMultiDual R n b s

Tactic:
apply LinearMap.ext_on (ιMulti_family_span_of_span R (Basis.span_eq b))

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Type u_5
inst✝ : LinearOrder I
b : Basis I R M
s : ↑(powersetCard I n)
⊢ EqOn (⇑((Basis.exteriorPower n b).coord s)) (⇑(ιMultiDual R n b s)) (range (ιMulti_family R n ⇑b))
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
N : Submodule R S
y : R
n : ↥N
⊢ ↑(N.lTensorOne' ((algebraMap R ↥⊥) y ⊗ₜ[R] n)) = ↑(y • n)

Tactic:
simp_rw [lTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul, Algebra.smul_def]
  exact mulMap_tmul _ N _ _

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : ¬span {x} ≤ I
y : R
hy : ¬span {y} ≤ I
h : x * y ∈ I
⊢ False

Tactic:
← left_lt_sup

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
⊢ False
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Noetherian

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
⊢ False

Tactic:
refine hI (((hmax _ hx).union (hmax _ hy)).subset fun p ⟨⟨hp, hI⟩, hmin⟩ ↦ ?_)

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I✝ : Ideal R
hI✝¹ : ¬I✝.minimalPrimes.Finite
I : Ideal R
hI✝ : ¬I.minimalPrimes.Finite
hmax : ∀ (I_1 : Submodule R R), I < I_1 → (Ideal.minimalPrimes I_1).Finite
h1 : ¬I.IsPrime
h2 : I ≠ ⊤
x : R
hx : I < I ⊔ span {x}
y : R
hy : I < I ⊔ span {y}
h : x * y ∈ I
p : Ideal R
x✝ : p ∈ I.minimalPrimes
hp : p.IsPrime
hI : I ≤ p
hmin : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
⊢ p ∈ (I ⊔ span {x}).minimalPrimes ∪ (I ⊔ span {y}).minimalPrimes
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
ι₂ : Type u_2
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
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
e : ι ≃ ι₂
⊢ map f ∘ₗ ↑(reindex R s e).symm = ↑(reindex R t e).symm ∘ₗ map fun i ↦ f (e.symm i)

Tactic:
by
  ext m
  apply LinearEquiv.injective (reindex R t e)
  simp only [LinearMap.compMultilinearMap_apply, LinearMap.coe_comp, LinearEquiv.coe_coe,
    comp_apply, ← map_reindex, LinearEquiv.apply_symm_apply, map_tprod]

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

Goal state before:
pp: case insert.inl
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 : ∀ 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
hfn : f ↑n = (-∑ i ∈ s, f i * a' i) * ↑hj.unit⁻¹
c : ι → R := fun i ↦ (-if i = ↑n then 0 else a' i) * ↑hj.unit⁻¹
hi : i = n✝
⊢ f i = 0

Tactic:
rw [hi, hfn, Finset.sum_eq_zero, neg_zero, zero_mul]
    intro i hi; rw [ih i hi, zero_mul]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝² : Free R (N ⧸ l.range)
this✝¹ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this✝ : Module.Finite R ↥l.ker
H : Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
this : Subsingleton (k ⊗[R] ↥l.ker)
⊢ Subsingleton ↥l.ker

Tactic:
← IsLocalRing.subsingleton_tensorProduct (R := R)

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R M
inst✝⁴ : Module R N
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R M
inst✝¹ : Module.Finite R N
inst✝ : Free R N
l : M →ₗ[R] N
h : Function.Injective ⇑(LinearMap.lTensor k l)
this✝² : Free R (N ⧸ l.range)
this✝¹ : Projective R ↥l.range
l' : M →ₗ[R] ↥l.ker
hl' : l' ∘ₗ l.ker.subtype = LinearMap.id
this✝ : Module.Finite R ↥l.ker
H : Function.Injective ⇑(LinearMap.lTensor k l.ker.subtype)
this : Subsingleton (k ⊗[R] ↥l.ker)
⊢ Subsingleton (k ⊗[R] ↥l.ker)
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : IsAssociatedPrime P M
hx : ⊥.colon {x} ≤ P
⊢ r ∈ ⋃ p, ⋃ (_ : p.IsPrime ∧ ∃ x, p = ⊥.colon {x}), ↑p

Tactic:
rw [isAssociatedPrime_iff] at hP

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
r : R
x : M
h : x ≠ 0
h' : r • x = 0
P : Ideal R
hP : P.IsPrime ∧ ∃ x, P = ⊥.colon {x}
hx : ⊥.colon {x} ≤ P
⊢ r ∈ ⋃ p, ⋃ (_ : p.IsPrime ∧ ∃ x, p = ⊥.colon {x}), ↑p
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
x : R
hx : x ≠ 0
hI : ↑I = ↑(Ideal.span {x})
⊢ ∃ x_1 y, x_1 ≠ 0 ∧ y ≠ 0 ∧ Ideal.span {x_1} * Ideal.span {x} = Ideal.span {y} * ⊤

Tactic:
exact ⟨1, x, one_ne_zero, hx, by rw [Ideal.span_singleton_one, Ideal.top_mul, Ideal.mul_top]⟩

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

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
⊢ ClassGroup R ≃* (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range

Tactic:
haveI : Subgroup.map
    (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
    (toPrincipalIdeal R (FractionRing R)).range = (toPrincipalIdeal R K).range := by
    ext I
    simp only [Subgroup.mem_map, mem_principal_ideals_iff]
    constructor
    · rintro ⟨I, ⟨x, hx⟩, rfl⟩
      refine ⟨FractionRing.algEquiv R K x, ?_⟩
      simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]
      rfl
    · rintro ⟨x, hx⟩
      refine ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩
      · simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
          canonicalEquiv_spanSingleton]
        rfl
      · simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv,
          RingEquiv.coe_toMulEquiv, canonicalEquiv_canonicalEquiv, canonicalEquiv_self,
          RingEquiv.refl_apply]

Goal state after:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
this :
  Subgroup.map (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
      (toPrincipalIdeal R (FractionRing R)).range =
    (toPrincipalIdeal R K).range
⊢ ClassGroup R ≃* (FractionalIdeal R⁰ K)ˣ ⧸ (toPrincipalIdeal R K).range
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case ind.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
⊢ IsSolvable ↥H

Tactic:
obtain ⟨n, hn⟩ := hH ⁅H, H⁆ (h H h')

Goal state after:
case ind.inr
G : Type u_1
inst✝¹ : Group G
inst✝ : WellFoundedLT (Subgroup G)
h : ∀ (H : Subgroup G), H ≠ ⊥ → ⁅H, H⁆ < H
H : Subgroup G
hH : ∀ y < H, IsSolvable ↥y
h' : H ≠ ⊥
n : ℕ
hn : derivedSeries (↥⁅H, H⁆) n = ⊥
⊢ IsSolvable ↥H