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

Goal state before:
pp: s : ℂ
n✝ : ℕ
χ : DirichletCharacter ℂ n✝
hs : s ≠ 0
m n : ℕ
⊢ χ ↑(m * n) * ↑↑(m * n) ^ (-s) = χ ↑m * ↑↑m ^ (-s) * (χ ↑n * ↑↑n ^ (-s))

Tactic:
simpa using

Goal state after:
s : ℂ
n✝ : ℕ
χ : DirichletCharacter ℂ n✝
hs : s ≠ 0
m n : ℕ
⊢ χ ↑m * χ ↑n * (↑↑m ^ (-s) * ↑↑n ^ (-s)) = χ ↑m * ↑↑m ^ (-s) * (χ ↑n * ↑↑n ^ (-s))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ a ≠ 0 ∨ 1 - s ≠ 0

Tactic:
simpa using

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
⊢ ¬a = 0 ∨ ¬1 = s
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ℝ⁻¹
⊢ s ≠ 0

Tactic:
simpa using

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ℝ⁻¹
⊢ ¬s = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: case h
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ 1 - s ≠ 0

Tactic:
simpa using

Goal state after:
case h
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ ¬1 = s
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ normalize ({A, B, C}.gcd id) = 1

Tactic:
normalize_eq_one

Goal state after:
n : ℕ
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : DecidableEq R
inst✝ : NormalizedGCDMonoid R
hn : ∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n
a b c : R
s : Finset R := {a, b, c}
d : R := s.gcd id
A : R
hA : a = d * A
B : R
hB : b = d * B
C : R
hC : c = d * C
ha : d ≠ 0 ∧ A ≠ 0
hb : d ≠ 0 ∧ B ≠ 0
hc : d ≠ 0 ∧ C ≠ 0
habc : A ^ n + B ^ n = C ^ n
⊢ IsUnit ({A, B, C}.gcd id)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
n : ℕ
⊢ s ≠ -↑n

Tactic:
simpa using

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
n : ℕ
⊢ ¬s = -↑n
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ s ≠ 0

Tactic:
simpa using

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ ¬s = 0
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: z : ℤ
⊢ ¬↑(z * z) = ↑2

Tactic:
simpa using

Goal state after:
z : ℤ
⊢ ¬↑z * ↑z = 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ z = 0

Tactic:
simpa using

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
⊢ z = 0
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: r s : ℤ
h : IsCoprime r s
⊢ IsCoprime (s ^ 2 + r ^ 2) s

Tactic:
apply Int.isCoprime_of_sq_sum h

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ PythagoreanTriple (x / ↑(x.gcd y)) (y / ↑(x.gcd y)) (z / ↑(x.gcd y))

