awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₁ :
  ((↑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:
suffices (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹ by
    simpa [modular_S_smul, coe_specialLinearGroup_apply]
-- 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
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : ¬c = 0
⊢ (↑c : ℂ) ≠ 0

Tactic:
norm_cast
-- 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
⊢ (↑c : ℂ) ≠ 0

Tactic:
replace hc : (c : ℂ) ≠ 0 := by norm_cast
-- 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
z : ℂ
hz : 0 < z.im
hc : (↑c : ℂ) ≠ 0
⊢ (↑c : ℂ) * z + (↑d : ℂ) ≠ 0

Tactic:
simpa using h_denom ⟨z, hz⟩

Premises used: UpperHalfPlane.mk
-- 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
z : ℂ
hz : 0 < z.im
hc : (↑c : ℂ) ≠ 0
⊢ (↑c : ℂ) * z + (↑d : ℂ) ≠ 0

Tactic:
replace h_denom : ↑c * z + d ≠ 0 := by simpa using h_denom ⟨z, hz⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
h : a * d - b * c = 1
z : ℂ
hz : 0 < z.im
hc : (↑c : ℂ) ≠ 0
h_denom : (↑c : ℂ) * z + (↑d : ℂ) ≠ 0
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : a * d - b * c = 1
⊢ (↑a : ℂ) * (↑d : ℂ) - (↑b : ℂ) * (↑c : ℂ) = 1

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
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 : ℂ) * (↑d : ℂ) - (↑b : ℂ) * (↑c : ℂ) = 1

Tactic:
replace h : (a * d - b * c : ℂ) = (1 : ℂ) := by norm_cast
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b c d : ℝ
z : ℂ
hz : 0 < z.im
hc : (↑c : ℂ) ≠ 0
h_denom : (↑c : ℂ) * z + (↑d : ℂ) ≠ 0
h : (↑a : ℂ) * (↑d : ℂ) - (↑b : ℂ) * (↑c : ℂ) = 1
⊢ ((↑a : ℂ) * z + (↑b : ℂ)) / ((↑c : ℂ) * z + (↑d : ℂ)) =
    (↑a : ℂ) / (↑c : ℂ) - ((↑c : ℂ) * (↑d : ℂ) + (↑c : ℂ) * (↑c : ℂ) * z)⁻¹

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ Eq (α := ℝ) (det (n := Fin 2) !![√z.im, z.re / √z.im; 0, 1 / √z.im]) 1

Tactic:
simp [mul_inv_cancel₀ (Real.sqrt_ne_zero'.mpr z.im_pos)]

Premises used: Iff.mpr, UpperHalfPlane.im_pos, mul_inv_cancel₀, Real.sqrt_ne_zero'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ z.toSL2R = Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![√z.im, z.re / √z.im; 0, 1 / √z.im] ⋯

Tactic:
(rfl)

Premises used: UpperHalfPlane.toSL2R, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ (↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) = !![√z.im, z.re / √z.im; 0, 1 / √z.im]

Tactic:
(rfl)

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ (↑√z.im : ℂ) ≠ 0

Tactic:
simpa [Real.sqrt_ne_zero'] using z.im_pos

Premises used: UpperHalfPlane.im_pos, Real.sqrt_ne_zero'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ (↑√z.im : ℂ) ≠ 0

Tactic:
have : √z.im ≠ (0 : ℂ) := by simpa [Real.sqrt_ne_zero'] using z.im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
this : (↑√z.im : ℂ) ≠ 0
coe : (↑(z.toSL2R • I) : ℂ) = (↑z : ℂ)
⊢ z.toSL2R • I = z

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
this_1 : (↑√z.im : ℂ) ≠ 0
this : (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
rw :
  (↑((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) 0 0)) : ℂ) * (↑I : ℂ) +
      (↑((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) 0 1)) : ℂ) =
    (↑z : ℂ) *
      ((↑((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) 1 0)) : ℂ) * (↑I : ℂ) +
        (↑((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) 1 1)) : ℂ))
⊢ (↑(z.toSL2R • I) : ℂ) = (↑z : ℂ)

Tactic:
rw [coe_specialLinearGroup_apply, div_eq_iff (mod_cast denom_ne_zero z.toSL2R I)]

Premises used: div_eq_iff, UpperHalfPlane.coe_specialLinearGroup_apply
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
this_1 : (↑√z.im : ℂ) ≠ 0
this : (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
⊢ (↑((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) 0 0)) : ℂ) * (↑I : ℂ) +
      (↑((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) 0 1)) : ℂ) =
    (↑z : ℂ) *
      ((↑((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) 1 0)) : ℂ) * (↑I : ℂ) +
        (↑((algebraMap ℝ ℝ : (a : ℝ) → ℝ) ((↑z.toSL2R : Matrix (Fin 2) (Fin 2) ℝ) 1 1)) : ℂ))

Tactic:
simpa [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
this : (↑√z.im : ℂ) ≠ 0
coe : (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
⊢ (↑(z.toSL2R • I) : ℂ) = (↑z : ℂ)

Tactic:
suffices z.re / √z.im + √z.im * Complex.I = z * (↑√z.im)⁻¹ by
    rw [coe_specialLinearGroup_apply, div_eq_iff (mod_cast denom_ne_zero z.toSL2R I)]
    simpa [add_comm]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
this : (↑√z.im : ℂ) ≠ 0
coe : ((↑z.re : ℂ) + (↑√z.im : ℂ) * Complex.I * (↑√z.im : ℂ)) / (↑√z.im : ℂ) = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
coe₁ : ((↑z.re : ℂ) + (↑√z.im : ℂ) * (↑√z.im : ℂ) * Complex.I) / (↑√z.im : ℂ) = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
coe₂ : ((↑z.re : ℂ) + (↑(√z.im * √z.im) : ℂ) * Complex.I) / (↑√z.im : ℂ) = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
coe₃ : ((↑z.re : ℂ) + (↑√(z.im * z.im) : ℂ) * Complex.I) / (↑√z.im : ℂ) = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
coe₄ : ((↑z.re : ℂ) + (↑z.im : ℂ) * Complex.I) / (↑√z.im : ℂ) = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
coe₅ : (↑z : ℂ) / (↑√z.im : ℂ) = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
coe₆ coe₇ : (↑z : ℂ) * (↑√z.im : ℂ)⁻¹ = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
⊢ (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹

Tactic:
rw [div_add' (hc := this), mul_right_comm, ← Complex.ofReal_mul, ← Real.sqrt_mul z.im_pos.le,
    Real.sqrt_mul_self z.im_pos.le, re_add_im, div_eq_mul_inv]

Premises used: UpperHalfPlane.im_pos, UpperHalfPlane.re_add_im, Real.sqrt_mul_self, div_add', LT.lt.le, Real.sqrt_mul, Complex.ofReal, div_eq_mul_inv, UpperHalfPlane.im, mul_right_comm, Real.sqrt, Complex.ofReal_mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
⊢ MulAction.IsPretransitive SL(2, ℝ) ℍ

Tactic:
.of_orbit fun z ↦ ⟨_, toSL2R_smul_I z⟩

Premises used: UpperHalfPlane.toSL2R, Exists.intro, MulAction.IsPretransitive.of_orbit, UpperHalfPlane.toSL2R_smul_I
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
⊢ MulAction.IsPretransitive (GL (Fin 2) ℝ) ℍ

Tactic:
.of_smul_eq ((↑) : SL(2, ℝ) → _) fun {g z} ↦ (MulAction.compHom_smul_def _ g z).symm

Premises used: MulAction.IsPretransitive.of_smul_eq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
⊢ Ne (α := ℝ) (det (n := Fin 2) !![-1, 0; 0, 1]) 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
τ : ℍ
⊢ ¬LT.lt (α := ℝ) 1 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
τ : ℍ
⊢ (↑(J • τ) : ℂ) = -(starRingEnd ℂ : (a : ℂ) → ℂ) (↑τ : ℂ)

Tactic:
simp [UpperHalfPlane.coe_smul, σ, J, show ¬(1 : ℝ) < 0 by simp, num, denom]

Premises used: UpperHalfPlane.coe_smul, UpperHalfPlane.denom, UpperHalfPlane.σ, UpperHalfPlane.J, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
⊢ (↑J : Matrix (Fin 2) (Fin 2) ℝ) = !![-1, 0; 0, 1]

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
huv : ∀ (i j : Fin 2), (↑(HPow.hPow (β := ℕ) J 2) : Matrix (Fin 2) (Fin 2) ℝ) i j = (↑1 : Matrix (Fin 2) (Fin 2) ℝ) i j
⊢ HPow.hPow (β := ℕ) J 2 = 1

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
i j : Fin 2
⊢ (↑(HPow.hPow (β := ℕ) J 2) : Matrix (Fin 2) (Fin 2) ℝ) i j = (↑1 : Matrix (Fin 2) (Fin 2) ℝ) i j

Tactic:
simp [J, sq, Matrix.one_fin_two]

Premises used: sq, UpperHalfPlane.J, Matrix.one_fin_two
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
huv : Eq (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) J) : ℝ) (↑(-1) : ℝ)
⊢ Eq (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) J : ℝˣ) (-1 : ℝˣ)

Tactic:
ext
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
⊢ Eq (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) J) : ℝ) (↑(-1) : ℝ)

