awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℝ
g : SL(2, R)
z : ℍ
rw :
  num (((mapGL ℝ : SL(2, R) →* GL (Fin 2) ℝ) : (a : SL(2, R)) → GL (Fin 2) ℝ) g) (↑z : ℂ) /
      denom (((mapGL ℝ : SL(2, R) →* GL (Fin 2) ℝ) : (a : SL(2, R)) → GL (Fin 2) ℝ) g) (↑z : ℂ) =
    ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
      ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ))
⊢ (↑(g • z) : ℂ) =
    ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
      ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ))

Tactic:
rw [MulAction.compHom_smul_def, coe_smul_of_det_pos (by simp)]

Premises used: MulAction.compHom_smul_def, UpperHalfPlane.coe_smul_of_det_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ num (((mapGL ℝ : SL(2, R) →* GL (Fin 2) ℝ) : (a : SL(2, R)) → GL (Fin 2) ℝ) g) (↑z : ℂ) /
      denom (((mapGL ℝ : SL(2, R) →* GL (Fin 2) ℝ) : (a : SL(2, R)) → GL (Fin 2) ℝ) g) (↑z : ℂ) =
    ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
      ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ))

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℝ
g : SL(2, R)
z : ℍ
coe :
  (↑(g • z) : ℂ) =
    (↑{
          coe :=
            ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
                (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
              ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
                (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ)),
          coe_im_pos := ⋯ } :
      ℂ)
⊢ g • z =
    {
      coe :=
        ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
          ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ)),
      coe_im_pos := ⋯ }

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Algebra R ℝ
g : SL(2, R)
z : ℍ
⊢ (↑(g • z) : ℂ) =
    (↑{
          coe :=
            ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 0)) : ℂ) * (↑z : ℂ) +
                (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 0 1)) : ℂ)) /
              ((↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0)) : ℂ) * (↑z : ℂ) +
                (↑((algebraMap R ℝ : (a : R) → ℝ) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)) : ℂ)),
          coe_im_pos := ⋯ } :
      ℂ)

Tactic:
simp [coe_specialLinearGroup_apply]

Premises used: UpperHalfPlane.coe_specialLinearGroup_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
rw :
  {
      coe :=
        ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
          ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)),
      coe_im_pos := ⋯ : ℍ } =
    { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ }
⊢ ModularGroup.S • z = { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ }

Tactic:
rw [specialLinearGroup_apply]

Premises used: UpperHalfPlane.specialLinearGroup_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ {
      coe :=
        ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
          ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
            (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑ModularGroup.S : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)),
      coe_im_pos := ⋯ : ℍ } =
    { coe := (-(↑z : ℂ))⁻¹, coe_im_pos := ⋯ }

Tactic:
simp [ModularGroup.S, neg_div, inv_neg]

Premises used: neg_div, inv_neg, ModularGroup.S
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
n : ℤ
rw :
  ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
      ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)) =
    (↑z : ℂ) + (↑(↑n : ℝ) : ℂ)
⊢ ModularGroup.T ^ n • z = HVAdd.hVAdd (α := ℝ) (↑n : ℝ) z

Tactic:
rw [UpperHalfPlane.ext_iff, coe_vadd, add_comm, coe_specialLinearGroup_apply]

Premises used: UpperHalfPlane.ext_iff, add_comm, UpperHalfPlane.coe_specialLinearGroup_apply, UpperHalfPlane.coe_vadd
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
n : ℤ
⊢ ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 0 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 0 1)) : ℂ)) /
      ((↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 1 0)) : ℂ) * (↑z : ℂ) +
        (↑((algebraMap ℤ ℝ : (a : ℤ) → ℝ) ((↑(ModularGroup.T ^ n) : Matrix (Fin 2) (Fin 2) ℤ) 1 1)) : ℂ)) =
    (↑z : ℂ) + (↑(↑n : ℝ) : ℂ)

Tactic:
simp [ModularGroup.coe_T_zpow,
    of_apply, cons_val_zero, Complex.ofReal_one, one_mul, cons_val_one,
    zero_mul, zero_add, div_one]

Premises used: MulZeroClass.zero_mul, Matrix.cons_val_one, Matrix.cons_val_zero, Complex.ofReal_one, Matrix.of_apply, zero_add, ModularGroup.coe_T_zpow, div_one, one_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ ModularGroup.T • z = HVAdd.hVAdd (α := ℝ) 1 z

Tactic:
simpa only [zpow_one, Int.cast_one] using modular_T_zpow_smul z 1

