mathlib-initiative/mathlib-tactics huggingface dataset:
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
hg11 : ↑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
hg11 : ↑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
hg11 : ↑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
hg11 : ↑g 1 1 = -1
⊢ ∃ x, x ≠ 0 ∧ g = -upperRightHom x
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

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

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
⊢ ↑(upperRightHom x) 0 0 = ↑(upperRightHom x) 1 1 ∧ ↑(upperRightHom x) 0 1 ≠ 0

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
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inl
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
b : ℝ
hb : IsLUB (range ⇑f) b
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
x : X
ha : IsGLB (range ⇑f) (f x)
hmem : ∀ (x_1 : X), f x_1 ∈ Icc (f x) b
hle : f x ≤ b
hlt : f x < b
c : ℝ := (f x + b) / 2
hac : f x < c
hcb : c < b
hsub : c - f x = b - c
hg_mem : ∀ (y : Y), g y ∈ Icc (f x) b
⊢ ∃ g, (∀ (y : Y), ∃ x, g y ∈ Icc (f x) b) ∧ ⇑g ∘ e = ⇑f

Tactic:
exact ⟨g, fun y => ⟨x, hg_mem _⟩, hgf⟩

Goal state after:
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «0»
z : ℂ
i : Fin 2
⊢ ![z.re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re - z.im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im,
        z.re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im + z.im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
z : ℂ
i : Fin 2
⊢ ![z.re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re - z.im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im,
        z.re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im + z.im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case «0»
z : ℂ
i : Fin 2
⊢ ![z.re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re - z.im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im,
        z.re * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).im + z.im * (![1, I] ((fun i ↦ i) ⟨0, ⋯⟩)).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun i ↦ i) ⟨0, ⋯⟩)

case «1»
z : ℂ
i : Fin 2
⊢ ![z.re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re - z.im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im,
        z.re * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).im + z.im * (![1, I] ((fun i ↦ i) ⟨1, ⋯⟩)).re]
      i =
    ![![z.re, -z.im], ![z.im, z.re]] i ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «0».«0»
z : ℂ
⊢ ![z.re, z.im] ((fun i ↦ i) ⟨0, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨0, ⋯⟩) 0

pp: case «0».«1»
z : ℂ
⊢ ![z.re, z.im] ((fun i ↦ i) ⟨1, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨1, ⋯⟩) 0

Tactic:
<;>

Goal state after:
case «0».«0»
z : ℂ
⊢ ![z.re, z.im] ((fun i ↦ i) ⟨0, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨0, ⋯⟩) 0

case «0».«1»
z : ℂ
⊢ ![z.re, z.im] ((fun i ↦ i) ⟨1, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨1, ⋯⟩) 0
Module: Mathlib.RingTheory.Complex

Goal state before:
pp: case «1».«0»
z : ℂ
⊢ ![-z.im, z.re] ((fun i ↦ i) ⟨0, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨0, ⋯⟩) 1

pp: case «1».«1»
z : ℂ
⊢ ![-z.im, z.re] ((fun i ↦ i) ⟨1, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨1, ⋯⟩) 1

Tactic:
<;>

Goal state after:
case «1».«0»
z : ℂ
⊢ ![-z.im, z.re] ((fun i ↦ i) ⟨0, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨0, ⋯⟩) 1

case «1».«1»
z : ℂ
⊢ ![-z.im, z.re] ((fun i ↦ i) ⟨1, ⋯⟩) = ![![z.re, -z.im], ![z.im, z.re]] ((fun i ↦ i) ⟨1, ⋯⟩) 1
Module: Mathlib.Topology.TietzeExtension

Goal state before:
pp: case inr.inl
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
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
hlt : a < b
c : ℝ := (a + b) / 2
hac : a < c
hcb : c < b
hsub : c - a = b - c
g : Y →ᵇ ℝ
hg_mem : ∀ (y : Y), g y ∈ Icc a b
ha' : ¬∃ x, f x = a
hd : Disjoint (range e ∪ ⇑g ⁻¹' Ici c) (⇑g ⁻¹' {a})
dg : Y →ᵇ ℝ
dg0 : EqOn (⇑dg) (Function.const Y 0) (range e ∪ ⇑g ⁻¹' Ici c)
dga : EqOn (⇑dg) (Function.const Y (c - a)) (⇑g ⁻¹' {a})
dgmem : ∀ (x : Y), dg x ∈ Icc 0 (c - a)
hgf : ∀ (x : X), (g + dg) (e x) = f x
y : Y
hay : a < (g + dg) y
x : X
left✝ : a ≤ f x
hxy : f x < (g + dg) y
hc : c ≤ g y
⊢ (g + dg) y ≤ b

Tactic:
simp [dg0 (Or.inr hc), (hg_mem y).2]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp { a // (a = k) = True } { a // (a = k) = True } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) True).map ⇑f)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det

Tactic:
mul_auxMat_toSquareBlock_eq,

Goal state after:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ ((Matrix.comp { a // (a = k) = True } { a // (a = k) = True } n n R) ((M k k • 1).map ⇑f)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det =
    (f (M k k)).det *
      ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R)
          (((M * auxMat M k).toSquareBlock (fun x ↦ x = k) False).map ⇑f)).det
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ ContinuousAt (↑ofComplex) z

Tactic:
ContinuousAt,

Goal state after:
case left
n : ℕ∞ω
z : ℂ
hz : 0 < z.im
⊢ Tendsto (↑ofComplex) (𝓝 z) (𝓝 (↑ofComplex z))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Measure

Goal state before:
pp: case inl
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
h : (↑g).det < 0
⊢ ‖↑(SignType.sign (↑g).det)‖₊ = 1

pp: case inr
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
h : 0 < (↑g).det
⊢ ‖↑(SignType.sign (↑g).det)‖₊ = 1

Tactic:
<;>

Goal state after:
case inl
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
h : (↑g).det < 0
⊢ ‖↑(SignType.sign (↑g).det)‖₊ = 1

case inr
g : GL (Fin 2) ℝ
s : Set ℍ
hs : MeasurableSet s
hinj : Set.InjOn (fun z ↦ ↑(g • ↑ofComplex z)) (UpperHalfPlane.coe '' s)
main :
  ∫⁻ (x : ℂ) in (fun z ↦ ↑(g • ↑ofComplex z)) '' UpperHalfPlane.coe '' s, ↑((1 / ‖x.im‖₊) ^ 2) =
    ∫⁻ (x : ℂ) in UpperHalfPlane.coe '' s,
      ENNReal.ofReal |(smulFDeriv g x).det| * ↑((1 / ‖(↑(g • ↑ofComplex x)).im‖₊) ^ 2)
τ : ℍ
h : 0 < (↑g).det
⊢ ‖↑(SignType.sign (↑g).det)‖₊ = 1
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: case neg
g : GL (Fin 2) ℝ
z x✝ : ℂ
hg : ¬0 < (↑g).det
⊢ (smulFDeriv (J * g) z) x✝ = (-↑Complex.conjCLE ∘SL smulFDeriv g z) x✝

Tactic:
· simp [smulFDeriv, σ, hg, g.det_ne_zero.lt_or_gt.resolve_right hg, neg_div]

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

Goal state before:
pp: case inr
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ¬0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ

Tactic:
replace hg := g.det.ne_zero.lt_or_gt.resolve_right hg

Goal state after:
case inr
g : GL (Fin 2) ℝ
τ : ℍ
this :
  ∀ (g : GL (Fin 2) ℝ),
    0 < ↑(Matrix.GeneralLinearGroup.det g) → HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
⊢ HasStrictFDerivAt (fun z ↦ ↑(g • ↑ofComplex z)) (smulFDeriv g ↑τ) ↑τ
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ 1 + 2 * dist ↑z ↑w ^ 2 / (2 * (2 * (z.im * w.im))) = 1 + dist ↑z ↑w ^ 2 / (2 * (z.im * w.im))

pp: z w : ℍ
⊢ 0 ≤ z.im * w.im

Tactic:
mul_div_mul_left

Goal state after:
z w : ℍ
⊢ 1 + dist ↑z ↑w ^ 2 / (2 * (z.im * w.im)) = 1 + dist ↑z ↑w ^ 2 / (2 * (z.im * w.im))

case hc
z w : ℍ
⊢ 2 ≠ 0

z w : ℍ
⊢ 0 ≤ z.im * w.im
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case hc
z w : ℍ
⊢ 2 ≠ 0

pp: z w : ℍ
⊢ 0 ≤ z.im * w.im

Tactic:
<;>

Goal state after:
case hc
z w : ℍ
⊢ 2 ≠ 0

z w : ℍ
⊢ 0 ≤ z.im * w.im
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hR : R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0

pp: case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hR : ¬R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0

Tactic:
<;>

Goal state after:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hR : R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0

case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
hR : ¬R = 0
⊢ inversion c R x = c ↔ x = c ∨ R = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case e_a.e_a
a b c : ℍ
⊢ 0 ≤ b.im

pp: case e_a.e_a.hx
a b c : ℍ
⊢ 0 ≤ a.im

pp: case e_a.e_a.hx
a b c : ℍ
⊢ 0 ≤ b.im

pp: case e_a.e_a.hx
a b c : ℍ
⊢ 0 ≤ a.im

Tactic:
<;>

Goal state after:
case e_a.e_a
a b c : ℍ
⊢ 0 ≤ b.im

case e_a.e_a.hx
a b c : ℍ
⊢ 0 ≤ a.im

case e_a.e_a.hx
a b c : ℍ
⊢ 0 ≤ b.im

case e_a.e_a.hx
a b c : ℍ
⊢ 0 ≤ a.im
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) = 1 / (dist b a * dist d a) * dist b d

pp: case e'_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a)) =
    1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d

Tactic:
<;>

Goal state after:
case e'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ dist a c * dist b d / (dist b a * (dist c a * dist d a)) = 1 / (dist b a * dist d a) * dist b d

case e'_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c d : P
hb : 0 < dist b a
hc : 0 < dist c a
hd : 0 < dist d a
H : 1 / (dist b a * dist d a) * dist b d ≤ 1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
⊢ (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a)) =
    1 / (dist b a * dist c a) * dist b c + 1 / (dist c a * dist d a) * dist c d
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case hre
z : ℍ
⊢ (z.center 0).re = z.re

pp: case him
z : ℍ
⊢ (z.center 0).im = z.im

Tactic:
<;>

Goal state after:
case hre
z : ℍ
⊢ (z.center 0).re = z.re

case him
z : ℍ
⊢ (z.center 0).im = z.im
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case inl
x : ℝ
h✝ : x ≤ 0
⊢ |sinh x| = sinh |x|

pp: case inr
x : ℝ
h✝ : 0 ≤ x
⊢ |sinh x| = sinh |x|

Tactic:
<;>

Goal state after:
case inl
x : ℝ
h✝ : x ≤ 0
⊢ |sinh x| = sinh |x|

case inr
x : ℝ
h✝ : 0 ≤ x
⊢ |sinh x| = sinh |x|
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case left
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[Units.instTopologicalSpaceUnits, inst✝¹] (Units.val ∘ ⇑det)

pp: case right
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[Units.instTopologicalSpaceUnits, inst✝¹] fun x ↦ ↑(det x⁻¹)

Tactic:
<;>

Goal state after:
case left
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[Units.instTopologicalSpaceUnits, inst✝¹] (Units.val ∘ ⇑det)

case right
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[Units.instTopologicalSpaceUnits, inst✝¹] fun x ↦ ↑(det x⁻¹)
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case left
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, x; 0, 1]

pp: case right
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, -x; 0, 1]

Tactic:
<;>

Goal state after:
case left
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, x; 0, 1]

case right
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, instTopologicalSpaceMatrix] fun x ↦ !![1, -x; 0, 1]
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case left.«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case left.«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case left.«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case left.«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case left.«0».«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case left.«0».«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case left.«1».«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case left.«1».«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case left.«0».«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case left.«0».«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case left.«1».«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case left.«1».«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case right.«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

pp: case right.«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

Tactic:
<;>

Goal state after:
case right.«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case right.«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
j : Fin 2
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case right.«0».«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case right.«0».«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

pp: case right.«1».«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case right.«1».«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
<;>

Goal state after:
case right.«0».«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case right.«0».«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)

case right.«1».«0»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨0, ⋯⟩)

case right.«1».«1»
R : Type u_4
inst✝² : Ring R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[inst✝¹, inst✝¹] fun a ↦ !![1, -a; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: n : Type u_1
R : Type u_2
S : Type u_3
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : CommRing S
inst✝ : TopologicalSpace S
f : R →+* S
hf : Continuous[inst✝², inst✝] ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] (Subtype.val ∘ ⇑(map f))

Tactic:
exact (continuous_id.matrix_map hf).comp continuous_subtype_val

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Matrix

Goal state before:
pp: case left
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] (Units.val ∘ ⇑toGL)

pp: case right
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun x ↦ ↑(toGL x⁻¹)

Tactic:
<;>

Goal state after:
case left
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] (Units.val ∘ ⇑toGL)

case right
n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
⊢ Continuous[instTopologicalSpace, instTopologicalSpaceMatrix] fun x ↦ ↑(toGL x⁻¹)