mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.ClassNumber

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsGalois ℚ K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∃ P ∈ (span {↑p}).primesOver (𝓞 K),
        ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
            p ^ P.inertiaDeg ℤ ∨
          Submodule.IsPrincipal P
p : ℕ
hpmem :
  p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
x✝ : P ∈ (span {↑p}).primesOver (𝓞 K)
hple :
  p ^ P.inertiaDeg ℤ ≤ ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (span {↑p})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
      p ^ Q.inertiaDeg ℤ ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (span {↑p})
⊢ Submodule.IsPrincipal P

Tactic:
have := (isPrime_of_prime (prime_span_singleton_iff.mpr (prime_iff_prime_int.mp hp))).isMaximal
    (by simp [hp.ne_zero])

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsGalois ℚ K
h :
  ∀ p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊,
    Nat.Prime p →
      ∃ P ∈ (span {↑p}).primesOver (𝓞 K),
        ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
            p ^ P.inertiaDeg ℤ ∨
          Submodule.IsPrincipal P
p : ℕ
hpmem :
  p ∈ Finset.Icc 1 ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hp : Nat.Prime p
P : Ideal (𝓞 K)
x✝ : P ∈ (span {↑p}).primesOver (𝓞 K)
hple :
  p ^ P.inertiaDeg ℤ ≤ ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊
hP1 : P.IsPrime
hP2 : P.LiesOver (span {↑p})
Q : Ideal (𝓞 K)
H :
  ⌊(4 / π) ^ nrComplexPlaces K * (↑(finrank ℚ K)! / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)⌋₊ <
      p ^ Q.inertiaDeg ℤ ∨
    Submodule.IsPrincipal Q
hQ1 : Q.IsPrime
hQ2 : Q.LiesOver (span {↑p})
this : (span {↑p}).IsMaximal
⊢ Submodule.IsPrincipal P
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) (a • y) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))

Tactic:
Algebra.smul_def,

Goal state after:
case refine_1.refine_3
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
x : K
hx : x ∈ span A (↑↑I * ↑↑J)
a : A
y : K
x✝ : y ∈ span A (↑↑I * ↑↑J)
hy : (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
⊢ (IsLocalization.map L f hf) ((algebraMap A K) a * y) ∈
    ↑(span B (⇑(IsLocalization.map L f hf) '' ↑I * ⇑(IsLocalization.map L f hf) '' ↑J))
Module: Mathlib.RingTheory.Trace.Quotient

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁶ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁵ : IsScalarTower R Rₚ Sₚ
this✝⁴ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝³ : IsDomain Sₚ
this✝² : IsTorsionFree Rₚ Sₚ
this✝¹ : Module.Finite Rₚ Sₚ
this✝ : IsIntegrallyClosed Sₚ
this : IsPrincipalIdealRing Rₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)

Tactic:
have : Module.Free Rₚ Sₚ := Module.free_of_finite_type_torsion_free'

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
p : Ideal R
inst✝⁵ : p.IsMaximal
x : S
inst✝⁴ : IsDedekindDomain R
inst✝³ : IsDomain S
inst✝² : IsTorsionFree R S
inst✝¹ : Module.Finite R S
inst✝ : IsIntegrallyClosed S
Rₚ : Type u_1 := Localization.AtPrime p
Sₚ : Type u_2 := Localization (algebraMapSubmonoid S p.primeCompl)
this✝⁷ : Algebra Rₚ Sₚ := localizationAlgebra p.primeCompl S
this✝⁶ : IsScalarTower R Rₚ Sₚ
this✝⁵ : IsLocalization (Submonoid.map (algebraMap R S) p.primeCompl) Sₚ
e : algebraMapSubmonoid S p.primeCompl ≤ S⁰
this✝⁴ : IsDomain Sₚ
this✝³ : IsTorsionFree Rₚ Sₚ
this✝² : Module.Finite Rₚ Sₚ
this✝¹ : IsIntegrallyClosed Sₚ
this✝ : IsPrincipalIdealRing Rₚ
this : Free Rₚ Sₚ
⊢ (trace (R ⧸ p) (S ⧸ pS)) ((Ideal.Quotient.mk pS) x) = (Ideal.Quotient.mk p) ((intTrace R S) x)
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
x : K
x✝ : L
hy : x✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑(spanSingleton M x))
a : A
hw : a • x ∈ ↑(spanSingleton M x)
⊢ (IsLocalization.map L f hf) (a • x) ∈ B ∙ (IsLocalization.map L f hf) x

Tactic:
Algebra.smul_def,

