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

Goal state before:
pp: case «0»
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
⊢ cd ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
⊢ cd ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
⊢ cd ((fun i ↦ i) ⟨0, ⋯⟩) = 0 ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
cd : Fin 2 → ℝ
z : ℂ
hz : z.im ≠ 0
this : cd 0 = 0
h : cd 1 = 0
⊢ cd ((fun i ↦ i) ⟨1, ⋯⟩) = 0 ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((starRingEnd ℂ) z) = (starRingEnd ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z)

pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE ((starRingEnd ℂ) z) = (starRingEnd ℂ) (Complex.conjCAE z)

Tactic:
<;>

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((starRingEnd ℂ) z) = (starRingEnd ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z)

case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE ((starRingEnd ℂ) z) = (starRingEnd ℂ) (Complex.conjCAE z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
y : ℝ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ↑y = ↑y

pp: case neg
g : GL (Fin 2) ℝ
y : ℝ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE ↑y = ↑y

Tactic:
<;>

Goal state after:
case pos
g : GL (Fin 2) ℝ
y : ℝ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ↑y = ↑y

case neg
g : GL (Fin 2) ℝ
y : ℝ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE ↑y = ↑y
Module: Mathlib.Analysis.Complex.UpperHalfPlane.FixedPoints

Goal state before:
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.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z) = z

pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE (Complex.conjCAE z) = z

Tactic:
<;>

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z) = z

case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ Complex.conjCAE (Complex.conjCAE z) = z
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

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

Tactic:
by
  simpa using isParabolic_conj_iff g⁻¹

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

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) z).im ≠ 0 ↔ z.im ≠ 0

pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ (Complex.conjCAE z).im ≠ 0 ↔ z.im ≠ 0

Tactic:
<;>

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ ((ContinuousAlgEquiv.refl ℝ ℂ) z).im ≠ 0 ↔ z.im ≠ 0

case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ (Complex.conjCAE z).im ≠ 0 ↔ z.im ≠ 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case inl
g g' : GL (Fin 2) ℝ
z : ℂ
h : (↑g).det < 0
⊢ (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)

pp: case inr
g g' : GL (Fin 2) ℝ
z : ℂ
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 inl
g g' : GL (Fin 2) ℝ
z : ℂ
h : (↑g).det < 0
⊢ (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)

case inr
g g' : GL (Fin 2) ℝ
z : ℂ
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 h.«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : Fin 2
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) j = m ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case h.«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : Fin 2
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) j = m ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case h.«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : Fin 2
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) j = m ((fun i ↦ i) ⟨0, ⋯⟩) j

case h.«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
j : Fin 2
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) j = m ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case h.«0».«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case h.«0».«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case h.«1».«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case h.«1».«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case h.«0».«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«0».«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case h.«1».«0»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case h.«1».«1»
R : Type u_1
inst✝¹ : CommRing R
m : Matrix (Fin 2) (Fin 2) R
inst✝ : IsReduced R
hm : m 1 0 = 0
aux : m.discr = 0 ↔ m 0 0 = m 1 1
h : m 0 0 = m 1 1
h' : m 0 1 = 0
⊢ (scalar (Fin 2)) (m 1 1) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) = m ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case «0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
j : Fin 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, ⋯⟩) j =
    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, ⋯⟩) j

pp: case «1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
j : Fin 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, ⋯⟩) j =
    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, ⋯⟩) j

Tactic:
<;>

Goal state after:
case «0»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
j : Fin 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, ⋯⟩) j =
    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, ⋯⟩) j

case «1»
K : Type u_1
inst✝¹ : Field K
m : Matrix (Fin 2) (Fin 2) K
inst✝ : NeZero 2
j : Fin 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, ⋯⟩) j =
    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, ⋯⟩) j
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : 0 < ↑(GeneralLinearGroup.det g)
h✝ : 0 < ↑(GeneralLinearGroup.det h)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z) =
    (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z)

pp: case neg
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : 0 < ↑(GeneralLinearGroup.det g)
h✝ : ¬0 < ↑(GeneralLinearGroup.det h)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) (Complex.conjCAE z) = Complex.conjCAE ((ContinuousAlgEquiv.refl ℝ ℂ) z)

pp: case pos
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : ¬0 < ↑(GeneralLinearGroup.det g)
h✝ : 0 < ↑(GeneralLinearGroup.det h)
⊢ Complex.conjCAE ((ContinuousAlgEquiv.refl ℝ ℂ) z) = (ContinuousAlgEquiv.refl ℝ ℂ) (Complex.conjCAE z)

pp: case neg
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : ¬0 < ↑(GeneralLinearGroup.det g)
h✝ : ¬0 < ↑(GeneralLinearGroup.det h)
⊢ Complex.conjCAE (Complex.conjCAE z) = Complex.conjCAE (Complex.conjCAE z)

Tactic:
<;>

Goal state after:
case pos
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : 0 < ↑(GeneralLinearGroup.det g)
h✝ : 0 < ↑(GeneralLinearGroup.det h)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z) =
    (ContinuousAlgEquiv.refl ℝ ℂ) ((ContinuousAlgEquiv.refl ℝ ℂ) z)

case neg
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : 0 < ↑(GeneralLinearGroup.det g)
h✝ : ¬0 < ↑(GeneralLinearGroup.det h)
⊢ (ContinuousAlgEquiv.refl ℝ ℂ) (Complex.conjCAE z) = Complex.conjCAE ((ContinuousAlgEquiv.refl ℝ ℂ) z)

case pos
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : ¬0 < ↑(GeneralLinearGroup.det g)
h✝ : 0 < ↑(GeneralLinearGroup.det h)
⊢ Complex.conjCAE ((ContinuousAlgEquiv.refl ℝ ℂ) z) = (ContinuousAlgEquiv.refl ℝ ℂ) (Complex.conjCAE z)

case neg
g h : GL (Fin 2) ℝ
z : ℂ
h✝¹ : ¬0 < ↑(GeneralLinearGroup.det g)
h✝ : ¬0 < ↑(GeneralLinearGroup.det h)
⊢ Complex.conjCAE (Complex.conjCAE z) = Complex.conjCAE (Complex.conjCAE z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction

Goal state before:
pp: case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ ‖(ContinuousAlgEquiv.refl ℝ ℂ) z‖ = ‖z‖

pp: case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ ‖Complex.conjCAE z‖ = ‖z‖

Tactic:
<;>

Goal state after:
case pos
g : GL (Fin 2) ℝ
z : ℂ
h✝ : 0 < ↑(GeneralLinearGroup.det g)
⊢ ‖(ContinuousAlgEquiv.refl ℝ ℂ) z‖ = ‖z‖

case neg
g : GL (Fin 2) ℝ
z : ℂ
h✝ : ¬0 < ↑(GeneralLinearGroup.det g)
⊢ ‖Complex.conjCAE z‖ = ‖z‖
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)

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 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)

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.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:
have : (4 : K) ≠ 0 := by simpa [show (4 : K) = 2 ^ 2 by norm_num] using NeZero.ne _

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
this : 4 ≠ 0
⊢ m.discr = 0
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp.«0»
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
hd : ↑g 1 1 = ↑g 0 0
j : Fin 2
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case mp.«1»
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
hd : ↑g 1 1 = ↑g 0 0
j : Fin 2
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case mp.«0»
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
hd : ↑g 1 1 = ↑g 0 0
j : Fin 2
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨0, ⋯⟩) j = ↑g ((fun i ↦ i) ⟨0, ⋯⟩) j

case mp.«1»
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
hd : ↑g 1 1 = ↑g 0 0
j : Fin 2
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨1, ⋯⟩) j = ↑g ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp.«0».«0»
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
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case mp.«0».«1»
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
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case mp.«1».«0»
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
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case mp.«1».«1»
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
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case mp.«0».«0»
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
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case mp.«0».«1»
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
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case mp.«1».«0»
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
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case mp.«1».«1»
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
hd : ↑g 1 1 = ↑g 0 0
⊢ (Matrix.scalar (Fin 2)) (↑g 0 0) ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩) =
    ↑g ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Topology

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

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

Tactic:
<;>

Goal state after:
case refine_2.refine_1
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ num g ↑x

case refine_2.refine_2
g : GL (Fin 2) ℝ
⊢ Continuous fun x ↦ denom g ↑x
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))
⊢ 0 ≤ 2 / 3

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))
⊢ 2 / 3 < 1

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))
⊢ 0 ≤ 2 / 3

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))
⊢ 2 / 3 < 1
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo

Goal state before:
pp: case mp.f
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
⊢ ↑g 1 1 = 1 → ∃ x, x ≠ 0 ∧ g = upperRightHom x

pp: case mp.g
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
⊢ ↑g 1 1 = -1 → ∃ x, x ≠ 0 ∧ g = -upperRightHom x

Tactic:
<;>

Goal state after:
case mp.f
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
⊢ ↑g 1 1 = 1 → ∃ x, x ≠ 0 ∧ g = upperRightHom x

case mp.g
K : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
h_det : det g = 1 ∨ det g = -1
hg10 : ↑g 1 0 = 0
hg00 : ↑g 0 0 = ↑g 1 1
hg01 : ↑g 0 1 ≠ 0
this : ↑g 1 1 ^ 2 = 1
⊢ ↑g 1 1 = -1 → ∃ x, x ≠ 0 ∧ g = -upperRightHom x