Tactic:
simp [J]

Premises used: UpperHalfPlane.J
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
⊢ σ J = Complex.conjCAE

Tactic:
simp [σ, J]

Premises used: UpperHalfPlane.σ, UpperHalfPlane.J
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
τ : ℂ
⊢ denom J τ = 1

Tactic:
simp [J, denom]

Premises used: UpperHalfPlane.denom, UpperHalfPlane.J
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : GL (Fin 2) ℝ
τ : ℂ
⊢ denom (J * g) τ = denom g τ

Tactic:
simp [denom, vecMul, vecHead, vecTail]

Premises used: Matrix.vecMul, UpperHalfPlane.denom, Matrix.vecHead, Matrix.vecTail
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : SL(2, ℤ)
⊢ coe a = coe b ↔ a = b

Tactic:
⟨fun h ↦ a.ext b fun i j ↦ ?_, congr_arg _⟩

Premises used: Matrix.SpecialLinearGroup.ext, congr_arg, Iff.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : SL(2, ℤ)
refine : ∀ (h : coe a = coe b) (i j : Fin 2), (↑a : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑b : Matrix (Fin 2) (Fin 2) ℤ) i j
⊢ coe a = coe b ↔ a = b

Tactic:
refine ⟨fun h ↦ a.ext b fun i j ↦ ?_, congr_arg _⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : SL(2, ℤ)
h : coe a = coe b
i j : Fin 2
⊢ ∀ (i j : Fin 2),
    (↑(↑(coe a) : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ) i j =
      (↑(↑(coe b) : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ) i j

Tactic:
simp only [Subtype.ext_iff, GeneralLinearGroup.ext_iff] at h

Premises used: Matrix.GeneralLinearGroup.ext_iff, Subtype.ext_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
a b : SL(2, ℤ)
i j : Fin 2
h :
  ∀ (i j : Fin 2),
    (↑(↑(coe a) : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ) i j =
      (↑(↑(coe b) : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) ℝ) i j
⊢ (↑a : Matrix (Fin 2) (Fin 2) ℤ) i j = (↑b : Matrix (Fin 2) (Fin 2) ℤ) i j

Tactic:
simpa [coe] using h i j

Premises used: ModularGroup.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
⊢ (coeHom : (a : SL(2, ℤ)) → ↥GL(2, ℝ)⁺) g = coe g

Tactic:
rfl

Premises used: rfl, ModularGroup.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
i j : Fin 2
⊢ (↑((↑(↑(coe g) : (Matrix (Fin 2) (Fin 2) ℝ)ˣ) : Matrix (Fin 2) (Fin 2) ℝ) i j) : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) i j) : ℂ)

Tactic:
rfl

Premises used: Matrix.map, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
⊢ (↑(↑(coe g) : (Matrix (Fin 2) (Fin 2) ℝ)ˣ) : Matrix (Fin 2) (Fin 2) ℝ).det = 1

Tactic:
simp only [SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, SpecialLinearGroup.det_coe, coe]

Premises used: Matrix.SpecialLinearGroup.det_coe, Matrix.SpecialLinearGroup.coe_GLPos_coe_GL_coe_matrix, ModularGroup.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
⊢ coe 1 = 1

Tactic:
simp only [coe, map_one]

Premises used: map_one, ModularGroup.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
s : SL(2, ℤ)
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ (s • g) • z =
    HMul.hMul (α := ↥GL(2, ℝ)⁺)
        ((toGLPos : (a : SL(2, ℝ)) → ↥GL(2, ℝ)⁺)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) s) :
          ↥GL(2, ℝ)⁺)
        g •
      z

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
s : SL(2, ℤ)
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ HMul.hMul (α := ↥GL(2, ℝ)⁺)
        ((toGLPos : (a : SL(2, ℝ)) → ↥GL(2, ℝ)⁺)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) s) :
          ↥GL(2, ℝ)⁺)
        g •
      z =
    s • g • z

