mathlib-initiative/mathlib-tactics huggingface dataset:
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✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝¹ x✝ : Ideal A
⊢ x✝¹ ⊔ x✝ ∣ x✝¹

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝¹ x✝ : Ideal A
⊢ x✝¹ ≤ x✝¹ ⊔ x✝
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✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝¹ x✝ : Ideal A
⊢ x✝¹ ⊔ x✝ ∣ x✝

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Field K
inst✝² : IsDedekindDomain A
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
x✝¹ x✝ : Ideal A
⊢ x✝ ≤ x✝¹ ⊔ x✝
Module: Mathlib.Algebra.Module.Lattice

Goal state before:
pp: R : Type u_1
inst✝⁹ : CommRing R
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
V : Type u_3
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module K V
inst✝⁴ : Module R V
inst✝³ : IsScalarTower R K V
inst✝² : IsDomain R
inst✝¹ : Module.Finite K V
inst✝ : IsFractionRing R K
M : Submodule R V
hfg : M.FG
hr : Module.rank K V ≤ Module.rank R ↥M
⊢ span K ↑M = ⊤

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁹ : CommRing R
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
V : Type u_3
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module K V
inst✝⁴ : Module R V
inst✝³ : IsScalarTower R K V
inst✝² : IsDomain R
inst✝¹ : Module.Finite K V
inst✝ : IsFractionRing R K
M : Submodule R V
hfg : M.FG
hr : Module.rank K V ≤ Module.rank R ↥M
⊢ span K ↑M = ⊤
Module: Mathlib.Algebra.Module.LinearMap.FiniteRange

Goal state before:
pp: K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u v : V →ₗ[K] V₂
u' : V₂ →ₗ[K] V₃
h : (u - v).HasNoetherianRange
⊢ (u' ∘ₗ u - u' ∘ₗ v).HasNoetherianRange

Tactic:
simpa using

Goal state after:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst✝⁶ : CommRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
u v : V →ₗ[K] V₂
u' : V₂ →ₗ[K] V₃
h : (u - v).HasNoetherianRange
⊢ (u' ∘ₗ u - u' ∘ₗ v).HasNoetherianRange
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ I ≠ ⊤ ↔ ∃ P, I ≤ P.asIdeal

Tactic:
by
  rw [Ideal.ne_top_iff_exists_maximal]
  constructor
  · rintro ⟨M, hMmax, hIM⟩
    exact ⟨(equivMaximalSpectrum hR).symm ⟨M, hMmax⟩, hIM⟩
  · rintro ⟨P, hP⟩
    exact ⟨((equivMaximalSpectrum hR) P).asIdeal, ((equivMaximalSpectrum hR) P).isMaximal, hP⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
P Q : HeightOneSpectrum R
hPQ : P ≠ Q
⊢ P.asIdeal ≠ Q.asIdeal

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
P Q : HeightOneSpectrum R
hPQ : P ≠ Q
⊢ ¬P.asIdeal = Q.asIdeal
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case refine_1
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (linearCombination R Subtype.val).ker.FG
⊢ (linearCombination R Subtype.val ∘ₗ
        ↑(lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card)).symm).range =
    ⊤

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (linearCombination R Subtype.val).ker.FG
⊢ Submodule.span R ↑ι = ⊤
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: case refine_2
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (linearCombination R Subtype.val).ker.FG
⊢ (linearCombination R Subtype.val ∘ₗ
        ↑(lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card)).symm).ker.FG

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Submodule.span R ↑ι = ⊤
hι₂ : (linearCombination R Subtype.val).ker.FG
⊢ (Submodule.map (↑(lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card)))
      (linearCombination R Subtype.val).ker).FG
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
n : ℕ
K : Submodule R (Fin n → R)
e : M ≃ₗ[R] (Fin n → R) ⧸ K
h : K.FG
m : ℕ
g' : (Fin m → R) →ₗ[R] Fin n → R
hg' : g'.range = K
⊢ Function.Surjective ⇑(↑e.symm ∘ₗ K.mkQ)

