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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Tactic:
convert! hasSum_mellin_pi_mul hp' hs hF ?_ using 2 with i

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
i : ι
⊢ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s = ↑π ^ (-s) * Complex.Gamma s * a' i / ↑(p i) ^ s

ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
a' : ι → ℂ := fun i ↦ if p i = 0 then 0 else a i
hp' : ∀ (i : ι), a' i = 0 ∨ 0 < p i
this : ∀ (i : ι) (t : ℝ), (if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) = a' i * ↑(rexp (-π * p i * t))
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a' i * ↑(rexp (-π * p i * t))) (F t)
⊢ Summable fun i ↦ ‖a' i‖ / p i ^ s.re
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ ContinuousAt (fun p ↦ jacobiTheta₂' p.1 p.2) (z, τ)

Tactic:
obtain ⟨T, hT, hτ'⟩ := exists_between hτ
  obtain ⟨S, hz⟩ := exists_gt |im z|
  let V := {u | |im u| < S} ×ˢ {v | T < im v}
  have hVo : IsOpen V := ((_root_.continuous_abs.comp continuous_im).isOpen_preimage _
    isOpen_Iio).prod (continuous_im.isOpen_preimage _ isOpen_Ioi)
  refine ContinuousOn.continuousAt ?_ (hVo.mem_nhds ⟨hz, hτ'⟩)
  let u (n : ℤ) : ℝ := 2 * π * |n| * rexp (-π * (T * n ^ 2 - 2 * S * |n|))
  have hu : Summable u := by simpa only [u, mul_assoc, pow_one]
      using (summable_pow_mul_jacobiTheta₂_term_bound S hT 1).mul_left (2 * π)
  refine continuousOn_tsum (fun n ↦ ?_) hu (fun n ⟨z', τ'⟩ ⟨hz', hτ'⟩ ↦ ?_)
  · apply Continuous.continuousOn
    unfold jacobiTheta₂'_term jacobiTheta₂_term
    fun_prop
  · exact norm_jacobiTheta₂'_term_le hT (le_of_lt hz') (le_of_lt hτ') n

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

Goal state before:
pp: x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 * ↑x / I = I * ↑x

Tactic:
div_eq_mul_inv,

Goal state after:
x : ℝ
hx : 0 < x
a : ℝ
⊢ -1 * ↑x * I⁻¹ = I * ↑x
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < (-1 / τ).im

Tactic:
div_eq_mul_inv,

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
⊢ 0 < (-1 * τ⁻¹).im
Module: Mathlib.NumberTheory.LSeries.RiemannZeta

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / ↑n ^ s

Tactic:
simpa only [QuotientAddGroup.mk_zero, cosZeta_zero, mul_zero, zero_mul, Real.cos_zero,
    ofReal_one] using (hasSum_nat_cosZeta 0 hs).tsum_eq.symm

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
n : ℕ
⊢ ‖((fun n ↦ χ ↑n) * f) n‖ ≤ ‖f n‖

Tactic:
simpa using mul_le_of_le_one_left (norm_nonneg <| f n) <| χ.norm_le_one n

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s ↦ completedHurwitzZetaEven a s / s.Gammaℝ) 0 ((if a = 0 then -1 else 0) / 2)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s

Tactic:
div_eq_mul_inv,

Goal state after:
a : UnitAddCircle
s : ℂ
hs' : s ≠ 1
this :
  DifferentiableAt ℂ
    (Function.update (fun s ↦ completedHurwitzZetaEven a s * s.Gammaℝ⁻¹) 0 ((if a = 0 then -1 else 0) * 2⁻¹)) s
⊢ DifferentiableAt ℂ (hurwitzZetaEven a) s
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : ⋯.IsPrimitiveClassified
⊢ h.IsClassified

Tactic:
convert!
    h.normalize.mul_isClassified (Int.gcd x y)
      (isClassified_of_isPrimitiveClassified h.normalize hc) <;>
    rw [Int.mul_ediv_cancel']
  · exact Int.gcd_dvd_left ..
  · exact Int.gcd_dvd_right ..
  · exact h.gcd_dvd

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin (↑π * s / 2) * sinZeta a s

Tactic:
div_eq_mul_inv,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedHurwitzZetaOdd a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin (↑π * s / 2) * sinZeta a s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a (1 - s) / (2 - s).Gammaℝ = s.Gammaℂ * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s

Tactic:
div_eq_mul_inv,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ completedSinZeta a (1 - s) * (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R[X]
ha : a ≠ 0
hb : b ≠ 0
⊢ max (a * derivative b).degree (derivative a * b).degree < a.degree + b.degree

Tactic:
rw [max_lt_iff]
      constructor
      case left =>
        apply lt_of_le_of_lt
        · exact degree_mul_le a (derivative b)
        · rw [← Polynomial.degree_ne_bot] at ha
          rw [WithBot.add_lt_add_iff_left ha]
          exact Polynomial.degree_derivative_lt hb
      case right =>
        apply lt_of_le_of_lt
        · exact degree_mul_le (derivative a) b
        · rw [← Polynomial.degree_ne_bot] at hb
          rw [WithBot.add_lt_add_iff_right hb]
          exact Polynomial.degree_derivative_lt ha

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
⊢ (∃ n, a ∣ b ^ n) ↔ radical a ∣ b

Tactic:
by
  rcases eq_or_ne b 0 with (rfl | hb)
  · exact ⟨by simp, fun _ ↦ ⟨1, by simp⟩⟩
  refine ⟨fun ⟨n, hdvd⟩ ↦ ?_, fun h ↦ ⟨normalizedFactors a |>.card, ?_⟩⟩
  · rcases eq_or_ne n 0 with (rfl | hn)
    · simp [radical_of_isUnit <| isUnit_of_dvd_one <| pow_zero b ▸ hdvd]
    grw [radical_dvd_radical hdvd <| pow_ne_zero _ hb, radical_pow b hn, radical_dvd_self]
  · classical
    rwa [dvd_iff_normalizedFactors_le_normalizedFactors ha <| pow_ne_zero _ hb,
      normalizedFactors_pow, Multiset.le_card_smul_iff_subset, ← Multiset.toFinset_subset,
      toFinset_normalizedFactors, toFinset_normalizedFactors,
      ← radical_dvd_iff_primeFactors_subset hb]

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
hc : IsRelPrime a b
⊢ (primeFactors (a * b)).prod id = (primeFactors a).prod id * (primeFactors b).prod id

Tactic:
rw [primeFactors_mul_eq_disjUnion hc, Finset.prod_disjUnion (disjoint_primeFactors hc)]

Goal state after:
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree + 1 ≤ (a * b * c).natDegree
hqb : q * b.natDegree + 1 ≤ (a * b * c).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
have hrc := hrc'.trans natDegree_radical_le

Goal state after:
case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
hpa' : p * a.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hqb' : q * b.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hrc' : r * c.natDegree + 1 ≤ (radical (a * b * c)).natDegree
hpa : p * a.natDegree + 1 ≤ (a * b * c).natDegree
hqb : q * b.natDegree + 1 ≤ (a * b * c).natDegree
hrc : r * c.natDegree + 1 ≤ (a * b * c).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
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✝ : Module.Finite ℚ K
x : K
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|

Tactic:
have : IsDomain K := IsFractionRing.isDomain R

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✝ : Module.Finite ℚ K
x : K
this : IsDomain K
⊢ absNorm (spanSingleton R⁰ x) = |(Algebra.norm ℚ) x|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
⊢ ‖(embedding_of_isReal hw) x‖ = ‖↑((embedding_of_isReal hw) x)‖

Tactic:
Complex.norm_real

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
hw : w.IsReal
x : K
⊢ ‖(embedding_of_isReal hw) x‖ = ‖(embedding_of_isReal hw) x‖
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).re‖
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.norm_real

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‖
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
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : (f ζ).im = 0
⊢ False

Tactic:
have hre : (f ζ).re = 1 ∨ (f ζ).re = -1 := by
    rw [← Complex.abs_re_eq_norm] at him
    have := Complex.norm_eq_one_of_pow_eq_one hζ'.pow_eq_one (by lia)
    rwa [← him, ← abs_one, abs_eq_abs] at this

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : (f ζ).im = 0
hre : (f ζ).re = 1 ∨ (f ζ).re = -1
⊢ False
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
v : InfinitePlace ℚ
⊢ Rat.infinitePlace.IsReal

Tactic:
exact Rat.isReal_infinitePlace

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Nontrivial (mixedSpace K)

Tactic:
by
  obtain ⟨w⟩ := (inferInstance : Nonempty (InfinitePlace K))
  obtain hw | hw := w.isReal_or_isComplex
  · have : Nonempty {w : InfinitePlace K // IsReal w} := ⟨⟨w, hw⟩⟩
    exact nontrivial_prod_left
  · have : Nonempty {w : InfinitePlace K // IsComplex w} := ⟨⟨w, hw⟩⟩
    exact nontrivial_prod_right

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

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : 0 < discr K
⊢ (discr K).sign = (-1) ^ nrComplexPlaces K

pp: case inr.inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : 0 = discr K
⊢ (discr K).sign = (-1) ^ nrComplexPlaces K

pp: case inr.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : discr K < 0
⊢ (discr K).sign = (-1) ^ nrComplexPlaces K

Tactic:
· rw [Int.sign_eq_one_of_pos h, Even.neg_one_pow (this.mp <| Int.cast_nonneg h.le)]

Goal state after:
case inr.inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : 0 = discr K
⊢ (discr K).sign = (-1) ^ nrComplexPlaces K

case inr.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : discr K < 0
⊢ (discr K).sign = (-1) ^ nrComplexPlaces K
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : discr K < 0
⊢ (discr K).sign = (-1) ^ nrComplexPlaces K

Tactic:
rw [Int.sign_eq_neg_one_of_neg h, Odd.neg_one_pow]

Goal state after:
case inr.inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : 0 ≤ ↑(discr K) ↔ Even (nrComplexPlaces K)
h : discr K < 0
⊢ Odd (nrComplexPlaces K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
⊢ mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u)) = 1

Tactic:
rw [norm_eq_norm, Units.norm, Rat.cast_one]

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

Goal state before:
pp: case isFalse
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
w : InfinitePlace K
inst✝ : IsGalois k K
h✝ : ¬IsUnramified k w
⊢ Nat.card ↥(Stab w) = 2

Tactic:
· rwa [← not_isUnramified_iff_card_stabilizer_eq_two]

Goal state after:
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)
⊢ #({a ∉ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) =
    Nat.card Gal(K/k) / 2

Tactic:
trans Finset.card (MulAction.orbit Gal(K/k) w).toFinset

Goal state after:
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)
⊢ #({a ∉ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w}) =
    #(MulAction.orbit Gal(K/k) w).toFinset

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) / 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑(1 * if True then B ^ if w₀.IsReal then 1 else 2 else 1)

