awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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)
have 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⁻¹] sorry :
        { 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) sorry) x)
Tactic: refine ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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 : ℝ)
⊢ 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)
have 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⁻¹] sorry :
        { 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) sorry) x)
      { coe := z, coe_im_pos := hz : ℍ }
Tactic: ext1 ⟨z, hz⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ 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 : ℍ }
have h : (↑(HSMul.hSMul (α := SL(2, ℝ))
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; 0, a⁻¹] sorry :
          { 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) sorry) x)
        { coe := z, coe_im_pos := hz : ℍ }) :
    ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ (↑(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 : ℍ }) :
      ℂ)
have h : (↑a : ℂ) * z * (↑a : ℂ) + (↑b : ℂ) * (↑a : ℂ) = (↑b : ℂ) * (↑a : ℂ) + (↑a : ℂ) * (↑a : ℂ) * z
Tactic: suffices ↑a * z * a + b * a = b * a + a * a * z by simpa [specialLinearGroup_apply, add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
Goal:
g : SL(2, ℝ)
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ ∃ (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)
have h_denom : ∀ (z : ℍ), denom ((toGL : (a : SL(2, ℝ)) → GL (Fin 2) ℝ) g) (↑z : ℂ) ≠ 0
Tactic: have h_denom (z : ℍ) := denom_ne_zero g z
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ ∃ (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)
have 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] sorry) : 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] sorry))
          (↑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] sorry :
            { 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: induction g using Matrix.SpecialLinearGroup.fin_two_induction with | _ a b c d h => ?_
Cleared hypotheses: g, hc, h_denom
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
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)
have hc₁ : c ≠ 0
Tactic: replace hc : c ≠ 0 := by simpa using hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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)
have 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] sorry :
        { 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) sorry) x)
Tactic: refine ⟨⟨_, mul_self_pos.mpr hc⟩, c * d, a / c, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ 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)
have 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] sorry :
        { 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) sorry) x)
      { coe := z, coe_im_pos := hz : ℍ }
Tactic: ext1 ⟨z, hz⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ 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 : ℍ }
have h₁ : (↑(HSMul.hSMul (α := SL(2, ℝ))
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) !![a, b; c, d] sorry :
          { 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) sorry) x)
        { coe := z, coe_im_pos := hz : ℍ }) :
    ℂ)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
⊢ (↑(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 : ℍ }) :
      ℂ)
have h₁ : ((↑a : ℂ) * z + (↑b : ℂ)) / ((↑c : ℂ) * z + (↑d : ℂ)) =
  (↑a : ℂ) / (↑c : ℂ) - ((↑c : ℂ) * (↑d : ℂ) + (↑c : ℂ) * (↑c : ℂ) * z)⁻¹
Tactic: suffices (↑a * z + b) / (↑c * z + d) = a / c - (c * d + ↑c * ↑c * z)⁻¹ by
    simpa [modular_S_smul, coe_specialLinearGroup_apply]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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
have norm_cast : ¬c = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
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
⊢ ((↑a : ℂ) * z + (↑b : ℂ)) / ((↑c : ℂ) * z + (↑d : ℂ)) =
    (↑a : ℂ) / (↑c : ℂ) - ((↑c : ℂ) * (↑d : ℂ) + (↑c : ℂ) * (↑c : ℂ) * z)⁻¹
have hc₁ : (↑c : ℂ) ≠ 0
Tactic: replace hc : (c : ℂ) ≠ 0 := by norm_cast
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
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
⊢ ((↑a : ℂ) * z + (↑b : ℂ)) / ((↑c : ℂ) * z + (↑d : ℂ)) =
    (↑a : ℂ) / (↑c : ℂ) - ((↑c : ℂ) * (↑d : ℂ) + (↑c : ℂ) * (↑c : ℂ) * z)⁻¹
have h_denom₁ : (↑c : ℂ) * z + (↑d : ℂ) ≠ 0
Tactic: replace h_denom : ↑c * z + d ≠ 0 := by simpa using h_denom ⟨z, hz⟩
Cleared hypotheses: h_denom
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
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 : ℂ) * z + (↑b : ℂ)) / ((↑c : ℂ) * z + (↑d : ℂ)) =
    (↑a : ℂ) / (↑c : ℂ) - ((↑c : ℂ) * (↑d : ℂ) + (↑c : ℂ) * (↑c : ℂ) * z)⁻¹