Tactic:
simpa using

Goal state after:
R : Type u
M : Type u_1
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
fp : FinitePresentation R M
n : ℕ
K : Submodule R (Fin n → R)
e : M ≃ₗ[R] (Fin n → R) ⧸ K
h : K.FG
m : ℕ
g' : (Fin m → R) →ₗ[R] Fin n → R
hg' : g'.range = K
⊢ Function.Surjective ⇑K.mkQ
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
⊢ ↑(finrank R ↥⊤) - ↑(finrank R (N ⧸ ⊥)) = ↑(finrank R M) - ↑(finrank R N)

Tactic:
simpa using

Goal state after:
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
⊢ finrank R (N ⧸ ⊥) = finrank R N
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
f : M →ₗ[R] N
inst✝ : Nontrivial R
hf : Injective ⇑f
⊢ f.index = -↑(finrank R (N ⧸ f.range))

Tactic:
simpa using

Goal state after:
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
f : M →ₗ[R] N
inst✝ : Nontrivial R
hf : Injective ⇑f
⊢ finrank R ↥f.ker = 0
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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
x✝ : ↥⋯.toFinset
x : N
hx : x ∈ ⋯.toFinset
⊢ ∃ a, l (b a) = x

Tactic:
simpa using

Goal state after:
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✝¹ : Free R M
inst✝ : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective ⇑l
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M → ↥⋯.toFinset := fun i ↦ ⟨l (b i), ⋯⟩
x✝ : ↥⋯.toFinset
x : N
hx : x ∈ ⋯.toFinset
⊢ ∃ a, l (b a) = x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : I = ⊥
⊢ a ∈ I ∨ b ∈ I ^ (n✝ + 1)

Tactic:
simpa using

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I.IsPrime
a b : R
n✝ : ℕ
h : a * b ∈ I ^ (n✝ + 1)
hI0 : I = ⊥
⊢ a = 0 ∨ b = 0
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
⊢ Irreducible (Associates.mk J)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J : Ideal R
hJ : J.IsPrime
hJ₀ : J ≠ ⊥
hI : Associates.mk I ≠ 0
⊢ Irreducible J
Module: Mathlib.Algebra.Module.LocalizedModule.Away

Goal state before:
pp: case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
N : Type u_5
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
r : R
h₁ : IsUnit ((algebraMap R (Module.End R N)) r)
h₂ : ∀ (x : N), ∃ n y, r ^ n • x = f y
h₃ : ∀ (x : M), f x = 0 → ∃ n, r ^ n • x = 0
x y : M
hxy : f x = f y
this : f (x - y) = 0
n : ℕ
hn : r ^ n • (x - y) = 0
⊢ r ^ n • x = r ^ n • y

Tactic:
simpa using

Goal state after:
case h
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_4
N : Type u_5
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
r : R
h₁ : IsUnit ((algebraMap R (Module.End R N)) r)
h₂ : ∀ (x : N), ∃ n y, r ^ n • x = f y
h₃ : ∀ (x : M), f x = 0 → ∃ n, r ^ n • x = 0
x y : M
hxy : f x = f y
this : f (x - y) = 0
n : ℕ
hn : r ^ n • (x - y) = 0
⊢ r ^ n • x = r ^ n • y
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ : J ∣ I
hK : K ∣ I
hJ0 : J = 0
⊢ J * K ∣ I

Tactic:
simpa using

Goal state after:
case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
I J K : Ideal R
coprime : ∀ (P : Ideal R), P ∣ J → P ∣ K → ¬P.IsPrime
hJ : J ∣ I
hK : K ∣ I
hJ0 : J = 0
⊢ 0 ∣ 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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
⊢ ∃ b, ∀ i ∈ s, IsInteger f (↑b • g i)

Tactic:
refine ⟨∏ i ∈ s, (sec i).2, fun i hi => ⟨?_, ?_⟩⟩

