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

Goal state before:
pp: case H
a : ℝ
⊢ ContinuousOn (fun x ↦ ↑(oddKernel (↑a) x)) (Ioi 0)

Tactic:
oddKernel_def' a

Goal state after:
case H
a : ℝ
⊢ ContinuousOn
    (fun x ↦
      cexp (-↑π * ↑a ^ 2 * ↑x) *
        (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x)))
    (Ioi 0)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ * (0 - 2 * ↑π * I * z * 0)

pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

pp: case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

Tactic:
mul_zero,

Goal state after:
case inl
z τ : ℂ
hτ : τ.im ≤ 0
⊢ 0 = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ * (0 - 0)

case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0

case inl.hτ
z τ : ℂ
hτ : τ.im ≤ 0
⊢ (-1 / τ).im ≤ 0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ deriv (fun x ↦ jacobiTheta₂ x τ) z =
    deriv (fun z ↦ 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)) z

Tactic:
rw [funext (jacobiTheta₂_functional_equation · τ)]

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

Tactic:
rcases eq_or_ne N 0 with rfl | hN

Goal state after:
case inl
s : ℂ
hs : 1 < s.re
χ : DirichletCharacter ℂ 0
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s

case inr
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
hN : N ≠ 0
⊢ L ((fun n ↦ χ ↑n) * fun n ↦ ↑(Λ n)) s = -deriv (L fun n ↦ χ ↑n) s / L (fun n ↦ χ ↑n) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      (s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        (s + 1).Gammaℝ * -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedSinZeta (↑a) s + (s + 1).Gammaℝ * -I * 0 * cexp (2 * ↑π * I * ↑a * 0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) s)

Tactic:
mul_zero,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
this :
  HasSum
    (fun n ↦
      (s + 1).Gammaℝ * -I * ↑(↑n).sign * cexp (2 * ↑π * I * ↑a * ↑↑n) / ↑|↑n| ^ s / 2 +
        (s + 1).Gammaℝ * -I * ↑(-↑n).sign * cexp (2 * ↑π * I * ↑a * ↑(-↑n)) / ↑|(-↑n)| ^ s / 2)
    (completedSinZeta (↑a) s + 0 * cexp 0 / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (completedSinZeta (↑a) 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
⊢ IsUnit ({A, B, C}.gcd id)

Tactic:
refine isUnit_of_associated_mul ?_ ha.1

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
⊢ Associated (d * {A, B, C}.gcd id) d
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)

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:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inr.inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 0
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

pp: case inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0

Tactic:
· right
    exact ⟨hx, hy⟩

Goal state after:
case inr.inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 1
hy : y % 2 = 1
⊢ x % 2 = 0 ∧ y % 2 = 1 ∨ x % 2 = 1 ∧ y % 2 = 0
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: M N : ℕ
inst✝ : NeZero N
hMN : M ∣ N
χ : DirichletCharacter ℂ M
s : ℂ
hs : 1 < s.re
⊢ L (fun n ↦ ((changeLevel hMN) χ) ↑n) s = L (fun n ↦ χ ↑n) s * ∏ p ∈ N.primeFactors, (1 - χ ↑p * ↑p ^ (-s))

Tactic:
rw [prod_eq_tprod_mulIndicator, ← DirichletCharacter.LSeries_eulerProduct_tprod _ hs,
    ← DirichletCharacter.LSeries_eulerProduct_tprod _ hs]
  -- convert to a form suitable for `tprod_subtype`
  have (f : Primes → ℂ) : ∏' (p : Primes), f p = ∏' (p : ↑{p : ℕ | p.Prime}), f p := rfl
  rw [this, tprod_subtype _ fun p : ℕ ↦ (1 - (changeLevel hMN χ) p * p ^ (-s))⁻¹,
    this, tprod_subtype _ fun p : ℕ ↦ (1 - χ p * p ^ (-s))⁻¹, ← Multipliable.tprod_mul]
  rotate_left -- deal with convergence goals first
  · exact multipliable_subtype_iff_mulIndicator.mp
      (DirichletCharacter.LSeries_eulerProduct_hasProd χ hs).multipliable
  · exact multipliable_subtype_iff_mulIndicator.mp Multipliable.of_finite
  · congr 1 with p
    simp only [Set.mulIndicator_apply, Set.mem_ofPred_eq, Finset.mem_coe, Nat.mem_primeFactors,
      ne_eq, mul_ite, mul_one]
    by_cases h : p.Prime; swap
    · simp only [h, false_and, if_false]
    simp only [h, true_and, if_true]
    by_cases hp' : p ∣ N; swap
    · simp only [hp', false_and, ↓reduceIte, inv_inj, sub_right_inj, mul_eq_mul_right_iff,
        cpow_eq_zero_iff, Nat.cast_eq_zero, h.ne_zero, ne_eq, neg_eq_zero, or_false]
      have hq : IsUnit (p : ZMod N) := (ZMod.isUnit_prime_iff_not_dvd h).mpr hp'
      simp only [hq.unit_spec ▸ DirichletCharacter.changeLevel_eq_cast_of_dvd χ hMN hq.unit,
        ZMod.cast_natCast hMN]
    · simp only [hp', NeZero.ne N, not_false_eq_true, and_self, ↓reduceIte]
      have : ¬IsUnit (p : ZMod N) := by rwa [ZMod.isUnit_prime_iff_not_dvd h, not_not]
      rw [MulChar.map_nonunit _ this, zero_mul, sub_zero, inv_one]
      refine (inv_mul_cancel₀ ?_).symm
      rw [sub_ne_zero, ne_comm]
      -- Remains to show `χ p * p ^ (-s) ≠ 1`. We show its norm is strictly `< 1`.
      apply_fun (‖·‖)
      simp only [norm_mul, norm_one]
      have ha : ‖χ p‖ ≤ 1 := χ.norm_le_one p
      have hb : ‖(p : ℂ) ^ (-s)‖ ≤ 1 / 2 := norm_prime_cpow_le_one_half ⟨p, h⟩ hs
      exact ((mul_le_mul ha hb (norm_nonneg _) zero_le_one).trans_lt (by norm_num)).ne

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

Goal state before:
pp: case inr
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 = ↑n + b
⊢ ↑(SignType.sign 0) / 0 ^ s = 1 / 0 ^ s

Tactic:
zero_cpow ((not_lt.mpr zero_le_one) ∘ (zero_re ▸ · ▸ hs)),

Goal state after:
case inr
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
b : ℝ
hb✝ : 0 ≤ b
hb : 0 = ↑n + b
⊢ ↑(SignType.sign 0) / 0 = 1 / 0
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)) * I - cexp (2 * ↑π * ↑a * ↑n * I) * I) / ↑n ^ s / 2 =
    (cexp (-(2 * ↑π * I * ↑a * ↑n)) * I - cexp (2 * ↑π * I * ↑a * ↑n) * I) / ↑n ^ s / 2

