awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hd :
  discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2
h :
  (↑z : ℂ) =
    (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
        Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
      (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
⊢ False
have refine : z.im ≤ 0
Tactic: refine z.im_pos.not_ge ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g_1 : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
hell : g.IsElliptic
hc : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hd :
  discrim (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ)
      ((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ))
      (-(↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1) : ℂ)) =
    HPow.hPow (β := ℕ) (Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) 2
h :
  (↑z : ℂ) =
    (-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
        Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
      (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))
⊢ z.im ≤ 0
have rw : ((-((↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1) : ℂ) - (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0) : ℂ)) -
        Complex.I * (↑√(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).discr) : ℂ)) /
      (2 * (↑((↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0) : ℂ))).im ≤
  0
Tactic: rw [← coe_im, h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
⊢ g • I = I ↔
    (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ∧
      (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
have rw : num g (↑I : ℂ) = HMul.hMul (α := ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ : (a : ℂ) → ℂ) (↑I : ℂ) : ℂ) (denom g (↑I : ℂ)) ↔
  (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ∧
    (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
Tactic: rw [gl_smul_eq_iff_num_eq, σ, if_pos hg]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) (↑((GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ) 0
⊢ g • I = I ↔
    (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ∧
      (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
have rw : num g (↑I : ℂ) = HMul.hMul (α := ℂ) ((Complex.conjCAE : (a : ℂ) → ℂ) (↑I : ℂ) : ℂ) (denom g (↑I : ℂ)) ↔
  (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 ∧
    (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
Tactic: rw [gl_smul_eq_iff_num_eq, σ, if_neg (not_lt_of_gt hg)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
⊢ (∀ (z : ℍ), g • z = z) ↔ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g
have mp : (∀ (z : ℍ), g • z = z) → Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
mp : (∀ (z : ℍ), g • z = z) → Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g
⊢ (∀ (z : ℍ), g • z = z) ↔ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g
have mpr : Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g → ∀ (z : ℍ), g • z = z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g
have mp : ∀ (hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)), False
Tactic: by_contra! hgc
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
⊢ False
have mp : ∀ (hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0), False
Tactic: rcases g.det_ne_zero.lt_or_gt with hlt | hgt
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
mp : ∀ (hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0), False
⊢ False
have mp₁ : ∀ (hgt : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det), False
Tactic: rcases g.det_ne_zero.lt_or_gt with hlt | hgt
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
⊢ False
have ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
Tactic: obtain ⟨ha, hb⟩ := (gl_smul_I_eq_I_iff_of_neg hlt).mp (hg _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
⊢ False
have hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
Tactic: obtain ⟨ha, hb⟩ := (gl_smul_I_eq_I_iff_of_neg hlt).mp (hg _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 = -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
⊢ False
have ha₁ : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
Tactic: rw [eq_neg_iff_add_eq_zero, ← Matrix.trace_fin_two] at ha
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
⊢ False
have mp : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), False
Tactic: rcases eq_or_ne (g 1 0) 0 with hc | hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
mp : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0), False
⊢ False
have mp₁ : ∀ (hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0), False
Tactic: rcases eq_or_ne (g 1 0) 0 with hc | hc
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ False
have hg₁ : g • { coe := 1 + Complex.I, coe_im_pos := sorry : ℍ } = { coe := 1 + Complex.I, coe_im_pos := sorry }
Tactic: specialize hg ⟨1 + .I, by simp⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
hg : g • { coe := 1 + Complex.I, coe_im_pos := ⋯ : ℍ } = { coe := 1 + Complex.I, coe_im_pos := ⋯ }
⊢ False
have hg₁ : { coe := 1 + Complex.I, coe_im_pos := sorry : ℍ }.re =
  (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 / (2 * (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1)
Tactic: rw [gl_smul_eq_self_iff_re_eq ha hc] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
⊢ False
have this : 0 < 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0|
Tactic: have : 0 < 1 + √(-g.val.det) / |g 1 0| := by simp [add_pos, *]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g : Matrix (Fin 2) (Fin 2) ℝ).det < 0
ha : (↑g : Matrix (Fin 2) (Fin 2) ℝ).trace = 0
hb : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 1 = (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0
hc : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 ≠ 0
this : 0 < 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0|
⊢ False
have hg₁ : g •
    {
      coe :=
        { re := -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
          im := 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0| : ℂ },
      coe_im_pos := this : ℍ } =
  {
    coe :=
      { re := -(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0,
        im := 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0| },
    coe_im_pos := this }
Tactic: specialize hg ⟨⟨-g 1 1 / g 1 0, 1 + √(-g.val.det) / |g 1 0|⟩, this⟩
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (hypothesis)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hgt : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
⊢ False
have this : g.IsElliptic
Tactic: have := isElliptic_of_exists_smul_eq_self hgt hgc ⟨.I, hg _⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hgt : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
this : g.IsElliptic
⊢ False
have mp : ∀ (hg : True), ∃ (z : ℍ), g • z ≠ z
Tactic: contrapose! hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
⊢ FaithfulSMul PGL(2, ℝ) ℍ
have rw : ∀ (g : PGL(2, ℝ)), (∀ (a : ℍ), g • a = a) → g = 1
Tactic: rw [faithfulSMul_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints (goal)
Goal:
g : PGL(2, ℝ)
⊢ (∀ (a : ℍ), g • a = a) → g = 1
have mk : ∀ (g : GL (Fin 2) ℝ),
  (∀ (a : ℍ),
      HSMul.hSMul (α := PGL(2, ℝ)) ((ProjGenLinGroup.mk : (a : GL (Fin 2) ℝ) → PGL(2, ℝ)) g : PGL(2, ℝ)) a = a) →
    Eq (α := PGL(2, ℝ)) ((ProjGenLinGroup.mk : (a : GL (Fin 2) ℝ) → PGL(2, ℝ)) g : PGL(2, ℝ)) (1 : PGL(2, ℝ))
Tactic: cases g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
⊢ atImInfty.NeBot
have refine : ∀ᶠ (x : ℝ) in atTop, x ∈ Set.range im
Tactic: refine comap_neBot_iff_frequently.mpr (Eventually.frequently ?_)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
⊢ ∀ᶠ (x : ℝ) in atTop, x ∈ Set.range im
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x : ℝ |
      Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Set.range im) x} x}
    a
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
    using ⟨⟨I * t, by simp [ht]⟩, by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 0 < x) x} x →
          Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ Set.range im) x} x}
      a
⊢ ∀ᶠ (x : ℝ) in atTop, x ∈ Set.range im
have h₁ : ∀ (a : ℝ), 0 < a → a ∈ Set.range im
Tactic: filter_upwards [eventually_gt_atTop 0] with t ht
    using ⟨⟨I * t, by simp [ht]⟩, by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
S : Set ℍ
⊢ S ∈ atImInfty ↔ ∃ (A : ℝ), ∀ (z : ℍ), A ≤ z.im → z ∈ S
have simp : (∃ (i : ℝ), im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ (A : ℝ), ∀ (z : ℍ), A ≤ z.im → z ∈ S
Tactic: simp only [atImInfty_basis.mem_iff, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
⊢ Tendsto (↑ofComplex : ℂ → ℍ) (comap Complex.im atTop) atImInfty
have simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im) (comap Complex.im atTop) atTop
Tactic: simp only [atImInfty, tendsto_comap_iff, Function.comp_def]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im) (comap Complex.im atTop) atTop
have refine : Complex.im =ᶠ[comap Complex.im atTop] fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im
Tactic: refine tendsto_comap.congr' ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
⊢ Complex.im =ᶠ[comap Complex.im atTop] fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im
have h : ∀ (z : ℂ) (hz : z ∈ Complex.im ⁻¹' Set.Ioi 0), z.im = ((↑ofComplex : ℂ → ℍ) z).im
Tactic: filter_upwards [preimage_mem_comap (Ioi_mem_atTop 0)] with z hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ Tendsto (fun (τ : ℍ) ↦ g • τ) atImInfty atImInfty
have suffices : Tendsto (β := ℝ) (fun (τ : ℍ) ↦ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1| * τ.im)
  atImInfty atTop
Tactic: suffices Tendsto (fun τ ↦ |g 0 0 / g 1 1| * τ.im) atImInfty atTop by
    simpa [atImInfty, Function.comp_def, im_smul, num, denom, hg, abs_div, abs_mul,
      abs_of_pos (UpperHalfPlane.im_pos _), mul_div_right_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty (goal)
Goal:
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ Tendsto (β := ℝ) (fun (τ : ℍ) ↦ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1| * τ.im)
    atImInfty atTop
have apply : 0 < |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1|
Tactic: apply tendsto_comap.const_mul_atTop
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑ofComplex : ℂ → ℍ) z
have rw : ContinuousAt (↑ofComplex : ℂ → ℍ) z ∧
  ContDiffWithinAt ℂ n
    ((↑(extChartAt 𝓘(ℂ, ℂ) ((↑ofComplex : ℂ → ℍ) z)) : ℍ → ℂ) ∘
      (↑ofComplex : ℂ → ℍ) ∘ (↑(extChartAt 𝓘(ℂ, ℂ) z).symm : ℂ → ℂ))
    (Set.range (↑𝓘(ℂ, ℂ) : ℂ → ℂ)) ((↑(extChartAt 𝓘(ℂ, ℂ) z) : ℂ → ℂ) z)
Tactic: rw [contMDiffAt_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex : ℂ → ℍ) z ∧
    ContDiffWithinAt ℂ n
      ((↑(extChartAt 𝓘(ℂ, ℂ) ((↑ofComplex : ℂ → ℍ) z)) : ℍ → ℂ) ∘
        (↑ofComplex : ℂ → ℍ) ∘ (↑(extChartAt 𝓘(ℂ, ℂ) z).symm : ℂ → ℂ))
      (Set.range (↑𝓘(ℂ, ℂ) : ℂ → ℂ)) ((↑(extChartAt 𝓘(ℂ, ℂ) z) : ℂ → ℂ) z)
have left : ContinuousAt (↑ofComplex : ℂ → ℍ) z
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
left : ContinuousAt (↑ofComplex : ℂ → ℍ) z
⊢ ContinuousAt (↑ofComplex : ℂ → ℍ) z ∧
    ContDiffWithinAt ℂ n
      ((↑(extChartAt 𝓘(ℂ, ℂ) ((↑ofComplex : ℂ → ℍ) z)) : ℍ → ℂ) ∘
        (↑ofComplex : ℂ → ℍ) ∘ (↑(extChartAt 𝓘(ℂ, ℂ) z).symm : ℂ → ℂ))
      (Set.range (↑𝓘(ℂ, ℂ) : ℂ → ℂ)) ((↑(extChartAt 𝓘(ℂ, ℂ) z) : ℂ → ℂ) z)
have right : ContDiffWithinAt ℂ n
  ((↑(extChartAt 𝓘(ℂ, ℂ) ((↑ofComplex : ℂ → ℍ) z)) : ℍ → ℂ) ∘
    (↑ofComplex : ℂ → ℍ) ∘ (↑(extChartAt 𝓘(ℂ, ℂ) z).symm : ℂ → ℂ))
  (Set.range (↑𝓘(ℂ, ℂ) : ℂ → ℂ)) ((↑(extChartAt 𝓘(ℂ, ℂ) z) : ℂ → ℂ) z)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex : ℂ → ℍ) z
have left : Tendsto (UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ)) (𝓝 z) (𝓝 (↑((↑ofComplex : ℂ → ℍ) z) : ℂ))
Tactic: rw [ContinuousAt, nhds_induced, tendsto_comap_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto (UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ)) (𝓝 z) (𝓝 (↑((↑ofComplex : ℂ → ℍ) z) : ℂ))
have left : Tendsto id (𝓝 z) (𝓝 (↑((↑ofComplex : ℂ → ℍ) z) : ℂ))
Tactic: refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContDiffAt ℂ n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
have rw : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
Tactic: rw [← contMDiffAt_iff_contDiffAt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
have refine_1 : ∀ (hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ), ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
refine_1 : ∀ (hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ), ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
have refine_2 : ∀ (hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)), ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ DifferentiableAt ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
have rw : MDiffAt f τ ↔ MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
Tactic: rw [← mdifferentiableAt_iff_differentiableAt]
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
have refine_1 : ∀ (hf : MDiffAt f τ), MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
τ : ℍ
refine_1 : ∀ (hf : MDiffAt f τ), MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ MDiffAt f τ ↔ MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
have refine_2 : ∀ (hf : MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)), MDiffAt f τ
Tactic: refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ 0 ∉ {0}ᶜ ∨ 0 ≤ k
have tauto : ¬0 ∉ {0}ᶜ → 0 ≤ k
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
tauto : ¬0 ∉ {0}ᶜ → 0 ≤ k
⊢ 0 ∉ {0}ᶜ ∨ 0 ≤ k
have tauto₁ : Membership.mem (γ := Set ℂ) {0}ᶜ 0 → 0 ≤ k
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (hypothesis)
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℂ) n (fun (x : ℍ) ↦ denom g (↑x : ℂ) ^ k) τ
have this : AnalyticAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x ^ k) (denom g (↑τ : ℂ))
Tactic: have : AnalyticAt ℂ (· ^ k) (denom g τ) := (differentiableOn_zpow k _ (by tauto)).analyticOnNhd
    isOpen_compl_singleton _ (denom_ne_zero g τ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℍ) n (fun (τ : ℍ) ↦ g • τ) τ
have refine : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n ((↑(extChartAt 𝓘(ℂ, ℂ) (g • τ)) : ℍ → ℂ) ∘ fun (τ : ℍ) ↦ g • τ) τ
Tactic: refine contMDiffAt_iff_target.mpr ⟨(continuous_const_smul g).continuousAt, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
hf : MDiff f
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 0
have rw : ∀ (hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}) {τ : ℍ} (hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0),
  f = 0