Goal state after:
case refine_1
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
x : K
x✝ : L
hy : x✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑(spanSingleton M x))
a : A
hw : a • x ∈ ↑(spanSingleton M x)
⊢ (IsLocalization.map L f hf) ((algebraMap A K) a * x) ∈ B ∙ (IsLocalization.map L f hf) x
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R
hP : P.IsPrime
inst✝ : IsDedekindDomain R
x : R
x_mem : x ∈ P
hxP2 : x ∉ P ^ 2
hxQ : ∀ (Q : Ideal R), Q.IsPrime → Q ≠ P → x ∉ Q
⊢ P = span {x}

Tactic:
by_cases hP0 : P = ⊥
  · subst hP0
    rwa [eq_comm, span_singleton_eq_bot, ← mem_bot]
  have hspan0 : span {x} ≠ ⊥ := mt Ideal.span_singleton_eq_bot.mp (hxP2 <| · ▸ zero_mem _)
  rw [← associated_iff_eq, associated_iff_normalizedFactors_eq_normalizedFactors hP0 hspan0]
  refine Multiset.ext' fun Q ↦ ?_
  rw [normalizedFactors_irreducible (Ideal.prime_of_isPrime hP0 hP).irreducible, normalize_eq,
    Multiset.count_singleton]
  symm
  split_ifs with hQ
  · subst hQ
    apply Ideal.count_normalizedFactors_eq <;> simpa
  by_cases hQp : IsPrime Q
  · apply Ideal.count_normalizedFactors_eq <;> simp [hxQ _ hQp hQ]
  exact Multiset.count_eq_zero.mpr fun hQi ↦
    hQp <| isPrime_of_prime <| irreducible_iff_prime.mp <| irreducible_of_normalized_factor _ hQi

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a✝ : Ideal R → A
ha✝ : ∀ M ∈ s, a✝ M ∈ I
b✝ : Ideal R → A
hb✝ : ∀ M ∈ s, b✝ M ∈ I'
hm : ∀ M ∈ s, a✝ M * b✝ M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b✝ M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
a : A
ha : a ∈ I
b : A
hb : b ∈ I'
hi : ↑I * ↑I' ≤ ↑1
⊢ ∃ c, (algebraMap R A) c = a * b