Goal state after:
case refine_1
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ M

case refine_2
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
ι : Type u_4
s : Finset ι
g : ι → M'
sec : ι → M × ↥S
hsec : ∀ (i : ι), (sec i).2 • g i = f (sec i).1
i : ι
hi : i ∈ s
⊢ f ?refine_1 = ↑(∏ i ∈ s, (sec i).2) • g i
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : span {x} * span {x} ∣ span {a}
⊢ IsUnit x

Tactic:
simpa using

Goal state after:
case refine_1
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : Squarefree (span {a})
x : R
hx : span {x} * span {x} ∣ span {a}
⊢ IsUnit x
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: case neg.refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : NormalizationMonoid R
a b : R
ha : a ∈ normalizedFactors b
hb : ¬b = 0
this : Prime (span {a})
h : span {b} = 0
⊢ False

Tactic:
exact hb (span_singleton_eq_bot.mp h)

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

Goal state before:
pp: case pos.hk
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a b : R
h : FiniteMultiplicity a b
⊢ a ^ multiplicity a b ∣ b

Tactic:
exact pow_multiplicity_dvd a b

Goal state after:
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
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁✝ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
hx₁ : y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))
hx : ↑y • f x ∈ y • Submodule.span R ↑s
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)

Tactic:
rw [hx₁, ← f.map_smul, ← Submodule.map_span f] at hx

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
x : M
s : Finset M'
y : ↥S := commonDenomOfFinset S f s
hx₁✝ : y • ↑s = ⇑f '' ↑(finsetIntegerMultiple S f s)
hx₁ : y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))
hx : f (↑y • x) ∈ Submodule.map f (Submodule.span R ↑(finsetIntegerMultiple S f s))
⊢ ∃ m, m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX₁ : normUnit X = 1
hX : Prime X
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count X (normalizedFactors r)

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
r X : R
hr : r ≠ 0
hX₁ : normUnit X = 1
hX : Prime X
⊢ Multiset.count (span {X}) (normalizedFactors (span {r})) = Multiset.count X (normalizedFactors r)
Module: Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

Goal state before:
pp: A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
x✝ : Ideal B
⊢ x✝ ∈ ↑(primesOverFinset p B) ↔ x✝ ∈ p.primesOver B

Tactic:
simpa using

Goal state after:
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpb : p ≠ ⊥
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : IsDomain A
inst✝ : IsTorsionFree A B
x✝ : Ideal B
⊢ x✝ ∈ normalizedFactors (map (algebraMap A B) p) ↔ x✝ ∈ p.primesOver B
Module: Mathlib.Algebra.Module.FinitePresentation

Goal state before:
pp: R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module A N
inst✝¹ : IsScalarTower R A N
f : M →ₗ[R] N
h : IsBaseChange A f
inst✝ : Module.FinitePresentation R M
⊢ (↑h.equiv).ker.FG

Tactic:
simpa using

Goal state after:
R : Type u_2
M : Type u_4
N : Type u_3
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
A : Type u_1
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module A N
inst✝¹ : IsScalarTower R A N
f : M →ₗ[R] N
h : IsBaseChange A f
inst✝ : Module.FinitePresentation R M
⊢ ⊥.FG
Module: Mathlib.Algebra.MvPolynomial.Supported

Goal state before:
pp: case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t

Tactic:
simpa using

