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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ Module.Finite S P.toExtension.H1Cotangent

Tactic:
Module.finite_def,

Goal state after:
R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this : FiniteType R P.toExtension.Ring
⊢ ⊤.FG
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this✝ : FiniteType R P.toExtension.Ring
this : Module.Finite S P.toExtension.Cotangent
⊢ P.toExtension.cotangentComplex.rangeRestrict.ker.FG

Tactic:
have : Module.FinitePresentation S (LinearMap.range P.toExtension.cotangentComplex) := by
    rw [← LinearMap.exact_iff.mp P.toExtension.exact_cotangentComplex_toKaehler]
    exact Module.finitePresentation_of_projective_of_exact
      _ _ (Subtype.val_injective) P.toExtension.toKaehler_surjective
      (LinearMap.exact_subtype_ker_map _)

Goal state after:
R : Type u
S : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Algebra R S
ι : Type w
ι' : Type u_1
P✝ : Generators R S ι
S' : Type u_2
inst✝⁹ : CommRing S'
inst✝⁸ : Algebra R S'
T : Type w
inst✝⁷ : CommRing T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra S T
inst✝⁴ : IsScalarTower R S T
inst✝³ : Algebra S' T
inst✝² : IsScalarTower R S' T
inst✝¹ : FinitePresentation R S
inst✝ : Projective S Ω[S⁄R]
P : Presentation R S (Fin (Presentation.ofFinitePresentationVars R S))
  (Fin (Presentation.ofFinitePresentationRels R S)) :=
  Presentation.ofFinitePresentation R S
this✝¹ : FiniteType R P.toExtension.Ring
this✝ : Module.Finite S P.toExtension.Cotangent
this : Module.FinitePresentation S ↥P.toExtension.cotangentComplex.range
⊢ P.toExtension.cotangentComplex.rangeRestrict.ker.FG
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
H : Module.support R M ⊆ PrimeSpectrum.zeroLocus {f}
m : M
h : ¬(R ∙ m).annihilator = ⊤
p : Ideal R
hp : (R ∙ m).annihilator ≤ p
hp' : p.IsPrime
⊢ f ∈ p

