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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ hurwitzZetaEven a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * cosZeta a s

Tactic:
rw [this, completedHurwitzZetaEven_one_sub, inv_Gammaℝ_one_sub hs, cosZeta,
    Function.update_of_ne (by simpa using hs 0), ← Gammaℂ]

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedCosZeta a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos (↑π * s / 2) * (completedCosZeta a s / s.Gammaℝ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case inr.e_a.e_a.e_a
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I =
    I * (cexp (2 * ↑π * I * ↑a * -↑n) - cexp (2 * ↑π * I * ↑a * ↑n))

Tactic:
mul_comm,

Goal state after:
case inr.e_a.e_a.e_a
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      ((s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) +
            (s + 1).Gammaℝ * -I * -↑(↑n).sign * cexp (2 * ↑π * I * ↑a * -↑n)) /
          ↑n ^ s /
        2)
    (completedSinZeta (↑a) s)
n : ℕ
h : n ≠ 0
⊢ I * (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) =
    I * (cexp (2 * ↑π * I * ↑a * -↑n) - cexp (2 * ↑π * I * ↑a * ↑n))
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: case inl.inl
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hap : a0 % 2 = 0
hbp : b0 % 2 = 0
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1

Tactic:
exfalso
      have h1 : 2 ∣ (Int.gcd a0 b0 : ℤ) :=
        Int.dvd_coe_gcd (Int.dvd_of_emod_eq_zero hap) (Int.dvd_of_emod_eq_zero hbp)
      rw [Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal hf)] at h1
      revert h1
      decide

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
have := (hasSum_int_sinZeta a hs).nat_add_neg

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (sinZeta (↑a) s + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ a * derivative a - derivative a * a = 0

Tactic:
mul_comm,

Goal state after:
R : Type u_1
inst✝ : CommRing R
a : R[X]
⊢ derivative a * a - derivative a * a = 0
Module: Mathlib.RingTheory.Polynomial.Radical

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ normalize p * (C (↑i + 1) * p ^ i)

Tactic:
mul_comm,

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
p : k[X]
hp : Prime p
i : ℕ
⊢ p ^ (i + 1) ∣ C (↑i + 1) * p ^ i * normalize p
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
this : primeFactors a = ∅
⊢ IsUnit a

Tactic:
primeFactors_eq_empty_iff ha

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
this : IsUnit a
⊢ IsUnit a
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ IsCoprime (C v * b ^ q) (C u * a ^ p + C v * b ^ q)

Tactic:
convert! IsCoprime.add_mul_left_right hab.symm 1 using 2

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
a b c : k[X]
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : -(C u * a ^ p + C v * b ^ q) = C w * c ^ r
hab : IsCoprime (C u * a ^ p) (C v * b ^ q)
hCu : IsUnit (C u)
hCv : IsUnit (C v)
hCw : IsUnit (C w)
⊢ C v * b ^ q = C v * b ^ q * 1
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : FractionalIdeal (𝓞 K)⁰ K
⊢ Free ℤ ↥↑I

Tactic:
refine Free.of_equiv (LinearEquiv.restrictScalars ℤ (I.equivNum ?_)).symm
  exact nonZeroDivisors.coe_ne_zero I.den

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h :
  x * (algebraMap (𝓞 K) K) ↑(a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).2 = (algebraMap (𝓞 K) K) (a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).1
⊢ ¬Ideal.absNorm (↑I).num = 0

Tactic:
Ideal.absNorm_eq_zero_iff

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h :
  x * (algebraMap (𝓞 K) K) ↑(a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).2 = (algebraMap (𝓞 K) K) (a, ⟨(algebraMap ℤ (𝓞 K)) d, ⋯⟩).1
⊢ ¬(↑I).num = ⊥
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' : Ideal.span {↑I.den} * I₀ = Ideal.span {↑a} * I.num
⊢ ↑(Ideal.absNorm (I.num * Ideal.span {↑a})) = ↑(Ideal.absNorm (I₀ * Ideal.span {↑I.den}))

Tactic:
mul_comm,

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' : Ideal.span {↑I.den} * I₀ = Ideal.span {↑a} * I.num
⊢ ↑(Ideal.absNorm (Ideal.span {↑a} * I.num)) = ↑(Ideal.absNorm (I₀ * Ideal.span {↑I.den}))
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
⊢ v₁ = v₂

Tactic:
by
  rw [← mk_embedding v₁, h, mk_conjugate_eq, mk_embedding]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
⊢ dist ((⇑ψ ∘ ⇑ι.symm) x) ((⇑ψ ∘ ⇑ι.symm) y) ≤ 1 * dist x y

Tactic:
one_mul,

Goal state after:
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
x y : ↥φ.range
⊢ dist ((⇑ψ ∘ ⇑ι.symm) x) ((⇑ψ ∘ ⇑ι.symm) y) ≤ dist x y
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr
x y z : ℤ
⊢ (∃ k m n,
      (x = k * (m ^ 2 - n ^ 2) ∧ y = k * (2 * m * n) ∨ x = k * (2 * m * n) ∧ y = k * (m ^ 2 - n ^ 2)) ∧
        (z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2))) →
    PythagoreanTriple x y z

