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

Goal state before:
pp: Λ : ℂ → ℂ
hf : ∀ (s : ℂ), s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ Λ s
L : ℂ
h_lim : Tendsto (fun s ↦ s * Λ s) (𝓝[≠] 0) (𝓝 L)
s : ℂ
hs' : s ≠ 1
⊢ DifferentiableAt ℂ (Function.update (fun s ↦ Λ s / s.Gammaℝ) 0 (L / 2)) s

Tactic:
by
  have claim (t) (ht : t ≠ 0) (ht' : t ≠ 1) : DifferentiableAt ℂ (fun u : ℂ ↦ Λ u / Gammaℝ u) t :=
    (hf t ht ht').mul differentiable_Gammaℝ_inv.differentiableAt
  have claim2 : Tendsto (fun s : ℂ ↦ Λ s / Gammaℝ s) (𝓝[≠] 0) (𝓝 <| L / 2) := by
    refine Tendsto.congr' ?_ (h_lim.div Gammaℝ_residue_zero two_ne_zero)
    filter_upwards [self_mem_nhdsWithin] with s (hs : s ≠ 0)
    rw [Pi.div_apply, ← div_div, mul_div_cancel_left₀ _ hs]
  rcases ne_or_eq s 0 with hs | rfl
  · -- Easy case : `s ≠ 0`
    refine (claim s hs hs').congr_of_eventuallyEq ?_
    filter_upwards [isOpen_compl_singleton.mem_nhds hs] with x hx
    simp [Function.update_of_ne hx]
  · -- Hard case : `s = 0`
    simp_rw [← claim2.limUnder_eq]
    have S_nhds : {(1 : ℂ)}ᶜ ∈ 𝓝 (0 : ℂ) := isOpen_compl_singleton.mem_nhds hs'
    refine ((Complex.differentiableOn_update_limUnder_of_isLittleO S_nhds
      (fun t ht ↦ (claim t ht.2 ht.1).differentiableWithinAt) ?_) 0 hs').differentiableAt S_nhds
    simp only [Gammaℝ, zero_div, div_zero, Complex.Gamma_zero, mul_zero, sub_zero]
    -- Remains to show completed zeta is `o (s ^ (-1))` near 0.
    refine (isBigO_const_of_tendsto claim2 <| one_ne_zero' ℂ).trans_isLittleO ?_
    rw [isLittleO_iff_tendsto']
    · exact Tendsto.congr (fun x ↦ by rw [← one_div, one_div_one_div]) nhdsWithin_le_nhds
    · exact eventually_of_mem self_mem_nhdsWithin fun x hx hx' ↦ (hx <| inv_eq_zero.mp hx').elim

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

Goal state before:
pp: a b : UnitAddCircle
⊢ Differentiable ℂ fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s

Tactic:
intro z

Goal state after:
a b : UnitAddCircle
z : ℂ
⊢ DifferentiableAt ℂ (fun s ↦ hurwitzZetaEven a s - hurwitzZetaEven b s) z
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 * ↑(Int.sign 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:
Int.sign_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 + (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)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2 =
    ↑(SignType.sign (↑↑n + a)) / ↑|↑↑n + a| ^ s / 2 + ↑(SignType.sign (-↑(↑n + 1) + a)) / ↑|-↑(↑n + 1) + a| ^ s / 2

Tactic:
Int.cast_add,

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2 =
    ↑(SignType.sign (↑↑n + a)) / ↑|↑↑n + a| ^ s / 2 + ↑(SignType.sign (-(↑↑n + ↑1) + a)) / ↑|-(↑↑n + ↑1) + a| ^ s / 2
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ x.natAbs

Tactic:
apply Int.natCast_dvd.1

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ ↑2 ∣ x
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ 2 ∣ y.natAbs

Tactic:
apply Int.natCast_dvd.1

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hx : x % 2 = 0
hy : y % 2 = 0
⊢ ↑2 ∣ y
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: 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 + -I * ↑(Int.sign 0) * cexp (2 * ↑π * I * ↑a * ↑0) / ↑|0| ^ s / 2)
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)

Tactic:
simp_rw [abs_neg, Int.sign_neg, Int.cast_neg, Nat.abs_cast, Int.cast_natCast, mul_neg, abs_zero,
    Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs), div_zero, zero_div, add_zero] at this

Goal state after:
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)
⊢ HasSum (fun n ↦ ↑(Real.sin (2 * π * a * ↑n)) / ↑n ^ s) (sinZeta (↑a) s)
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
⊢ p ∣ 1

Tactic:
← h

Goal state after:
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
⊢ p ∣ m.gcd n
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:
by
  ext p
  simp [mem_normalizedFactors_iff', mem_primeFactors, ha, hb]

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))
⊢ 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)) / 2 % 2 = 0