Tactic:
simpa using

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
hx : x = 0
hy : y = 0
hz : z = 0
⊢ PythagoreanTriple 0 0 0
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x : K
⊢ ¬1 = -1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x : K
⊢ ¬1 + 1 = 0
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hpow_le : ∀ (p : Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ < 1
f : ℕ → ℂ := fun n ↦ χ ↑n * ↑(Λ n) / ↑(Real.log ↑n) * ↑n ^ (-s)
⊢ ∑' (p : Primes) (k : ℕ),
      χ (↑↑p ^ (k + 1)) * ↑(↑p ^ (k + 1)) ^ (-s) * ↑(Λ (↑p ^ (k + 1))) / ↑(Real.log (↑↑p ^ (k + 1))) =
    ∑' (n : { n // IsPrimePow n }), f ↑n

Tactic:
by
      rw [← tsum_primes_pow_eq]
      · exact tsum_congr fun p ↦ tsum_congr fun k ↦ (by unfold f; simp; ring)
      · apply comp_injective _ Subtype.coe_injective (f := f)
        apply of_norm_bounded_eventually_nat (g := (↑· ^ (-s.re)))
        · simp [hs]
        · filter_upwards [eventually_gt_atTop 1] with n hn
          simp only [f, norm_mul, norm_div, norm_real, norm_eq_abs]
          grw [norm_le_one, vonMangoldt_le_log]
          have := log_pos (x := n) (mod_cast hn)
          field_simp
          rw [← ofReal_natCast n, norm_cpow_eq_rpow_re_of_nonneg (by simp) (by simp; grind)]
          simp

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
⊢ False

Tactic:
have h2n : (p : ℤ) ∣ 2 * n ^ 2 := by
    convert! dvd_sub hp2 hp1 using 1
    ring

Goal state after:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 0
hn : n % 2 = 1
H : ¬(m ^ 2 - n ^ 2).gcd (m ^ 2 + n ^ 2) = 1
p : ℕ
hp : Nat.Prime p
hp1 : ↑p ∣ m ^ 2 - n ^ 2
hp2 : ↑p ∣ m ^ 2 + n ^ 2
h2m : ↑p ∣ 2 * m ^ 2
h2n : ↑p ∣ 2 * n ^ 2
⊢ False
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℝ
hs : 1 < s
⊢ 1 < (↑s).re

Tactic:
simpa using

Goal state after:
s : ℝ
hs : 1 < s
⊢ 1 < s
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : Prime a
n : ℕ
hn : n ≠ 0
⊢ radical a = normalize a

Tactic:
exact radical_of_prime 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 : Irreducible a
hb : b ≠ 0
ha' : a ∣ b
c : M
hc : c ∈ normalizedFactors b
hc' : Associated a c
⊢ c ∈ primeFactors b

Tactic:
simpa using

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : Irreducible a
hb : b ≠ 0
ha' : a ∣ b
c : M
hc : c ∈ normalizedFactors b
hc' : Associated a c
⊢ c ∈ normalizedFactors b
Module: Mathlib.NumberTheory.FLT.MasonStothers

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : b + c + a = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
⊢ w = c.wronskian a

Tactic:
simpa using

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
hsum : b + c + a = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
⊢ w = c.wronskian a
Module: Mathlib.NumberTheory.NumberField.FractionalIdeal

Goal state before:
pp: case e_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
x✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ ((basisOfFractionalIdeal K I).reindex e.symm) x✝ = (Subtype.val ∘ ⇑((fractionalIdealBasis K ↑I).reindex e.symm)) x✝

Tactic:
simpa using

Goal state after:
case e_6
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
e : Free.ChooseBasisIndex ℤ (𝓞 K) ≃ Free.ChooseBasisIndex ℤ ↥↑↑I
x✝ : Free.ChooseBasisIndex ℤ (𝓞 K)
⊢ (basisOfFractionalIdeal K I) (e x✝) = ↑((fractionalIdealBasis K ↑I) (e x✝))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
⊢ PythagoreanTriple x y (-z)

Tactic:
simpa using

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
⊢ x * x + y * y = z * z
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl
z m n : ℤ
h : PythagoreanTriple (m ^ 2 - n ^ 2) (2 * m * n) z ∧ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
this : z ^ 2 = (m ^ 2 + n ^ 2) ^ 2
⊢ z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)

Tactic:
simpa using

Goal state after:
case h.inl
z m n : ℤ
h : PythagoreanTriple (m ^ 2 - n ^ 2) (2 * m * n) z ∧ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
this : z ^ 2 = (m ^ 2 + n ^ 2) ^ 2
⊢ z = m ^ 2 + n ^ 2 ∨ z = -n ^ 2 + -m ^ 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inr
z m n : ℤ
h : PythagoreanTriple (2 * m * n) (m ^ 2 - n ^ 2) z ∧ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
this : z ^ 2 = (m ^ 2 + n ^ 2) ^ 2
⊢ z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)

Tactic:
simpa using

Goal state after:
case h.inr
z m n : ℤ
h : PythagoreanTriple (2 * m * n) (m ^ 2 - n ^ 2) z ∧ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
this : z ^ 2 = (m ^ 2 + n ^ 2) ^ 2
⊢ z = m ^ 2 + n ^ 2 ∨ z = -n ^ 2 + -m ^ 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x✝¹ x✝ : InfinitePlace K
h : x✝¹.embedding = x✝.embedding
⊢ x✝¹ = x✝

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
x✝¹ x✝ : InfinitePlace K
h : x✝¹.embedding = x✝.embedding
⊢ x✝¹ = x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w, w x ^ w.mult = ‖∏ σ, σ x‖

pp: case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|(Algebra.norm ℚ) x| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) x)‖

Tactic:
· rw [norm_prod, ← Fintype.prod_equiv (RingHom.equivRatAlgHom K ℂ) (fun f => ‖f x‖)
      (fun φ => ‖φ x‖) fun _ => by simp [RingHom.equivRatAlgHom_apply]]
    rw [← Finset.prod_fiberwise Finset.univ mk (fun φ => ‖φ x‖)]
    have (w : InfinitePlace K) (φ) (hφ : φ ∈ ({φ | mk φ = w} : Finset _)) :
        ‖φ x‖ = w x := by rw [← (Finset.mem_filter.mp hφ).2, apply]
    simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]

Goal state after:
case e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|(Algebra.norm ℚ) x| = ‖(algebraMap ℚ ℂ) ((Algebra.norm ℚ) x)‖
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ ∑ w, ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (𝓞 K)ˣ
⊢ ∑ w, ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑x)) = 0
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
this : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Tactic:
simpa using

Goal state after:
case h.inl
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) z
this : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -(k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inr
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
this : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -k * (m ^ 2 + n ^ 2)

Tactic:
simpa using

Goal state after:
case h.inr
z k m n : ℤ
right✝ : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) z
this : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2
⊢ z = k * (m ^ 2 + n ^ 2) ∨ z = -(k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ ζ ∈ CommGroup.torsion (𝓞 K)ˣ

Tactic:
rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ^ torsionOrder K = 1
⊢ ∃ n, 0 < n ∧ ζ ^ n = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : ℚ
val✝ : AbsoluteValue K ℝ
property✝ : ∃ φ, place φ = val✝
⊢ ⟨val✝, property✝⟩ ↑x = ‖x‖

Tactic:
aesop (add simp [coe_apply])

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x : ℚ
⊢ v ↑x = ‖x‖

Tactic:
rcases v with ⟨_, _⟩
  aesop (add simp [coe_apply])

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
n : ℕ
val✝ : AbsoluteValue K ℝ
property✝ : ∃ φ, place φ = val✝
⊢ ⟨val✝, property✝⟩ ↑n = ↑n

Tactic:
aesop (add simp [coe_apply])

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

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

Tactic:
rcases v with ⟨_, _⟩
  aesop (add simp [coe_apply])

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
z : ℤ
val✝ : AbsoluteValue K ℝ
property✝ : ∃ φ, place φ = val✝
⊢ ⟨val✝, property✝⟩ ↑z = ‖z‖

Tactic:
aesop (add simp [coe_apply])

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
z : ℤ
⊢ v ↑z = ‖z‖

Tactic:
rcases v with ⟨_, _⟩
  aesop (add simp [coe_apply])

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
t : ℝ
h : (fun x ↦ w x) ^ t = ⇑v
n : ℕ
hn : 1 < n
⊢ ↑n ^ t = ↑n ^ 1

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
t : ℝ
h : (fun x ↦ w x) ^ t = ⇑v
n : ℕ
hn : 1 < n
⊢ ↑n ^ t = ↑n
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
h✝ : (↑w).IsEquiv ↑v
t : ℝ
left✝ : 0 < t
h : (fun x ↦ ↑w x ^ t) = ⇑↑v
k : K
⊢ w k = v k

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝ : Field K
v w : InfinitePlace K
h✝ : (↑w).IsEquiv ↑v
t : ℝ
left✝ : 0 < t
h : (fun x ↦ ↑w x ^ t) = ⇑↑v
k : K
⊢ ↑w k = ↑v k
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
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₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2

Tactic:
simpa using

Goal state after:
case refine_2
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₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
h : maximalRealSubfield K = ⊤
⊢ IsTotallyReal K

Tactic:
have : Algebra.IsIntegral (⊤ : Subfield K) K := Algebra.IsIntegral.tower_top ℚ
    rw [← isTotallyReal_top_iff, isTotallyReal_iff_le_maximalRealSubfield, h]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)

Tactic:
let B := Pi.basisFun ℂ (K →+* ℂ)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
⊢ Basis (Free.ChooseBasisIndex ℤ (𝓞 K)) ℂ ((K →+* ℂ) → ℂ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume (if w₀ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} else ball 0 ↑(f ↑w₀)) = 4 * ↑(f ↑w₀) ^ 2

Tactic:
simpa using

Goal state after:
case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ volume {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑w₀) ^ 2} = 4 * ↑(f ↑w₀) ^ 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
A : AffineSubspace ℝ (mixedSpace K) := ↑{ carrier := {x | x.1 w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
h : A = ⊤
⊢ False

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : { w // w.IsReal }
A : AffineSubspace ℝ (mixedSpace K) := ↑{ carrier := {x | x.1 w = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
h : A = ⊤
⊢ False
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsRamified k w
⊢ ¬ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
simpa using

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsRamified k w
⊢ ¬IsSelfAdjoint w.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsRamified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsMixed k (star (star φ))

Tactic:
simpa using

Goal state after:
case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsRamified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsMixed k (conjugate (mk φ).embedding)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : (w.comap (algebraMap k K)).IsReal
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
simpa using

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h : IsUnramified k w
hw : (w.comap (algebraMap k K)).IsReal
⊢ IsSelfAdjoint w.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k (star (star φ))

Tactic:
simpa using

Goal state after:
case refine_1.inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnramified k (mk φ)
hr : (mk φ).embedding = conjugate φ
⊢ IsUnmixed k (conjugate (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:
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.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 : IsUnmixed k φ
hv : ¬ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ ((mk φ).comap (algebraMap k K)).IsComplex

Tactic:
simpa using

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
hv : ¬ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ (mk (φ.comp (algebraMap k K))).IsComplex
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ Bornology.IsBounded (convexBodySum K B)

Tactic:
classical
  refine Metric.isBounded_iff.mpr ⟨B + B, fun x hx y hy => ?_⟩
  simp_rw [dist_eq_norm]
  refine le_trans (norm_sub_le x y) (add_le_add ?_ ?_)
  · exact le_trans (norm_le_convexBodySumFun x) hx
  · exact le_trans (norm_le_convexBodySumFun y) hy

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 →+* ℂ
σ : Gal(K/k)
⊢ σ ∈ Stab (mk φ) ↔ σ = 1 ∨ ComplexEmbedding.IsConj φ σ

Tactic:
by
  simp only [MulAction.mem_stabilizer_iff, smul_mk, mk_eq_iff]
  rw [← ComplexEmbedding.isConj_symm, ComplexEmbedding.conjugate, star_eq_iff_star_eq]
  refine or_congr ⟨fun H ↦ ?_, fun H ↦ H ▸ rfl⟩ Iff.rfl
  exact congr_arg AlgEquiv.symm
    (AlgEquiv.ext (g := AlgEquiv.refl) fun x ↦ φ.injective (RingHom.congr_fun H x))

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ x_1,
      fromBlocks (diagonal fun x ↦ 1) 0 0
          ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
            (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]))
          c x_1 *
        x ((indexEquiv K) x_1)

Tactic:
Fintype.sum_sum_type,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
hx : ∀ (φ : K →+* ℂ), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
c : index K
⊢ ↑(((stdBasis K).repr (fun w ↦ (x (↑w).embedding).re, fun w ↦ x (↑w).embedding)) c) =
    ∑ a₁,
        fromBlocks (diagonal fun x ↦ 1) 0 0
            ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
              (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]))
            c (Sum.inl a₁) *
          x ((indexEquiv K) (Sum.inl a₁)) +
      ∑ a₂,
        fromBlocks (diagonal fun x ↦ 1) 0 0
            ((reindex (Equiv.prodComm (Fin 2) { w // w.IsComplex }) (Equiv.prodComm (Fin 2) { w // w.IsComplex }))
              (blockDiagonal fun x ↦ 2⁻¹ • !![1, 1; -I, I]))
            c (Sum.inr a₂) *
          x ((indexEquiv K) (Sum.inr a₂))