Tactic:
· rintro ⟨k, m, n, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl | rfl⟩ <;> delta PythagoreanTriple <;> ring

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (a : InfinitePlace K), a.IsReal → a x < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      a.embedding x ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
h₁ : ∀ (a : InfinitePlace K), a.IsReal → a x < ↑(f a)
h₂ :
  ∀ (a : InfinitePlace K) (b : a.IsComplex),
    a.embedding x ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
w : InfinitePlace K
h_ne : w ≠ ↑w₀
⊢ w x < ↑(f w)

Tactic:
by_cases hw : IsReal w
    · exact norm_embedding_eq w _ ▸ h₁ w hw
    · specialize h₂ w (not_isReal_iff_isComplex.mp hw)
      rw [apply_ite (w.embedding x ∈ ·), Set.mem_ofPred_eq,
        mem_ball_zero_iff, norm_embedding_eq] at h₂
      rwa [if_neg (by exact Subtype.coe_ne_coe.1 h_ne)] at h₂

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : d ^ n * (a' ^ n + b' ^ n) = c' ^ n * d ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
mul_comm,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : (a' ^ n + b' ^ n) * d ^ n = c' ^ n * d ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
hn : 3 ≤ n
chn : ↑n ≠ 0
a b c a' b' : k[X]
d : k[X] := gcd a b
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
goal : a'.natDegree = 0 ∧ b'.natDegree = 0 ∧ c'.natDegree = 0
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
by
    simp only [natDegree_eq_zero] at goal
    obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal
    rw [← ha', ← hb', ← hc']
    rw [← ha', C_ne_zero] at ha
    rw [← hb', C_ne_zero] at hb
    rw [← hc', C_ne_zero] at hc
    exact ⟨ha.right.isUnit_C, hb.right.isUnit_C, hc.right.isUnit_C⟩

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

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
⊢ IsTotallyReal ↥E

Tactic:
let _ : Algebra E (maximalRealSubfield K) := RingHom.toAlgebra <| Subfield.inclusion h

Goal state after:
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E : Subfield K
h : E ≤ maximalRealSubfield K
x✝ : Algebra ↥E ↥(maximalRealSubfield K) := (Subfield.inclusion h).toAlgebra
⊢ IsTotallyReal ↥E
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case mpr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
r : ℝ
h✝ : 0 ≤ r
heq : ∀ (x : K), (canonicalEmbedding K) x ∈ Metric.closedBall 0 r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r
x✝ : (K →+* ℂ) → ℂ
⊢ x✝ ∈ ⇑(canonicalEmbedding K) '' {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r} →
    x✝ ∈ ↑(integerLattice K) ∩ Metric.closedBall 0 r

Tactic:
rintro ⟨x, ⟨hx1, hx2⟩, rfl⟩
      exact ⟨⟨x, ⟨⟨x, hx1⟩, rfl⟩, rfl⟩, (heq x).mpr hx2⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card { φ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2 = finrank ℚ K

Tactic:
mul_comm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card { φ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces K = finrank ℚ K
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
⊢ IsUnramified k w ↔ w.IsReal ∨ (w.comap (algebraMap k K)).IsComplex

Tactic:
by
  rw [← not_iff_not, not_isUnramified_iff, not_or,
    not_isReal_iff_isComplex, not_isComplex_iff_isReal]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ∑ x_1, 1 * (normAtPlace ↑x_1) x + ∑ x_1, ↑2 * (normAtPlace ↑x_1) x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖

Tactic:
one_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ∑ x_1, (normAtPlace ↑x_1) x + ∑ x_1, ↑2 * (normAtPlace ↑x_1) x = ∑ w, ‖x.1 w‖ + 2 * ∑ w, ‖x.2 w‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ x_1, ↑x_1.mult * |c| * (normAtPlace x_1) x = |c| * ∑ w, ↑w.mult * (normAtPlace w) x

Tactic:
mul_comm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ ∑ x_1, |c| * ↑x_1.mult * (normAtPlace x_1) x = |c| * ∑ w, ↑w.mult * (normAtPlace w) x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = {a | ∑ x, ↑x.mult * B⁻¹ * (normAtPlace x) a ≤ 1}

Tactic:
mul_comm,

Goal state after:
case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = {a | ∑ x, B⁻¹ * ↑x.mult * (normAtPlace x) a ≤ 1}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∃ a ∈ univ, (normAtPlace a) x ^ a.mult = 0) ↔ ∃ w, (normAtPlace w) x = 0

Tactic:
mem_univ,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∃ a, True ∧ (normAtPlace a) x ^ a.mult = 0) ↔ ∃ w, (normAtPlace w) x = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (∃ a, (normAtPlace a) x ^ a.mult = 0) ↔ ∃ w, (normAtPlace w) x = 0

Tactic:
pow_eq_zero_iff mult_ne_zero

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

Goal state before:
pp: case refine_1.inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
⊢ K →+* ℂ

Tactic:
| inl w =>

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 1 *
      ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
          (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I])).det =
    ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det

Tactic:
one_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
        (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I])).det =
    ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(x (↑w).embedding).re =
    (∑ x_1, if w = x_1 then 1 * x (↑x_1).embedding else 0 * x (↑x_1).embedding) +
      ∑ x_1, (0 * x (↑x_1).embedding + 0 * x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
one_mul,

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(x (↑w).embedding).re =
    (∑ x_1, if w = x_1 then x (↑x_1).embedding else 0 * x (↑x_1).embedding) +
      ∑ x_1, (0 * x (↑x_1).embedding + 0 * x (ComplexEmbedding.conjugate (↑x_1).embedding))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(x (↑w).embedding).re = (if w ∈ univ then x (↑w).embedding else 0) + ∑ x, (0 + 0)

Tactic:
mem_univ,

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(x (↑w).embedding).re = (if True then x (↑w).embedding else 0) + ∑ x, (0 + 0)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
w : { w // w.IsReal }
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) (Sum.inl w)) =
    ∑ x_1,
        fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
            (Sum.inl w) (Sum.inl x_1) *
          x (↑x_1).embedding +
      ∑ x_1,
        (fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 0)) *
            x (↑x_1).embedding +
          fromBlocks 1 0 0 ((blockDiagonal fun x ↦ !![2⁻¹, 2⁻¹; 2⁻¹ * -I, 2⁻¹ * I]).submatrix Prod.swap Prod.swap)
              (Sum.inl w) (Sum.inr (x_1, 1)) *
            x (ComplexEmbedding.conjugate (↑x_1).embedding))

