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

Goal state before:
pp: case e_a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ ↑(count J (normalizedFactors I)) = emultiplicity J I

pp: case e_a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ FiniteMultiplicity J I

Tactic:
emultiplicity_eq_count_normalizedFactors hJ hI,

Goal state after:
case e_a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ ↑(count J (normalizedFactors I)) = ↑(count (normalize J) (normalizedFactors I))

case e_a
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ FiniteMultiplicity J I
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : emultiplicity J I ≤ ↑n
⊢ count J (normalizedFactors I) ≤ n

Tactic:
emultiplicity_eq_count_normalizedFactors hJ hI,

Goal state after:
T : Type u_4
inst✝¹ : CommRing T
inst✝ : IsDedekindDomain T
I J : Ideal T
hI : I ≠ ⊥
hJ : Irreducible J
n : ℕ
hn : ↑(count (normalize J) (normalizedFactors I)) ≤ ↑n
⊢ count J (normalizedFactors I) ≤ n
Module: Mathlib.Algebra.Module.LinearMap.Prod

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsLinearMap R fun x ↦ x.1 - x.2

Tactic:
apply IsLinearMap.mk
  · simp [add_comm, add_assoc, add_left_comm, sub_eq_add_neg]
  · simp [smul_sub]

Goal state after:
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.inf fun i ↦ (f i).asIdeal ^ e i) = ∏ i ∈ s, (f i).asIdeal ^ e i

Tactic:
rw [prod_eq_iInf_of_pairwise_isCoprime]

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
⊢ (s.inf fun i ↦ (f i).asIdeal ^ e i) = ⨅ i ∈ s, (f i).asIdeal ^ e i

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)
Module: Mathlib.Algebra.Module.LocalizedModule.Int

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' ↑(Finset.image (fun t ↦ integerMultiple S f s id t) s.attach) = commonDenomOfFinset S f s • ↑s

Tactic:
rw [Finset.coe_image]

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Submonoid R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
M' : Type u_3
inst✝³ : AddCommMonoid M'
inst✝² : Module R M'
f : M →ₗ[R] M'
inst✝¹ : IsLocalizedModule S f
inst✝ : DecidableEq M
s : Finset M'
⊢ ⇑f '' (fun t ↦ integerMultiple S f s id t) '' ↑s.attach = commonDenomOfFinset S f s • ↑s
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
r : R
hr : r ≠ 0
⊢ ↑{d | d ∈ normalizedFactors r} ≃ ↑{I | I ∈ normalizedFactors (span {r})}

Tactic:
by
  refine Equiv.ofBijective ?_ ?_
  · exact fun d =>
      ⟨span {↑d}, singleton_span_mem_normalizedFactors_of_mem_normalizedFactors d.prop⟩
  · refine ⟨?_, ?_⟩
    · rintro ⟨a, ha⟩ ⟨b, hb⟩ h
      rw [Subtype.mk_eq_mk, span_singleton_eq_span_singleton, Subtype.coe_mk,
          Subtype.coe_mk] at h
      exact Subtype.mk_eq_mk.mpr (mem_normalizedFactors_eq_of_associated ha hb h)
    · rintro ⟨i, hi⟩
      have : i.IsPrime := isPrime_of_prime (prime_of_normalized_factor i hi)
      have := exists_mem_normalizedFactors_of_dvd hr
        (Submodule.IsPrincipal.prime_generator_of_isPrime i
        (prime_of_normalized_factor i hi).ne_zero).irreducible ?_
      · obtain ⟨a, ha, ha'⟩ := this
        use ⟨a, ha⟩
        simp only [← span_singleton_eq_span_singleton.mpr ha',
            span_singleton_generator]
      · exact (Submodule.IsPrincipal.mem_iff_generator_dvd i).mp
          ((show span {r} ≤ i from dvd_iff_le.mp (dvd_of_mem_normalizedFactors hi))
            (mem_span_singleton.mpr (dvd_refl r)))

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

Goal state before:
pp: case refine_2
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FinitePresentation R S
inst✝ : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : (Fin n → S) →ₗ[R] M := ↑R (↑e.symm ∘ₗ K.mkQ)
⊢ f.ker.FG

Tactic:
have : Module.Finite S
        (Submodule.restrictScalars R (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ))) :=
      .of_fg <| show (LinearMap.ker (e.symm.toLinearMap ∘ₗ K.mkQ)).FG by simpa

Goal state after:
case refine_2
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
S : Type u_1
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : Module S M
inst✝² : IsScalarTower R S M
inst✝¹ : FinitePresentation R S
inst✝ : FinitePresentation S M
n : ℕ
K : Submodule S (Fin n → S)
e : M ≃ₗ[S] (Fin n → S) ⧸ K
hK : K.FG
f : (Fin n → S) →ₗ[R] M := ↑R (↑e.symm ∘ₗ K.mkQ)
this : Module.Finite S ↥(Submodule.restrictScalars R (↑e.symm ∘ₗ K.mkQ).ker)
⊢ f.ker.FG
Module: Mathlib.Algebra.Module.PID

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
m : ℕ
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
e : M ≃ₗ[R] (Fin m →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
⊢ ∃ x, (toSpanSingleton R M x).ker = annihilator R M

Tactic:
refine ⟨e.symm (Finsupp.equivFunOnFinite.symm fun _ ↦ 1, DFinsupp.equivFunOnFintype.symm
    fun _ ↦ mkQ _ 1), le_antisymm (fun x h ↦ ?_) fun x h ↦ mem_annihilator.mp h _⟩

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
M : Type v
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : Module.Finite R M
m : ℕ
ι : Type u
w✝ : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
e : M ≃ₗ[R] (Fin m →₀ R) × ⨁ (i : ι), R ⧸ R ∙ p i ^ n i
x : R
h :
  x ∈
    (toSpanSingleton R M
        (e.symm
          (Finsupp.equivFunOnFinite.symm fun x ↦ 1, DFinsupp.equivFunOnFintype.symm fun x ↦ (R ∙ p x ^ n x).mkQ 1))).ker
⊢ x ∈ annihilator R M
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p✝ : MvPolynomial Unit R
hp : p✝ ∈ Ideal.span {C r * X () - 1}
p q : MvPolynomial Unit R
⊢ p ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
    q ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
      (aeval fun x ↦ invSelf r) p = 0 → (aeval fun x ↦ invSelf r) q = 0 → (aeval fun x ↦ invSelf r) (p + q) = 0

Tactic:
_

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p✝ : MvPolynomial Unit R
hp : p✝ ∈ Ideal.span {C r * X () - 1}
p q : MvPolynomial Unit R
hx✝ : p ∈ MvPolynomial Unit R ∙ (C r * X () - 1)
⊢ q ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
    (aeval fun x ↦ invSelf r) p = 0 → (aeval fun x ↦ invSelf r) q = 0 → (aeval fun x ↦ invSelf r) (p + q) = 0
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p✝ : MvPolynomial Unit R
hp : p✝ ∈ Ideal.span {C r * X () - 1}
p q : MvPolynomial Unit R
hx✝ : p ∈ MvPolynomial Unit R ∙ (C r * X () - 1)
⊢ q ∈ MvPolynomial Unit R ∙ (C r * X () - 1) →
    (aeval fun x ↦ invSelf r) p = 0 → (aeval fun x ↦ invSelf r) q = 0 → (aeval fun x ↦ invSelf r) (p + q) = 0

Tactic:
_

Goal state after:
case refine_3
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p✝ : MvPolynomial Unit R
hp : p✝ ∈ Ideal.span {C r * X () - 1}
p q : MvPolynomial Unit R
hx✝ : p ∈ MvPolynomial Unit R ∙ (C r * X () - 1)
hy✝ : q ∈ MvPolynomial Unit R ∙ (C r * X () - 1)
⊢ (aeval fun x ↦ invSelf r) p = 0 → (aeval fun x ↦ invSelf r) q = 0 → (aeval fun x ↦ invSelf r) (p + q) = 0
Module: Mathlib.RingTheory.MvPolynomial.Localization

Goal state before:
pp: case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
a x : MvPolynomial Unit R
⊢ x ∈ MvPolynomial Unit R ∙ (C r * X () - 1) → (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) (a • x) = 0

Tactic:
_

Goal state after:
case refine_4
σ : Type u_1
R : Type u_2
inst✝³ : CommRing R
M : Submonoid R
S : Type u_3
inst✝² : CommRing S
inst✝¹ : Algebra R S
r : R
inst✝ : Away r S
p : MvPolynomial Unit R
hp : p ∈ Ideal.span {C r * X () - 1}
a x : MvPolynomial Unit R
hx✝ : x ∈ MvPolynomial Unit R ∙ (C r * X () - 1)
⊢ (aeval fun x ↦ invSelf r) x = 0 → (aeval fun x ↦ invSelf r) (a • x) = 0
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)
x m : L
hm : m ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
⊢ ⁅x, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier

Tactic:
have hx : x ∈ ⨆ χ : Weight K H L, genWeightSpace L χ := by
      simp [LieModule.iSup_genWeightSpace_eq_top']

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)
x m : L
hm : m ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
hx : x ∈ ⨆ χ, genWeightSpace L ⇑χ
⊢ ⁅x, m⁆ ∈ (↑(⨆ α, sl2SubmoduleOfRoot ⋯)).carrier
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
b : B
w : presM.R →₀ B
⊢ r ∉ w.support →
    b ≠ 0 →
      w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
        Finsupp.single r b + w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
_

Goal state after:
case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
b : B
w : presM.R →₀ B
a✝ : r ∉ w.support
⊢ b ≠ 0 →
    w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
      Finsupp.single r b + w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
b : B
w : presM.R →₀ B
a✝ : r ∉ w.support
⊢ b ≠ 0 →
    w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
      Finsupp.single r b + w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
_

Goal state after:
case single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
b : B
w : presM.R →₀ B
a✝¹ : r ∉ w.support
a✝ : b ≠ 0
⊢ w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
    Finsupp.single r b + w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝¹ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝ : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
⊢ g ∉ f.support →
    a ≠ 0 →
      Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
        Finsupp.single r (presB.π (Finsupp.single g a + f)) ∈
          Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
_

Goal state after:
case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝² : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝¹ : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝ : g ∉ f.support
⊢ a ≠ 0 →
    Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
      Finsupp.single r (presB.π (Finsupp.single g a + f)) ∈
        Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.Algebra.Module.Presentation.RestrictScalars

Goal state before:
pp: case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝² : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝¹ : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝ : g ∉ f.support
⊢ a ≠ 0 →
    Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
      Finsupp.single r (presB.π (Finsupp.single g a + f)) ∈
        Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)

Tactic:
_

Goal state after:
case single_add.single_add
B : Type u_1
inst✝⁸ : Ring B
M : Type u_2
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module B M
inst✝⁵ : DecidableEq B
presM : Presentation B M
inst✝⁴ : DecidableEq presM.G
A : Type u_3
inst✝³ : CommRing A
inst✝² : Algebra A B
inst✝¹ : Module A M
inst✝ : IsScalarTower A B M
presB : Presentation A B
data : presM.RestrictScalarsData presB
v : presM.R →₀ B
r : presM.R
w : presM.R →₀ B
a✝³ : r ∉ w.support
hw : w ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
β : presB.G →₀ A
a✝² : presB.π β ≠ 0
g : presB.G
a : A
f : presB.G →₀ A
a✝¹ : g ∉ f.support
a✝ : a ≠ 0
⊢ Finsupp.single r (presB.π f) ∈ Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1) →
    Finsupp.single r (presB.π (Finsupp.single g a + f)) ∈
      Submodule.span A (Set.range fun x ↦ presB.var x.1 • Finsupp.single x.2 1)
Module: Mathlib.RingTheory.Extension.Cotangent.Basic

Goal state before:
pp: case tmul
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
y : Ω[P.Ring⁄R]
⊢ (CotangentSpace.map (g.comp f)) (x ⊗ₜ[P.Ring] y) =
    (↑S (CotangentSpace.map g) ∘ₗ CotangentSpace.map f) (x ⊗ₜ[P.Ring] y)

Tactic:
| tmul x y =>

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

Goal state before:
pp: case tmul
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
y : Ω[P.Ring⁄R]
⊢ (CotangentSpace.map f - CotangentSpace.map g) (x ⊗ₜ[P.Ring] y) = (↑S P'.cotangentComplex ∘ₗ f.sub g) (x ⊗ₜ[P.Ring] y)

Tactic:
| tmul x y =>

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
s : Finset (↥M' × N)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this : VanishesTrivially R (fun i ↦ ↑(↑(e i)).1) fun i ↦ (↑(e i)).2
⊢ VanishesTrivially R (fun i ↦ (↑i).1) fun i ↦ (↑i).2

Tactic:
← e.vanishesTrivially_comp

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)
e : Fin (Fintype.card ↥s) ≃ ↥s
hx : ∑ i, ↑(↑(e i)).1 ⊗ₜ[R] (↑(e i)).2 = 0
this : VanishesTrivially R (fun i ↦ ↑(↑(e i)).1) fun i ↦ (↑(e i)).2
⊢ VanishesTrivially R ((fun i ↦ (↑i).1) ∘ ⇑e) ((fun i ↦ (↑i).2) ∘ ⇑e)
Module: Mathlib.LinearAlgebra.TensorProduct.Vanishing

Goal state before:
pp: case mp
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
h : ∀ {l : ℕ} {m : Fin l → M} {n : Fin l → N}, ∑ i, m i ⊗ₜ[R] n i = 0 → VanishesTrivially R m n
M' : Submodule R M
⊢ M'.FG → Injective ⇑(rTensor N M'.subtype)

Tactic:
_

Goal state after:
case mp
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
h : ∀ {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'.FG
⊢ Injective ⇑(rTensor N M'.subtype)
Module: Mathlib.RingTheory.Localization.Finiteness

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

Tactic:
obtain ⟨⟨_, a, ha₁, rfl⟩, ha₂⟩ :=
    (IsLocalization.eq_iff_exists (M.map (algebraMap R S)) S').mp hx''

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
⊢ p ∈ support R A ↔ p ∈ PrimeSpectrum.zeroLocus ↑(RingHom.ker (algebraMap R A))

Tactic:
simp only [mem_support_iff', ne_eq, PrimeSpectrum.mem_zeroLocus, SetLike.coe_subset_coe]

Goal state after:
R : Type u_1
inst✝² : CommRing R
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra R A
p : PrimeSpectrum R
⊢ (∃ m, ∀ r ∉ p.asIdeal, ¬r • m = 0) ↔ RingHom.ker (algebraMap R A) ≤ p.asIdeal
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis ι R ↥M
H : Function.Injective ⇑(mulLeftMap N ⇑m)
⊢ M.LinearDisjoint N

Tactic:
mulLeftMap_eq_mulMap_comp,

Goal state after:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
M N : Submodule R S
ι : Type u_1
m : Basis ι R ↥M
H :
  Function.Injective
    ⇑(M.mulMap N ∘ₗ
        LinearMap.rTensor (↥N) (Finsupp.linearCombination R ⇑m) ∘ₗ ↑(TensorProduct.finsuppScalarLeft R (↥N) ι).symm)
⊢ M.LinearDisjoint N