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

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

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

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

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:
<;>

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

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

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

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
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
x : K
| ψ x

Tactic:
← hiφ x

Goal state after:
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑φ.fieldRange.subtype
x : K
| ψ (j (φ x))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
x : K
| ψ x

Tactic:
← hiφ x

Goal state after:
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ⇑φ
ι : K ≃+* ↥φ.range := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ⇑(ψ.comp ι.symm.toRingHom)
h : (↑↑(ψ.comp ι.symm.toRingHom)).toFun = ⇑(starRingEnd ℂ) ∘ ⇑φ.fieldRange.subtype
x : K
| ψ (j (φ x))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ → φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ

pp: case mpr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ → mk φ = mk ψ

Tactic:
· -- We prove that the map ψ ∘ φ⁻¹ between φ(K) and ℂ is uniform continuous, thus it is either the
    -- inclusion or the complex conjugation using `Complex.uniformContinuous_ringHom_eq_id_or_conj`
    intro h₀
    obtain ⟨j, hiφ⟩ := (φ.injective).hasLeftInverse
    let ι := RingEquiv.ofLeftInverse hiφ
    have hlip : LipschitzWith 1 (RingHom.comp ψ ι.symm.toRingHom) := by
      change LipschitzWith 1 (ψ ∘ ι.symm)
      apply LipschitzWith.of_dist_le_mul
      intro x y
      rw [NNReal.coe_one, one_mul, dist_eq_norm, Function.comp_apply, Function.comp_apply,
        ← map_sub, ← map_sub]
      apply le_of_eq
      suffices ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖ by
        rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _,
          dist_eq_norm]
        rfl
      exact congrFun (congrArg (↑) h₀) _
    cases
      Complex.uniformContinuous_ringHom_eq_id_or_conj φ.fieldRange hlip.uniformContinuous with
    | inl h =>
        left; ext1 x
        conv_rhs => rw [← hiφ x]
        exact (congrFun h (ι x)).symm
    | inr h =>
        right; ext1 x
        conv_rhs => rw [← hiφ x]
        exact (congrFun h (ι x)).symm

Goal state after:
case mpr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ → mk φ = mk ψ
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

pp: case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : ¬w.IsReal
⊢ 0 < 2

Tactic:
<;>

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.PythagoreanTriples

Goal state before:
pp: case 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 : ℤ
ht1 : x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2
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 : m < 0
⊢ ∃ 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

Tactic:
· use -m, -n
    rcases ht1 with h_odd | h_even
    · rw [neg_sq m]
      rw [neg_sq n]
      apply And.intro h_odd.1
      constructor
      · rw [h_odd.2]
        ring
      rcases ht2 with h_pos | h_neg
      · apply And.intro h_pos
        constructor
        · delta Int.gcd
          rw [Int.natAbs_neg, Int.natAbs_neg]
          exact ht3
        · rw [Int.neg_emod_two, Int.neg_emod_two]
          apply And.intro ht4
          lia
      · exfalso
        revert h_pos
        rw [h_neg]
        exact imp_false.mpr (not_lt.mpr (neg_nonpos.mpr (by positivity)))
    exfalso
    rcases h_even with ⟨rfl, -⟩
    rw [mul_assoc, Int.mul_emod_right] at h_parity
    exact zero_ne_one h_parity

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

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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.PythagoreanTriples

Goal state before:
pp: case mpr.inl.inl
k m n : ℤ
⊢ PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) (k * (m ^ 2 + n ^ 2))

pp: case mpr.inl.inr
k m n : ℤ
⊢ PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) (-k * (m ^ 2 + n ^ 2))

pp: case mpr.inr.inl
k m n : ℤ
⊢ PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) (k * (m ^ 2 + n ^ 2))

pp: case mpr.inr.inr
k m n : ℤ
⊢ PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) (-k * (m ^ 2 + n ^ 2))

Tactic:
<;>

Goal state after:
case mpr.inl.inl
k m n : ℤ
⊢ PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) (k * (m ^ 2 + n ^ 2))

