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

Goal state before:
pp: case inr.inr
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : 0 < (↑g').det
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)

Tactic:
·

Goal state after:
case inr.inr
g g' : GL (Fin 2) ℝ
z : ℂ
h : 0 < (↑g).det
h' : 0 < (↑g').det
⊢ (if 0 < ↑(GeneralLinearGroup.det g) * ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ
      else Complex.conjCAE)
      z =
    (if 0 < ↑(GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE)
      ((if 0 < ↑(GeneralLinearGroup.det g') then ContinuousAlgEquiv.refl ℝ ℂ else Complex.conjCAE) z)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «0».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
·

Goal state after:
case «0».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «0».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case «0».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨0, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «1».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨1, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
·

Goal state after:
case «1».«0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨1, ⋯⟩)
      ((fun i ↦ i) ⟨0, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «1».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨1, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
·

Goal state after:
case «1».«1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
⊢ ((m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2) * (m - diagonal fun x ↦ (m 0 0 + m 1 1) / 2)) ((fun i ↦ i) ⟨1, ⋯⟩)
      ((fun i ↦ i) ⟨1, ⋯⟩) =
    diagonal (fun x ↦ ((m 0 0 + m 1 1) * (m 0 0 + m 1 1) - 2 * 2 * (m 0 0 * m 1 1 - m 0 1 * m 1 0)) / (2 * 2))
      ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g h : GL (Fin 2) ℝ
z : ℂ
⊢ (σ g) ((σ h) z) = (σ h) ((σ g) z)

Tactic:
simp only [σ]
  split_ifs <;> simp

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

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℂ
⊢ ‖(σ g) z‖ = ‖z‖

Tactic:
simp only [σ]
  split_ifs <;> simp

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

Goal state before:
pp: case inr
g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g).det
hell : g.IsElliptic
this : ∀ {g : GL (Fin 2) ℝ}, 0 < (↑g).det → ∀ (hell : g.IsElliptic), 0 < ↑g 1 0 → (g • z = z ↔ z = fixedPt g hell)
hc : ¬0 < ↑g 1 0
⊢ g • z = z ↔ 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
⊢ g • z = z ↔ z = fixedPt g hell

Tactic:
·

Goal state after:
case inr
g : GL (Fin 2) ℝ
z : ℍ
hpos : 0 < (↑g).det
hell : g.IsElliptic
this : ∀ {g : GL (Fin 2) ℝ}, 0 < (↑g).det → ∀ (hell : g.IsElliptic), 0 < ↑g 1 0 → (g • z = z ↔ z = fixedPt g hell)
hc : ¬0 < ↑g 1 0
⊢ g • z = z ↔ 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
⊢ 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)
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:
·

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

Goal state after:
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
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
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:
·

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
⊢ m ∉ Set.range ⇑(scalar (Fin 2))

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

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
⊢ m ∉ Set.range ⇑(scalar (Fin 2))
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:
·

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
⊢ 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
⊢ num (g * h) u / denom (g * h) u = num g (num h u / denom h u) / denom g (num h u / denom h u)

Tactic:
have hu : u.im ≠ 0 := by simpa only [← hu, σ_im_ne_zero] using! z.im_ne_zero

Goal state after:
g h : GL (Fin 2) ℝ
z : ℍ
u : ℂ
hu✝ : (σ g) ((σ h) ↑z) = u
hu : u.im ≠ 0
⊢ num (g * h) u / denom (g * h) u = num g (num h u / denom h u) / denom g (num h u / denom h u)
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
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))

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))
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:
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: case mp
g : GL (Fin 2) ℝ
⊢ (∀ (z : ℍ), g • z = z) → g ∈ Subgroup.center (GL (Fin 2) ℝ)

pp: case mpr
g : GL (Fin 2) ℝ
⊢ g ∈ Subgroup.center (GL (Fin 2) ℝ) → ∀ (z : ℍ), g • z = z

Tactic:
·

Goal state after:
case mp
g : GL (Fin 2) ℝ
⊢ (∀ (z : ℍ), g • z = z) → g ∈ Subgroup.center (GL (Fin 2) ℝ)
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
⊢ False

pp: case mp.inr
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hgt : 0 < (↑g).det
⊢ 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
⊢ 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 : ℕ
⊢ ‖g n + F (f - (g n).compContinuous e) - g n‖ = ‖F (f - (g n).compContinuous e)‖

Tactic:
add_sub_cancel_left

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

pp: case mp.inl.inr
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:
·

Goal state after:
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
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp
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))

pp: case mpr
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2)) → C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0

Tactic:
·

Goal state after:
case mp
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.inr
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:
·

Goal state after:
case mp.inl.inr
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
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mp.inr
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hgt : 0 < (↑g).det
⊢ False

Tactic:
·

Goal state after:
case mp.inr
g : GL (Fin 2) ℝ
hg : ∀ (z : ℍ), g • z = z
hgc : g ∉ Subgroup.center (GL (Fin 2) ℝ)
hgt : 0 < (↑g).det
⊢ False
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
pp: case mpr
g : GL (Fin 2) ℝ
⊢ g ∈ Subgroup.center (GL (Fin 2) ℝ) → ∀ (z : ℍ), g • z = z

Tactic:
·

Goal state after:
case mpr
g : GL (Fin 2) ℝ
⊢ g ∈ Subgroup.center (GL (Fin 2) ℝ) → ∀ (z : ℍ), g • z = z
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: ⊢ ContractibleSpace ↑upperHalfPlaneSet

