mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ (↑s).Pairwise (Function.onFun IsCoprime fun i ↦ (f i).asIdeal ^ e i)

Tactic:
intro i hi j hj hij

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
e : ι → ℕ
f : ι → HeightOneSpectrum R
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ Function.onFun IsCoprime (fun i ↦ (f i).asIdeal ^ e i) i j
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
⊢ (↑s).Pairwise (Function.onFun IsCoprime fun i ↦ f i ^ e i)

Tactic:
intro i hi j hj hij

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
ι : Type u_4
inst✝ : IsDedekindDomain R
s : Finset ι
f : ι → Ideal R
e : ι → ℕ
prime : ∀ i ∈ s, Prime (f i)
coprime : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
⊢ Function.onFun IsCoprime (fun i ↦ f i ^ e i) i j
Module: Mathlib.Algebra.Module.Presentation.Cokernel

Goal state before:
pp: A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ Submodule.map f ⊤ ≤ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }).ker

Tactic:
← hg₁,

Goal state after:
A : Type u
inst✝⁸ : Ring A
M₁ : Type v₁
M₂ : Type v₂
M₃ : Type v₃
inst✝⁷ : AddCommGroup M₁
inst✝⁶ : Module A M₁
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module A M₂
inst✝³ : AddCommGroup M₃
inst✝² : Module A M₃
pres₂ : Presentation A M₂
f : M₁ →ₗ[A] M₂
ι : Type w₁
g₁ : ι → M₁
data : pres₂.CokernelData f g₁
hg₁ : Submodule.span A (Set.range g₁) = ⊤
N✝ : Type w
inst✝¹ : AddCommGroup N✝
inst✝ : Module A N✝
s : (pres₂.cokernelRelations data).Solution N✝
⊢ Submodule.map f (Submodule.span A (Set.range g₁)) ≤ (⋯.desc { var := s.var, linearCombination_var_relation := ⋯ }).ker
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: case h.succ.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R (⇑(R ∙ s j).mkQ '' Set.range s) = (R ∙ s j).mkQ.range
⊢ Submodule.span R (Set.range s') = ⊤

Tactic:
range_mkQ

Goal state after:
case h.succ.refine_2
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsPrincipalIdealRing R
inst✝² : IsDomain R
p : R
hp : Irreducible p
d : ℕ
IH :
  ∀ {M : Type v} [inst : AddCommGroup M] [inst_1 : Module R M],
    IsTorsion' M ↥(Submonoid.powers p) →
      ∀ (s : Fin d → M), Submodule.span R (Set.range s) = ⊤ → ∃ k, Nonempty (M ≃ₗ[R] ⨁ (i : Fin d), R ⧸ R ∙ p ^ k i)
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
hM : IsTorsion' M ↥(Submonoid.powers p)
s : Fin (d + 1) → M
hs : Submodule.span R (Set.range s) = ⊤
this : (x : M) → Decidable (x = 0)
j : Fin d.succ
hj : IsTorsionBy R M (p ^ pOrder hM (s j))
s' : Fin d → M ⧸ R ∙ s j := Submodule.Quotient.mk ∘ s ∘ j.succAbove
hs' : Submodule.span R (⇑(R ∙ s j).mkQ '' Set.range s) = ⊤
⊢ Submodule.span R (Set.range s') = ⊤
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case pos
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : ¬Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
w_minus : ¬Weight.toLinear K (↥H) L χ - Weight.toLinear K (↥H) L α = 0
w_chi : Weight.toLinear K (↥H) L χ = 0
⊢ ⁅x_χ, m_α⁆ ∈ ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
have hx_χ_in_H : x_χ ∈ H.toLieSubmodule := by
      rw [← rootSpace_zero_eq K L H]
      convert! hx_χ; ext h; simp only [Pi.zero_apply]
      have h_apply : (χ.toLinear : H → K) h = 0 := by rw [w_chi, LinearMap.zero_apply]
      exact h_apply.symm
    apply LieSubmodule.mem_iSup_of_mem ⟨α, hαq, hα₀⟩
    rw [← (by rfl : ⁅(⟨x_χ, hx_χ_in_H⟩ : H), m_α⁆ = ⁅x_χ, m_α⁆)]
    exact (sl2SubmoduleOfRoot hα₀).lie_mem hm_α_original

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: case mem.add
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
x m : L
χ : Weight K (↥H) L
x_χ : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
m₁ m₂ : L
hx✝ : m₁ ∈ ⨆ i, sl2SubmoduleOfRoot ⋯
hy✝ : m₂ ∈ ⨆ i, sl2SubmoduleOfRoot ⋯
ih₁ : ⁅x_χ, m₁⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
ih₂ : ⁅x_χ, m₂⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
⊢ ⁅x_χ, m₁ + m₂⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier

Tactic:
simp only [lie_add, Submodule.carrier_eq_coe, SetLike.mem_coe] at ih₁ ih₂ ⊢
        exact add_mem ih₁ ih₂

Goal state after:
Module: Mathlib.Algebra.Lie.Weights.IsSimple

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
q : Submodule K (Dual K ↥H)
hq : ∀ (i : ↥LieSubalgebra.root), q ∈ End.invtSubmodule ↑((rootSystem H).reflection i)
⊢ LieSubmodule.restr (invtSubmoduleToLieIdeal q hq) H = ⨆ α, sl2SubmoduleOfRoot ⋯

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.restr_toSubmodule,
    coe_invtSubmoduleToLieIdeal_eq_iSup, LieSubmodule.iSup_toSubmodule]

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' : x ∈ Ideal.span (Set.range (⇑((↑e).comp ↑TensorProduct.includeRight) ∘ P.relation))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))

Tactic:
RingHom.coe_comp,

Goal state after:
case a
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type u_1
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Presentation R S ι σ
x : MvPolynomial ι T
hx : (aeval (Generators.baseChange T P.toGenerators).val) x = 0
H :
  RingHom.ker (TensorProduct.map (AlgHom.id R T) (IsScalarTower.toAlgHom R P.Ring S)) =
    Ideal.map TensorProduct.includeRight (RingHom.ker (IsScalarTower.toAlgHom R P.Ring S))
e : T ⊗[R] MvPolynomial ι R ≃ₐ[T] MvPolynomial ι T := algebraTensorAlgEquiv R T
H' : x ∈ Ideal.span (Set.range ((⇑↑e ∘ ⇑↑TensorProduct.includeRight) ∘ P.relation))
⊢ x ∈ Ideal.span (Set.range fun i ↦ (MvPolynomial.map (algebraMap R T)) (P.relation i))
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1.refine_1
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' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
r : P.Ring
hr : r ∈ P.ker
s : P.Ring
hs : s ∈ P.ker
⊢ 1 ⊗ₜ[P.Ring] ⟨r • s, ⋯⟩ = 0

Tactic:
trans (r • 1) ⊗ₜ[P.Ring] ⟨s, hs⟩

Goal state after:
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' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
r : P.Ring
hr : r ∈ P.ker
s : P.Ring
hs : s ∈ P.ker
⊢ 1 ⊗ₜ[P.Ring] ⟨r • s, ⋯⟩ = (r • 1) ⊗ₜ[P.Ring] ⟨s, hs⟩

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' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
r : P.Ring
hr : r ∈ P.ker
s : P.Ring
hs : s ∈ P.ker
⊢ (r • 1) ⊗ₜ[P.Ring] ⟨s, hs⟩ = 0
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1.refine_2
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' S''
inst✝¹⁰ : Algebra S S'
inst✝⁹ : Algebra S' S''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S'
inst✝⁶ : IsScalarTower R R' S'
inst✝⁵ : Algebra R R''
inst✝⁴ : IsScalarTower R R' R''
inst✝³ : IsScalarTower R' R'' S''
inst✝² : Algebra R S''
inst✝¹ : IsScalarTower R R'' S''
inst✝ : IsScalarTower S S' S''
x : ↥P.ker
hx : ↑x ∈ P.ker * P.ker
⊢ ∀ (x : P.Ring) (hx : x ∈ P.ker • P.ker) (y : P.Ring) (hy : y ∈ P.ker • P.ker),
    1 ⊗ₜ[P.Ring] ⟨x, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨y, ⋯⟩ = 0 → 1 ⊗ₜ[P.Ring] ⟨x + y, ⋯⟩ = 0

Tactic:
intro a ha b hb ha' hb'
      convert! congr($ha' + $hb')
      rw [← tmul_add]
      rfl

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : (R ∙ m).annihilator = ⊤
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
rw [Submodule.annihilator_eq_top_iff, Submodule.span_singleton_eq_bot] at h

Goal state after:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : m = 0
⊢ ∃ r ∈ Submonoid.powers f, r • m = 0
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
⊢ Module.support R M ⊆ PrimeSpectrum.zeroLocus {f} → ∀ (m : M), ∃ r ∈ Submonoid.powers f, r • m = 0

Tactic:
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.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
n : ℕ
f : M →ₗ[R] M →ₗ[R] M [⋀^Fin n]→ₗ[R] N
v : Fin (n + 2) → M
i j : Fin (n + 1)
hj : i ≤ j
⊢ (-1) ^ ↑i • (-1) ^ ↑j • ((f (v i.castSucc)) (i.castSucc.removeNth v j)) (j.removeNth (i.castSucc.removeNth v)) +
      (-1) ^ (↑j + 1) • (-1) ^ ↑i • ((f (v j.succ)) (j.succ.removeNth v i)) (i.removeNth (j.succ.removeNth v)) =
    (-1) ^ (↑i + ↑j) •
      (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
        ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))

Tactic:
have H₁ : i.castSucc.removeNth v j = v j.succ := by
    simp [Fin.removeNth_apply, Fin.succAbove_of_le_castSucc, hj]

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
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
⊢ (-1) ^ ↑i • (-1) ^ ↑j • ((f (v i.castSucc)) (i.castSucc.removeNth v j)) (j.removeNth (i.castSucc.removeNth v)) +
      (-1) ^ (↑j + 1) • (-1) ^ ↑i • ((f (v j.succ)) (j.succ.removeNth v i)) (i.removeNth (j.succ.removeNth v)) =
    (-1) ^ (↑i + ↑j) •
      (((f (v i.castSucc)) (v j.succ)) (j.removeNth (i.castSucc.removeNth v)) -
        ((f (v j.succ)) (v i.castSucc)) (j.removeNth (i.castSucc.removeNth v)))
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: case insert
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
⊢ f i = 0

Tactic:
have a_eq i : a i j = a' i.1 := by simp_rw [a', dif_pos i.2]

Goal state after:
case insert
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 i = 0
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)
E : Type u_9
inst✝¹ : AddCommMonoid E
inst✝ : Module R E
φ : MultilinearMap R s E
r : R
x : ⨂[R] (i : ι), s i
⊢ (liftAux φ) (r • x) = r • (liftAux φ) x

