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

Goal state before:
pp: ⊢ evenKernel 0 = cosKernel 0

Tactic:
ext1 x

Goal state after:
x : ℝ
⊢ evenKernel 0 x = cosKernel 0 x
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
⊢ ContinuousOn (cosKernel a) (Ioi 0)

Tactic:
by
  induction a using QuotientAddGroup.induction_on with | H a' =>
  apply continuous_re.comp_continuousOn (f := fun x ↦ (cosKernel a' x : ℂ))
  simp only [cosKernel_def]
  refine continuousOn_of_forall_continuousAt (fun x hx ↦ ?_)
  exact (continuousAt_jacobiTheta₂ a' <| by simpa).comp
    (f := fun u : ℝ ↦ ((a' : ℂ), I * u)) (by fun_prop)

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

Goal state before:
pp: a t : ℝ
ht : 0 < t
⊢ HasSum (fun n ↦ if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) (evenKernel (↑a) t - if ↑a = 0 then 1 else 0)

Tactic:
by
  have := Classical.propDecidable -- speed up instance search for `if / then / else`
  simp_rw [AddCircle.coe_eq_zero_iff, zsmul_one]
  split_ifs with h
  · obtain ⟨k, rfl⟩ := h
    simpa [← Int.cast_add, add_eq_zero_iff_eq_neg]
      using hasSum_ite_sub_hasSum (hasSum_int_evenKernel (k : ℝ) ht) (-k)
  · suffices ∀ (n : ℤ), n + a ≠ 0 by simpa [this] using hasSum_int_evenKernel a ht
    contrapose! h
    let ⟨n, hn⟩ := h
    exact ⟨-n, by simpa [neg_eq_iff_add_eq_zero]⟩

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

Goal state before:
pp: case refine_2
a : ℝ
s : ℂ
hs : 1 < s.re
hF :
  ∀ (t : ℝ),
    0 < t →
      HasSum (fun n ↦ if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)))
        ((↑(evenKernel (↑a) t) - ↑(if ↑a = 0 then 1 else 0)) / 2)
n : ℤ
⊢ s.Gammaℝ / ↑|↑n + a| ^ s / 2 = s.Gammaℝ * (1 / 2) / ↑|↑n + a| ^ s

Tactic:
· rw [mul_one_div, div_right_comm]

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

Goal state before:
pp: case inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ |a| ^ n + |b| ^ n = |c| ^ n

Tactic:
simp only [hn.pow_abs, habc]

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

Goal state before:
pp: case inl
a : UnitAddCircle
s : ℂ
hs'✝ : s ≠ 1 ∨ a ≠ 0
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (cosZeta a) s

Tactic:
exact differentiableAt_update_of_residue (fun _ ht ht' ↦
      differentiableAt_completedCosZeta a ht (Or.inl ht')) (completedCosZeta_residue_zero a) s hs'

Goal state after:
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 : ↑{p | Nat.Prime p}), (1 - ((changeLevel hMN) χ) ↑↑p * ↑↑p ^ (-s))⁻¹ =
    (∏' (p : Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) *
      ∏' (x : ℕ), (↑N.primeFactors).mulIndicator (fun p ↦ 1 - χ ↑p * ↑p ^ (-s)) x

Tactic:
tprod_subtype _ fun p : ℕ ↦ (1 - (changeLevel hMN χ) p * p ^ (-s))⁻¹,

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
⊢ ∏' (x : ℕ), {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - ((changeLevel hMN) χ) ↑p * ↑p ^ (-s))⁻¹) x =
    (∏' (p : Primes), (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) *
      ∏' (x : ℕ), (↑N.primeFactors).mulIndicator (fun p ↦ 1 - χ ↑p * ↑p ^ (-s)) x
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.refine_2
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
p : ℤ
hp : Prime p
hpa : p ∣ a
hpb : p ∣ b
⊢ p ∣ 1

Tactic:
rw [← Hgcd]
    refine Finset.dvd_gcd_iff.mpr fun x hx ↦ ?_
    simp only [Finset.mem_insert, Finset.mem_singleton] at hx
    rcases hx with hx | hx | hx <;> simp only [id_eq, hx, hpa, hpb,
      dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT hp hpa hpb HF]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
⊢ PythagoreanTriple x y z ↔ PythagoreanTriple y x z

Tactic:
delta PythagoreanTriple

Goal state after:
x y z : ℤ
⊢ x * x + y * y = z * z ↔ y * y + x * x = z * z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑(1 * (↑k).natAbs) ∣ z

Tactic:
Int.natAbs_natCast,

Goal state after:
case neg
z : ℤ
k : ℕ
x0 y0 : ℤ
left✝ : 0 < k
h2 : x0.gcd y0 = 1
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) z
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
⊢ ↑(1 * k) ∣ z
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
⊢ PythagoreanTriple (a ^ 2) (b ^ 2) c

Tactic:
delta PythagoreanTriple

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
⊢ a ^ 2 * a ^ 2 + b ^ 2 * b ^ 2 = c * c
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
⊢ PythagoreanTriple a n m

Tactic:
delta PythagoreanTriple

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
⊢ a * a + n * n = m * m
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(1 * (↑k).natAbs) * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑(1 * (↑k).natAbs)) (y0 * ↑k / ↑(1 * (↑k).natAbs))
    (↑(1 * (↑k).natAbs) * z0 / ↑(1 * (↑k).natAbs))

Tactic:
Int.natAbs_natCast,

Goal state after:
case neg
z0 : ℤ
k : ℕ
x0 y0 : ℤ
k0 : 0 < k
h2 : x0.gcd y0 = 1
h0 : ¬(x0 * ↑k).gcd (y0 * ↑k) = 0
h : PythagoreanTriple (x0 * ↑k) (y0 * ↑k) (↑(1 * k) * z0)
hk : ↑k ≠ 0
⊢ PythagoreanTriple (x0 * ↑k / ↑(1 * k)) (y0 * ↑k / ↑(1 * k)) (↑(1 * k) * z0 / ↑(1 * k))
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
⊢ (a * derivative b).degree < a.degree + b.degree

Tactic:
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

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

Goal state before:
pp: case refine_2.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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
⊢ (↑↑ψ).toFun = ⇑K.subtype

Tactic:
ext1 x

Goal state after:
case refine_2.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 = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
⊢ (↑↑ψ).toFun x = K.subtype x
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
⊢ ↑(Ideal.absNorm (num 0)) / ↑|(Algebra.norm ℤ) ↑(den 0)| = 0

Tactic:
num_zero_eq,

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
⊢ ↑(Ideal.absNorm 0) / ↑|(Algebra.norm ℤ) ↑(den 0)| = 0

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
⊢ Function.Injective ⇑(algebraMap R K)
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
delta PythagoreanTriple

Goal state after:
case mpr
x y z : ℤ
⊢ (∃ m n,
      (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
        (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)) →
    x * x + y * y = z * z ∧ x.gcd y = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mp.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := ⋯
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
⊢ φ = ψ

Tactic:
ext1 x

Goal state after:
case mp.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
x : K
⊢ φ x = ψ x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mp.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := ⋯
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
⊢ ComplexEmbedding.conjugate φ = ψ

Tactic:
ext1 x

Goal state after:
case mp.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
x : K
⊢ (ComplexEmbedding.conjugate φ) x = ψ x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk φ = mk ψ

Tactic:
· rw [← mk_conjugate_eq]
      exact congr_arg mk h

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : (mk φ).IsReal
⊢ ComplexEmbedding.IsReal φ

Tactic:
contrapose h

Goal state after:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ ¬(mk φ).IsReal
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inl.inl
k m n : ℤ
⊢ PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) (k * (m ^ 2 + n ^ 2))

Tactic:
delta PythagoreanTriple

Goal state after:
case mpr.inl.inl
k m n : ℤ
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) =
    k * (m ^ 2 + n ^ 2) * (k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inl.inr
k m n : ℤ
⊢ PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) (-k * (m ^ 2 + n ^ 2))

Tactic:
delta PythagoreanTriple

Goal state after:
case mpr.inl.inr
k m n : ℤ
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) =
    -k * (m ^ 2 + n ^ 2) * (-k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inl
k m n : ℤ
⊢ PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) (k * (m ^ 2 + n ^ 2))

Tactic:
delta PythagoreanTriple

Goal state after:
case mpr.inr.inl
k m n : ℤ
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) =
    k * (m ^ 2 + n ^ 2) * (k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inr
k m n : ℤ
⊢ PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) (-k * (m ^ 2 + n ^ 2))

Tactic:
delta PythagoreanTriple

Goal state after:
case mpr.inr.inr
k m n : ℤ
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) =
    -k * (m ^ 2 + n ^ 2) * (-k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case neg.«0»
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hi : orderOf ↑x = 0
hc : 0 ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1

Tactic:
linarith [orderOf_pos_iff.2 ((CommGroup.mem_torsion x.1).1 x.2)]

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
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra k K
inst✝² : Algebra k F
inst✝¹ : Algebra K F
inst✝ : IsScalarTower k K F
w : InfinitePlace F
h : IsUnramified k w
⊢ IsUnramified K w

Tactic:
rw [InfinitePlace.isUnramified_iff_mult_le, ← h.eq, IsScalarTower.algebraMap_eq k K F,
    InfinitePlace.comap_comp]
  exact InfinitePlace.mult_comap_le _ _

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
φ : K →+* ℂ
h : IsMixed k φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
rcases embedding_mk_eq φ with (_ | _)

Goal state after:
case inl
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
h✝ : (mk φ).embedding = φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

case inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
h✝ : (mk φ).embedding = conjugate φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ‖x‖ ≤ convexBodySumFun x

Tactic:
rw [norm_eq_sup'_normAtPlace]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ (Finset.univ.sup' ⋯ fun w ↦ (normAtPlace w) x) ≤ convexBodySumFun x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
⊢ -x ∈ convexBodySum K B

Tactic:
Set.mem_ofPred,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
x : mixedSpace K
hx : x ∈ convexBodySum K B
⊢ convexBodySumFun (-x) ≤ B
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
prod_mul_distrib,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ (∏ x, |c| ^ x.mult) * ∏ x_1, (normAtPlace x_1) x ^ x_1.mult = |c| ^ finrank ℚ K * ∏ w, (normAtPlace w) x ^ w.mult
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:
by
  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.InfinitePlace.Ramification

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
h : ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ v.embeddingConjugateIte w = w.embedding

Tactic:
by simp [embeddingConjugateIte, h]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
h : ¬ComplexEmbedding.LiesOver w.embedding v.embedding
⊢ v.embeddingConjugateIte w = conjugate w.embedding

Tactic:
by simp [embeddingConjugateIte, h]

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

Goal state before:
pp: K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
⊢ (unramifiedPlacesOver L v).ncard + 2 * (ramifiedPlacesOver L v).ncard = finrank K L

Tactic:
let : Algebra K ℂ := v.embedding.toAlgebra

Goal state after:
K : Type u_4
L : Type u_5
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
v : InfinitePlace K
inst✝¹ : NumberField K
inst✝ : NumberField L
this : Algebra K ℂ := v.embedding.toAlgebra
⊢ (unramifiedPlacesOver L v).ncard + 2 * (ramifiedPlacesOver L v).ncard = finrank K L
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: 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| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
← rpow_natCast,

Goal state after:
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| ≤ (B / ↑(finrank ℚ K)) ^ ↑(finrank ℚ K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
⊢ (normAtPlace w) ((negAt s) x) = (normAtPlace w) x

Tactic:
obtain hw | hw := isReal_or_isComplex w

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsReal
⊢ (normAtPlace w) ((negAt s) x) = (normAtPlace w) x

case inr
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ (normAtPlace w) ((negAt s) x) = (normAtPlace w) x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝ : realSpace K
h : (∀ (x : { w // w.IsReal }), x✝ ↑x = 0 x) ∧ ∀ (x : { w // w.IsComplex }), ↑(x✝ ↑x) = 0 x
w : InfinitePlace K
⊢ x✝ w = 0 w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
x✝ : realSpace K
h : (∀ (x : { w // w.IsReal }), x✝ ↑x = 0 x) ∧ ∀ (x : { w // w.IsComplex }), ↑(x✝ ↑x) = 0 x
w : InfinitePlace K
hw : w.IsReal
⊢ x✝ w = 0 w

case inr
K : Type u_1
inst✝ : Field K
x✝ : realSpace K
h : (∀ (x : { w // w.IsReal }), x✝ ↑x = 0 x) ∧ ∀ (x : { w // w.IsComplex }), ↑(x✝ ↑x) = 0 x
w : InfinitePlace K
hw : w.IsComplex
⊢ x✝ w = 0 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
⊢ (normAtPlace w) (mixedSpaceOfRealSpace x) = x w

Tactic:
simp only [mixedSpaceOfRealSpace_apply]

Goal state after:
K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
⊢ (normAtPlace w) (fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)) = x w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
⊢ (normAtPlace w) (fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)) = x w

Tactic:
obtain hw | hw := isReal_or_isComplex w

Goal state after:
case inl
K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsReal
⊢ (normAtPlace w) (fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)) = x w

case inr
K : Type u_1
inst✝ : Field K
x : realSpace K
w : InfinitePlace K
hx : 0 ≤ x w
hw : w.IsComplex
⊢ (normAtPlace w) (fun w ↦ x ↑w, fun w ↦ ↑(x ↑w)) = x w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
obtain hw | hw := isReal_or_isComplex w

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

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