-- Mathlib/NumberTheory/Modular.lean
theorem abs_c_le_one (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : |g 1 0| ≤ 1

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ 9 * c ^ 4 < c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16

Tactic:
linarith

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ (c * z.im) ^ 4 / nsq ^ 2 * 16 ≤ 16

Tactic:
linarith

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c' ^ 2 < 4
⊢ |↑g 1 0| ≤ 1

Tactic:
replace this : c' ^ 2 ≤ 1 ^ 2 := by omega

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c' ^ 2 ≤ 1 ^ 2
⊢ |↑g 1 0| ≤ 1

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
⊢ 9 * c ^ 4 < 16

Tactic:
have h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4 := by
  gcongr <;> apply three_lt_four_mul_im_sq_of_mem_fdo <;> assumption

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
⊢ 9 * c ^ 4 < 16

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ 9 * c ^ 4 < 16

Tactic:
calc
  9 * c ^ 4 < c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 := by linarith
  _ = c ^ 4 * z.im ^ 4 / nsq ^ 2 * 16 := by
    rw [im_smul_eq_div_normSq, div_pow]
    ring
  _ ≤ 16 := by rw [← mul_pow]; linarith

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ |↑g 1 0| ≤ 1

Tactic:
suffices 3 * c ^ 2 < 4 by
  rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_lt] at this
  replace this : c' ^ 2 ≤ 1 ^ 2 := by omega
  rwa [sq_le_sq, abs_one] at this

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ 3 * c ^ 2 < 4

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ c ≠ 0 → 9 * c ^ 4 < 16

Tactic:
intro hc

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
⊢ 9 * c ^ 4 < 16

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c' ^ 2 < 4
⊢ c' ^ 2 ≤ 1 ^ 2

Tactic:
omega

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ c ^ 4 * z.im ^ 4 / nsq ^ 2 * 16 ≤ 16

Tactic:
rw [← mul_pow]

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ (c * z.im) ^ 4 / nsq ^ 2 * 16 ≤ 16

Proof state:
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c = 0
⊢ 3 * c ^ 2 < 4

Tactic:
rw [hc]

Result:
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c = 0
⊢ 3 * 0 ^ 2 < 4

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ c ^ 4 * z.im ^ 2 * (g • z).im ^ 2 * 16 = c ^ 4 * z.im ^ 4 / nsq ^ 2 * 16

Tactic:
rw [im_smul_eq_div_normSq, div_pow]

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ c ^ 4 * z.im ^ 2 * (z.im ^ 2 / normSq (denom (↑g) z) ^ 2) * 16 = c ^ 4 * z.im ^ 4 / nsq ^ 2 * 16

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
⊢ 9 * c ^ 4 < 16

Tactic:
let nsq := normSq (denom g z)

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
nsq : ℝ := normSq (denom (↑g) z)
⊢ 9 * c ^ 4 < 16

Proof state:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c ≠ 0
⊢ (3 * c ^ 2) ^ 2 < 4 ^ 2

Tactic:
specialize this hc

Result:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
this : 9 * c ^ 4 < 16
⊢ (3 * c ^ 2) ^ 2 < 4 ^ 2

Proof state:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c ≠ 0
⊢ 3 * c ^ 2 < 4

Tactic:
refine (abs_lt_of_sq_lt_sq' ?_ (by norm_num)).2

Result:
case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c ≠ 0
⊢ (3 * c ^ 2) ^ 2 < 4 ^ 2

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
⊢ 9 * c ^ 4 < 16

Tactic:
have h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1 :=
  div_le_one_of_le₀
    (pow_four_le_pow_two_of_pow_two_le (z.c_mul_im_sq_le_normSq_denom g))
    (sq_nonneg _)

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
h₁ : 3 * 3 * c ^ 4 < 4 * (g • z).im ^ 2 * (4 * z.im ^ 2) * c ^ 4
h₂ : (c * z.im) ^ 4 / normSq (denom (↑g) z) ^ 2 ≤ 1
⊢ 9 * c ^ 4 < 16

Proof state:
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c = 0
⊢ 3 * 0 ^ 2 < 4

Tactic:
norm_num

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
⊢ 3 * c ^ 2 < 4

Tactic:
rcases eq_or_ne c 0 with (hc | hc)

Result:
case inl
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c = 0
⊢ 3 * c ^ 2 < 4

case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c ≠ 0
⊢ 3 * c ^ 2 < 4

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c ≠ 0 → 9 * c ^ 4 < 16
hc : c ≠ 0
⊢ 0 ≤ 4

Tactic:
norm_num

Result:
no goals

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c ^ 2 < 4
⊢ |↑g 1 0| ≤ 1

Tactic:
rw [← Int.cast_pow, ← Int.cast_three, ← Int.cast_four, ← Int.cast_mul, Int.cast_lt] at this

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c' ^ 2 < 4
⊢ |↑g 1 0| ≤ 1

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
⊢ |↑g 1 0| ≤ 1

Tactic:
let c := (c' : ℝ)

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ |↑g 1 0| ≤ 1

Proof state:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
⊢ |↑g 1 0| ≤ 1

Tactic:
let c' : ℤ := g 1 0

Result:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟ᵒ
c' : ℤ := ↑g 1 0
⊢ |↑g 1 0| ≤ 1