Tactic:
apply mul_smul'

Premises used: UpperHalfPlane.mul_smul'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
z : ℍ
⊢ g • z =
    HSMul.hSMul (α := GL (Fin 2) ℝ)
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
          ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g) :
        GL (Fin 2) ℝ)
      z

Tactic:
rfl

Premises used: UpperHalfPlane.smulAux, SMul.comp.smul, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
z : ℍ
rw :
  HSMul.hSMul (α := GL (Fin 2) ℝ)
      (-(toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-g)) :
        GL (Fin 2) ℝ)
      z =
    g • z
⊢ -g • z = g • z

Tactic:
rw [sl_moeb, ← z.neg_smul]

Premises used: ModularGroup.sl_moeb, UpperHalfPlane.neg_smul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
z : ℍ
e_a :
  ∀ (i j : Fin 2),
    Eq (α := ℝ)
      ((↑(-(toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
                ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-g))) :
          Matrix (Fin 2) (Fin 2) ℝ)
        i j)
      ((↑((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g) : Matrix (Fin 2) (Fin 2) ℝ) i j)
⊢ HSMul.hSMul (α := GL (Fin 2) ℝ)
      (-(toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
            ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-g)) :
        GL (Fin 2) ℝ)
      z =
    g • z

Tactic:
congr 1 with i j
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
z : ℍ
i j : Fin 2
⊢ Eq (α := ℝ)
    ((↑(-(toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) (-g))) :
        Matrix (Fin 2) (Fin 2) ℝ)
      i j)
    ((↑((mapGL ℝ : (a : SL(2, ℤ)) → GL (Fin 2) ℝ) g) : Matrix (Fin 2) (Fin 2) ℝ) i j)