Premises used: zpow_one, UpperHalfPlane.modular_T_zpow_smul, OfNat.ofNat, Int.cast_one
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℝ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
obtain :
  ∀ (a b : ℝ) (ha : a ≠ 0)
    (hc :
      Eq (α := ℝ)
        ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯) :
              Matrix (Fin 2) (Fin 2) ℝ)
            1 0 :
          ℝ)
        (0 : ℝ)),
    ∃ (u : { x : ℝ // 0 < x }) (v : ℝ),
      Eq (α := ℍ → ℍ)
        (fun (x : ℍ) ↦
          HSMul.hSMul (α := SL(2, ℝ))
            (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
              { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
            x)
        ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
⊢ ∃ (u : { x : ℝ // 0 < x }) (v : ℝ),
    Eq (α := ℍ → ℍ) (fun (x : ℍ) ↦ g • x) ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

Tactic:
obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc

Premises used: Matrix.SpecialLinearGroup.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : ℝ
ha : a ≠ 0
hc :
  Eq (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯) : Matrix (Fin 2) (Fin 2) ℝ)
        1 0 :
      ℝ)
    (0 : ℝ)
⊢ ∃ (u : { x : ℝ // 0 < x }) (v : ℝ),
    Eq (α := ℍ → ℍ)
      (fun (x : ℍ) ↦
        HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          x)
      ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

Tactic:
⟨⟨_, mul_self_pos.mpr ha⟩, b * a, ?_⟩

Premises used: Iff.mpr, HMul.hMul, mul_self_pos, Subtype.mk, Exists.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : ℝ
ha : a ≠ 0
hc :
  Eq (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯) : Matrix (Fin 2) (Fin 2) ℝ)
        1 0 :
      ℝ)
    (0 : ℝ)
refine :
  Eq (α := ℍ → ℍ)
    (fun (x : ℍ) ↦
      HSMul.hSMul (α := SL(2, ℝ))
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
          { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
        x)
    ((fun (x : ℍ) ↦ b * a +ᵥ x) ∘ fun (x : ℍ) ↦
      HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (a * a) ⋯) x)
⊢ ∃ (u : { x : ℝ // 0 < x }) (v : ℝ),
    Eq (α := ℍ → ℍ)
      (fun (x : ℍ) ↦
        HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          x)
      ((fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

Tactic:
refine ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : ℝ
ha : a ≠ 0
hc :
  Eq (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯) : Matrix (Fin 2) (Fin 2) ℝ)
        1 0 :
      ℝ)
    (0 : ℝ)
h :
  ∀ (z : ℂ) (hz : 0 < z.im),
    HSMul.hSMul (α := SL(2, ℝ))
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
          { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
        { coe := z, coe_im_pos := hz : ℍ } =
      ((fun (x : ℍ) ↦ b * a +ᵥ x) ∘ fun (x : ℍ) ↦
          HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (a * a) ⋯) x)
        { coe := z, coe_im_pos := hz : ℍ }
⊢ Eq (α := ℍ → ℍ)
    (fun (x : ℍ) ↦
      HSMul.hSMul (α := SL(2, ℝ))
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
          { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
        x)
    ((fun (x : ℍ) ↦ b * a +ᵥ x) ∘ fun (x : ℍ) ↦
      HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (a * a) ⋯) x)

Tactic:
ext1 ⟨z, hz⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : ℝ
ha : a ≠ 0
hc :
  Eq (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯) : Matrix (Fin 2) (Fin 2) ℝ)
        1 0 :
      ℝ)
    (0 : ℝ)
z : ℂ
hz : 0 < z.im
h :
  (↑(HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ) =
    (↑(((fun (x : ℍ) ↦ b * a +ᵥ x) ∘ fun (x : ℍ) ↦
            HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (a * a) ⋯) x)
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ)
⊢ HSMul.hSMul (α := SL(2, ℝ))
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
        { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
      { coe := z, coe_im_pos := hz : ℍ } =
    ((fun (x : ℍ) ↦ b * a +ᵥ x) ∘ fun (x : ℍ) ↦
        HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (a * a) ⋯) x)
      { coe := z, coe_im_pos := hz : ℍ }

Tactic:
ext1
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : ℝ
ha : a ≠ 0
hc :
  Eq (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯) : Matrix (Fin 2) (Fin 2) ℝ)
        1 0 :
      ℝ)
    (0 : ℝ)
z : ℂ
hz : 0 < z.im
this : (↑a : ℂ) * z * (↑a : ℂ) + (↑b : ℂ) * (↑a : ℂ) = (↑b : ℂ) * (↑a : ℂ) + (↑a : ℂ) * (↑a : ℂ) * z
⊢ (↑(HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ) =
    (↑(((fun (x : ℍ) ↦ b * a +ᵥ x) ∘ fun (x : ℍ) ↦
            HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (a * a) ⋯) x)
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ)

Tactic:
simpa [specialLinearGroup_apply, add_mul]

Premises used: add_mul, UpperHalfPlane.specialLinearGroup_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : ℝ
ha : a ≠ 0
hc :
  Eq (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯) : Matrix (Fin 2) (Fin 2) ℝ)
        1 0 :
      ℝ)
    (0 : ℝ)
z : ℂ
hz : 0 < z.im
h : (↑a : ℂ) * z * (↑a : ℂ) + (↑b : ℂ) * (↑a : ℂ) = (↑b : ℂ) * (↑a : ℂ) + (↑a : ℂ) * (↑a : ℂ) * z
⊢ (↑(HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ) =
    (↑(((fun (x : ℍ) ↦ b * a +ᵥ x) ∘ fun (x : ℍ) ↦
            HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (a * a) ⋯) x)
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ)

Tactic:
suffices ↑a * z * a + b * a = b * a + a * a * z by simpa [specialLinearGroup_apply, add_mul]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : ℝ
ha : a ≠ 0
hc :
  Eq (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] ⋯) : Matrix (Fin 2) (Fin 2) ℝ)
        1 0 :
      ℝ)
    (0 : ℝ)
