mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
D : MvPolynomial σ R →ₗ[R] A
h₁ : D 1 = 0
⊢ (∀ (p q : MvPolynomial σ R), D (p * q) = p • D q + q • D p) ↔
    ∀ (s : σ →₀ ℕ) (i : σ), D ((monomial s) 1 * X i) = (monomial s) 1 • D (X i) + X i • D ((monomial s) 1)

Tactic:
by
  refine ⟨fun H p i => H _ _, fun H => ?_⟩
  have hC : ∀ r, D (C r) = 0 := by intro r; rw [C_eq_smul_one, D.map_smul, h₁, smul_zero]
  have : ∀ p i, D (p * X i) = p • D (X i) + (X i : MvPolynomial σ R) • D p := by
    intro p i
    induction p using MvPolynomial.induction_on' with
    | monomial s r =>
      rw [← mul_one r, ← C_mul_monomial, mul_assoc, C_mul', D.map_smul, H, C_mul', smul_assoc,
        smul_add, D.map_smul, smul_comm r (X i)]
    | add p q hp hq => rw [add_mul, map_add, map_add, hp, hq, add_smul, smul_add, add_add_add_comm]
  intro p q
  induction q using MvPolynomial.induction_on with
  | C c =>
    rw [mul_comm, C_mul', hC, smul_zero, zero_add, D.map_smul, C_eq_smul_one, smul_one_smul]
  | add q₁ q₂ h₁ h₂ => simp only [mul_add, map_add, h₁, h₂, smul_add, add_smul]; abel
  | mul_X q i hq =>
    simp only [this, ← mul_assoc, hq, mul_smul, smul_add, add_assoc]
    rw [smul_comm (X i), smul_comm (X i)]

Goal state after:
Module: Mathlib.Algebra.MvPolynomial.Derivation

Goal state before:
pp: σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ (s.sum fun i_1 k ↦ (monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) +
      (monomial (s + Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i =
    (monomial s) 1 • (monomial (Finsupp.single i 1 - Finsupp.single i 1)) ↑1 • f i +
      (monomial (Finsupp.single i 1)) 1 • s.sum fun i k ↦ (monomial (s - Finsupp.single i 1)) ↑k • f i

Tactic:
rw [tsub_self, add_tsub_cancel_right, Nat.cast_one, ← C_apply, C_1, one_smul, add_comm,
        Finsupp.smul_sum]

Goal state after:
σ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : Module R A
inst✝¹ : Module (MvPolynomial σ R) A
inst✝ : IsScalarTower R (MvPolynomial σ R) A
f : σ → A
s : σ →₀ ℕ
i : σ
⊢ ((monomial s) 1 • f i + s.sum fun i_1 k ↦ (monomial (s + Finsupp.single i 1 - Finsupp.single i_1 1)) ↑k • f i_1) =
    (monomial s) 1 • f i +
      s.sum fun a b ↦ (monomial (Finsupp.single i 1)) 1 • (monomial (s - Finsupp.single a 1)) ↑b • f a
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ X i * (pderiv i) ((monomial m) r) = m i • (monomial m) r

Tactic:
pderiv_monomial,

Goal state after:
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m : σ →₀ ℕ
r : R
⊢ X i * (monomial (m - single i 1)) (r * ↑(m i)) = m i • (monomial m) r
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.map (R ∙ s j).mkQ (Submodule.span R (Set.range s)) = Submodule.map (R ∙ s j).mkQ ⊤
⊢ Submodule.span R (Set.range s') = ⊤

Tactic:
Submodule.map_span,

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.map (R ∙ s j).mkQ ⊤
⊢ Submodule.span R (Set.range s') = ⊤
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: case monomial
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
⊢ coeff m ((pderiv i) ((monomial n) a)) = coeff (m + single i 1) ((monomial n) a) * (↑(m i) + 1)

Tactic:
pderiv_monomial,

Goal state after:
case monomial
R : Type u
σ : Type v
inst✝ : CommSemiring R
i : σ
m n : σ →₀ ℕ
a : R
⊢ coeff m ((monomial (n - single i 1)) (a * ↑(n i))) = coeff (m + single i 1) ((monomial n) a) * (↑(m i) + 1)
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R M'
⊢ ∀ {x₁ x₂ : M'}, LinearMap.id x₁ = LinearMap.id x₂ → ∃ c, c • x₁ = c • x₂

Tactic:
simpa using ⟨1, S.one_mem⟩

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)
α : ↥LieSubalgebra.root
⊢ α ∈ (invtSubmoduleToLieIdeal q hq).rootSet ↔ (rootSystem H).root α ∈ q

Tactic:
set J := invtSubmoduleToLieIdeal q hq

Goal state after:
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)
α : ↥LieSubalgebra.root
J : LieIdeal K L := invtSubmoduleToLieIdeal q hq
⊢ α ∈ J.rootSet ↔ (rootSystem H).root α ∈ q
Module: Mathlib.RingTheory.Extension.Basic

Goal state before:
pp: case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : mk x ∈ Submodule.restrictScalars P.Ring (map f).ker
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))

Tactic:
simp only [Submodule.restrictScalars_mem, LinearMap.mem_ker, map_mk, Hom.toAlgHom_apply,
      mk_eq_zero_iff] at hx

Goal state after:
case refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
P' : Extension R S
f : P.Hom P'
h : Function.Surjective ⇑f
eq : Ideal.comap f.toRingHom P'.ker = RingHom.ker f.toRingHom ⊔ P.ker
eq_map : P'.ker = Ideal.map f.toRingHom P.ker
x : ↥P.ker
hx : f.toRingHom ↑x ∈ P'.ker ^ 2
⊢ mk x ∈ Submodule.map mk (Submodule.comap (Submodule.subtype P.ker) (RingHom.ker f.toRingHom ⊓ P.ker))
Module: Mathlib.Algebra.Module.Presentation.Differentials

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Submodule.map (Submodule.subtype pres.ker) (Submodule.span pres.Ring (Set.range fun r ↦ ⟨pres.relation r, ⋯⟩)) =
    pres.ker

Tactic:
Submodule.map_span,

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
pres : Presentation R S ι σ
φ : (σ →₀ S) →ₗ[pres.Ring] pres.toExtension.Cotangent := { toFun := ⇑(hom₁ pres), map_add' := ⋯, map_smul' := ⋯ }
h₁ : Function.Surjective ⇑Extension.Cotangent.mk
⊢ Submodule.span pres.Ring (⇑(Submodule.subtype pres.ker) '' Set.range fun r ↦ ⟨pres.relation r, ⋯⟩) = pres.ker
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
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
| s

Tactic:
rw [← P.aeval_val_σ s]

Goal state after:
R : Type u
S : Type v
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
P✝ : Generators R S ι
ι' : Type u_1
T : Type ?u.18
inst✝¹ : CommRing T
inst✝ : Algebra R T
P : Generators R S ι'
e : ι ≃ ι'
s : S
| (aeval P.val) (P.σ s)
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) (n : P.Ring) (hn : n ∈ P.ker), 1 ⊗ₜ[P.Ring] ⟨r • n, ⋯⟩ = 0

Tactic:
hr

Goal state after:
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
⊢ ∀ (n : P.Ring) (hn : n ∈ P.ker), 1 ⊗ₜ[P.Ring] ⟨r • n, ⋯⟩ = 0
Module: Mathlib.Algebra.Module.Presentation.Free

Goal state before:
pp: A : Type u
inst✝³ : Ring A
relations : Relations A
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : IsEmpty relations.R
r : relations.R
⊢ False

Tactic:
exact IsEmpty.false r

Goal state after:
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:
by
        symm
        rw [← sub_eq_zero]
        simpa using s.linearCombination_var_relation (.add m₁ m₂)

Goal state after:
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
P : Extension R S
R' : Type u'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
this✝² : Algebra P.Ring S' := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
this✝¹ : IsScalarTower P.Ring S S'
this✝ : Algebra P.Ring P'.Ring := f.toAlgHom.toAlgebra
this : IsScalarTower P.Ring P'.Ring S'
⊢ P.CotangentSpace →ₗ[S] P'.CotangentSpace

Tactic:
apply LinearMap.liftBaseChange

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'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
this✝² : Algebra P.Ring S' := ⋯
this✝¹ : IsScalarTower P.Ring S S'
this✝ : Algebra P.Ring P'.Ring := ⋯
this : IsScalarTower P.Ring P'.Ring S'
⊢ Ω[P.Ring⁄R] →ₗ[P.Ring] P'.CotangentSpace
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: case tmul.zero
R : Type u
S : Type v
inst✝²² : CommRing R
inst✝²¹ : CommRing S
inst✝²⁰ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝¹⁹ : CommRing R'
inst✝¹⁸ : CommRing S'
inst✝¹⁷ : Algebra R' S'
P' : Extension R' S'
inst✝¹⁶ : Algebra R R'
inst✝¹⁵ : Algebra S S'
inst✝¹⁴ : Algebra R S'
inst✝¹³ : IsScalarTower R R' S'
R'' : Type u''
S'' : Type v''
inst✝¹² : CommRing R''
inst✝¹¹ : CommRing S''
inst✝¹⁰ : Algebra R'' S''
P'' : Extension R'' S''
inst✝⁹ : Algebra R R''
inst✝⁸ : Algebra S S''
inst✝⁷ : Algebra R S''
inst✝⁶ : IsScalarTower R R'' S''
inst✝⁵ : Algebra R' R''
inst✝⁴ : Algebra S' S''
inst✝³ : Algebra R' S''
inst✝² : IsScalarTower R' R'' S''
inst✝¹ : IsScalarTower R R' R''
inst✝ : IsScalarTower S S' S''
f : P.Hom P'
g : P'.Hom P''
x : S
⊢ (CotangentSpace.map (g.comp f)) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo 0) =
    (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo 0)

Tactic:
simp only [map_zero, tmul_zero]

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: 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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
⊢ VanishesTrivially R m n

Tactic:
set G : (ι →₀ R) →ₗ[R] M := Finsupp.linearCombination R m with hG
  have G_basis_eq (i : ι) : G (Finsupp.single i 1) = m i := by simp [hG]
  have G_surjective : Surjective G := by
    apply LinearMap.range_eq_top.mp
    apply top_le_iff.mp
    rw [← hm]
    apply Submodule.span_le.mpr
    rintro _ ⟨i, rfl⟩
    use Finsupp.single i 1, G_basis_eq i
  /- Consider the element $\sum_i e_i \otimes n_i$ of $R^\iota \otimes N$. It is in the kernel of
  $R^\iota \otimes N \to M \otimes N$. -/
  set en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ n i with hen
  have en_mem_ker : en ∈ ker (rTensor N G) := by simp [hen, G_basis_eq, hmn]
  -- We have an exact sequence $\ker G \to R^\iota \to M \to 0$.
  have exact_ker_subtype : Exact (ker G).subtype G := G.exact_subtype_ker_map
  -- Tensor the exact sequence with $N$.
  have exact_rTensor_ker_subtype : Exact (rTensor N (ker G).subtype) (rTensor N G) :=
    rTensor_exact (M := ↥(ker G)) N exact_ker_subtype G_surjective
  /- We conclude that $\sum_i e_i \otimes n_i$ is in the range of
    $\ker G \otimes N \to R^\iota \otimes N$. -/
  have en_mem_range : en ∈ range (rTensor N (ker G).subtype) :=
    exact_rTensor_ker_subtype.linearMap_ker_eq ▸ en_mem_ker
  /- There is an element of in $\ker G \otimes N$ that maps to $\sum_i e_i \otimes n_i$.
  Write it as a finite sum of pure tensors. -/
  obtain ⟨kn, hkn⟩ := en_mem_range
  obtain ⟨ma, rfl : kn = ∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2⟩ := exists_finset kn
  /- Let $\sum_j k_j \otimes y_j$ be the sum obtained in the previous step.
  In order to show that $\sum_i m_i \otimes n_i$ vanishes trivially, it suffices to prove that there
  exist $(a_{ij})_{i, j}$ such that for all $i$,
  $$n_i = \sum_j a_{ij} y_j$$
  and for all $j$,
  $$\sum_i a_{ij} m_i = 0.$$
  For this, take $a_{ij}$ to be the coefficient of $e_i$ in $k_j$. -/
  refine .of_fintype (κ := ma) (fun i ⟨⟨kj, _⟩, _⟩ ↦ (kj : ι →₀ R) i) (fun ⟨⟨_, yj⟩, _⟩ ↦ yj) ?_ ?_
  · intro i
    classical
    apply_fun finsuppScalarLeft R N ι at hkn
    apply_fun (· i) at hkn
    symm at hkn
    simp only [map_sum, finsuppScalarLeft_apply_tmul, zero_smul, Finsupp.single_zero,
      Finsupp.sum_single_index, one_smul, Finsupp.finsetSum_apply, Finsupp.single_apply,
      Finset.sum_ite_eq', Finset.mem_univ, ↓reduceIte, rTensor_tmul, coe_subtype, Finsupp.sum_apply,
      Finsupp.sum_ite_eq', Finsupp.mem_support_iff, ne_eq, ite_not, en] at hkn
    simp only [Finset.univ_eq_attach, Finset.sum_attach ma (fun x ↦ (x.1 : ι →₀ R) i • x.2)]
    convert! hkn using 2 with x _
    split
    · next h'x => rw [h'x, zero_smul]
    · rfl
  · rintro ⟨⟨⟨k, hk⟩, _⟩, _⟩
    simpa only [hG, linearCombination_apply, zero_smul, implies_true, Finsupp.sum_fintype] using
      mem_ker.mp hk

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: 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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := ⋯
m'_eq : m' = Subtype.coind m mem_M'
⊢ Submodule.map (span R (Set.range m)).subtype (span R (Set.range m')) = Submodule.map (span R (Set.range m)).subtype ⊤

Tactic:
Submodule.map_span,

Goal state after:
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
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : Injective ⇑(rTensor N (span R (Set.range m)).subtype)
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
mem_M' : ∀ (i : ι), m i ∈ span R (Set.range m)
m' : ι → ↥(span R (Set.range m)) := Subtype.coind m mem_M'
m'_eq : m' = Subtype.coind m mem_M'
⊢ span R (⇑(span R (Set.range m)).subtype '' Set.range m') = Submodule.map (span R (Set.range m)).subtype ⊤
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: case tmul.zero
R : Type u
S : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
P : Extension R S
R' : Type u'
S' : Type v'
inst✝⁷ : CommRing R'
inst✝⁶ : CommRing S'
inst✝⁵ : Algebra R' S'
P' : Extension R' S'
inst✝⁴ : Algebra R R'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R R' S'
inst✝ : IsScalarTower R S S'
f g : P.Hom P'
x : S
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo 0) =
    (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] (D R P.Ring).tensorProductTo 0)

Tactic:
simp only [map_zero, tmul_zero]

Goal state after:
Module: Mathlib.RingTheory.QuotSMulTop

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
r : R
M : Type u_1
M' : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
⊢ (map r) f ∘ₗ (r • ⊤).mkQ = (r • ⊤).mkQ ∘ₗ f

Tactic:
ext; rfl

Goal state after:
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ ∀ x ∈ support R M, x ∈ support R N

Tactic:
mem_support_iff'

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
⊢ ∀ (x : PrimeSpectrum R), (∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ ∀ x ∈ support R N, x ∈ support R M

Tactic:
mem_support_iff'

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
hf : Function.Surjective ⇑f
⊢ ∀ (x : PrimeSpectrum R), (∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0) → ∃ m, ∀ r ∉ x.asIdeal, r • m ≠ 0
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✝ : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.map ((TensorProduct.mk R k M) 1) (Submodule.span R (Set.range f)) = ⊤

Tactic:
Submodule.map_span,

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✝ : Module.Finite R M
ι : Type u_5
f : ι → M
b : Basis ι k (k ⊗[R] M)
hb : ∀ (i : ι), 1 ⊗ₜ[R] f i = b i
⊢ Submodule.span R (⇑((TensorProduct.mk R k M) 1) '' Set.range f) = ⊤
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
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n)) R ↥(⋀[R]^n M) := Basis.exteriorPower n (Free.chooseBasis R M)
⊢ Nat.card ↑(powersetCard (Free.ChooseBasisIndex R M) n) = (Fintype.card (Free.ChooseBasisIndex R M)).choose n

Tactic:
powersetCard.card,

Goal state after:
R : Type u_1
M : Type u_3
n : ℕ
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : Nontrivial R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
this : LinearOrder (Free.ChooseBasisIndex R M) := linearOrderOfSTO WellOrderingRel
B : Basis (↑(powersetCard (Free.ChooseBasisIndex R M) n)) R ↥(⋀[R]^n M) := Basis.exteriorPower n (Free.chooseBasis R M)
⊢ (Nat.card (Free.ChooseBasisIndex R M)).choose n = (Fintype.card (Free.ChooseBasisIndex R M)).choose n
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✝ : Module.Finite R M
p : PrimeSpectrum R
⊢ p ∈ support R M ↔ Nontrivial (p.asIdeal.ResidueField ⊗[R] M)

Tactic:
let K := p.asIdeal.ResidueField
  let e := (AlgebraTensorModule.cancelBaseChange R (Localization.AtPrime p.asIdeal) K K M).symm
  rw [e.nontrivial_congr, Module.mem_support_iff,
    (LocalizedModule.equivTensorProduct p.asIdeal.primeCompl M).nontrivial_congr,
    ← not_iff_not, not_nontrivial_iff_subsingleton, not_nontrivial_iff_subsingleton,
    IsLocalRing.subsingleton_tensorProduct]

Goal state after: