[GOAL]
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ γ ∈ Gamma N ↔ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
[PROOFSTEP]
rw [Gamma_mem']
[GOAL]
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 ↔
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
[PROOFSTEP]
constructor
[GOAL]
case mp
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1 →
    ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
[PROOFSTEP]
intro h
[GOAL]
case mp
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
[PROOFSTEP]
simp [← SL_reduction_mod_hom_val N γ, h]
[GOAL]
case mpr
N✝ N : ℕ
γ : SL(2, ℤ)
⊢ ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1 →
    ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
[PROOFSTEP]
intro h
[GOAL]
case mpr
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ = 1
[PROOFSTEP]
ext i j
[GOAL]
case mpr.a
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
i j : Fin 2
⊢ ↑(↑(SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) i j = ↑1 i j
[PROOFSTEP]
rw [SL_reduction_mod_hom_val N γ]
[GOAL]
case mpr.a
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
i j : Fin 2
⊢ ↑(↑γ i j) = ↑1 i j
[PROOFSTEP]
fin_cases i
[GOAL]
case mpr.a.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
j : Fin 2
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } j) = ↑1 { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case mpr.a.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
j : Fin 2
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } j) = ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case mpr.a.head.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }) =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp only [h]
[GOAL]
case mpr.a.head.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp only [h]
[GOAL]
case mpr.a.tail.head.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }) =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp only [h]
[GOAL]
case mpr.a.tail.head.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp only [h]
[GOAL]
case mpr.a.head.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }) =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
case mpr.a.head.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
case mpr.a.tail.head.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }) =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
case mpr.a.tail.head.tail.head
N✝ N : ℕ
γ : SL(2, ℤ)
h : ↑(↑γ 0 0) = 1 ∧ ↑(↑γ 0 1) = 0 ∧ ↑(↑γ 1 0) = 0 ∧ ↑(↑γ 1 1) = 1
⊢ ↑(↑γ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }) =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]
[GOAL]
N : ℕ
⊢ Gamma 1 = ⊤
[PROOFSTEP]
ext
[GOAL]
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Gamma 1 ↔ x✝ ∈ ⊤
[PROOFSTEP]
simp
[GOAL]
N : ℕ
⊢ Gamma 0 = ⊥
[PROOFSTEP]
ext
[GOAL]
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ ∈ Gamma 0 ↔ x✝ ∈ ⊥
[PROOFSTEP]
simp only [Gamma_mem, coe_matrix_coe, Int.coe_castRingHom, map_apply, Int.cast_id, Subgroup.mem_bot]
[GOAL]
case h
N : ℕ
x✝ : SL(2, ℤ)
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 ↔ x✝ = 1
[PROOFSTEP]
constructor
[GOAL]
case h.mp
N : ℕ
x✝ : SL(2, ℤ)
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1 → x✝ = 1
[PROOFSTEP]
intro h
[GOAL]
case h.mp
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ x✝ = 1
[PROOFSTEP]
ext i j
[GOAL]
case h.mp.a
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
i j : Fin 2
⊢ ↑x✝ i j = ↑1 i j
[PROOFSTEP]
fin_cases i
[GOAL]
case h.mp.a.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
j : Fin 2
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } j = ↑1 { val := 0, isLt := (_ : 0 < 2) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.mp.a.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
j : Fin 2
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } j = ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } j
[PROOFSTEP]
fin_cases j
[GOAL]
case h.mp.a.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp only [h]
[GOAL]
case h.mp.a.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp only [h]
[GOAL]
case h.mp.a.tail.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
simp only [h]
[GOAL]
case h.mp.a.tail.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
simp only [h]
[GOAL]
case h.mp.a.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 0, isLt := (_ : 0 < 2) }
case h.mp.a.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑1 { val := 0, isLt := (_ : 0 < 2) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
case h.mp.a.tail.head.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) } =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 0, isLt := (_ : 0 < 2) }
case h.mp.a.tail.head.tail.head
N : ℕ
x✝ : SL(2, ℤ)
h : ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
⊢ ↑x✝ { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) } =
    ↑1 { val := 1, isLt := (_ : (fun a => a < 2) 1) } { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
exacts [h.1, h.2.1, h.2.2.1, h.2.2.2]
[GOAL]
case h.mpr
N : ℕ
x✝ : SL(2, ℤ)
⊢ x✝ = 1 → ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
[PROOFSTEP]
intro h
[GOAL]
case h.mpr
N : ℕ
x✝ : SL(2, ℤ)
h : x✝ = 1
⊢ ↑(↑x✝ 0 0) = 1 ∧ ↑(↑x✝ 0 1) = 0 ∧ ↑(↑x✝ 1 0) = 0 ∧ ↑(↑x✝ 1 1) = 1
[PROOFSTEP]
simp [h]
[GOAL]
N✝ N : ℕ
⊢ ∀ {a b : SL(2, ℤ)}, a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}
[PROOFSTEP]
intro a b ha hb
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
⊢ a * b ∈ {g | ↑(↑g 1 0) = 0}
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
⊢ ↑(↑(a * b) 1 0) = 0
[PROOFSTEP]
have h := (Matrix.two_mul_expl a.1 b.1).2.2.1
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : a ∈ {g | ↑(↑g 1 0) = 0}
hb : b ∈ {g | ↑(↑g 1 0) = 0}
h : (↑a * ↑b) 1 0 = ↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0
⊢ ↑(↑(a * b) 1 0) = 0
[PROOFSTEP]
simp only [coe_matrix_coe, coe_mul, Int.coe_castRingHom, map_apply, Set.mem_setOf_eq] at *
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : ↑(↑a 1 0) = 0
hb : ↑(↑b 1 0) = 0
h : (↑a * ↑b) 1 0 = ↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0
⊢ ↑((↑a * ↑b) 1 0) = 0
[PROOFSTEP]
rw [h]
[GOAL]
N✝ N : ℕ
a b : SL(2, ℤ)
ha : ↑(↑a 1 0) = 0
hb : ↑(↑b 1 0) = 0
h : (↑a * ↑b) 1 0 = ↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0
⊢ ↑(↑a 1 0 * ↑b 0 0 + ↑a 1 1 * ↑b 1 0) = 0
[PROOFSTEP]
simp [ha, hb]
[GOAL]
N✝ N : ℕ
⊢ 1 ∈
    { carrier := {g | ↑(↑g 1 0) = 0},
        mul_mem' :=
          (_ :
            ∀ {a b : SL(2, ℤ)},
              a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) }.carrier
[PROOFSTEP]
simp
[GOAL]
N✝ N : ℕ
⊢ ∀ {x : SL(2, ℤ)},
    x ∈
        {
              toSubsemigroup :=
                { carrier := {g | ↑(↑g 1 0) = 0},
                  mul_mem' :=
                    (_ :
                      ∀ {a b : SL(2, ℤ)},
                        a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
              one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier →
      x⁻¹ ∈
        {
              toSubsemigroup :=
                { carrier := {g | ↑(↑g 1 0) = 0},
                  mul_mem' :=
                    (_ :
                      ∀ {a b : SL(2, ℤ)},
                        a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
              one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
[PROOFSTEP]
intro a ha
[GOAL]
N✝ N : ℕ
a : SL(2, ℤ)
ha :
  a ∈
    {
          toSubsemigroup :=
            { carrier := {g | ↑(↑g 1 0) = 0},
              mul_mem' :=
                (_ :
                  ∀ {a b : SL(2, ℤ)},
                    a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
          one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
⊢ a⁻¹ ∈
    {
          toSubsemigroup :=
            { carrier := {g | ↑(↑g 1 0) = 0},
              mul_mem' :=
                (_ :
                  ∀ {a b : SL(2, ℤ)},
                    a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
          one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
N✝ N : ℕ
a : SL(2, ℤ)
ha :
  a ∈
    {
          toSubsemigroup :=
            { carrier := {g | ↑(↑g 1 0) = 0},
              mul_mem' :=
                (_ :
                  ∀ {a b : SL(2, ℤ)},
                    a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
          one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
⊢ ↑(↑a⁻¹ 1 0) = 0
[PROOFSTEP]
rw [SL2_inv_expl a]
[GOAL]
N✝ N : ℕ
a : SL(2, ℤ)
ha :
  a ∈
    {
          toSubsemigroup :=
            { carrier := {g | ↑(↑g 1 0) = 0},
              mul_mem' :=
                (_ :
                  ∀ {a b : SL(2, ℤ)},
                    a ∈ {g | ↑(↑g 1 0) = 0} → b ∈ {g | ↑(↑g 1 0) = 0} → a * b ∈ {g | ↑(↑g 1 0) = 0}) },
          one_mem' := (_ : ↑(OfNat.ofNat 1 1 0) = 0) }.toSubsemigroup.carrier
⊢ ↑(↑{ val := ![![↑a 1 1, -↑a 0 1], ![-↑a 1 0, ↑a 0 0]],
            property := (_ : det ![![↑a 1 1, -↑a 0 1], ![-↑a 1 0, ↑a 0 0]] = 1) }
        1 0) =
    0
[PROOFSTEP]
simp only [cons_val_zero, cons_val_one, head_cons, coe_matrix_coe, coe_mk, Int.coe_castRingHom, map_apply, Int.cast_neg,
  neg_eq_zero, Set.mem_setOf_eq] at *
[GOAL]
N✝ N : ℕ
a : SL(2, ℤ)
ha : ↑(↑a 1 0) = 0
⊢ ↑(↑a 1 0) = 0
[PROOFSTEP]
exact ha
[GOAL]
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ ↑(det ↑↑A) = 1
[PROOFSTEP]
simp [A.1.property]
[GOAL]
N✝ N : ℕ
⊢ (fun g => ↑(↑↑g 1 1)) 1 = 1
[PROOFSTEP]
simp
[GOAL]
N✝ N : ℕ
⊢ ∀ (x y : { x // x ∈ Gamma0 N }),
    OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } (x * y) =
      OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } x *
        OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } y
[PROOFSTEP]
intro A B
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
⊢ OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } (A * B) =
    OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } A *
      OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } B
[PROOFSTEP]
have := (two_mul_expl A.1.1 B.1.1).2.2.2
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
⊢ OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } (A * B) =
    OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } A *
      OneHom.toFun { toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } B
[PROOFSTEP]
simp only [Subgroup.coe_mul, coe_matrix_coe, coe_mul, Int.coe_castRingHom, map_apply] at *
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
⊢ ↑((↑↑A * ↑↑B) 1 1) = ↑(↑↑A 1 1) * ↑(↑↑B 1 1)
[PROOFSTEP]
rw [this]
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
⊢ ↑(↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1) = ↑(↑↑A 1 1) * ↑(↑↑B 1 1)
[PROOFSTEP]
have ha := A.property
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
ha : ↑A ∈ Gamma0 N
⊢ ↑(↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1) = ↑(↑↑A 1 1) * ↑(↑↑B 1 1)
[PROOFSTEP]
simp only [Int.cast_add, Int.cast_mul, add_left_eq_self, Gamma0_mem, coe_matrix_coe, Int.coe_castRingHom,
  map_apply] at *
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
ha : ↑(↑↑A 1 0) = 0
⊢ ↑(↑↑A 1 0) * ↑(↑↑B 0 1) = 0
[PROOFSTEP]
rw [ha]
[GOAL]
N✝ N : ℕ
A B : { x // x ∈ Gamma0 N }
this : (↑↑A * ↑↑B) 1 1 = ↑↑A 1 0 * ↑↑B 0 1 + ↑↑A 1 1 * ↑↑B 1 1
ha : ↑(↑↑A 1 0) = 0
⊢ 0 * ↑(↑↑B 0 1) = 0
[PROOFSTEP]
simp
[GOAL]
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ A ∈ Gamma1' N ↔ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
intro ha
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
have hA := A.property
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑A ∈ Gamma0 N
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
rw [Gamma0_mem] at hA
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
have adet := Gamma0_det N A
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
adet : ↑(det ↑↑A) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
rw [Matrix.det_fin_two] at adet
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : A ∈ Gamma1' N
hA : ↑(↑↑A 1 0) = 0
adet : ↑(↑↑A 0 0 * ↑↑A 1 1 - ↑↑A 0 1 * ↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
simp only [Gamma0Map, coe_matrix_coe, Int.coe_castRingHom, map_apply, Gamma1_mem', MonoidHom.coe_mk, OneHom.coe_mk,
  Int.cast_sub, Int.cast_mul] at *
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * ↑(↑↑A 1 1) - ↑(↑↑A 0 1) * ↑(↑↑A 1 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
rw [hA, ha] at adet
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) * 1 - ↑(↑↑A 0 1) * 0 = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
simp only [mul_one, mul_zero, sub_zero] at adet
[GOAL]
case mp
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
hA : ↑(↑↑A 1 0) = 0
ha : ↑(↑↑A 1 1) = 1
adet : ↑(↑↑A 0 0) = 1
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
[PROOFSTEP]
simp only [adet, hA, ha, eq_self_iff_true, and_self_iff]
[GOAL]
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N
[PROOFSTEP]
intro ha
[GOAL]
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ A ∈ Gamma1' N
[PROOFSTEP]
simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, coe_matrix_coe, Int.coe_castRingHom, map_apply]
[GOAL]
case mpr
N✝ N : ℕ
A : { x // x ∈ Gamma0 N }
ha : ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0
⊢ ↑{ toFun := fun g => ↑(↑↑g 1 1), map_one' := (_ : ↑(OfNat.ofNat 1 1 1) = 1) } A = 1
[PROOFSTEP]
exact ha.2.1
[GOAL]
N✝ N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N ↔ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
N✝ N : ℕ
A : SL(2, ℤ)
⊢ A ∈ Gamma1 N → ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
intro ha
[GOAL]
case mp
N✝ N : ℕ
A : SL(2, ℤ)
ha : A ∈ Gamma1 N
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
simp_rw [Gamma1, Subgroup.mem_map] at ha
[GOAL]
case mp
N✝ N : ℕ
A : SL(2, ℤ)
ha : ∃ x, x ∈ ⊤ ∧ ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) x = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
obtain ⟨⟨x, hx⟩, hxx⟩ := ha
[GOAL]
case mp.intro.mk
N✝ N : ℕ
A : SL(2, ℤ)
x : { x // x ∈ Gamma0 N }
hx : x ∈ Gamma1' N
hxx :
  { val := x, property := hx } ∈ ⊤ ∧
    ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx } = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
rw [Gamma1_to_Gamma0_mem] at hx
[GOAL]
case mp.intro.mk
N✝ N : ℕ
A : SL(2, ℤ)
x : { x // x ∈ Gamma0 N }
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx :
  { val := x, property := hx✝ } ∈ ⊤ ∧
    ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ } = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
simp only [Subgroup.mem_top, true_and] at hxx
[GOAL]
case mp.intro.mk
N✝ N : ℕ
A : SL(2, ℤ)
x : { x // x ∈ Gamma0 N }
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ } = A
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
rw [← hxx]
[GOAL]
case mp.intro.mk
N✝ N : ℕ
A : SL(2, ℤ)
x : { x // x ∈ Gamma0 N }
hx✝ : x ∈ Gamma1' N
hx : ↑(↑↑x 0 0) = 1 ∧ ↑(↑↑x 1 1) = 1 ∧ ↑(↑↑x 1 0) = 0
hxx : ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ } = A
⊢ ↑(↑(↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ }) 0
          0) =
      1 ∧
    ↑(↑(↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ }) 1
            1) =
        1 ∧
      ↑(↑(↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) { val := x, property := hx✝ })
            1 0) =
        0
[PROOFSTEP]
convert hx
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0 → A ∈ Gamma1 N
[PROOFSTEP]
intro ha
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma1 N
[PROOFSTEP]
simp_rw [Gamma1, Subgroup.mem_map]
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ ∃ x, x ∈ ⊤ ∧ ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) x = A
[PROOFSTEP]
have hA : A ∈ Gamma0 N := by simp [ha.right.right, Gamma0_mem]
[GOAL]
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
⊢ A ∈ Gamma0 N
[PROOFSTEP]
simp [ha.right.right, Gamma0_mem]
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ∃ x, x ∈ ⊤ ∧ ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) x = A
[PROOFSTEP]
have HA : (⟨A, hA⟩ : Gamma0 N) ∈ Gamma1' N :=
  by
  simp only [Gamma1_to_Gamma0_mem, Subgroup.coe_mk, coe_matrix_coe, Int.coe_castRingHom, map_apply]
  exact ha
[GOAL]
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ { val := A, property := hA } ∈ Gamma1' N
[PROOFSTEP]
simp only [Gamma1_to_Gamma0_mem, Subgroup.coe_mk, coe_matrix_coe, Int.coe_castRingHom, map_apply]
[GOAL]
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
exact ha
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : { val := A, property := hA } ∈ Gamma1' N
⊢ ∃ x, x ∈ ⊤ ∧ ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N))) x = A
[PROOFSTEP]
refine' ⟨(⟨(⟨A, hA⟩ : Gamma0 N), HA⟩ : (Gamma1' N : Subgroup (Gamma0 N))), _⟩
[GOAL]
case mpr
N✝ N : ℕ
A : SL(2, ℤ)
ha : ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
hA : A ∈ Gamma0 N
HA : { val := A, property := hA } ∈ Gamma1' N
⊢ { val := { val := A, property := hA }, property := HA } ∈ ⊤ ∧
    ↑(MonoidHom.comp (Subgroup.subtype (Gamma0 N)) (Subgroup.subtype (Gamma1' N)))
        { val := { val := A, property := hA }, property := HA } =
      A
[PROOFSTEP]
simp
[GOAL]
N✝ N : ℕ
⊢ Gamma1 N ≤ Gamma0 N
[PROOFSTEP]
intro x HA
[GOAL]
N✝ N : ℕ
x : SL(2, ℤ)
HA : x ∈ Gamma1 N
⊢ x ∈ Gamma0 N
[PROOFSTEP]
simp only [Gamma0_mem, Gamma1_mem, coe_matrix_coe, Int.coe_castRingHom, map_apply] at *
[GOAL]
N✝ N : ℕ
x : SL(2, ℤ)
HA : ↑(↑x 0 0) = 1 ∧ ↑(↑x 1 1) = 1 ∧ ↑(↑x 1 0) = 0
⊢ ↑(↑x 1 0) = 0
[PROOFSTEP]
exact HA.2.2
[GOAL]
N : ℕ
H K : Subgroup SL(2, ℤ)
h : H ≤ K
h2 : IsCongruenceSubgroup H
⊢ IsCongruenceSubgroup K
[PROOFSTEP]
obtain ⟨N, hN⟩ := h2
[GOAL]
case intro
N✝ : ℕ
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ+
hN : Gamma ↑N ≤ H
⊢ IsCongruenceSubgroup K
[PROOFSTEP]
refine' ⟨N, le_trans hN h⟩
[GOAL]
N✝ : ℕ
N : ℕ+
⊢ Gamma ↑N ≤ Gamma ↑N
[PROOFSTEP]
simp only [le_refl]
[GOAL]
N✝ : ℕ
N : ℕ+
⊢ IsCongruenceSubgroup (Gamma1 ↑N)
[PROOFSTEP]
refine' ⟨N, _⟩
[GOAL]
N✝ : ℕ
N : ℕ+
⊢ Gamma ↑N ≤ Gamma1 ↑N
[PROOFSTEP]
intro A hA
[GOAL]
N✝ : ℕ
N : ℕ+
A : SL(2, ℤ)
hA : A ∈ Gamma ↑N
⊢ A ∈ Gamma1 ↑N
[PROOFSTEP]
simp only [Gamma1_mem, Gamma_mem] at *
[GOAL]
N✝ : ℕ
N : ℕ+
A : SL(2, ℤ)
hA : ↑(↑A 0 0) = 1 ∧ ↑(↑A 0 1) = 0 ∧ ↑(↑A 1 0) = 0 ∧ ↑(↑A 1 1) = 1
⊢ ↑(↑A 0 0) = 1 ∧ ↑(↑A 1 1) = 1 ∧ ↑(↑A 1 0) = 0
[PROOFSTEP]
simp only [hA, eq_self_iff_true, and_self_iff]
[GOAL]
N✝ N : ℕ
g : ConjAct SL(2, ℤ)
⊢ g • Gamma N = Gamma N
[PROOFSTEP]
apply Subgroup.Normal.conjAct (Gamma_normal N)
[GOAL]
N : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
⊢ IsCongruenceSubgroup (g • Γ)
[PROOFSTEP]
obtain ⟨N, HN⟩ := h
[GOAL]
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ IsCongruenceSubgroup (g • Γ)
[PROOFSTEP]
refine' ⟨N, _⟩
[GOAL]
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ Gamma ↑N ≤ g • Γ
[PROOFSTEP]
rw [← Gamma_cong_eq_self N g, Subgroup.pointwise_smul_le_pointwise_smul_iff]
[GOAL]
case intro
N✝ : ℕ
g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
N : ℕ+
HN : Gamma ↑N ≤ Γ
⊢ Gamma ↑N ≤ Γ
[PROOFSTEP]
exact HN


[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : Field A
inst✝¹ : CharZero A
inst✝ : IsAlgClosed A
⊢ Fintype.card (K →+* A) = finrank ℚ K
[PROOFSTEP]
rw [Fintype.ofEquiv_card RingHom.equivRatAlgHom.symm, AlgHom.card]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : Field A
inst✝¹ : CharZero A
inst✝ : IsAlgClosed A
⊢ Nonempty (K →+* A)
[PROOFSTEP]
rw [← Fintype.card_pos_iff, NumberField.Embeddings.card K A]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : Field A
inst✝¹ : CharZero A
inst✝ : IsAlgClosed A
⊢ 0 < finrank ℚ K
[PROOFSTEP]
exact FiniteDimensional.finrank_pos
[GOAL]
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ => ↑φ x) = rootSet (minpoly ℚ x) A
[PROOFSTEP]
convert (NumberField.isAlgebraic K).range_eval_eq_rootSet_minpoly A x using 1
[GOAL]
case h.e'_2
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
⊢ (range fun φ => ↑φ x) = range fun ψ => ↑ψ x
[PROOFSTEP]
ext a
[GOAL]
case h.e'_2.h
K : Type u_1
A : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : Field A
inst✝¹ : Algebra ℚ A
inst✝ : IsAlgClosed A
x : K
a : (fun x => A) x
⊢ (a ∈ range fun φ => ↑φ x) ↔ a ∈ range fun ψ => ↑ψ x
[PROOFSTEP]
exact ⟨fun ⟨φ, hφ⟩ => ⟨φ.toRatAlgHom, hφ⟩, fun ⟨φ, hφ⟩ => ⟨φ.toRingHom, hφ⟩⟩
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
⊢ ‖coeff (minpoly ℚ x) i‖ ≤ max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))
[PROOFSTEP]
have hx := IsSeparable.isIntegral ℚ x
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖coeff (minpoly ℚ x) i‖ ≤ max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))
[PROOFSTEP]
rw [← norm_algebraMap' A, ← coeff_map (algebraMap ℚ A)]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
⊢ ‖coeff (map (algebraMap ℚ A) (minpoly ℚ x)) i‖ ≤ max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))
[PROOFSTEP]
refine
  coeff_bdd_of_roots_le _ (minpoly.monic hx) (IsAlgClosed.splits_codomain _) (minpoly.natDegree_le x) (fun z hz => ?_) i
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : (fun x => A) (coeff (minpoly ℚ x) i)
hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
⊢ ‖z‖ ≤ B
[PROOFSTEP]
classical
rw [← Multiset.mem_toFinset] at hz
obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
exact h φ
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : (fun x => A) (coeff (minpoly ℚ x) i)
hz : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
⊢ ‖z‖ ≤ B
[PROOFSTEP]
rw [← Multiset.mem_toFinset] at hz
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
z : (fun x => A) (coeff (minpoly ℚ x) i)
hz✝ : z ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
hz : z ∈ Multiset.toFinset (roots (map (algebraMap ℚ A) (minpoly ℚ x)))
⊢ ‖z‖ ≤ B
[PROOFSTEP]
obtain ⟨φ, rfl⟩ := (range_eval_eq_rootSet_minpoly K A x).symm.subset hz
[GOAL]
case intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
x : K
h : ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B
i : ℕ
hx : IsIntegral ℚ x
φ : K →+* A
hz✝ : (fun φ => ↑φ x) φ ∈ roots (map (algebraMap ℚ A) (minpoly ℚ x))
hz : (fun φ => ↑φ x) φ ∈ Multiset.toFinset (roots (map (algebraMap ℚ A) (minpoly ℚ x)))
⊢ ‖(fun φ => ↑φ x) φ‖ ≤ B
[PROOFSTEP]
exact h φ
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
⊢ Set.Finite {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
[PROOFSTEP]
let C := Nat.ceil (max B 1 ^ finrank ℚ K * (finrank ℚ K).choose (finrank ℚ K / 2))
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
⊢ Set.Finite {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
[PROOFSTEP]
have := bUnion_roots_finite (algebraMap ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
⊢ Set.Finite {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
[PROOFSTEP]
refine this.subset fun x hx => ?_
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
⊢ x ∈
    ⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f)))
[PROOFSTEP]
simp_rw [mem_iUnion]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
⊢ ∃ i i_1, x ∈ ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) i)))
[PROOFSTEP]
have h_map_ℚ_minpoly := minpoly.isIntegrallyClosed_eq_field_fractions' ℚ hx.1
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ ∃ i i_1, x ∈ ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) i)))
[PROOFSTEP]
refine ⟨_, ⟨?_, fun i => ?_⟩, mem_rootSet.2 ⟨minpoly.ne_zero hx.1, minpoly.aeval ℤ x⟩⟩
[GOAL]
case refine_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ natDegree (minpoly ℤ x) ≤ finrank ℚ K
[PROOFSTEP]
rw [← (minpoly.monic hx.1).natDegree_map (algebraMap ℤ ℚ), ← h_map_ℚ_minpoly]
[GOAL]
case refine_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
⊢ natDegree (minpoly ℚ x) ≤ finrank ℚ K
[PROOFSTEP]
exact minpoly.natDegree_le x
[GOAL]
case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ coeff (minpoly ℤ x) i ∈
    Icc (-↑⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊)
      ↑⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
