awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
this : 0 < 1 + √(-(↑g : Matrix (Fin 2) (Fin 2) ℝ).det) / |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0|
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 }
⊢ False

Tactic:
simp [gl_smul_eq_self_iff_dist_eq hlt ha hc, Complex.dist_eq_re_im, Real.sqrt_sq this.le]
          at hg

Premises used: LT.lt.le, Real.sqrt_sq, UpperHalfPlane.gl_smul_eq_self_iff_dist_eq, Complex.dist_eq_re_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
⊢ g.IsElliptic

Tactic:
have := isElliptic_of_exists_smul_eq_self hgt hgc ⟨.I, hg _⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
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
mp : ∀ (hg : True), ∃ (z : ℍ), g • z ≠ z
⊢ False

Tactic:
contrapose! hg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hgt : 0 < (↑g : Matrix (Fin 2) (Fin 2) ℝ).det
this : g.IsElliptic
hg : True
⊢ ∃ (z : ℍ), g • z ≠ z

Tactic:
simp [gl_smul_eq_self_iff_eq_fixedPt hgt this, exists_ne]

Premises used: UpperHalfPlane.gl_smul_eq_self_iff_eq_fixedPt, exists_ne
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : GL (Fin 2) ℝ
⊢ Membership.mem (γ := Subgroup (GL (Fin 2) ℝ)) (Subgroup.center (GL (Fin 2) ℝ)) g → ∀ (z : ℍ), g • z = z

Tactic:
aesop (add simp GeneralLinearGroup.center_eq_range_scalar)

Premises used: Matrix.GeneralLinearGroup.center_eq_range_scalar
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
rw : ∀ (g : PGL(2, ℝ)), (∀ (a : ℍ), g • a = a) → g = 1
⊢ FaithfulSMul PGL(2, ℝ) ℍ

Tactic:
rw [faithfulSMul_iff]

Premises used: faithfulSMul_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
g : PGL(2, ℝ)
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, ℝ))
⊢ (∀ (a : ℍ), g • a = a) → g = 1

Tactic:
cases g
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints
Goal:
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:
simp [forall_smul_eq_self_iff_mem_center]

Premises used: UpperHalfPlane.forall_smul_eq_self_iff_mem_center
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
⊢ atImInfty.NeBot

Tactic:
comap_neBot_iff_frequently.mpr (Eventually.frequently ?_)

Premises used: Iff.mpr, UpperHalfPlane.atImInfty, Filter.Eventually.frequently, Filter.comap_neBot_iff_frequently
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
refine : ∀ᶠ (x : ℝ) in atTop, x ∈ Set.range im
⊢ atImInfty.NeBot

Tactic:
refine comap_neBot_iff_frequently.mpr (Eventually.frequently ?_)

Premises used: Iff.mpr, Filter.Eventually.frequently, Filter.comap_neBot_iff_frequently
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
t : ℝ
ht : 0 < t
⊢ 0 < ((↑I : ℂ) * (↑t : ℂ)).im

Tactic:
simp [ht]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
t : ℝ
ht : 0 < t
⊢ { coe := (↑I : ℂ) * (↑t : ℂ), coe_im_pos := ⋯ : ℍ }.im = t

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
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
h₁ h₂ : ∀ (t : ℝ) (ht : 0 < t), t ∈ Set.range im
⊢ ∀ᶠ (x : ℝ) in atTop, x ∈ Set.range im

Tactic:
filter_upwards [eventually_gt_atTop 0] with t ht
    using ⟨⟨I * t, by simp [ht]⟩, by simp⟩

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
⊢ atImInfty.HasBasis (fun (x : ℝ) ↦ True) fun (i : ℝ) ↦ im ⁻¹' Set.Ici i

Tactic:
Filter.HasBasis.comap UpperHalfPlane.im Filter.atTop_basis

Premises used: Filter.atTop_basis, UpperHalfPlane.atImInfty, Filter.HasBasis.comap, UpperHalfPlane.im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
S : Set ℍ
simp : (∃ (i : ℝ), im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ (A : ℝ), ∀ (z : ℍ), A ≤ z.im → z ∈ S
⊢ S ∈ atImInfty ↔ ∃ (A : ℝ), ∀ (z : ℍ), A ≤ z.im → z ∈ S

Tactic:
simp only [atImInfty_basis.mem_iff, true_and]

Premises used: Filter.HasBasis.mem_iff, UpperHalfPlane.atImInfty_basis, true_and
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
S : Set ℍ
⊢ (∃ (i : ℝ), im ⁻¹' Set.Ici i ⊆ S) ↔ ∃ (A : ℝ), ∀ (z : ℍ), A ≤ z.im → z ∈ S

Tactic:
rfl
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
α : Type u_1
inst : NormedField α
⊢ IsBoundedAtImInfty.{u_1} (α := α) 0

Tactic:
const_boundedAtFilter atImInfty (0 : α)

Premises used: UpperHalfPlane.IsBoundedAtImInfty, UpperHalfPlane.atImInfty, Filter.const_boundedAtFilter, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
α : Type u_1
inst : Norm α
f : ℍ → α
⊢ IsBoundedAtImInfty f ↔ ∃ (M : ℝ) (A : ℝ), ∀ (z : ℍ), A ≤ z.im → ‖f z‖ ≤ M

Tactic:
simp [IsBoundedAtImInfty, BoundedAtFilter, Asymptotics.isBigO_iff, Filter.Eventually,
    atImInfty_mem]

Premises used: UpperHalfPlane.IsBoundedAtImInfty, Asymptotics.isBigO_iff, Filter.Eventually, Filter.BoundedAtFilter, UpperHalfPlane.atImInfty_mem
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
α : Type u_1
inst : SeminormedAddGroup α
f : ℍ → α
⊢ (∀ (ib : ℝ),
      0 < ib → ∃ (ia : ℝ), True ∧ ∀ x ∈ im ⁻¹' Set.Ici ia, Membership.mem (γ := Set α) (Metric.closedBall 0 ib) (f x)) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ (A : ℝ), ∀ (z : ℍ), A ≤ z.im → ‖f z‖ ≤ ε

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
α : Type u_1
inst : SeminormedAddGroup α
f : ℍ → α
hf : IsZeroAtImInfty f
⊢ IsBoundedAtImInfty f

Tactic:
hf.boundedAtFilter

Premises used: UpperHalfPlane.IsBoundedAtImInfty, Filter.ZeroAtFilter.boundedAtFilter
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
simp : Tendsto (β := ℝ) (fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im) (comap Complex.im atTop) atTop
⊢ Tendsto (↑ofComplex : ℂ → ℍ) (comap Complex.im atTop) atImInfty

Tactic:
simp only [atImInfty, tendsto_comap_iff, Function.comp_def]

Premises used: UpperHalfPlane.atImInfty, Filter.tendsto_comap_iff, Function.comp_def
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im) (comap Complex.im atTop) atTop

Tactic:
tendsto_comap.congr' ?_

Premises used: Filter.tendsto_comap, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
refine : Complex.im =ᶠ[comap Complex.im atTop] fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im
⊢ Tendsto (β := ℝ) (fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im) (comap Complex.im atTop) atTop

Tactic:
refine tendsto_comap.congr' ?_

Premises used: Filter.tendsto_comap, Filter.Tendsto.congr'
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
h : ∀ (z : ℂ) (hz : z ∈ Complex.im ⁻¹' Set.Ioi 0), z.im = ((↑ofComplex : ℂ → ℍ) z).im
⊢ Complex.im =ᶠ[comap Complex.im atTop] fun (x : ℂ) ↦ ((↑ofComplex : ℂ → ℍ) x).im

Tactic:
filter_upwards [preimage_mem_comap (Ioi_mem_atTop 0)] with z hz

Premises used: Filter.Ioi_mem_atTop, Filter.preimage_mem_comap, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
z : ℂ
hz : z ∈ Complex.im ⁻¹' Set.Ioi 0
⊢ z.im = ((↑ofComplex : ℂ → ℍ) z).im

Tactic:
simp [ofComplex_apply_of_im_pos hz]

Premises used: UpperHalfPlane.ofComplex_apply_of_im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
⊢ Tendsto UpperHalfPlane.coe atImInfty (comap Complex.im atTop)

Tactic:
simpa only [atImInfty, tendsto_comap_iff, Function.comp_def,
    funext UpperHalfPlane.coe_im] using tendsto_comap

Premises used: UpperHalfPlane.atImInfty, Filter.tendsto_comap_iff, Filter.tendsto_comap, funext, Function.comp_def, UpperHalfPlane.coe_im
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
this :
  Tendsto (β := ℝ) (fun (τ : ℍ) ↦ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1| * τ.im)
    atImInfty atTop
⊢ Tendsto (fun (τ : ℍ) ↦ g • τ) atImInfty atImInfty

Tactic:
simpa [atImInfty, Function.comp_def, im_smul, num, denom, hg, abs_div, abs_mul,
      abs_of_pos (UpperHalfPlane.im_pos _), mul_div_right_comm]

Premises used: UpperHalfPlane.im_pos, UpperHalfPlane.atImInfty, abs_mul, abs_div, UpperHalfPlane.im_smul, mul_div_right_comm, Function.comp_def, UpperHalfPlane.denom, abs_of_pos, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
suffices :
  Tendsto (β := ℝ) (fun (τ : ℍ) ↦ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1| * τ.im)
    atImInfty atTop
⊢ Tendsto (fun (τ : ℍ) ↦ g • τ) atImInfty atImInfty

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]
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
apply : 0 < |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1|
⊢ Tendsto (β := ℝ) (fun (τ : ℍ) ↦ |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1| * τ.im)
    atImInfty atTop

Tactic:
apply tendsto_comap.const_mul_atTop

Premises used: Filter.Tendsto.const_mul_atTop, Filter.tendsto_comap
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
Goal:
g : GL (Fin 2) ℝ
hg : (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 0 = 0
⊢ 0 < |(↑g : Matrix (Fin 2) (Fin 2) ℝ) 0 0 / (↑g : Matrix (Fin 2) (Fin 2) ℝ) 1 1|

Tactic:
simpa [Matrix.det_fin_two, hg] using g.det_ne_zero

Premises used: Matrix.GeneralLinearGroup.det_ne_zero, Matrix.det_fin_two
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
⊢ IsManifold 𝓘(ℂ, ℂ) ω ℍ

Tactic:
isOpenEmbedding_coe.isManifold_singleton

Premises used: UpperHalfPlane.isOpenEmbedding_coe, Topology.IsOpenEmbedding.isManifold_singleton
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n UpperHalfPlane.coe

Tactic:
fun _ => contMDiffAt_extChartAt

Premises used: ContMDiff, contMDiffAt_extChartAt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
⊢ MDiff UpperHalfPlane.coe

Tactic:
contMDiff_coe.mdifferentiable one_ne_zero

Premises used: UpperHalfPlane.contMDiff_coe, ContMDiff.mdifferentiable, one_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
rw :
  ContinuousAt (↑ofComplex : ℂ → ℍ) z ∧
    ContDiffWithinAt ℂ n
      ((↑(extChartAt 𝓘(ℂ, ℂ) ((↑ofComplex : ℂ → ℍ) z)) : ℍ → ℂ) ∘
        (↑ofComplex : ℂ → ℍ) ∘ (↑(extChartAt 𝓘(ℂ, ℂ) z).symm : ℂ → ℂ))
      (Set.range (↑𝓘(ℂ, ℂ) : ℂ → ℂ)) ((↑(extChartAt 𝓘(ℂ, ℂ) z) : ℂ → ℂ) z)
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (↑ofComplex : ℂ → ℍ) z

Tactic:
rw [contMDiffAt_iff]

Premises used: contMDiffAt_iff
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
left : ContinuousAt (↑ofComplex : ℂ → ℍ) z
right :
  ContDiffWithinAt ℂ n
    ((↑(extChartAt 𝓘(ℂ, ℂ) ((↑ofComplex : ℂ → ℍ) z)) : ℍ → ℂ) ∘
      (↑ofComplex : ℂ → ℍ) ∘ (↑(extChartAt 𝓘(ℂ, ℂ) z).symm : ℂ → ℂ))
    (Set.range (↑𝓘(ℂ, ℂ) : ℂ → ℂ)) ((↑(extChartAt 𝓘(ℂ, ℂ) z) : ℂ → ℂ) z)
⊢ ContinuousAt (↑ofComplex : ℂ → ℍ) z ∧
    ContDiffWithinAt ℂ n
      ((↑(extChartAt 𝓘(ℂ, ℂ) ((↑ofComplex : ℂ → ℍ) z)) : ℍ → ℂ) ∘
        (↑ofComplex : ℂ → ℍ) ∘ (↑(extChartAt 𝓘(ℂ, ℂ) z).symm : ℂ → ℂ))
      (Set.range (↑𝓘(ℂ, ℂ) : ℂ → ℂ)) ((↑(extChartAt 𝓘(ℂ, ℂ) z) : ℂ → ℂ) z)

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
left : Tendsto (UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ)) (𝓝 z) (𝓝 (↑((↑ofComplex : ℂ → ℍ) z) : ℂ))
⊢ ContinuousAt (↑ofComplex : ℂ → ℍ) z

Tactic:
rw [ContinuousAt, nhds_induced, tendsto_comap_iff]

Premises used: ContinuousAt, Filter.tendsto_comap_iff, nhds_induced
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto (UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ)) (𝓝 z) (𝓝 (↑((↑ofComplex : ℂ → ℍ) z) : ℂ))

Tactic:
Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_

Premises used: UpperHalfPlane.eventuallyEq_coe_comp_ofComplex, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
left : Tendsto id (𝓝 z) (𝓝 (↑((↑ofComplex : ℂ → ℍ) z) : ℂ))
⊢ Tendsto (UpperHalfPlane.coe ∘ (↑ofComplex : ℂ → ℍ)) (𝓝 z) (𝓝 (↑((↑ofComplex : ℂ → ℍ) z) : ℂ))

Tactic:
refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_

Premises used: UpperHalfPlane.eventuallyEq_coe_comp_ofComplex, Filter.Tendsto.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto id (𝓝 z) (𝓝 (↑((↑ofComplex : ℂ → ℍ) z) : ℂ))

Tactic:
simpa [ofComplex_apply_of_im_pos hz] using tendsto_id

Premises used: Filter.tendsto_id, UpperHalfPlane.ofComplex_apply_of_im_pos
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContDiffWithinAt ℂ n
    ((↑(extChartAt 𝓘(ℂ, ℂ) ((↑ofComplex : ℂ → ℍ) z)) : ℍ → ℂ) ∘
      (↑ofComplex : ℂ → ℍ) ∘ (↑(extChartAt 𝓘(ℂ, ℂ) z).symm : ℂ → ℂ))
    (Set.range (↑𝓘(ℂ, ℂ) : ℂ → ℂ)) ((↑(extChartAt 𝓘(ℂ, ℂ) z) : ℂ → ℂ) z)

Tactic:
simpa using contDiffAt_id.congr_of_eventuallyEq (eventuallyEq_coe_comp_ofComplex hz)

Premises used: UpperHalfPlane.eventuallyEq_coe_comp_ofComplex, contDiffAt_id, ContDiffAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
z : ℂ
hz : 0 < z.im
⊢ MDiffAt (↑ofComplex : ℂ → ℍ) z

Tactic:
(contMDiffAt_ofComplex hz).mdifferentiableAt one_ne_zero

Premises used: ContMDiffAt.mdifferentiableAt, UpperHalfPlane.contMDiffAt_ofComplex, one_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
rw : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContDiffAt ℂ n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
rw [← contMDiffAt_iff_contDiffAt]

Premises used: contMDiffAt_iff_contDiffAt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
refine_1 : ∀ (hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ), ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
refine_2 : ∀ (hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)), ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
exact (ofComplex_apply τ ▸ hf).comp _ (contMDiffAt_ofComplex τ.im_pos)
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ

Tactic:
simpa only [Function.comp_def, ofComplex_apply] using hf.comp τ (contMDiff_coe τ)

Premises used: UpperHalfPlane.contMDiff_coe, UpperHalfPlane.ofComplex_apply, Function.comp_def, ContMDiffAt.comp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
τ : ℍ
rw : MDiffAt f τ ↔ MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ MDiffAt f τ ↔ DifferentiableAt ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
rw [← mdifferentiableAt_iff_differentiableAt]

Premises used: mdifferentiableAt_iff_differentiableAt
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
⟨fun hf ↦ ?_, fun hf ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
τ : ℍ
refine_1 : ∀ (hf : MDiffAt f τ), MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
refine_2 : ∀ (hf : MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)), MDiffAt f τ
⊢ MDiffAt f τ ↔ MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt f τ
⊢ MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)

Tactic:
exact (ofComplex_apply τ ▸ hf).comp _ (mdifferentiableAt_ofComplex τ.im_pos)
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt (f ∘ (↑ofComplex : ℂ → ℍ)) (↑τ : ℂ)
⊢ MDiffAt f τ

Tactic:
simpa only [Function.comp_def, ofComplex_apply] using hf.comp τ (mdifferentiable_coe τ)

Premises used: UpperHalfPlane.ofComplex_apply, Function.comp_def, UpperHalfPlane.mdifferentiable_coe, MDifferentiableAt.comp
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
f : ℍ → ℂ
⊢ MDiff f ↔ DifferentiableOn ℂ (f ∘ (↑ofComplex : ℂ → ℍ)) {z : ℂ | 0 < z.im}