have h₁ : (↑a : ℂ) * (↑d : ℂ) - (↑b : ℂ) * (↑c : ℂ) = 1
Tactic: replace h : (a * d - b * c : ℂ) = (1 : ℂ) := by norm_cast
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
Goal:
z : ℍ
⊢ z.toSL2R • I = z
have this : (↑√z.im : ℂ) ≠ 0
Tactic: have : √z.im ≠ (0 : ℂ) := by simpa [Real.sqrt_ne_zero'] using z.im_pos
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
z : ℍ
this : (↑√z.im : ℂ) ≠ 0
⊢ z.toSL2R • I = z
have coe : (↑(z.toSL2R • I) : ℂ) = (↑z : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
z : ℍ
this_1 : (↑√z.im : ℂ) ≠ 0
this : (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
⊢ (↑(z.toSL2R • I) : ℂ) = (↑z : ℂ)
have 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)) : ℂ))
Tactic: rw [coe_specialLinearGroup_apply, div_eq_iff (mod_cast denom_ne_zero z.toSL2R I)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
z : ℍ
this : (↑√z.im : ℂ) ≠ 0
⊢ (↑(z.toSL2R • I) : ℂ) = (↑z : ℂ)
have coe : (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
z : ℍ
this : (↑√z.im : ℂ) ≠ 0
⊢ (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
have coe : ((↑z.re : ℂ) + (↑√z.im : ℂ) * Complex.I * (↑√z.im : ℂ)) / (↑√z.im : ℂ) = (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
z : ℍ
this : (↑√z.im : ℂ) ≠ 0
coe : ((↑z.re : ℂ) + (↑√z.im : ℂ) * Complex.I * (↑√z.im : ℂ)) / (↑√z.im : ℂ) = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
⊢ (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
have coe₁ : ((↑z.re : ℂ) + (↑√z.im : ℂ) * (↑√z.im : ℂ) * Complex.I) / (↑√z.im : ℂ) = (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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 : ℂ)⁻¹
⊢ (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
have coe₂ : ((↑z.re : ℂ) + (↑(√z.im * √z.im) : ℂ) * Complex.I) / (↑√z.im : ℂ) = (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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 : ℂ)⁻¹
⊢ (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
have coe₃ : ((↑z.re : ℂ) + (↑√(z.im * z.im) : ℂ) * Complex.I) / (↑√z.im : ℂ) = (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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 : ℂ)⁻¹
⊢ (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
have coe₄ : ((↑z.re : ℂ) + (↑z.im : ℂ) * Complex.I) / (↑√z.im : ℂ) = (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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 : ℂ)⁻¹
⊢ (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
have coe₅ : (↑z : ℂ) / (↑√z.im : ℂ) = (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
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 : ℂ)⁻¹
⊢ (↑z.re : ℂ) / (↑√z.im : ℂ) + (↑√z.im : ℂ) * Complex.I = (↑z : ℂ) * (↑√z.im : ℂ)⁻¹
have coe₆ : (↑z : ℂ) * (↑√z.im : ℂ)⁻¹ = (↑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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
⊢ HPow.hPow (β := ℕ) J 2 = 1
have huv : ∀ (i j : Fin 2), (↑(HPow.hPow (β := ℕ) J 2) : Matrix (Fin 2) (Fin 2) ℝ) i j = (↑1 : Matrix (Fin 2) (Fin 2) ℝ) i j
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
⊢ Eq (α := ℝˣ) ((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) J : ℝˣ) (-1 : ℝˣ)
have huv : Eq (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) J) : ℝ) (↑(-1) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
a b : SL(2, ℤ)
⊢ coe a = coe b ↔ a = b
have 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
Tactic: refine ⟨fun h ↦ a.ext b fun i j ↦ ?_, congr_arg _⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (hypothesis)
Goal:
a b : SL(2, ℤ)
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
have 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
Tactic: simp only [Subtype.ext_iff, GeneralLinearGroup.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : SL(2, ℤ)
z : ℍ
⊢ -g • z = g • z
have 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
Tactic: rw [sl_moeb, ← z.neg_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction (goal)
Goal:
g : SL(2, ℤ)
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 =
    g • z
have 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)
Tactic: congr 1 with i j
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction (goal)
Goal:
⊢ Continuous toSL2R
have apply : Continuous (Subtype.val (p := fun (A : Matrix (Fin 2) (Fin 2) ℝ) ↦ A.det = 1) ∘ toSL2R)
Tactic: apply continuous_induced_rng.mpr