Tactic: rw [mdifferentiable_iff] at hf
Cleared hypotheses: hf, τ, hτ
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (hypothesis)
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
⊢ f = 0
have this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
Tactic: have := hf.analyticOnNhd isOpen_upperHalfPlaneSet
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
⊢ f = 0
have h : ∀ (w : ℍ), f w = 0 w
Tactic: ext w
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
⊢ f w = 0 w
have h : f w = (f ∘ (↑ofComplex : ℂ → ℍ)) (↑w : ℂ)
Tactic: convert! this.eqOn_zero_of_preconnected_of_frequently_eq_zero (z₀ := ↑τ) ?_ τ.2 ?_ w.im_pos
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
h : f w = (f ∘ (↑ofComplex : ℂ → ℍ)) (↑w : ℂ)
⊢ f w = 0 w
have h₁ : IsPreconnected (α := ℂ) {z : ℂ | 0 < z.im}
Tactic: convert! this.eqOn_zero_of_preconnected_of_frequently_eq_zero (z₀ := ↑τ) ?_ τ.2 ?_ w.im_pos
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
h : f w = (f ∘ (↑ofComplex : ℂ → ℍ)) (↑w : ℂ)
h₁ : IsPreconnected (α := ℂ) {z : ℂ | 0 < z.im}
⊢ f w = 0 w
have h₂ : ∃ᶠ (z : ℂ) in 𝓝[≠] (↑τ : ℂ), (f ∘ (↑ofComplex : ℂ → ℍ)) z = 0
Tactic: convert! this.eqOn_zero_of_preconnected_of_frequently_eq_zero (z₀ := ↑τ) ?_ τ.2 ?_ w.im_pos
-- Lean 4 proof step from Mathlib.Analysis.Complex.UpperHalfPlane.Manifold (goal)
Goal:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
τ : ℍ
hτ : ∃ᶠ (z : ℍ) in 𝓝[≠] τ, f z = 0
this : AnalyticOnNhd ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}
w : ℍ
⊢ f w = (f ∘ (↑ofComplex : ℂ → ℍ)) (↑w : ℂ)
have h : f w = f ((↑ofComplex : ℂ → ℍ) (↑w : ℂ))
Tactic: rw [Function.comp_apply, ofComplex_apply]