Tactic:
Int.mul_ediv_cancel_left,

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))
⊢ 2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0) % 2 = 0

case H
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))
⊢ 2 ≠ 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 (b + c)

Tactic:
convert! IsCoprime.add_mul_left_right hbc.symm 1

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
⊢ c = c * 1
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
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
⊢ p ∣ 1

Tactic:
← h

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
⊢ p ∣ (m0 * 2 + 1).gcd (n0 * 2 + 1)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: m n : ℤ
h : m.gcd n = 1
hm : m % 2 = 1
hn : n % 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

Tactic:
obtain ⟨m0, hm2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hm)
  obtain ⟨n0, hn2⟩ := exists_eq_mul_left_of_dvd (Int.dvd_self_sub_of_emod_eq hn)
  rw [sub_eq_iff_eq_add] at hm2 hn2
  subst m
  subst n
  have h1 : (m0 * 2 + 1) ^ 2 + (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 + n0 ^ 2 + m0 + n0) + 1) := by
    ring
  have h2 : (m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2 = 2 * (2 * (m0 ^ 2 - n0 ^ 2 + m0 - n0)) := by ring
  have h3 : ((m0 * 2 + 1) ^ 2 - (n0 * 2 + 1) ^ 2) / 2 % 2 = 0 := by
    rw [h2, Int.mul_ediv_cancel_left, Int.mul_emod_right]
    decide
  refine ⟨⟨_, h1⟩, ⟨_, h2⟩, h3, ?_⟩
  have h20 : (2 : ℤ) ≠ 0 := by decide
  rw [h1, h2, Int.mul_ediv_cancel_left _ h20, Int.mul_ediv_cancel_left _ h20]
  by_contra h4
  obtain ⟨p, hp, hp1, hp2⟩ := Nat.Prime.not_coprime_iff_dvd.mp h4
  apply hp.not_dvd_one
  rw [← h]
  rw [← Int.natCast_dvd] at hp1 hp2
  apply Nat.dvd_gcd
  · apply Int.Prime.dvd_natAbs_of_coe_dvd_sq hp
    convert! dvd_add hp1 hp2
    ring
  · apply Int.Prime.dvd_natAbs_of_coe_dvd_sq hp
    convert! dvd_sub hp2 hp1
    ring

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 x : E
h : radical a * x = a
⊢ x = divRadical a

Tactic:
apply EuclideanDomain.eq_div_of_mul_eq_left radical_ne_zero
  rwa [mul_comm]

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

Goal state before:
pp: case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h : x * (algebraMap (𝓞 K) K) ((algebraMap ℤ (𝓞 K)) d) = (algebraMap (𝓞 K) K) a
⊢ ⟨d * ↑(Ideal.absNorm (↑I).num), ⋯⟩ • x = ↑(Ideal.absNorm (↑I).num) * (algebraMap (𝓞 K) K) a

Tactic:
← h

Goal state after:
case refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
I : (FractionalIdeal (𝓞 K)⁰ K)ˣ
x : K
a : 𝓞 K
d : ℤ
hd : d ∈ ↑ℤ⁰
h : x * (algebraMap (𝓞 K) K) ((algebraMap ℤ (𝓞 K)) d) = (algebraMap (𝓞 K) K) a
⊢ ⟨d * ↑(Ideal.absNorm (↑I).num), ⋯⟩ • x =
    ↑(Ideal.absNorm (↑I).num) * (x * (algebraMap (𝓞 K) K) ((algebraMap ℤ (𝓞 K)) d))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
⊢ h.IsPrimitiveClassified

Tactic:
rcases h.even_odd_of_coprime hc with h1 | h2

Goal state after:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ h.IsPrimitiveClassified

case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h : ↑φ = ↑ψ
⊢ φ = ψ

Tactic:
← Subtype.ext_iff

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h : φ = ψ
⊢ φ = ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2
⊢ ∑ j, ∑ i with mkComplex i = j, 1 = 2 * nrComplexPlaces K

Tactic:
simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones,
      Finset.mul_sum, Finset.sum_const, smul_eq_mul, mul_one]

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

Goal state before:
pp: case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h : ↑x✝¹ = ↑x✝
⊢ x✝¹ = x✝

Tactic:
← Subtype.ext_iff