Tactic:
congr 5 <;> ring

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ hurwitzZetaOdd a (1 - s) = 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * sinZeta a s

Tactic:
by
  rw [← Gammaℂ, hurwitzZetaOdd, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv,
    inv_Gammaℝ_two_sub hs, completedHurwitzZetaOdd_one_sub, sinZeta, ← div_eq_mul_inv,
    ← mul_div_assoc, ← mul_div_assoc, mul_comm]

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
h2n : ↑p ∣ 2 * n ^ 2
⊢ False

Tactic:
have hmc : p = 2 ∨ p ∣ Int.natAbs m := prime_two_or_dvd_of_dvd_two_mul_pow_self_two hp h2m

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
hmc : p = 2 ∨ p ∣ m.natAbs
⊢ False
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: case inr.inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
hc : IsRelPrime a 0
⊢ primeFactors (a * 0) = (primeFactors a).disjUnion (primeFactors 0) ⋯

Tactic:
rw [isRelPrime_zero_right] at hc

Goal state after:
case inr.inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
hc✝ : IsRelPrime a 0
hc : IsUnit a
⊢ primeFactors (a * 0) = (primeFactors a).disjUnion (primeFactors 0) ⋯
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 : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : -(b + c) = a
⊢ IsCoprime c a

Tactic:
rw [← hsum', IsCoprime.neg_right_iff]

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 : a + b + c = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : -(b + c) = a
⊢ IsCoprime c (b + c)
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
⊢ radical a ∣ radical b ↔ primeFactors a ⊆ primeFactors b

Tactic:
by
  classical
  rw [radical_dvd_radical_iff_normalizedFactors_subset_normalizedFactors, primeFactors,
    primeFactors, Multiset.toFinset_subset]

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 b : E
h : IsCoprime (radical a * EuclideanDomain.divRadical a) (radical b * EuclideanDomain.divRadical b)
⊢ IsCoprime (EuclideanDomain.divRadical a) (EuclideanDomain.divRadical b)

Tactic:
exact h.of_mul_left_right.of_mul_right_right

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

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

Tactic:
h_neg

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

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

Tactic:
cases mk_eq_iff.mp (mk_embedding (mk φ)) with
  | inl h => rwa [h] at hφ
  | inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ

Goal state after:
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) * ∏ w, f ↑w

Tactic:
rw [← Equiv.prod_comp (Equiv.subtypeEquivRight (fun _ ↦ not_isReal_iff_isComplex))]
  simp [Fintype.prod_subtype_mul_prod_subtype]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl.right.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
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_neg : z = -(m ^ 2 + n ^ 2)
⊢ 0 < z → False

