mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
⊢ ∃ N, ∀ n ⊇ N, dist (∏ b ∈ n, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε

Tactic:
obtain ⟨N₀, hN₀⟩ := norm_tsum_factoredNumbers_sub_tsum_lt hsum.of_norm hf₀ hε

Goal state after:
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
⊢ ∃ N, ∀ n ⊇ N, dist (∏ b ∈ n, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • P.Λ₀ s) (𝓝 0) (𝓝 (0 • P.Λ₀ 0))

pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)

pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)

Tactic:
· exact (continuous_id.smul P.differentiable_Λ₀.continuous).tendsto _

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (1 / s) • P.f₀) (𝓝[≠] 0) (𝓝 P.f₀)

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ Tendsto (fun s ↦ s • (P.ε / (↑P.k - s)) • P.g₀) (𝓝[≠] 0) (𝓝 0)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂' (z + τ) τ = cexp (-↑π * I * (τ + 2 * z)) * (jacobiTheta₂' z τ - 2 * ↑π * I * jacobiTheta₂ z τ)

Tactic:
simp_rw [jacobiTheta₂_undef _ hτ, jacobiTheta₂'_undef _ hτ, mul_zero, sub_zero, mul_zero]

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

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign (r i)) / ↑|r i| ^ s = (s + 1).Gammaℝ * (a i * ↑(r i)) / ↑|r i| ^ (s + 1)

Tactic:
h,

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ (s + 1).Gammaℝ * a i * ↑(SignType.sign 0) / ↑|0| ^ s = (s + 1).Gammaℝ * (a i * ↑0) / ↑|0| ^ (s + 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ 2 * Real.cos (2 * π * a * (↑n + 1)) * rexp (-π * (↑n + 1) ^ 2 * t)) (cosKernel (↑a) t - 1)

Tactic:
rw [← hasSum_ofReal, ofReal_sub, ofReal_one]

Goal state after:
a t : ℝ
ht : 0 < t
⊢ HasSum (fun x ↦ ↑(2 * Real.cos (2 * π * a * (↑x + 1)) * rexp (-π * (↑x + 1) ^ 2 * t))) (↑(cosKernel (↑a) t) - 1)
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ ‖a i * ↑(r i)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re

Tactic:
h,

Goal state after:
case inl
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i = 0
⊢ ‖a i * ↑0‖ / |0| ^ (s + 1).re = ‖a i‖ / |0| ^ s.re
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: case inr
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / |r i| ^ s.re
hs₁ : s ≠ 0
hs₂ : 0 < (s + 1).re
hs₃ : s + 1 ≠ 0
this :
  ∀ (i : ι) (t : ℝ),
    a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t)) = if r i = 0 then 0 else a i * ↑(r i) * ↑(rexp (-π * r i ^ 2 * t))
i : ι
h : r i ≠ 0
⊢ ‖a i * ↑(r i)‖ / |r i| ^ (s + 1).re = ‖a i‖ / |r i| ^ s.re

Tactic:
rw [add_re, one_re, rpow_add (abs_pos.mpr h), rpow_one, norm_mul, norm_real,
        Real.norm_eq_abs, ← div_div, div_right_comm, mul_div_cancel_right₀ _ (abs_ne_zero.mpr h)]

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

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ evenKernel a x - if a = 0 then 1 else 0) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ (ofReal ∘ evenKernel a) x - if a = 0 then 1 else 0) =O[atTop] fun x ↦ x ^ r

Tactic:
← isBigO_norm_left

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖evenKernel a x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ evenKernel a) x - if a = 0 then 1 else 0‖) =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ↑(ζ n)) s * L (fun n ↦ ↑(μ n)) s = 1

Tactic:
← LSeries_convolution' (LSeriesSummable_zeta_iff.mpr hs)
    (LSeriesSummable_moebius_iff.mpr hs)

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ L ((fun x ↦ ↑(ζ x)) ⍟ fun n ↦ ↑(μ n)) s = 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : oddKernel a =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ (ofReal ∘ oddKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
← isBigO_norm_left

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖oddKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ oddKernel a) x - 0‖) =O[atTop] fun x ↦ x ^ r
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : sinKernel a =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ (ofReal ∘ sinKernel a) x - 0) =O[atTop] fun x ↦ x ^ r