z : ℂ
hz : 0 < z.im
⊢ (↑a : ℂ) * z * (↑a : ℂ) + (↑b : ℂ) * (↑a : ℂ) = (↑b : ℂ) * (↑a : ℂ) + (↑a : ℂ) * (↑a : ℂ) * z

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℝ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ ∀ (z : ℍ), denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) g) (↑z : ℂ) ≠ 0

Tactic:
have h_denom (z : ℍ) := denom_ne_zero g z
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
hc :
  Ne (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 1
        0 :
      ℝ)
    (0 : ℝ)
h_denom :
  ∀ (z : ℍ),
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯))
        (↑z : ℂ) ≠
      0
⊢ ∃ (u : { x : ℝ // 0 < x }) (v : ℝ) (w : ℝ),
    Eq (α := ℍ → ℍ)
      (fun (x : ℍ) ↦
        HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          x)
      ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

Tactic:
?_
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℝ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
h_denom : ∀ (z : ℍ), denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) g) (↑z : ℂ) ≠ 0
h :
  ∀ (a b c d : ℝ) (h : a * d - b * c = 1)
    (hc :
      Ne (α := ℝ)
        ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯) :
              Matrix (Fin 2) (Fin 2) ℝ)
            1 0 :
          ℝ)
        (0 : ℝ))
    (h_denom :
      ∀ (z : ℍ),
        denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯))
            (↑z : ℂ) ≠
          0),
    ∃ (u : { x : ℝ // 0 < x }) (v : ℝ) (w : ℝ),
      Eq (α := ℍ → ℍ)
        (fun (x : ℍ) ↦
          HSMul.hSMul (α := SL(2, ℝ))
            (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
              { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
            x)
        ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)
⊢ ∃ (u : { x : ℝ // 0 < x }) (v : ℝ) (w : ℝ),
    Eq (α := ℍ → ℍ) (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 => ?_

Premises used: Matrix.SpecialLinearGroup.fin_two_induction
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
hc :
  Ne (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 1
        0 :
      ℝ)
    (0 : ℝ)
h_denom :
  ∀ (z : ℍ),
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯))
        (↑z : ℂ) ≠
      0
⊢ c ≠ 0

Tactic:
simpa using hc
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
hc :
  Ne (α := ℝ)
    ((↑(Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 1
        0 :
      ℝ)
    (0 : ℝ)
h_denom :
  ∀ (z : ℍ),
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯))
        (↑z : ℂ) ≠
      0
⊢ c ≠ 0

Tactic:
replace hc : c ≠ 0 := by simpa using hc
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯))
        (↑z : ℂ) ≠
      0
hc : c ≠ 0
⊢ ∃ (u : { x : ℝ // 0 < x }) (v : ℝ) (w : ℝ),
    Eq (α := ℍ → ℍ)
      (fun (x : ℍ) ↦
        HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          x)
      ((fun (x : ℍ) ↦ w +ᵥ x) ∘ (fun (x : ℍ) ↦ ModularGroup.S • x) ∘ (fun (x : ℍ) ↦ v +ᵥ x) ∘ fun (x : ℍ) ↦ u • x)

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

Premises used: Iff.mpr, HMul.hMul, HDiv.hDiv, mul_self_pos, Subtype.mk, Exists.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯))
        (↑z : ℂ) ≠
      0
hc : c ≠ 0
h₁ :
  Eq (α := ℍ → ℍ)
    (fun (x : ℍ) ↦
      HSMul.hSMul (α := SL(2, ℝ))
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
          { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
        x)
    ((fun (x : ℍ) ↦ a / c +ᵥ x) ∘
      (fun (x : ℍ) ↦ ModularGroup.S • x) ∘
        (fun (x : ℍ) ↦ c * d +ᵥ x) ∘ fun (x : ℍ) ↦
          HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (c * c) ⋯) x)
⊢ ∃ (u : { x : ℝ // 0 < x }) (v : ℝ) (w : ℝ),
    Eq (α := ℍ → ℍ)
      (fun (x : ℍ) ↦
        HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          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, ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯))
        (↑z : ℂ) ≠
      0
hc : c ≠ 0
h₁ :
  ∀ (z : ℂ) (hz : 0 < z.im),
    HSMul.hSMul (α := SL(2, ℝ))
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
          { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
        { coe := z, coe_im_pos := hz : ℍ } =
      ((fun (x : ℍ) ↦ a / c +ᵥ x) ∘
          (fun (x : ℍ) ↦ ModularGroup.S • x) ∘
            (fun (x : ℍ) ↦ c * d +ᵥ x) ∘ fun (x : ℍ) ↦
              HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (c * c) ⋯) x)
        { coe := z, coe_im_pos := hz : ℍ }
⊢ Eq (α := ℍ → ℍ)
    (fun (x : ℍ) ↦
      HSMul.hSMul (α := SL(2, ℝ))
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
          { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
        x)
    ((fun (x : ℍ) ↦ a / c +ᵥ x) ∘
      (fun (x : ℍ) ↦ ModularGroup.S • x) ∘
        (fun (x : ℍ) ↦ c * d +ᵥ x) ∘ fun (x : ℍ) ↦
          HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (c * c) ⋯) x)

Tactic:
ext1 ⟨z, hz⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯))
        (↑z : ℂ) ≠
      0
hc : c ≠ 0
z : ℂ
hz : 0 < z.im
h₁ :
  (↑(HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ) =
    (↑(((fun (x : ℍ) ↦ a / c +ᵥ x) ∘
            (fun (x : ℍ) ↦ ModularGroup.S • x) ∘
              (fun (x : ℍ) ↦ c * d +ᵥ x) ∘ fun (x : ℍ) ↦
                HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (c * c) ⋯) x)
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ)
⊢ HSMul.hSMul (α := SL(2, ℝ))
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
        { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
      { coe := z, coe_im_pos := hz : ℍ } =
    ((fun (x : ℍ) ↦ a / c +ᵥ x) ∘
        (fun (x : ℍ) ↦ ModularGroup.S • x) ∘
          (fun (x : ℍ) ↦ c * d +ᵥ x) ∘ fun (x : ℍ) ↦
            HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (c * c) ⋯) x)
      { coe := z, coe_im_pos := hz : ℍ }

Tactic:
ext1
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
h_denom :
  ∀ (z : ℍ),
    denom
        ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![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)⁻¹
⊢ (↑(HSMul.hSMul (α := SL(2, ℝ))
          (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] ⋯ :
            { A : Matrix (Fin 2) (Fin 2) ℝ // A.det = 1 })
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ) =
    (↑(((fun (x : ℍ) ↦ a / c +ᵥ x) ∘
            (fun (x : ℍ) ↦ ModularGroup.S • x) ∘
              (fun (x : ℍ) ↦ c * d +ᵥ x) ∘ fun (x : ℍ) ↦
                HSMul.hSMul (α := { x : ℝ // 0 < x }) (Subtype.mk (p := fun (x : ℝ) ↦ 0 < x) (c * c) ⋯) x)
          { coe := z, coe_im_pos := hz : ℍ }) :
      ℂ)

Tactic:
simpa [modular_S_smul, coe_specialLinearGroup_apply]

Premises used: UpperHalfPlane.modular_S_smul, UpperHalfPlane.coe_specialLinearGroup_apply