Tactic:
simp [toGL]

Premises used: Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
z : ℍ
⊢ (g • z).im =
    HDiv.hDiv (β := ℝ) z.im
      ((Complex.normSq : (a : ℂ) → ℝ)
          (denom
            ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
              ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
            (↑z : ℂ)) :
        ℝ)

Tactic:
simpa using z.im_smul_eq_div_normSq g

Premises used: Real, UpperHalfPlane.im_smul_eq_div_normSq, Matrix.SpecialLinearGroup.map, Int.castRingHom, DFunLike.coe, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
g : SL(2, ℤ)
z : ℍ
⊢ denom
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) g))
      (↑z : ℂ) =
    (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑g : Matrix (Fin 2) (Fin 2) ℤ) 1 1) : ℂ)

Tactic:
rfl

Premises used: UpperHalfPlane.denom, Matrix.map, rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Goal:
z : ℍ
⊢ denom
      ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ)
        ((SpecialLinearGroup.map (Int.castRingHom ℝ) : (a : SL(2, ℤ)) → SL(2, ℝ)) S))
      (↑z : ℂ) =
    (↑z : ℂ)

Tactic:
simp [S, denom_apply]

Premises used: ModularGroup.denom_apply, ModularGroup.S
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
⊢ Continuous
    (Function.HasUncurry.uncurry (α := (g : GL (Fin 2) ℝ) → (z : ℂ) → ℂ) fun (g : GL (Fin 2) ℝ) (z : ℂ) ↦
      (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * z + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
⊢ Continuous
    (Function.HasUncurry.uncurry (α := (g : GL (Fin 2) ℝ) → (z : ℂ) → ℂ) fun (g : GL (Fin 2) ℝ) (z : ℂ) ↦
      (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * z + (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ))

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
apply : Continuous (Subtype.val (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) ∘ toSL2R)
⊢ Continuous toSL2R

Tactic:
apply continuous_induced_rng.mpr

Premises used: Iff.mpr, continuous_induced_rng
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
⊢ ∀ (x : ℍ), √x.im ≠ 0

Tactic:
grind [im_pos]

Premises used: UpperHalfPlane.im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
funProp funProp₁ : ∀ (x : ℍ), √x.im ≠ 0
⊢ Continuous (Y := Matrix (Fin 2) (Fin 2) ℝ) fun (x : ℍ) ↦ !![√x.im, x.re / √x.im; 0, 1 / √x.im]

Tactic:
fun_prop (disch := grind [im_pos])

Premises used: UpperHalfPlane.im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
this :
  ∀ (g : SL(2, ℝ)) (τ : ℍ),
    ContinuousAt (Y := ℂ)
      (fun (x : SL(2, ℝ) × ℍ) ↦
        match (motive := SL(2, ℝ) × ℍ → ℂ) x with
        | (h, z) =>
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
            ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)))
      (g, τ)
⊢ Continuous (Y := ℍ) fun (p : SL(2, ℝ) × ℍ) ↦ p.1 • p.2

Tactic:
simpa [continuous_induced_rng, continuous_iff_continuousAt, Function.comp_def,
        coe_specialLinearGroup_apply]

Premises used: Function.comp_def, UpperHalfPlane.coe_specialLinearGroup_apply, continuous_iff_continuousAt, continuous_induced_rng
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
suffices :
  ∀ (g : SL(2, ℝ)) (τ : ℍ),
    ContinuousAt (Y := ℂ)
      (fun (x : SL(2, ℝ) × ℍ) ↦
        match (motive := SL(2, ℝ) × ℍ → ℂ) x with
        | (h, z) =>
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
            ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)))
      (g, τ)
⊢ Continuous (Y := ℍ) fun (p : SL(2, ℝ) × ℍ) ↦ p.1 • p.2

Tactic:
suffices ∀ (g : SL(2, ℝ)) (τ : ℍ),
        ContinuousAt (fun ⟨h, z⟩ ↦ (h 0 0 * (z : ℂ) + h 0 1) / (h 1 0 * z + h 1 1)) (g, τ) by
      simpa [continuous_induced_rng, continuous_iff_continuousAt, Function.comp_def,
        coe_specialLinearGroup_apply]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : SL(2, ℝ)
τ : ℍ
⊢ (↑((↑(g, τ).1 : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑(g, τ).2 : ℂ) +
      (↑((↑(g, τ).1 : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) ≠
    0

Tactic:
denom_ne_zero g τ

Premises used: UpperHalfPlane.denom, DFunLike.coe, UpperHalfPlane.denom_ne_zero, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : SL(2, ℝ)
τ : ℍ
⊢ (↑((↑(g, τ).1 : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑(g, τ).2 : ℂ) +
      (↑((↑(g, τ).1 : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) ≠
    0

Tactic:
exact denom_ne_zero g τ

Premises used: DFunLike.coe, UpperHalfPlane.denom_ne_zero, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : SL(2, ℝ)
τ : ℍ
funProp :
  (↑((↑(g, τ).1 : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑(g, τ).2 : ℂ) +
      (↑((↑(g, τ).1 : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) ≠
    0
⊢ ContinuousAt (Y := ℂ)
    (fun (x : SL(2, ℝ) × ℍ) ↦
      match (motive := SL(2, ℝ) × ℍ → ℂ) x with
      | (h, z) =>
        ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) /
          ((↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ) * (↑z : ℂ) + (↑((↑h : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ)))
    (g, τ)

Tactic:
fun_prop (disch := exact denom_ne_zero g τ)

Premises used: DFunLike.coe, UpperHalfPlane.denom_ne_zero, Matrix.SpecialLinearGroup.toGL
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
pos :
  ∀ (hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
neg :
  ∀ (hg : ¬LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)),
    σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g

Tactic:
by_cases hg : 0 < g.det.val

Premises used: Units.val, Matrix.GeneralLinearGroup.det, DFunLike.coe
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
this : {h : GL (Fin 2) ℝ | LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g
h : GL (Fin 2) ℝ
hh : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)
⊢ σ h = σ g

Tactic:
simp only [σ, hh, ↓reduceIte, hg]

Premises used: reduceIte, UpperHalfPlane.σ
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
this : {h : GL (Fin 2) ℝ | LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g
h :
  ∀ (a : GL (Fin 2) ℝ),
    Membership.mem (γ := Set (GL (Fin 2) ℝ))
      {x : GL (Fin 2) ℝ |
        Membership.mem (γ := Set (GL (Fin 2) ℝ))
            {h : GL (Fin 2) ℝ | LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)}
            x →
          Membership.mem (γ := Set (GL (Fin 2) ℝ))
            {x : GL (Fin 2) ℝ | (fun (x : GL (Fin 2) ℝ) ↦ σ x = (fun (x : GL (Fin 2) ℝ) ↦ σ g) x) x} x}
      a
h₁ h₂ :
  ∀ (h : GL (Fin 2) ℝ) (hh : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)),
    σ h = σ g
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g

Tactic:
filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
pos : {h : GL (Fin 2) ℝ | LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) h) : ℝ)} ∈ 𝓝 g
⊢ σ =ᶠ[𝓝 g] fun (x : GL (Fin 2) ℝ) ↦ σ g

Tactic:
suffices {h | 0 < h.det.val} ∈ 𝓝 g by
      filter_upwards [this] with h hh using by simp only [σ, hh, ↓reduceIte, hg]