Tactic:
← isBigO_norm_left

Goal state after:
a : UnitAddCircle
r v : ℝ
hv : 0 < v
hv' : (fun x ↦ ‖sinKernel a x‖) =O[atTop] fun x ↦ rexp (-v * x)
⊢ (fun x ↦ ‖(ofReal ∘ sinKernel a) x - 0‖) =O[atTop] fun x ↦ x ^ r
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
n : ℤ
⊢ ‖-I * cexp (↑(2 * π * a * ↑n) * I)‖ / ‖2‖ = 1 / 2

Tactic:
RCLike.norm_ofNat,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
n : ℤ
⊢ ‖-I * cexp (↑(2 * π * a * ↑n) * I)‖ / 2 = 1 / 2
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ Tendsto (fun n ↦ ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n))

Tactic:
apply eulerProduct_completely_multiplicative <| summable_riemannZetaSummand hs

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: case pos
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
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else (1 - χ ↑p * ↑p ^ (-s))⁻¹

Tactic:
by_cases hp' : p ∣ N

Goal state after:
case pos
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
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else (1 - χ ↑p * ↑p ^ (-s))⁻¹

case neg
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
⊢ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹ =
    if p ∣ N ∧ ¬N = 0 then (1 - χ ↑p * ↑p ^ (-s))⁻¹ * (1 - χ ↑p * ↑p ^ (-s)) else (1 - χ ↑p * ↑p ^ (-s))⁻¹
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ False

Tactic:
apply Nat.not_coprime_of_dvd_of_dvd (by decide : 1 < 2) _ _ hc

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ x.natAbs

x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ y.natAbs
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
x0 : ℤ
hx2 : x = x0 * 2 + 1
y0 : ℤ
hy2 : y = y0 * 2 + 1
⊢ ∃ x0 y0, x = x0 * 2 + 1 ∧ y = y0 * 2 + 1

Tactic:
exact ⟨x0, y0, hx2, hy2⟩

Goal state after:
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
⊢ (derivative a * b).degree < a.degree + b.degree

Tactic:
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.Polynomial.Radical

Goal state before:
pp: case h1
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ : k[X]
a✝ : IsUnit x✝
⊢ divRadical x✝ ∣ derivative x✝

pp: case hpr
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p✝ : k[X]
i✝ : ℕ
a✝ : Prime p✝
⊢ divRadical (p✝ ^ i✝) ∣ derivative (p✝ ^ i✝)

pp: case hcp
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ y✝ : k[X]
a✝² : IsRelPrime x✝ y✝
a✝¹ : divRadical x✝ ∣ derivative x✝
a✝ : divRadical y✝ ∣ derivative y✝
⊢ divRadical (x✝ * y✝) ∣ derivative (x✝ * y✝)

Tactic:
· case h1 a ha =>
    exact (divRadical_isUnit ha).dvd

Goal state after:
case hpr
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p✝ : k[X]
i✝ : ℕ
a✝ : Prime p✝
⊢ divRadical (p✝ ^ i✝) ∣ derivative (p✝ ^ i✝)

case hcp
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
x✝ y✝ : k[X]
a✝² : IsRelPrime x✝ y✝
a✝¹ : divRadical x✝ ∣ derivative x✝
a✝ : divRadical y✝ ∣ derivative y✝
⊢ divRadical (x✝ * y✝) ∣ derivative (x✝ * y✝)
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case pos
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a = 0
⊢ radical a ∣ a

pp: case neg
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ radical a ∣ a

Tactic:
· rw [ha]
    apply dvd_zero

Goal state after:
case neg
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : ¬a = 0
⊢ radical a ∣ a
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : radical a = 1
ha : ¬a = 0
⊢ primeFactors (radical a) = ∅

Tactic:
h,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
h : radical a = 1
ha : ¬a = 0
⊢ primeFactors 1 = ∅
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
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : a • I.den • ↑I = a • Submodule.map (Algebra.linearMap R K) I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|

Tactic:
h,

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
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : I.den • Submodule.map (Algebra.linearMap R K) I₀ = a • Submodule.map (Algebra.linearMap R K) I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) (contract (ringChar k) a)
h : contract (ringChar k) a = 0
⊢ False

Tactic:
h,

Goal state after:
case refine_1
k : Type u_1
inst✝ : Field k
a : k[X]
ha : a ≠ 0
hda : derivative a = 0
chn0 : ringChar k ≠ 0
heq : a = (expand k (ringChar k)) 0
h : contract (ringChar k) a = 0
⊢ False
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
⊢ mk v₁.embedding = v₂

Tactic:
h,

Goal state after:
K : Type u_1
inst✝ : Field K
v₁ v₂ : InfinitePlace K
h : v₁.embedding = ComplexEmbedding.conjugate v₂.embedding
⊢ mk (ComplexEmbedding.conjugate v₂.embedding) = v₂
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ = 1
⊢ ζ ^ ↑k = 1

Tactic:
h,

Goal state after:
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ = 1
⊢ 1 ^ ↑k = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
this : nrRealPlaces K + 2 * 0 = finrank ℚ K
⊢ nrRealPlaces K = 1

Tactic:
h,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
this : nrRealPlaces K + 2 * 0 = 1
⊢ nrRealPlaces K = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_3
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsReal
⊢ w x < ↑(f w)

Tactic:
exact h₁ w (ne_of_isReal_isComplex hw w₀.prop)

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), (normAtPlace w) x = 0

Tactic:
h,

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : x = 0
⊢ ∀ (w : InfinitePlace K), (normAtPlace w) 0 = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_1
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

Tactic:
exact le_mul_of_one_le_left (normAtPlace_nonneg w x) one_le_mult

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
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ IsUnramified k w ↔ Nat.card ↥(Stab w) = 1

Tactic:
rw [isUnramified_iff_stabilizer_eq_bot, Subgroup.card_eq_one]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖) =
    (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K

Tactic:
integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (∫ (x : ℝ), rexp (-‖x‖)) ^ card { w // w.IsReal } * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖) =
    (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ 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))
⊢ minkowskiBound K I = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
← ENNReal.ofReal_pow (by positivity),

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))
⊢ minkowskiBound K I = ↑(convexBodySumFactor K) * ENNReal.ofReal (B ^ finrank ℚ K)
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) *
      ↑((∏ x ∈ Finset.univ.erase w₀, if x = w₀ then B ^ x.mult else 1) * if True then B ^ w₀.mult else 1)

Tactic:
Finset.prod_ite_eq'

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) *
      ↑((if w₀ ∈ Finset.univ.erase w₀ then B ^ w₀.mult else 1) * if True then B ^ w₀.mult else 1)
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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLT'Factor K) *
      ↑((∏ x ∈ Finset.univ.erase w₀, if x = w₀ then NNReal.sqrt B ^ x.mult else 1) *
          if True then NNReal.sqrt B ^ w₀.mult else 1)

Tactic:
Finset.prod_ite_eq'

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₀ : InfinitePlace K
hw₀ : w₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 <
    ↑(convexBodyLT'Factor K) *
      ↑((if w₀ ∈ Finset.univ.erase w₀ then NNReal.sqrt B ^ w₀.mult else 1) *
          if True then NNReal.sqrt B ^ w₀.mult else 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ volume (convexBodySum K B)
⊢ ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_of_norm_le K ↑1 h

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ volume (convexBodySum K B)
w✝ : K
h_mem : w✝ ∈ ↑1
h_nz : w✝ ≠ 0
h_bd : ↑|(Algebra.norm ℚ) w✝| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
⊢ ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : (algebraMap B L) b ∈ IntermediateField.fixedField ⊤
⊢ ∃ a, (algebraMap A B) a = b

Tactic:
h,

Goal state after:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : Algebra A K
inst✝¹⁰ : Algebra B L
inst✝⁹ : IsFractionRing A K
inst✝⁸ : IsFractionRing B L
inst✝⁷ : Algebra A B
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : IsScalarTower A B L
inst✝² : IsIntegrallyClosed A
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
h✝ : IsGalois K L
h : IntermediateField.fixedField ⊤ = ⊥
this : MulSemiringAction Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
b : B
hb : (algebraMap B L) b ∈ ⊥
⊢ ∃ a, (algebraMap A B) a = b