mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (cexp (-↑π * I * z ^ 2 * τ⁻¹) * (deriv (fun z ↦ -↑π * I * z ^ 2) z * τ⁻¹) * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-↑π * I * z ^ 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * ↑π * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))

Tactic:
deriv_const_mul_field,

Goal state after:
z τ : ℂ
hτ : 0 < τ.im
hτ' : 0 < (-1 / τ).im
hj : HasDerivAt (fun w ↦ jacobiTheta₂ (w / τ) (-1 / τ)) (1 / τ * jacobiTheta₂' (z / τ) (-1 / τ)) z
⊢ (cexp (-↑π * I * z ^ 2 * τ⁻¹) * (-↑π * I * deriv (fun z ↦ z ^ 2) z * τ⁻¹) * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹) +
        cexp (-↑π * I * z ^ 2 * τ⁻¹) * (1 * τ⁻¹ * jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹))) *
      (1 / (-I * τ) ^ (1 / 2)) =
    1 / (-I * τ) ^ (1 / 2) * cexp (-↑π * I * z ^ 2 * τ⁻¹) * τ⁻¹ *
      (jacobiTheta₂' (z * τ⁻¹) (-1 * τ⁻¹) - 2 * ↑π * I * z * jacobiTheta₂ (z * τ⁻¹) (-1 * τ⁻¹))
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
⊢ (-if a = 0 then 1 else 0) = if a = 0 then -1 else 0

Tactic:
split_ifs

Goal state after:
case pos
a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
h✝ : a = 0
⊢ -1 = -1

case neg
a : UnitAddCircle
h1 : Tendsto (fun s ↦ s * (hurwitzEvenFEPair a).Λ s) (𝓝[≠] 0) (𝓝 (-if a = 0 then 1 else 0))
h✝ : ¬a = 0
⊢ -0 = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
⊢ (if n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) =
    (if n = 0 then 0 else cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) / 2

Tactic:
split_ifs

Goal state after:
case pos
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
h✝ : n = 0
⊢ 0 = 0 / 2

case neg
a : ℝ
s : ℂ
hs : 1 < s.re
c : ℤ → ℂ := fun n ↦ cexp (2 * ↑π * I * ↑a * ↑n) / 2
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ¬n = 0
⊢ c n * ↑(rexp (-π * ↑n ^ 2 * t)) = cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) / 2
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaEven

Goal state before:
pp: a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
⊢ (if ↑n + a = 0 then 0 else 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t))) =
    ↑(if ↑n + a = 0 then 0 else rexp (-π * (↑n + a) ^ 2 * t)) / 2

Tactic:
split_ifs

Goal state after:
case pos
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ↑n + a = 0
⊢ 0 = ↑0 / 2

case neg
a : ℝ
s : ℂ
hs : 1 < s.re
t : ℝ
ht : 0 < t
n : ℤ
h✝ : ¬↑n + a = 0
⊢ 1 / 2 * ↑(rexp (-π * (↑n + a) ^ 2 * t)) = ↑(rexp (-π * (↑n + a) ^ 2 * t)) / 2
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ deriv (L 1) s = deriv riemannZeta s

Tactic:
refine Filter.EventuallyEq.deriv_eq <| Filter.eventuallyEq_iff_exists_mem.mpr ?_

Goal state after:
s : ℂ
hs : 1 < s.re
⊢ ∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1
Module: Mathlib.NumberTheory.LSeries.Dirichlet

Goal state before:
pp: s : ℂ
hs : 1 < s.re
⊢ ∃ s_1 ∈ nhds s, Set.EqOn (L 1) riemannZeta s_1

Tactic:
exact ⟨{z | 1 < z.re}, (isOpen_lt continuous_const continuous_re).mem_nhds hs,
    fun _ ↦ LSeries_one_eq_riemannZeta⟩

Goal state after:
Module: Mathlib.NumberTheory.EulerProduct.DirichletLSeries

Goal state before:
pp: s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ ∑' (n : ℕ), (dirichletSummandHom χ ⋯) n = L (fun n ↦ χ ↑n) s

Tactic:
by
  simp only [dirichletSummandHom, cpow_neg, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, LSeries,
    LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), div_eq_mul_inv]

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

Goal state before:
pp: case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
⊢ Fermat42 a1 b1 c1 → s0.2.2.natAbs ≤ c1.natAbs

Tactic:
h1

Goal state after:
case right
a b c : ℤ
h : Fermat42 a b c
S : Set ℕ := {n | ∃ s, Fermat42 s.1 s.2.1 s.2.2 ∧ n = s.2.2.natAbs}
S_nonempty : S.Nonempty
m : ℕ := Nat.find S_nonempty
s0 : ℤ × ℤ × ℤ
hs0 : Fermat42 s0.1 s0.2.1 s0.2.2
hs1 : m = s0.2.2.natAbs
a1 b1 c1 : ℤ
h1 : Fermat42 a1 b1 c1
⊢ s0.2.2.natAbs ≤ c1.natAbs
Module: Mathlib.NumberTheory.FLT.Four