Tactic:
simpa using H (Module.mem_support_iff_exists_annihilator (p := ⟨p, hp'⟩).mpr ⟨_, hp⟩)

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

Goal state before:
pp: case h
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
R' : Type u_3
inst✝⁶ : CommSemiring R'
inst✝⁵ : Algebra R R'
N : Type u_5
inst✝⁴ : AddCommMonoid N
inst✝³ : Module R N
inst✝² : Module R' N
inst✝¹ : IsScalarTower R R' N
inst✝ : IsLocalization M R'
x : N
hs' : x ∈ Submodule.span R' ↑∅
⊢ 1 • x ∈ Submodule.span R ↑∅

Tactic:
simpa using hs'

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

Goal state before:
pp: R : Type u_3
S : Type u_4
Rₚ : Type u_1
Sₚ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : CommSemiring Rₚ
inst✝⁹ : CommSemiring Sₚ
inst✝⁸ : Algebra R S
inst✝⁷ : Algebra R Rₚ
inst✝⁶ : Algebra R Sₚ
inst✝⁵ : Algebra S Sₚ
inst✝⁴ : Algebra Rₚ Sₚ
inst✝³ : IsScalarTower R S Sₚ
inst✝² : IsScalarTower R Rₚ Sₚ
M : Submonoid R
inst✝¹ : IsLocalization M Rₚ
inst✝ : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₚ
hRS : Module.Finite R S
⊢ Module.Finite Rₚ Sₚ

Tactic:
have : algebraMap Rₚ Sₚ = IsLocalization.map (T := Algebra.algebraMapSubmonoid S M) Sₚ
      (algebraMap R S) (Submonoid.le_comap_map M) := by
    apply IsLocalization.ringHom_ext M
    simp only [IsLocalization.map_comp, ← IsScalarTower.algebraMap_eq]
  -- We claim that if `S` is generated by `T` as an `R`-module,
  -- then `S'` is generated by `T` as an `R'`-module.
  obtain ⟨T, hT⟩ := hRS
  use T.image (algebraMap S Sₚ)
  simpa using span_eq_top_localization_localization Rₚ M Sₚ hT

Goal state after:
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
I : Ideal R
p : PrimeSpectrum R
hp₁ : Nontrivial (LocalizedModule p.asIdeal.primeCompl M)
hp₂ : p ∈ zeroLocus ↑I
Rₚ : Type u_1 := Localization.AtPrime p.asIdeal
Mₚ : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl M
Mₚ' : Type (max u_1 u_2) := LocalizedModule p.asIdeal.primeCompl (M ⧸ I • ⊤)
Mₚ'' : Type (max u_1 u_2) := Mₚ ⧸ Ideal.map (algebraMap R Rₚ) I • ⊤
e : Mₚ' ≃ₗ[Rₚ] Mₚ'' :=
  (localizedQuotientEquiv p.asIdeal.primeCompl (I • ⊤)).symm ≪≫ₗ
    (Submodule.localized p.asIdeal.primeCompl (I • ⊤)).quotEquivOfEq (Ideal.map (algebraMap R Rₚ) I • ⊤) ⋯
this : Nontrivial Mₚ''
⊢ Nontrivial Mₚ'

Tactic:
exact e.nontrivial

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

Goal state before:
pp: R : Type u
inst✝¹⁰ : CommSemiring R
M : Type v
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
N : Submodule R M
R' : Type u_1
inst✝⁷ : CommSemiring R'
inst✝⁶ : Algebra R R'
M' : Type u_2
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : Module R M'
inst✝³ : Module R' M'
inst✝² : IsScalarTower R R' M'
S : Submonoid R
inst✝¹ : IsLocalization S R'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
s : Set M
hfin : s.Finite
hspan : span R s = N
⊢ span R' (⇑f '' s) = localized' R' S f N

Tactic:
by rw [← hspan, localized'_span]

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 [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ (-1) ^ (↑p + ↑p) • f (Matrix.vecCons x v) = f (Matrix.vecCons x v)

Tactic:
Even.neg_one_pow,

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 [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ 1 • f (Matrix.vecCons x v) = f (Matrix.vecCons x v)

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 [⋀^Fin (n + 1)]→ₗ[R] N
p : Fin (n + 1)
x : M
v : Fin n → M
⊢ Even (↑p + ↑p)
Module: Mathlib.LinearAlgebra.ExteriorPower.Basis

Goal state before:
pp: K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
⊢ LinearIndependent (ι := ↑(powersetCard I n)) K (ιMulti_family K n v)

Tactic:
suffices ∃ b : Basis I K W, v = W.subtype ∘ b by
    obtain ⟨b, hb⟩ := this
    rw [hb, ← map_comp_ιMulti_family]
    exact LinearIndependent.map' (coe_basis K n b ▸ (b.exteriorPower n).linearIndependent)
      _ (LinearMap.ker_eq_bot.mpr (map_injective_field (Submodule.subtype_injective _)))

Goal state after:
K : Type u_2
E : Type u_4
n : ℕ
inst✝³ : Field K
inst✝² : AddCommGroup E
inst✝¹ : Module K E
I : Type u_5
inst✝ : LinearOrder I
v : I → E
hv : LinearIndependent K v
W : Submodule K E := Submodule.span K (range v)
⊢ ∃ b, v = ⇑W.subtype ∘ ⇑b
Module: Mathlib.RingTheory.LocalRing.Module

Goal state before:
pp: R : Type u_1
inst✝¹² : CommRing R
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
N₂ : Type u_9
N₃ : Type u_10
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup M₂
inst✝⁸ : Module R M₂
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R M₃
inst✝⁵ : AddCommGroup N₁
inst✝⁴ : Module R N₁
inst✝³ : AddCommGroup N₂
inst✝² : Module R N₂
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hfexact : Exact ⇑f₁ ⇑f₂
hfsurj : Surjective ⇑f₂
hgexact : Exact ⇑g₁ ⇑g₂
hgsurj : Surjective ⇑g₂
hfinj : Function.Injective ⇑(LinearMap.rTensor N₃ f₁)
hginj : Function.Injective ⇑(LinearMap.lTensor M₂ g₁)
⊢ Function.Injective ⇑(LinearMap.lTensor M₃ g₁)

Tactic:
by
  rw [injective_iff_map_eq_zero]
  intro x hx
  obtain ⟨x, rfl⟩ := f₂.rTensor_surjective N₁ hfsurj x
  have : f₂.rTensor N₂ (g₁.lTensor M₂ x) = 0 := by
    rw [← hx, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
      LinearMap.lTensor_comp_rTensor]
  obtain ⟨y, hy⟩ := (rTensor_exact N₂ hfexact hfsurj _).mp this
  have : g₂.lTensor M₁ y = 0 := by
    apply hfinj
    trans g₂.lTensor M₂ (g₁.lTensor M₂ x)
    · rw [← hy, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.rTensor_comp_lTensor,
        LinearMap.lTensor_comp_rTensor]
    rw [← LinearMap.comp_apply, ← LinearMap.lTensor_comp, hgexact.linearMap_comp_eq_zero]
    simp
  obtain ⟨z, rfl⟩ := (lTensor_exact _ hgexact hgsurj _).mp this
  obtain rfl : f₁.rTensor N₁ z = x := by
    apply hginj
    simp only [← hy, ← LinearMap.comp_apply, ← LinearMap.comp_apply, LinearMap.lTensor_comp_rTensor,
      LinearMap.rTensor_comp_lTensor]
  rw [← LinearMap.comp_apply, ← LinearMap.rTensor_comp, hfexact.linearMap_comp_eq_zero]
  simp

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
inst✝⁵ : Monoid R₁
inst✝⁴ : DistribMulAction R₁ R
inst✝³ : SMulCommClass R₁ R R
inst✝² : Monoid R₂
inst✝¹ : DistribMulAction R₂ R
inst✝ : SMulCommClass R₂ R R
x z y : ⨂[R] (i : ι), s i
ihz : 1 • z = z
ihy : 1 • y = y
⊢ 1 • (z + y) = z + y

Tactic:
simp_rw [PiTensorProduct.smul_add, ihz, ihy]

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
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 z y : ⨂[R] (i : ι), s i
ihz : r' • r'' • z = r'' • r' • z
ihy : r' • r'' • y = r'' • r' • y
⊢ r' • r'' • (z + y) = r'' • r' • (z + y)

Tactic:
simp_rw [PiTensorProduct.smul_add, ihz, ihy]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ (mulLeftMap N m).ker = ⊥

Tactic:
refine LinearMap.ker_eq_bot_of_injective ?_

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥N
ι : Type u_1
m : ι → ↥M
hm : LinearIndependent R m
⊢ Function.Injective ⇑(mulLeftMap N m)
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✝¹ : SMul R₁ R₂
inst✝ : IsScalarTower R₁ R₂ R
r' : R₁
r'' : R₂
x z y : ⨂[R] (i : ι), s i
ihz : (r' • r'') • z = r' • r'' • z
ihy : (r' • r'') • y = r' • r'' • y
⊢ (r' • r'') • (z + y) = r' • r'' • (z + y)

Tactic:
simp_rw [PiTensorProduct.smul_add, ihz, ihy]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ (M.mulRightMap n).ker = ⊥

Tactic:
refine LinearMap.ker_eq_bot_of_injective ?_

Goal state after:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Flat R ↥M
ι : Type u_1
n : ι → ↥N
hn : LinearIndependent R n
⊢ Function.Injective ⇑(M.mulRightMap n)
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)
x y : ⨂[R] (i : ι), s i
p q : FreeAddMonoid (R × ((i : ι) → s i))
hp : p ∈ x.lifts
hq : q ∈ y.lifts
⊢ p + q ∈ (x + y).lifts

Tactic:
by
  simp only [lifts, Set.mem_ofPred_eq, AddCon.coe_add]
  rw [hp, hq]

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
φ : MultilinearMap R s E
⊢ (fun φ' ↦ φ'.compMultilinearMap (tprod R))
      ((fun φ ↦
          let __src := liftAux φ;
          { toFun := (↑__src).toFun, map_add' := ⋯, map_smul' := ⋯ })
        φ) =
    φ

Tactic:
ext
    simp [liftAux_tprod, LinearMap.compMultilinearMap]

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
⊢ I.minimalPrimes.Finite

Tactic:
by_contra hI

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
hR : IsNoetherianRing R
I : Ideal R
hI : ¬I.minimalPrimes.Finite
⊢ False
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
v : ι → M
h : LinearIndependent k (⇑((TensorProduct.mk R k M) 1) ∘ v)
⊢ LinearIndependent R v

Tactic:
by
  rw [linearIndependent_iff']; intro s f hfv i hi
  classical
  induction s using Finset.induction generalizing v i with
  | empty => exact (Finset.notMem_empty _ hi).elim
  | insert n s hn ih => ?_
  rw [← Finset.sum_coe_sort] at hfv
  have ⟨l, a, y, hay, hfa⟩ := Flat.isTrivialRelation_of_sum_smul_eq_zero hfv
  have : v n ∉ 𝔪 • (⊤ : Submodule R M) := by
    simpa only [← LinearMap.ker_tensorProductMk] using! h.ne_zero n
  set n : ↥(insert n s) := ⟨n, Finset.mem_insert_self ..⟩ with n_def
  obtain ⟨j, hj⟩ : ∃ j, IsUnit (a n j) := by
    contrapose! this
    rw [show v n = _ from hay n]
    exact sum_mem fun _ _ ↦ Submodule.smul_mem_smul (this _) ⟨⟩
  let a' (i : ι) : R := if hi : _ then a ⟨i, hi⟩ j else 0
  have a_eq i : a i j = a' i.1 := by simp_rw [a', dif_pos i.2]
  have hfn : f n = -(∑ i ∈ s, f i * a' i) * hj.unit⁻¹ := by
    rw [← hj.mul_left_inj, mul_assoc, hj.val_inv_mul, mul_one, eq_neg_iff_add_eq_zero]
    convert! hfa j
    simp_rw [a_eq, Finset.sum_coe_sort _ (fun i ↦ f i * a' i), s.sum_insert hn, n_def]
  let c (i : ι) : R := -(if i = n then 0 else a' i) * hj.unit⁻¹
  specialize ih (v + (c · • v n)) ?_ ?_
  · convert! (linearIndependent_add_smul_iff (c := Ideal.Quotient.mk _ ∘ c) (i := n.1) ?_).mpr h
    · ext; simp [tmul_add]; rfl
    simp_rw [Function.comp_def, c, if_pos, neg_zero, zero_mul, map_zero]
  · rw [Finset.sum_coe_sort _ (fun i ↦ f i • v i), s.sum_insert hn, add_comm, hfn] at hfv
    simp_rw [Pi.add_apply, smul_add, s.sum_add_distrib, c, smul_smul, ← s.sum_smul, ← mul_assoc,
      ← s.sum_mul, mul_neg, s.sum_neg_distrib, ← hfv]
    congr 4
    exact s.sum_congr rfl fun i hi ↦ by rw [if_neg (ne_of_mem_of_not_mem hi hn)]
  obtain hi | hi := Finset.mem_insert.mp hi
  · rw [hi, hfn, Finset.sum_eq_zero, neg_zero, zero_mul]
    intro i hi; rw [ih i hi, zero_mul]
  · exact ih i hi

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✝ : Subsingleton ι
i₀ : ι
f : (i : ι) → s i
h : update 0 i₀ (f i₀) = f
⊢ (({ toFun := fun x ↦ (tprod R) (update 0 i₀ x), map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
            lift { toFun := fun f ↦ f i₀, map_update_add' := ⋯, map_update_smul' := ⋯ }).compMultilinearMap
        (tprod R))
      f =
    (LinearMap.id.compMultilinearMap (tprod R)) f

Tactic:
simp [h]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this✝ : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
g : R := T.gcd id
hK' : K' ≤ span {g}
y : R
hyJ : y ∈ J
hJK : J * K = R ∙ y * g
hxmemJK : y * g ∈ J * K
hxT : y * g ∈ J * K'
hxJg : y * g ∈ J * span {g}
hx0 : y * g ≠ 0
this : J = span {y}
⊢ Submodule.IsPrincipal J

Tactic:
exact ⟨y, this⟩

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

Goal state before:
pp: A : Type u
inst✝² : CommRing A
inst✝¹ : IsNoetherianRing A
inst✝ : IsFractionRing A A
I : Ideal A
hI : I.IsMaximal
fin : (associatedPrimes A A).Finite
⊢ ↑I ⊆ ⋃ i ∈ associatedPrimes A A, ↑i

Tactic:
biUnion_associatedPrimes_eq_compl_nonZeroDivisors

Goal state after:
A : Type u
inst✝² : CommRing A
inst✝¹ : IsNoetherianRing A
inst✝ : IsFractionRing A A
I : Ideal A
hI : I.IsMaximal
fin : (associatedPrimes A A).Finite
⊢ ↑I ⊆ (↑(nonZeroDivisors A))ᶜ
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)
x : A
hP : I ≤ ⊥.colon {x}
prime : (⊥.colon {x}).IsPrime
h : x = 0
⊢ ⊥.colon {x} = ⊤

Tactic:
simp [h]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: case refine_1
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
g : T →+* S ⊗[R] T := ⋯
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∈ ↑x.asIdeal

Tactic:
Algebra.TensorProduct.tmul_mul_tmul,

Goal state after:
case refine_1
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
x : PrimeSpectrum (S ⊗[R] T)
hx₁ : a ⊗ₜ[R] 1 ∉ x.asIdeal
hx₂ : 1 ⊗ₜ[R] t ∉ x.asIdeal
hx₃ : f ∈ x.asIdeal
⊢ (a * 1) ⊗ₜ[R] (1 * t) ∈ ↑x.asIdeal
Module: Mathlib.RingTheory.Spectrum.Prime.TensorProduct

Goal state before:
pp: case refine_1
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ tensorProductTo R S T ⁻¹' (basicOpen a).carrier ×ˢ (basicOpen t).carrier ⊆ ↑(basicOpen f)

Tactic:
rintro x ⟨hx₁ : a ⊗ₜ[R] (1 : T) ∉ x.asIdeal, hx₂ : (1 : S) ⊗ₜ[R] t ∉ x.asIdeal⟩
      (hx₃ : f ∈ x.asIdeal)
    apply x.asIdeal.primeCompl.mul_mem hx₁ hx₂
    rw [Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← e]
    exact x.asIdeal.mul_mem_left _ hx₃

Goal state after:
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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ a ⊗ₜ[R] 1 * 1 ⊗ₜ[R] t ∉ J.asIdeal

Tactic:
Algebra.TensorProduct.tmul_mul_tmul,

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
g : T →+* S ⊗[R] T := Algebra.TensorProduct.includeRight.toRingHom
f : S ⊗[R] T
J : PrimeSpectrum (S ⊗[R] T)
hJ : f ∉ J.asIdeal
t : T
r : R
a : S
ht : r • t ∉ Ideal.comap g J.asIdeal
e : 1 ⊗ₜ[R] (r • t) * f = a ⊗ₜ[R] t
⊢ (a * 1) ⊗ₜ[R] (1 * t) ∉ J.asIdeal
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
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (mk K) ((FractionalIdeal.mk0 K) I) = (mk (FractionRing R)) ((FractionalIdeal.mk0 (FractionRing R)) I)

Tactic:
← ClassGroup.mk_canonicalEquiv K (FractionRing R),

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
inst✝ : IsDedekindDomain R
I : ↥(Ideal R)⁰
⊢ (mk (FractionRing R)) ((Units.map ↑(canonicalEquiv R⁰ K (FractionRing R))) ((FractionalIdeal.mk0 K) I)) =
    (mk (FractionRing R)) ((FractionalIdeal.mk0 (FractionRing R)) I)