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

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ {
      re :=
        { re := -↑x, im := ↑y }.re * { re := ↑z, im := -↑w }.re +
          ↑d * { re := -↑x, im := ↑y }.im * { re := ↑z, im := -↑w }.im,
      im :=
        { re := -↑x, im := ↑y }.re * { re := ↑z, im := -↑w }.im +
          { re := -↑x, im := ↑y }.im * { re := ↑z, im := -↑w }.re } =
    { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }

Tactic:
by simp [add_comm]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ {
      re :=
        { re := ↑x, im := -↑y }.re * { re := -↑z, im := ↑w }.re +
          ↑d * { re := ↑x, im := -↑y }.im * { re := -↑z, im := ↑w }.im,
      im :=
        { re := ↑x, im := -↑y }.re * { re := -↑z, im := ↑w }.im +
          { re := ↑x, im := -↑y }.im * { re := -↑z, im := ↑w }.re } =
    { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }

Tactic:
by simp [add_comm]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ {
      re :=
        { re := ↑x, im := -↑y }.re * { re := ↑z, im := -↑w }.re +
          ↑d * { re := ↑x, im := -↑y }.im * { re := ↑z, im := -↑w }.im,
      im :=
        { re := ↑x, im := -↑y }.re * { re := ↑z, im := -↑w }.im +
          { re := ↑x, im := -↑y }.im * { re := ↑z, im := -↑w }.re } =
    { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }

Tactic:
by simp [add_comm]

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
N : Submonoid M
⊢ Function.Surjective ⇑(domRestrictHom N R)

Tactic:
intro χ
  obtain ⟨ψ, hψ⟩ := (χ.toUnitHom.comp N.unitsEquivUnitsType).domRestrict_surjective R N.units
  refine ⟨MulChar.ofUnitHom ψ, ext fun _ ↦ ?_⟩
  rw [MonoidHom.domRestrictHom_apply] at hψ
  rw [domRestrictHom_apply, domRestrict_ofUnitHom]
  simp [hψ]

Goal state after:
Module: Mathlib.NumberTheory.MulChar.Duality

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝³ : CommMonoid M
inst✝² : CommRing R
inst✝¹ : Finite M
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)
m : Mˣ
χ : MulChar M R
⊢ ((mulCharEquiv M R).symm m) χ = χ ↑m

Tactic:
by
  classical
  rw [show ((mulCharEquiv M R).symm m) χ =
    if IsUnit χ then ↑(mulEquivToUnitHom χ m) else (0 : R) by rfl, if_pos (Group.isUnit χ),
    mulEquivToUnitHom_apply, coe_equivToUnitHom]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #(N.smoothNumbersUpTo k) + #(N.roughNumbersUpTo k) = N

Tactic:
smoothNumbersUpTo,

Goal state after:
N k : ℕ
⊢ #({n ∈ Finset.range (N + 1) | n ∈ k.smoothNumbers}) + #(N.roughNumbersUpTo k) = N
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
x0 : y = 0
⊢ z % y = z

pp: case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
hl : z < y
⊢ z % y = z

Tactic:
· rw [x0, mod_zero]

Goal state after:
case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
hl : z < y
⊢ z % y = z
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime 0 v
hf : u - ⌊ξ⌋ * v = 0
⊢ False

Tactic:
simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop

Goal state after:
case refine_1
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = 0
huv_cop : v = 1 ∨ v = -1
⊢ False
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
huv_cop : IsCoprime v v
hf : u - ⌊ξ⌋ * v = v
⊢ False

Tactic:
simp only [isCoprime_zero_left, isCoprime_self, isUnit_iff] at huv_cop

Goal state after:
case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
hu₁ : u - ⌊ξ⌋ * v ≤ v
hf : u - ⌊ξ⌋ * v = v
huv_cop : v = 1 ∨ v = -1
⊢ False
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_3
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑↑q.den
hq₁ : 0 < 2 * ↑↑q.den - 1
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹

Tactic:
replace hq₁ := mul_pos hq₀ hq₁

Goal state after:
case refine_3
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
hq₀ : 0 < ↑↑q.den
hq₁ : 0 < ↑↑q.den * (2 * ↑↑q.den - 1)
⊢ |ξ - ↑q.num / ↑↑q.den| < (↑↑q.den * (2 * ↑↑q.den - 1))⁻¹
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
norm_jacobiTheta₂_term,

