mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2) (hurwitzZetaEven (↑a) s)

Tactic:
refine (hasSum_nat_hurwitzZetaEven a hs).congr_fun fun n ↦ ?_
  congr 2 <;>
  rw [abs_of_nonneg (by linarith [ha.1, ha.2])] <;>
  simp

Goal state after:
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)

Tactic:
rw [completedSinZeta, (isStrong_hurwitzOddFEPair _).symm_Λ_eq]

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
hF : ∀ (t : ℝ), 0 < t → HasSum (fun n ↦ c n * ↑n * ↑(rexp (-π * ↑n ^ 2 * t))) (↑(sinKernel (↑a) t) / 2)
h_sum : Summable fun i ↦ ‖c i‖ / |↑i| ^ s.re
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2)
    (mellin (hurwitzOddFEPair ↑a).g ((s + 1) / 2) / 2)
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ ‖χ ↑p * ↑p ^ (-s)‖ ≠ ‖1‖

Tactic:
simp only [norm_mul, norm_one]

Goal state after:
M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
this✝ : ∀ (f : Primes → ℂ), ∏' (p : Primes), f p = ∏' (p : ↑{p | Nat.Prime p}), f p
p : ℕ
h : Nat.Prime p
hp' : p ∣ N
this : ¬IsUnit ↑p
⊢ ‖χ ↑p‖ * ‖↑p ^ (-s)‖ ≠ 1
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
ι : Type u_2
f : ι → M
i : ι
s : Finset ι
his : i ∉ s
ih : (↑s).Pairwise (Function.onFun IsRelPrime f) → radical (∏ i ∈ s, f i) = ∏ i ∈ s, radical (f i)
h : (insert i ↑s).Pairwise (Function.onFun IsRelPrime f)
⊢ i ∉ ↑s

Tactic:
by simpa

Goal state after:
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(basisOfFractionalIdeal K I)) ↔ x ∈ ↑↑I

Tactic:
rw [basisOfFractionalIdeal, (fractionalIdealBasis K I.1).ofIsLocalizedModule_span ℚ ℤ⁰ _]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
⊢ x ∈ (↑ℤ (↑↑I).subtype).range ↔ x ∈ ↑↑I
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
⊢ h.IsPrimitiveClassified

Tactic:
by_cases! hz : 0 < z
  · exact h.isPrimitiveClassified_of_coprime_of_pos hc hz
  have h' : PythagoreanTriple x y (-z) := by simpa [PythagoreanTriple, neg_mul_neg] using h.eq
  apply h'.isPrimitiveClassified_of_coprime_of_pos hc
  apply lt_of_le_of_ne _ (h'.ne_zero_of_coprime hc).symm
  exact le_neg.mp hz

Goal state after:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = RingHom.id ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

pp: case refine_2.inr.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

Tactic:
· left
        ext1 z
        convert! RingHom.congr_fun h z using 1
        exact (IsDenseInducing.extend_eq di hc.continuous z).symm

Goal state after:
case refine_2.inr.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ ¬(algebraMap ℤ ℚ) ((Algebra.norm ℤ) ↑I.den) = 0

Tactic:
IsFractionRing.to_map_eq_zero_iff,

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ ¬(Algebra.norm ℤ) ↑I.den = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| #{φ | mk φ = w}

Tactic:
congr; congr; ext
    rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]

Goal state after:
case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : K →+* ℂ
| x✝ = w.embedding ∨ x✝ = star w.embedding

case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ DecidablePred ?m.24
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℕ
⊢ (algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n

Tactic:
by
  rw [← map_pow, ← val_pow_eq_pow_val]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ ‖w.embedding ↑x‖
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |(w.embedding ↑x).re| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : (w.embedding ↑x).im = 0
⊢ 1 ≤ |(w.embedding ↑x).re|

Tactic:
← Complex.re_add_im (embedding w x),

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ ‖↑(w.embedding ↑x).re + ↑(w.embedding ↑x).im * Complex.I‖
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |(w.embedding ↑x).re| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : (w.embedding ↑x).im = 0
⊢ 1 ≤ |(w.embedding ↑x).re|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
n : ℕ
hn : 1 < n
⊢ 1 < v ↑n

Tactic:
by simpa

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : IsTotallyReal K
⊢ nrRealPlaces K + 2 * nrComplexPlaces K = nrRealPlaces K

Tactic:
nrComplexPlaces_eq_zero_iff.mpr h,

Goal state after:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : IsTotallyReal K
⊢ nrRealPlaces K + 2 * 0 = nrRealPlaces K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2}

pp: case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : ¬x✝¹ = w₀
⊢ Convex ℝ (ball 0 ↑(f ↑x✝¹))

Tactic:
· simp_rw [abs_lt]
    refine Convex.inter ((convex_halfSpace_re_gt _).inter (convex_halfSpace_re_lt _))
      ((convex_halfSpace_im_gt _).inter (convex_halfSpace_im_lt _))

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : ¬x✝¹ = w₀
⊢ Convex ℝ (ball 0 ↑(f ↑x✝¹))
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ((basisMatrix K).submatrix id ⇑(Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯)).det = (basisMatrix K).det ↔
    Even (nrComplexPlaces K)

Tactic:
det_permute',

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ↑↑(Equiv.Perm.sign (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯)) * (basisMatrix K).det =
      (basisMatrix K).det ↔
    Even (nrComplexPlaces K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ ∑ w, ↑w.mult * (normAtPlace w) x

Tactic:
← Finset.univ.add_sum_erase _ (Finset.mem_univ w)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
w : InfinitePlace K
x✝ : w ∈ Finset.univ
⊢ (normAtPlace w) x ≤ ↑w.mult * (normAtPlace w) x + ∑ x_1 ∈ Finset.univ.erase w, ↑x_1.mult * (normAtPlace x_1) x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ ∀ ⦃x : Gal(K/k)⦄, x ∈ Stab (mk w.embedding) → x ∈ ⊥

Tactic:
simp only [mem_stabilizer_mk_iff, Subgroup.mem_bot, forall_eq_or_imp, true_and]

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
⊢ ∀ (a : Gal(K/k)), ComplexEmbedding.IsConj w.embedding a → a = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ #(MulAction.orbit Gal(K/k) w).toFinset = Nat.card Gal(K/k)

Tactic:
rw [Nat.card_eq_fintype_card,
        ← MulAction.card_orbit_mul_card_stabilizer_eq_card_group _ w,
        ← Nat.card_eq_fintype_card (α := Stab w), card_stabilizer, if_pos,
        mul_one, Set.toFinset_card]

Goal state after:
case hc
k : Type u_1
inst✝⁵ : Field k
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ IsUnramified k w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑|(Algebra.norm ℚ) a| ^ (∑ x, ↑x.mult)⁻¹ ≤ (∏ i, ↑i a ^ ↑i.mult) ^ (∑ i, ↑i.mult)⁻¹

Tactic:
simp_rw [← prod_eq_abs_norm, rpow_natCast]

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ (∏ w, w a ^ w.mult) ^ (∑ x, ↑x.mult)⁻¹ ≤ (∏ x, ↑x a ^ x.mult) ^ (∑ i, ↑i.mult)⁻¹
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝² : IsIntegralClosure B A L
this✝¹ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this : Algebra Aₘ K := f.toAlgebra
⊢ algebraMap A K = f.comp (algebraMap A Aₘ)

Tactic:
IsLocalization.map_comp,

Goal state after:
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝² : IsIntegralClosure B A L
this✝¹ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this : Algebra Aₘ K := f.toAlgebra
⊢ algebraMap A K = (algebraMap A K).comp (RingHom.id A)
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁵ : IsIntegralClosure B A L
this✝⁴ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝³ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝² : Algebra Aₘ K := f.toAlgebra
this✝¹ : IsScalarTower A Aₘ K
this✝ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this : Algebra Bₘ L := g.toAlgebra
⊢ algebraMap B L = g.comp (algebraMap B Bₘ)

Tactic:
IsLocalization.map_comp,

Goal state after:
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁵ : IsIntegralClosure B A L
this✝⁴ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝³ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝² : Algebra Aₘ K := f.toAlgebra
this✝¹ : IsScalarTower A Aₘ K
this✝ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this : Algebra Bₘ L := g.toAlgebra
⊢ algebraMap B L = (algebraMap B L).comp (RingHom.id B)
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁸ : IsIntegralClosure B A L
this✝⁷ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝⁶ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝⁵ : Algebra Aₘ K := f.toAlgebra
this✝⁴ : IsScalarTower A Aₘ K
this✝³ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝² : Algebra Bₘ L := g.toAlgebra
this✝¹ : IsScalarTower B Bₘ L
this✝ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Aₘ K L
⊢ (algebraMap K L).comp (f.comp (algebraMap A Aₘ)) = g.comp ((algebraMap B Bₘ).comp (algebraMap A B))

Tactic:
IsLocalization.map_comp,

Goal state after:
A : Type u_1
B : Type u_6
inst✝²⁴ : CommRing A
inst✝²³ : CommRing B
inst✝²² : Algebra A B
Aₘ : Type u_9
Bₘ : Type u_10
inst✝²¹ : CommRing Aₘ
inst✝²⁰ : CommRing Bₘ
inst✝¹⁹ : Algebra Aₘ Bₘ
inst✝¹⁸ : Algebra A Aₘ
inst✝¹⁷ : Algebra B Bₘ
inst✝¹⁶ : Algebra A Bₘ
inst✝¹⁵ : IsScalarTower A Aₘ Bₘ
inst✝¹⁴ : IsScalarTower A B Bₘ
M : Submonoid A
inst✝¹³ : IsLocalization M Aₘ
inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ
inst✝¹¹ : IsDomain A
inst✝¹⁰ : IsIntegrallyClosed A
inst✝⁹ : IsDomain B
inst✝⁸ : IsIntegrallyClosed B
inst✝⁷ : Module.Finite A B
inst✝⁶ : IsTorsionFree A B
inst✝⁵ : IsDomain Aₘ
inst✝⁴ : IsIntegrallyClosed Aₘ
inst✝³ : IsDomain Bₘ
inst✝² : IsIntegrallyClosed Bₘ
inst✝¹ : IsTorsionFree Aₘ Bₘ
inst✝ : Module.Finite Aₘ Bₘ
x : B
hM : M ≤ A⁰
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
this✝⁸ : IsIntegralClosure B A L
this✝⁷ : Algebra.IsAlgebraic (FractionRing A) (FractionRing B)
this✝⁶ : IsLocalization (algebraMapSubmonoid B A⁰) L
f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM
this✝⁵ : Algebra Aₘ K := f.toAlgebra
this✝⁴ : IsScalarTower A Aₘ K
this✝³ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K
g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯
this✝² : Algebra Bₘ L := g.toAlgebra
this✝¹ : IsScalarTower B Bₘ L
this✝ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra
this : IsScalarTower Aₘ K L
⊢ (algebraMap K L).comp ((algebraMap A K).comp (RingHom.id A)) = g.comp ((algebraMap B Bₘ).comp (algebraMap A B))