Tactic:
refine PiTensorProduct.induction_on' x ?_ ?_
  · intro z f
    rw [smul_tprodCoeff' r z f, liftAux_tprodCoeff, liftAux_tprodCoeff, smul_assoc]
  · intro z y ihz ihy
    rw [smul_add, (liftAux φ).map_add, ihz, ihy, (liftAux φ).map_add, smul_add]

Goal state after:
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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) x) = x

Tactic:
refine x.induction_on ?_ ?_

Goal state after:
case refine_1
ι : 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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ ∀ (r : R) (f : (i : ι) → s i),
    (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (r • (tprod R) f)) = r • (tprod R) f

case refine_2
ι : 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
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
inst✝ : IsEmpty ι
x : ⨂[R] (i : ι), s i
⊢ ∀ (x y : ⨂[R] (i : ι), s i),
    (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) x) = x →
      (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) y) = y →
        (fun r ↦ r • (tprod R) isEmptyElim) ((lift (constOfIsEmpty R s 1)) (x + y)) = x + y
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommSemiring R
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : IsNoetherianRing R
x : M
h : (⊥.colon {x}).IsPrime
r : R
h' : r ∈ ↑(⊥.colon {x})
⊢ r ∈ {r | ∃ x, x ≠ 0 ∧ r • x = 0}