Tactic:
⟨fun h z hz ↦ (mdifferentiableAt_iff.mp (h ⟨z, hz⟩)).differentiableWithinAt,
    fun h ⟨z, hz⟩ ↦ mdifferentiableAt_iff.mpr <| (h z hz).differentiableAt
     <| isOpen_upperHalfPlaneSet.mem_nhds hz⟩

Premises used: Iff.mpr, DifferentiableWithinAt.differentiableAt, DifferentiableAt.differentiableWithinAt, MDifferentiableAt, _private.0.UpperHalfPlane.mdifferentiable_iff.match_1, UpperHalfPlane.mk, IsOpen.mem_nhds, Iff.intro, Iff.mp, modelWithCornersSelf, Complex, UpperHalfPlane.mdifferentiableAt_iff, UpperHalfPlane.isOpen_upperHalfPlaneSet
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℂ) n fun (τ : ℍ) ↦ num g (↑τ : ℂ)

Tactic:
(contMDiff_const.mul contMDiff_coe).add contMDiff_const

Premises used: UpperHalfPlane.contMDiff_coe, ContMDiff.mul, contMDiff_const, ContMDiff.add, UpperHalfPlane.num
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℂ) n fun (τ : ℍ) ↦ denom g (↑τ : ℂ)

Tactic:
(contMDiff_const.mul contMDiff_coe).add contMDiff_const