Tactic:
h_neg

Goal state after:
case h.inl.right.inr
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
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_neg : z = -(m ^ 2 + n ^ 2)
⊢ 0 < -(m ^ 2 + n ^ 2) → False
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
h : ζ ^ ↑k = 1
⊢ orderOf ζ ∣ torsionOrder K

Tactic:
· have hζ : ζ ∈ torsion K := by
      rw [torsion, CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
      exact ⟨k, k.prop, h⟩
    rw [orderOf_submonoid (⟨ζ, hζ⟩ : torsion K)]
    apply orderOf_dvd_natCard

Goal state after:
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)ˣ

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

Tactic:
· rw [CommGroup.mem_torsion, isOfFinOrder_iff_pow_eq_one]
    exact ⟨torsionOrder K, torsionOrder_pos K, h⟩

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
h : ζ ∈ CommGroup.torsion (𝓞 K)ˣ
⊢ ζ ^ torsionOrder K = 1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
this : nrRealPlaces K + 2 * 0 = 1
⊢ nrRealPlaces K = 1

Tactic:
mul_zero,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
this : nrRealPlaces K + 0 = 1
⊢ nrRealPlaces K = 1
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
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 : d ≠ 0 ∧ ca' ≠ 0
ha' : C ca' = a'
cb' : k
hb : d ≠ 0 ∧ cb' ≠ 0
hb' : C cb' = b'
cc' : k
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')

Tactic:
← hc',

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
eq_a : a = a' * d
eq_b : b = b' * d
hd : d ≠ 0
c' : k[X]
heq : a' ^ n + b' ^ n = c' ^ n
eq_c : c = c' * d
ca' : k
ha : d ≠ 0 ∧ ca' ≠ 0
ha' : C ca' = a'
cb' : k
hb : d ≠ 0 ∧ cb' ≠ 0
hb' : C cb' = b'
cc' : k
hc : d ≠ 0 ∧ C cc' ≠ 0
hc' : C cc' = c'
⊢ IsUnit (C ca') ∧ IsUnit (C cb') ∧ IsUnit (C cc')
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : IsTotallyReal K
⊢ nrRealPlaces K + 2 * 0 = nrRealPlaces K

Tactic:
mul_zero,

Goal state after:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : IsTotallyReal K
⊢ nrRealPlaces K + 0 = nrRealPlaces K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
⊢ x = 0

Tactic:
ext1 φ

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : (K →+* ℂ) → ℂ
h_zero : (commMap K) x = 0
h_mem : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))
φ : K →+* ℂ
⊢ x φ = 0 φ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ convexBodySum K B = B • convexBodySum K 1

Tactic:
simp_rw [← Set.preimage_smul_inv₀ (ne_of_gt hB), Set.preimage_ofPred_eq, convexBodySumFun,
        normAtPlace_smul, abs_inv, abs_eq_self.mpr (le_of_lt hB), ← mul_assoc, mul_comm, mul_assoc,
        ← Finset.mul_sum, inv_mul_le_iff₀ hB, mul_one]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (fun c ↦
        Sum.casesOn (motive := fun t ↦ c = t → K →+* ℂ) c (fun w h ↦ (↑w).embedding)
          (fun wj h ↦
            Prod.casesOn wj fun w j ↦ if j = 0 then (↑w).embedding else ComplexEmbedding.conjugate (↑w).embedding)
          ⋯)
      (Sum.inl (mkReal ⟨φ, hφ⟩)) =
    φ

Tactic:
simp [embedding_mk_eq_of_isReal hφ]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∏ _k, 2⁻¹ * I = (2⁻¹ * I) ^ Fintype.card { w // w.IsComplex }

Tactic:
prod_const,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (2⁻¹ * I) ^ #univ = (2⁻¹ * I) ^ Fintype.card { w // w.IsComplex }
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 : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ {a ∈ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w} =
    (MulAction.orbit Gal(K/k) w).toFinset

Tactic:
ext w'

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
w : InfinitePlace K
hw : IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
⊢ w' ∈ {a ∈ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w} ↔
    w' ∈ (MulAction.orbit Gal(K/k) w).toFinset
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 : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
⊢ {a ∉ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w} =
    (MulAction.orbit Gal(K/k) w).toFinset

Tactic:
ext w'

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
w : InfinitePlace K
hw : ¬IsUnramifiedIn K ((fun x ↦ x.comap (algebraMap k K)) w)
w' : InfinitePlace K
⊢ w' ∈ {a ∉ {w | IsUnramified k w} | a.comap (algebraMap k K) = (fun x ↦ x.comap (algebraMap k K)) w} ↔
    w' ∈ (MulAction.orbit Gal(K/k) w).toFinset
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
B : ℝ
h : minkowskiBound K I ≤ volume (convexBodySum K B)
hB : 0 ≤ B
h1 : 0 < (↑(finrank ℚ K))⁻¹
h2 : 0 ≤ B / ↑(finrank ℚ K)
h_fund :
  IsAddFundamentalDomain (↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup)
    (fundamentalDomain (fractionalIdealLatticeBasis K I)) volume
this : Countable ↥(span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
a : K
ha : a ∈ ↑↑I
hx : (mixedEmbedding K) a ∈ (span ℤ (Set.range ⇑(fractionalIdealLatticeBasis K I))).toAddSubgroup
h_nz : ⟨(mixedEmbedding K) a, hx⟩ ≠ 0
h_mem : ↑⟨(mixedEmbedding K) a, hx⟩ ∈ convexBodySum K B
⊢ ↑|(Algebra.norm ℚ) a| ^ (∑ x, ↑x.mult)⁻¹ ≤ (∏ i, ↑i a ^ ↑i.mult) ^ (∑ i, ↑i.mult)⁻¹

Tactic:
simp_rw [← prod_eq_abs_norm, rpow_natCast]
    exact le_of_eq rfl

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nm :
  ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
I₀ : Ideal (𝓞 K)
hI : span {a} = ↑J * 0
h_nz : I₀ = 0
⊢ (Algebra.linearMap (𝓞 K) K) a = 0

Tactic:
mul_zero,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
a : 𝓞 K
ha : a ∈ ↑↑J
h_nm :
  ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤
    ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ nrComplexPlaces K * ↑(finrank ℚ K)! /
        ↑(finrank ℚ K) ^ finrank ℚ K *
      √|↑(discr K)|
I₀ : Ideal (𝓞 K)
hI : span {a} = 0
h_nz : I₀ = 0
⊢ (Algebra.linearMap (𝓞 K) K) a = 0
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : absNorm (under ℤ I) = 0
⊢ absNorm (under ℤ I) = sInf {d | 0 < d ∧ ↑d ∈ I}

Tactic:
have : {d : ℕ | 0 < d ∧ ↑d ∈ I} = ∅ := by
      refine Set.eq_empty_of_forall_notMem ?_
      intro x ⟨hx₁, hx₂⟩
      rw [← cast_natCast, cast_mem_ideal_iff, h, natCast_dvd_natCast, Nat.zero_dvd] at hx₂
      rw [Nat.pos_iff_ne_zero] at hx₁
      exact hx₁ hx₂
    rw [h, this, Nat.sInf_empty]

Goal state after:
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ¬absNorm (under ℤ I) = 0
h₁ : absNorm (under ℤ I) ∈ {d | 0 < d ∧ ↑d ∈ I}
⊢ absNorm (under ℤ I) ≤ sInf {d | 0 < d ∧ ↑d ∈ I}

Tactic:
by_contra! h₀

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
I : Ideal R
h : ¬absNorm (under ℤ I) = 0
h₁ : absNorm (under ℤ I) ∈ {d | 0 < d ∧ ↑d ∈ I}
h₀ : sInf {d | 0 < d ∧ ↑d ∈ I} < absNorm (under ℤ I)
⊢ False
Module: Mathlib.RingTheory.Ideal.Int

Goal state before:
pp: S : Type u_2
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I : Ideal S
h✝ : Finite (S ⧸ I)
this : Fintype (S ⧸ I)
d : ℕ
h : ∀ (x : S ⧸ I), (Ideal.Quotient.mk I) ↑d * x = 0
⊢ (Ideal.Quotient.mk I) ↑d = 0

Tactic:
simpa using h 1

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

Goal state before:
pp: L : Type u_3
inst✝¹ : Field L
inst✝ : NumberField L
K₁ K₂ : IntermediateField ℚ L
h₁ : K₁.LinearDisjoint ↥K₂
h₂ : K₁ ⊔ K₂ = ⊤
h₃ :
  IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))
    (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
x✝ : Algebra (FractionRing (𝓞 ↥K₁)) (FractionRing (𝓞 L)) := FractionRing.liftAlgebra (𝓞 ↥K₁) (FractionRing (𝓞 L))
h_main : (discr L).natAbs = Ideal.absNorm (differentIdeal (𝓞 ↥K₂) (𝓞 L)) * (discr ↥K₂).natAbs ^ finrank (↥K₂) L
⊢ IsCoprime (Ideal.map (algebraMap (𝓞 ↥K₂) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₂)))
    (Ideal.map (algebraMap (𝓞 ↥K₁) (𝓞 L)) (differentIdeal ℤ (𝓞 ↥K₁)))

Tactic:
rwa [isCoprime_comm]

Goal state after: