-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem pow_eq_one_of_norm_eq_one {x : K} (hxi : IsIntegral ℤ x) (hx : ∀ φ : K →+* A, ‖φ x‖ = 1) :
    ∃ (n : ℕ) (_ : 0 < n), x ^ n = 1

Proof state:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
⊢ x ^ (a - b) = 1

Tactic:
refine h.resolve_right fun hp => ?_

Result:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
⊢ False

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a : ℕ
x✝ : a ∈ univ
φ : K →+* A
⊢ ‖φ ((fun x_1 => x ^ x_1) a)‖ ≤ 1

Tactic:
simp [hx φ]

Result:
no goals

Proof state:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
hx : 0 = 1
⊢ False

Tactic:
norm_num at hx

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Tactic:
wlog hlt : b < a

Result:
case intro.intro.intro.intro.intro.inr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
this :
  ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (A : Type u_2) [inst_2 : NormedField A]
    [inst_3 : IsAlgClosed A] [inst_4 : NormedAlgebra ℚ A] {x : K},
    IsIntegral ℤ x →
      (∀ (φ : K →+* A), ‖φ x‖ = 1) → ∀ (a b : ℕ), a ≠ b → x ^ a = x ^ b → b < a → ∃ n, ∃ (_ : 0 < n), x ^ n = 1
hlt : ¬b < a
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Proof state:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
⊢ False

Tactic:
specialize hx (IsAlgClosed.lift (R := ℚ)).toRingHom

Result:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
hx : ‖IsAlgClosed.lift.toRingHom x‖ = 1
⊢ False

Proof state:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ x ^ (a - b) = 1

Tactic:
rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h

Result:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
⊢ x ^ (a - b) = 1

Proof state:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
hx : ‖IsAlgClosed.lift.toRingHom x‖ = 1
⊢ False

Tactic:
rw [pow_eq_zero hp, map_zero, norm_zero] at hx

Result:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
a b : ℕ
habne : a ≠ b
h : x ^ (a - b) = 1 ∨ x ^ b = 0
hlt : b < a
hp : x ^ b = 0
hx : 0 = 1
⊢ False

Proof state:
case intro.intro.intro.intro.intro.inr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
this :
  ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (A : Type u_2) [inst_2 : NormedField A]
    [inst_3 : IsAlgClosed A] [inst_4 : NormedAlgebra ℚ A] {x : K},
    IsIntegral ℤ x →
      (∀ (φ : K →+* A), ‖φ x‖ = 1) → ∀ (a b : ℕ), a ≠ b → x ^ a = x ^ b → b < a → ∃ n, ∃ (_ : 0 < n), x ^ n = 1
hlt : ¬b < a
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Tactic:
exact this K A hxi hx b a habne.symm h.symm (habne.lt_or_lt.resolve_right hlt)

Result:
no goals

Proof state:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ ∃ n, ∃ (_ : 0 < n), x ^ n = 1

Tactic:
refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩

Result:
K✝ : Type u_1
inst✝⁶ : Field K✝
A✝ : Type u_2
inst✝⁵ : NormedField A✝
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
a b : ℕ
habne : a ≠ b
h : x ^ a = x ^ b
hlt : b < a
⊢ x ^ (a - b) = 1

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
x : K
hxi : IsIntegral ℤ x
hx : ∀ (φ : K →+* A), ‖φ x‖ = 1
⊢ MapsTo (fun x_1 => x ^ x_1) univ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖φ x‖ ≤ 1}

Tactic:
exact fun a _ => ⟨hxi.pow a, fun φ => by simp [hx φ]⟩

Result:
no goals