Premises used: UpperHalfPlane.contMDiff_coe, ContMDiff.mul, contMDiff_const, ContMDiff.add, UpperHalfPlane.denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
tauto : ¬0 ∉ {0}ᶜ → 0 ≤ k
tauto₁ : Membership.mem (γ := Set ℂ) {0}ᶜ 0 → 0 ≤ k
⊢ 0 ∉ {0}ᶜ ∨ 0 ≤ k

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ 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 τ)
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
this : AnalyticAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x ^ k) (denom g (↑τ : ℂ))
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℂ) n (fun (x : ℍ) ↦ denom g (↑x : ℂ) ^ k) τ

Tactic:
this.contDiffAt.contMDiffAt.comp τ (contMDiff_denom g τ)

Premises used: ContMDiffAt.comp, UpperHalfPlane.contMDiff_denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
this : AnalyticAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x ^ k) (denom g (↑τ : ℂ))
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℂ) n (fun (x : ℍ) ↦ denom g (↑x : ℂ) ^ k) τ

Tactic:
exact this.contDiffAt.contMDiffAt.comp τ (contMDiff_denom g τ)

Premises used: ContMDiffAt.comp, UpperHalfPlane.contMDiff_denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℂ) n fun (τ : ℍ) ↦ (denom g (↑τ : ℂ))⁻¹

Tactic:
simpa using contMDiff_denom_zpow g (-1)

Premises used: UpperHalfPlane.contMDiff_denom_zpow, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℍ) n (fun (τ : ℍ) ↦ g • τ) τ

Tactic:
contMDiffAt_iff_target.mpr ⟨(continuous_const_smul g).continuousAt, ?_⟩

Premises used: Iff.mpr, ContinuousConstSMul.continuous_const_smul, Continuous.continuousAt, And.intro, contMDiffAt_iff_target
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
τ : ℍ
refine : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n ((↑(extChartAt 𝓘(ℂ, ℂ) (g • τ)) : ℍ → ℂ) ∘ fun (τ : ℍ) ↦ g • τ) τ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) (M' := ℍ) n (fun (τ : ℍ) ↦ g • τ) τ

Tactic:
refine contMDiffAt_iff_target.mpr ⟨(continuous_const_smul g).continuousAt, ?_⟩

Premises used: Iff.mpr, ContinuousConstSMul.continuous_const_smul, Continuous.continuousAt, And.intro, contMDiffAt_iff_target
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
n : ℕ∞ω
g : GL (Fin 2) ℝ
hg : LT.lt (α := ℝ) 0 (↑((Matrix.GeneralLinearGroup.det : (a : GL (Fin 2) ℝ) → ℝˣ) g) : ℝ)
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n ((↑(extChartAt 𝓘(ℂ, ℂ) (g • τ)) : ℍ → ℂ) ∘ fun (τ : ℍ) ↦ g • τ) τ

Tactic:
simpa [glPos_smul_def hg] using (contMDiff_num g τ).mul (contMDiff_inv_denom g τ)

Premises used: UpperHalfPlane.glPos_smul_def, UpperHalfPlane.contMDiff_inv_denom, UpperHalfPlane.contMDiff_num, ContMDiffAt.mul
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
⊢ MDiff fun (τ : ℍ) ↦ num g (↑τ : ℂ)

Tactic:
(contMDiff_num g).mdifferentiable one_ne_zero

Premises used: ContMDiff.mdifferentiable, UpperHalfPlane.contMDiff_num, one_ne_zero
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
⊢ MDiff fun (τ : ℍ) ↦ denom g (↑τ : ℂ)

Tactic:
(contMDiff_denom g).mdifferentiable one_ne_zero

Premises used: ContMDiff.mdifferentiable, one_ne_zero, UpperHalfPlane.contMDiff_denom
-- Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
Goal:
g : GL (Fin 2) ℝ
k : ℤ
⊢ MDiff fun (x : ℍ) ↦ denom g (↑x : ℂ) ^ k

Tactic:
(contMDiff_denom_zpow g k).mdifferentiable one_ne_zero

Premises used: ContMDiff.mdifferentiable, UpperHalfPlane.contMDiff_denom_zpow, one_ne_zero