mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
⊢ denom (g * h) ↑z = (σ h) (denom g ↑(smulAux h z)) * denom h ↑z

Tactic:
simpa using

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
⊢ ↑((↑g * ↑h) 1 0) * ↑z + ↑((↑g * ↑h) 1 1) =
    (↑(↑g 1 0) * (num h ↑z / (↑(↑h 1 0) * ↑z + ↑(↑h 1 1))) + ↑(↑g 1 1)) * (↑(↑h 1 0) * ↑z + ↑(↑h 1 1))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ 0 ≤ -(↑g).discr

Tactic:
simpa using

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ (↑g).discr ≤ 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ m.IsParabolic → ∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0

pp: case mpr
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0) → m.IsParabolic

Tactic:
· exact fun hm ↦ ⟨_, _, (add_sub_cancel ..).symm, sub_ne_zero.mpr fun h ↦ hm.1 ⟨_, h.symm⟩,
      hm.sub_eigenvalue_sq_eq_zero⟩

Goal state after:
case mpr
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ (∃ a n, m = (scalar (Fin 2)) a + n ∧ n ≠ 0 ∧ n ^ 2 = 0) → m.IsParabolic
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.left
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m - (scalar (Fin 2)) a = n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
x✝ : m ∈ Set.range ⇑(scalar (Fin 2))
b : K
hb : (scalar (Fin 2)) b = m
⊢ n = 0

Tactic:
simpa using

Goal state after:
case mpr.left
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m - (scalar (Fin 2)) a = n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
x✝ : m ∈ Set.range ⇑(scalar (Fin 2))
b : K
hb : (scalar (Fin 2)) b = m
⊢ b - a = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
this : m.discr = 0 ∨ 4 = 0
⊢ 4 ≠ 0

Tactic:
simpa using

Goal state after:
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
a : K
n : Matrix (Fin 2) (Fin 2) K
hm : m = (scalar (Fin 2)) a + n
hn0 : n ≠ 0
hnsq : n ^ 2 = 0
this : m.discr = 0 ∨ 4 = 0
⊢ ¬2 = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g)⁻¹ * m * ↑g).IsHyperbolic ↔ m.IsHyperbolic

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g)⁻¹ * m * ↑g).IsHyperbolic ↔ m.IsHyperbolic
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g)⁻¹ * m * ↑g).IsElliptic ↔ m.IsElliptic

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Preorder R
m : Matrix (Fin 2) (Fin 2) R
g : GL (Fin 2) R
⊢ ((↑g)⁻¹ * m * ↑g).IsElliptic ↔ m.IsElliptic
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.inl.inl
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hlt : (↑g).det < 0
ha : (↑g).trace = 0
hb : ↑g 0 1 = ↑g 1 0
hc : ↑g 1 0 = 0
⊢ False

Tactic:
specialize hg ⟨1 + .I, by simp⟩
        rw [gl_smul_eq_self_iff_re_eq ha hc] at hg
        simp_all

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
⊢ ↑g 0 1 = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
⊢ ↑g 0 1 = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
⊢ ↑g 1 0 = 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
⊢ ↑g 1 0 = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
hc : ↑g 1 0 = 0
⊢ ↑g 1 1 = ↑g 0 0

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
hP : C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0
hb : ↑g 0 1 = 0
hc : ↑g 1 0 = 0
⊢ ↑g 1 1 = ↑g 0 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
⊢ (↑g).trace ^ 2 = 4 * (↑g).det

Tactic:
simpa using

Goal state after:
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
⊢ (↑g).trace ^ 2 = 4 * (↑g).det
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ (↑g).parabolicEigenvalue ≠ 0

Tactic:
rw [parabolicEigenvalue, div_ne_zero_iff, eq_true_intro (two_ne_zero' K), and_true,
    Ne, ← sq_eq_zero_iff, this, show (4 : K) = 2 ^ 2 by norm_num, mul_eq_zero,
    sq_eq_zero_iff, not_or]

Goal state after:
K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : NeZero 2
hg : g.IsParabolic
this : (↑g).trace ^ 2 = 4 * (↑g).det
⊢ ¬2 = 0 ∧ ¬(↑g).det = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: a : ℍ
hw : ¬0 < (↑a).im
⊢ a.im ≤ 0

Tactic:
simpa using

Goal state after:
a : ℍ
hw : ¬0 < (↑a).im
⊢ a.im ≤ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
⊢ 0 < (-(starRingEnd ℂ) ↑τ).im

Tactic:
simpa using

Goal state after:
τ : ℍ
⊢ 0 < τ.im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖↑τ‖ ∧ r - ‖↑τ‖ < ε
hr' : r < 0
this✝ : ‖↑τ‖ < ε
this : 0 ∈ Metric.ball (↑τ) ε
⊢ False

Tactic:
simpa using

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : -ε < r - ‖↑τ‖ ∧ r - ‖↑τ‖ < ε
hr' : r < 0
this✝ : ‖↑τ‖ < ε
this : 0 ∈ Metric.ball (↑τ) ε
⊢ False
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: K : Type u_2
inst✝¹ : Field K
g : GL (Fin 2) K
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
this : a ≠ 0
⊢ (↑n * a ^ (n - 1)) • m ≠ 0

Tactic:
simp [this, hm0, hn]

Goal state after:
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ‖↑τ‖ ≠ 0

Tactic:
simpa using

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
⊢ ¬↑τ = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
⊢ ModularGroup.T • z = 1 +ᵥ z

Tactic:
simpa using

Goal state after:
z : ℍ
⊢ ModularGroup.T • z = 1 +ᵥ z
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ⇑g ∘ e = ⇑(f - const X ((a + b) / 2))
y : Y
this : ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2
⊢ (const Y ((a + b) / 2) + g) y ∈ Icc a b

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
a b : ℝ
e : X → Y
hf : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
he : IsClosedEmbedding e
g : Y →ᵇ ℝ
hgf : ‖g‖ = ‖f - const X ((a + b) / 2)‖
hge : ⇑g ∘ e = ⇑(f - const X ((a + b) / 2))
y : Y
this : ‖f - const X ((a + b) / 2)‖ ≤ (b - a) / 2
⊢ |g y| ≤ (b - a) / 2
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.inl
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det : det (upperRightHom x) = 1 ∨ det (upperRightHom x) = -1
hg10 : ↑(upperRightHom x) 1 0 = 0
⊢ ↑(upperRightHom x) 0 0 = ↑(upperRightHom x) 1 1 ∧ ↑(upperRightHom x) 0 1 ≠ 0

Tactic:
simpa using

Goal state after:
case mpr.inl
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det : det (upperRightHom x) = 1 ∨ det (upperRightHom x) = -1
hg10 : ↑(upperRightHom x) 1 0 = 0
⊢ ¬x = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.inr
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det : det (-upperRightHom x) = 1 ∨ det (-upperRightHom x) = -1
hg10 : ↑(-upperRightHom x) 1 0 = 0
⊢ ↑(-upperRightHom x) 0 0 = ↑(-upperRightHom x) 1 1 ∧ ↑(-upperRightHom x) 0 1 ≠ 0

Tactic:
simpa using

Goal state after:
case mpr.inr
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
x : K
hx : x ≠ 0
h_det : det (-upperRightHom x) = 1 ∨ det (-upperRightHom x) = -1
hg10 : ↑(-upperRightHom x) 1 0 = 0
⊢ ¬x = 0
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
hb : IsLUB (range ⇑f) a
hmem : ∀ (x : X), f x ∈ Icc a a
hle : a ≤ a
⊢ ∀ (x : X), f x = a

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
hb : IsLUB (range ⇑f) a
hmem : ∀ (x : X), f x ∈ Icc a a
hle : a ≤ a
⊢ ∀ (x : X), f x = a
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
this : ↑r / ↑‖↑τ‖ * ↑τ ∈ Metric.ball (↑τ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : ↑ξ = ↑r / ↑‖↑τ‖ * ↑τ
⊢ ‖↑τ‖ ≠ 0

Tactic:
simpa using

Goal state after:
τ : ℍ
U : Set ℝ
hU : U ∈ map (fun τ ↦ ‖↑τ‖) (𝓝 τ)
s : Set ℍ
hs' : (fun τ ↦ ‖↑τ‖) '' s ⊆ U
ε : ℝ
hεpos : ε > 0
hεs : Metric.ball (↑τ) ε ⊆ UpperHalfPlane.coe '' s
r : ℝ
hr : r ∈ Metric.ball ‖↑τ‖ ε
hr' : 0 ≤ r
this : ↑r / ↑‖↑τ‖ * ↑τ ∈ Metric.ball (↑τ) ε
ξ : ℍ
hξs : ξ ∈ s
hξτ : ↑ξ = ↑r / ↑‖↑τ‖ * ↑τ
⊢ ¬↑τ = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: ⊢ Tendsto UpperHalfPlane.coe atImInfty (comap Complex.im atTop)

Tactic:
simpa using

Goal state after:
⊢ Tendsto im (comap im atTop) atTop
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ↑g 1 0 = 0
⊢ 0 < |↑g 0 0 / ↑g 1 1|

Tactic:
simpa using

Goal state after:
g : GL (Fin 2) ℝ
hg : ↑g 1 0 = 0
⊢ ¬↑g 0 0 = 0 ∧ ¬↑g 1 1 = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: z : ℍ
⊢ ↑√z.im ≠ 0

Tactic:
simpa using

Goal state after:
z : ℍ
⊢ 0 < z.im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: a b : SL(2, ℤ)
i j : Fin 2
h : ∀ (i j : Fin 2), ↑↑(coe a) i j = ↑↑(coe b) i j
⊢ ↑a i j = ↑b i j

Tactic:
simpa using

Goal state after:
a b : SL(2, ℤ)
i j : Fin 2
h : ∀ (i j : Fin 2), ↑↑(coe a) i j = ↑↑(coe b) i j
⊢ ↑a i j = ↑b i j
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
⊢ (g • z).im = z.im / Complex.normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)

Tactic:
simpa using

Goal state after:
g : SL(2, ℤ)
z : ℍ
⊢ (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g) • z).im =
    z.im / Complex.normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ ↔ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ ↑ofComplex) ↑τ

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

Goal state after:
case refine_1
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ ↑ofComplex) ↑τ

case refine_2
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ ↑ofComplex) ↑τ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case refine_2
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ ↑ofComplex) ↑τ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ

Tactic:
simpa using

Goal state after:
case refine_2
n : ℕ∞ω
f : ℍ → ℂ
τ : ℍ
hf : ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n (f ∘ ↑ofComplex) ↑τ
⊢ ContMDiffAt 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n f τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
τ : ℍ
⊢ MDiffAt f τ ↔ MDiffAt (f ∘ ↑ofComplex) ↑τ

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

Goal state after:
case refine_1
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt f τ
⊢ MDiffAt (f ∘ ↑ofComplex) ↑τ

case refine_2
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt (f ∘ ↑ofComplex) ↑τ
⊢ MDiffAt f τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case refine_2
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt (f ∘ ↑ofComplex) ↑τ
⊢ MDiffAt f τ

Tactic:
simpa using

Goal state after:
case refine_2
f : ℍ → ℂ
τ : ℍ
hf : MDiffAt (f ∘ ↑ofComplex) ↑τ
⊢ MDiffAt f τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: n : ℕ∞ω
g : GL (Fin 2) ℝ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun τ ↦ (denom g ↑τ)⁻¹

Tactic:
simpa using

Goal state after:
n : ℕ∞ω
g : GL (Fin 2) ℝ
⊢ ContMDiff 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) n fun τ ↦ (denom g ↑τ)⁻¹
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case neg
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : ¬FiniteDimensional K L
⊢ IsIntegral R ((norm K) x)

Tactic:
simpa using

Goal state after:
case neg
R : Type u_1
inst✝⁶ : CommRing R
L : Type u_6
K : Type u_7
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra K L
inst✝² : Algebra R L
inst✝¹ : Algebra R K
inst✝ : IsScalarTower R K L
x : L
hx : IsIntegral R x
h : ¬FiniteDimensional K L
⊢ IsIntegral R 1
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
a : ℍ
ha : ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
⊢ a ∈ {τ}ᶜ → f a ≠ 0