Tactic:
obtain ⟨c, -, hc⟩ := hi (Submodule.mul_mem_mul ha hb)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a✝ : Ideal R → A
ha✝ : ∀ M ∈ s, a✝ M ∈ I
b✝ : Ideal R → A
hb✝ : ∀ M ∈ s, b✝ M ∈ I'
hm : ∀ M ∈ s, a✝ M * b✝ M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b✝ M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
a : A
ha : a ∈ I
b : A
hb : b ∈ I'
hi : ↑I * ↑I' ≤ ↑1
c : R
hc : (Algebra.linearMap R A) c = a * b
⊢ ∃ c, (algebraMap R A) c = a * b
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hmem : u M • (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
hc : (algebraMap R A) c = a M * b M
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
c : R
hmem : (algebraMap R A) (u M) * (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
hc : (algebraMap R A) c = a M * b M
⊢ (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
Module: Mathlib.RingTheory.DedekindDomain.PID

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A) c = a M * b M'
⊢ u M' • (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M

Tactic:
Algebra.smul_def,

Goal state after:
case a
R : Type u_1
inst✝³ : CommRing R
A : Type u_2
inst✝² : CommRing A
inst✝¹ : Algebra R A
S : Submonoid R
inst✝ : IsLocalization S A
hS : S ≤ R⁰
hf : {I | I.IsMaximal}.Finite
I I' : FractionalIdeal S A
hinv : ↑I * ↑I' = ↑1
hinv' : I * I' = 1
s : Finset (Ideal R) := hf.toFinset
this✝ : DecidableEq (Ideal R)
coprime : ∀ M ∈ s, ∀ M' ∈ s.erase M, M ⊔ M' = ⊤
nle : ∀ M ∈ s, ¬⨅ M' ∈ s.erase M, M' ≤ M
a : Ideal R → A
ha : ∀ M ∈ s, a M ∈ I
b : Ideal R → A
hb : ∀ M ∈ s, b M ∈ I'
hm : ∀ M ∈ s, a M * b M ∉ IsLocalization.coeSubmodule A M
u : Ideal R → R
hu : ∀ M ∈ s, u M ∈ ⨅ M' ∈ s.erase M, M'
hum : ∀ M ∈ s, u M ∉ M
v : A := ∑ M ∈ s, u M • b M
hv : v ∈ I'
h : ¬Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) = ⊤
M : Ideal R
hJM : Submodule.comap (Algebra.linearMap R A) (↑↑(Units.mkOfMulEqOne I I' hinv') * (R ∙ v)) ≤ M
hM : M ∈ hf.toFinset
this : ∀ a ∈ I, ∀ b ∈ I', ∃ c, (algebraMap R A) c = a * b
hmem : u M • (a M * b M) + ∑ x ∈ s.erase M, u x • (a M * b x) ∈ IsLocalization.coeSubmodule A M
M' : Ideal R
hM' : M' ≠ M ∧ M' ∈ s
c : R
hc : (algebraMap R A) c = a M * b M'
⊢ (algebraMap R A) (u M') * (algebraMap R A) c ∈ IsLocalization.coeSubmodule A M
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝¹⁸ : CommRing R
inst✝¹⁷ : IsDomain R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : IsIntegrallyClosed R
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : IsTorsionFree R S
T : Type u_4
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain T
inst✝⁷ : IsIntegrallyClosed T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T S
inst✝⁴ : Module.Finite R T
inst✝³ : Module.Finite T S
inst✝² : IsTorsionFree R T
inst✝¹ : IsTorsionFree T S
inst✝ : IsScalarTower R T S
I : Ideal S
x : S
hx : x ∈ ↑I
⊢ (intNorm R T) ((intNorm T S) x) = (intNorm R S) x

Tactic:
intNorm_intNorm

Goal state after:
R : Type u_1
inst✝¹⁸ : CommRing R
inst✝¹⁷ : IsDomain R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : IsIntegrallyClosed R
inst✝¹³ : IsIntegrallyClosed S
inst✝¹² : Algebra R S
inst✝¹¹ : Module.Finite R S
inst✝¹⁰ : IsTorsionFree R S
T : Type u_4
inst✝⁹ : CommRing T
inst✝⁸ : IsDomain T
inst✝⁷ : IsIntegrallyClosed T
inst✝⁶ : Algebra R T
inst✝⁵ : Algebra T S
inst✝⁴ : Module.Finite R T
inst✝³ : Module.Finite T S
inst✝² : IsTorsionFree R T
inst✝¹ : IsTorsionFree T S
inst✝ : IsScalarTower R T S
I : Ideal S
x : S
hx : x ∈ ↑I
⊢ (intNorm R S) x = (intNorm R S) x
Module: Mathlib.RingTheory.DedekindDomain.LinearDisjoint

Goal state before:
pp: A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝³⁴ : CommRing A
inst✝³³ : Field K
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : CommRing B
inst✝²⁹ : Field L
inst✝²⁸ : Algebra B L
inst✝²⁷ : Algebra A L
inst✝²⁶ : Algebra K L
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝²³ : CommRing R₁
inst✝²² : CommRing R₂
inst✝²¹ : IsDomain R₁
inst✝²⁰ : Algebra A R₁
inst✝¹⁹ : Algebra A R₂
inst✝¹⁸ : Algebra R₁ B
inst✝¹⁷ : Algebra R₂ B
inst✝¹⁶ : Algebra R₁ L
inst✝¹⁵ : Algebra R₂ L
inst✝¹⁴ : IsScalarTower A R₁ L
inst✝¹³ : IsScalarTower R₁ B L
inst✝¹² : IsScalarTower R₂ B L
inst✝¹¹ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝¹⁰ : Algebra R₁ ↥F₁
inst✝⁹ : Algebra R₂ ↥F₂
inst✝⁸ : IsTorsionFree R₁ ↥F₁
inst✝⁷ : IsScalarTower A (↥F₂) L
inst✝⁶ : IsScalarTower A R₂ ↥F₂
inst✝⁵ : IsScalarTower R₁ (↥F₁) L
inst✝⁴ : IsScalarTower R₂ (↥F₂) L
inst✝³ : Algebra.IsSeparable K ↥F₂
inst✝² : Algebra.IsSeparable (↥F₁) L
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : x ∈ restrictScalars R₁ (traceDual R₁ (↥F₁) 1)
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis (Free.ChooseBasisIndex A R₂) K ↥F₂ := Basis.localizationLocalization K A⁰ (↥F₂) (Free.chooseBasis A R₂)
⊢ x ∈ span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))

Tactic:
let B₁ := h₁.basisOfBasisRight h₂' b₂

Goal state after:
A : Type u_1
B : Type u_2
K : Type u_3
L : Type u_4
inst✝³⁴ : CommRing A
inst✝³³ : Field K
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : CommRing B
inst✝²⁹ : Field L
inst✝²⁸ : Algebra B L
inst✝²⁷ : Algebra A L
inst✝²⁶ : Algebra K L
inst✝²⁵ : FiniteDimensional K L
inst✝²⁴ : IsScalarTower A K L
R₁ : Type u_5
R₂ : Type u_6
inst✝²³ : CommRing R₁
inst✝²² : CommRing R₂
inst✝²¹ : IsDomain R₁
inst✝²⁰ : Algebra A R₁
inst✝¹⁹ : Algebra A R₂
inst✝¹⁸ : Algebra R₁ B
inst✝¹⁷ : Algebra R₂ B
inst✝¹⁶ : Algebra R₁ L
inst✝¹⁵ : Algebra R₂ L
inst✝¹⁴ : IsScalarTower A R₁ L
inst✝¹³ : IsScalarTower R₁ B L
inst✝¹² : IsScalarTower R₂ B L
inst✝¹¹ : Module.Finite A R₂
F₁ F₂ : IntermediateField K L
inst✝¹⁰ : Algebra R₁ ↥F₁
inst✝⁹ : Algebra R₂ ↥F₂
inst✝⁸ : IsTorsionFree R₁ ↥F₁
inst✝⁷ : IsScalarTower A (↥F₂) L
inst✝⁶ : IsScalarTower A R₂ ↥F₂
inst✝⁵ : IsScalarTower R₁ (↥F₁) L
inst✝⁴ : IsScalarTower R₂ (↥F₂) L
inst✝³ : Algebra.IsSeparable K ↥F₂
inst✝² : Algebra.IsSeparable (↥F₁) L
inst✝¹ : Free A R₂
inst✝ : IsLocalization (algebraMapSubmonoid R₂ A⁰) ↥F₂
h₁ : F₁.LinearDisjoint ↥F₂
h₂ : F₁ ⊔ F₂ = ⊤
x : L
hx : x ∈ restrictScalars R₁ (traceDual R₁ (↥F₁) 1)
h₂' : F₁.toSubalgebra ⊔ F₂.toSubalgebra = ⊤
b₂ : Basis (Free.ChooseBasisIndex A R₂) K ↥F₂ := Basis.localizationLocalization K A⁰ (↥F₂) (Free.chooseBasis A R₂)
B₁ : Basis (Free.ChooseBasisIndex A R₂) (↥F₁) L := h₁.basisOfBasisRight h₂' b₂
⊢ x ∈ span R₁ (⇑(algebraMap (↥F₂) L) '' ↑(traceDual A K 1))
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Basic

Goal state before:
pp: p k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ k)
⊢ (algebraMap (𝓞 K) K) hζ.integralPowerBasisOfPrimePow.gen = ↑hζ.toInteger

Tactic:
rw [integralPowerBasisOfPrimePow, PowerBasis.map_gen, adjoin.powerBasis'_gen]
    simp only [adjoinEquivRingOfIntegersOfPrimePow_apply, IsIntegralClosure.algebraMap_lift]
    rfl

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → Q.coeff m = p * g m
k : ℕ
hk : k ∈ range (j + 1)
⊢ (p * g k) • B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → Q.coeff m = p * g m
k : ℕ
hk : k ∈ range (j + 1)
⊢ (algebraMap R L) (p * g k) * B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k
Module: Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral

Goal state before:
pp: R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → Q.coeff m = p * g m
k : ℕ
hk : k ∈ range (j + 1)
⊢ (algebraMap R L) (p * g k) * B.gen ^ k = (algebraMap R L) p * g k • B.gen ^ k

Tactic:
Algebra.smul_def,

Goal state after:
R : Type u
K : Type v
L : Type z
p : R
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : Algebra R K
inst✝³ : IsScalarTower R K L
inst✝² : IsDomain R
inst✝¹ : IsFractionRing R K
inst✝ : IsIntegrallyClosed R
B : PowerBasis K L
hp : _root_.Prime p
hBint : IsIntegral R B.gen
z : L
hzint : IsIntegral R z
this✝ : Module.Finite K L
P : R[X] := minpoly R B.gen
hei : P.IsEisensteinAt (R ∙ p)
hndiv : ¬p ^ 2 ∣ P.coeff 0
hP : P = minpoly R B.gen
n : ℕ
hn : B.dim = n.succ
this : Module.IsTorsionFree R L
Q₁ : R[X]
Q : R[X] := Q₁ %ₘ P
hQ₁ : Q = Q₁ %ₘ P
hQ : (aeval B.gen) Q = p • z
hQzero : ¬Q = 0
j : ℕ
hj : j + 1 ∈ range (Q.natDegree + 1)
H : j + 1 + 1 ≤ P.natDegree
Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j)
g : ℕ → R
hg : ∀ m ≤ j, m ∈ range (Q.natDegree + 1) → Q.coeff m = p * g m
k : ℕ
hk : k ∈ range (j + 1)
⊢ (algebraMap R L) (p * g k) * B.gen ^ k = (algebraMap R L) p * ((algebraMap R L) (g k) * B.gen ^ k)