mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case zero
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ 1 = spanSingleton S 1

Tactic:
spanSingleton_one

Goal state after:
case zero
R : Type u_1
inst✝³ : CommRing R
S : Submonoid R
P : Type u_2
inst✝² : CommRing P
inst✝¹ : Algebra R P
inst✝ : IsLocalization S P
x : P
⊢ 1 = 1
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Basic

Goal state before:
pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ spanSingleton A⁰ 1 = 1

pp: A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ (algebraMap A (FractionRing A)) a ≠ 0

pp: case hI0
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ J ≠ ⊥

Tactic:
spanSingleton_one

Goal state after:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ 1 = 1

A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ (algebraMap A (FractionRing A)) a ≠ 0

case hI0
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
x✝ : IsDedekindDomain A
a : A
J : Ideal A
ha : a ≠ 0
hI : spanSingleton A⁰ ((algebraMap A (FractionRing A)) a)⁻¹ * ↑J ≠ ⊥
⊢ J ≠ ⊥
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: case h
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
inst✝³ : IsLocalization S P
P' : Type u_5
inst✝² : CommRing P'
inst✝¹ : Algebra R P'
inst✝ : IsLocalization S P'
x : P
z : R
hx' : z • x ∈ spanSingleton S x
h : (IsLocalization.map P' (RingHom.id R) ⋯) (z • x) ∈ (canonicalEquiv S P P') (spanSingleton S x)
⊢ z • (IsLocalization.map P' (RingHom.id R) ⋯) x = (IsLocalization.map P' (RingHom.id R) ⋯) (z • x)

Tactic:
rw [IsLocalization.map_smul, RingHom.id_apply]

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Operations

Goal state before:
pp: R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
⊢ spanSingleton R₁⁰ 1 = 1

Tactic:
spanSingleton_one

Goal state after:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I J : Ideal R₁
x y : R₁
hy : y ∈ R₁⁰
⊢ 1 = 1
Module: Mathlib.Algebra.Module.DedekindDomain

Goal state before:
pp: case hI
R : Type u
inst✝³ : CommRing R
inst✝² : IsDedekindDomain R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
hI : I ≠ ⊥
hM : Module.IsTorsionBySet R M ↑I
P : Multiset (Ideal R) := factors I
prime_of_mem : ∀ p ∈ P.toFinset, Prime p
p : Ideal R
hp : p ∈ ↑(factors I).toFinset
q : Ideal R
hq : q ∈ ↑(factors I).toFinset
pq : p ≠ q
⊢ q ^ Multiset.count q P ≠ ⊥

Tactic:
rw [← Ideal.zero_eq_bot]; apply pow_ne_zero; exact (prime_of_mem q hq).ne_zero

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_2
K : Type u_3
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
J : Ideal A
hJ : J ≠ ⊤
ι : Type u_4
s : Finset ι
f : ι → K
j : ι
hjs : j ∈ s
hjf : f j ≠ 0
I : FractionalIdeal A⁰ K := spanFinset A s f
hI0 : I ≠ 0
⊢ 0 < I⁻¹

Tactic:
simpa [pos_iff_ne_zero]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
R : Type u_3
inst✝³ : Ring R
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : StrongRankCondition R
e : M ≃ₗ[R] N
a✝ : Nontrivial R
this✝ : (↑e).index = -↑(finrank R (N ⧸ (↑e).range))
this : (↑e).index = ↑(finrank R ↥(↑e).ker)
⊢ (↑e).index = 0

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.Index

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
k : Type u_3
inst✝⁴ : DivisionRing k
inst✝³ : Module k M
inst✝² : Module k N
f : M →ₗ[k] N
inst✝¹ : FiniteDimensional k M
inst✝ : FiniteDimensional k N
h₁ : finrank k (N ⧸ f.range) + finrank k ↥f.range = finrank k N
h₂ : finrank k (M ⧸ f.ker) = finrank k ↥f.range
h₃ : finrank k (M ⧸ f.ker) + finrank k ↥f.ker = finrank k M
⊢ ↑(finrank k ↥f.ker) - ↑(finrank k (N ⧸ f.range)) = ↑(finrank k M) - ↑(finrank k N)

Tactic:
lia

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
s : Finset N
hs : Submodule.span R ↑s = ⊤
hs' : (linearCombination R Subtype.val).ker.FG
H : Function.Surjective ⇑(linearCombination R Subtype.val)
⊢ ∃ f, l ∘ₗ f = linearCombination R Subtype.val

Tactic:
choose f hf using show _ from hl
    exact ⟨Finsupp.linearCombination R (fun i ↦ f i), by ext; simp [hf]⟩

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
hJ' : Irreducible (Associates.mk J)
⊢ ¬(Associates.mk J).count (Associates.mk I).factors + 1 ≤ (Associates.mk J).count (Associates.mk I).factors