[PROOFSTEP]
rw [mem_Icc, ← abs_le, ← @Int.cast_le ℝ]
[GOAL]
case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|coeff (minpoly ℤ x) i| ≤ ↑↑⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
[PROOFSTEP]
refine (Eq.trans_le ?_ <| coeff_bdd_of_norm_le hx.2 i).trans (Nat.le_ceil _)
[GOAL]
case refine_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
A : Type u_2
inst✝² : NormedField A
inst✝¹ : IsAlgClosed A
inst✝ : NormedAlgebra ℚ A
B : ℝ
C : ℕ := ⌈max B 1 ^ finrank ℚ K * ↑(Nat.choose (finrank ℚ K) (finrank ℚ K / 2))⌉₊
this :
  Set.Finite
    (⋃ (f : ℤ[X]) (_ : natDegree f ≤ finrank ℚ K ∧ ∀ (i : ℕ), coeff f i ∈ Icc (-↑C) ↑C),
      ↑(Multiset.toFinset (roots (map (algebraMap ℤ K) f))))
x : K
hx : x ∈ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ B}
h_map_ℚ_minpoly : minpoly ℚ x = map (algebraMap ℤ ℚ) (minpoly ℤ x)
i : ℕ
⊢ ↑|coeff (minpoly ℤ x) i| = ‖coeff (minpoly ℚ x) i‖
[PROOFSTEP]
rw [h_map_ℚ_minpoly, coeff_map, eq_intCast, Int.norm_cast_rat, Int.norm_eq_abs, Int.cast_abs]
[GOAL]
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
⊢ ∃ n x_1, x ^ n = 1
[PROOFSTEP]
obtain ⟨a, -, b, -, habne, h⟩ :=
  @Set.Infinite.exists_ne_map_eq_of_mapsTo _ _ _ _ ((· ^ ·) x : ℕ → K) Set.infinite_univ
    (by exact fun a _ => ⟨hxi.pow a, fun φ => by simp [hx φ]⟩) (finite_of_norm_le K A (1 : ℝ))