case mpr.inl.inr
k m n : ℤ
⊢ PythagoreanTriple (k * (m ^ 2 - n ^ 2)) (k * (2 * m * n)) (-k * (m ^ 2 + n ^ 2))

case mpr.inr.inl
k m n : ℤ
⊢ PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) (k * (m ^ 2 + n ^ 2))

case mpr.inr.inr
k m n : ℤ
⊢ PythagoreanTriple (k * (2 * m * n)) (k * (m ^ 2 - n ^ 2)) (-k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mpr.inl.inl
k m n : ℤ
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) =
    k * (m ^ 2 + n ^ 2) * (k * (m ^ 2 + n ^ 2))

pp: case mpr.inl.inr
k m n : ℤ
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) =
    -k * (m ^ 2 + n ^ 2) * (-k * (m ^ 2 + n ^ 2))

pp: case mpr.inr.inl
k m n : ℤ
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) =
    k * (m ^ 2 + n ^ 2) * (k * (m ^ 2 + n ^ 2))

pp: case mpr.inr.inr
k m n : ℤ
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) =
    -k * (m ^ 2 + n ^ 2) * (-k * (m ^ 2 + n ^ 2))

Tactic:
<;>

Goal state after:
case mpr.inl.inl
k m n : ℤ
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) =
    k * (m ^ 2 + n ^ 2) * (k * (m ^ 2 + n ^ 2))

case mpr.inl.inr
k m n : ℤ
⊢ k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) + k * (2 * m * n) * (k * (2 * m * n)) =
    -k * (m ^ 2 + n ^ 2) * (-k * (m ^ 2 + n ^ 2))

case mpr.inr.inl
k m n : ℤ
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) =
    k * (m ^ 2 + n ^ 2) * (k * (m ^ 2 + n ^ 2))

case mpr.inr.inr
k m n : ℤ
⊢ k * (2 * m * n) * (k * (2 * m * n)) + k * (m ^ 2 - n ^ 2) * (k * (m ^ 2 - n ^ 2)) =
    -k * (m ^ 2 + n ^ 2) * (-k * (m ^ 2 + n ^ 2))
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : |(f ζ).re| = ‖f ζ‖
this : ‖f ζ‖ = 1
⊢ (f ζ).re = 1 ∨ (f ζ).re = -1

Tactic:
← him,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
k : ℕ
hk : 2 < k
hζ : IsPrimitiveRoot ζ k
x✝ : { w // w.IsReal }
w : InfinitePlace K
hwreal : ComplexEmbedding.IsReal w.embedding
f : K →+* ℂ := w.embedding
hζ' : IsPrimitiveRoot (f ζ) k
him : |(f ζ).re| = ‖f ζ‖
this : |(f ζ).re| = 1
⊢ (f ζ).re = 1 ∨ (f ζ).re = -1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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.NumberField.CanonicalEmbedding.ConvexBody

Goal state before:
pp: 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}

pp: 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✝¹)

Tactic:
<;>

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.InfinitePlace.Ramification

Goal state before:
pp: case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : (w.comap (algebraMap k K)).IsReal
h₂ : w.IsReal
⊢ ¬1 = 1 ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

pp: case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : (w.comap (algebraMap k K)).IsReal
h₂ : ¬w.IsReal
⊢ ¬1 = 2 ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

pp: case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : ¬(w.comap (algebraMap k K)).IsReal
h₂ : w.IsReal
⊢ ¬2 = 1 ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

pp: case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : ¬(w.comap (algebraMap k K)).IsReal
h₂ : ¬w.IsReal
⊢ ¬2 = 2 ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

Tactic:
<;>

Goal state after:
case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : (w.comap (algebraMap k K)).IsReal
h₂ : w.IsReal
⊢ ¬1 = 1 ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : (w.comap (algebraMap k K)).IsReal
h₂ : ¬w.IsReal
⊢ ¬1 = 2 ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

case pos
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : ¬(w.comap (algebraMap k K)).IsReal
h₂ : w.IsReal
⊢ ¬2 = 1 ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal

case neg
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
w : InfinitePlace K
h₁ : ¬(w.comap (algebraMap k K)).IsReal
h₂ : ¬w.IsReal
⊢ ¬2 = 2 ↔ ¬w.IsReal ∧ (w.comap (algebraMap k K)).IsReal
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inl
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
h✝ : (mk φ).embedding = φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

pp: case inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
h✝ : (mk φ).embedding = conjugate φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

Tactic:
<;>

Goal state after:
case inl
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
h✝ : (mk φ).embedding = φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding

case inr
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
φ : K →+* ℂ
h : IsMixed k φ
h✝ : (mk φ).embedding = conjugate φ
⊢ ¬ComplexEmbedding.IsReal (mk φ).embedding
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: 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✝⟩‖

pp: 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, ⋯⟩‖

Tactic:
<;>

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: case pos
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
h✝ : w.IsReal
⊢ 0 ≤ ‖x.1 ⟨w, h✝⟩‖

pp: case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : mixedSpace K
h✝ : ¬w.IsReal
⊢ 0 ≤ ‖x.2 ⟨w, ⋯⟩‖

Tactic:
<;>

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: 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✝⟩‖

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

Tactic:
<;>

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: 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✝⟩‖

pp: 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, ⋯⟩‖

Tactic:
<;>

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: 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✝⟩‖

pp: 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, ⋯⟩‖

Tactic:
<;>

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: case fst
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
x✝ : { w // w.IsReal }
⊢ (fun x ↦ c, fun x ↦ ↑c).1 x✝ = (c • 1).1 x✝

pp: case snd
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
x✝ : { w // w.IsComplex }
⊢ (fun x ↦ c, fun x ↦ ↑c).2 x✝ = (c • 1).2 x✝

Tactic:
<;>

Goal state after:
case fst
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
x✝ : { w // w.IsReal }
⊢ (fun x ↦ c, fun x ↦ ↑c).1 x✝ = (c • 1).1 x✝

case snd
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
c : ℝ
x✝ : { w // w.IsComplex }
⊢ (fun x ↦ c, fun x ↦ ↑c).2 x✝ = (c • 1).2 x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

pp: case neg
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
h✝ : ¬w.IsReal
⊢ Continuous fun x ↦ ‖x.2 ⟨w, ⋯⟩‖

Tactic:
<;>

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.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 φ σ
⊢ ¬ComplexEmbedding.IsReal φ ∧ ComplexEmbedding.IsReal (φ.comp (algebraMap k K)) ↔ ¬ComplexEmbedding.IsReal φ

Tactic:
eq_true h.isReal_comp,

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 φ σ
⊢ ¬ComplexEmbedding.IsReal φ ∧ True ↔ ¬ComplexEmbedding.IsReal φ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: case fst
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w.IsReal }
⊢ (fun x ↦ c, fun x ↦ ↑c).1 x✝ = (c • 1).1 x✝

pp: case snd
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w.IsComplex }
⊢ (fun x ↦ c, fun x ↦ ↑c).2 x✝ = (c • 1).2 x✝

Tactic:
<;>

Goal state after:
case fst
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w.IsReal }
⊢ (fun x ↦ c, fun x ↦ ↑c).1 x✝ = (c • 1).1 x✝

case snd
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w.IsComplex }
⊢ (fun x ↦ c, fun x ↦ ↑c).2 x✝ = (c • 1).2 x✝
Module: Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Goal state before:
pp: case inl
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
e : Nat.card ↥(Stab w) = 1
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2

pp: case inr
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
e : Nat.card ↥(Stab w) = 2
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2

Tactic:
<;>

Goal state after:
case inl
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
e : Nat.card ↥(Stab w) = 1
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2

case inr
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
e : Nat.card ↥(Stab w) = 2
⊢ ¬Nat.card ↥(Stab w) = 1 ↔ Nat.card ↥(Stab w) = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

Goal state before:
pp: 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

pp: 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

Tactic:
<;>

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