Tactic:
exact ⟨x, by simpa using h.ne_top, by simpa using h'⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝⁴ : CommRing A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : IsNoetherianRing A
inst✝ : Module.Finite A M
N : Submodule A M
hN : N ≠ ⊤
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs₁ : s.head = ⊥
hs₂ : s.last = N
this : Nontrivial (M ⧸ N)
p : Ideal A
hp : p ∈ associatedPrimes A (M ⧸ N)
⊢ ∃ M_1 > N, ∃ s, s.head = ⊥ ∧ s.last = M_1

Tactic:
AssociatedPrimes.mem_iff,

Goal state after:
A : Type u
inst✝⁴ : CommRing A
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module A M
inst✝¹ : IsNoetherianRing A
inst✝ : Module.Finite A M
N : Submodule A M
hN : N ≠ ⊤
s : RelSeries {(N₁, N₂) | N₁.IsQuotientEquivQuotientPrime N₂}
hs₁ : s.head = ⊥
hs₂ : s.last = N
this : Nontrivial (M ⧸ N)
p : Ideal A
hp : IsAssociatedPrime p (M ⧸ N)
⊢ ∃ M_1 > N, ∃ s, s.head = ⊥ ∧ s.last = M_1
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
⊢ Subgroup.map (↑unitsMulEquivSubmodule) (Subgroup.map (toPrincipalIdeal R (FractionRing R)) ⊤) =
    Subgroup.map (Units.map ↑(Submodule.spanSingleton R)) ⊤

Tactic:
Subgroup.map_map

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
⊢ Subgroup.map ((↑unitsMulEquivSubmodule).comp (toPrincipalIdeal R (FractionRing R))) ⊤ =
    Subgroup.map (Units.map ↑(Submodule.spanSingleton R)) ⊤
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness

Goal state before:
pp: A : Type u
inst✝¹ : CommRing A
inst✝ : IsNoetherianRing A
I : Ideal A
h✝ : Disjoint ↑I ↑(nonZeroDivisors A)
P : Ideal A
h : P ∈ associatedPrimes A A
hP : I ≤ P
⊢ ⊥ < Module.annihilator A ↥I

Tactic:
AssociatedPrimes.mem_iff,

Goal state after:
A : Type u
inst✝¹ : CommRing A
inst✝ : IsNoetherianRing A
I : Ideal A
h✝ : Disjoint ↑I ↑(nonZeroDivisors A)
P : Ideal A
h : IsAssociatedPrime P A
hP : I ≤ P
⊢ ⊥ < Module.annihilator A ↥I
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
⊢ False

Tactic:
obtain ⟨t, r, a, ht, e⟩ := hRT.exists_mul_eq_tmul x
    (p₂.asIdeal.comap g) inferInstance

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : CommRing T
inst✝ : Algebra R T
hRT : (algebraMap R T).SurjectiveOnStalks
p₁ p₂ : PrimeSpectrum (S ⊗[R] T)
h : tensorProductTo R S T p₁ = tensorProductTo R S T p₂
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
x : S ⊗[R] T
hxp₁ : x ∈ p₁.asIdeal
hxp₂ : x ∉ p₂.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g p₂.asIdeal
e : 1 ⊗ₜ[R] (r • t) * x = a ⊗ₜ[R] t
⊢ False