[GOAL]
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 x_1 => x ^ x_1) x) univ {x | IsIntegral ℤ x ∧ ∀ (φ : K →+* A), ‖↑φ x‖ ≤ 1}
[PROOFSTEP]
exact fun a _ => ⟨hxi.pow a, fun φ => by simp [hx φ]⟩
[GOAL]
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 x_1 => x ^ x_1) x a)‖ ≤ 1
[PROOFSTEP]
simp [hx φ]
[GOAL]
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 : (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b
⊢ ∃ n x_1, x ^ n = 1
[PROOFSTEP]
wlog hlt : b < a
[GOAL]
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 : (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) 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 → (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b → b < a → ∃ n x_1, x ^ n = 1
hlt : ¬b < a
⊢ ∃ n x_1, x ^ n = 1
[PROOFSTEP]
exact this K A hxi hx b a habne.symm h.symm (habne.lt_or_lt.resolve_right hlt)
[GOAL]
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 : (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b
hlt : b < a
⊢ ∃ n x_1, x ^ n = 1
[PROOFSTEP]
refine ⟨a - b, tsub_pos_of_lt hlt, ?_⟩
[GOAL]
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 : (fun x x_1 => x ^ x_1) x a = (fun x x_1 => x ^ x_1) x b
hlt : b < a
⊢ x ^ (a - b) = 1
[PROOFSTEP]
dsimp at h
[GOAL]
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
[PROOFSTEP]
rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h
[GOAL]
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
[PROOFSTEP]
refine h.resolve_right fun hp => ?_
[GOAL]
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
[PROOFSTEP]
specialize hx (IsAlgClosed.lift (NumberField.isAlgebraic K)).toRingHom
[GOAL]
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 (_ : Algebra.IsAlgebraic ℚ K)) x‖ = 1
⊢ False
[PROOFSTEP]
rw [pow_eq_zero hp, map_zero, norm_zero] at hx
[GOAL]
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
[PROOFSTEP]
norm_num at hx
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ place (conjugate φ) = place φ
[PROOFSTEP]
ext
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x✝ : K
⊢ ↑(place (conjugate φ)) x✝ = ↑(place φ) x✝
[PROOFSTEP]
simp only [place_apply, norm_eq_abs, abs_conj, conjugate_coe_eq]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
⊢ (fun x => (↑φ x).re) 1 = 1
[PROOFSTEP]
simp only [map_one, one_re]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
⊢ ∀ (x y : K),
    OneHom.toFun { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) } (x * y) =
      OneHom.toFun { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) } x *
        OneHom.toFun { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) } y
[PROOFSTEP]
simp only [Complex.conj_eq_iff_im.mp (RingHom.congr_fun hφ _), map_mul, mul_re, mul_zero, tsub_zero, eq_self_iff_true,
  forall_const]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) },
          map_mul' := (_ : ∀ (a a_1 : K), (↑φ (a * a_1)).re = (↑φ a).re * (↑φ a_1).re) })
      0 =
    0
