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

Goal state before:
pp: case inl
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)
n : ℕ
h : n ≠ 0
⊢ (cexp (-(2 * ↑π * ↑a * ↑n) * I) - cexp (2 * ↑π * ↑a * ↑n * I)) * I / 2 / ↑n ^ s =
    -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑n ^ s / 2 +
      -(-I * ↑(↑n).sign) * cexp (-(2 * ↑π * I * ↑a * ↑n)) / ↑n ^ s / 2

Tactic:
simp only [neg_mul, sub_mul, div_right_comm _ (2 : ℂ), Int.sign_natCast_of_ne_zero h,
      Int.cast_one, mul_one, mul_comm I, neg_neg, ← add_div, ← sub_eq_neg_add]
    congr 5 <;> ring

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Wronskian

Goal state before:
pp: case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ derivative a

Tactic:
apply hc.dvd_of_dvd_mul_right

Goal state after:
case left
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
a b : R[X]
hc : IsCoprime a b
hw : a * derivative b = derivative a * b
⊢ a ∣ derivative a * b
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
have hp2' : p = 2 := (Nat.le_of_dvd zero_lt_two hp2).antisymm hp.two_le
      revert hp1
      rw [hp2']
      apply mt Int.emod_eq_zero_of_dvd
      simp only [sq, Nat.cast_ofNat, Int.sub_emod, Int.mul_emod, hm, hn,
        mul_zero, EuclideanDomain.zero_mod, mul_one, zero_sub]
      decide

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 : M
h : radical a = 1
ha : ¬a = 0
this : primeFactors a = ∅
⊢ IsUnit a

Tactic:
rwa [primeFactors_eq_empty_iff ha] at this

Goal state after:
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * a / radical a = a

Tactic:
mul_div_cancel_left₀ _ radical_ne_zero

Goal state after:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ a = a
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inl.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 0
hn2 : n % 2 = 0
h1 : 2 ∣ ↑(n.gcd m)
⊢ False

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  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
⊢ 0 < (m ^ 2 + n ^ 2) / 2

Tactic:
lia

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg.inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ↑x / ↑z
w : ℚ := ↑y / ↑z
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := (circleEquivGen hQ).symm ⟨(v, w), hp⟩
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ↑q.den
n : ℤ := q.num
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
⊢ h.IsPrimitiveClassified

Tactic:
· -- m odd, n odd
    exfalso
    have h1 :
      2 ∣ m ^ 2 + n ^ 2 ∧
        2 ∣ m ^ 2 - n ^ 2 ∧
          (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ Int.gcd ((m ^ 2 - n ^ 2) / 2) ((m ^ 2 + n ^ 2) / 2) = 1 :=
      coprime_sq_sub_sq_sum_of_odd_odd hmncp hm2 hn2
    have h2 : y = (m ^ 2 - n ^ 2) / 2 ∧ z = (m ^ 2 + n ^ 2) / 2 := by
      apply Rat.div_int_inj hzpos _ (h.coprime_of_coprime hc) h1.2.2.2
      · change w = _
        rw [← Rat.divInt_eq_div, ← Rat.divInt_mul_right (by simp : (2 : ℤ) ≠ 0)]
        rw [Int.ediv_mul_cancel h1.1, Int.ediv_mul_cancel h1.2.1, hw2, Rat.divInt_eq_div]
        norm_cast
      · lia
    norm_num [h2.1, h1.2.2.1] at hyo

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ x = m ^ 2 - (-n) ^ 2 ∧
    y = 2 * -m * -n ∧
      z = m ^ 2 + (-n) ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
rw [neg_sq n]

Goal state after:
case h.inl
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
⊢ x = m ^ 2 - n ^ 2 ∧
    y = 2 * -m * -n ∧
      z = m ^ 2 + n ^ 2 ∧ (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.right.inl.right
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos✝ : 0 < z
m n : ℤ
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_odd : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n
h_pos : z = m ^ 2 + n ^ 2
⊢ 0 ≤ -m

Tactic:
lia

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
x✝ : ch ≠ 1
⊢ 2 ≤ ch

Tactic:
lia

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
x✝ : ch ≠ 1
hch2 : 2 ≤ ch
⊢ ca.natDegree + 1 ≤ ca.natDegree * 2

Tactic:
lia

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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ ca.natDegree ≤ d

pp: k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0

Tactic:
· have _ : ch ≠ 1 := CharP.ringChar_ne_one
        have hch2 : 2 ≤ ch := by lia
        rw [← add_le_add_iff_right 1, ← eq_d, eq_deg_a]
        grw [← hch2]
        lia

Goal state after:
k : Type u_1
inst✝ : Field k
p q r : ℕ
u v w : k
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
d : ℕ
a b c : k[X]
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
eq_d : a.natDegree = d + 1
ad : derivative a = 0
bd : derivative b = 0
cd : derivative c = 0
ca : k[X]
ca_nz : ca ≠ 0
cb : k[X]
cb_nz : cb ≠ 0
cc : k[X]
cc_nz : cc ≠ 0
ch : ℕ := ringChar k
chn0 : ch ≠ 0
eq_a : a = (expand k ch) ca
eq_deg_a : a.natDegree = ca.natDegree * ch
eq_b : b = (expand k ch) cb
eq_deg_b : b.natDegree = cb.natDegree * ch
eq_c : c = (expand k ch) cc
eq_deg_c : c.natDegree = cc.natDegree * ch
hnca : ¬ca.natDegree = 0
⊢ C u * ca ^ p + C v * cb ^ q + C w * cc ^ r = 0
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ ‖↑(w.embedding ↑x).re + 0 * Complex.I‖
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |(w.embedding ↑x).re| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : (w.embedding ↑x).im = 0
⊢ 1 ≤ |(w.embedding ↑x).re|

Tactic:
zero_mul,

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : 𝓞 K
w : InfinitePlace K
h₁ : x ≠ 0
h₂ : ∀ ⦃w' : InfinitePlace K⦄, w' ≠ w → w' ↑x < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ ‖↑(w.embedding ↑x).re + 0‖
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
hw : |(w.embedding ↑x).re| < 1
h' : ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
this : (w.embedding ↑x).im = 0
⊢ 1 ≤ |(w.embedding ↑x).re|
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : |(f ζ).re| = ‖f ζ‖
⊢ k ≠ 0

Tactic:
lia

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : (f ζ).im = 0
hone : (f ζ).re = 1
⊢ 1 < k

Tactic:
lia

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : (f ζ).im = 0
hone : (f ζ).re = 1
⊢ (f ζ).re = Complex.re 1

Tactic:
simp [hone]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
him : (f ζ).im = 0
hnegone : (f ζ).re = -1
hζ' : k = if 0 = 2 then 1 else 2
⊢ False

Tactic:
lia

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 : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
a' b' : k[X]
d : k[X] := gcd a b
heq : d ^ n * (a' ^ n + b' ^ n) = c ^ n
eq_a : a = d * a'
eq_b : b = d * b'
hd : d ≠ 0
⊢ n ≠ 0

Tactic:
lia

Goal state after:
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 }
inst✝ : NumberField K
B : ℝ≥0
⊢ MeasurableSet fun x ↦ Real.lt✝ |x.im| (↑B ^ 2)

Tactic:
exact measurableSet_lt (measurable_norm.comp Complex.measurable_im) measurable_const

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:
by
  classical
  -- Let `B` be the canonical basis of `(K →+* ℂ) → ℂ`. We prove that the determinant of
  -- the image by `canonicalEmbedding` of the integral basis of `K` is nonzero. This
  -- will imply the result.
    let B := Pi.basisFun ℂ (K →+* ℂ)
    let e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) :=
      Fintype.equivOfCardEq ((Embeddings.card K ℂ).trans (finrank_eq_card_basis (integralBasis K)))
    let M := B.toMatrix (fun i => canonicalEmbedding K (integralBasis K (e i)))
    suffices M.det ≠ 0 by
      rw [← isUnit_iff_ne_zero, ← Basis.det_apply, ← Basis.is_basis_iff_det] at this
      exact (basisOfPiSpaceOfLinearIndependent this.1).reindex e
  -- In order to prove that the determinant is nonzero, we show that it is equal to the
  -- square of the discriminant of the integral basis and thus it is not zero
    let N := Algebra.embeddingsMatrixReindex ℚ ℂ (fun i => integralBasis K (e i))
      (RingHom.equivRatAlgHom K ℂ)
    rw [show M = N.transpose by { ext : 2; rfl }]
    rw [Matrix.det_transpose, ← pow_ne_zero_iff two_ne_zero]
    convert!
      (map_ne_zero_iff _ (algebraMap ℚ ℂ).injective).mpr
        (Algebra.discr_not_zero_of_basis ℚ (integralBasis K))
    rw [← Algebra.discr_reindex ℚ (integralBasis K) e.symm]
    exact (Algebra.discr_eq_det_embeddingsMatrixReindex_pow_two ℚ ℂ
      (fun i => integralBasis K (e i)) (RingHom.equivRatAlgHom K ℂ)).symm

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
i : Free.ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ Finset.univ
⊢ (latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)

Tactic:
exact Set.mem_range_self i

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
⊢ (fun x ↦ c, fun x ↦ ↑c) = c • 1

Tactic:
ext <;> simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ (fun x ↦ c, fun x ↦ ↑c) = c • 1

Tactic:
ext <;> simp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
⊢ a = 0 ↔ (mixedEmbedding K) a = 0

Tactic:
map_eq_zero

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : K
⊢ a = 0 ↔ a = 0
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
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2

Tactic:
obtain (e | e) := nat_card_stabilizer_eq_one_or_two k w

Goal state after:
case inl
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
e : Nat.card ↥(Stab w) = 1
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2

case inr
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
e : Nat.card ↥(Stab w) = 2
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∏ _k, (2⁻¹ • !![1, 1; -I, I]).det = ∏ _k, 2⁻¹ * I

Tactic:
refine prod_congr (Eq.refl _) (fun _ _ => ?_)
      simp [field]; ring

Goal state after:
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 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:
zero_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, (0 + 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 < volume (convexBodyLT K fun w ↦ if w = w₀ then B else 1)

Tactic:
convexBodyLT_volume,

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) * ↑(∏ w, (if w = w₀ then B else 1) ^ w.mult)
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
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ card (InfinitePlace k) * finrank k K + 0 * (finrank k K / 2) = card (InfinitePlace k) * finrank k K

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
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ Finset.univᶜ = ∅

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
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ x ∈ Finset.univ, InfinitePlace.IsUnramifiedIn K x

Tactic:
zero_mul,

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
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ card (InfinitePlace k) * finrank k K + 0 = card (InfinitePlace k) * finrank 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
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ Finset.univᶜ = ∅

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
inst✝ : IsUnramifiedAtInfinitePlaces k K
⊢ ∀ x ∈ Finset.univ, InfinitePlace.IsUnramifiedIn K x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
i : ChooseBasisIndex ℤ (𝓞 K)
x✝ : i ∈ univ
⊢ (latticeBasis K) i ∈ Set.range ⇑(latticeBasis K)

Tactic:
exact Set.mem_range_self i

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

Goal state before:
pp: case neg
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₀, hw₀⟩).embedding ↑a).re| < 1 ∧
    |((↑⟨w₀, hw₀⟩).embedding ↑a).im| < ↑(if ↑⟨w₀, hw₀⟩ = w₀ then NNReal.sqrt B else 1) ^ 2
w : InfinitePlace K
h_eq : ¬w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)

Tactic:
· refine lt_of_lt_of_le (if_neg h_eq ▸ h_le w h_eq) ?_
      rw [NNReal.coe_one, Real.le_sqrt' zero_lt_one, one_pow]
      norm_num

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

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

Tactic:
simp_rw [normAtPlace_apply_of_isComplex hw, negAt_apply_isComplex]

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Galois

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
p : Ideal A
P : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
G : Type u_3
inst✝⁴ : Group G
inst✝³ : Finite G
inst✝² : MulSemiringAction G B
inst✝¹ : IsGaloisGroup G A B
σ : G
hQp : (σ • P).IsPrime
inst✝ : (σ • P).LiesOver p
⊢ P.ramificationIdx A = (σ • P).ramificationIdx A

Tactic:
rw [ramificationIdx_smul]

Goal state after: