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

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S}
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
⊢ (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ x ::ₒ t) = 0

Tactic:
simp only [Poly.map_apply]

Goal state after:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S}
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
⊢ p ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
k : ℕ
this : Summable fun n ↦ ↑n ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑n))
⊢ Summable fun n ↦ ↑|n| ^ k * rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
by
    apply Summable.of_nat_of_neg <;>
    simpa only [Int.cast_neg, neg_sq, abs_neg, Int.cast_natCast, Nat.abs_cast]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
P : WeakFEPair E
inst✝ : CompleteSpace E
s : ℂ
hs : P.k < s.re
h_re1 : -1 < (s - 1).re
h_re2 : -1 < (s - ↑P.k - 1).re
⊢ s ≠ 0

Tactic:
grind [P.hk, zero_re]

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

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

Tactic:
refine ((Tendsto.sub ?_ ?_).mono_left nhdsWithin_le_nhds).sub ?_

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

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

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ 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
⊢ 0 < (s + 1).re

Tactic:
rw [add_re, one_re]

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
r : ι → ℝ
F : ℝ → ℂ
s : ℂ
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ 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
⊢ 0 < s.re + 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖Real.cos (2 * π * a * (↑n + 1))‖ * rexp (-π * (↑n + 1) ^ 2 * t) ≤ rexp (-π * (↑n + 1) ^ 2 * t)

Tactic:
Real.norm_eq_abs

Goal state after:
a p : ℝ
hp : 0 < p
hp' : (fun t ↦ HurwitzKernelBounds.F_nat 0 1 t - if 1 = 0 then 1 else 0) =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ |Real.cos (2 * π * a * (↑n + 1))| * rexp (-π * (↑n + 1) ^ 2 * t) ≤ rexp (-π * (↑n + 1) ^ 2 * t)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ 1 / 2 = (hurwitzEvenFEPair a).k

Tactic:
by rfl

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ (hurwitzEvenFEPair a).ε = 1

Tactic:
by rfl

Goal state after:
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
⊢ ∏' (p : Primes), f ↑p = ∏' (n : ℕ), if Prime n then f n else 1

Tactic:
rw [ite_prime_eq_mulIndicator]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
⊢ ∏' (p : Primes), f ↑p = tprod ({n | Prime n}.mulIndicator f)
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
⊢ (Multipliable fun p ↦ f ↑p) ↔ Multipliable fun n ↦ if Prime n then f n else 1

Tactic:
rw [ite_prime_eq_mulIndicator]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
⊢ (Multipliable fun p ↦ f ↑p) ↔ Multipliable ({n | Prime n}.mulIndicator f)
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
a : M
⊢ HasProd (fun p ↦ f ↑p) a ↔ HasProd (fun n ↦ if Prime n then f n else 1) a

Tactic:
rw [ite_prime_eq_mulIndicator]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
f : ℕ → M
a : M
⊢ HasProd (fun p ↦ f ↑p) a ↔ HasProd ({n | Prime n}.mulIndicator f) a
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: case h
a p : ℝ
hp : 0 < p
hp' : HurwitzKernelBounds.F_nat 1 0 =O[atTop] fun t ↦ rexp (-p * t)
t : ℝ
ht : 0 < t
n : ℕ
⊢ ↑n * ‖Real.sin (2 * π * a * ↑n)‖ ≤ ↑n

Tactic:
exact mul_le_of_le_one_right (Nat.cast_nonneg _) (abs_sin_le_one _)

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

Goal state before:
pp: a : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ completedHurwitzZetaEven₀ a s - (if a = 0 then 1 else 0) / s) 1

Tactic:
exact (differentiable_completedHurwitzZetaEven₀ a _).sub
    <| (differentiableAt_const _).div differentiableAt_id one_ne_zero

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

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < (s + 1).re

Tactic:
rw [add_re, one_re]

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℤ
⊢ 0 < s.re + 1
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
hn : n ≠ 0
⊢ (normalizedFactors (a ^ n)).toFinset = (normalizedFactors a).toFinset

Tactic:
normalizedFactors_pow,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
n : ℕ
hn : n ≠ 0
⊢ (n • normalizedFactors a).toFinset = (normalizedFactors a).toFinset
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✝

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

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 1
m0 : ℤ
hm2 : m - 1 = m0 * 2
n0 : ℤ
hn2 : n - 1 = n0 * 2
⊢ 2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1

Tactic:
rw [sub_eq_iff_eq_add] at hm2 hn2

Goal state after:
m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 2 = 1
m0 : ℤ
hm2 : m = m0 * 2 + 1
n0 : ℤ
hn2 : n = n0 * 2 + 1
⊢ 2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.refine_2
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
h : radical a ∣ b
⊢ normalizedFactors a ≤ normalizedFactors (b ^ (normalizedFactors a).card)

Tactic:
normalizedFactors_pow,

Goal state after:
case inr.refine_2
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
h : radical a ∣ b
⊢ normalizedFactors a ≤ (normalizedFactors a).card • normalizedFactors b
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
⊢ absNorm 1 = 1

Tactic:
by convert! absNorm.map_one'

Goal state after:
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |((Algebra.leftMulMatrix b₀) ((algebraMap R K) ↑I.den)).det| * |(b₀.toMatrix (Subtype.val ∘ ⇑bI)).det| /
      |↑((Algebra.norm ℤ) ↑I.den)|

Tactic:
← Algebra.norm_eq_matrix_det,

Goal state after:
R : Type u_1
inst✝¹¹ : CommRing R
inst✝¹⁰ : IsDedekindDomain R
inst✝⁹ : Free ℤ R
inst✝⁸ : Module.Finite ℤ R
K : Type u_2
inst✝⁷ : CommRing K
inst✝⁶ : Algebra R K
inst✝⁵ : IsFractionRing R K
inst✝⁴ : IsLocalization (Algebra.algebraMapSubmonoid R ℤ⁰) K
inst✝³ : Algebra ℚ K
inst✝² : IsDomain K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
b : Basis ι ℤ R
I : FractionalIdeal R⁰ K
bI : Basis ι ℤ ↥↑I
this : Nontrivial K
b₀ : Basis ι ℚ K := Basis.localizationLocalization ℚ ℤ⁰ K b
bI.num : Basis ι ℤ ↥I.num := bI.map (LinearEquiv.restrictScalars ℤ (equivNum ⋯))
⊢ |((Basis.localizationLocalization ℚ ℤ⁰ K b).toMatrix (Subtype.val ∘ ⇑bI)).det| =
    |(Algebra.norm ℚ) ((algebraMap R K) ↑I.den)| * |(b₀.toMatrix (Subtype.val ∘ ⇑bI)).det| /
      |↑((Algebra.norm ℤ) ↑I.den)|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

Tactic:
obtain ⟨j, hiφ⟩ := (φ.injective).hasLeftInverse

Goal state after:
case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

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

Tactic:
· exact congr_arg mk h

Goal state after:
case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk φ = mk ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬w.IsReal ↔ ¬ComplexEmbedding.IsReal w.embedding

Tactic:
isReal_iff

Goal state after:
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬ComplexEmbedding.IsReal w.embedding ↔ ¬ComplexEmbedding.IsReal w.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ ¬ComplexEmbedding.conjugate w.embedding = w.embedding

Tactic:
← ComplexEmbedding.isReal_iff,

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬w.IsReal
⊢ ¬ComplexEmbedding.IsReal w.embedding
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝² : Field K
α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : NumberField K
f : InfinitePlace K → α
⊢ ∏ w, f w = (∏ w, f ↑w) * ∏ i, f ↑((Equiv.subtypeEquivRight ⋯) i)

Tactic:
simp [Fintype.prod_subtype_mul_prod_subtype]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : (𝓞 K)ˣ
n : ℤ
⊢ ((coeHom K).comp (map ↑(algebraMap (𝓞 K) K))) (x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n

Tactic:
exact map_zpow _ x n

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

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

Tactic:
← orderOf_submonoid

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : 2 < orderOf ↑↑↑x
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex), ‖x.2 ⟨a, b⟩‖ < ↑(f a)
⊢ (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex), ‖x.2 ⟨a, b⟩‖ < ↑(f a)

Tactic:
exact hx

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 : a' ^ n + b' ^ n = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
goal : (∃ x, C x = a') ∧ (∃ x, C x = b') ∧ ∃ x, C x = c'
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'

Tactic:
obtain ⟨⟨ca', ha'⟩, ⟨cb', hb'⟩, ⟨cc', hc'⟩⟩ := goal

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 = c' ^ n
hc : d ≠ 0 ∧ c' ≠ 0
eq_c : c = c' * d
ca' : k
ha' : C ca' = a'
cb' : k
hb' : C cb' = b'
cc' : k
hc' : C cc' = c'
⊢ IsUnit a' ∧ IsUnit b' ∧ IsUnit c'
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
⊢ (commMap K) ((canonicalEmbedding K) x) = (mixedEmbedding K) x

Tactic:
simp only [canonicalEmbedding, commMap, LinearMap.coe_mk, AddHom.coe_mk, RingHom.pi_apply,
    mixedEmbedding, RingHom.prod_apply, Prod.mk.injEq]

Goal state after:
K : Type u_1
inst✝ : Field K
x : K
⊢ (fun w ↦ ((↑w).embedding x).re) = (RingHom.pi fun w ↦ embedding_of_isReal ⋯) x ∧
    (fun w ↦ (↑w).embedding x) = (RingHom.pi fun w ↦ (↑w).embedding) 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
w : InfinitePlace K
h : IsUnramified k w
hw : ComplexEmbedding.IsReal ((conjugate w.embedding).comp (algebraMap k K))
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)

Tactic:
simp_rw [conjugate_comp, IsSelfAdjoint.star_iff, ← isReal_mk_iff, ← comap_mk, mk_embedding] at hw

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
⊢ ComplexEmbedding.IsReal (conjugate w.embedding)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
⊢ (mk φ).IsReal ∨ ((mk φ).comap (algebraMap k K)).IsComplex

Tactic:
isReal_iff

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsUnmixed k φ
⊢ ComplexEmbedding.IsReal (mk φ).embedding ∨ ((mk φ).comap (algebraMap k K)).IsComplex
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · ext w
    · exact norm_eq_zero.mp (normAtPlace_apply_of_isReal w.prop _ ▸ h w.1)
    · exact norm_eq_zero.mp (normAtPlace_apply_of_isComplex w.prop _ ▸ h w.1)
  · simp_rw [h, map_zero, implies_true]

Goal state after:
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
⊢ convexBodySumFun x ≤ B

Tactic:
exact hx

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 (mk w.embedding) ↔ Stab (mk w.embedding) = ⊥

Tactic:
isUnramified_mk_iff_forall_isConj

Goal state after:
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
⊢ (∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj w.embedding σ → σ = 1) ↔ Stab (mk w.embedding) = ⊥
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case e'_3
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
hw : ¬IsUnramified k w
H : ¬Finite Gal(K/k)
⊢ Nat.card Gal(K/k) = 0

Tactic:
by_contra e

Goal state after:
case e'_3
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
hw : ¬IsUnramified k w
H : ¬Finite Gal(K/k)
e : ¬Nat.card Gal(K/k) = 0
⊢ 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
inst✝² : NumberField K
inst✝¹ : NumberField k
inst✝ : IsGalois k K
⊢ #{w | IsUnramified k w} = #{w | IsUnramifiedIn K w} * Nat.card Gal(K/k)

Tactic:
Finset.card_eq_sum_card_fiberwise (f := (comap · (algebraMap k K)))
    (t := {w : InfinitePlace k | w.IsUnramifiedIn K}),

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
⊢ ∑ b with IsUnramifiedIn K b, #({a ∈ {w | IsUnramified k w} | a.comap (algebraMap k K) = b}) =
    #{w | IsUnramifiedIn K w} * Nat.card Gal(K/k)

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
⊢ Set.MapsTo (fun x ↦ x.comap (algebraMap k K)) ↑{w | IsUnramified k w} ↑{w | IsUnramifiedIn K w}
Module: Mathlib.RingTheory.IntegralClosure.IntegralRestrict

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
L₂ : Type u_4
B : Type u_6
B₂ : Type u_7
inst✝²⁰ : CommRing A
inst✝¹⁹ : CommRing B
inst✝¹⁸ : CommRing B₂
inst✝¹⁷ : Algebra A B
inst✝¹⁶ : Algebra A B₂
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Field L₂
inst✝¹² : Algebra A K
inst✝¹¹ : Algebra K L
inst✝¹⁰ : Algebra A L
inst✝⁹ : IsScalarTower A K L
inst✝⁸ : Algebra K L₂
inst✝⁷ : Algebra A L₂
inst✝⁶ : IsScalarTower A K L₂
inst✝⁵ : Algebra B L
inst✝⁴ : IsScalarTower A B L
inst✝³ : IsIntegralClosure B A L
inst✝² : Algebra B₂ L₂
inst✝¹ : IsScalarTower A B₂ L₂
inst✝ : IsIntegralClosure B₂ A L₂
σ : L →ₐ[K] L₂
x : B
⊢ (algebraMap B₂ L₂) ((galRestrict' A B B₂ σ) x) = σ ((algebraMap B L) x)

Tactic:
simp [galRestrict', galRestrict', Subalgebra.algebraMap_eq]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsTotallyComplex K
⊢ ↑(finrank ℚ K) ^ (2 * finrank ℚ K) / ((4 / π) ^ finrank ℚ K * ↑(finrank ℚ K).factorial ^ 2) ≤ ↑|discr K|

Tactic:
by
  have := abs_discr_ge' K
  rwa [← IsTotallyComplex.finrank] at this

Goal state after:
Module: Mathlib.RingTheory.Invariant.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
⊢ (aeval ((aeval d) (C ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a))) * (aeval d) X))
      (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) p)) =
    0

Tactic:
aeval_C,

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁹ : CommRing A
inst✝¹⁸ : CommRing B
inst✝¹⁷ : Algebra A B
G : Type u_3
inst✝¹⁶ : Finite G
inst✝¹⁵ : Group G
inst✝¹⁴ : MulSemiringAction G B
inst✝¹³ : Algebra.IsInvariant A B G
P : Ideal A
Q : Ideal B
inst✝¹² : Q.LiesOver P
inst✝¹¹ : P.IsPrime
inst✝¹⁰ : Q.IsPrime
K : Type u_4
L : Type u_5
inst✝⁹ : Field K
inst✝⁸ : Field L
inst✝⁷ : Algebra K L
inst✝⁶ : Algebra (A ⧸ P) K
inst✝⁵ : IsFractionRing (A ⧸ P) K
inst✝⁴ : Algebra (B ⧸ Q) L
inst✝³ : IsFractionRing (B ⧸ Q) L
inst✝² : Algebra (A ⧸ P) L
inst✝¹ : IsScalarTower (A ⧸ P) (B ⧸ Q) L
inst✝ : IsScalarTower (A ⧸ P) K L
this✝ : Algebra.IsIntegral A B
this : Algebra.IsAlgebraic K L
x y : B ⧸ Q
hy : y ∈ nonZeroDivisors (B ⧸ Q)
a : A
ha : (algebraMap A (A ⧸ P)) a ≠ 0
b : B
h : (algebraMap A (A ⧸ P)) a • x = y * (algebraMap B (B ⧸ Q)) b
val✝ : Fintype G
p : A[X]
hp : Polynomial.map (algebraMap A B) p = MulSemiringAction.charpoly G b
h_monic : p.Monic
h_eval : (aeval b) p = 0
q : A[X] := p.comp (C a * X)
d : L := (algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y
comm₁ : (algebraMap K L).comp (algebraMap (A ⧸ P) K) = (algebraMap (B ⧸ Q) L).comp (algebraMap (A ⧸ P) (B ⧸ Q))
comm₂ : (algebraMap (A ⧸ P) (B ⧸ Q)).comp (algebraMap A (A ⧸ P)) = (algebraMap B (B ⧸ Q)).comp (algebraMap A B)
⊢ (aeval ((algebraMap K L) ((algebraMap (A ⧸ P) K) ((algebraMap A (A ⧸ P)) a)) * (aeval d) X))
      (Polynomial.map (algebraMap (A ⧸ P) K) (Polynomial.map (algebraMap A (A ⧸ P)) p)) =
    0
Module: Mathlib.NumberTheory.NumberField.Discriminant.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
a : 𝓞 K
h : (minpoly ℚ ↑a).natDegree = finrank ℚ K
⊢ (minpoly ℤ ↑a).natDegree ≤ rankOfDiscrBdd N

Tactic:
minpoly.isIntegrallyClosed_eq_field_fractions' ℚ a.isIntegral_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
N : ℕ
hK : |discr K| ≤ ↑N
a : 𝓞 K
h : (Polynomial.map (algebraMap ℤ ℚ) (minpoly ℤ ((algebraMap (𝓞 K) K) a))).natDegree = finrank ℚ K
⊢ (minpoly ℤ ↑a).natDegree ≤ rankOfDiscrBdd N