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

Goal state before:
pp: case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
⊢ ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = Real.Gamma s.re / p i ^ s.re

Tactic:
have := Real.integral_rpow_mul_exp_neg_mul_Ioi hs hpi

Goal state after:
case e'_5.inr.e_a
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), a i = 0 ∨ 0 < p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ a i * ↑(rexp (-p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
i : ι
hpi : 0 < p i
this : ∫ (t : ℝ) in Ioi 0, t ^ (s.re - 1) * rexp (-(p i * t)) = (1 / p i) ^ s.re * Real.Gamma s.re
⊢ ‖∫ (a : ℝ) in Ioi 0, ‖↑a ^ (s - 1) * ↑(rexp (-p i * a))‖ ∂volume‖ = Real.Gamma s.re / p i ^ s.re
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

Goal state before:
pp: z τ : ℂ
⊢ (starRingEnd ℂ) (jacobiTheta₂'' z τ) = jacobiTheta₂'' ((starRingEnd ℂ) z) (-(starRingEnd ℂ) τ)

Tactic:
by
  simp [jacobiTheta₂'', jacobiTheta₂'_conj, jacobiTheta₂_conj, ← exp_conj, map_ofNat, div_neg,
    neg_div, jacobiTheta₂'_neg_left]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)

Tactic:
rcases le_or_gt (im τ) 0 with hτ | hτ

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

case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂ z τ = 1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) * jacobiTheta₂ (z / τ) (-1 / τ)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: z τ : ℂ
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))

Tactic:
rcases le_or_gt (im τ) 0 with hτ | hτ

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

case inr
z τ : ℂ
hτ : 0 < τ.im
⊢ jacobiTheta₂' z τ =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 / τ) / τ *
      (jacobiTheta₂' (z / τ) (-1 / τ) - 2 * ↑π * I * z * jacobiTheta₂ (z / τ) (-1 / τ))
Module: Mathlib.NumberTheory.LSeries.HurwitzZeta

Goal state before:
pp: a : UnitAddCircle
s : ℂ
⊢ sinZeta a s = (expZeta a s - expZeta (-a) s) / (2 * I)

Tactic:
rw [expZeta, expZeta, cosZeta_neg, sinZeta_neg]
  field

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

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

Tactic:
hurwitzZetaOdd_neg,

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s +
      I * (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.sin (↑π * s / 2) * hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-↑π * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
⊢ LSeriesSummable ((fun n ↦ χ ↑n) * f) s

Tactic:
refine .of_norm <| h.norm.of_nonneg_of_le (fun _ ↦ norm_nonneg _) fun n ↦ norm_term_le s ?_

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
f : ℕ → ℂ
s : ℂ
h : LSeriesSummable f s
n : ℕ
⊢ ‖((fun n ↦ χ ↑n) * f) n‖ ≤ ‖f n‖
Module: Mathlib.NumberTheory.FLT.Basic

Goal state before:
pp: n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
⊢ False

Tactic:
obtain hn | hn := n.even_or_odd

Goal state after:
case inl
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Even n
⊢ False

case inr
n : ℕ
h : FermatLastTheoremWith ℕ n
a b c : ℤ
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
habc : a ^ n + b ^ n = c ^ n
hn : Odd n
⊢ False
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

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

Tactic:
by
  simp [completedHurwitzZetaOdd, (isStrong_hurwitzOddFEPair _).Λ_eq, mellin,
    oddKernel_neg, integral_neg, neg_div]

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

Goal state before:
pp: a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedCosZeta a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) =
    2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * Complex.cos (↑π * s / 2) * (completedCosZeta a s / s.Gammaℝ)

Tactic:
← Gammaℂ

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
hs' : a ≠ 0 ∨ s ≠ 1
this : hurwitzZetaEven a (1 - s) = completedHurwitzZetaEven a (1 - s) * (1 - s).Gammaℝ⁻¹
⊢ completedCosZeta a s * (s.Gammaℂ * Complex.cos (↑π * s / 2) * s.Gammaℝ⁻¹) =
    s.Gammaℂ * Complex.cos (↑π * s / 2) * (completedCosZeta a s / s.Gammaℝ)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

Tactic:
← Gammaℂ

Goal state after:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
⊢ cosZeta a (1 - s) = s.Gammaℂ * Complex.cos (↑π * s / 2) * hurwitzZetaEven a s
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 ∧ ↑1 = 2 * 1 * 0 ∨ 0 = 2 * 1 * 0 ∧ ↑1 = 1 ^ 2 - 0 ^ 2) ∧
    Int.gcd 1 0 = 1 ∧ (1 % 2 = 0 ∧ 0 % 2 = 1 ∨ 1 % 2 = 1 ∧ 0 % 2 = 0)