Tactic:
exact (convex_halfSpace_im_gt 0).contractibleSpace ⟨I, one_pos.trans_eq I_im.symm⟩

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

Goal state before:
pp: case refine_1
g : GL (Fin 2) ℝ
⊢ Continuous ⇑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else conjCAE)

pp: case refine_2
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ num g ↑x / denom g ↑x

Tactic:
·

Goal state after:
case refine_1
g : GL (Fin 2) ℝ
⊢ Continuous ⇑(if 0 < ↑(Matrix.GeneralLinearGroup.det g) then ContinuousAlgEquiv.refl ℝ ℂ else conjCAE)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case refine_2
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ num g ↑x / denom g ↑x

Tactic:
·

Goal state after:
case refine_2
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ num g ↑x / denom g ↑x
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
g : GL (Fin 2) R
⊢ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2)) → C (↑g 1 0) * X ^ 2 + C (↑g 1 1 - ↑g 0 0) * X - C (↑g 0 1) = 0

Tactic:
·

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

Goal state before:
pp: case inl
hK : IsCompact ∅
⊢ ∃ A B, 0 < B ∧ ∅ ⊆ verticalStrip A B

pp: case inr
K : Set ℍ
hK : IsCompact K
hne : K.Nonempty
⊢ ∃ A B, 0 < B ∧ K ⊆ verticalStrip A B

Tactic:
·

Goal state after:
case inl
hK : IsCompact ∅
⊢ ∃ A B, 0 < B ∧ ∅ ⊆ verticalStrip A B
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: g : GL (Fin 2) ℝ
z : ℍ
⊢ (g • z).re = (num g ↑z / denom g ↑z).re

Tactic:
by
  change (smulAux' g z).re = _
  simp +contextual [smulAux', σ, DFunLike.ite_apply, apply_ite, Complex.div_re]

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

Goal state before:
pp: case pos
w : ℂ
hw : 0 < w.im
⊢ ↑ofComplex w = { coe := w, coe_im_pos := hw }

pp: case neg
w : ℂ
hw : ¬0 < w.im
⊢ ↑ofComplex w = Classical.choice ⋯

Tactic:
·

Goal state after:
case pos
w : ℂ
hw : 0 < w.im
⊢ ↑ofComplex w = { coe := w, coe_im_pos := hw }
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

Goal state before:
pp: case neg
w : ℂ
hw : ¬0 < w.im
⊢ ↑ofComplex w = Classical.choice ⋯

Tactic:
·

Goal state after:
case neg
w : ℂ
hw : ¬0 < w.im
⊢ ↑ofComplex w = Classical.choice ⋯
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case refine_1
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
⊢ ↑(g ^ n) = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m

pp: case refine_2
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
⊢ (↑n * a ^ (n - 1)) • m ≠ 0

Tactic:
·

Goal state after:
case refine_1
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
⊢ ↑(g ^ n) = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: u : ℝˣ
z : ℍ
⊢ { coe := num ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z / denom ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z,
      coe_im_pos := ⋯ } =
    z

pp: case hg
u : ℝˣ
z : ℍ
⊢ 0 < ↑(GeneralLinearGroup.det ((GeneralLinearGroup.scalar (Fin 2)) u))

Tactic:
·

Goal state after:
u : ℝˣ
z : ℍ
⊢ { coe := num ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z / denom ((GeneralLinearGroup.scalar (Fin 2)) u) ↑z,
      coe_im_pos := ⋯ } =
    z
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case hg
u : ℝˣ
z : ℍ
⊢ 0 < ↑(GeneralLinearGroup.det ((GeneralLinearGroup.scalar (Fin 2)) u))

Tactic:
·

Goal state after:
case hg
u : ℝˣ
z : ℍ
⊢ 0 < ↑(GeneralLinearGroup.det ((GeneralLinearGroup.scalar (Fin 2)) u))
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✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ n = n - 1 + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case refine_1
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‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖atTop.limUnder g‖ ≤ ‖f‖

pp: case refine_2
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‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖f‖ ≤ ‖atTop.limUnder g‖

Tactic:
·

Goal state after:
case refine_1
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‖
hg_dist : ∀ (n : ℕ), dist (g n) (g (n + 1)) ≤ 1 / 3 * ‖f‖ * (2 / 3) ^ n
hg_cau : CauchySeq g
this : Tendsto (fun n ↦ (g n).compContinuous e) atTop (𝓝 ((atTop.limUnder g).compContinuous e))
hge : (atTop.limUnder g).compContinuous e = f
⊢ ‖atTop.limUnder g‖ ≤ ‖f‖
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✝ : ℕ
a : K
m : Matrix (Fin 2) (Fin 2) K
hg : ↑g = (Matrix.scalar (Fin 2)) a + m
hm0 : m ≠ 0
hmsq : m ^ 2 = 0
n : ℕ
hn : 1 ≤ n
IH : ((Matrix.scalar (Fin 2)) a + m) ^ n = (Matrix.scalar (Fin 2)) (a ^ n) + (↑n * a ^ (n - 1)) • m
⊢ n - 1 + 1 = n

Tactic:
by lia

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

Goal state before:
pp: case refine_2
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
⊢ (↑n * a ^ (n - 1)) • m ≠ 0

Tactic:
·

Goal state after:
case refine_2
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
⊢ (↑n * a ^ (n - 1)) • m ≠ 0