Goal state after:
case mp
σ : Type u_1
R : Type u
inst✝¹ : CommSemiring R
s t : Set σ
inst✝ : Nontrivial R
h : supported R s ≤ supported R t
i : σ
⊢ i ∈ s → i ∈ t
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✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
a : N
⊢ (g ∘ₗ l ∘ₗ l') a = (g ∘ₗ (s₀ • LinearMap.id)) a

Tactic:
simpa using

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✝¹ : Module.Finite R M
inst✝ : Module.FinitePresentation R N
l : M →ₗ[R] N
hf : Function.Bijective ⇑((IsLocalizedModule.map S f g) l)
e : M' ≃ₗ[R] N' := LinearEquiv.ofBijective ((IsLocalizedModule.map S f g) l) hf
l' : N →ₗ[R] M
s₀ : ↥S
H : f ∘ₗ l' = s₀ • ↑e.symm ∘ₗ g
a : N
⊢ g (l (l' a)) = s₀ • g a
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
hx_χ_neg : x_χ ∈ genWeightSpace L ⇑(-Weight.toLinear K (↥H) L α)
⊢ (-α).IsNonZero

Tactic:
simpa using

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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
hx_χ_neg : x_χ ∈ genWeightSpace L ⇑(-Weight.toLinear K (↥H) L α)
⊢ α.IsNonZero
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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
hx_χ_neg : x_χ ∈ genWeightSpace L ⇑(-Weight.toLinear K (↥H) L α)
c : K
hc : c • ⟨f, hf⟩ = ⟨x_χ, hx_χ_neg⟩
⊢ x_χ = 0 • e + c • f + 0 • ⁅e, f⁆

Tactic:
simpa using

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)
χ : Weight K (↥H) L
x_χ m_α : L
hx_χ : x_χ ∈ genWeightSpace L ⇑χ
α : Weight K (↥H) L
hαq : Weight.toLinear K (↥H) L α ∈ q
hα₀ : α.IsNonZero
hm_α : m_α ∈ genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α) ⊔ corootSubmodule α
hm_α_original : m_α ∈ sl2SubmoduleOfRoot hα₀
m_αneg : L
hm_αneg : m_αneg ∈ ↑(genWeightSpace L ⇑α ⊔ genWeightSpace L (-⇑α))
m_h : L
hm_h : m_h ∈ ↑(corootSubmodule α)
hm_eq : m_αneg + m_h = m_α
m_pos : L
hm_pos : m_pos ∈ ↑(genWeightSpace L ⇑α)
m_neg : L
hm_neg : m_neg ∈ ↑(genWeightSpace L (-⇑α))
hm_αneg_eq : m_pos + m_neg = m_αneg
hm_α_decomp : m_α = m_pos + m_neg + m_h
h_bracket_sum : ⁅x_χ, m_α⁆ = ⁅x_χ, m_pos⁆ + ⁅x_χ, m_neg⁆ + ⁅x_χ, m_h⁆
w_plus : Weight.toLinear K (↥H) L χ + Weight.toLinear K (↥H) L α = 0
h e f : L
ht : IsSl2Triple h e f
he : e ∈ rootSpace H ⇑α
hf : f ∈ rootSpace H (-⇑α)
hx_χ_neg : x_χ ∈ genWeightSpace L ⇑(-Weight.toLinear K (↥H) L α)
c : K
hc : c • ⟨f, hf⟩ = ⟨x_χ, hx_χ_neg⟩
⊢ x_χ = c • f
Module: Mathlib.Algebra.MvPolynomial.PDeriv

Goal state before:
pp: R : Type u
σ : Type v
inst✝¹ : CommSemiring R
S : Type u_1
inst✝ : CommSemiring S
φ : R →+* S
f : MvPolynomial σ R
i : σ
p q : MvPolynomial σ R
hp : (pderiv i) ((map φ) p) = (map φ) ((pderiv i) p)
hq : (pderiv i) ((map φ) q) = (map φ) ((pderiv i) q)
⊢ (pderiv i) ((map φ) (p + q)) = (map φ) ((pderiv i) (p + q))

Tactic:
by simp [hp, hq]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (d.compAEval a) f = derivative f • (AEval.of R M a) (d a)

Tactic:
simpa using

Goal state after:
R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : Module A M
inst✝¹ : Module R M
inst✝ : IsScalarTower R A M
a : A
d : Derivation R A M
f : R[X]
⊢ (AEval.of R M a) ((aeval a) (derivative f) • d a) = derivative f • (AEval.of R M a) (d a)