[GOAL]
⊢ 0 < Complex.I.im
[PROOFSTEP]
simp
[GOAL]
z : ℍ
⊢ 0 < ↑Complex.normSq ↑z
[PROOFSTEP]
rw [Complex.normSq_pos]
[GOAL]
z : ℍ
⊢ ↑z ≠ 0
[PROOFSTEP]
exact z.ne_zero
[GOAL]
z : ℍ
⊢ 0 < (-↑z)⁻¹.im
[PROOFSTEP]
simpa using div_pos z.property (normSq_pos z)
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : cd ≠ 0
⊢ ↑(cd 0) * ↑z + ↑(cd 1) ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
⊢ cd = 0
[PROOFSTEP]
have : cd 0 = 0 := by
  -- we will need this twice
  apply_fun Complex.im at h 
  simpa only [z.im_ne_zero, Complex.add_im, add_zero, coe_im, zero_mul, or_false_iff, Complex.ofReal_im,
    Complex.zero_im, Complex.mul_im, mul_eq_zero] using h
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
⊢ cd 0 = 0
[PROOFSTEP]
apply_fun Complex.im at h 
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : (↑(cd 0) * ↑z + ↑(cd 1)).im = 0.im
⊢ cd 0 = 0
[PROOFSTEP]
simpa only [z.im_ne_zero, Complex.add_im, add_zero, coe_im, zero_mul, or_false_iff, Complex.ofReal_im, Complex.zero_im,
  Complex.mul_im, mul_eq_zero] using h
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
h : ↑(cd 0) * ↑z + ↑(cd 1) = 0
this : cd 0 = 0
⊢ cd = 0
[PROOFSTEP]
simp only [this, zero_mul, Complex.ofReal_zero, zero_add, Complex.ofReal_eq_zero] at h 
[GOAL]
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
⊢ cd = 0
[PROOFSTEP]
ext i
[GOAL]
case h
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
i : Fin 2
⊢ cd i = OfNat.ofNat 0 i
[PROOFSTEP]
fin_cases i
[GOAL]
case h.head
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
⊢ cd { val := 0, isLt := (_ : 0 < 2) } = OfNat.ofNat 0 { val := 0, isLt := (_ : 0 < 2) }
[PROOFSTEP]
assumption
[GOAL]
case h.tail.head
cd : Fin 2 → ℝ
z : ℍ
this : cd 0 = 0
h : cd 1 = 0
⊢ cd { val := 1, isLt := (_ : (fun a => a < 2) 1) } = OfNat.ofNat 0 { val := 1, isLt := (_ : (fun a => a < 2) 1) }
[PROOFSTEP]
assumption
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ denom g z ≠ 0
[PROOFSTEP]
intro H
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
⊢ False
[PROOFSTEP]
have DET := (mem_glpos _).1 g.prop
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < ↑(↑GeneralLinearGroup.det ↑g)
⊢ False
[PROOFSTEP]
have hz := z.prop
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < ↑(↑GeneralLinearGroup.det ↑g)
hz : 0 < (↑z).im
⊢ False
[PROOFSTEP]
simp only [GeneralLinearGroup.det_apply_val] at DET 
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
⊢ False
[PROOFSTEP]
have H1 : (↑ₘg 1 0 : ℝ) = 0 ∨ z.im = 0 := by simpa [num, denom] using congr_arg Complex.im H
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
⊢ ↑↑g 1 0 = 0 ∨ im z = 0
[PROOFSTEP]
simpa [num, denom] using congr_arg Complex.im H
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
H1 : ↑↑g 1 0 = 0 ∨ im z = 0
⊢ False
[PROOFSTEP]
cases' H1 with H1
[GOAL]
case inl
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
H1 : ↑↑g 1 0 = 0
⊢ False
[PROOFSTEP]
simp only [H1, Complex.ofReal_zero, denom, zero_mul, zero_add, Complex.ofReal_eq_zero] at H 
[GOAL]
case inl
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
H1 : ↑↑g 1 0 = 0
H : ↑↑g 1 1 = 0
⊢ False
[PROOFSTEP]
rw [Matrix.det_fin_two (↑ₘg : Matrix (Fin 2) (Fin 2) ℝ)] at DET 
[GOAL]
case inl
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
DET : 0 < ↑↑g 0 0 * ↑↑g 1 1 - ↑↑g 0 1 * ↑↑g 1 0
hz : 0 < (↑z).im
H1 : ↑↑g 1 0 = 0
H : ↑↑g 1 1 = 0
⊢ False
[PROOFSTEP]
simp only [H, H1, mul_zero, sub_zero, lt_self_iff_false] at DET 
[GOAL]
case inr
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
hz : 0 < (↑z).im
h✝ : im z = 0
⊢ False
[PROOFSTEP]
change z.im > 0 at hz 
[GOAL]
case inr
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
H : denom g z = 0
DET : 0 < det ↑↑g
h✝ : im z = 0
hz : im z > 0
⊢ False
[PROOFSTEP]
linarith
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (smulAux' g z).im = det ↑↑g * im z / ↑Complex.normSq (denom g z)
[PROOFSTEP]
rw [smulAux', Complex.div_im]
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (num g z).im * (denom g z).re / ↑Complex.normSq (denom g z) -
      (num g z).re * (denom g z).im / ↑Complex.normSq (denom g z) =
    det ↑↑g * im z / ↑Complex.normSq (denom g z)
[PROOFSTEP]
field_simp [smulAux', num, denom]
  -- porting note: the local notation still didn't work here
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ↑↑g 0 0 * im z * (↑↑g 1 0 * re z + ↑↑g 1 1) / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) -
      (↑↑g 0 0 * re z + ↑↑g 0 1) * (↑↑g 1 0 * im z) / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    det ↑↑g * im z / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1))