[PROOFSTEP]
simp only [map_zero, zero_re]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
⊢ ∀ (x y : K),
    OneHom.toFun
        (↑{ toOneHom := { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) },
            map_mul' := (_ : ∀ (a a_1 : K), (↑φ (a * a_1)).re = (↑φ a).re * (↑φ a_1).re) })
        (x + y) =
      OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) },
              map_mul' := (_ : ∀ (a a_1 : K), (↑φ (a * a_1)).re = (↑φ a).re * (↑φ a_1).re) })
          x +
        OneHom.toFun
          (↑{ toOneHom := { toFun := fun x => (↑φ x).re, map_one' := (_ : (↑φ 1).re = 1) },
              map_mul' := (_ : ∀ (a a_1 : K), (↑φ (a * a_1)).re = (↑φ a).re * (↑φ a_1).re) })
          y
[PROOFSTEP]
simp only [map_add, add_re, eq_self_iff_true, forall_const]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ ↑(↑(embedding hφ) x) = ↑φ x
[PROOFSTEP]
ext
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(↑(embedding hφ) x)).re = (↑φ x).re
[PROOFSTEP]
rfl
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ (↑(↑(embedding hφ) x)).im = (↑φ x).im
[PROOFSTEP]
rw [ofReal_im, eq_comm, ← Complex.conj_eq_iff_im]
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : IsReal φ
x : K
⊢ ↑(starRingEnd ℂ) (↑φ x) = ↑φ x
[PROOFSTEP]
exact RingHom.congr_fun hφ x
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ mk (ComplexEmbedding.conjugate φ) = mk φ
[PROOFSTEP]
refine FunLike.ext _ _ (fun x => ?_)
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
x : K
⊢ ↑(mk (ComplexEmbedding.conjugate φ)) x = ↑(mk φ) x
[PROOFSTEP]
rw [apply, apply, ComplexEmbedding.conjugate_coe_eq, Complex.abs_conj]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖↑(embedding w) x‖ = ↑w x
[PROOFSTEP]
nth_rewrite 2 [← mk_embedding w]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x : K
⊢ ‖↑(embedding w) x‖ = ↑(mk (embedding w)) x
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
⊢ (∀ (φ : K →+* ℂ), ‖↑φ x‖ = r) → ∀ (w : InfinitePlace K), ↑w x = r
[PROOFSTEP]
rintro hφ ⟨w, ⟨φ, rfl⟩⟩
[GOAL]
case mk.intro
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖↑φ x‖ = r
φ : K →+* ℂ
⊢ ↑{ val := place φ, property := (_ : ∃ φ_1, place φ_1 = place φ) } x = r
[PROOFSTEP]
exact hφ φ
[GOAL]
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
⊢ (∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r) → ∀ (w : InfinitePlace K), ↑w x ≤ r
[PROOFSTEP]
rintro hφ ⟨w, ⟨φ, rfl⟩⟩
[GOAL]
case mk.intro
K : Type u_1
inst✝ : Field K
x : K
r : ℝ
hφ : ∀ (φ : K →+* ℂ), ‖↑φ x‖ ≤ r
φ : K →+* ℂ
⊢ ↑{ val := place φ, property := (_ : ∃ φ_1, place φ_1 = place φ) } x ≤ r
[PROOFSTEP]
exact hφ φ
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ ↔ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ mk φ = mk ψ → φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
intro h₀
[GOAL]
case mp
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
obtain ⟨j, hiφ⟩ := (φ.injective).hasLeftInverse
[GOAL]
case mp.intro
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
let ι := RingEquiv.ofLeftInverse hiφ
[GOAL]
case mp.intro
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
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, NormedField.dist_eq, 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 ι _]
    rfl
  exact congrFun (congrArg (↑) h₀) _
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
[PROOFSTEP]
change LipschitzWith 1 (ψ ∘ ι.symm)
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
⊢ LipschitzWith 1 (↑ψ ∘ ↑(RingEquiv.symm ι))
[PROOFSTEP]
apply LipschitzWith.of_dist_le_mul
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
⊢ ∀ (x y : { x // x ∈ RingHom.range φ }),
    dist ((↑ψ ∘ ↑(RingEquiv.symm ι)) x) ((↑ψ ∘ ↑(RingEquiv.symm ι)) y) ≤ ↑1 * dist x y
[PROOFSTEP]
intro x y
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
⊢ dist ((↑ψ ∘ ↑(RingEquiv.symm ι)) x) ((↑ψ ∘ ↑(RingEquiv.symm ι)) y) ≤ ↑1 * dist x y
[PROOFSTEP]
rw [NNReal.coe_one, one_mul, NormedField.dist_eq, Function.comp_apply, Function.comp_apply, ← map_sub, ← map_sub]
[GOAL]
case a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
⊢ ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖ ≤ dist x y
[PROOFSTEP]
apply le_of_eq
[GOAL]
case a.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
⊢ ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖ = dist x y
[PROOFSTEP]
suffices ‖φ (ι.symm (x - y))‖ = ‖ψ (ι.symm (x - y))‖
  by
  rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _]
  rfl
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
this : ‖↑φ (↑(RingEquiv.symm ι) (x - y))‖ = ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖
⊢ ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖ = dist x y
[PROOFSTEP]
rw [← this, ← RingEquiv.ofLeftInverse_apply hiφ _, RingEquiv.apply_symm_apply ι _]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
this : ‖↑φ (↑(RingEquiv.symm ι) (x - y))‖ = ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖
⊢ ‖↑(x - y)‖ = dist x y
[PROOFSTEP]
rfl
[GOAL]
case a.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
x y : { x // x ∈ RingHom.range φ }
⊢ ‖↑φ (↑(RingEquiv.symm ι) (x - y))‖ = ‖↑ψ (↑(RingEquiv.symm ι) (x - y))‖
[PROOFSTEP]
exact congrFun (congrArg (↑) h₀) _
[GOAL]
case mp.intro
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
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]
case mp.intro
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
x✝ :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ)) ∨
    (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
      ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
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]
case mp.intro.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]

| inl h =>
  left; ext1 x
  conv_rhs => rw [← hiφ x]
  exact (congrFun h (ι x)).symm
[GOAL]
case mp.intro.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
left
[GOAL]
case mp.intro.inl.h
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ
[PROOFSTEP]
ext1 x
[GOAL]
case mp.intro.inl.h.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
conv_rhs => rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
case mp.intro.inl.h.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h : (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun = ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
⊢ ↑φ x = ↑ψ (j (↑φ x))
[PROOFSTEP]
exact (congrFun h (ι x)).symm
[GOAL]
case mp.intro.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]

| inr h =>
  right; ext1 x
  conv_rhs => rw [← hiφ x]
  exact (congrFun h (ι x)).symm
[GOAL]
case mp.intro.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
right
[GOAL]
case mp.intro.inr.h
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
⊢ ComplexEmbedding.conjugate φ = ψ
[PROOFSTEP]
ext1 x
[GOAL]
case mp.intro.inr.h.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
⊢ ↑(ComplexEmbedding.conjugate φ) x = ↑ψ x
[PROOFSTEP]
conv_rhs => rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
| ↑ψ x
[PROOFSTEP]
rw [← hiφ x]
[GOAL]
case mp.intro.inr.h.a
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h₀ : mk φ = mk ψ
j : ℂ → K
hiφ : Function.LeftInverse j ↑φ
ι : K ≃+* { x // x ∈ RingHom.range φ } := RingEquiv.ofLeftInverse hiφ
hlip : LipschitzWith 1 ↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))
h :
  (↑↑(RingHom.comp ψ (RingEquiv.toRingHom (RingEquiv.symm ι)))).toFun =
    ↑(starRingEnd ℂ) ∘ ↑(Subfield.subtype (RingHom.fieldRange φ))
x : K
⊢ ↑(ComplexEmbedding.conjugate φ) x = ↑ψ (j (↑φ x))
[PROOFSTEP]
exact (congrFun h (ι x)).symm
[GOAL]
case mpr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
⊢ φ = ψ ∨ ComplexEmbedding.conjugate φ = ψ → mk φ = mk ψ
[PROOFSTEP]
rintro (⟨h⟩ | ⟨h⟩)
[GOAL]
case mpr.inl
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : φ = ψ
⊢ mk φ = mk ψ
[PROOFSTEP]
exact congr_arg mk h
[GOAL]
case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk φ = mk ψ
[PROOFSTEP]
rw [← mk_conjugate_eq]
[GOAL]
case mpr.inr
K : Type u_1
inst✝ : Field K
φ ψ : K →+* ℂ
h : ComplexEmbedding.conjugate φ = ψ
⊢ mk (ComplexEmbedding.conjugate φ) = mk ψ
[PROOFSTEP]
exact congr_arg mk h
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
⊢ embedding (mk φ) = φ ∨ embedding (mk φ) = ComplexEmbedding.conjugate φ
[PROOFSTEP]
rw [@eq_comm _ _ φ, @eq_comm _ _ (ComplexEmbedding.conjugate φ), ← mk_eq_iff, mk_embedding]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ embedding (mk φ) = φ
[PROOFSTEP]
have := embedding_mk_eq φ
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
this : embedding (mk φ) = φ ∨ embedding (mk φ) = ComplexEmbedding.conjugate φ
⊢ embedding (mk φ) = φ
[PROOFSTEP]
rwa [ComplexEmbedding.isReal_iff.mp h, or_self] at this
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsReal w ↔ ComplexEmbedding.IsReal (embedding w)
[PROOFSTEP]
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsReal w → ComplexEmbedding.IsReal (embedding w)
[PROOFSTEP]
rintro ⟨φ, ⟨hφ, rfl⟩⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal φ
⊢ ComplexEmbedding.IsReal (embedding (mk φ))
[PROOFSTEP]
rwa [embedding_mk_eq_of_isReal hφ]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsComplex w ↔ ¬ComplexEmbedding.IsReal (embedding w)
[PROOFSTEP]
refine ⟨?_, fun h => ⟨embedding w, h, mk_embedding w⟩⟩
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsComplex w → ¬ComplexEmbedding.IsReal (embedding w)
[PROOFSTEP]
rintro ⟨φ, ⟨hφ, rfl⟩⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ¬ComplexEmbedding.IsReal φ
⊢ ¬ComplexEmbedding.IsReal (embedding (mk φ))
[PROOFSTEP]
contrapose! hφ
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
cases mk_eq_iff.mp (mk_embedding (mk φ)) with
| inl h => rwa [h] at hφ
| inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ
[GOAL]
case intro.intro
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
x✝ : embedding (mk φ) = φ ∨ ComplexEmbedding.conjugate (embedding (mk φ)) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
cases mk_eq_iff.mp (mk_embedding (mk φ)) with
| inl h => rwa [h] at hφ
| inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ
[GOAL]
case intro.intro.inl
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
h : embedding (mk φ) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]

