[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ₀ χ₁ : MulChar R R'
h : (fun χ => χ.toFun) χ₀ = (fun χ => χ.toFun) χ₁
⊢ χ₀ = χ₁
[PROOFSTEP]
cases χ₀
[GOAL]
case mk
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ₁ : MulChar R R'
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝) a = 0
h : (fun χ => χ.toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } = (fun χ => χ.toFun) χ₁
⊢ { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } = χ₁
[PROOFSTEP]
cases χ₁
[GOAL]
case mk.mk
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝¹) a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝) a = 0
h :
  (fun χ => χ.toFun) { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    (fun χ => χ.toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
⊢ { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMonoidHom
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝¹) a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝) a = 0
h :
  (fun χ => χ.toFun) { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    (fun χ => χ.toFun) { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
⊢ toMonoidHom✝¹ = toMonoidHom✝
[PROOFSTEP]
apply MonoidHom.ext (fun _ => congr_fun h _)
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ R → R'
[PROOFSTEP]
classical exact fun x => if IsUnit x then 1 else 0
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ R → R'
[PROOFSTEP]
exact fun x => if IsUnit x then 1 else 0
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ (if IsUnit 1 then 1 else 0) = 1
[PROOFSTEP]
simp only [isUnit_one, if_true]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ ∀ (x y : R),
    OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
        (x * y) =
      OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
          x *
        OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
          y
[PROOFSTEP]
intro x y
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
⊢ OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
      (x * y) =
    OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) } x *
      OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) } y
[PROOFSTEP]
classical
simp only [IsUnit.mul_iff, boole_mul]
split_ifs <;> tauto
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
⊢ OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
      (x * y) =
    OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) } x *
      OneHom.toFun { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) } y
[PROOFSTEP]
simp only [IsUnit.mul_iff, boole_mul]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
⊢ (if IsUnit x ∧ IsUnit y then 1 else 0) = if IsUnit x then if IsUnit y then 1 else 0 else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
h✝² : IsUnit x ∧ IsUnit y
h✝¹ : IsUnit x
h✝ : IsUnit y
⊢ 1 = 1
[PROOFSTEP]
tauto
[GOAL]
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
h✝² : IsUnit x ∧ IsUnit y
h✝¹ : IsUnit x
h✝ : ¬IsUnit y
⊢ 1 = 0
[PROOFSTEP]
tauto
[GOAL]
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
h✝¹ : IsUnit x ∧ IsUnit y
h✝ : ¬IsUnit x
⊢ 1 = 0
[PROOFSTEP]
tauto
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
h✝² : ¬(IsUnit x ∧ IsUnit y)
h✝¹ : IsUnit x
h✝ : IsUnit y
⊢ 0 = 1
[PROOFSTEP]
tauto
[GOAL]
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
h✝² : ¬(IsUnit x ∧ IsUnit y)
h✝¹ : IsUnit x
h✝ : ¬IsUnit y
⊢ 0 = 0
[PROOFSTEP]
tauto
[GOAL]
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
x y : R
h✝¹ : ¬(IsUnit x ∧ IsUnit y)
h✝ : ¬IsUnit x
⊢ 0 = 0
[PROOFSTEP]
tauto
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a : R),
    ¬IsUnit a →
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : R),
                    OneHom.toFun
                        { toFun := fun x => if IsUnit x then 1 else 0,
                          map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := fun x => if IsUnit x then 1 else 0,
                            map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun x => if IsUnit x then 1 else 0,
                            map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
                          y) })
          a =
        0
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
a : R
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : R),
                OneHom.toFun
                    { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => if IsUnit x then 1 else 0, map_one' := (_ : (if IsUnit 1 then 1 else 0) = 1) }
                      y) })
      a =
    0
[PROOFSTEP]
simp only [ha, if_false]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : R), ↑χ a = ↑χ' a
⊢ χ = χ'
[PROOFSTEP]
cases χ
[GOAL]
case mk
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ' : MulChar R R'
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝) a = 0
h : ∀ (a : R), ↑{ toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a = ↑χ' a
⊢ { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } = χ'
[PROOFSTEP]
cases χ'
[GOAL]
case mk.mk
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝¹) a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝) a = 0
h :
  ∀ (a : R),
    ↑{ toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } a =
      ↑{ toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a
⊢ { toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } =
    { toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ }
[PROOFSTEP]
congr
[GOAL]
case mk.mk.e_toMonoidHom
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
toMonoidHom✝¹ : R →* R'
map_nonunit'✝¹ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝¹) a = 0
toMonoidHom✝ : R →* R'
map_nonunit'✝ : ∀ (a : R), ¬IsUnit a → OneHom.toFun (↑toMonoidHom✝) a = 0
h :
  ∀ (a : R),
    ↑{ toMonoidHom := toMonoidHom✝¹, map_nonunit' := map_nonunit'✝¹ } a =
      ↑{ toMonoidHom := toMonoidHom✝, map_nonunit' := map_nonunit'✝ } a
⊢ toMonoidHom✝¹ = toMonoidHom✝
[PROOFSTEP]
exact MonoidHom.ext h
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
⊢ χ = χ'
[PROOFSTEP]
apply ext'
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
⊢ ∀ (a : R), ↑χ a = ↑χ' a
[PROOFSTEP]
intro a
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
⊢ ↑χ a = ↑χ' a
[PROOFSTEP]
by_cases ha : IsUnit a
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
ha : IsUnit a
⊢ ↑χ a = ↑χ' a
[PROOFSTEP]
exact h ha.unit
[GOAL]
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
a : R
ha : ¬IsUnit a
⊢ ↑χ a = ↑χ' a
[PROOFSTEP]
rw [map_nonunit χ ha, map_nonunit χ' ha]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
⊢ χ = χ' → ∀ (a : Rˣ), ↑χ ↑a = ↑χ' ↑a
[PROOFSTEP]
rintro rfl a
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
⊢ ↑χ ↑a = ↑χ ↑a
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ R → R'
[PROOFSTEP]
classical exact fun x => if hx : IsUnit x then f hx.unit else 0
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ R → R'
[PROOFSTEP]
exact fun x => if hx : IsUnit x then f hx.unit else 0
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1
[PROOFSTEP]
have h1 : (isUnit_one.unit : Rˣ) = 1 := Units.eq_iff.mp rfl
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
h1 : IsUnit.unit (_ : IsUnit 1) = 1
⊢ (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1
[PROOFSTEP]
simp only [h1, dif_pos, Units.val_eq_one, map_one, isUnit_one]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ ∀ (x y : R),
    OneHom.toFun
        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
            map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
          x *
        OneHom.toFun
          { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
            map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
          y
[PROOFSTEP]
classical
intro x y
by_cases hx : IsUnit x
· simp only [hx, IsUnit.mul_iff, true_and_iff, dif_pos]
  by_cases hy : IsUnit y
  · simp only [hy, dif_pos]
    have hm : (IsUnit.mul_iff.mpr ⟨hx, hy⟩).unit = hx.unit * hy.unit := Units.eq_iff.mp rfl
    rw [hm, map_mul]
    norm_cast
  · simp only [hy, not_false_iff, dif_neg, mul_zero]
· simp only [hx, IsUnit.mul_iff, false_and_iff, not_false_iff, dif_neg, zero_mul]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ ∀ (x y : R),
    OneHom.toFun
        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
            map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
          x *
        OneHom.toFun
          { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
            map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
          y
[PROOFSTEP]
intro x y
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
⊢ OneHom.toFun
      { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
        map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
        y
[PROOFSTEP]
by_cases hx : IsUnit x
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
⊢ OneHom.toFun
      { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
        map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
        y
[PROOFSTEP]
simp only [hx, IsUnit.mul_iff, true_and_iff, dif_pos]
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
⊢ (if h : IsUnit y then ↑(↑f (IsUnit.unit (_ : IsUnit (x * y)))) else 0) =
    ↑(↑f (IsUnit.unit (_ : IsUnit x))) * if h : IsUnit y then ↑(↑f (IsUnit.unit (_ : IsUnit y))) else 0
[PROOFSTEP]
by_cases hy : IsUnit y
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
hy : IsUnit y
⊢ (if h : IsUnit y then ↑(↑f (IsUnit.unit (_ : IsUnit (x * y)))) else 0) =
    ↑(↑f (IsUnit.unit (_ : IsUnit x))) * if h : IsUnit y then ↑(↑f (IsUnit.unit (_ : IsUnit y))) else 0
[PROOFSTEP]
simp only [hy, dif_pos]
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
hy : IsUnit y
⊢ ↑(↑f (IsUnit.unit (_ : IsUnit (x * y)))) = ↑(↑f (IsUnit.unit (_ : IsUnit x))) * ↑(↑f (IsUnit.unit (_ : IsUnit y)))
[PROOFSTEP]
have hm : (IsUnit.mul_iff.mpr ⟨hx, hy⟩).unit = hx.unit * hy.unit := Units.eq_iff.mp rfl
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
hy : IsUnit y
hm : IsUnit.unit (_ : IsUnit (x * y)) = IsUnit.unit hx * IsUnit.unit hy
⊢ ↑(↑f (IsUnit.unit (_ : IsUnit (x * y)))) = ↑(↑f (IsUnit.unit (_ : IsUnit x))) * ↑(↑f (IsUnit.unit (_ : IsUnit y)))
[PROOFSTEP]
rw [hm, map_mul]
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
hy : IsUnit y
hm : IsUnit.unit (_ : IsUnit (x * y)) = IsUnit.unit hx * IsUnit.unit hy
⊢ ↑(↑f (IsUnit.unit hx) * ↑f (IsUnit.unit hy)) = ↑(↑f (IsUnit.unit (_ : IsUnit x))) * ↑(↑f (IsUnit.unit (_ : IsUnit y)))
[PROOFSTEP]
norm_cast
[GOAL]
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : IsUnit x
hy : ¬IsUnit y
⊢ (if h : IsUnit y then ↑(↑f (IsUnit.unit (_ : IsUnit (x * y)))) else 0) =
    ↑(↑f (IsUnit.unit (_ : IsUnit x))) * if h : IsUnit y then ↑(↑f (IsUnit.unit (_ : IsUnit y))) else 0
[PROOFSTEP]
simp only [hy, not_false_iff, dif_neg, mul_zero]
[GOAL]
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x y : R
hx : ¬IsUnit x
⊢ OneHom.toFun
      { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
        map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
        y
[PROOFSTEP]
simp only [hx, IsUnit.mul_iff, false_and_iff, not_false_iff, dif_neg, zero_mul]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ ∀ (a : R),
    ¬IsUnit a →
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
                  map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : R),
                    OneHom.toFun
                        { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
                          map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
                            map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
                          x *
                        OneHom.toFun
                          { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
                            map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
                          y) })
          a =
        0
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
a : R
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
              map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : R),
                OneHom.toFun
                    { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
                      map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
                        map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
                      x *
                    OneHom.toFun
                      { toFun := fun x => if hx : IsUnit x then ↑(↑f (IsUnit.unit hx)) else 0,
                        map_one' := (_ : (if hx : IsUnit 1 then ↑(↑f (IsUnit.unit hx)) else 0) = 1) }
                      y) })
      a =
    0
[PROOFSTEP]
simp only [ha, not_false_iff, dif_neg]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
a : Rˣ
⊢ ↑(ofUnitHom f) ↑a = ↑(↑f a)
[PROOFSTEP]
simp [ofUnitHom]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ Function.LeftInverse ofUnitHom toUnitHom
[PROOFSTEP]
intro χ
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ ofUnitHom (toUnitHom χ) = χ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ ↑(ofUnitHom (toUnitHom χ)) ↑x = ↑χ ↑x
[PROOFSTEP]
rw [ofUnitHom_coe, coe_toUnitHom]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ Function.RightInverse ofUnitHom toUnitHom
[PROOFSTEP]
intro f
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
⊢ toUnitHom (ofUnitHom f) = f
[PROOFSTEP]
ext x
[GOAL]
case h.a
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
f : Rˣ →* R'ˣ
x : Rˣ
⊢ ↑(↑(toUnitHom (ofUnitHom f)) x) = ↑(↑f x)
[PROOFSTEP]
simp only [coe_toUnitHom, ofUnitHom_coe]
[GOAL]
R✝ : Type u
inst✝³ : CommMonoid R✝
R' : Type v
inst✝² : CommMonoidWithZero R'
R : Type u
inst✝¹ : CommMonoidWithZero R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ ↑χ 0 = 0
[PROOFSTEP]
rw [map_nonunit χ not_isUnit_zero]
[GOAL]
R✝ : Type u
inst✝³ : CommMonoid R✝
R' : Type v
inst✝² : CommMonoidWithZero R'
R : Type u
inst✝¹ : CommRing R
inst✝ : Nontrivial R
χ : MulChar R R'
⊢ ↑χ ↑(ringChar R) = 0
[PROOFSTEP]
rw [ringChar.Nat.cast_ringChar, χ.map_zero]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
a : Rˣ
⊢ ↑1 ↑a = 1
[PROOFSTEP]
classical exact dif_pos a.isUnit
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
a : Rˣ
⊢ ↑1 ↑a = 1
[PROOFSTEP]
exact dif_pos a.isUnit
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
src✝ : R →* R' := χ.toMonoidHom * χ'.toMonoidHom
a : R
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := ↑χ * ↑χ', map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1) },
          map_mul' :=
            (_ : ∀ (x y : R), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
      a =
    0
[PROOFSTEP]
simp only [map_nonunit χ ha, zero_mul, Pi.mul_apply]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ 1 * χ = χ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a✝ : Rˣ
⊢ ↑(1 * χ) ↑a✝ = ↑χ ↑a✝
[PROOFSTEP]
simp only [one_mul, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ * 1 = χ
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a✝ : Rˣ
⊢ ↑(χ * 1) ↑a✝ = ↑χ ↑a✝
[PROOFSTEP]
simp only [mul_one, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
src✝ : R →* R' := MonoidHom.comp (↑MonoidWithZero.inverse) χ.toMonoidHom
a : R
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := fun a => ↑MonoidWithZero.inverse (↑χ a), map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1) },
          map_mul' :=
            (_ : ∀ (x y : R), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
      a =
    0
[PROOFSTEP]
simp [map_nonunit _ ha]
[GOAL]
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
[PROOFSTEP]
by_cases ha : IsUnit a
[GOAL]
case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
[PROOFSTEP]
rw [inv_apply_eq_inv]
[GOAL]
case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
⊢ Ring.inverse (↑χ a) = ↑χ (Ring.inverse a)
[PROOFSTEP]
have h := IsUnit.map χ ha
[GOAL]
case pos
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ Ring.inverse (↑χ a) = ↑χ (Ring.inverse a)
[PROOFSTEP]
apply IsUnit.mul_right_injective h
[GOAL]
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ (fun x x_1 => x * x_1) (↑χ a) (Ring.inverse (↑χ a)) = (fun x x_1 => x * x_1) (↑χ a) (↑χ (Ring.inverse a))
[PROOFSTEP]
dsimp only
  -- Porting note: was
      -- rw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha, MulChar.map_one]
[GOAL]
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ ↑χ a * Ring.inverse (↑χ a) = ↑χ a * ↑χ (Ring.inverse a)
[PROOFSTEP]
erw [Ring.mul_inverse_cancel _ h, ← map_mul, Ring.mul_inverse_cancel _ ha]
[GOAL]
case pos.a
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : IsUnit a
h : IsUnit (↑χ a)
⊢ 1 = ↑χ 1
[PROOFSTEP]
exact (MulChar.map_one χ).symm
[GOAL]
case neg
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
ha : ¬IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
[PROOFSTEP]
revert ha
[GOAL]
case neg
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
⊢ ¬IsUnit a → ↑χ⁻¹ a = ↑χ (Ring.inverse a)
[PROOFSTEP]
nontriviality R
[GOAL]
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
✝ : Nontrivial R
⊢ ¬IsUnit a → ↑χ⁻¹ a = ↑χ (Ring.inverse a)
[PROOFSTEP]
intro ha
[GOAL]
R✝ : Type u
inst✝² : CommMonoid R✝
R' : Type v
inst✝¹ : CommMonoidWithZero R'
R : Type u
inst✝ : CommMonoidWithZero R
χ : MulChar R R'
a : R
✝ : Nontrivial R
ha : ¬IsUnit a
⊢ ↑χ⁻¹ a = ↑χ (Ring.inverse a)
[PROOFSTEP]
rw [map_nonunit _ ha, Ring.inverse_non_unit a ha, MulChar.map_zero χ]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ⁻¹ * χ = 1
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ ↑(χ⁻¹ * χ) ↑x = ↑1 ↑x
[PROOFSTEP]
rw [coeToFun_mul, Pi.mul_apply, inv_apply_eq_inv]
  -- Porting note: was
    -- simp only [Ring.inverse_mul_cancel _ (IsUnit.map _ x.isUnit)]
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ Ring.inverse (↑χ ↑x) * ↑χ ↑x = ↑1 ↑x
[PROOFSTEP]
erw [Ring.inverse_mul_cancel _ (IsUnit.map χ x.isUnit)]
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
x : Rˣ
⊢ 1 = ↑1 ↑x
[PROOFSTEP]
rw [one_apply_coe]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a b c : MulChar R R'), a * b * c = a * (b * c)
[PROOFSTEP]
intro χ₁ χ₂ χ₃
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ χ₃ : MulChar R R'
⊢ χ₁ * χ₂ * χ₃ = χ₁ * (χ₂ * χ₃)
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ χ₃ : MulChar R R'
a : Rˣ
⊢ ↑(χ₁ * χ₂ * χ₃) ↑a = ↑(χ₁ * (χ₂ * χ₃)) ↑a
[PROOFSTEP]
simp only [mul_assoc, Pi.mul_apply, MulChar.coeToFun_mul]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
⊢ ∀ (a b : MulChar R R'), a * b = b * a
[PROOFSTEP]
intro χ₁ χ₂
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
⊢ χ₁ * χ₂ = χ₂ * χ₁
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ₁ χ₂ : MulChar R R'
a : Rˣ
⊢ ↑(χ₁ * χ₂) ↑a = ↑(χ₂ * χ₁) ↑a
[PROOFSTEP]
simp only [mul_comm, Pi.mul_apply, MulChar.coeToFun_mul]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
a : Rˣ
⊢ ↑(χ ^ n) ↑a = ↑χ ↑a ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
⊢ ↑(χ ^ Nat.zero) ↑a = ↑χ ↑a ^ Nat.zero
[PROOFSTEP]
rw [pow_zero, pow_zero, one_apply_coe]
[GOAL]
case succ
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : ↑(χ ^ n) ↑a = ↑χ ↑a ^ n
⊢ ↑(χ ^ Nat.succ n) ↑a = ↑χ ↑a ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, pow_succ, mul_apply, ih]
[GOAL]
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : 0 < n
a : R
⊢ ↑(χ ^ n) a = ↑χ a ^ n
[PROOFSTEP]
by_cases ha : IsUnit a
[GOAL]
case pos
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : 0 < n
a : R
ha : IsUnit a
⊢ ↑(χ ^ n) a = ↑χ a ^ n
[PROOFSTEP]
exact pow_apply_coe χ n ha.unit
[GOAL]
case neg
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : 0 < n
a : R
ha : ¬IsUnit a
⊢ ↑(χ ^ n) a = ↑χ a ^ n
[PROOFSTEP]
rw [map_nonunit (χ ^ n) ha, map_nonunit χ ha, zero_pow hn]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
⊢ IsNontrivial χ ↔ χ ≠ 1
[PROOFSTEP]
simp only [IsNontrivial, Ne.def, ext_iff, not_forall, one_apply_coe]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
src✝ : R →* R'' := MonoidHom.comp (↑f) χ.toMonoidHom
a : R
ha : ¬IsUnit a
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := fun a => ↑f (↑χ a), map_one' := (_ : OneHom.toFun (↑src✝) 1 = 1) },
          map_mul' :=
            (_ : ∀ (x y : R), OneHom.toFun (↑src✝) (x * y) = OneHom.toFun (↑src✝) x * OneHom.toFun (↑src✝) y) })
      a =
    0
[PROOFSTEP]
simp only [map_nonunit χ ha, map_zero]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsNontrivial χ
f : R' →+* R''
hf : Function.Injective ↑f
⊢ IsNontrivial (ringHomComp χ f)
[PROOFSTEP]
obtain ⟨a, ha⟩ := hχ
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ IsNontrivial (ringHomComp χ f)
[PROOFSTEP]
use a
[GOAL]
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ ↑(ringHomComp χ f) ↑a ≠ 1
[PROOFSTEP]
simp_rw [ringHomComp_apply, ← RingHom.map_one f]
[GOAL]
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
f : R' →+* R''
hf : Function.Injective ↑f
a : Rˣ
ha : ↑χ ↑a ≠ 1
⊢ ↑f (↑χ ↑a) ≠ ↑f 1
[PROOFSTEP]
exact fun h => ha (hf h)
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
f : R' →+* R''
⊢ IsQuadratic (ringHomComp χ f)
[PROOFSTEP]
intro a
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
f : R' →+* R''
a : R
⊢ ↑(ringHomComp χ f) a = 0 ∨ ↑(ringHomComp χ f) a = 1 ∨ ↑(ringHomComp χ f) a = -1
[PROOFSTEP]
rcases hχ a with (ha | ha | ha)
[GOAL]
case inl
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
f : R' →+* R''
a : R
ha : ↑χ a = 0
⊢ ↑(ringHomComp χ f) a = 0 ∨ ↑(ringHomComp χ f) a = 1 ∨ ↑(ringHomComp χ f) a = -1
[PROOFSTEP]
simp [ha]
[GOAL]
case inr.inl
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
f : R' →+* R''
a : R
ha : ↑χ a = 1
⊢ ↑(ringHomComp χ f) a = 0 ∨ ↑(ringHomComp χ f) a = 1 ∨ ↑(ringHomComp χ f) a = -1
[PROOFSTEP]
simp [ha]
[GOAL]
case inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
f : R' →+* R''
a : R
ha : ↑χ a = -1
⊢ ↑(ringHomComp χ f) a = 0 ∨ ↑(ringHomComp χ f) a = 1 ∨ ↑(ringHomComp χ f) a = -1
[PROOFSTEP]
simp [ha]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
⊢ χ⁻¹ = χ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
⊢ ↑χ⁻¹ ↑x = ↑χ ↑x
[PROOFSTEP]
rw [inv_apply_eq_inv]
[GOAL]
case h
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
[PROOFSTEP]
rcases hχ x with (h₀ | h₁ | h₂)
[GOAL]
case h.inl
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₀ : ↑χ ↑x = 0
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
[PROOFSTEP]
rw [h₀, Ring.inverse_zero]
[GOAL]
case h.inr.inl
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₁ : ↑χ ↑x = 1
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
[PROOFSTEP]
rw [h₁, Ring.inverse_one]
[GOAL]
case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
[PROOFSTEP]
have : (-1 : R') = (-1 : R'ˣ) := by rw [Units.val_neg, Units.val_one]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
⊢ -1 = ↑(-1)
[PROOFSTEP]
rw [Units.val_neg, Units.val_one]
[GOAL]
case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
this : -1 = ↑(-1)
⊢ Ring.inverse (↑χ ↑x) = ↑χ ↑x
[PROOFSTEP]
rw [h₂, this, Ring.inverse_unit (-1 : R'ˣ)]
[GOAL]
case h.inr.inr
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
x : Rˣ
h₂ : ↑χ ↑x = -1
this : -1 = ↑(-1)
⊢ ↑(-1)⁻¹ = ↑(-1)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
⊢ χ ^ 2 = 1
[PROOFSTEP]
rw [← mul_left_inv χ, pow_two, hχ.inv]
[GOAL]
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
⊢ χ ^ p = χ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
⊢ ↑(χ ^ p) ↑x = ↑χ ↑x
[PROOFSTEP]
rw [pow_apply_coe]
[GOAL]
case h
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
⊢ ↑χ ↑x ^ p = ↑χ ↑x
[PROOFSTEP]
rcases hχ x with (hx | hx | hx)
[GOAL]
case h.inl
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : ↑χ ↑x = 0
⊢ ↑χ ↑x ^ p = ↑χ ↑x
[PROOFSTEP]
rw [hx]
[GOAL]
case h.inr.inl
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : ↑χ ↑x = 1
⊢ ↑χ ↑x ^ p = ↑χ ↑x
[PROOFSTEP]
rw [hx]
[GOAL]
case h.inr.inr
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : ↑χ ↑x = -1
⊢ ↑χ ↑x ^ p = ↑χ ↑x
[PROOFSTEP]
rw [hx]
[GOAL]
case h.inl
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : ↑χ ↑x = 0
⊢ 0 ^ p = 0
[PROOFSTEP]
rw [zero_pow (@Fact.out p.Prime).pos]
[GOAL]
case h.inr.inl
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : ↑χ ↑x = 1
⊢ 1 ^ p = 1
[PROOFSTEP]
rw [one_pow]
[GOAL]
case h.inr.inr
R : Type u
inst✝³ : CommRing R
R' : Type v
inst✝² : CommRing R'
R'' : Type w
inst✝¹ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R' p
x : Rˣ
hx : ↑χ ↑x = -1
⊢ (-1) ^ p = -1
[PROOFSTEP]
exact CharP.neg_one_pow_char R' p
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
n : ℕ
hn : Even n
⊢ χ ^ n = 1
[PROOFSTEP]
obtain ⟨n, rfl⟩ := even_iff_two_dvd.mp hn
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
n : ℕ
hn : Even (2 * n)
⊢ χ ^ (2 * n) = 1
[PROOFSTEP]
rw [pow_mul, hχ.sq_eq_one, one_pow]
[GOAL]
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
n : ℕ
hn : Odd n
⊢ χ ^ n = χ
[PROOFSTEP]
obtain ⟨n, rfl⟩ := hn
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
R' : Type v
inst✝¹ : CommRing R'
R'' : Type w
inst✝ : CommRing R''
χ : MulChar R R'
hχ : IsQuadratic χ
n : ℕ
⊢ χ ^ (2 * n + 1) = χ
[PROOFSTEP]
rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]
[GOAL]
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
hχ : IsNontrivial χ
⊢ ∑ a : R, ↑χ a = 0
[PROOFSTEP]
rcases hχ with ⟨b, hb⟩
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ∑ a : R, ↑χ a = 0
[PROOFSTEP]
refine'
  eq_zero_of_mul_eq_self_left hb
    _
      -- POrting note: `map_mul` isn't applied
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ↑χ ↑b * ∑ a : R, ↑χ a = ∑ a : R, ↑χ a
[PROOFSTEP]
simp only [Finset.mul_sum, ← map_mul]
[GOAL]
case intro
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : IsDomain R'
χ : MulChar R R'
b : Rˣ
hb : ↑χ ↑b ≠ 1
⊢ ∑ x : R, ↑χ (↑b * x) = ∑ x : R, ↑χ x
[PROOFSTEP]
refine Fintype.sum_bijective _ (Units.mulLeft_bijective b) _ _ fun x => rfl
[GOAL]
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
⊢ ∑ a : R, ↑1 a = ↑(Fintype.card Rˣ)
[PROOFSTEP]
calc
  (∑ a, (1 : MulChar R R') a) = ∑ a : R, if IsUnit a then 1 else 0 := Finset.sum_congr rfl fun a _ => ?_
  _ = ((Finset.univ : Finset R).filter IsUnit).card := Finset.sum_boole
  _ = (Finset.univ.map ⟨((↑) : Rˣ → R), Units.ext⟩).card := ?_
  _ = Fintype.card Rˣ := congr_arg _ (Finset.card_map _)
[GOAL]
case calc_1
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
⊢ ↑1 a = if IsUnit a then 1 else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : IsUnit a
⊢ ↑1 a = 1
[PROOFSTEP]
exact one_apply_coe h.unit
[GOAL]
case neg
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ ↑1 a = 0
[PROOFSTEP]
exact map_nonunit _ h
[GOAL]
case calc_2
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
⊢ ↑(Finset.card (Finset.filter IsUnit Finset.univ)) =
    ↑(Finset.card (Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ))
[PROOFSTEP]
congr
[GOAL]
case calc_2.e_a.e_s
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
⊢ Finset.filter IsUnit Finset.univ =
    Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ
[PROOFSTEP]
ext a
[GOAL]
case calc_2.e_a.e_s.a
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
⊢ a ∈ Finset.filter IsUnit Finset.univ ↔
    a ∈ Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ
[PROOFSTEP]
simp only [Finset.mem_filter, Finset.mem_univ, true_and_iff, Finset.mem_map, Function.Embedding.coeFn_mk,
  exists_true_left, IsUnit]


[GOAL]
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
f g : SlashInvariantForm Γ k
h : f.toFun = g.toFun
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
g : SlashInvariantForm Γ k
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ (γ : { x // x ∈ Γ }), toFun✝ ∣[k] γ = toFun✝
h : { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
toFun✝¹ : ℍ → ℂ
slash_action_eq'✝¹ : ∀ (γ : { x // x ∈ Γ }), toFun✝¹ ∣[k] γ = toFun✝¹
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ (γ : { x // x ∈ Γ }), toFun✝ ∣[k] γ = toFun✝
h :
  { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ }.toFun =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ } =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
Γ✝ : outParam (Subgroup SL(2, ℤ))
k✝ : outParam ℤ
k : ℤ
Γ : Subgroup SL(2, ℤ)
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : { x // x ∈ Γ }
z : ℍ
⊢ ↑f (γ • z) = (↑(↑↑↑γ 1 0) * ↑z + ↑(↑↑↑γ 1 1)) ^ k * ↑f z
[PROOFSTEP]
rw [← ModularForm.slash_action_eq'_iff, slash_action_eqn]
[GOAL]
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
f g : SlashInvariantForm Γ k
γ : { x // x ∈ Γ }
⊢ (↑f + ↑g) ∣[k] γ = ↑f + ↑g
[PROOFSTEP]
rw [SlashAction.add_slash, slash_action_eqn, slash_action_eqn]
[GOAL]
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : { x // x ∈ Γ }
⊢ (c • ↑f) ∣[k] γ = c • ↑f
[PROOFSTEP]
rw [SlashAction.smul_slash_of_tower, slash_action_eqn]
[GOAL]
F : Type u_1
Γ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
f : SlashInvariantForm Γ k
γ : { x // x ∈ Γ }
⊢ (-↑f) ∣[k] γ = -↑f
[PROOFSTEP]
rw [SlashAction.neg_slash, slash_action_eqn]
[GOAL]
F : Type u_1
Γ✝ : outParam (Subgroup SL(2, ℤ))
k : outParam ℤ
k₁ k₂ : ℤ
Γ : Subgroup SL(2, ℤ)
f : SlashInvariantForm Γ k₁
g : SlashInvariantForm Γ k₂
A : { x // x ∈ Γ }
⊢ (↑f * ↑g) ∣[k₁ + k₂] A = ↑f * ↑g
[PROOFSTEP]
simp_rw [ModularForm.mul_slash_subgroup, SlashInvariantFormClass.slash_action_eq]


[GOAL]
⊢ {x | ∃ p, p > 2 ∧ LiouvilleWith p x} ⊆
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
rintro x ⟨p, hp, hxp⟩
[GOAL]
case intro.intro
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
⊢ x ∈
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
rcases exists_nat_one_div_lt (sub_pos.2 hp) with ⟨n, hn⟩
[GOAL]
case intro.intro.intro
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 1 / (↑n + 1) < p - 2
⊢ x ∈
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
rw [lt_sub_iff_add_lt'] at hn
[GOAL]
case intro.intro.intro
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ x ∈
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
suffices
  ∀ y : ℝ,
    LiouvilleWith p y →
      y ∈ Ico (0 : ℝ) 1 →
        ∃ᶠ b : ℕ in atTop, ∃ a ∈ Finset.Icc (0 : ℤ) b, |y - a / b| < 1 / (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ)
  by
  simp only [mem_iUnion, mem_preimage]
  have hx : x + ↑(-⌊x⌋) ∈ Ico (0 : ℝ) 1 := by
    simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff, mem_Ico,
      Int.cast_neg, le_add_neg_iff_add_le]
  refine' ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩
[GOAL]
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ x ∈
    ⋃ (m : ℤ),
      (fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}
[PROOFSTEP]
simp only [mem_iUnion, mem_preimage]
[GOAL]
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ ∃ i i_1 i_2, x + ↑i ∈ {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑i_1)}
[PROOFSTEP]
have hx : x + ↑(-⌊x⌋) ∈ Ico (0 : ℝ) 1 := by
  simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff, mem_Ico, Int.cast_neg,
    le_add_neg_iff_add_le]
[GOAL]
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
⊢ x + ↑(-⌊x⌋) ∈ Ico 0 1
[PROOFSTEP]
simp only [Int.floor_le, Int.lt_floor_add_one, add_neg_lt_iff_le_add', zero_add, and_self_iff, mem_Ico, Int.cast_neg,
  le_add_neg_iff_add_le]
[GOAL]
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
this :
  ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
hx : x + ↑(-⌊x⌋) ∈ Ico 0 1
⊢ ∃ i i_1 i_2, x + ↑i ∈ {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑i_1)}
[PROOFSTEP]
refine' ⟨-⌊x⌋, n + 1, n.succ_pos, this _ (hxp.add_int _) hx⟩
[GOAL]
case intro.intro.intro
x p : ℝ
hp : p > 2
hxp : LiouvilleWith p x
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
clear hxp x
[GOAL]
case intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
⊢ ∀ (y : ℝ),
    LiouvilleWith p y →
      y ∈ Ico 0 1 → ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |y - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
intro x hxp hx01
[GOAL]
case intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
⊢ ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
refine' ((hxp.frequently_lt_rpow_neg hn).and_eventually (eventually_ge_atTop 1)).mono _
[GOAL]
case intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
⊢ ∀ (x_1 : ℕ),
    (∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < ↑x_1 ^ (-(2 + 1 / (↑n + 1)))) ∧ 1 ≤ x_1 →
      ∃ a, a ∈ Finset.Icc 0 ↑x_1 ∧ |x - ↑a / ↑x_1| < 1 / ↑x_1 ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
rintro b ⟨⟨a, -, hlt⟩, hb⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < ↑b ^ (-(2 + 1 / (↑n + 1)))
⊢ ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
rw [rpow_neg b.cast_nonneg, ← one_div, ← Nat.cast_succ] at hlt
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
⊢ ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(n + 1))
[PROOFSTEP]
refine' ⟨a, _, hlt⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
replace hb : (1 : ℝ) ≤ b
[GOAL]
case hb
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
hb : 1 ≤ b
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
⊢ 1 ≤ ↑b
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
exact Nat.one_le_cast.2 hb
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
have hb0 : (0 : ℝ) < b := zero_lt_one.trans_le hb
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
replace hlt : |x - a / b| < 1 / b
[GOAL]
case hlt
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ |x - ↑a / ↑b| < 1 / ↑b
[PROOFSTEP]
refine' hlt.trans_le (one_div_le_one_div_of_le hb0 _)
[GOAL]
case hlt
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ ↑b ≤ ↑b ^ (2 + 1 / ↑(Nat.succ n))
[PROOFSTEP]
calc
  (b : ℝ) = (b : ℝ) ^ (1 : ℝ) := (rpow_one _).symm
  _ ≤ (b : ℝ) ^ (2 + 1 / (n + 1 : ℕ) : ℝ) := rpow_le_rpow_of_exponent_le hb (one_le_two.trans ?_)
[GOAL]
case hlt
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hlt : |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑(Nat.succ n))
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
⊢ 2 ≤ 2 + 1 / ↑(n + 1)
[PROOFSTEP]
simpa using n.cast_add_one_pos.le
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : |x - ↑a / ↑b| < 1 / ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
rw [sub_div' _ _ _ hb0.ne', abs_div, abs_of_pos hb0, div_lt_div_right hb0, abs_sub_lt_iff, sub_lt_iff_lt_add,
  sub_lt_iff_lt_add, ← sub_lt_iff_lt_add'] at hlt
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ a ∈ Finset.Icc 0 ↑b
[PROOFSTEP]
rw [Finset.mem_Icc, ← Int.lt_add_one_iff, ← Int.lt_add_one_iff, ← neg_lt_iff_pos_add, add_comm, ← @Int.cast_lt ℝ, ←
  @Int.cast_lt ℝ]
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ ↑(-1) < ↑a ∧ ↑a < ↑(1 + ↑b)
[PROOFSTEP]
push_cast
[GOAL]
case intro.intro.intro.intro.intro.intro
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ -1 < ↑a ∧ ↑a < 1 + ↑b
[PROOFSTEP]
refine' ⟨lt_of_le_of_lt _ hlt.1, hlt.2.trans_le _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ -1 ≤ x * ↑b - 1
[PROOFSTEP]
simp only [mul_nonneg hx01.left b.cast_nonneg, neg_le_sub_iff_le_add, le_add_iff_nonneg_left]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ 1 + x * ↑b ≤ 1 + ↑b
[PROOFSTEP]
rw [add_le_add_iff_left]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : x * ↑b - 1 < ↑a ∧ ↑a < 1 + x * ↑b
⊢ x * ↑b ≤ ↑b
[PROOFSTEP]
exact mul_le_of_le_one_left hb0.le hx01.2.le
[GOAL]
⊢ ↑↑volume (⋃ (p : ℝ) (_ : 2 < p), {x | LiouvilleWith p x}) = 0
[PROOFSTEP]
simp only [← setOf_exists, exists_prop]
[GOAL]
⊢ ↑↑volume {x | ∃ i, 2 < i ∧ LiouvilleWith i x} = 0
[PROOFSTEP]
refine' measure_mono_null setOf_liouvilleWith_subset_aux _
[GOAL]
⊢ ↑↑volume
      (⋃ (m : ℤ),
        (fun x => x + ↑m) ⁻¹'
          ⋃ (n : ℕ) (_ : n > 0),
            {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
[PROOFSTEP]
rw [measure_iUnion_null_iff]
[GOAL]
⊢ ∀ (i : ℤ),
    ↑↑volume
        ((fun x => x + ↑i) ⁻¹'
          ⋃ (n : ℕ) (_ : n > 0),
            {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
      0
[PROOFSTEP]
intro m
[GOAL]
m : ℤ
⊢ ↑↑volume
      ((fun x => x + ↑m) ⁻¹'
        ⋃ (n : ℕ) (_ : n > 0),
          {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
[PROOFSTEP]
rw [measure_preimage_add_right]
[GOAL]
m : ℤ
⊢ ↑↑volume
      (⋃ (n : ℕ) (_ : n > 0),
        {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
[PROOFSTEP]
clear m
[GOAL]
⊢ ↑↑volume
      (⋃ (n : ℕ) (_ : n > 0),
        {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
[PROOFSTEP]
refine' (measure_biUnion_null_iff <| to_countable _).2 fun n (hn : 1 ≤ n) => _
[GOAL]
n : ℕ
hn : 1 ≤ n
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)} = 0
[PROOFSTEP]
generalize hr : (2 + 1 / n : ℝ) = r
[GOAL]
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
[PROOFSTEP]
replace hr : 2 < r
[GOAL]
case hr
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 + 1 / ↑n = r
⊢ 2 < r
[PROOFSTEP]
simp [← hr, zero_lt_one.trans_le hn]
[GOAL]
n : ℕ
hn : 1 ≤ n
r : ℝ
hr : 2 < r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
[PROOFSTEP]
clear hn n
[GOAL]
r : ℝ
hr : 2 < r
⊢ ↑↑volume {x | ∃ᶠ (b : ℕ) in atTop, ∃ a, a ∈ Finset.Icc 0 ↑b ∧ |x - ↑a / ↑b| < 1 / ↑b ^ r} = 0
[PROOFSTEP]
refine' measure_setOf_frequently_eq_zero _
[GOAL]
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), ↑↑volume {x | ∃ a, a ∈ Finset.Icc 0 ↑i ∧ |x - ↑a / ↑i| < 1 / ↑i ^ r} ≠ ⊤
[PROOFSTEP]
simp only [setOf_exists, ← exists_prop, ← Real.dist_eq, ← mem_ball, setOf_mem_eq]
[GOAL]
r : ℝ
hr : 2 < r
⊢ ∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
[PROOFSTEP]
set B : ℤ → ℕ → Set ℝ := fun a b => ball (a / b) (1 / (b : ℝ) ^ r)
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
⊢ ∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
[PROOFSTEP]
have hB : ∀ a b, volume (B a b) = ↑((2 : ℝ≥0) / (b : ℝ≥0) ^ r) := fun a b ↦ by
  rw [Real.volume_ball, mul_one_div, ← NNReal.coe_two, ← NNReal.coe_nat_cast, ← NNReal.coe_rpow, ← NNReal.coe_div,
    ENNReal.ofReal_coe_nnreal]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
a : ℤ
b : ℕ
⊢ ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
[PROOFSTEP]
rw [Real.volume_ball, mul_one_div, ← NNReal.coe_two, ← NNReal.coe_nat_cast, ← NNReal.coe_rpow, ← NNReal.coe_div,
  ENNReal.ofReal_coe_nnreal]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
⊢ ∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
[PROOFSTEP]
have : ∀ b : ℕ, volume (⋃ a ∈ Finset.Icc (0 : ℤ) b, B a b) ≤ ↑(2 * ((b : ℝ≥0) ^ (1 - r) + (b : ℝ≥0) ^ (-r))) := fun b ↦
  calc
    volume (⋃ a ∈ Finset.Icc (0 : ℤ) b, B a b) ≤ ∑ a in Finset.Icc (0 : ℤ) b, volume (B a b) :=
      measure_biUnion_finset_le _ _
    _ = ↑((b + 1) * (2 / (b : ℝ≥0) ^ r)) := by
      simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero, ← Int.ofNat_succ, Int.toNat_coe_nat, ←
        Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_nat]
    _ = _ := by
      have : 1 - r ≠ 0 := by linarith
      rw [ENNReal.coe_eq_coe]
      simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' _ this, mul_add, mul_left_comm]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ ∑ a in Finset.Icc 0 ↑b, ↑↑volume (B a b) = ↑((↑b + 1) * (2 / ↑b ^ r))
[PROOFSTEP]
simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero, ← Int.ofNat_succ, Int.toNat_coe_nat, ←
  Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_nat]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ ↑((↑b + 1) * (2 / ↑b ^ r)) = ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
[PROOFSTEP]
have : 1 - r ≠ 0 := by linarith
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
⊢ 1 - r ≠ 0
[PROOFSTEP]
linarith
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
this : 1 - r ≠ 0
⊢ ↑((↑b + 1) * (2 / ↑b ^ r)) = ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
[PROOFSTEP]
rw [ENNReal.coe_eq_coe]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
b : ℕ
this : 1 - r ≠ 0
⊢ (↑b + 1) * (2 / ↑b ^ r) = 2 * (↑b ^ (1 - r) + ↑b ^ (-r))
[PROOFSTEP]
simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' _ this, mul_add, mul_left_comm]
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ ∑' (i : ℕ), ↑↑volume (⋃ (i_1 : ℤ) (_ : i_1 ∈ Finset.Icc 0 ↑i), ball (↑i_1 / ↑i) (1 / ↑i ^ r)) ≠ ⊤
[PROOFSTEP]
refine' ne_top_of_le_ne_top (ENNReal.tsum_coe_ne_top_iff_summable.2 _) (ENNReal.tsum_le_tsum this)
[GOAL]
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a => 2 * (↑a ^ (1 - r) + ↑a ^ (-r))
[PROOFSTEP]
refine' (Summable.add _ _).mul_left _
[GOAL]
case refine'_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a => ↑a ^ (1 - r)
[PROOFSTEP]
simp only [NNReal.summable_rpow]
[GOAL]
case refine'_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ Summable fun a => ↑a ^ (-r)
[PROOFSTEP]
simp only [NNReal.summable_rpow]
[GOAL]
case refine'_1
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ 1 - r < -1
[PROOFSTEP]
linarith
[GOAL]
case refine'_2
r : ℝ
hr : 2 < r
B : ℤ → ℕ → Set ℝ := fun a b => ball (↑a / ↑b) (1 / ↑b ^ r)
hB : ∀ (a : ℤ) (b : ℕ), ↑↑volume (B a b) = ↑(2 / ↑b ^ r)
this : ∀ (b : ℕ), ↑↑volume (⋃ (a : ℤ) (_ : a ∈ Finset.Icc 0 ↑b), B a b) ≤ ↑(2 * (↑b ^ (1 - r) + ↑b ^ (-r)))
⊢ -r < -1
[PROOFSTEP]
linarith
[GOAL]
⊢ ∀ᵐ (x : ℝ), ∀ (p : ℝ), p > 2 → ¬LiouvilleWith p x
[PROOFSTEP]
simpa only [ae_iff, not_forall, Classical.not_not, setOf_exists] using volume_iUnion_setOf_liouvilleWith
[GOAL]
x : ℝ
h₁ : ∀ (p : ℝ), p > 2 → ¬LiouvilleWith p x
h₂ : Liouville x
⊢ 3 > 2
[PROOFSTEP]
norm_num
[GOAL]
⊢ ↑↑volume {x | Liouville x} = 0
[PROOFSTEP]
simpa only [ae_iff, Classical.not_not] using ae_not_liouville


[GOAL]
⊢ IsPrincipalIdealRing { x // x ∈ 𝓞 ℚ }
[PROOFSTEP]
convert
  IsPrincipalIdealRing.of_surjective (Rat.ringOfIntegersEquiv.symm : ℤ →+* ringOfIntegers ℚ)
    Rat.ringOfIntegersEquiv.symm.surjective


[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
⊢ ‖cexp (↑π * I * ↑n ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
let y := rexp (-π * z.im)
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
⊢ ‖cexp (↑π * I * ↑n ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hz)
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ ‖cexp (↑π * I * ↑n ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
refine' (le_of_eq _).trans (_ : y ^ n ^ 2 ≤ _)
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ ‖cexp (↑π * I * ↑n ^ 2 * z)‖ = y ^ n ^ 2
[PROOFSTEP]
rw [Complex.norm_eq_abs, Complex.abs_exp]
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ rexp (↑π * I * ↑n ^ 2 * z).re = y ^ n ^ 2
[PROOFSTEP]
have : (↑π * I * (n : ℂ) ^ 2 * z).re = -π * z.im * (n : ℝ) ^ 2 :=
  by
  rw [(by push_cast ; ring : ↑π * I * (n : ℂ) ^ 2 * z = ↑(π * (n : ℝ) ^ 2) * (z * I)), ofReal_mul_re, mul_I_re]
  ring
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ (↑π * I * ↑n ^ 2 * z).re = -π * z.im * ↑n ^ 2
[PROOFSTEP]
rw [(by push_cast ; ring : ↑π * I * (n : ℂ) ^ 2 * z = ↑(π * (n : ℝ) ^ 2) * (z * I)), ofReal_mul_re, mul_I_re]
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ ↑π * I * ↑n ^ 2 * z = ↑(π * ↑n ^ 2) * (z * I)
[PROOFSTEP]
push_cast
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ ↑π * I * ↑n ^ 2 * z = ↑π * ↑n ^ 2 * (z * I)
[PROOFSTEP]
ring
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ π * ↑n ^ 2 * -z.im = -π * z.im * ↑n ^ 2
[PROOFSTEP]
ring
[GOAL]
case refine'_1
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * z).re = -π * z.im * ↑n ^ 2
⊢ rexp (↑π * I * ↑n ^ 2 * z).re = y ^ n ^ 2
[PROOFSTEP]
obtain ⟨m, hm⟩ := Int.eq_ofNat_of_zero_le (sq_nonneg n)
[GOAL]
case refine'_1.intro
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
this : (↑π * I * ↑n ^ 2 * z).re = -π * z.im * ↑n ^ 2
m : ℕ
hm : n ^ 2 = ↑m
⊢ rexp (↑π * I * ↑n ^ 2 * z).re = y ^ n ^ 2
[PROOFSTEP]
rw [this, exp_mul, ← Int.cast_pow, rpow_int_cast, hm, zpow_ofNat]
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ y ^ n ^ 2 ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
have : n ^ 2 = ↑(n.natAbs ^ 2) := by rw [Nat.cast_pow, Int.natAbs_sq]
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
⊢ n ^ 2 = ↑(Int.natAbs n ^ 2)
[PROOFSTEP]
rw [Nat.cast_pow, Int.natAbs_sq]
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
this : n ^ 2 = ↑(Int.natAbs n ^ 2)
⊢ y ^ n ^ 2 ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
rw [this, zpow_ofNat]
[GOAL]
case refine'_2
z : ℂ
hz : 0 < z.im
n : ℤ
y : ℝ := rexp (-π * z.im)
h : y < 1
this : n ^ 2 = ↑(Int.natAbs n ^ 2)
⊢ y ^ Int.natAbs n ^ 2 ≤ rexp (-π * z.im) ^ Int.natAbs n
[PROOFSTEP]
exact pow_le_pow_of_le_one (exp_pos _).le h.le ((sq n.natAbs).symm ▸ n.natAbs.le_mul_self)
[GOAL]
R : ℝ
hR : 0 < R
⊢ ∃ bd, Summable bd ∧ ∀ {τ : ℂ}, R ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ bd n
[PROOFSTEP]
let y := rexp (-π * R)
[GOAL]
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
⊢ ∃ bd, Summable bd ∧ ∀ {τ : ℂ}, R ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ bd n
[PROOFSTEP]
have h : y < 1 := exp_lt_one_iff.mpr (mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hR)
[GOAL]
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ ∃ bd, Summable bd ∧ ∀ {τ : ℂ}, R ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ bd n
[PROOFSTEP]
refine' ⟨fun n => y ^ n.natAbs, summable_int_of_summable_nat _ _, fun hτ n => _⟩
[GOAL]
case refine'_1
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs ↑n
case refine'_2
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs (-↑n)
case refine'_3
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
τ✝ : ℂ
hτ : R ≤ τ✝.im
n : ℤ
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ✝)‖ ≤ (fun n => y ^ Int.natAbs n) n
[PROOFSTEP]
pick_goal 3
[GOAL]
case refine'_3
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
τ✝ : ℂ
hτ : R ≤ τ✝.im
n : ℤ
⊢ ‖cexp (↑π * I * ↑n ^ 2 * τ✝)‖ ≤ (fun n => y ^ Int.natAbs n) n
[PROOFSTEP]
refine' (norm_exp_mul_sq_le (hR.trans_le hτ) n).trans _
[GOAL]
case refine'_3
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
τ✝ : ℂ
hτ : R ≤ τ✝.im
n : ℤ
⊢ rexp (-π * τ✝.im) ^ Int.natAbs n ≤ (fun n => y ^ Int.natAbs n) n
[PROOFSTEP]
refine' pow_le_pow_of_le_left (exp_pos _).le (Real.exp_le_exp.mpr _) _
[GOAL]
case refine'_3
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
τ✝ : ℂ
hτ : R ≤ τ✝.im
n : ℤ
⊢ -π * τ✝.im ≤ -π * R
[PROOFSTEP]
rwa [mul_le_mul_left_of_neg (neg_lt_zero.mpr pi_pos)]
[GOAL]
case refine'_1
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs ↑n
case refine'_2 R : ℝ hR : 0 < R y : ℝ := rexp (-π * R) h : y < 1 ⊢ Summable fun n => y ^ Int.natAbs (-↑n)
[PROOFSTEP]
all_goals simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using summable_geometric_of_lt_1 (Real.exp_pos _).le h
[GOAL]
case refine'_1
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs ↑n
[PROOFSTEP]
simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using summable_geometric_of_lt_1 (Real.exp_pos _).le h
[GOAL]
case refine'_2
R : ℝ
hR : 0 < R
y : ℝ := rexp (-π * R)
h : y < 1
⊢ Summable fun n => y ^ Int.natAbs (-↑n)
[PROOFSTEP]
simpa only [Int.natAbs_neg, Int.natAbs_ofNat] using summable_geometric_of_lt_1 (Real.exp_pos _).le h
[GOAL]
z : ℂ
⊢ jacobiTheta (2 + z) = jacobiTheta z
[PROOFSTEP]
refine' tsum_congr fun n => _
[GOAL]
z : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * (2 + z)) = cexp (↑π * I * ↑n ^ 2 * z)
[PROOFSTEP]
suffices cexp (↑π * I * (n : ℂ) ^ 2 * 2) = 1 by rw [mul_add, Complex.exp_add, this, one_mul]
[GOAL]
z : ℂ
n : ℤ
this : cexp (↑π * I * ↑n ^ 2 * 2) = 1
⊢ cexp (↑π * I * ↑n ^ 2 * (2 + z)) = cexp (↑π * I * ↑n ^ 2 * z)
[PROOFSTEP]
rw [mul_add, Complex.exp_add, this, one_mul]
[GOAL]
z : ℂ
n : ℤ
⊢ cexp (↑π * I * ↑n ^ 2 * 2) = 1
[PROOFSTEP]
rw [(by push_cast ; ring : ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * π * I)), Complex.exp_int_mul, Complex.exp_two_pi_mul_I,
  one_zpow]
[GOAL]
z : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑(n ^ 2) * (2 * ↑π * I)
[PROOFSTEP]
push_cast
[GOAL]
z : ℂ
n : ℤ
⊢ ↑π * I * ↑n ^ 2 * 2 = ↑n ^ 2 * (2 * ↑π * I)
[PROOFSTEP]
ring
[GOAL]
τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ
[PROOFSTEP]
suffices ↑(ModularGroup.T ^ 2 • τ) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add]
[GOAL]
τ : ℍ
this : ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ
[PROOFSTEP]
simp_rw [this, jacobiTheta_two_add]
[GOAL]
τ : ℍ
⊢ ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
[PROOFSTEP]
have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := by rfl
[GOAL]
τ : ℍ
⊢ ModularGroup.T ^ 2 = ModularGroup.T ^ 2
[PROOFSTEP]
rfl
[GOAL]
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
[PROOFSTEP]
simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd]
[GOAL]
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑↑2 + ↑τ = 2 + ↑τ
[PROOFSTEP]
norm_cast
[GOAL]
τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.S • τ) = (-I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
[PROOFSTEP]
unfold jacobiTheta
[GOAL]
τ : ℍ
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑(ModularGroup.S • τ)) =
    (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
rw [UpperHalfPlane.modular_S_smul, UpperHalfPlane.coe_mk]
[GOAL]
τ : ℍ
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have ha : 0 < (-I * τ).re :=
  by
  rw [neg_mul, neg_re, mul_re, I_re, I_im, zero_mul, one_mul, zero_sub, neg_neg]
  exact τ.im_pos
[GOAL]
τ : ℍ
⊢ 0 < (-I * ↑τ).re
[PROOFSTEP]
rw [neg_mul, neg_re, mul_re, I_re, I_im, zero_mul, one_mul, zero_sub, neg_neg]
[GOAL]
τ : ℍ
⊢ 0 < (↑τ).im
[PROOFSTEP]
exact τ.im_pos
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have ha' : (-I * τ) ^ (1 / 2 : ℂ) ≠ 0 := by
  rw [Ne.def, cpow_eq_zero_iff]
  contrapose! ha
  rw [ha.1, zero_re]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
⊢ (-I * ↑τ) ^ (1 / 2) ≠ 0
[PROOFSTEP]
rw [Ne.def, cpow_eq_zero_iff]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
⊢ ¬(-I * ↑τ = 0 ∧ 1 / 2 ≠ 0)
[PROOFSTEP]
contrapose! ha
[GOAL]
τ : ℍ
ha : -I * ↑τ = 0 ∧ 1 / 2 ≠ 0
⊢ (-I * ↑τ).re ≤ 0
[PROOFSTEP]
rw [ha.1, zero_re]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have hτ : (τ : ℂ) ≠ 0 := τ.ne_zero
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have := Complex.tsum_exp_neg_mul_int_sq ha
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this :
  ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2) = 1 / (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2)
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
rw [mul_comm ((1 : ℂ) / _) _, mul_one_div, eq_div_iff ha', mul_comm _ (_ ^ _), eq_comm] at this
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have expo1 : ∀ n : ℤ, -↑π / (-I * ↑τ) * (n : ℂ) ^ 2 = ↑π * I * (n : ℂ) ^ 2 * (-↑τ)⁻¹ :=
  by
  intro n
  field_simp [hτ, I_ne_zero]
  ring_nf
  rw [I_sq, mul_neg, mul_one, neg_neg]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
⊢ ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
[PROOFSTEP]
intro n
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
n : ℤ
⊢ -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
[PROOFSTEP]
field_simp [hτ, I_ne_zero]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
n : ℤ
⊢ ↑π * ↑n ^ 2 * ↑τ = -(↑π * I * ↑n ^ 2 * (I * ↑τ))
[PROOFSTEP]
ring_nf
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
n : ℤ
⊢ ↑π * ↑n ^ 2 * ↑τ = -(↑π * ↑n ^ 2 * ↑τ * I ^ 2)
[PROOFSTEP]
rw [I_sq, mul_neg, mul_one, neg_neg]
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
this : ∑' (n : ℤ), cexp (-↑π / (-I * ↑τ) * ↑n ^ 2) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
simp_rw [expo1] at this
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
have expo2 : ∀ n : ℤ, -↑π * (-I * ↑τ) * (n : ℂ) ^ 2 = ↑π * I * (n : ℂ) ^ 2 * ↑τ :=
  by
  intro n
  ring_nf
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
⊢ ∀ (n : ℤ), -↑π * (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * ↑τ
[PROOFSTEP]
intro n
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
n : ℤ
⊢ -↑π * (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * ↑τ
[PROOFSTEP]
ring_nf
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (-↑π * (-I * ↑τ) * ↑n ^ 2)
expo2 : ∀ (n : ℤ), -↑π * (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * ↑τ
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
simp_rw [expo2] at this
[GOAL]
τ : ℍ
ha : 0 < (-I * ↑τ).re
ha' : (-I * ↑τ) ^ (1 / 2) ≠ 0
hτ : ↑τ ≠ 0
expo1 : ∀ (n : ℤ), -↑π / (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * (-↑τ)⁻¹
expo2 : ∀ (n : ℤ), -↑π * (-I * ↑τ) * ↑n ^ 2 = ↑π * I * ↑n ^ 2 * ↑τ
this : ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
⊢ ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * (-↑τ)⁻¹) = (-I * ↑τ) ^ (1 / 2) * ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * ↑τ)
[PROOFSTEP]
exact this
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)
[PROOFSTEP]
have := (summable_exp_mul_sq hz).hasSum.sum_nat_of_sum_int
[GOAL]
z : ℂ
hz : 0 < z.im
this :
  HasSum (fun n => cexp (↑π * I * ↑↑n ^ 2 * z) + cexp (↑π * I * ↑(-↑n) ^ 2 * z))
    (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) + cexp (↑π * I * ↑0 ^ 2 * z))
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)
[PROOFSTEP]
rw [← @hasSum_nat_add_iff' ℂ _ _ _ _ 1] at this
[GOAL]
z : ℂ
hz : 0 < z.im
this :
  HasSum (fun n => cexp (↑π * I * ↑↑(n + 1) ^ 2 * z) + cexp (↑π * I * ↑(-↑(n + 1)) ^ 2 * z))
    (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) + cexp (↑π * I * ↑0 ^ 2 * z) -
      ∑ i in Finset.range 1, (cexp (↑π * I * ↑↑i ^ 2 * z) + cexp (↑π * I * ↑(-↑i) ^ 2 * z)))
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)
[PROOFSTEP]
simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_ofNat, Nat.cast_zero, neg_zero, Int.cast_zero, sq (0 : ℂ),
  mul_zero, zero_mul, neg_sq, ← mul_two, Complex.exp_zero, add_sub_assoc, (by norm_num : (1 : ℂ) - 1 * 2 = -1), ←
  sub_eq_add_neg, Nat.cast_add, Nat.cast_one] at this
[GOAL]
z : ℂ
hz : 0 < z.im
this : HasSum (fun n => cexp (↑π * I * ↑(n + 1) ^ 2 * z) * 2) (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) + (1 - 1 * 2))
⊢ 1 - 1 * 2 = -1
[PROOFSTEP]
norm_num
[GOAL]
z : ℂ
hz : 0 < z.im
this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z) * 2) (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) - 1)
⊢ HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) ((jacobiTheta z - 1) / 2)
[PROOFSTEP]
convert this.div_const 2 using 1
[GOAL]
case h.e'_5
z : ℂ
hz : 0 < z.im
this : HasSum (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z) * 2) (∑' (b : ℤ), cexp (↑π * I * ↑b ^ 2 * z) - 1)
⊢ (fun n => cexp (↑π * I * (↑n + 1) ^ 2 * z)) = fun i => cexp (↑π * I * (↑i + 1) ^ 2 * z) * 2 / 2
[PROOFSTEP]
simp_rw [mul_div_cancel (G₀ := ℂ) _ two_ne_zero]
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ jacobiTheta z = 1 + 2 * ∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)
[PROOFSTEP]
rw [(hasSum_nat_jacobiTheta hz).tsum_eq, mul_div_cancel' _ (two_ne_zero' ℂ), ← add_sub_assoc, add_sub_cancel']
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ ‖jacobiTheta z - 1‖ ≤ 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im)
[PROOFSTEP]
suffices ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im)) by
  calc
    ‖jacobiTheta z - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ := by
      rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hz), norm_mul, Complex.norm_eq_abs, Complex.abs_two]
    _ ≤ 2 * (rexp (-π * z.im) / (1 - rexp (-π * z.im))) := by rwa [mul_le_mul_left (zero_lt_two' ℝ)]
    _ = 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im) := by rw [div_mul_comm, mul_comm]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
⊢ ‖jacobiTheta z - 1‖ ≤ 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im)
[PROOFSTEP]
calc
  ‖jacobiTheta z - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ := by
    rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hz), norm_mul, Complex.norm_eq_abs, Complex.abs_two]
  _ ≤ 2 * (rexp (-π * z.im) / (1 - rexp (-π * z.im))) := by rwa [mul_le_mul_left (zero_lt_two' ℝ)]
  _ = 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im) := by rw [div_mul_comm, mul_comm]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
⊢ ‖jacobiTheta z - 1‖ = 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖
[PROOFSTEP]
rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hz), norm_mul, Complex.norm_eq_abs, Complex.abs_two]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
⊢ 2 * ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ 2 * (rexp (-π * z.im) / (1 - rexp (-π * z.im)))
[PROOFSTEP]
rwa [mul_le_mul_left (zero_lt_two' ℝ)]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
⊢ 2 * (rexp (-π * z.im) / (1 - rexp (-π * z.im))) = 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im)
[PROOFSTEP]
rw [div_mul_comm, mul_comm]
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
[PROOFSTEP]
have : ∀ n : ℕ, ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1) :=
  by
  intro n
  simpa only [Int.cast_add, Int.cast_one] using norm_exp_mul_sq_le hz (n + 1)
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
[PROOFSTEP]
intro n
[GOAL]
z : ℂ
hz : 0 < z.im
n : ℕ
⊢ ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
[PROOFSTEP]
simpa only [Int.cast_add, Int.cast_one] using norm_exp_mul_sq_le hz (n + 1)
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
[PROOFSTEP]
have s : HasSum (fun n : ℕ => rexp (-π * z.im) ^ (n + 1)) (rexp (-π * z.im) / (1 - rexp (-π * z.im))) :=
  by
  simp_rw [pow_succ, div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
  exact
    hasSum_geometric_of_lt_1 (exp_pos (-π * z.im)).le
      (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hz)
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
⊢ HasSum (fun n => rexp (-π * z.im) ^ (n + 1)) (rexp (-π * z.im) / (1 - rexp (-π * z.im)))
[PROOFSTEP]
simp_rw [pow_succ, div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
⊢ HasSum (fun i => rexp (-π * z.im) ^ i) (1 - rexp (-π * z.im))⁻¹
[PROOFSTEP]
exact
  hasSum_geometric_of_lt_1 (exp_pos (-π * z.im)).le
    (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hz)
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
s : HasSum (fun n => rexp (-π * z.im) ^ (n + 1)) (rexp (-π * z.im) / (1 - rexp (-π * z.im)))
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
[PROOFSTEP]
have aux : Summable fun n : ℕ => ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * z)‖ :=
  summable_of_nonneg_of_le (fun n => norm_nonneg _) this s.summable
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (n : ℕ), ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) ^ (n + 1)
s : HasSum (fun n => rexp (-π * z.im) ^ (n + 1)) (rexp (-π * z.im) / (1 - rexp (-π * z.im)))
aux : Summable fun n => ‖cexp (↑π * I * (↑n + 1) ^ 2 * z)‖
⊢ ‖∑' (n : ℕ), cexp (↑π * I * (↑n + 1) ^ 2 * z)‖ ≤ rexp (-π * z.im) / (1 - rexp (-π * z.im))
[PROOFSTEP]
exact (norm_tsum_le_tsum_norm aux).trans ((tsum_mono aux s.summable this).trans (le_of_eq s.tsum_eq))
[GOAL]
⊢ (fun τ => jacobiTheta τ - 1) =O[comap im atTop] fun τ => rexp (-π * τ.im)
[PROOFSTEP]
simp_rw [IsBigO, IsBigOWith, Filter.eventually_comap, Filter.eventually_atTop]
[GOAL]
⊢ ∃ c a, ∀ (b : ℝ), b ≥ a → ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖
[PROOFSTEP]
refine'
  ⟨2 / (1 - rexp (-π)), 1, fun y hy z hz =>
    (norm_jacobiTheta_sub_one_le (hz.symm ▸ zero_lt_one.trans_le hy : 0 < im z)).trans _⟩
[GOAL]
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im) ≤ 2 / (1 - rexp (-π)) * ‖rexp (-π * z.im)‖
[PROOFSTEP]
rw [Real.norm_eq_abs, Real.abs_exp]
[GOAL]
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 2 / (1 - rexp (-π * z.im)) * rexp (-π * z.im) ≤ 2 / (1 - rexp (-π)) * rexp (-π * z.im)
[PROOFSTEP]
refine' mul_le_mul_of_nonneg_right _ (exp_pos _).le
[GOAL]
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 2 / (1 - rexp (-π * z.im)) ≤ 2 / (1 - rexp (-π))
[PROOFSTEP]
rw [div_le_div_left (zero_lt_two' ℝ), sub_le_sub_iff_left, exp_le_exp, neg_mul, neg_le_neg_iff]
[GOAL]
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ π ≤ π * z.im
[PROOFSTEP]
exact le_mul_of_one_le_right pi_pos.le (hz.symm ▸ hy)
[GOAL]
case hb
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 0 < 1 - rexp (-π * z.im)
[PROOFSTEP]
rw [sub_pos, exp_lt_one_iff, neg_mul, neg_lt_zero]
[GOAL]
case hb
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 0 < π * z.im
[PROOFSTEP]
exact mul_pos pi_pos (hz.symm ▸ zero_lt_one.trans_le hy)
[GOAL]
case hc
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 0 < 1 - rexp (-π)
[PROOFSTEP]
rw [sub_pos, exp_lt_one_iff, neg_lt_zero]
[GOAL]
case hc
y : ℝ
hy : y ≥ 1
z : ℂ
hz : z.im = y
⊢ 0 < π
[PROOFSTEP]
exact pi_pos
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ DifferentiableAt ℂ jacobiTheta z
[PROOFSTEP]
suffices
  ∀ (y : ℝ) (_ : 0 < y), DifferentiableOn ℂ (fun z => ∑' n : ℤ, cexp (π * I * (n : ℂ) ^ 2 * z)) {w : ℂ | y < im w}
  by
  let ⟨y, hy, hy'⟩ := exists_between hz
  exact (this y hy).differentiableAt ((Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hy')
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (y : ℝ), 0 < y → DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
⊢ DifferentiableAt ℂ jacobiTheta z
[PROOFSTEP]
let ⟨y, hy, hy'⟩ := exists_between hz
[GOAL]
z : ℂ
hz : 0 < z.im
this : ∀ (y : ℝ), 0 < y → DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
y : ℝ
hy : 0 < y
hy' : y < z.im
⊢ DifferentiableAt ℂ jacobiTheta z
[PROOFSTEP]
exact (this y hy).differentiableAt ((Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hy')
[GOAL]
z : ℂ
hz : 0 < z.im
⊢ ∀ (y : ℝ), 0 < y → DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
intro y hy
[GOAL]
z : ℂ
hz : 0 < z.im
y : ℝ
hy : 0 < y
⊢ DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
have h1 :
  ∀ (n : ℤ) (w : ℂ) (_ : y < im w),
    DifferentiableWithinAt ℂ (fun v : ℂ => cexp (π * I * (n : ℂ) ^ 2 * v)) {z : ℂ | y < im z} w :=
  fun n w _ => (differentiableAt_id.const_mul _).cexp.differentiableWithinAt
[GOAL]
z : ℂ
hz : 0 < z.im
y : ℝ
hy : 0 < y
h1 : ∀ (n : ℤ) (w : ℂ), y < w.im → DifferentiableWithinAt ℂ (fun v => cexp (↑π * I * ↑n ^ 2 * v)) {z | y < z.im} w
⊢ DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
have h2 : IsOpen {w : ℂ | y < im w} := continuous_im.isOpen_preimage _ isOpen_Ioi
[GOAL]
z : ℂ
hz : 0 < z.im
y : ℝ
hy : 0 < y
h1 : ∀ (n : ℤ) (w : ℂ), y < w.im → DifferentiableWithinAt ℂ (fun v => cexp (↑π * I * ↑n ^ 2 * v)) {z | y < z.im} w
h2 : IsOpen {w | y < w.im}
⊢ DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
obtain ⟨bd, bd_s, le_bd⟩ := exists_summable_bound_exp_mul_sq hy
[GOAL]
case intro.intro
z : ℂ
hz : 0 < z.im
y : ℝ
hy : 0 < y
h1 : ∀ (n : ℤ) (w : ℂ), y < w.im → DifferentiableWithinAt ℂ (fun v => cexp (↑π * I * ↑n ^ 2 * v)) {z | y < z.im} w
h2 : IsOpen {w | y < w.im}
bd : ℤ → ℝ
bd_s : Summable bd
le_bd : ∀ {τ : ℂ}, y ≤ τ.im → ∀ (n : ℤ), ‖cexp (↑π * I * ↑n ^ 2 * τ)‖ ≤ bd n
⊢ DifferentiableOn ℂ (fun z => ∑' (n : ℤ), cexp (↑π * I * ↑n ^ 2 * z)) {w | y < w.im}
[PROOFSTEP]
exact differentiableOn_tsum_of_summable_norm bd_s h1 h2 fun i w hw => le_bd (le_of_lt hw) i