Tactic:
lia

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hI : I ≠ 0
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
⊢ (Associates.mk J).count (Associates.mk I).factors = Multiset.count J (normalizedFactors I)

Tactic:
replace hI : Associates.mk I ≠ 0 := Associates.mk_ne_zero.mpr hI
  have hJ' : Irreducible (Associates.mk J) := by
    simpa only [Associates.irreducible_mk] using (prime_of_isPrime hJ₀ hJ).irreducible
  apply (count_normalizedFactors_eq (p := J) (x := I) _ _).symm
  all_goals
    rw [← dvd_iff_le, ← Associates.mk_dvd_mk, Associates.mk_pow]
    simp only [Associates.dvd_eq_le]
    rw [Associates.prime_pow_dvd_iff_le hI hJ']
  lia

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

Goal state before:
pp: σ : Type u_1
R : Type u
inst✝ : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ p ∈ supported R s ↔ ↑p.vars ⊆ s

Tactic:
by
  classical
  rw [supported_eq_range_rename, AlgHom.mem_range]
  constructor
  · rintro ⟨p, rfl⟩
    refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_
    simp
  · intro hs
    exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)

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
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
⊢ C a • D f = a • D f

Tactic:
have : C (σ := σ) a • D f = D (C a * f) := by simp

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
D : Derivation R (MvPolynomial σ R) A
a : R
f : MvPolynomial σ R
this : C a • D f = D (C a * f)
⊢ C a • D f = a • D f
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : AddCommGroup N'
inst✝¹ : Module R N'
S : Submonoid R
f : N →ₗ[R] N'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] N'
σ : Finset M
hσ : Submodule.span R ↑σ = ⊤
τ : Finset (↥σ →₀ R)
hτ : Submodule.span R ↑τ = (linearCombination R Subtype.val).ker
π : (↥σ →₀ R) →ₗ[R] M := linearCombination R Subtype.val
hπ : Function.Surjective ⇑π
⊢ ∃ h s, f ∘ₗ h = s • g

Tactic:
choose s hs using IsLocalizedModule.surj S f
  let i : σ → N :=
    fun x ↦ (∏ j ∈ σ.erase x.1, (s (g j)).2) • (s (g x)).1
  let s₀ := ∏ j ∈ σ, (s (g j)).2
  have hi : f ∘ₗ Finsupp.linearCombination R i = (s₀ • g) ∘ₗ π := by
    ext j
    simp only [LinearMap.coe_comp, Function.comp_apply, Finsupp.lsingle_apply,
      linearCombination_single, one_smul, LinearMap.map_smul_of_tower, ← hs, LinearMap.smul_apply,
      i, s₀, π]
    rw [← mul_smul, Finset.prod_erase_mul]
    exact j.prop
  have : ∀ x : τ, ∃ s : S, s • (Finsupp.linearCombination R i x) = 0 := by
    intro x
    convert_to ∃ s : S, s • (Finsupp.linearCombination R i x) = s • 0
    · simp only [smul_zero]
    apply IsLocalizedModule.exists_of_eq (S := S) (f := f)
    rw [← LinearMap.comp_apply, map_zero, hi, LinearMap.comp_apply]
    convert! map_zero (s₀ • g)
    rw [← LinearMap.mem_ker, ← hτ]
    exact Submodule.subset_span x.prop
  choose s' hs' using this
  let s₁ := ∏ i : τ, s' i
  have : LinearMap.ker π ≤ LinearMap.ker (s₁ • Finsupp.linearCombination R i) := by
    rw [← hτ, Submodule.span_le]
    intro x hxσ
    simp only [s₁]
    rw [SetLike.mem_coe, LinearMap.mem_ker, LinearMap.smul_apply,
      ← Finset.prod_erase_mul _ _ (Finset.mem_univ ⟨x, hxσ⟩), mul_smul]
    convert! smul_zero _
    exact hs' ⟨x, hxσ⟩
  refine ⟨Submodule.liftQ _ _ this ∘ₗ
    (LinearMap.quotKerEquivOfSurjective _ hπ).symm.toLinearMap, s₁ * s₀, ?_⟩
  ext x
  obtain ⟨x, rfl⟩ := hπ x
  rw [← LinearMap.comp_apply, ← LinearMap.comp_apply, mul_smul, LinearMap.smul_comp, ← hi,
    ← LinearMap.comp_smul, LinearMap.comp_assoc, LinearMap.comp_assoc]
  simp

Goal state after:
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this✝ : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := Submonoid.powers (r * ↑s)
Rᵣₛ : Type u_3 := Localization rs
hsu : IsUnit ((algebraMap R Rᵣₛ) ↑s)
this : Function.Bijective ⇑(↑hsu.unit⁻¹ • (LocalizedModule.map rs) l')
x : M
⊢ ((LocalizedModule.lift (Submonoid.powers (r * ↑s)) g ⋯ ∘ₗ
          ↑R ↑(LinearEquiv.ofBijective (↑hsu.unit⁻¹ • (LocalizedModule.map rs) l') this)) ∘ₗ
        LocalizedModule.mkLinearMap rs M)
      x =
    ((↑l ∘ₗ LocalizedModule.lift (Submonoid.powers (r * ↑s)) f ⋯) ∘ₗ LocalizedModule.mkLinearMap rs M) x

Tactic:
apply ((Module.End.isUnit_iff _).mp (IsLocalizedModule.map_units g s)).1

Goal state after:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
S : Submonoid R
M' : Type u_1
inst✝⁷ : AddCommGroup M'
inst✝⁶ : Module R M'
f : M →ₗ[R] M'
inst✝⁵ : IsLocalizedModule S f
N' : Type u_2
inst✝⁴ : AddCommGroup N'
inst✝³ : Module R N'
g : N →ₗ[R] N'
inst✝² : IsLocalizedModule S g
inst✝¹ : FinitePresentation R M
inst✝ : FinitePresentation R N
l : M' ≃ₗ[R] N'
l' : M →ₗ[R] N
s : ↥S
H : g ∘ₗ l' = s • ↑l ∘ₗ f
this✝ : Function.Bijective ⇑((map S f g) l')
r : R
hr : r ∈ S
hr' : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) l')
rs : Submonoid R := ⋯
Rᵣₛ : Type u_3 := ⋯
hsu : IsUnit ((algebraMap R Rᵣₛ) ↑s)
this : Function.Bijective ⇑(↑hsu.unit⁻¹ • (LocalizedModule.map rs) l')
x : M
⊢ ((algebraMap R (End R N')) ↑s)
      (((LocalizedModule.lift (Submonoid.powers (r * ↑s)) g ⋯ ∘ₗ
            ↑R ↑(LinearEquiv.ofBijective (↑hsu.unit⁻¹ • (LocalizedModule.map rs) l') this)) ∘ₗ
          LocalizedModule.mkLinearMap rs M)
        x) =
    ((algebraMap R (End R N')) ↑s)
      (((↑l ∘ₗ LocalizedModule.lift (Submonoid.powers (r * ↑s)) f ⋯) ∘ₗ LocalizedModule.mkLinearMap rs M) x)
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'
this : IsLocalizedModule S LinearMap.id
r : R
hrp : r ∈ S
H : ∀ (t : R), r ∣ t → Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers t)) f)
hrp' : Submonoid.powers r ≤ S
y : M'
x : M
n : ℕ
hx :
  ((LocalizedModule.map (Submonoid.powers r)) f)
      (Function.uncurry (mk' (LocalizedModule.mkLinearMap (Submonoid.powers r) M)) (x, ⟨(fun x ↦ r ^ x) n, ⋯⟩)) =
    (LocalizedModule.mkLinearMap (Submonoid.powers r) M') y
⊢ ∃ m, r ^ (m + n) • y = f (r ^ m • x)

Tactic:
by
      simpa [LocalizedModule.map, IsLocalizedModule.mk_eq_mk', -IsLocalizedModule.mk'_one,
        pow_add, mul_smul, IsLocalizedModule.mk'_eq_mk'_iff, Submonoid.mem_powers_iff,
        Submonoid.smul_def] using hx

Goal state after:
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 ι σ
⊢ pres.toExtension.toKaehler ∘ₗ ↑pres.cotangentSpaceBasis.repr.symm =
    Finsupp.linearCombination S fun g ↦ (D R S) (pres.val g)

Tactic:
ext
  simp

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
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
y : P.Ring
y_in : y ∈ P.ker ^ 2
z : P.Ring
z_in : z ∈ RingHom.ker f.toRingHom
hyz : z = ↑x - y
⊢ 2 ≠ 0

Tactic:
lia

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

Goal state before:
pp: case mpr
A : Type u
inst✝² : Ring A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
⊢ (∃ pres, Finite pres.G ∧ Finite pres.R) → FinitePresentation A M

Tactic:
· rintro ⟨pres, _, _⟩
    exact pres.finitePresentation

Goal state after:
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
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(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)) =
    coeff i ((Q.ofComp P).toAlgHom x)

Tactic:
Finset.sum_filter,

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
e : (ι' ⊕ ι →₀ ℕ) ≃+ (ι' →₀ ℕ) × (ι →₀ ℕ) := Finsupp.sumFinsuppAddEquivProdFinsupp
i : ι' →₀ ℕ
this :
  ∀ (x : (Q.comp P).Ring),
    (Function.support fun a ↦ if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) ⊆
      ↑(Finset.map (↑e).toEmbedding (support x))
⊢ (∑ a ∈ Finset.map (↑e).toEmbedding (support x),
      if a.1 = i then (aeval P.val) ((monomial a.2) (coeff (e.symm a) x)) else 0) =
    coeff i ((Q.ofComp P).toAlgHom x)
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
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
hkn : (rTensor N G.ker.subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
⊢ VanishesTrivially R m n

Tactic:
refine .of_fintype (κ := ma) (fun i ⟨⟨kj, _⟩, _⟩ ↦ (kj : ι →₀ R) i) (fun ⟨⟨_, yj⟩, _⟩ ↦ yj) ?_ ?_

Goal state after:
case refine_1
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
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
hkn : (rTensor N G.ker.subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
⊢ ∀ (i : ι),
    n i =
      ∑ j,
        (match j with
          | ⟨(kj, snd), property⟩ => ↑kj i) •
          match j with
          | ⟨(fst, yj), property⟩ => yj

case refine_2
R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : Fintype ι
m : ι → M
n : ι → N
hm : span R (Set.range m) = ⊤
hmn : ∑ i, m i ⊗ₜ[R] n i = 0
G : (ι →₀ R) →ₗ[R] M := linearCombination R m
hG : G = linearCombination R m
G_basis_eq : ∀ (i : ι), G (Finsupp.single i 1) = m i
G_surjective : Surjective ⇑G
en : (ι →₀ R) ⊗[R] N := ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
hen : en = ∑ i, Finsupp.single i 1 ⊗ₜ[R] n i
en_mem_ker : en ∈ (rTensor N G).ker
exact_ker_subtype : Exact ⇑G.ker.subtype ⇑G
exact_rTensor_ker_subtype : Exact ⇑(rTensor N G.ker.subtype) ⇑(rTensor N G)
ma : Finset (↥G.ker × N)
hkn : (rTensor N G.ker.subtype) (∑ kj ∈ ma, kj.1 ⊗ₜ[R] kj.2) = en
⊢ ∀ (j : ↥ma),
    ∑ i,
        (match j with
          | ⟨(kj, snd), property⟩ => ↑kj i) •
          m i =
      0
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'
f : P.Hom P'
x : P.Cotangent
⊢ (CotangentSpace.map f) (P.cotangentComplex x) = P'.cotangentComplex ((Cotangent.map f) x)

Tactic:
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
  rw [cotangentComplex_mk, map_tmul, map_one, Cotangent.map_mk, cotangentComplex_mk]

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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
x : ↥M' ⊗[R] N
hx : (rTensor N M'.subtype) x = 0
⊢ x = 0

Tactic:
obtain ⟨s, rfl⟩ := exists_finset x

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
hMN : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
s : Finset (↥M' × N)
hx : (rTensor N M'.subtype) (∑ i ∈ s, i.1 ⊗ₜ[R] i.2) = 0
⊢ ∑ i ∈ s, i.1 ⊗ₜ[R] i.2 = 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
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
e₁ : r • m ∈ Set.range ⇑f
⊢ ∃ r ∉ x.asIdeal, r • m = 0

Tactic:
obtain ⟨m', hm'⟩ := e₁

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
P : Type u_4
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Function.Exact ⇑f ⇑g
hf : Function.Injective ⇑f
hg : Function.Surjective ⇑g
x : PrimeSpectrum R
H₁ : ∀ (m : M), ∃ r ∉ x.asIdeal, r • m = 0
H₂ : ∀ (m : P), ∃ r ∉ x.asIdeal, r • m = 0
m : N
r : R
hr : r ∉ x.asIdeal
m' : M
hm' : f m' = r • m
⊢ ∃ r ∉ x.asIdeal, r • m = 0
Module: Mathlib.RingTheory.Support

Goal state before:
pp: case a.refine_2
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
⊢ I ≤ (I • ⊤).colon Set.univ

Tactic:
exact fun x hx ↦ Submodule.mem_colon.mpr fun p hp ↦ Submodule.smul_mem_smul hx hp

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
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 • ⊤
⊢ Submodule.localized' (Localization p.asIdeal.primeCompl) p.asIdeal.primeCompl
      (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) (I • ⊤) =
    Ideal.map (algebraMap R Rₚ) I • ⊤

Tactic:
Submodule.localized'_smul,

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
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 • ⊤
⊢ Submodule.localized' (Localization p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (Algebra.linearMap R (Localization p.asIdeal.primeCompl)) I •
      Submodule.localized' (Localization p.asIdeal.primeCompl) p.asIdeal.primeCompl
        (LocalizedModule.mkLinearMap p.asIdeal.primeCompl M) ⊤ =
    Ideal.map (algebraMap R Rₚ) I • ⊤