Tactic:
| inl w =>

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
⊢ card (InfinitePlace K) = #{w | IsUnramified k w} + #{w | IsUnramified k w}ᶜ

Tactic:
Finset.card_add_card_compl

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
⊢ card (InfinitePlace K) = card (InfinitePlace 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) * (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹)

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)⁻¹ ≠ ∞

pp: case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
⊢ ↑(finrank ℚ K) ≠ 0

Tactic:
mul_comm,

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 = minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹ * ↑(convexBodySumFactor K)

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)⁻¹ ≠ ∞

case h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ := (minkowskiBound K I * ↑(convexBodySumFactor K)⁻¹).toReal ^ (1 / ↑(finrank ℚ K))
⊢ ↑(finrank ℚ K) ≠ 0
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 * B ^ 1)

Tactic:
one_mul,

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) * ↑(B ^ 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ finrank ℚ K = Fintype.card { φ // ComplexEmbedding.IsReal φ } + nrComplexPlaces K * 2

Tactic:
mul_comm,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : LinearIndependent ℝ (⇑(commMap K) ∘ ⇑(canonicalEmbedding.latticeBasis K))
⊢ finrank ℚ K = Fintype.card { φ // ComplexEmbedding.IsReal φ } + 2 * nrComplexPlaces 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₀.IsComplex
B : ℝ≥0
hB : minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑B
⊢ minkowskiBound K 1 < ↑(convexBodyLT'Factor K) * ↑(1 * NNReal.sqrt B ^ 2)

Tactic:
one_mul,

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) * ↑(NNReal.sqrt B ^ 2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos.refine_2
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
this : minkowskiBound K 1 < volume (convexBodyLT' K (fun w ↦ if w = w₀ then NNReal.sqrt B else 1) ⟨w₀, hw₀⟩)
a : 𝓞 K
h_nz : a ≠ 0
h_le : ∀ (w : InfinitePlace K), w ≠ ↑⟨w₀, hw₀⟩ → w ↑a < ↑(if w = w₀ then NNReal.sqrt B else 1)
h_le₀ : |(w₀.embedding ↑a).re| < 1 ∧ |(w₀.embedding ↑a).im| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ (w₀.embedding ↑a).im ^ 2 < ↑B ^ 2

Tactic:
rw [sq_lt_sq, NNReal.abs_eq, ← NNReal.sq_sqrt B]
        exact h_le₀.2

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm 1) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
⊢ ↑|(Algebra.norm ℚ) ↑a| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|

Tactic:
FractionalIdeal.absNorm_one,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : 𝓞 K
h_mem : (algebraMap (𝓞 K) K) a ∈ ↑1
h_nz : (algebraMap (𝓞 K) K) a ≠ 0
h_nm :
  ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) a)| ≤
    ↑1 * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|
⊢ ↑|(Algebra.norm ℚ) ↑a| ≤
    (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|