Goal state after:
case e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
x✝¹ x✝ : { x // mkComplex x = ⟨w, hw⟩ }
h : x✝¹ = x✝
⊢ x✝¹ = x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Equiv.Perm.sign (Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯) = (-1) ^ nrComplexPlaces K

Tactic:
rw [Equiv.Perm.sign_of_pow_two_eq_one, Embeddings.card, ← card_add_two_mul_card_eq_rank,
    ← card_real_embeddings, Fintype.card, Fintype.card, Nat.add_sub_cancel_left,
    Nat.mul_div_cancel_left _ zero_lt_two]
  exact Equiv.ext (ComplexEmbedding.involutive_conjugate K).toPerm_involutive

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

Goal state before:
pp: case pos.a
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 →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ (x φ).im = Complex.im 0

Tactic:
· rw [Complex.zero_im, ← Complex.conj_eq_iff_im, canonicalEmbedding.conj_apply _ h_mem,
        ComplexEmbedding.isReal_iff.mp hφ]

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

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

Tactic:
by simpa using (isReal_mk_iff.not.2 hv)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ ‖x‖₊ = univ.sup fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯

Tactic:
have :
      (univ : Finset (InfinitePlace K)) =
      (univ.image (fun w : {w : InfinitePlace K // IsReal w} ↦ w.1)) ∪
      (univ.image (fun w : {w : InfinitePlace K // IsComplex w} ↦ w.1)) := by
    ext; simp [isReal_or_isComplex]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
this : univ = image (fun w ↦ ↑w) univ ∪ image (fun w ↦ ↑w) univ
⊢ ‖x‖₊ = univ.sup fun w ↦ NNReal.mk ((normAtPlace w) x) ⋯
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case pos
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:
rw [if_pos rfl] at h_le₀

Goal state after:
case pos
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| < ↑(NNReal.sqrt B) ^ 2
w : InfinitePlace K
h_eq : w = w₀
⊢ w ↑a < √(1 + ↑B ^ 2)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case pos
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ (neg ℝ).symm (x.1 w) = -x.1 w

Tactic:
symm_neg,

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
s : Set { w // w.IsReal }
x : mixedSpace K
w : { w // w.IsReal }
hw : w ∈ s
⊢ (neg ℝ) (x.1 w) = -x.1 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✝¹³ : IsFractionRing 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₂
inst✝ : Algebra.IsAlgebraic K L
σ : L →ₐ[K] L₂
this✝ : IsDomain A
this : IsLocalization (Algebra.algebraMapSubmonoid B A⁰) L
x : B
⊢ ((↑(galLift K L L₂ (galRestrict' A B B₂ σ))).comp (algebraMap B L)) x = ((↑σ).comp (algebraMap B L)) x

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

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

Goal state before:
pp: case inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
s t : Set { w // w.IsReal }
hst : s ≠ t
x✝ : mixedSpace K
hx : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) s
hx' : x✝ ∈ (fun s ↦ ⇑(negAt s) '' plusPart A) t
w : { w // w.IsReal }
hw : w ∈ t ∧ w ∉ s
⊢ False

Tactic:
exact lt_irrefl _ <|
      (neg_of_mem_negA_plusPart A hx' hw.1).trans (pos_of_notMem_negAt_plusPart A hx hw.2)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
h : minkowskiBound K 1 ≤ volume (convexBodySum K B)
⊢ ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(finrank ℚ K)) ^ finrank ℚ K

Tactic:
by
  obtain ⟨_, h_mem, h_nz, h_bd⟩ := exists_ne_zero_mem_ideal_of_norm_le K ↑1 h
  obtain ⟨a, rfl⟩ := (FractionalIdeal.mem_one_iff _).mp h_mem
  exact ⟨a, RingOfIntegers.coe_ne_zero_iff.mp h_nz, h_bd⟩

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

Goal state before:
pp: case e'_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ a (m + 1) = a m * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)

pp: case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)

Tactic:
· simp_rw [a, add_mul, one_mul, pow_succ, Nat.factorial_succ]
          field_simp
          simp [field, div_pow]
          ring

Goal state after:
case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : 1 < finrank ℚ K
a : ℕ → ℝ := fun n ↦ ↑n ^ (n * 2) / ((4 / π) ^ n * ↑n.factorial ^ 2)
n m : ℕ
hmn✝ : 2 ≤ m
h_m : 4 / 9 * (3 * π / 4) ^ m ≤ a m
this : 3 ≤ (1 + 1 / ↑m) ^ (2 * m)
⊢ 4 / 9 * (3 * π / 4) ^ (m + 1) ≤ a m * (1 + 1 / ↑m) ^ (2 * m) / (4 / π)
Module: Mathlib.RingTheory.FractionalIdeal.Extended

Goal state before:
pp: 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
x : K
x✝ : L
⊢ x✝ ∈ extended L hf (spanSingleton M x) ↔ x✝ ∈ spanSingleton N ((IsLocalization.map L f hf) x)

Tactic:
rw [mem_extended_iff, mem_spanSingleton, ← mem_span_singleton]

Goal state after:
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
x : K
x✝ : L
⊢ x✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑(spanSingleton M x)) ↔ x✝ ∈ B ∙ (IsLocalization.map L f hf) x
Module: Mathlib.RingTheory.DedekindDomain.Instances

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
inst✝¹¹ : Algebra R Rₘ
inst✝¹⁰ : IsTorsionFree R S
inst✝⁹ : Algebra.IsSeparable K L
M : Submonoid R
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra (FractionRing Rₘ) (FractionRing Sₘ)
inst✝ : IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : algebraMapSubmonoid S M ≤ S⁰
f₁ : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
f₂ : Sₘ →+* L := IsLocalization.map L (RingHom.id S) hM'
algInst✝¹ : Algebra Rₘ K := f₁.toAlgebra
algInst✝ : Algebra Sₘ L := f₂.toAlgebra
this✝³ : IsScalarTower R Rₘ K
this✝² : IsScalarTower S Sₘ L
this✝¹ : IsFractionRing Rₘ K
this✝ : IsFractionRing Sₘ L
this : IsDomain Rₘ
x✝ : R
⊢ (algebraMap Rₘ (FractionRing Sₘ)) ((algebraMap R Rₘ) x✝) = (algebraMap R (FractionRing Sₘ)) x✝

Tactic:
← algebraMap_apply

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁸ : CommRing R
inst✝¹⁷ : CommRing S
inst✝¹⁶ : IsDomain R
inst✝¹⁵ : IsDomain S
inst✝¹⁴ : Algebra R S
Rₘ : Type u_4
Sₘ : Type u_5
inst✝¹³ : CommRing Rₘ
inst✝¹² : CommRing Sₘ
inst✝¹¹ : Algebra R Rₘ
inst✝¹⁰ : IsTorsionFree R S
inst✝⁹ : Algebra.IsSeparable K L
M : Submonoid R
inst✝⁸ : IsLocalization M Rₘ
inst✝⁷ : Algebra Rₘ Sₘ
inst✝⁶ : Algebra S Sₘ
inst✝⁵ : Algebra R Sₘ
inst✝⁴ : IsScalarTower R Rₘ Sₘ
inst✝³ : IsScalarTower R S Sₘ
inst✝² : IsLocalization (algebraMapSubmonoid S M) Sₘ
inst✝¹ : Algebra (FractionRing Rₘ) (FractionRing Sₘ)
inst✝ : IsScalarTower Rₘ (FractionRing Rₘ) (FractionRing Sₘ)
hM : M ≤ R⁰
M' : Submonoid S := algebraMapSubmonoid S M
hM' : algebraMapSubmonoid S M ≤ S⁰
f₁ : Rₘ →+* K := IsLocalization.map K (RingHom.id R) hM
f₂ : Sₘ →+* L := IsLocalization.map L (RingHom.id S) hM'
algInst✝¹ : Algebra Rₘ K := f₁.toAlgebra
algInst✝ : Algebra Sₘ L := f₂.toAlgebra
this✝³ : IsScalarTower R Rₘ K
this✝² : IsScalarTower S Sₘ L
this✝¹ : IsFractionRing Rₘ K
this✝ : IsFractionRing Sₘ L
this : IsDomain Rₘ
x✝ : R
⊢ (algebraMap R (FractionRing Sₘ)) x✝ = (algebraMap R (FractionRing Sₘ)) x✝
Module: Mathlib.RingTheory.Ideal.Norm.RelNorm

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
inst✝⁷ : IsDomain R
S : Type u_3
inst✝⁶ : CommRing S
inst✝⁵ : IsDomain S
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsIntegrallyClosed S
inst✝² : Algebra R S
inst✝¹ : Module.Finite R S
inst✝ : IsTorsionFree R S
I : Ideal S
⊢ spanNorm R I = ⊥ ↔ I = ⊥

Tactic:
simp only [spanNorm, span_eq_bot, Set.mem_image, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂, Algebra.intNorm_eq_zero, @eq_bot_iff _ _ _ I, SetLike.le_def, map,
    mem_bot]

Goal state after: