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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ num g ↑z = Complex.conjCAE ↑z * denom g ↑z ↔
    ((↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re +
          (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im) *
        ↑g 1 0 ^ 2 =
      -(↑g).det

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : ↑g 0 0 = -↑g 1 1
hc : ↑g 1 0 ≠ 0
⊢ num g ↑z = Complex.conjCAE ↑z * denom g ↑z ↔
    ((↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).re +
          (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im * (↑z - -↑(↑g 1 1) / ↑(↑g 1 0)).im) *
        ↑g 1 0 ^ 2 =
      -(↑g).det
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 →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hc₂ : IsClosed[inst✝¹] (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hd : Disjoint (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Iic (-‖f‖ / 3))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' ⇑f ⁻¹' Ici (‖f‖ / 3))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
x : X
hfx : -‖f‖ ≤ f x ∧ f x ≤ ‖f‖
hle₁ : -‖f‖ / 3 ≤ f x
hle₂ : ‖f‖ / 3 ≤ f x
⊢ f x - ‖f‖ / 3 = f x - ‖f‖ / 3

Tactic:
]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0| ↔
    dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0)) = √(-(↑g).det) / |↑g 1 0|

pp: case hy
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ ↑g 1 0 ^ 2

pp: case hx
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ -(↑g).det / ↑g 1 0 ^ 2

pp: case hy
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0))

Tactic:
]

Goal state after:
case hy
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ ↑g 1 0 ^ 2

case hx
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ -(↑g).det / ↑g 1 0 ^ 2

case hy
g : GL (Fin 2) ℝ
z : ℍ
h : (↑g).det < 0
htrace : (↑g).trace = 0
hc : ↑g 1 0 ≠ 0
⊢ 0 ≤ dist (↑z) (-↑(↑g 1 1) / ↑(↑g 1 0))
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case left
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ m ∉ (scalar (Fin 2)).range

Tactic:
]

Goal state after:
case left
R : Type u_1
inst✝ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
h : m.IsParabolic
⊢ m ∉ (scalar (Fin 2)).range
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
⊢ m ∉ Set.range ⇑(scalar (Fin 2)) ∧ m.discr = 0 ↔ m 0 0 = m 1 1 ∧ m 0 1 ≠ 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
⊢ m ∉ Set.range ⇑(scalar (Fin 2)) ∧ m.discr = 0 ↔ m 0 0 = m 1 1 ∧ m 0 1 ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
this : m.discr = (m 0 0 - m 1 1) ^ 2
⊢ m 0 0 = m 1 1 ↔ m 0 0 = m 1 1

Tactic:
]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑(↑g).discr

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz : g • z = z
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑(↑g).discr
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz :
  ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + ↑√(↑g).discr) / (2 * ↑(↑g 1 0)) ∨
    ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - ↑√(↑g).discr) / (2 * ↑(↑g 1 0))
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑√(↑g).discr * ↑√(↑g).discr
⊢ False

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
h : 0 < (↑g).det
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
z : ℍ
hz :
  ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + ↑√(↑g).discr) / (2 * ↑(↑g 1 0)) ∨
    ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - ↑√(↑g).discr) / (2 * ↑(↑g 1 0))
hc : ↑g 1 0 ≠ 0
hge : 0 ≤ (↑g).discr
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = ↑√(↑g).discr * ↑√(↑g).discr
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) (num g z / denom g z)).im =
    ↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)

Tactic:
]

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) (num g z / denom g z)).im =
    ↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ (Complex.conjCAE (num g z / denom g z)).im = -↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)

Tactic:
]

Goal state after:
case neg
g : GL (Fin 2) ℝ
z : ℂ
h : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ (Complex.conjCAE (num g z / denom g z)).im = -↑(GeneralLinearGroup.det g) * z.im / Complex.normSq (denom g z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ 0 < |↑(GeneralLinearGroup.det g)| * (↑z).im / Complex.normSq (denom g ↑z)

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
z : ℍ
⊢ 0 < |↑(GeneralLinearGroup.det g)| * (↑z).im / Complex.normSq (denom g ↑z)
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
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = Complex.I ^ 2 * ↑(-(↑g).discr)

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:
]

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = Complex.I ^ 2 * ↑(-(↑g).discr)

g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
⊢ 0 ≤ -(↑g).discr
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((F (f - (g n).compContinuous e)).compContinuous e) (f - (g n).compContinuous e) ≤ 2 / 3 * ((2 / 3) ^ n * ‖f‖)

Tactic:
]

Goal state after:
case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((F (f - (g n).compContinuous e)).compContinuous e) (f - (g n).compContinuous e) ≤ 2 / 3 * ((2 / 3) ^ n * ‖f‖)
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
⊢ (m - (scalar (Fin 2)) (m.trace / 2)) ^ 2 = (scalar (Fin 2)) (m.discr / 4)

Tactic:
by
  simp only [scalar_apply, trace_fin_two, discr_fin_two, trace_fin_two,
    det_fin_two, sq, (by norm_num : (4 : K) = 2 * 2)]
  ext i j
  fin_cases i <;>
  fin_cases j <;>
  · simp [Matrix.mul_apply]
    field

Goal state after:
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:
]

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
⊢ n = 0
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
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ∨
      ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ↔
    z = fixedPt g hell

Tactic:
]

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ∨
      ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ↔
    z = fixedPt g hell
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
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ↔ z = fixedPt g hell

pp: g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ ¬↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))

Tactic:
]

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) + Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0)) ↔ z = fixedPt g hell

g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
⊢ ¬↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 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
⊢ m.discr = 0

Tactic:
]

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
⊢ m.discr = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
⊢ ↑(GeneralLinearGroup.det h) * u.im / Complex.normSq (denom h u) ≠ 0

Tactic:
]

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
⊢ ↑(GeneralLinearGroup.det h) * u.im / Complex.normSq (denom h u) ≠ 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.right
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
⊢ (m - (scalar (Fin 2)) (m.trace / 2)) ^ 2 = 0

Tactic:
hm,

Goal state after:
case mpr.right
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
⊢ ((scalar (Fin 2)) a + n - (scalar (Fin 2)) (((scalar (Fin 2)) a + n).trace / 2)) ^ 2 = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.right
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
⊢ ((diagonal fun x ↦ a) + n - (scalar (Fin 2)) ((∑ i, a + n.trace) / 2)) ^ 2 = 0

Tactic:
]

Goal state after:
case mpr.right
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
⊢ ((diagonal fun x ↦ a) + n - (scalar (Fin 2)) ((∑ i, a + n.trace) / 2)) ^ 2 = 0
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖

Tactic:
]

Goal state after:
case succ
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
n : ℕ
ihn : dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
⊢ dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr.right
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
⊢ m.discr = 0

Tactic:
suffices scalar (Fin 2) (m.discr / 4) = 0 by
        rw [← map_zero (scalar (Fin 2)), scalar_inj, div_eq_zero_iff] at this
        have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _
        tauto
      rw [← sub_scalar_sq_eq_discr, hm, trace_add, scalar_apply, trace_diagonal]
      simp [mul_div_cancel_left₀ _ (NeZero.ne (2 : K)),
        (Matrix.isNilpotent_trace_of_isNilpotent ⟨2, hnsq⟩).eq_zero, hnsq]

Goal state after:
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
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
h : ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))
⊢ ((-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))).im ≤ 0

Tactic:
]

Goal state after:
g✝ : GL (Fin 2) ℝ
z : ℍ
g : GL (Fin 2) ℝ
hpos : 0 < (↑g).det
hell : g.IsElliptic
hc : 0 < ↑g 1 0
hd : discrim (↑(↑g 1 0)) (↑(↑g 1 1) - ↑(↑g 0 0)) (-↑(↑g 0 1)) = (Complex.I * ↑√(-(↑g).discr)) ^ 2
h : ↑z = (-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))
⊢ ((-(↑(↑g 1 1) - ↑(↑g 0 0)) - Complex.I * ↑√(-(↑g).discr)) / (2 * ↑(↑g 1 0))).im ≤ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ num g ↑I = (ContinuousAlgEquiv.refl ℝ ℂ) ↑I * denom g ↑I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
⊢ num g ↑I = (ContinuousAlgEquiv.refl ℝ ℂ) ↑I * denom g ↑I ↔ ↑g 0 0 = ↑g 1 1 ∧ ↑g 0 1 = -↑g 1 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ False

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
m : Matrix (Fin 2) (Fin 2) R
hm : (m 0 0 + m 1 1) ^ 2 - 4 * (m 0 0 * m 1 1 - 0) < 0
hc : m 0 1 * m 1 0 = 0
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    num g (num h u / denom h u) * denom (g * h) u

Tactic:
]

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    num g (num h u / denom h u) * denom (g * h) u
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ↑(GeneralLinearGroup.det g) < 0
⊢ num g ↑I = Complex.conjCAE ↑I * denom g ↑I ↔ ↑g 0 0 = -↑g 1 1 ∧ ↑g 0 1 = ↑g 1 0

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
hg : ↑(GeneralLinearGroup.det g) < 0
⊢ num g ↑I = Complex.conjCAE ↑I * denom g ↑I ↔ ↑g 0 0 = -↑g 1 1 ∧ ↑g 0 1 = ↑g 1 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.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
⊢ False

Tactic:
]

Goal state after:
case mp.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
⊢ False
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 →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ ‖F (f - (g n).compContinuous e)‖ = ‖F (f - (g n).compContinuous e)‖

Tactic:
]

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
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))

Tactic:
]

Goal state after:
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.inl.inl
g : GL (Fin 2) ℝ
hg : { coe := 1 + Complex.I, coe_im_pos := ⋯ }.re = ↑g 0 1 / (2 * ↑g 1 1)
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:
]

Goal state after:
case mp.inl.inl
g : GL (Fin 2) ℝ
hg : { coe := 1 + Complex.I, coe_im_pos := ⋯ }.re = ↑g 0 1 / (2 * ↑g 1 1)
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
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    (↑(↑g 0 0) * num h u + ↑(↑g 0 1) * denom h u) * denom (g * h) u / denom h u

Tactic:
]

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
hu' : (num h u / denom h u).im ≠ 0
⊢ num (g * h) u * (↑(↑g 1 0) * num h u + ↑(↑g 1 1) * denom h u) / denom h u =
    (↑(↑g 0 0) * num h u + ↑(↑g 0 1) * denom h u) * denom (g * h) u / denom h u
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: ⊢ ∀ (g : PGL(2, ℝ)), (∀ (a : ℍ), g • a = a) → g = 1

Tactic:
]

Goal state after:
⊢ ∀ (g : PGL(2, ℝ)), (∀ (a : ℍ), g • a = a) → g = 1
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: ⊢ ContractibleSpace ↑upperHalfPlaneSet

Tactic:
]

Goal state after:
⊢ ContractibleSpace ↑upperHalfPlaneSet
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 →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
F : (X →ᵇ ℝ) → Y →ᵇ ℝ
hF_norm : ∀ (f : X →ᵇ ℝ), ‖F f‖ ≤ ‖f‖ / 3
hF_dist : ∀ (f : X →ᵇ ℝ), dist ((F f).compContinuous e) f ≤ 2 / 3 * ‖f‖
g : ℕ → Y →ᵇ ℝ := fun n ↦ (fun g ↦ g + F (f - g.compContinuous e))^[n] 0
g0 : g 0 = 0
g_succ : ∀ (n : ℕ), g (n + 1) = g n + F (f - (g n).compContinuous e)
hgf : ∀ (n : ℕ), dist ((g n).compContinuous e) f ≤ (2 / 3) ^ n * ‖f‖
n : ℕ
⊢ 3⁻¹ * ‖f - (g n).compContinuous e‖ = 3⁻¹ * ‖f - (g n).compContinuous e‖

Tactic:
]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(GeneralLinearGroup.det g)
z : ℍ
⊢ (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) / (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)) =
    (↑(↑g 0 0) * ↑z + ↑(↑g 0 1)) / (↑(↑g 1 0) * ↑z + ↑(↑g 1 1))

Tactic:
]

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

Goal state before:
pp: case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
⊢ ↑(↑N * -n) +ᵥ z ∈ verticalStrip (↑N) z.im

Tactic:
]

Goal state after:
case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
⊢ ↑(↑N * -n) +ᵥ z ∈ verticalStrip (↑N) z.im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℍ
h : 0 < ↑(GeneralLinearGroup.det g)
⊢ ↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z) =
    ↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z)

Tactic:
]

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

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z : ℍ
h : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ -↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z) =
    -↑(GeneralLinearGroup.det g) * (↑z).im / Complex.normSq (denom g ↑z)

Tactic:
]

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

Goal state before:
pp: case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
⊢ |z.re + ↑(-↑N * ⌊z.re / ↑N⌋)| ≤ ↑N

Tactic:
]

Goal state after:
case h
z : ℍ
N : ℕ
hn : 0 < N
n : ℤ := ⌊z.re / ↑N⌋
h : (↑(↑N * -n) +ᵥ z).re = ↑(-↑N * ⌊z.re / ↑N⌋) + z.re
⊢ |z.re + ↑(-↑N * ⌊z.re / ↑N⌋)| ≤ ↑N