Theorem: ℤω.normSq_mod_lt (Mordell4/Eisenstein.lean)

State before:
a b c : ℤω
h : b ≠ 0
⊢ natNorm (mod a b) < natNorm b
Tactic:
suffices Complex.normSq (mod a b) < normSq b
  by
  simp only [natNorm_coe] at this
  exact_mod_cast this
State after:
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) (mod a b)) < ↑normSq (OneHom.toFun (↑↑inclusion) b)

State before:
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (OneHom.toFun (↑↑inclusion) (mod a b)) < ↑normSq (OneHom.toFun (↑↑inclusion) b)
Tactic:
simp [mod, div]
State after:
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)

State before:
a b c : ℤω
h : b ≠ 0
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
have bound : Complex.normSq (a / b - nearestℤω (a / b)) < 1 :=
  norm_sub_nearestℤω_self_lt (a / b : ℂ)
State after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)

State before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
have : (a / b : ℂ) - nearestℤω (a / b) = (a - nearestℤω (a / b) * b) * b⁻¹ :=
  by
  ring_nf
  have : (b : ℂ) * (b : ℂ)⁻¹ = 1 := by
    apply mul_inv_cancel
    simpa [coe_eq_zero] using h
  congr
  rw [mul_comm (b : ℂ)]
  rw [_root_.mul_assoc]
  rw [this]
  rw [_root_.mul_one]
State after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)

State before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
rw [this] at bound
State after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      ((OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
        sorryAx ℂ true) <
    1
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)

State before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      ((OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
        sorryAx ℂ true) <
    1
this :
  OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
clear this
State after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      ((OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
        sorryAx ℂ true) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)

State before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      ((OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
        sorryAx ℂ true) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)
Tactic:
rw [normSq_mul] at bound
State after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
        (OneHom.toFun (↑↑inclusion) a -
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
            OneHom.toFun (↑↑inclusion) b) *
      ↑normSq (sorryAx ℂ true) <
    1
⊢ ↑normSq (↑inclusion a - ↑inclusion b * ↑inclusion (nearestℤω (↑inclusion a / ↑inclusion b))) < ↑normSq (↑inclusion b)

State before:
a b c : ℤω
h : b ≠ 0
this : ↑normSq (OneHom.toFun (↑↑inclusion) (mod a b)) < ↑normSq (OneHom.toFun (↑↑inclusion) b)
⊢ natNorm (mod a b) < natNorm b
Tactic:
simp only [natNorm_coe] at this
State after:
a b c : ℤω
h : b ≠ 0
this : ↑(natNorm (mod a b)) < ↑(natNorm b)
⊢ natNorm (mod a b) < natNorm b

State before:
a b c : ℤω
h : b ≠ 0
this : ↑(natNorm (mod a b)) < ↑(natNorm b)
⊢ natNorm (mod a b) < natNorm b
Tactic:
exact_mod_cast this
State after:
no goals

State before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) =
    (OneHom.toFun (↑↑inclusion) a -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b)) *
          OneHom.toFun (↑↑inclusion) b) *
      sorryAx ℂ true
Tactic:
ring_nf
State after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true

State before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true
Tactic:
have : (b : ℂ) * (b : ℂ)⁻¹ = 1 := by
  apply mul_inv_cancel
  simpa [coe_eq_zero] using h
State after:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true

State before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹ -
      OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) a * sorryAx ℂ true -
      OneHom.toFun (↑↑inclusion) b *
          OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
        sorryAx ℂ true
Tactic:
congr
State after:
case e_a.e_a
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ (OneHom.toFun (↑↑inclusion) b)⁻¹ = sorryAx ℂ true

case e_a
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
this : OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
⊢ OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) =
    OneHom.toFun (↑↑inclusion) b *
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a * (OneHom.toFun (↑↑inclusion) b)⁻¹)) *
      sorryAx ℂ true

State before:
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b * (OneHom.toFun (↑↑inclusion) b)⁻¹ = 1
Tactic:
apply mul_inv_cancel
State after:
case h
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b ≠ 0

State before:
case h
a b c : ℤω
h : b ≠ 0
bound :
  ↑normSq
      (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b -
        OneHom.toFun (↑↑inclusion) (nearestℤω (OneHom.toFun (↑↑inclusion) a / OneHom.toFun (↑↑inclusion) b))) <
    1
⊢ OneHom.toFun (↑↑inclusion) b ≠ 0
Tactic:
simpa [coe_eq_zero] using h
State after:
no goals