Tactic:
simpa using

Goal state after:
f : ℍ → ℂ
hf : DifferentiableOn ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
τ : ℍ
this : AnalyticOnNhd ℂ (f ∘ ↑ofComplex) {z | 0 < z.im}
w : ℍ
hτ : ∀ᶠ (a : ℍ) in 𝓝 τ, ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
a : ℍ
ha : ↑a ∈ {↑τ}ᶜ → (f ∘ ↑ofComplex) ↑a ≠ 0
⊢ ¬a = τ → ¬f a = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f g : ℍ → ℂ
hf : MDiff f
hg : MDiff g
hfg : f * g = 0
⊢ ∀ (x : ℍ), f x = 0 ∨ g x = 0

Tactic:
simpa using

Goal state after:
f g : ℍ → ℂ
hf : MDiff f
hg : MDiff g
hfg : f * g = 0
⊢ ∀ (x : ℍ), f x = 0 ∨ g x = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : ∏ i ∈ s, f i = 0
⊢ ∀ (x : ℍ), ∏ i ∈ s, f i x = 0

Tactic:
simpa using

Goal state after:
ι : Type u_1
f : ι → ℍ → ℂ
s : Finset ι
hf : ∀ i ∈ s, MDiff (f i)
h0 : ∏ i ∈ s, f i = 0
⊢ ∀ (x : ℍ), ∏ i ∈ s, f i x = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ HasDerivAt (fun x ↦ denom g x) ↑(↑g 1 0) ↑τ

Tactic:
simpa using

Goal state after:
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
⊢ HasDerivAt (HMul.hMul ↑(↑g 1 0)) ↑(↑g 1 0) ↑τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
hd : HasDerivAt (fun x ↦ denom g x) ↑(↑g 1 0) ↑τ
this : HasDerivAt ((fun x ↦ x ^ k) ∘ denom g) (↑k * denom g ↑τ ^ (k - 1) * ↑(↑g 1 0)) ↑τ
⊢ HasDerivAt (fun z ↦ denom g z ^ k) (↑k * ↑(↑g 1 0) * denom g ↑τ ^ (k - 1)) ↑τ

Tactic:
simpa using

Goal state after:
g : GL (Fin 2) ℝ
k : ℤ
τ : ℍ
hd : HasDerivAt (fun x ↦ denom g x) ↑(↑g 1 0) ↑τ
this : HasDerivAt ((fun x ↦ x ^ k) ∘ denom g) (↑k * denom g ↑τ ^ (k - 1) * ↑(↑g 1 0)) ↑τ
⊢ HasDerivAt (fun z ↦ denom g z ^ k) (↑k * denom g ↑τ ^ (k - 1) * ↑(↑g 1 0)) ↑τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
this : HasStrictDerivAt (num g / denom g) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ
⊢ HasStrictDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (↑(↑g).det / denom g ↑τ ^ 2) ↑τ

Tactic:
refine this.congr_of_eventuallyEq ?_
    rw [← isOpenEmbedding_coe.map_nhds_eq, eventuallyEq_map]
    simp [Function.comp_def, coe_smul_of_det_pos hg]

Goal state after:
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K) x = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L

Tactic:
nth_rw 1 [← coe_gen K x]

Goal state after:
case pos
L : Type u_6
K : Type u_7
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
h : FiniteDimensional K L
F : IntermediateField K L := K⟮x⟯
⊢ (norm K) ↑(gen K x) = (norm K) (gen K x) ^ finrank (↥K⟮x⟯) L
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / ‖x -ᵥ c‖) ^ 2 • (x -ᵥ c)) ((R / ‖y -ᵥ c‖) ^ 2 • (y -ᵥ c)) = R ^ 2 / (‖x -ᵥ c‖ * ‖y -ᵥ c‖) * dist x y

Tactic:
simpa using

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
hx : x ≠ c
hy : y ≠ c
R : ℝ
⊢ dist ((R / ‖x -ᵥ c‖) ^ 2 • (x -ᵥ c)) ((R / ‖y -ᵥ c‖) ^ 2 • (y -ᵥ c)) = R ^ 2 / (‖x -ᵥ c‖ * ‖y -ᵥ c‖) * dist x y
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] 0)
hratio : Tendsto (fun x ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop
⊢ Tendsto (fun x ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop

Tactic:
simpa using

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
hdist : Tendsto (dist c) (𝓝[≠] c) (𝓝[>] 0)
hratio : Tendsto (fun x ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop
⊢ Tendsto (inversion c R) (𝓝[≠] c) (Bornology.cobounded P)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w✝ : ℍ
r : ℝ
z w : ℍ
h : dist z w = 0
⊢ z = w

Tactic:
simpa using

Goal state after:
z✝ w✝ : ℍ
r : ℝ
z w : ℍ
h : dist z w = 0
⊢ z = w
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ 0 < sinh x ↔ 0 < x

Tactic:
simpa using

Goal state after:
x : ℝ
⊢ 0 < sinh x ↔ 0 < x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x ≤ 0 ↔ x ≤ 0

Tactic:
simpa using

Goal state after:
x : ℝ
⊢ sinh x ≤ 0 ↔ x ≤ 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ sinh x < 0 ↔ x < 0

Tactic:
simpa using

Goal state after:
x : ℝ
⊢ sinh x < 0 ↔ x < 0
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
⊢ 0 ≤ sinh x ↔ 0 ≤ x

Tactic:
simpa using

Goal state after:
x : ℝ
⊢ 0 ≤ sinh x ↔ 0 ≤ x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case hab
z w : ℍ
⊢ dist { re := 0, im := z.im } { re := 0, im := w.im } ≤ dist ↑z ↑w

Tactic:
simpa using

Goal state after:
case hab
z w : ℍ
⊢ |z.im - w.im| ≤ dist ↑z ↑w
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Type u_4
inst✝ : CommRing A
x : GL n A
⊢ x ∈ Set.range ⇑toGL ↔ x ∈ ⇑GeneralLinearGroup.det ⁻¹' {1}

Tactic:
simpa using

Goal state after:
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
A : Type u_4
inst✝ : CommRing A
x : GL n A
⊢ (∃ y, ↑y = ↑x) ↔ (↑x).det = 1
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T0Space R
⊢ IsClosed[Units.instTopologicalSpaceUnits] (Set.range ⇑toGL)

Tactic:
simpa using

Goal state after:
n : Type u_1
R : Type u_2
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T0Space R
⊢ IsClosed[Units.instTopologicalSpaceUnits] (⇑GeneralLinearGroup.det ⁻¹' {1})
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
x : OnePoint X
⊢ x ≠ ∞ ↔ ∃ y, ↑y = x

Tactic:
induction x using OnePoint.rec

Goal state after:
case infty
X : Type u_1
⊢ ∞ ≠ ∞ ↔ ∃ y, ↑y = ∞

case coe
X : Type u_1
x✝ : X
⊢ ↑x✝ ≠ ∞ ↔ ∃ y, ↑y = ↑x✝
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
x : OnePoint X
⊢ x ∉ range some ↔ x = ∞

Tactic:
by
  rw [← mem_compl_iff, compl_range_coe, mem_singleton_iff]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen[inst✝] (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen[inst✝] (some ⁻¹' t)
hms' : ∞ ∈ s
hmt' : ∞ ∈ t
⊢ IsCompact (some ⁻¹' (s ∩ t))ᶜ

Tactic:
simpa using

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
s t : Set (OnePoint X)
hms : ∞ ∈ s → IsCompact (some ⁻¹' s)ᶜ
hs : IsOpen[inst✝] (some ⁻¹' s)
hmt : ∞ ∈ t → IsCompact (some ⁻¹' t)ᶜ
ht : IsOpen[inst✝] (some ⁻¹' t)
hms' : ∞ ∈ s
hmt' : ∞ ∈ t
⊢ IsCompact ((some ⁻¹' s)ᶜ ∪ (some ⁻¹' t)ᶜ)
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen[instTopologicalSpace] (some '' s) ↔ IsOpen[inst✝] s

Tactic:
isOpen_iff_of_notMem infty_notMem_image_coe,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsOpen[inst✝] (some ⁻¹' some '' s) ↔ IsOpen[inst✝] s