Goal state after:
S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ rexp (-π * ↑n ^ 2 * τ.im - 2 * π * ↑n * z.im) ≤ rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖(P.ε⁻¹ * ↑(x ^ P.k)) • (P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀)‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖

Tactic:
norm_smul,

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.ε⁻¹ * ↑(x ^ P.k)‖ * ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖
⊢ ‖P.f x - (P.ε * ↑(x ^ (-P.k))) • P.g₀‖ ≤ ‖P.ε‖ * C * ‖x ^ r‖
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * ‖x ^ r‖ = C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖

Tactic:
simp_rw [norm_mul, norm_real, one_div, inv_rpow hx.le, rpow_neg hx.le, inv_inv, norm_inv,
      norm_of_nonneg (rpow_pos_of_pos hx _).le, rpow_add hx]

Goal state after:
case e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
r C : ℝ
hC :
  ∀ᶠ (x : ℝ) in 𝓝 0,
    x ∈ Ioi 0 → ‖((fun x ↦ P.g x - P.g₀) ∘ fun x ↦ x⁻¹) x‖ ≤ C * ‖((fun x ↦ x ^ (-(r + P.k))) ∘ fun x ↦ x⁻¹) x‖
x : ℝ
hx : 0 < x
h_nv2 : ↑(x ^ P.k) ≠ 0
h_nv : P.ε⁻¹ * ↑(x ^ P.k) ≠ 0
hC' : ‖P.f x - (P.ε⁻¹ * ↑(x ^ P.k))⁻¹ • P.g₀‖ ≤ C * ‖(1 / x) ^ (-(r + P.k))‖ / ‖P.ε⁻¹ * ↑(x ^ P.k)‖
⊢ ‖P.ε‖ * C * x ^ r = C * (x ^ r * x ^ P.k) / (‖P.ε‖⁻¹ * x ^ P.k)
Module: Mathlib.NumberTheory.LSeries.AbstractFuncEq

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ ‖P.ε • ↑(x ^ (-P.k)) • P.g₀‖) =O[𝓝[>] 0] fun x ↦ ‖x ^ (-P.k)‖

Tactic:
norm_smul,

Goal state after:
case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
P : WeakFEPair E
⊢ (fun x ↦ ‖P.ε‖ * (‖↑(x ^ (-P.k))‖ * ‖P.g₀‖)) =O[𝓝[>] 0] fun x ↦ ‖x ^ (-P.k)‖
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: case refine_2.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ ‖jacobiTheta₂_term x z τ‖
⊢ False

Tactic:
norm_jacobiTheta₂_term,

Goal state after:
case refine_2.inr
z τ : ℂ
hτ✝ : τ.im ≤ 0
hτ : τ.im = 0
h : Summable fun x ↦ rexp (-π * ↑x ^ 2 * τ.im - 2 * π * ↑x * z.im)
⊢ False
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
n : ℤ
⊢ ‖f_int k a t n‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) n‖

Tactic:
rcases n with - | m

Goal state after:
case ofNat
k : ℕ
a t : ℝ
ht : 0 < t
a✝ : ℕ
⊢ ‖f_int k a t (Int.ofNat a✝)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.ofNat a✝)‖

case negSucc
k : ℕ
a t : ℝ
ht : 0 < t
m : ℕ
⊢ ‖f_int k a t (Int.negSucc m)‖ = ‖(fun t_1 ↦ Int.rec (f_nat k a t) (f_nat k (1 - a) t) t_1) (Int.negSucc m)‖
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

Tactic:
rcases le_or_gt x 0 with hx | hx

Goal state after:
case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)

case inr
a : UnitAddCircle
x : ℝ
hx : 0 < x
⊢ evenKernel a x = 1 / x ^ (1 / 2) * cosKernel a (1 / x)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: a x : ℝ
⊢ ↑(oddKernel (↑a) x) =
    cexp (-↑π * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * I * ↑x) (I * ↑x) / (2 * ↑π * I) + ↑a * jacobiTheta₂ (↑a * I * ↑x) (I * ↑x))

