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

Goal state before:
pp: a x : ℝ
hx : 0 < x
⊢ HasSum (fun n ↦ (↑n + a) * rexp (-π * (↑n + a) ^ 2 * x)) (oddKernel (↑a) x)

Tactic:
← hasSum_ofReal,

Goal state after:
a x : ℝ
hx : 0 < x
⊢ HasSum (fun x_1 ↦ ↑((↑x_1 + a) * rexp (-π * (↑x_1 + a) ^ 2 * x))) ↑(oddKernel (↑a) x)
Module: Mathlib.NumberTheory.SumPrimeReciprocals

Goal state before:
pp: case neg
r : ℝ
h : ¬r < -1
⊢ (Summable fun p ↦ ↑↑p ^ r) ↔ r < -1

Tactic:
· -- case `-1 ≤ r`
    simp only [h, iff_false]
    refine fun H ↦ Nat.Primes.not_summable_one_div <| H.of_nonneg_of_le (fun _ ↦ by positivity) ?_
    intro p
    rw [one_div, ← Real.rpow_neg_one]
    exact Real.rpow_le_rpow_of_exponent_le (by exact_mod_cast p.prop.one_lt.le) <| not_lt.mp h

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

Goal state before:
pp: case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / s.Gammaℝ) 0 ((𝓝[≠] 0).limUnder fun s ↦ Λ s / s.Gammaℝ)) 0

Tactic:
refine ((Complex.differentiableOn_update_limUnder_of_isLittleO S_nhds
      (fun t ht ↦ (claim t ht.2 ht.1).differentiableWithinAt) ?_) 0 hs').differentiableAt S_nhds

Goal state after:
case inr
Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
claim : ∀ (t : ℂ), t ≠ 0 → t ≠ 1 → DifferentiableAt ℂ (fun u ↦ Λ u / u.Gammaℝ) t
claim2 : Tendsto (fun s ↦ Λ s / s.Gammaℝ) (𝓝[≠] 0) (𝓝 (L / 2))
hs' : 0 ≠ 1
S_nhds : {1}ᶜ ∈ 𝓝 0
⊢ (fun z ↦ Λ z / z.Gammaℝ - Λ 0 / Gammaℝ 0) =o[𝓝[≠] 0] fun z ↦ (z - 0)⁻¹
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ completedHurwitzZetaOdd a (1 - s) = completedSinZeta a s

Tactic:
rw [completedHurwitzZetaOdd, completedSinZeta,
    (by { push_cast; ring } : (1 - s + 1) / 2 = ↑(3 / 2 : ℝ) - (s + 1) / 2),
    ← hurwitzOddFEPair_k, (hurwitzOddFEPair a).functional_equation ((s + 1) / 2),
    hurwitzOddFEPair_ε, one_smul]

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

Goal state before:
pp: case inr
a b : UnitAddCircle
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) 1

Tactic:
convert!
    (differentiableAt_hurwitzZetaEven_sub_one_div a).fun_sub
      (differentiableAt_hurwitzZetaEven_sub_one_div b) using
    2 with s

Goal state after:
case e'_11
a b : UnitAddCircle
x✝ : ℂ
⊢ hurwitzZetaEven a x✝ - hurwitzZetaEven b x✝ =
    hurwitzZetaEven a x✝ - 1 / (x✝ - 1) / x✝.Gammaℝ - (hurwitzZetaEven b x✝ - 1 / (x✝ - 1) / x✝.Gammaℝ)
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: case inr.refine_1
n : ℕ
a b c : ℤ
Hgcd : {a, b, c}.gcd id = 1
HF : a ^ n + b ^ n + c ^ n = 0
hn : n ≠ 0
⊢ ¬(a = 0 ∧ b = 0)

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:
· rintro ⟨rfl, rfl⟩
    simp only [ne_eq, hn, not_false_eq_true, zero_pow, add_zero, zero_add, pow_eq_zero_iff]
      at HF
    simp only [HF, Finset.mem_singleton, Finset.insert_eq_of_mem, Finset.gcd_singleton, id_eq,
      normalize_zero, zero_ne_one] at Hgcd

Goal state after:
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
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
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi : m = i ^ 2 ∨ m = -i ^ 2
h1 : m = -i ^ 2
⊢ False

Tactic:
have hit : -i ^ 2 ≤ 0 := neg_nonpos.mpr (sq_nonneg i)

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
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : m.gcd (r * s) = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = m * (r * s)
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi : m = i ^ 2 ∨ m = -i ^ 2
h1 : m = -i ^ 2
hit : -i ^ 2 ≤ 0
⊢ False
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
⊢ 2 = 1 + 1 ^ 2

Tactic:
one_pow 2

Goal state after:
K : Type u_1
inst✝ : Field K
hk : ∀ (x : K), 1 + x ^ 2 ≠ 0
x✝ : { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
x y : K
hy : (x, y).2 ≠ -1
hxy : x ^ 2 + y ^ 2 = 1
h2 : y + 1 ≠ 0
h3 : (y + 1) ^ 2 + x ^ 2 = 2 * (y + 1)
⊢ 2 = 1 + 1
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case neg
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
hmc : p = 2 ∨ p ∣ m.natAbs
hnc : p = 2 ∨ p ∣ n.natAbs
h2 : ¬p = 2
⊢ False

Tactic:
· apply hp.not_dvd_one
    rw [← h]
    exact Nat.dvd_gcd (Or.resolve_left hmc h2) (Or.resolve_left hnc h2)

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
⊢ a ∈ primeFactors b ↔ a ∈ normalizedFactors b

Tactic:
by
  simp only [primeFactors, Multiset.mem_toFinset]

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
inst✝ : DecidableEq M
ha : a ≠ 0
hb : b ≠ 0
⊢ primeFactors (a * b) = primeFactors a ∪ primeFactors b

Tactic:
ext p
  simp [mem_normalizedFactors_iff', mem_primeFactors, ha, hb]

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

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ a.natDegree + b.natDegree + c.natDegree = (a * b).natDegree + c.natDegree

Tactic:
Polynomial.natDegree_mul ha hb

Goal state after:
k : Type u_1
inst✝¹ : Field k
inst✝ : DecidableEq k
a b c w : k[X]
hw : w ≠ 0
wab : w = a.wronskian b
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
ab_nz : a * b ≠ 0
abc_nz : a * b * c ≠ 0
abc_dr : k[X] := divRadical (a * b * c)
abc_dr_dvd_w : abc_dr ∣ w
abc_dr_ndeg_lt : abc_dr.natDegree < a.natDegree + b.natDegree
abc_r : k[X] := radical (a * b * c)
⊢ a.natDegree + b.natDegree + c.natDegree = a.natDegree + b.natDegree + c.natDegree
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
⊢ IsRadical (radical a)

Tactic:
intro n p ha
  rw [radical]
  apply Finset.prod_dvd_of_isRelPrime
  · exact pairwise_primeFactors_isRelPrime
  intro i hi
  simp only [mem_primeFactors] at hi
  have : i ∣ radical a := by
    rw [dvd_radical_iff_of_irreducible]
    · exact dvd_of_mem_normalizedFactors hi
    · exact irreducible_of_normalized_factor i hi
    · rintro rfl
      simp only [normalizedFactors_zero, Multiset.notMem_zero] at hi
  exact (prime_of_normalized_factor i hi).isRadical n p (this.trans ha)

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)
h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))
h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0
h20 : 2 ≠ 0
h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1
⊢ False

Tactic:
obtain ⟨p, hp, hp1, hp2⟩ := Nat.Prime.not_coprime_iff_dvd.mp h4

Goal state after:
m0 n0 : ℤ
hm : (m0 * 2 + 1) % 2 = 1
hn : (n0 * 2 + 1) % 2 = 1
h : (m0 * 2 + 1).gcd (n0 * 2 + 1) = 1
h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1)
h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0))
h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0
h20 : 2 ≠ 0
h4 : ¬(2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).gcd (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) = 1
p : ℕ
hp : Nat.Prime p
hp1 : p ∣ (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)).natAbs
hp2 : p ∣ (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1).natAbs
⊢ False
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : IsRadical a
hb₀ : b ≠ 0
hab : a ∣ b
ha₀ : a ≠ 0
⊢ a ∣ radical b

Tactic:
exact (ha.dvd_radical ha₀).trans (radical_dvd_radical hab hb₀)

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

Goal state before:
pp: L : Type u_1
K : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
⊢ (Algebra.norm K) ((algebraMap K L) ((algebraMap (𝓞 K) K) x)) = ↑(x ^ finrank K L)

Tactic:
Algebra.norm_algebraMap,

Goal state after:
L : Type u_1
K : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
⊢ (algebraMap (𝓞 K) K) x ^ finrank K L = ↑(x ^ finrank K L)
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
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
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  (C u * a ^ p).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q)) * radical (C w * c ^ r)).natDegree ∧
    (C v * b ^ q).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q)) * radical (C w * c ^ r)).natDegree ∧
      (C w * c ^ r).natDegree + 1 ≤ (radical (C u * a ^ p * (C v * b ^ q)) * radical (C w * c ^ r)).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
radical_mul habp.isRelPrime,

Goal state after:
case inl
k : Type u_1
inst✝ : Field k
p q r : ℕ
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
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
nd_lt :
  (C u * a ^ p).natDegree + 1 ≤ (radical (C u * a ^ p) * radical (C v * b ^ q) * radical (C w * c ^ r)).natDegree ∧
    (C v * b ^ q).natDegree + 1 ≤ (radical (C u * a ^ p) * radical (C v * b ^ q) * radical (C w * c ^ r)).natDegree ∧
      (C w * c ^ r).natDegree + 1 ≤ (radical (C u * a ^ p) * radical (C v * b ^ q) * radical (C w * c ^ r)).natDegree
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified

Tactic:
obtain ⟨m, n, H⟩ := h.symm.isPrimitiveClassified_of_coprime_of_odd_of_pos hc h2.left hzpos

Goal state after:
case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : y.gcd x = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
m n : ℤ
H :
  (y = m ^ 2 - n ^ 2 ∧ x = 2 * m * n ∨ y = 2 * m * n ∧ x = m ^ 2 - n ^ 2) ∧
    m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
⊢ h.IsPrimitiveClassified
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
    rintro ⟨m, n, ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩, rfl | rfl, co, pp⟩ <;>
      first
      | constructor; ring; exact coprime_sq_sub_mul co pp
      | constructor; ring; rw [Int.gcd_comm]; exact coprime_sq_sub_mul co pp

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Even (torsionOrder K)

Tactic:
suffices orderOf (⟨-1, neg_one_mem_torsion⟩ : torsion K) = 2 by
    rw [even_iff_two_dvd, ← this]
    apply orderOf_dvd_natCard

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ orderOf ⟨-1, ⋯⟩ = 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: 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
h₃ : w.IsReal ∨ |(w.embedding ↑x).re| < 1
ψ : K →ₐ[ℚ] ℂ
hψ : w.embedding.toRatAlgHom ↑x = ψ ↑x
h : 1 ≤ w ↑x
main : w.embedding = ψ.toRingHom ∨ ComplexEmbedding.conjugate w.embedding = ψ.toRingHom
⊢ w.embedding.toRatAlgHom = ψ

Tactic:
cases h₃ with

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

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

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

Tactic:
· simpa [h_ne]

Goal state after:
case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : K
x✝ :
  (∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)) ∧
    |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
h₁ : ∀ (w : InfinitePlace K), w ≠ ↑w₀ → w x < ↑(f w)
h₂ : |((↑w₀).embedding x).re| < 1 ∧ |((↑w₀).embedding x).im| < ↑(f ↑w₀) ^ 2
w : InfinitePlace K
hw : w.IsComplex
h_ne : ¬w = ↑w₀
⊢ w.embedding x ∈ if ⟨w, hw⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f w) ^ 2} else ball 0 ↑(f w)
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F✝ : Type u_1
inst✝³ : Field F✝
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E F : Subfield K
hE : IsTotallyReal ↥E
hF : IsTotallyReal ↥F
⊢ IsTotallyReal ↥(E ⊔ F)

Tactic:
rw [isTotallyReal_iff_le_maximalRealSubfield, sup_le_iff,
    ← isTotallyReal_iff_le_maximalRealSubfield, ← isTotallyReal_iff_le_maximalRealSubfield]

Goal state after:
F✝ : Type u_1
inst✝³ : Field F✝
K : Type u_2
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : Algebra.IsAlgebraic ℚ K
E F : Subfield K
hE : IsTotallyReal ↥E
hF : IsTotallyReal ↥F
⊢ IsTotallyReal ↥E ∧ IsTotallyReal ↥F
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : mixedSpace K
⊢ x ∈ Submodule.span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I)) ↔ x ∈ ⇑(mixedEmbedding K) '' ↑↑I

Tactic:
rw [show Set.range (fractionalIdealLatticeBasis K I) =
        (mixedEmbedding K).toIntAlgHom.toLinearMap '' (Set.range (basisOfFractionalIdeal K I)) by
      rw [← Set.range_comp]
      exact congr_arg Set.range (funext (fun i ↦ fractionalIdealLatticeBasis_apply K I i))]
  rw [← Submodule.map_span, ← SetLike.mem_coe, Submodule.map_coe]
  rw [show Submodule.span ℤ (Set.range (basisOfFractionalIdeal K I)) = (I : Set K) by
        ext; simp [mem_span_basisOfFractionalIdeal]]
  rfl

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
⊢ DiscreteTopology ↥(idealLattice K I)

Tactic:
rw [← span_idealLatticeBasis]
  infer_instance

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)
b : B ⧸ Q
a : A ⧸ P
ha : a ≠ 0
h : a • x = y * b
⊢ (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y))).Splits

Tactic:
obtain ⟨a, rfl⟩ := Quotient.mk_surjective a

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)
b : B ⧸ Q
a : A
ha : (Quotient.mk P) a ≠ 0
h : (Quotient.mk P) a • x = y * b
⊢ (Polynomial.map (algebraMap K L) (minpoly K ((algebraMap (B ⧸ Q) L) x / (algebraMap (B ⧸ Q) L) y))).Splits
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
G : Type u_3
inst✝¹³ : Group G
inst✝¹² : MulSemiringAction G B
inst✝¹¹ : SMulCommClass G A B
K : Type u_4
L : Type u_5
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra A K
inst✝⁷ : IsFractionRing A K
inst✝⁶ : Algebra B L
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra A L
inst✝³ : IsScalarTower A B L
inst✝² : IsScalarTower A K L
inst✝¹ : IsIntegralClosure B A L
inst✝ : FiniteDimensional K L
σ τ : Gal(L/K)
Q : ↑(p.primesOver B)
⊢ map ((galRestrict A K L B) σ * (galRestrict A K L B) τ) ↑Q =
    map ((galRestrict A K L B) σ) (map ((galRestrict A K L B) τ) ↑Q)

Tactic:
exact (Q.1.map_map ((galRestrict A K L B) τ).toRingHom ((galRestrict A K L B) σ).toRingHom).symm

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 Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝⁴ : Q.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
⊢ ∃ σ, σ • P = Q

Tactic:
rcases IsInvariant.exists_smul_of_under_eq A B G P Q <|
    (over_def P p).symm.trans (over_def Q p) with ⟨σ, hs⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra A B
p : Ideal A
P Q : Ideal B
hPp : P.IsPrime
hp : P.LiesOver p
hQp : Q.IsPrime
inst✝⁴ : Q.LiesOver p
G : Type u_3
inst✝³ : Group G
inst✝² : Finite G
inst✝¹ : MulSemiringAction G B
inst✝ : IsGaloisGroup G A B
σ : G
hs : Q = σ • P
⊢ ∃ σ, σ • P = Q
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: case hs
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
y : K
hy : y ∈ ↑(I + J)
⊢ (IsLocalization.map L f hf) y ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))

Tactic:
obtain ⟨i, hi, j, hj, rfl⟩ := (mem_add I J y).mp <| SetLike.mem_coe.mp hy

Goal state after:
case hs
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I J : FractionalIdeal M K
i : K
hi : i ∈ I
j : K
hj : j ∈ J
hy : i + j ∈ ↑(I + J)
⊢ (IsLocalization.map L f hf) (i + j) ∈ ↑(span B (⇑(IsLocalization.map L f hf) '' (↑I ∪ ↑J)))