Tactic:
Int.gcd_zero_right

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 ∧ ↑1 = 2 * 1 * 0 ∨ 0 = 2 * 1 * 0 ∧ ↑1 = 1 ^ 2 - 0 ^ 2) ∧
    Int.natAbs 1 = 1 ∧ (1 % 2 = 0 ∧ 0 % 2 = 1 ∨ 1 % 2 = 1 ∧ 0 % 2 = 0)
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
p : M
⊢ p ∈ primeFactors (a * b) ↔ p ∈ primeFactors a ∪ primeFactors b

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

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

Goal state before:
pp: case inr.refine_1.inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
x✝ : ∃ n, a ∣ b ^ n
hdvd : a ∣ b ^ 0
⊢ radical a ∣ b

pp: case inr.refine_1.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
x✝ : ∃ n, a ∣ b ^ n
n : ℕ
hdvd : a ∣ b ^ n
hn : n ≠ 0
⊢ radical a ∣ b

Tactic:
· simp [radical_of_isUnit <| isUnit_of_dvd_one <| pow_zero b ▸ hdvd]

Goal state after:
case inr.refine_1.inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
x✝ : ∃ n, a ∣ b ^ n
n : ℕ
hdvd : a ∣ b ^ n
hn : n ≠ 0
⊢ radical a ∣ b
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = RingHom.id ℂ
z : ↥K
⊢ (↑↑ψ).toFun z = K.subtype z

Tactic:
convert! RingHom.congr_fun h z using 1

Goal state after:
case e'_2
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = RingHom.id ℂ
z : ↥K
⊢ (↑↑ψ).toFun z = ψ₁ ↑z
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
z : ↥K
⊢ (↑↑ψ).toFun z = (⇑(starRingEnd ℂ) ∘ ⇑K.subtype) z

Tactic:
convert! RingHom.congr_fun h z using 1

Goal state after:
case e'_2
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
z : ↥K
⊢ (↑↑ψ).toFun z = ψ₁ ↑z
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_1
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
⊢ DenseRange ι

Tactic:
· let j : { x // x ∈ closure (id '' K) } → (K.topologicalClosure : Set ℂ) :=
      fun x =>
      ⟨x, by
        convert! x.prop
        simp only [id, Set.image_id']
        rfl ⟩
    convert!
      DenseRange.comp (Function.Surjective.denseRange _) (IsDenseEmbedding.id.subtype (· ∈ K)).dense
        (by fun_prop : Continuous j)
    rintro ⟨y, hy⟩
    use
      ⟨y, by
        convert! hy
        simp only [id, Set.image_id']
        rfl ⟩

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ (mk (ComplexEmbedding.conjugate φ)) x = (mk φ) x

Tactic:
apply,

Goal state after:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ ‖(ComplexEmbedding.conjugate φ) x‖ = (mk φ) x
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ ‖(ComplexEmbedding.conjugate φ) x‖ = (mk φ) x

Tactic:
apply,

Goal state after:
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ ‖(ComplexEmbedding.conjugate φ) x‖ = ‖φ x‖
Module: Mathlib.NumberTheory.PythagoreanTriples

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

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

Tactic:
· apply And.intro h_odd.1
      apply And.intro h_odd.2
      rcases ht2 with h_pos | h_neg
      · apply And.intro h_pos (And.intro ht3 (And.intro ht4 hm))
      · exfalso
        revert h_pos
        rw [h_neg]
        exact imp_false.mpr (not_lt.mpr (neg_nonpos.mpr (by positivity)))

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x : ℚ
⊢ v ↑x = ‖x‖

Tactic:
rcases v with ⟨_, _⟩

Goal state after:
K : Type u_1
inst✝ : Field K
x : ℚ
val✝ : AbsoluteValue K ℝ
property✝ : ∃ φ, place φ = val✝
⊢ ⟨val✝, property✝⟩ ↑x = ‖x‖
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
n : ℕ
⊢ v ↑n = ↑n

Tactic:
rcases v with ⟨_, _⟩

Goal state after:
K : Type u_1
inst✝ : Field K
n : ℕ
val✝ : AbsoluteValue K ℝ
property✝ : ∃ φ, place φ = val✝
⊢ ⟨val✝, property✝⟩ ↑n = ↑n
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
z : ℤ
⊢ v ↑z = ‖z‖

Tactic:
rcases v with ⟨_, _⟩

Goal state after:
K : Type u_1
inst✝ : Field K
z : ℤ
val✝ : AbsoluteValue K ℝ
property✝ : ∃ φ, place φ = val✝
⊢ ⟨val✝, property✝⟩ ↑z = ‖z‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ (∀ (x_1 : InfinitePlace K), x_1.IsReal ∨ x_1.IsComplex → ‖x_1.embedding x‖ < ↑(f x_1)) ↔
    ∀ (w : InfinitePlace K), w x < ↑(f w)

Tactic:
← not_isReal_iff_isComplex,

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
x : K
⊢ (∀ (x_1 : InfinitePlace K), x_1.IsReal ∨ ¬x_1.IsReal → ‖x_1.embedding x‖ < ↑(f x_1)) ↔
    ∀ (w : InfinitePlace K), w x < ↑(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
⊢ E ⊔ F ≤ maximalRealSubfield K

Tactic:
sup_le_iff,

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
⊢ E ≤ maximalRealSubfield K ∧ F ≤ maximalRealSubfield K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      x.2 ⟨a, b⟩ ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
⊢ (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      -x.2 ⟨a, b⟩ ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)

Tactic:
convert! hx using 3

Goal state after:
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
x : mixedSpace K
hx :
  (∀ (a : InfinitePlace K) (b : a.IsReal), |x.1 ⟨a, b⟩| < ↑(f a)) ∧
    ∀ (a : InfinitePlace K) (b : a.IsComplex),
      x.2 ⟨a, b⟩ ∈ if ⟨a, b⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a) ^ 2} else ball 0 ↑(f a)
a✝¹ : InfinitePlace K
a✝ : a✝¹.IsComplex
⊢ (-x.2 ⟨a✝¹, a✝⟩ ∈ if ⟨a✝¹, a✝⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a✝¹) ^ 2} else ball 0 ↑(f a✝¹)) ↔
    x.2 ⟨a✝¹, a✝⟩ ∈ if ⟨a✝¹, a✝⟩ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f a✝¹) ^ 2} else ball 0 ↑(f a✝¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ (Finset.univ.sup fun b ↦ ‖(canonicalEmbedding K) x b‖₊) = Finset.univ.sup fun φ ↦ ‖φ x‖₊

Tactic:
apply_at

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
r : ℝ
⊢ ‖(canonicalEmbedding K) x‖ ≤ r ↔ ∀ (φ : K →+* ℂ), ‖φ x‖ ≤ r

Tactic:
obtain hr | hr := lt_or_ge r 0
  · obtain ⟨φ⟩ := (inferInstance : Nonempty (K →+* ℂ))
    refine iff_of_false ?_ ?_
    · exact (hr.trans_le (norm_nonneg _)).not_ge
    · exact fun h => hr.not_ge (le_trans (norm_nonneg _) (h φ))
  · lift r to NNReal using hr
    simp_rw [← coe_nnnorm, nnnorm_eq, NNReal.coe_le_coe, Finset.sup_le_iff, Finset.mem_univ,
      forall_true_left]

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
σ : Gal(K/k)
w : InfinitePlace K
⊢ (σ • w).IsComplex ↔ w.IsComplex

Tactic:
← not_isReal_iff_isComplex,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
⊢ ¬(σ • w).IsReal ↔ 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
σ : Gal(K/k)
w : InfinitePlace K
⊢ ¬(σ • w).IsReal ↔ w.IsComplex

Tactic:
← not_isReal_iff_isComplex,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
w : InfinitePlace K
⊢ ¬(σ • w).IsReal ↔ ¬w.IsReal
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
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ (mk φ).IsComplex ∧ ((mk φ).comap (algebraMap k K)).IsReal ↔ ¬ComplexEmbedding.IsReal φ

Tactic:
← not_isReal_iff_isComplex,

Goal state after:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : Gal(K/k)
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ ¬(mk φ).IsReal ∧ ((mk φ).comap (algebraMap k K)).IsReal ↔ ¬ComplexEmbedding.IsReal φ
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✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : (mk φ).IsComplex ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ False

Tactic:
← not_isReal_iff_isComplex,

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬(mk φ).IsReal ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ False
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✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
⊢ False

Tactic:
let := (φ.comp (algebraMap k K)).toAlgebra

Goal state after:
k : Type u_1
inst✝³ : Field k
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
φ : K →+* ℂ
H : ∀ (σ : Gal(K/k)), ComplexEmbedding.IsConj φ σ → σ = 1
hφ : ¬ComplexEmbedding.IsConj φ 1 ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K))
this : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedEmbedding.norm x = 0 ↔ ∃ w, (normAtPlace w) x = 0

Tactic:
simp_rw [mixedEmbedding.norm, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, prod_eq_zero_iff,
    mem_univ, true_and, pow_eq_zero_iff mult_ne_zero]

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

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ENNReal.ofReal ((∫ (x : mixedSpace K), rexp (-convexBodySumFun x ^ 1)) / Gamma (↑(finrank ℚ K) / 1 + 1)) =
    ↑(convexBodySumFactor K)

Tactic:
div_one,

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : ℝ
hB : 0 < B
⊢ ENNReal.ofReal ((∫ (x : mixedSpace K), rexp (-convexBodySumFun x ^ 1)) / Gamma (↑(finrank ℚ K) + 1)) =
    ↑(convexBodySumFactor K)