Tactic:
by
  rw [oddKernel_def, jacobiTheta₂'', ← mul_assoc ↑a I x,
    (by ring : ↑π * I * ↑a ^ 2 * (I * ↑x) = I ^ 2 * ↑π * ↑a ^ 2 * x), I_sq, neg_one_mul]

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

Goal state before:
pp: a : UnitAddCircle
x : ℝ
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)

Tactic:
rcases le_or_gt x 0 with hx | hx

Goal state after:
case inl
a : UnitAddCircle
x : ℝ
hx : x ≤ 0
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)

case inr
a : UnitAddCircle
x : ℝ
hx : 0 < x
⊢ oddKernel a x = 1 / x ^ (3 / 2) * sinKernel a (1 / x)
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: case e'_5
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 1 / (↑n + ↑a) ^ s = (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2 + (1 / (↑n + ↑a) ^ s - 1 / (↑n + 1 - ↑a) ^ s) / 2

Tactic:
apply show ∀ (x y : ℂ), x = (x + y) / 2 + (x - y) / 2 by intros; ring

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

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ riemannZeta s = ∑' (n : ℕ), 1 / (↑n + 1) ^ s

Tactic:
have := zeta_eq_tsum_one_div_nat_cpow hs
  rw [Summable.tsum_eq_zero_add] at this
  · simpa [zero_cpow (Complex.ne_zero_of_one_lt_re hs)]
  · rwa [Complex.summable_one_div_nat_cpow]

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

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

Tactic:
have hc (n : ℤ) : ‖c n‖ = 1 / 2 := by
    simp_rw [c, (by { push_cast; ring } : 2 * π * I * a * n = ↑(2 * π * a * n) * I), norm_div,
      RCLike.norm_ofNat, norm_mul, norm_neg, norm_I, one_mul, norm_exp_ofReal_mul_I]

Goal state after:
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ -I * cexp (2 * ↑π * I * ↑a * ↑n) / 2
hc : ∀ (n : ℤ), ‖c n‖ = 1 / 2
⊢ HasSum (fun n ↦ (s + 1).Gammaℝ * -I * ↑n.sign * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedSinZeta (↑a) s)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
this : cosZeta a (1 - s) = completedCosZeta a (1 - s) * (1 - s).Gammaℝ⁻¹
n : ℕ
⊢ s ≠ -↑n

Tactic:
by simpa using hs (n + 1)

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

Goal state before:
pp: a b c : ℤ
h : Fermat42 a b c
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0

Tactic:
obtain ⟨a0, b0, c0, hf, hc⟩ := exists_odd_minimal h

Goal state after:
a b c : ℤ
h : Fermat42 a b c
a0 b0 c0 : ℤ
hf : Minimal a0 b0 c0
hc : a0 % 2 = 1
⊢ ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 ∧ 0 < c0
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ ↑(x.gcd y) ∣ z

Tactic:
obtain ⟨hx, hy⟩ := Int.gcd_eq_zero_iff.mp h0
    have hz : z = 0 := by
      simpa only [PythagoreanTriple, hx, hy, add_zero, zero_eq_mul, mul_zero,
        or_self_iff] using h
    simp [h0, hz]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ (0 = 1 ^ 2 - 0 ^ 2 ∧ y = 2 * 1 * 0 ∨ 0 = 2 * 1 * 0 ∧ y = 1 ^ 2 - 0 ^ 2) ∧
    Int.gcd 1 0 = 1 ∧ (1 % 2 = 0 ∧ 0 % 2 = 1 ∨ 1 % 2 = 1 ∧ 0 % 2 = 0)

Tactic:
hy,

Goal state after:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = ↑y.natAbs
⊢ (0 = 1 ^ 2 - 0 ^ 2 ∧ ↑y.natAbs = 2 * 1 * 0 ∨ 0 = 2 * 1 * 0 ∧ ↑y.natAbs = 1 ^ 2 - 0 ^ 2) ∧
    Int.gcd 1 0 = 1 ∧ (1 % 2 = 0 ∧ 0 % 2 = 1 ∨ 1 % 2 = 1 ∧ 0 % 2 = 0)
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ (0 = 0 ^ 2 - 1 ^ 2 ∧ y = 2 * 0 * 1 ∨ 0 = 2 * 0 * 1 ∧ y = 0 ^ 2 - 1 ^ 2) ∧
    Int.gcd 0 1 = 1 ∧ (0 % 2 = 0 ∧ 1 % 2 = 1 ∨ 0 % 2 = 1 ∧ 1 % 2 = 0)

Tactic:
hy,

Goal state after:
case h
y z : ℤ
h : PythagoreanTriple 0 y z
hc : y.natAbs = 1
hy : y = -↑y.natAbs
⊢ (0 = 0 ^ 2 - 1 ^ 2 ∧ -↑y.natAbs = 2 * 0 * 1 ∨ 0 = 2 * 0 * 1 ∧ -↑y.natAbs = 0 ^ 2 - 1 ^ 2) ∧
    Int.gcd 0 1 = 1 ∧ (0 % 2 = 0 ∧ 1 % 2 = 1 ∨ 0 % 2 = 1 ∧ 1 % 2 = 0)
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 : M
ha₀ : a ≠ 0
x : M
hx : x ∈ ↑(primeFactors a)
y : M
hy : y ∈ ↑(primeFactors a)
hxy : x ≠ y
⊢ IsRelPrime x y

Tactic:
simp only [Finset.mem_coe, mem_primeFactors, mem_normalizedFactors_iff' ha₀] at hx hy

Goal state after:
case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha₀ : a ≠ 0
x y : M
hxy : x ≠ y
hx : Irreducible x ∧ normalize x = x ∧ x ∣ a
hy : Irreducible y ∧ normalize y = y ∧ y ∣ a
⊢ IsRelPrime x y
Module: Mathlib.RingTheory.Radical.Basic

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

Tactic:
rw [mul_comm]

Goal state after:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

Tactic:
rwa [← isComplex_mk_iff]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
⊢ ζ ∈ rootsOfUnity (↑k) (𝓞 K) ↔ ζ = 1

Tactic:
rw [mem_rootsOfUnity]

Goal state after:
K : Type u_1
inst✝ : Field K
k : ℕ+
hc : (↑k).Coprime (torsionOrder K)
ζ : (𝓞 K)ˣ
⊢ ζ ^ ↑k = 1 ↔ ζ = 1
Module: Mathlib.NumberTheory.NumberField.Units.Basic

Goal state before:
pp: case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  ((torsion K).equivMapOfInjective (Units.complexEmbedding φ) ⋯).symm.toEquiv
⊢ torsionOrder K ≤ Nat.card ↥(torsion K)

Tactic:
torsionOrder

Goal state after:
case hcard
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
φ : K →+* ℂ
e : ↥(Subgroup.map (Units.complexEmbedding φ) (torsion K)) ≃ ↥(torsion K) :=
  ((torsion K).equivMapOfInjective (Units.complexEmbedding φ) ⋯).symm.toEquiv
⊢ Nat.card ↥(torsion K) ≤ Nat.card ↥(torsion K)
Module: Mathlib.NumberTheory.NumberField.Units.Basic

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

Tactic:
by_cases! hc : 2 < orderOf (x : (𝓞 K)ˣ)

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

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h : Odd (Module.finrank ℚ K)
x : ↥(torsion K)
hc : orderOf ↑x ≤ 2
⊢ ↑x = 1 ∨ ↑x = -1
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ star (x✝ b✝) * x✝ a✝ = x✝ a✝ * x✝ b✝

Tactic:
hy,

Goal state after:
F : Type u_1
inst✝¹ : Field F
K : Type u_2
inst✝ : Field K
a✝ b✝ : K
hx : a✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
hy : b✝ ∈ {x | ∀ (φ : K →+* ℂ), star (φ x) = φ x}
x✝ : K →+* ℂ
⊢ x✝ b✝ * x✝ a✝ = x✝ a✝ * x✝ b✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: k : Type u_1
inst✝¹ : Field k
K : Type u_2
inst✝ : Field K
f : k →+* K
w : InfinitePlace K
h : (w.comap f).IsReal
⊢ ComplexEmbedding.IsReal (w.embedding.comp f)

Tactic:
rwa [← isReal_mk_iff, ← comap_mk, mk_embedding]

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

Goal state before:
pp: case refine_1
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ Function.Injective (Quotient.lift (fun x ↦ x.comap (algebraMap k K)) ⋯)

pp: case refine_2
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ Function.Surjective (Quotient.lift (fun x ↦ x.comap (algebraMap k K)) ⋯)

Tactic:
· rintro ⟨w⟩ ⟨w'⟩ e
    exact Quotient.sound (mem_orbit_iff.mpr e.symm)

Goal state after:
case refine_2
k : Type u_1
inst✝⁴ : Field k
K : Type u_2
inst✝³ : Field K
F : Type u_3
inst✝² : Field F
inst✝¹ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
inst✝ : IsGalois k K
⊢ Function.Surjective (Quotient.lift (fun x ↦ x.comap (algebraMap k K)) ⋯)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case neg
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 φ = 0

Tactic:
have := congrFun (congrArg (fun x => x.2) h_zero) ⟨InfinitePlace.mk φ, ⟨φ, hφ, rfl⟩⟩

Goal state after:
case neg
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 φ
this : ((commMap K) x).2 ⟨InfinitePlace.mk φ, ⋯⟩ = 0.2 ⟨InfinitePlace.mk φ, ⋯⟩
⊢ x φ = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case refine_1.fst
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
w : { w // w.IsReal }
⊢ x.1 w = 0.1 w

pp: case refine_1.snd
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
w : { w // w.IsComplex }
⊢ x.2 w = 0.2 w

Tactic:
· exact norm_eq_zero.mp (normAtPlace_apply_of_isReal w.prop _ ▸ h w.1)

Goal state after:
case refine_1.snd
K : Type u_1
inst✝ : Field K
x : mixedSpace K
h : ∀ (w : InfinitePlace K), (normAtPlace w) x = 0
w : { w // w.IsComplex }
⊢ x.2 w = 0.2 w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
⊢ volume (convexBodySum K B) = 0

Tactic:
suffices convexBodySum K B = { 0 } by rw [this, measure_singleton]

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB✝ : B ≤ 0
hB : B = 0
⊢ convexBodySum K B = {0}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
⊢ IsCompact (convexBodySum K B)

Tactic:
classical
  rw [Metric.isCompact_iff_isClosed_bounded]
  refine ⟨?_, convexBodySum_isBounded K B⟩
  convert! IsClosed.preimage (convexBodySumFun_continuous K) (isClosed_Icc : IsClosed (Set.Icc 0 B))
  ext
  simp [convexBodySumFun_nonneg]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ volume (convexBodySum K B) = ↑(convexBodySumFactor K) * ENNReal.ofReal B ^ finrank ℚ K

Tactic:
rw [mul_comm]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
this : volume (convexBodySum K 1) = ↑(convexBodySumFactor K)
⊢ volume (convexBodySum K B) = ENNReal.ofReal B ^ finrank ℚ K * ↑(convexBodySumFactor K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ mixedEmbedding.norm (c • 1) = |c| ^ finrank ℚ K

Tactic:
norm_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
⊢ |c| ^ finrank ℚ K * mixedEmbedding.norm 1 = |c| ^ finrank ℚ K
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
hw : ¬IsUnramified k w
⊢ Even (finrank k K)

Tactic:
by
  by_cases FiniteDimensional k K
  · exact IsGalois.card_aut_eq_finrank k K ▸ even_card_aut_of_not_isUnramified hw
  · exact finrank_of_not_finite ‹_› ▸ Even.zero

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (∫ (x : { w // w.IsReal } → ℝ), ∏ w, rexp (-‖x w‖)) * ∫ (x : { w // w.IsComplex } → ℂ), ∏ w, rexp (-2 * ‖x w‖) =
    (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K

Tactic:
rw [integral_fintype_prod_volume_eq_pow (fun x => exp (-‖x‖)),
          integral_fintype_prod_volume_eq_pow (fun x => exp (-2 * ‖x‖))]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ (∫ (x : ℝ), rexp (-‖x‖)) ^ card { w // w.IsReal } * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ card { w // w.IsComplex } =
    (∫ (x : ℝ), rexp (-|x|)) ^ nrRealPlaces K * (∫ (x : ℂ), rexp (-2 * ‖x‖)) ^ nrComplexPlaces K