Goal state before:
pp: a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hs : b' ^ 2 = r * s * m
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
⊢ False

Tactic:
h1

Goal state after:
a b c : ℤ
h : Minimal a b c
ha2 : a % 2 = 1
hc : 0 < c
ht : PythagoreanTriple (a ^ 2) (b ^ 2) c
h2 : (a ^ 2).gcd (b ^ 2) = 1
ha22 : a ^ 2 % 2 = 1
m n : ℤ
ht1 : a ^ 2 = m ^ 2 - n ^ 2
ht2 : b ^ 2 = 2 * m * n
ht3 : c = m ^ 2 + n ^ 2
ht4 : m.gcd n = 1
ht5 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
ht6 : 0 ≤ m
htt : PythagoreanTriple a n m
h3 : a.gcd n = 1
hb20 : b ^ 2 ≠ 0
h4 : 0 < m
r s : ℤ
left✝ : a = r ^ 2 - s ^ 2
htt2 : n = 2 * r * s
htt3 : m = r ^ 2 + s ^ 2
htt4 : r.gcd s = 1
htt5 : r % 2 = 0 ∧ s % 2 = 1 ∨ r % 2 = 1 ∧ s % 2 = 0
htt6 : 0 ≤ r
hcp : (r * s).gcd m = 1
b' : ℤ
hb2' : b = 2 * b'
hrsz : r * s ≠ 0
h2b0 : b' ≠ 0
i : ℤ
hi' : ¬m = -i ^ 2
hi : m = i ^ 2
d : ℤ
hs : b' ^ 2 = -d ^ 2 * m
hd : r * s = d ^ 2 ∨ r * s = -d ^ 2
h1 : r * s = -d ^ 2
⊢ False
Module: Mathlib.RingTheory.Radical.Basic

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ (normalizedFactors a).toFinset = ∅ ↔ IsUnit a

Tactic:
Multiset.toFinset_eq_empty,

Goal state after:
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ normalizedFactors a = 0 ↔ IsUnit a
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 : b + c + a = 0
w : k[X] := a.wronskian b
wab : w = a.wronskian b
hbc : IsCoprime b c
hsum' : b + c + a = 0
hca : IsCoprime c a
wbc : w = b.wronskian c
⊢ w = c.wronskian a

Tactic:
simpa only [← wbc] using wronskian_eq_of_sum_zero hsum

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

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
⊢ (∃ n, a ∣ b ^ n) ↔ radical a ∣ b

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Goal state after:
case inl
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a : M
ha : a ≠ 0
⊢ (∃ n, a ∣ 0 ^ n) ↔ radical a ∣ 0

case inr
M : Type u_1
inst✝² : CommMonoidWithZero M
inst✝¹ : NormalizationMonoid M
inst✝ : UniqueFactorizationMonoid M
a b : M
ha : a ≠ 0
hb : b ≠ 0
⊢ (∃ n, a ∣ b ^ n) ↔ radical a ∣ b
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
⊢ IsUnit ((norm K) x) ↔ IsUnit x

Tactic:
let : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K

Goal state after:
K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
⊢ IsUnit ((norm K) x) ↔ IsUnit x
Module: Mathlib.NumberTheory.NumberField.Norm

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
F : Type u_3
inst✝³ : Field F
inst✝² : Algebra K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : 𝓞 F
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField K (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F ↥L
this : IsGalois F ↥L
⊢ IsUnit ((norm K) x ^ finrank F ↥L) ↔ IsUnit ((norm K) ((algebraMap (𝓞 F) (𝓞 ↥L)) x))

Tactic:
rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inl
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) + (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) = (m ^ 2 + n ^ 2) * (m ^ 2 + n ^ 2) ∧
    (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1

Tactic:
constructor; ring; rw [Int.gcd_comm]; exact coprime_sq_sub_mul co pp

Goal state after:
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inr.inr
m n : ℤ
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ 2 * m * n * (2 * m * n) + (m ^ 2 - n ^ 2) * (m ^ 2 - n ^ 2) = -(m ^ 2 + n ^ 2) * -(m ^ 2 + n ^ 2) ∧
    (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1

Tactic:
constructor; ring; rw [Int.gcd_comm]; exact coprime_sq_sub_mul co pp

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ 0 < if w.IsReal then 1 else 2

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : w.IsReal
⊢ 0 < 1

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : ¬w.IsReal
⊢ 0 < 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
⊢ (if z.IsReal then 1 else 2) ≠ 0

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
h✝ : z.IsReal
⊢ 1 ≠ 0

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
a : 𝓞 K
ha : a ≠ 0
h : ∀ ⦃z : InfinitePlace K⦄, z ≠ w → z ↑a < 1
this : w ↑a < 1
z : InfinitePlace K
x✝ : z ∈ Finset.univ
h✝ : ¬z.IsReal
⊢ 2 ≠ 0
Module: Mathlib.NumberTheory.NumberField.Units.Basic

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

Tactic:
one_pow

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

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

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:
· exact orderOf_dvd_of_pow_eq_one h

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∀ (w : { w // w.IsComplex }), #{φ | mkComplex φ = w} = 2

Tactic:
rintro ⟨w, hw⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : w.IsComplex
⊢ #{φ | mkComplex φ = ⟨w, hw⟩} = 2
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (-1) ^ ((#Finset.univ + 2 * nrComplexPlaces K - #Finset.univ) / 2) = (-1) ^ nrComplexPlaces K

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯ ^ 2 = 1

Tactic:
Nat.add_sub_cancel_left,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (-1) ^ (2 * nrComplexPlaces K / 2) = (-1) ^ nrComplexPlaces K

K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Function.Involutive.toPerm ComplexEmbedding.conjugate ⋯ ^ 2 = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
⊢ ↑(if w₁.IsReal then 1 else 2) ≠ 0

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
h✝ : w₁.IsReal
⊢ ↑1 ≠ 0

case neg
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℝ≥0
hf : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
S : ℝ≥0 := ∏ w ∈ Finset.univ.erase w₁, f w ^ w.mult
h✝ : ¬w₁.IsReal
⊢ ↑2 ≠ 0
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case e'_4
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
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
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
⊢ b' = b / gcd a b

pp: case convert_6
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
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
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
⊢ b ≠ 0

Tactic:
· exact EuclideanDomain.eq_div_of_mul_eq_left ha.left eq_b.symm

Goal state after:
case convert_6
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
hb : d ≠ 0 ∧ b' ≠ 0
ha : d ≠ 0 ∧ a' ≠ 0
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
⊢ b ≠ 0
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
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✝¹)

Tactic:
split_ifs

Goal state after:
case pos
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
h✝ : ⟨a✝¹, a✝⟩ = w₀
⊢ -x.2 ⟨a✝¹, a✝⟩ ∈ {x | |x.re| < 1 ∧ |x.im| < ↑(f a✝¹) ^ 2} ↔ x.2 ⟨a✝¹, a✝⟩ ∈ {x | |x.re| < 1 ∧ |x.im| < ↑(f a✝¹) ^ 2}

case neg
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
h✝ : ¬⟨a✝¹, a✝⟩ = w₀
⊢ -x.2 ⟨a✝¹, a✝⟩ ∈ ball 0 ↑(f a✝¹) ↔ x.2 ⟨a✝¹, a✝⟩ ∈ ball 0 ↑(f a✝¹)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
⊢ Convex ℝ (if x✝¹ = w₀ then {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2} else ball 0 ↑(f ↑x✝¹))

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : x✝¹ = w₀
⊢ Convex ℝ {x | |x.re| < 1 ∧ |x.im| < ↑(f ↑x✝¹) ^ 2}

case neg
K : Type u_1
inst✝ : Field K
f : InfinitePlace K → ℝ≥0
w₀ x✝¹ : { w // w.IsComplex }
x✝ : x✝¹ ∈ Set.univ
h✝ : ¬x✝¹ = w₀
⊢ Convex ℝ (ball 0 ↑(f ↑x✝¹))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ N.transpose.det ≠ 0

Tactic:
Matrix.det_transpose,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis (K →+* ℂ) ℂ ((K →+* ℂ) → ℂ) := Pi.basisFun ℂ (K →+* ℂ)
e : (K →+* ℂ) ≃ Free.ChooseBasisIndex ℤ (𝓞 K) := Fintype.equivOfCardEq ⋯
M : Matrix (K →+* ℂ) (K →+* ℂ) ℂ := B.toMatrix fun i ↦ (canonicalEmbedding K) ((integralBasis K) (e i))
N : Matrix (K →+* ℂ) (K →+* ℂ) ℂ :=
  Algebra.embeddingsMatrixReindex ℚ ℂ (fun i ↦ (integralBasis K) (e i)) (RingHom.equivRatAlgHom K ℂ)
⊢ N.det ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: case e_a.e_a
K : Type u_1
inst✝¹ : Field K
f : InfinitePlace K → ℝ≥0
w₀ : { w // w.IsComplex }
inst✝ : NumberField K
vol_box : ∀ (B : ℝ≥0), volume {x | |x.re| < 1 ∧ |x.im| < ↑B ^ 2} = 4 * ↑B ^ 2
⊢ ∏ x ∈ Finset.univ.erase w₀,
      volume (if x = w₀ then {x_1 | |x_1.re| < 1 ∧ |x_1.im| < ↑(f ↑x) ^ 2} else ball 0 ↑(f ↑x)) =
    ∏ x ∈ Finset.univ.erase w₀, ENNReal.ofReal ↑(f ↑x) ^ 2 * ↑pi

Tactic:
refine Finset.prod_congr rfl (fun w' hw' ↦ ?_)
        rw [if_neg (Finset.ne_of_mem_erase hw'), Complex.volume_ball]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
x : K
⊢ (commMap K) ((canonicalEmbedding K) x) = (mixedEmbedding K) x

Tactic:
simp only [canonicalEmbedding, commMap, LinearMap.coe_mk, AddHom.coe_mk, RingHom.pi_apply,
    mixedEmbedding, RingHom.prod_apply, Prod.mk.injEq]
  exact ⟨rfl, rfl⟩

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x * y).1 ⟨w, hw⟩‖ else ‖(x * y).2 ⟨w, ⋯⟩‖) =
    (if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖) * if hw : w.IsReal then ‖y.1 ⟨w, hw⟩‖ else ‖y.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
h✝ : w.IsReal
⊢ ‖(x * y).1 ⟨w, h✝⟩‖ = ‖x.1 ⟨w, h✝⟩‖ * ‖y.1 ⟨w, h✝⟩‖

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
h✝ : ¬w.IsReal
⊢ ‖(x * y).2 ⟨w, ⋯⟩‖ = ‖x.2 ⟨w, ⋯⟩‖ * ‖y.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ 0 ≤ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
h✝ : w.IsReal
⊢ 0 ≤ ‖x.1 ⟨w, h✝⟩‖

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
h✝ : ¬w.IsReal
⊢ 0 ≤ ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
⊢ (if hw : w.IsReal then ‖(-x).1 ⟨w, hw⟩‖ else ‖(-x).2 ⟨w, ⋯⟩‖) = if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
h✝ : w.IsReal
⊢ ‖(-x).1 ⟨w, h✝⟩‖ = ‖x.1 ⟨w, h✝⟩‖

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
h✝ : ¬w.IsReal
⊢ ‖(-x).2 ⟨w, ⋯⟩‖ = ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
⊢ (if hw : w.IsReal then ‖(x + y).1 ⟨w, hw⟩‖ else ‖(x + y).2 ⟨w, ⋯⟩‖) ≤
    (if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖) + if hw : w.IsReal then ‖y.1 ⟨w, hw⟩‖ else ‖y.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
h✝ : w.IsReal
⊢ ‖(x + y).1 ⟨w, h✝⟩‖ ≤ ‖x.1 ⟨w, h✝⟩‖ + ‖y.1 ⟨w, h✝⟩‖

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x y : mixedSpace K
h✝ : ¬w.IsReal
⊢ ‖(x + y).2 ⟨w, ⋯⟩‖ ≤ ‖x.2 ⟨w, ⋯⟩‖ + ‖y.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
⊢ (if hw : w.IsReal then ‖(c • x).1 ⟨w, hw⟩‖ else ‖(c • x).2 ⟨w, ⋯⟩‖) =
    |c| * if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
h✝ : w.IsReal
⊢ ‖(c • x).1 ⟨w, h✝⟩‖ = |c| * ‖x.1 ⟨w, h✝⟩‖

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
c : ℝ
h✝ : ¬w.IsReal
⊢ ‖(c • x).2 ⟨w, ⋯⟩‖ = |c| * ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ Continuous fun x ↦ if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : w.IsReal
⊢ Continuous fun x ↦ ‖x.1 ⟨w, h✝⟩‖

case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : ¬w.IsReal
⊢ Continuous fun x ↦ ‖x.2 ⟨w, ⋯⟩‖
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ univ
⊢ Continuous fun a ↦ if h : x✝¹.IsReal then ‖a.1 ⟨x✝¹, h⟩‖ ^ x✝¹.mult else ‖a.2 ⟨x✝¹, ⋯⟩‖ ^ x✝¹.mult

Tactic:
split_ifs

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ univ
h✝ : x✝¹.IsReal
⊢ Continuous fun a ↦ ‖a.1 ⟨x✝¹, h✝⟩‖ ^ x✝¹.mult

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝¹ : InfinitePlace K
x✝ : x✝¹ ∈ univ
h✝ : ¬x✝¹.IsReal
⊢ Continuous fun a ↦ ‖a.2 ⟨x✝¹, ⋯⟩‖ ^ x✝¹.mult
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case hc
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)
⊢ IsUnramified k w

Tactic:
← isUnramifiedIn_comap

Goal state after:
case hc
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)
⊢ IsUnramifiedIn K (w.comap (algebraMap k K))