| inl h => rwa [h] at hφ
[GOAL]
case intro.intro.inl
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
h : embedding (mk φ) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
rwa [h] at hφ
[GOAL]
case intro.intro.inr
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
h : ComplexEmbedding.conjugate (embedding (mk φ)) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]

| inr h => rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ
[GOAL]
case intro.intro.inr
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
hφ : ComplexEmbedding.IsReal (embedding (mk φ))
h : ComplexEmbedding.conjugate (embedding (mk φ)) = φ
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
rwa [← ComplexEmbedding.isReal_conjugate_iff, h] at hφ
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ ¬IsReal w ↔ IsComplex w
[PROOFSTEP]
rw [isComplex_iff, isReal_iff]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsReal w ∨ IsComplex w
[PROOFSTEP]
rw [← not_isReal_iff_isComplex]
[GOAL]
K : Type u_1
inst✝ : Field K
w : InfinitePlace K
⊢ IsReal w ∨ ¬IsReal w
[PROOFSTEP]
exact em _
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : IsReal (mk φ)
⊢ ComplexEmbedding.IsReal φ
[PROOFSTEP]
contrapose! h
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ ¬IsReal (mk φ)
[PROOFSTEP]
rw [not_isReal_iff_isComplex]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ¬ComplexEmbedding.IsReal φ
⊢ IsComplex (mk φ)
[PROOFSTEP]
exact ⟨φ, h, rfl⟩
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : IsComplex (mk φ)
⊢ ¬ComplexEmbedding.IsReal φ
[PROOFSTEP]
contrapose! h
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ ¬IsComplex (mk φ)
[PROOFSTEP]
rw [← not_isReal_iff_isComplex.not, not_not]
[GOAL]
K : Type u_1
inst✝ : Field K
φ : K →+* ℂ
h : ComplexEmbedding.IsReal φ
⊢ IsReal (mk φ)
[PROOFSTEP]
exact ⟨φ, h, rfl⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ) = mult w
[PROOFSTEP]
conv_lhs =>
  congr; congr; ext
  rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ)
[PROOFSTEP]
  congr; congr; ext
  rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ)
[PROOFSTEP]
  congr; congr; ext
  rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ)
[PROOFSTEP]
congr
[GOAL]
case s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.filter (fun φ => mk φ = w) Finset.univ
[PROOFSTEP]
congr
[GOAL]
case s.p
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| fun φ => mk φ = w
case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ
K : Type u_1 inst✝¹ : Field K inst✝ : NumberField K w : InfinitePlace K ⊢ DecidablePred ?m.1138470
[PROOFSTEP]
ext
[GOAL]
case s.p.h
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : K →+* ℂ
| mk x✝ = w
case s.s
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
| Finset.univ
K : Type u_1 inst✝¹ : Field K inst✝ : NumberField K w : InfinitePlace K ⊢ DecidablePred ?m.1138470
[PROOFSTEP]
rw [← mk_embedding w, mk_eq_iff, ComplexEmbedding.conjugate, star_involutive.eq_iff]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ Finset.card (Finset.filter (fun x => x = embedding w ∨ x = star (embedding w)) Finset.univ) = mult w
[PROOFSTEP]
simp_rw [Finset.filter_or, Finset.filter_eq' _ (embedding w),
  Finset.filter_eq' _ (ComplexEmbedding.conjugate (embedding w)), Finset.mem_univ, ite_true, mult]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
⊢ Finset.card ({embedding w} ∪ {ComplexEmbedding.conjugate (embedding w)}) = if IsReal w then 1 else 2
[PROOFSTEP]
split_ifs with hw
[GOAL]
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsReal w
⊢ Finset.card ({embedding w} ∪ {ComplexEmbedding.conjugate (embedding w)}) = 1
[PROOFSTEP]
rw [ComplexEmbedding.isReal_iff.mp (isReal_iff.mp hw), Finset.union_idempotent, Finset.card_singleton]
[GOAL]
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬IsReal w
⊢ Finset.card ({embedding w} ∪ {ComplexEmbedding.conjugate (embedding w)}) = 2
[PROOFSTEP]
refine Finset.card_doubleton ?_
[GOAL]
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : ¬IsReal w
⊢ embedding w ≠ ComplexEmbedding.conjugate (embedding w)
[PROOFSTEP]
rwa [Ne.def, eq_comm, ← ComplexEmbedding.isReal_iff, ← isReal_iff]
[GOAL]
K : Type u_1
inst✝ : Field K
⊢ { φ // ComplexEmbedding.IsReal φ } ≃ { w // IsReal w }
[PROOFSTEP]
refine (Equiv.ofBijective (fun φ => ⟨mk φ, ?_⟩) ⟨fun φ ψ h => ?_, fun w => ?_⟩)
[GOAL]
case refine_1
K : Type u_1
inst✝ : Field K
φ : { φ // ComplexEmbedding.IsReal φ }
⊢ IsReal (mk ↑φ)
[PROOFSTEP]
exact ⟨φ, φ.prop, rfl⟩
[GOAL]
case refine_2
K : Type u_1
inst✝ : Field K
φ ψ : { φ // ComplexEmbedding.IsReal φ }
h :
  (fun φ => { val := mk ↑φ, property := (_ : ∃ φ_1, ComplexEmbedding.IsReal φ_1 ∧ mk φ_1 = mk ↑φ) }) φ =
    (fun φ => { val := mk ↑φ, property := (_ : ∃ φ_1, ComplexEmbedding.IsReal φ_1 ∧ mk φ_1 = mk ↑φ) }) ψ
⊢ φ = ψ
[PROOFSTEP]
rwa [Subtype.mk.injEq, mk_eq_iff, ComplexEmbedding.isReal_iff.mp φ.prop, or_self, ← Subtype.ext_iff] at h
[GOAL]
case refine_3
K : Type u_1
inst✝ : Field K
w : { w // IsReal w }
⊢ ∃ a, (fun φ => { val := mk ↑φ, property := (_ : ∃ φ_1, ComplexEmbedding.IsReal φ_1 ∧ mk φ_1 = mk ↑φ) }) a = w
[PROOFSTEP]
exact ⟨⟨embedding w, isReal_iff.mp w.prop⟩, by simp⟩
[GOAL]
K : Type u_1
inst✝ : Field K
w : { w // IsReal w }
⊢ (fun φ => { val := mk ↑φ, property := (_ : ∃ φ_1, ComplexEmbedding.IsReal φ_1 ∧ mk φ_1 = mk ↑φ) })
      { val := embedding ↑w, property := (_ : ComplexEmbedding.IsReal (embedding ↑w)) } =
    w
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w = ↑|↑(Algebra.norm ℚ) x|
[PROOFSTEP]
convert (congr_arg Complex.abs (@Algebra.norm_eq_prod_embeddings ℚ _ _ _ _ ℂ _ _ _ _ _ x)).symm
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w = ↑Complex.abs (∏ σ : K →ₐ[ℚ] ℂ, ↑σ x)
[PROOFSTEP]
rw [map_prod, ←
  Equiv.prod_comp' RingHom.equivRatAlgHom (fun f => Complex.abs (f x)) (fun φ => Complex.abs (φ x)) fun _ => by
    simp [RingHom.equivRatAlgHom_apply]; rfl]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
x✝ : K →+* ℂ
⊢ (fun f => ↑Complex.abs (↑f x)) x✝ = (fun φ => ↑Complex.abs (↑φ x)) (↑RingHom.equivRatAlgHom x✝)
[PROOFSTEP]
simp [RingHom.equivRatAlgHom_apply]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
x✝ : K →+* ℂ
⊢ ↑Complex.abs (↑x✝ x) = ↑Complex.abs (↑(RingHom.toRatAlgHom x✝) x)
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w = ∏ i : K →+* ℂ, ↑Complex.abs (↑i x)
[PROOFSTEP]
rw [← Finset.prod_fiberwise Finset.univ (fun φ => mk φ) (fun φ => Complex.abs (φ x))]
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w =
    ∏ b : InfinitePlace K, ∏ a in Finset.filter (fun a => mk a = b) Finset.univ, ↑Complex.abs (↑a x)
[PROOFSTEP]
have : ∀ w : InfinitePlace K, ∀ φ ∈ Finset.filter (fun a ↦ mk a = w) Finset.univ, Complex.abs (φ x) = w x :=
  by
  intro _ _ hφ
  rw [← (Finset.mem_filter.mp hφ).2]
  rfl
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ∀ (w : InfinitePlace K) (φ : K →+* ℂ), φ ∈ Finset.filter (fun a => mk a = w) Finset.univ → ↑Complex.abs (↑φ x) = ↑w x
[PROOFSTEP]
intro _ _ hφ
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
w✝ : InfinitePlace K
φ✝ : K →+* ℂ
hφ : φ✝ ∈ Finset.filter (fun a => mk a = w✝) Finset.univ
⊢ ↑Complex.abs (↑φ✝ x) = ↑w✝ x
[PROOFSTEP]
rw [← (Finset.mem_filter.mp hφ).2]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
w✝ : InfinitePlace K
φ✝ : K →+* ℂ
hφ : φ✝ ∈ Finset.filter (fun a => mk a = w✝) Finset.univ
⊢ ↑Complex.abs (↑φ✝ x) = ↑(mk φ✝) x
[PROOFSTEP]
rfl
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
this :
  ∀ (w : InfinitePlace K) (φ : K →+* ℂ), φ ∈ Finset.filter (fun a => mk a = w) Finset.univ → ↑Complex.abs (↑φ x) = ↑w x
⊢ ∏ w : InfinitePlace K, ↑w x ^ mult w =
    ∏ b : InfinitePlace K, ∏ a in Finset.filter (fun a => mk a = b) Finset.univ, ↑Complex.abs (↑a x)
[PROOFSTEP]
simp_rw [Finset.prod_congr rfl (this _), Finset.prod_const, card_filter_mk_eq]
[GOAL]
case h.e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ↑|↑(Algebra.norm ℚ) x| = ↑Complex.abs (↑(algebraMap ℚ ℂ) (↑(Algebra.norm ℚ) x))
[PROOFSTEP]
rw [eq_ratCast, Rat.cast_abs, ← Complex.abs_ofReal, Complex.ofReal_rat_cast]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ¬ComplexEmbedding.IsReal φ } = 2 * card { w // IsComplex w }
[PROOFSTEP]
suffices
  ∀ w : { w : InfinitePlace K // IsComplex w },
    (Finset.univ.filter fun φ : { φ // ¬ComplexEmbedding.IsReal φ } => mkComplex φ = w).card = 2
  by
  rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]
  simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones, Finset.mul_sum]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // IsComplex w }), Finset.card (Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
⊢ card { φ // ¬ComplexEmbedding.IsReal φ } = 2 * card { w // IsComplex w }
[PROOFSTEP]
rw [Fintype.card, Finset.card_eq_sum_ones, ← Finset.sum_fiberwise _ (fun φ => mkComplex φ)]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : ∀ (w : { w // IsComplex w }), Finset.card (Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
⊢ ∑ b : { w // IsComplex w }, ∑ a in Finset.filter (fun a => mkComplex a = b) Finset.univ, 1 =
    2 * card { w // IsComplex w }
[PROOFSTEP]
simp_rw [Finset.sum_const, this, smul_eq_mul, mul_one, Fintype.card, Finset.card_eq_sum_ones, Finset.mul_sum]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ∀ (w : { w // IsComplex w }), Finset.card (Finset.filter (fun φ => mkComplex φ = w) Finset.univ) = 2
[PROOFSTEP]
rintro ⟨w, hw⟩
[GOAL]
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ Finset.card (Finset.filter (fun φ => mkComplex φ = { val := w, property := hw }) Finset.univ) = 2
[PROOFSTEP]
convert card_filter_mk_eq w
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ Finset.card (Finset.filter (fun φ => mkComplex φ = { val := w, property := hw }) Finset.univ) =
    Finset.card (Finset.filter (fun φ => mk φ = w) Finset.univ)
[PROOFSTEP]
rw [← Fintype.card_subtype, ← Fintype.card_subtype]
[GOAL]
case h.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ card { x // mkComplex x = { val := w, property := hw } } = card { x // mk x = w }
[PROOFSTEP]
refine Fintype.card_congr (Equiv.ofBijective ?_ ⟨fun _ _ h => ?_, fun ⟨φ, hφ⟩ => ?_⟩)
[GOAL]
case h.e'_2.refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ { x // mkComplex x = { val := w, property := hw } } → { x // mk x = w }
[PROOFSTEP]
exact fun ⟨φ, hφ⟩ => ⟨φ.val, by rwa [Subtype.ext_iff] at hφ ⟩
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
x✝ : { x // mkComplex x = { val := w, property := hw } }
φ : { φ // ¬ComplexEmbedding.IsReal φ }
hφ : mkComplex φ = { val := w, property := hw }
⊢ mk ↑φ = w
[PROOFSTEP]
rwa [Subtype.ext_iff] at hφ
[GOAL]
case h.e'_2.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
x✝¹ x✝ : { x // mkComplex x = { val := w, property := hw } }
h :
  (match x✝¹ with
    | { val := φ, property := hφ } => { val := ↑φ, property := (_ : ↑(mkComplex φ) = ↑{ val := w, property := hw }) }) =
    match x✝ with
    | { val := φ, property := hφ } => { val := ↑φ, property := (_ : ↑(mkComplex φ) = ↑{ val := w, property := hw }) }
⊢ x✝¹ = x✝
[PROOFSTEP]
rwa [Subtype.mk_eq_mk, ← Subtype.ext_iff, ← Subtype.ext_iff] at h
[GOAL]
case h.e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ ∃ a,
    (match a with
      | { val := φ, property := hφ } =>
        { val := ↑φ, property := (_ : ↑(mkComplex φ) = ↑{ val := w, property := hw }) }) =
      { val := φ, property := hφ }
[PROOFSTEP]
refine ⟨⟨⟨φ, not_isReal_of_mk_isComplex (hφ.symm ▸ hw)⟩, ?_⟩, rfl⟩
[GOAL]
case h.e'_2.refine_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
x✝ : { x // mk x = w }
φ : K →+* ℂ
hφ : mk φ = w
⊢ mkComplex { val := φ, property := (_ : ¬ComplexEmbedding.IsReal φ) } = { val := w, property := hw }
[PROOFSTEP]
rwa [Subtype.ext_iff, mkComplex_coe]
[GOAL]
case h.e'_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
hw : IsComplex w
⊢ 2 = mult w
[PROOFSTEP]
simp_rw [mult, not_isReal_iff_isComplex.mpr hw]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { w // IsReal w } + 2 * card { w // IsComplex w } = finrank ℚ K
[PROOFSTEP]
rw [← card_real_embeddings, ← card_complex_embeddings]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ComplexEmbedding.IsReal φ } + card { φ // ¬ComplexEmbedding.IsReal φ } = finrank ℚ K
[PROOFSTEP]
rw [Fintype.card_subtype_compl, ← Embeddings.card K ℂ, Nat.add_sub_of_le]
[GOAL]
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ card { φ // ComplexEmbedding.IsReal φ } ≤ card (K →+* ℂ)
[PROOFSTEP]
exact Fintype.card_subtype_le _


[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsSeparable K L
x : { x // x ∈ 𝓞 K }
⊢ ↑(norm K) (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) x) = x ^ finrank K L
[PROOFSTEP]
rw [← Subtype.coe_inj, RingOfIntegers.coe_norm_algebraMap, Algebra.norm_algebraMap, SubsemiringClass.coe_pow]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
classical
refine' ⟨fun hx => _, IsUnit.map _⟩
replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)
refine'
  @isUnit_of_mul_isUnit_right (𝓞 L) _
    ⟨(univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x,
      prod_mem fun σ _ => map_isIntegral (σ : L →+* L).toIntAlgHom x.2⟩
    _ _
convert hx using 1
ext
push_cast
convert_to
  ((univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x) * ∏ σ : L ≃ₐ[K] L in { AlgEquiv.refl }, σ (x : L) = _
· rw [prod_singleton, AlgEquiv.coe_refl, _root_.id]
· rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
refine' ⟨fun hx => _, IsUnit.map _⟩
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(norm K) x)
⊢ IsUnit x
[PROOFSTEP]
replace hx : IsUnit (algebraMap (𝓞 K) (𝓞 L) <| norm K x) := hx.map (algebraMap (𝓞 K) <| 𝓞 L)
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ IsUnit x
[PROOFSTEP]
refine'
  @isUnit_of_mul_isUnit_right (𝓞 L) _
    ⟨(univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x,
      prod_mem fun σ _ => map_isIntegral (σ : L →+* L).toIntAlgHom x.2⟩
    _ _
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ IsUnit
    ({ val := ∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x, property := (_ : ∏ c in univ \ {AlgEquiv.refl}, ↑c ↑x ∈ 𝓞 L) } * x)
[PROOFSTEP]
convert hx using 1
[GOAL]
case h.e'_3
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ { val := ∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x, property := (_ : ∏ c in univ \ {AlgEquiv.refl}, ↑c ↑x ∈ 𝓞 L) } * x =
    ↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.a
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ ↑({ val := ∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x, property := (_ : ∏ c in univ \ {AlgEquiv.refl}, ↑c ↑x ∈ 𝓞 L) } * x) =
    ↑(↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
[PROOFSTEP]
push_cast
[GOAL]
case h.e'_3.a
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ (∏ x_1 in univ \ {AlgEquiv.refl}, ↑x_1 ↑x) * ↑x = ↑(↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
[PROOFSTEP]
convert_to
  ((univ \ { AlgEquiv.refl }).prod fun σ : L ≃ₐ[K] L => σ x) * ∏ σ : L ≃ₐ[K] L in { AlgEquiv.refl }, σ (x : L) = _
[GOAL]
case h.e'_2
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ (∏ x_1 in univ \ {AlgEquiv.refl}, ↑x_1 ↑x) * ↑x =
    (∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x) * ∏ σ in {AlgEquiv.refl}, ↑σ ↑x
[PROOFSTEP]
rw [prod_singleton, AlgEquiv.coe_refl, _root_.id]
[GOAL]
case h.e'_3.a.convert_2
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hx : IsUnit (↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
⊢ (∏ σ in univ \ {AlgEquiv.refl}, ↑σ ↑x) * ∏ σ in {AlgEquiv.refl}, ↑σ ↑x =
    ↑(↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x))
[PROOFSTEP]
rw [prod_sdiff <| subset_univ _, ← norm_eq_prod_automorphisms, coe_algebraMap_norm]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
⊢ x ∣ ↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)
[PROOFSTEP]
classical
have hint : ∏ σ : L ≃ₐ[K] L in univ.erase AlgEquiv.refl, σ x ∈ 𝓞 L :=
  Subalgebra.prod_mem _ fun σ _ => (mem_ringOfIntegers _ _).2 (map_isIntegral σ (RingOfIntegers.isIntegral_coe x))
refine' ⟨⟨_, hint⟩, Subtype.ext _⟩
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
⊢ x ∣ ↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)
[PROOFSTEP]
have hint : ∏ σ : L ≃ₐ[K] L in univ.erase AlgEquiv.refl, σ x ∈ 𝓞 L :=
  Subalgebra.prod_mem _ fun σ _ => (mem_ringOfIntegers _ _).2 (map_isIntegral σ (RingOfIntegers.isIntegral_coe x))
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hint : ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x ∈ 𝓞 L
⊢ x ∣ ↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)
[PROOFSTEP]
refine' ⟨⟨_, hint⟩, Subtype.ext _⟩
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hint : ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x ∈ 𝓞 L
⊢ ↑(↑(algebraMap { x // x ∈ 𝓞 K } { x // x ∈ 𝓞 L }) (↑(norm K) x)) =
    ↑(x * { val := ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x, property := hint })
[PROOFSTEP]
rw [coe_algebraMap_norm K x, norm_eq_prod_automorphisms]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : { x // x ∈ 𝓞 L }
hint : ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x ∈ 𝓞 L
⊢ ∏ σ : L ≃ₐ[K] L, ↑σ ↑x = ↑(x * { val := ∏ σ in erase univ AlgEquiv.refl, ↑σ ↑x, property := hint })
[PROOFSTEP]
simp [← Finset.mul_prod_erase _ _ (mem_univ AlgEquiv.refl)]
[GOAL]
L : Type u_1
K : Type u_2
inst✝¹² : Field K
inst✝¹¹ : Field L
inst✝¹⁰ : Algebra K L
inst✝⁹ : FiniteDimensional K L
F : Type u_3
inst✝⁸ : Field F
inst✝⁷ : Algebra K F
inst✝⁶ : IsSeparable K F
inst✝⁵ : FiniteDimensional K F
inst✝⁴ : IsSeparable K L
inst✝³ : Algebra F L
inst✝² : IsSeparable F L
inst✝¹ : FiniteDimensional F L
inst✝ : IsScalarTower K F L
x : { x // x ∈ 𝓞 L }
⊢ ↑(norm K) (↑(norm F) x) = ↑(norm K) x
[PROOFSTEP]
rw [← Subtype.coe_inj, norm_apply_coe, norm_apply_coe, norm_apply_coe, Algebra.norm_norm]
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
letI : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
[GOAL]
L : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Algebra K L
inst✝⁵ : FiniteDimensional K L
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
let L := normalClosure K F (AlgebraicClosure F)
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
haveI : FiniteDimensional F L := FiniteDimensional.right K F L
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this✝ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this : FiniteDimensional F { x // x ∈ L }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
haveI : IsAlgClosure K (AlgebraicClosure F) :=
  IsAlgClosure.ofAlgebraic K F (AlgebraicClosure F) (Algebra.isAlgebraic_of_finite K F)
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this✝¹ : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝ : FiniteDimensional F { x // x ∈ L }
this : IsAlgClosure K (AlgebraicClosure F)
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
haveI : IsGalois F L := IsGalois.tower_top_of_isGalois K F L
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this✝² : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝¹ : FiniteDimensional F { x // x ∈ L }
this✝ : IsAlgClosure K (AlgebraicClosure F)
this : IsGalois F { x // x ∈ L }
⊢ IsUnit (↑(norm K) x) ↔ IsUnit x
[PROOFSTEP]
calc
  IsUnit (norm K x) ↔ IsUnit ((norm K) x ^ finrank F L) := (isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)).symm
  _ ↔ IsUnit (norm K (algebraMap (𝓞 F) (𝓞 L) x)) := by
    rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]
  _ ↔ IsUnit (algebraMap (𝓞 F) (𝓞 L) x) := (isUnit_norm_of_isGalois K)
  _ ↔ IsUnit (norm F (algebraMap (𝓞 F) (𝓞 L) x)) := (isUnit_norm_of_isGalois F).symm
  _ ↔ IsUnit (x ^ finrank F L) := (congr_arg IsUnit (norm_algebraMap F _)).to_iff
  _ ↔ IsUnit x := isUnit_pow_iff (pos_iff_ne_zero.mp finrank_pos)
[GOAL]
L✝ : Type u_1
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Field L✝
inst✝⁶ : Algebra K L✝
inst✝⁵ : FiniteDimensional K L✝
F : Type u_3
inst✝⁴ : Field F
inst✝³ : Algebra K F
inst✝² : IsSeparable K F
inst✝¹ : FiniteDimensional K F
inst✝ : CharZero K
x : { x // x ∈ 𝓞 F }
this✝² : Algebra K (AlgebraicClosure K) := AlgebraicClosure.instAlgebra K
L : IntermediateField F (AlgebraicClosure F) := normalClosure K F (AlgebraicClosure F)
this✝¹ : FiniteDimensional F { x // x ∈ L }
this✝ : IsAlgClosure K (AlgebraicClosure F)
this : IsGalois F { x // x ∈ L }
⊢ IsUnit (↑(norm K) x ^ finrank F { x // x ∈ L }) ↔
    IsUnit (↑(norm K) (↑(algebraMap { x // x ∈ 𝓞 F } { x // x ∈ 𝓞 { x // x ∈ L } }) x))
[PROOFSTEP]
rw [← norm_norm K F (algebraMap (𝓞 F) (𝓞 L) x), norm_algebraMap F _, map_pow]