Tactic:
hw₀,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsReal
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑(1 * if True then B ^ if True then 1 else 2 else 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (ChooseBasisIndex ℤ (𝓞 K)) ℝ (mixedSpace K)

Tactic:
classical
    -- We construct an `ℝ`-linear independent family from the image of
    -- `canonicalEmbedding.lattice_basis` by `commMap`
    have := LinearIndependent.map (LinearIndependent.restrict_scalars
      (by { simpa only [Complex.real_smul, mul_one] using Complex.ofReal_injective })
      (canonicalEmbedding.latticeBasis K).linearIndependent)
      (disjoint_span_commMap_ker K)
    -- and it's a basis since it has the right cardinality
    refine basisOfLinearIndependentOfCardEqFinrank this ?_
    rw [← finrank_eq_card_chooseBasisIndex, RingOfIntegers.rank, finrank_prod, finrank_pi,
      finrank_pi_fintype, Complex.finrank_real_complex, sum_const, card_univ, ← nrRealPlaces,
      ← nrComplexPlaces, ← card_real_embeddings, smul_eq_mul, mul_comm,
      ← card_complex_embeddings, ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
      Nat.add_sub_of_le (Fintype.card_subtype_le _)]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (↑(finrank ℚ K).factorial / (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K)) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
div_eq_mul_inv,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (↑(finrank ℚ K).factorial * (2 ^ nrRealPlaces K * (π * 2⁻¹) ^ nrComplexPlaces K)⁻¹) =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
h_le : minkowskiBound K I ≤ volume (convexBodySum K B)
x✝ : K
⊢ ↑(FractionalIdeal.absNorm ↑I) * 2⁻¹ ^ nrComplexPlaces K * ↑(sqrt ‖discr K‖₊) * 2 ^ finrank ℚ K *
      (2 ^ nrRealPlaces K * (π / 2) ^ nrComplexPlaces K / ↑(finrank ℚ K).factorial)⁻¹ =
    ↑(FractionalIdeal.absNorm ↑I) *
            2 ^ (↑(finrank ℚ K) - ↑(nrComplexPlaces K) - ↑(nrRealPlaces K) + ↑(nrComplexPlaces K)) *
          √‖discr K‖ *
        ↑(finrank ℚ K).factorial *
      π⁻¹ ^ nrComplexPlaces K

Tactic:
by
      simp_rw [inv_div, div_eq_mul_inv, mul_inv, ← zpow_neg_one, ← zpow_natCast, mul_zpow,
        ← zpow_mul, neg_one_mul, mul_neg_one, neg_neg, Real.coe_sqrt, coe_nnnorm, sub_eq_add_neg,
        zpow_add₀ (two_ne_zero : (2 : ℝ) ≠ 0)]
      ring

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
x : realSpace K
hx : ∀ (w : InfinitePlace K), w.IsComplex → 0 ≤ x w
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtComplexPlaces (mixedSpaceOfRealSpace x) w = x w

Tactic:
· rw [normAtComplexPlaces_apply_isComplex ⟨w, hw⟩, mixedSpaceOfRealSpace_apply,
      Complex.norm_of_nonneg (hx w hw)]

Goal state after:
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: case neg
A : Type u_1
B : Type u_6
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
inst✝⁶ : Algebra A B
inst✝⁵ : IsDomain A
inst✝⁴ : IsIntegrallyClosed A
inst✝³ : IsDomain B
inst✝² : IsIntegrallyClosed B
inst✝¹ : Module.Finite A B
inst✝ : IsTorsionFree A B
x : B
this : FiniteDimensional (FractionRing A) (FractionRing B)
hx : ¬x = 0
K : Type u_1 := FractionRing A
L : Type u_6 := FractionRing B
E : Type u_6 := AlgebraicClosure L
⊢ (algebraMap B E) x ∈ (minpoly K ((algebraMap B L) x)).aroots E

Tactic:
· simp only [mem_roots', ne_eq, Polynomial.map_eq_zero, IsRoot.def, eval_map_algebraMap]
    refine ⟨minpoly.ne_zero (IsIntegral.isIntegral _), ?_⟩
    simp [algebraMap_apply B L E, aeval_algebraMap_apply]

Goal state after: