-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem exists_SL2_smul_eq_of_apply_zero_one_ne_zero (g : SL(2, ℝ)) (hc : g 1 0 ≠ 0) :
    ∃ (u : { x : ℝ // 0 < x }) (v w : ℝ),
      (g • · : ℍ → ℍ) =
        (w +ᵥ ·) ∘ (ModularGroup.S • · : ℍ → ℍ) ∘ (v +ᵥ · : ℍ → ℍ) ∘ (u • · : ℍ → ℍ)

Proof state:
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑c ≠ 0

Tactic:
norm_cast

Result:
no goals

Proof state:
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

Tactic:
exact mul_ne_zero hc h_denom

Result:
no goals

Proof state:
case h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
⊢ ∃ u v w,
    (fun x => ⟨!![a, b; c, d], ⋯⟩ • x) =
      (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x

Tactic:
refine ⟨⟨_, mul_self_pos.mpr hc⟩, c * d, a / c, ?_⟩

Result:
case h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
⊢ (fun x => ⟨!![a, b; c, d], ⋯⟩ • x) =
    (fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x

Proof state:
case h
a b c d : ℝ
h : a * d - b * c = 1
hc : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
⊢ ∃ u v w,
    (fun x => ⟨!![a, b; c, d], ⋯⟩ • x) =
      (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x

Tactic:
replace hc : c ≠ 0 := by simpa using hc

Result:
case h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
⊢ ∃ u v w,
    (fun x => ⟨!![a, b; c, d], ⋯⟩ • x) =
      (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x

Proof state:
case h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
⊢ (fun x => ⟨!![a, b; c, d], ⋯⟩ • x) =
    (fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x

Tactic:
ext1 ⟨z, hz⟩

Result:
case h.h.mk
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ⟨!![a, b; c, d], ⋯⟩ • ⟨z, hz⟩ =
    ((fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x) ⟨z, hz⟩

Proof state:
a b c d : ℝ
h : a * d - b * c = 1
hc : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
⊢ c ≠ 0

Tactic:
simpa using hc

Result:
no goals

Proof state:
case h.h.mk.h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
z : ℂ
hz : 0 < z.im
hc : ↑c ≠ 0
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹

Tactic:
replace h_denom : ↑c * z + d ≠ 0 := by simpa using h_denom ⟨z, hz⟩

Result:
case h.h.mk.h
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)⁻¹

Proof state:
g : SL(2, ℝ)
hc : ↑g 1 0 ≠ 0
⊢ ∃ u v w, (fun x => g • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x

Tactic:
have h_denom := denom_ne_zero g

Result:
g : SL(2, ℝ)
hc : ↑g 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (toGLPos g) z ≠ 0
⊢ ∃ u v w, (fun x => g • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x

Proof state:
case h.h.mk
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ⟨!![a, b; c, d], ⋯⟩ • ⟨z, hz⟩ =
    ((fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x) ⟨z, hz⟩

Tactic:
ext1

Result:
case h.h.mk.h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑(⟨!![a, b; c, d], ⋯⟩ • ⟨z, hz⟩) =
    ↑(((fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x) ⟨z, hz⟩)

Proof state:
case h.h.mk.h
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)

Tactic:
linear_combination (-(z * (c : ℂ) ^ 2) - c * d) * h

Result:
no goals

Proof state:
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

Tactic:
rw [mul_assoc, ← mul_add, add_comm]

Result:
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

Proof state:
case h.h.mk.h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ ↑(⟨!![a, b; c, d], ⋯⟩ • ⟨z, hz⟩) =
    ↑(((fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x) ⟨z, hz⟩)

Tactic:
suffices (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹ by
  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]

Result:
case h.h.mk.h
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
⊢ (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹

Proof state:
a b c d : ℝ
h : a * d - b * c = 1
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
this : (↑a * z + ↑b) / (↑c * z + ↑d) = ↑a / ↑c - (↑c * ↑d + ↑c * ↑c * z)⁻¹
⊢ ↑(⟨!![a, b; c, d], ⋯⟩ • ⟨z, hz⟩) =
    ↑(((fun x => a / c +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => c * d +ᵥ x) ∘ fun x => ⟨c * c, ⋯⟩ • x) ⟨z, hz⟩)

Tactic:
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]

Result:
no goals

Proof state:
case h.h.mk.h
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)⁻¹

Tactic:
have h_aux : (c : ℂ) * d + ↑c * ↑c * z ≠ 0 := by
  rw [mul_assoc, ← mul_add, add_comm]
  exact mul_ne_zero hc h_denom

Result:
case h.h.mk.h
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)⁻¹

Proof state:
g : SL(2, ℝ)
hc : ↑g 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (toGLPos g) z ≠ 0
⊢ ∃ u v w, (fun x => g • x) = (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x

Tactic:
induction' g using Matrix.SpecialLinearGroup.fin_two_induction with a b c d h

Result:
case h
a b c d : ℝ
h : a * d - b * c = 1
hc : ↑⟨!![a, b; c, d], ⋯⟩ 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom (toGLPos ⟨!![a, b; c, d], ⋯⟩) z ≠ 0
⊢ ∃ u v w,
    (fun x => ⟨!![a, b; c, d], ⋯⟩ • x) =
      (fun x => w +ᵥ x) ∘ (fun x => ModularGroup.S • x) ∘ (fun x => v +ᵥ x) ∘ fun x => u • x

Proof state:
case h.h.mk.h
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)⁻¹

Tactic:
field_simp

Result:
case h.h.mk.h
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)