[PROOFSTEP]
rw [Matrix.det_fin_two ((g : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ)]
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ↑↑g 0 0 * im z * (↑↑g 1 0 * re z + ↑↑g 1 1) / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) -
      (↑↑g 0 0 * re z + ↑↑g 0 1) * (↑↑g 1 0 * im z) / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    (↑↑g 0 0 * ↑↑g 1 1 - ↑↑g 0 1 * ↑↑g 1 0) * im z / ↑Complex.normSq (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1))
[PROOFSTEP]
ring
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ 0 < (smulAux' g z).im
[PROOFSTEP]
rw [smulAux'_im]
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ 0 < det ↑↑g * im z / ↑Complex.normSq (denom g z)
[PROOFSTEP]
convert mul_pos ((mem_glpos _).1 g.prop) (div_pos z.im_pos (Complex.normSq_pos.mpr (denom_ne_zero g z))) using 1
[GOAL]
case h.e'_4
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ det ↑↑g * im z / ↑Complex.normSq (denom g z) = ↑(↑GeneralLinearGroup.det ↑g) * (im z / ↑Complex.normSq (denom g z))
[PROOFSTEP]
simp only [GeneralLinearGroup.det_apply_val]
[GOAL]
case h.e'_4
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ det ↑↑g * im z / ↑Complex.normSq (denom g z) = det ↑↑g * (im z / ↑Complex.normSq (denom g z))
[PROOFSTEP]
ring
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ denom (x * y) z = denom x (smulAux y z) * denom y z
[PROOFSTEP]
change _ = (_ * (_ / _) + _) * _
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ denom (x * y) z = (↑(↑↑x 1 0) * (num y z / denom y z) + ↑(↑↑x 1 1)) * denom y z
[PROOFSTEP]
field_simp [denom_ne_zero]
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ denom (x * y) z = ↑(↑↑x 1 0) * num y z + ↑(↑↑x 1 1) * denom y z
[PROOFSTEP]
simp only [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, denom, num, Subgroup.coe_mul, GeneralLinearGroup.coe_mul,
  Fintype.univ_ofSubsingleton, Fin.mk_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add,
  Complex.ofReal_mul]
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (↑(↑↑x 1 0) * ↑(↑↑y 0 0) + ↑(↑↑x 1 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 1 0) * ↑(↑↑y 0 1) + ↑(↑↑x 1 1) * ↑(↑↑y 1 1)) =
    ↑(↑↑x 1 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 1 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))
[PROOFSTEP]
ring
[GOAL]
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ smulAux (x * y) z = smulAux x (smulAux y z)
[PROOFSTEP]
ext1
  -- Porting note: was `change _ / _ = (_ * (_ / _) + _) * _`
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ↑(smulAux (x * y) z) = ↑(smulAux x (smulAux y z))
[PROOFSTEP]
change _ / _ = (_ * (_ / _) + _) / _
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (x * y) z / denom (x * y) z = (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)
[PROOFSTEP]
rw [denom_cocycle]
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (x * y) z / (denom x (smulAux y z) * denom y z) =
    (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)
[PROOFSTEP]
field_simp [denom_ne_zero]
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (x * y) z * (denom y z * denom x (smulAux y z)) =
    (↑(↑↑x 0 0) * num y z + ↑(↑↑x 0 1) * denom y z) * (denom x (smulAux y z) * denom y z)
[PROOFSTEP]
simp only [Matrix.mul_apply, dotProduct, Fin.sum_univ_succ, num, denom, Subgroup.coe_mul, GeneralLinearGroup.coe_mul,
  Fintype.univ_ofSubsingleton, Fin.mk_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, Complex.ofReal_add,
  Complex.ofReal_mul]
[GOAL]
case h
x y : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ((↑(↑↑x 0 0) * ↑(↑↑y 0 0) + ↑(↑↑x 0 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 0 0) * ↑(↑↑y 0 1) + ↑(↑↑x 0 1) * ↑(↑↑y 1 1))) *
      ((↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)) * (↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1))) =
    (↑(↑↑x 0 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 0 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))) *
      ((↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1)) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)))
[PROOFSTEP]
ring
[GOAL]
z : ℍ
⊢ 1 • z = z
[PROOFSTEP]
ext1
[GOAL]
case h
z : ℍ
⊢ ↑(1 • z) = ↑z
[PROOFSTEP]
change _ / _ = _
[GOAL]
case h
z : ℍ
⊢ num 1 z / denom 1 z = ↑z
[PROOFSTEP]
simp [num, denom]
[GOAL]
Γ : Subgroup SL(2, ℤ)
g : SL(2, ℤ)
⊢ det ↑↑↑g = 1
[PROOFSTEP]
simp only [SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, SpecialLinearGroup.det_coe, coe']
[GOAL]
Γ : Subgroup SL(2, ℤ)
⊢ ∀ (x : SL(2, ℤ)) (y : { x // x ∈ GL(2, ℝ)⁺ }) (z : ℍ), (x • y) • z = x • y • z
[PROOFSTEP]
intro s g z
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : SL(2, ℤ)
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (s • g) • z = s • g • z
[PROOFSTEP]
simp only [SLOnGLPos_smul_apply]
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : SL(2, ℤ)
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (↑s * g) • z = s • g • z
[PROOFSTEP]
apply mul_smul'
[GOAL]
Γ : Subgroup SL(2, ℤ)
⊢ ∀ (x : { x // x ∈ Γ }) (y : { x // x ∈ GL(2, ℝ)⁺ }) (z : ℍ), (x • y) • z = x • y • z
[PROOFSTEP]
intro s g z
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : { x // x ∈ Γ }
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (s • g) • z = s • g • z
[PROOFSTEP]
simp only [subgroup_on_glpos_smul_apply]
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : { x // x ∈ Γ }
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (↑↑s * g) • z = s • g • z
[PROOFSTEP]
apply mul_smul'
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : { x // x ∈ Γ }
g : SL(2, ℤ)
z : ℍ
⊢ (s • g) • z = s • g • z
[PROOFSTEP]
rw [subgroup_on_SL_apply]
[GOAL]
Γ : Subgroup SL(2, ℤ)
s : { x // x ∈ Γ }
g : SL(2, ℤ)
z : ℍ
⊢ (↑s * g) • z = s • g • z
[PROOFSTEP]
apply MulAction.mul_smul
[GOAL]
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ -g • z = g • z
[PROOFSTEP]
ext1
[GOAL]
case h
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ ↑(-g • z) = ↑(g • z)
[PROOFSTEP]
change _ / _ = _ / _
[GOAL]
case h
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (-g) z / denom (-g) z = num g z / denom g z
[PROOFSTEP]
field_simp [denom_ne_zero]
[GOAL]
case h
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ num (-g) z * denom g z = num g z * denom (-g) z
[PROOFSTEP]
simp only [num, denom, Complex.ofReal_neg, neg_mul, GLPos.coe_neg_GL, Units.val_neg, neg_apply]
[GOAL]
case h
g : { x // x ∈ GL(2, ℝ)⁺ }
z : ℍ
⊢ (-(↑(↑↑g 0 0) * ↑z) + -↑(↑↑g 0 1)) * (↑(↑↑g 1 0) * ↑z + ↑(↑↑g 1 1)) =
    (↑(↑↑g 0 0) * ↑z + ↑(↑↑g 0 1)) * (-(↑(↑↑g 1 0) * ↑z) + -↑(↑↑g 1 1))
[PROOFSTEP]
ring_nf
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
g : SL(2, ℤ)
z : ℍ
⊢ -g • z = g • z
[PROOFSTEP]
simp only [coe_GLPos_neg, sl_moeb, coe_int_neg, neg_smul, coe']
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
⊢ (↑↑(↑toGLPos g) 1 0 * im z) ^ 2 ≤ ↑Complex.normSq (denom (↑toGLPos g) z)
[PROOFSTEP]
let c := (↑ₘg 1 0 : ℝ)
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
⊢ (↑↑(↑toGLPos g) 1 0 * im z) ^ 2 ≤ ↑Complex.normSq (denom (↑toGLPos g) z)
[PROOFSTEP]
let d := (↑ₘg 1 1 : ℝ)
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
d : ℝ := ↑↑(↑toGLPos g) 1 1
⊢ (↑↑(↑toGLPos g) 1 0 * im z) ^ 2 ≤ ↑Complex.normSq (denom (↑toGLPos g) z)
[PROOFSTEP]
calc
  (c * z.im) ^ 2 ≤ (c * z.im) ^ 2 + (c * z.re + d) ^ 2 := by nlinarith
  _ = Complex.normSq (denom g z) := by dsimp [denom, Complex.normSq]; ring
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
d : ℝ := ↑↑(↑toGLPos g) 1 1
⊢ (c * im z) ^ 2 ≤ (c * im z) ^ 2 + (c * re z + d) ^ 2
[PROOFSTEP]
nlinarith
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
d : ℝ := ↑↑(↑toGLPos g) 1 1
⊢ (c * im z) ^ 2 + (c * re z + d) ^ 2 = ↑Complex.normSq (denom (↑toGLPos g) z)
[PROOFSTEP]
dsimp [denom, Complex.normSq]
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
z : ℍ
g : SL(2, ℝ)
c : ℝ := ↑↑(↑toGLPos g) 1 0
d : ℝ := ↑↑(↑toGLPos g) 1 1
⊢ (↑g 1 0 * im z) ^ 2 + (↑g 1 0 * re z + ↑g 1 1) ^ 2 =
    (↑g 1 0 * re z - 0 * im z + ↑g 1 1) * (↑g 1 0 * re z - 0 * im z + ↑g 1 1) +
      (↑g 1 0 * im z + 0 * re z + 0) * (↑g 1 0 * im z + 0 * re z + 0)
[PROOFSTEP]
ring
[GOAL]
g : SL(2, ℤ)
z : ℍ
Γ : Subgroup SL(2, ℤ)
⊢ im (g • z) = im z / ↑Complex.normSq (denom (↑g) z)
[PROOFSTEP]
convert im_smul_eq_div_normSq g z
[GOAL]
case h.e'_3.h.e'_5
g : SL(2, ℤ)
z : ℍ
Γ : Subgroup SL(2, ℤ)
⊢ im z = det ↑↑↑g * im z
[PROOFSTEP]
simp only [GeneralLinearGroup.det_apply_val, coe_GLPos_coe_GL_coe_matrix, Int.coe_castRingHom, (g : SL(2, ℝ)).prop,
  one_mul, coe']
[GOAL]
g✝ : SL(2, ℤ)
z✝ : ℍ
Γ : Subgroup SL(2, ℤ)
g : SL(2, ℤ)
z : ℍ
⊢ denom (↑g) z = ↑(↑g 1 0) * ↑z + ↑(↑g 1 1)
[PROOFSTEP]
simp [denom, coe']
[GOAL]
x : { x // 0 < x }
z : ℍ
⊢ 0 < (↑x • ↑z).im
[PROOFSTEP]
simpa using mul_pos x.2 z.2
[GOAL]
x : ℝ
z : ℍ
⊢ 0 < (↑x + ↑z).im
[PROOFSTEP]
simpa using z.im_pos
[GOAL]
x✝ : ℍ
⊢ ↑(0 +ᵥ x✝) = ↑x✝
[PROOFSTEP]
simp [HVAdd.hVAdd]
[GOAL]
x y : ℝ
z : ℍ
⊢ ↑(x + y +ᵥ z) = ↑(x +ᵥ (y +ᵥ z))
[PROOFSTEP]
simp [HVAdd.hVAdd, add_assoc]
[GOAL]
z : ℍ
⊢ ModularGroup.S • z = mk (-↑z)⁻¹ (_ : 0 < (-↑z)⁻¹.im)
[PROOFSTEP]
rw [specialLinearGroup_apply]
[GOAL]
z : ℍ
⊢ mk
      ((↑(↑(algebraMap ℤ ℝ) (↑↑ModularGroup.S 0 0)) * ↑z + ↑(↑(algebraMap ℤ ℝ) (↑↑ModularGroup.S 0 1))) /
        (↑(↑(algebraMap ℤ ℝ) (↑↑ModularGroup.S 1 0)) * ↑z + ↑(↑(algebraMap ℤ ℝ) (↑↑ModularGroup.S 1 1))))
      (_ : 0 < (↑(ModularGroup.S • z)).im) =
    mk (-↑z)⁻¹ (_ : 0 < (-↑z)⁻¹.im)
[PROOFSTEP]
simp [ModularGroup.S, neg_div, inv_neg, coeToGL]
[GOAL]
z : ℍ
n : ℤ
⊢ ModularGroup.T ^ n • z = ↑n +ᵥ z
[PROOFSTEP]
rw [← ext_iff, coe_vadd, add_comm, specialLinearGroup_apply, coe_mk]
  -- Porting note: added `coeToGL` and merged `rw` and `simp`
[GOAL]
z : ℍ
n : ℤ
⊢ (↑(↑(algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 0 0)) * ↑z + ↑(↑(algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 0 1))) /
      (↑(↑(algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 1 0)) * ↑z + ↑(↑(algebraMap ℤ ℝ) (↑↑(ModularGroup.T ^ n) 1 1))) =
    ↑z + ↑↑n
[PROOFSTEP]
simp [coeToGL, ModularGroup.coe_T_zpow, of_apply, cons_val_zero, algebraMap.coe_one, Complex.ofReal_one, one_mul,
  cons_val_one, head_cons, algebraMap.coe_zero, zero_mul, zero_add, div_one]
[GOAL]
z : ℍ
⊢ ModularGroup.T • z = 1 +ᵥ z
[PROOFSTEP]
simpa only [Int.cast_one] using modular_T_zpow_smul z 1
[GOAL]
g : SL(2, ℝ)
hc : ↑↑g 1 0 = 0
⊢ ∃ u v, (fun x x_1 => x • x_1) g = (fun z => v +ᵥ z) ∘ fun z => u • z
[PROOFSTEP]
obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc
[GOAL]
case intro.intro.intro
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
⊢ ∃ u v,
    (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } =
      (fun z => v +ᵥ z) ∘ fun z => u • z
[PROOFSTEP]
refine' ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, _⟩
[GOAL]
case intro.intro.intro
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
⊢ (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } =
    (fun z => b * a +ᵥ z) ∘ fun z => { val := a * a, property := (_ : 0 < a * a) } • z
[PROOFSTEP]
ext1 ⟨z, hz⟩
[GOAL]
case intro.intro.intro.h.mk
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
      { val := z, property := hz } =
    ((fun z => b * a +ᵥ z) ∘ fun z => { val := a * a, property := (_ : 0 < a * a) } • z) { val := z, property := hz }
[PROOFSTEP]
ext1
[GOAL]
case intro.intro.intro.h.mk.h
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑((fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
        { val := z, property := hz }) =
    ↑(((fun z => b * a +ᵥ z) ∘ fun z => { val := a * a, property := (_ : 0 < a * a) } • z) { val := z, property := hz })
[PROOFSTEP]
suffices ↑a * z * a + b * a = b * a + a * a * z by
  -- Porting note: added `coeToGL` and merged `rw` and `simpa`simpa [coeToGL, specialLinearGroup_apply, add_mul]
[GOAL]
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
z : ℂ
hz : 0 < z.im
this : ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z
⊢ ↑((fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) }
        { val := z, property := hz }) =
    ↑(((fun z => b * a +ᵥ z) ∘ fun z => { val := a * a, property := (_ : 0 < a * a) } • z) { val := z, property := hz })
[PROOFSTEP]
simpa [coeToGL, specialLinearGroup_apply, add_mul]
[GOAL]
case intro.intro.intro.h.mk.h
a b : ℝ
ha : a ≠ 0
hc : ↑↑{ val := ↑of ![![a, b], ![0, a⁻¹]], property := (_ : det (↑of ![![a, b], ![0, a⁻¹]]) = 1) } 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z
[PROOFSTEP]
ring
[GOAL]
g : SL(2, ℝ)
hc : ↑↑g 1 0 ≠ 0
⊢ ∃ u v w,
    (fun x x_1 => x • x_1) g =
      (fun x x_1 => x +ᵥ x_1) w ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
[PROOFSTEP]
have h_denom := denom_ne_zero g
[GOAL]
g : SL(2, ℝ)
hc : ↑↑g 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
⊢ ∃ u v w,
    (fun x x_1 => x • x_1) g =
      (fun x x_1 => x +ᵥ x_1) w ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
[PROOFSTEP]
induction' g using Matrix.SpecialLinearGroup.fin_two_induction with a b c d h
[GOAL]
case h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
hc : ↑↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 ≠ 0
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
⊢ ∃ u v w,
    (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      (fun x x_1 => x +ᵥ x_1) w ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
[PROOFSTEP]
replace hc : c ≠ 0
[GOAL]
case hc
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
hc : ↑↑{ val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } 1 0 ≠ 0
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
⊢ c ≠ 0
[PROOFSTEP]
simpa using hc
[GOAL]
case h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
⊢ ∃ u v w,
    (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
      (fun x x_1 => x +ᵥ x_1) w ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘ (fun x x_1 => x +ᵥ x_1) v ∘ (fun x x_1 => x • x_1) u
[PROOFSTEP]
refine' ⟨⟨_, mul_self_pos.mpr hc⟩, c * d, a / c, _⟩
[GOAL]
case h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
⊢ (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) } =
    (fun x x_1 => x +ᵥ x_1) (a / c) ∘
      (fun x x_1 => x • x_1) ModularGroup.S ∘
        (fun x x_1 => x +ᵥ x_1) (c * d) ∘ (fun x x_1 => x • x_1) { val := c * c, property := (_ : 0 < c * c) }
[PROOFSTEP]
ext1 ⟨z, hz⟩
[GOAL]
case h.h.mk
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ (fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
      { val := z, property := hz } =
    ((fun x x_1 => x +ᵥ x_1) (a / c) ∘
        (fun x x_1 => x • x_1) ModularGroup.S ∘
          (fun x x_1 => x +ᵥ x_1) (c * d) ∘ (fun x x_1 => x • x_1) { val := c * c, property := (_ : 0 < c * c) })
      { val := z, property := hz }
[PROOFSTEP]
ext1
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑((fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
        { val := z, property := hz }) =
    ↑(((fun x x_1 => x +ᵥ x_1) (a / c) ∘
          (fun x x_1 => x • x_1) ModularGroup.S ∘
            (fun x x_1 => x +ᵥ x_1) (c * d) ∘ (fun x x_1 => x • x_1) { val := c * c, property := (_ : 0 < c * c) })
        { val := z, property := hz })
[PROOFSTEP]
suffices (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹ by
  -- Porting note: golfed broken proofsimpa only [modular_S_smul, inv_neg, Function.comp_apply, coe_vadd,
    Complex.ofReal_mul, coe_pos_real_smul, Complex.real_smul, Complex.ofReal_div, coe_mk]
[GOAL]
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
this : (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
⊢ ↑((fun x x_1 => x • x_1) { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }
        { val := z, property := hz }) =
    ↑(((fun x x_1 => x +ᵥ x_1) (a / c) ∘
          (fun x x_1 => x • x_1) ModularGroup.S ∘
            (fun x x_1 => x +ᵥ x_1) (c * d) ∘ (fun x x_1 => x • x_1) { val := c * c, property := (_ : 0 < c * c) })
        { val := z, property := hz })
[PROOFSTEP]
simpa only [modular_S_smul, inv_neg, Function.comp_apply, coe_vadd, Complex.ofReal_mul, coe_pos_real_smul,
  Complex.real_smul, Complex.ofReal_div, coe_mk]
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
replace hc : (c : ℂ) ≠ 0
[GOAL]
case hc
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑c ≠ 0
[PROOFSTEP]
norm_cast
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
replace h_denom : ↑c * z + d ≠ 0
[GOAL]
case h_denom
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom (↑toGLPos { val := ↑of ![![a, b], ![c, d]], property := (_ : det (↑of ![![a, b], ![c, d]]) = 1) }) z ≠ 0
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
⊢ ↑c * z + ↑d ≠ 0
[PROOFSTEP]
simpa using h_denom ⟨z, hz⟩
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
have h_aux : (c : ℂ) * d + ↑c * ↑c * z ≠ 0 :=
  by
  rw [mul_assoc, ← mul_add, add_comm]
  exact mul_ne_zero hc h_denom
[GOAL]
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
⊢ ↑c * ↑d + ↑c * ↑c * z ≠ 0
[PROOFSTEP]
rw [mul_assoc, ← mul_add, add_comm]
[GOAL]
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
⊢ ↑c * (↑c * z + ↑d) ≠ 0
[PROOFSTEP]
exact mul_ne_zero hc h_denom
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
replace h : (a * d - b * c : ℂ) = (1 : ℂ)
[GOAL]
case h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
⊢ ↑a * ↑d - ↑b * ↑c = 1
[PROOFSTEP]
norm_cast
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
h : ↑a * ↑d - ↑b * ↑c = 1
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
[PROOFSTEP]
field_simp
[GOAL]
case h.h.mk.h
g : SL(2, ℝ)
hc✝ : ↑↑g 1 0 ≠ 0
h_denom✝ : ∀ (z : ℍ), denom (↑toGLPos g) z ≠ 0
a b c d : ℝ
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
h_denom : ↑c * z + ↑d ≠ 0
h_aux : ↑c * ↑d + ↑c * ↑c * z ≠ 0
h : ↑a * ↑d - ↑b * ↑c = 1
⊢ (↑a * z + ↑b) * (↑c * (↑c * ↑d + ↑c * ↑c * z)) = (↑a * (↑c * ↑d + ↑c * ↑c * z) - ↑c) * (↑c * z + ↑d)
[PROOFSTEP]
linear_combination (-(z * (c : ℂ) ^ 2) - c * d) * h
