mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Norm.Transitivity

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

Tactic:
]

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g).det / denom g ↑τ ^ 2 ≠ 0

Tactic:
]

Goal state after:
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
τ : ℍ
⊢ ↑(↑g).det / denom g ↑τ ^ 2 ≠ 0
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
F : Type u_8
inst✝¹ : Field F
inst✝ : Algebra K F
x : L
hF : (Polynomial.map (algebraMap K F) (minpoly K x)).Splits
⊢ ((minpoly K x).aroots F).prod ^ finrank (↥K⟮x⟯) L = ((minpoly K x).aroots F).prod ^ finrank (↥K⟮x⟯) L

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ -x < √(1 + x ^ 2)

Tactic:
]

Goal state after:
x : ℝ
⊢ -x < √(1 + x ^ 2)
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ -x + √(1 + (-x) ^ 2) = (x + √(1 + x ^ 2))⁻¹

Tactic:
]

Goal state after:
x : ℝ
⊢ -x + √(1 + (-x) ^ 2) = (x + √(1 + x ^ 2))⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ 1 = 1

pp: x : ℝ
⊢ 0 ≤ 1 + x ^ 2

Tactic:
]

Goal state after:
x : ℝ
⊢ 0 ≤ 1 + x ^ 2
Module: Mathlib.RingTheory.Norm.Transitivity

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ (∏ σ, σ (adjoin.powerBasis hx).gen) ^ finrank (↥K⟮x⟯) L = ∏ σ, σ x

pp: L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ IsSeparable K (adjoin.powerBasis hx).gen

Tactic:
]

Goal state after:
L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ (∏ σ, σ (adjoin.powerBasis hx).gen) ^ finrank (↥K⟮x⟯) L = ∏ σ, σ x

L : Type u_6
K : Type u_7
inst✝⁷ : Field K
inst✝⁶ : Field L
inst✝⁵ : Algebra K L
E : Type u_9
inst✝⁴ : Field E
inst✝³ : Algebra K E
inst✝² : FiniteDimensional K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : IsAlgClosed E
x : L
hx : IsIntegral K x
⊢ IsSeparable K (adjoin.powerBasis hx).gen
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x

Tactic:
]

Goal state after:
x : ℝ
⊢ (x + √(1 + x ^ 2) - (-x + √(1 + x ^ 2))) / 2 = x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Manifold

Goal state before:
pp: f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ meromorphicOrderAt F (G ↑τ) = meromorphicOrderAt (fun z ↦ f (↑ofComplex z)) ↑(g • τ)

pp: case hg
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ AnalyticAt ℂ G ↑τ

pp: case hg'
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ deriv G ↑τ ≠ 0

Tactic:
]

Goal state after:
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ meromorphicOrderAt F (G ↑τ) = meromorphicOrderAt (fun z ↦ f (↑ofComplex z)) ↑(g • τ)

case hg
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ AnalyticAt ℂ G ↑τ

case hg'
f : ℍ → ℂ
τ : ℍ
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
G : ℂ → ℂ := fun z ↦ ↑(g • ↑ofComplex z)
F : ℂ → ℂ := fun z ↦ f (↑ofComplex z)
this : (fun z ↦ f (g • ↑ofComplex z)) = F ∘ G
⊢ deriv G ↑τ ≠ 0
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ √(1 + x ^ 2) = √(1 + x ^ 2)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

Goal state before:
pp: x : ℝ
⊢ x / √(1 + x ^ 2) = x / √(1 + x ^ 2)

Tactic:
]

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

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) =
    ∏ x_1, (algebraMap L (AlgebraicClosure L)) (x_1 x)

Tactic:
]

Goal state after:
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) =
    ∏ x_1, (algebraMap L (AlgebraicClosure L)) (x_1 x)
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
]

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

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = ∏ x, ?f x

pp: case f
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L

pp: case h
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    ?f x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)

Tactic:
]

Goal state after:
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap L (AlgebraicClosure L)) ((algebraMap K L) ((norm K) x)) = ∏ x, ?f x

case f
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (L →ₐ[K] AlgebraicClosure L) → AlgebraicClosure L

case h
L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ ∀ (x_1 : L →ₐ[K] AlgebraicClosure L),
    ?f x_1 = (algebraMap L (AlgebraicClosure L)) (((Normal.algHomEquivAut K (AlgebraicClosure L) L) x_1) x)
Module: Mathlib.Analysis.SpecialFunctions.Arsinh

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

Tactic:
]

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

Goal state before:
pp: L : Type u_6
K : Type u_7
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : FiniteDimensional K L
inst✝ : IsGalois K L
x : L
⊢ (algebraMap K (AlgebraicClosure L)) ((norm K) x) = (algebraMap K (AlgebraicClosure L)) ((norm K) x)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ x = x

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ dist x c ≠ 0

Tactic:
]

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ dist x c ≠ 0
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ x ≠ c

Tactic:
]

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
hne : x ≠ c
⊢ x ≠ c
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

Tactic:
]

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

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

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

pp: z w : ℍ
⊢ (2 * √(z.im * w.im)) ^ 2 ≠ 0

pp: case ha
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

pp: case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))

Tactic:
]

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

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

z w : ℍ
⊢ (2 * √(z.im * w.im)) ^ 2 ≠ 0

case ha
z w : ℍ
⊢ 0 ≤ cosh (dist z w / 2)

case hb
z w : ℍ
⊢ 0 ≤ dist (↑z) ((starRingEnd ℂ) ↑w) / (2 * √(z.im * w.im))
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
⊢ x = x

Tactic:
]

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

Goal state before:
pp: z w : ℍ
⊢ dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w) = dist ↑z ↑w / dist (↑z) ((starRingEnd ℂ) ↑w)

pp: z w : ℍ
⊢ 2 * √(z.im * w.im) ≠ 0

Tactic:
]

Goal state after:
z w : ℍ
⊢ 2 * √(z.im * w.im) ≠ 0
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x : P
R : ℝ
⊢ R ^ 2 / dist x c = R ^ 2 / dist x c

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
R : ℝ
hR : R ≠ 0
x : P
⊢ x = x

Tactic:
]

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

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

Tactic:
]

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

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

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 inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ x = x

pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ R ^ 2 ≠ 0

Tactic:
]

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
x : P
hne : x ≠ c
⊢ R ^ 2 ≠ 0
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ R ^ 2 / (dist x c * (R ^ 2 / dist y c)) * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c

Tactic:
]

Goal state after:
case inr
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c x y : P
R : ℝ
hx : x ≠ c
hy : y ≠ c
hR : R ≠ 0
hy' : inversion c R y ≠ c
⊢ R ^ 2 / (dist x c * (R ^ 2 / dist y c)) * dist x (inversion c R y) * dist x c = dist x (inversion c R y) * dist y c
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (√(a.im * b.im) * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (√(a.im * c.im) * b.im))

Tactic:
]

Goal state after:
a b c : ℍ
⊢ (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (√(a.im * b.im) * √(b.im * c.im))) =
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist (↑a) ((starRingEnd ℂ) ↑b) * dist ↑b ↑c) /
      (2 * 2 * (√(a.im * c.im) * b.im))
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
⊢ dist b c * dist b d ≤ dist b c * dist b d

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ 0 ≤ dist c b * dist c d + dist b c * dist c d

Tactic:
]

Goal state after:
case inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ c
⊢ 0 ≤ dist c b * dist c d + dist b c * dist c d
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case e_a.e_a
a b c : ℍ
⊢ √a.im * √c.im * b.im = √a.im * √c.im * b.im

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 inr.inr.inl
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
b c d : P
hb : b ≠ d
hc : c ≠ d
⊢ dist b d * dist c d ≤ dist b d * dist c d

Tactic:
]

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

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (r / 2) ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (r / 2)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inr
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 : b ≠ a
hc : c ≠ a
hd : 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 a b * dist c d + dist b c * dist a d

Tactic:
]

Goal state after:
case inr.inr.inr
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 : b ≠ a
hc : c ≠ a
hd : 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 a b * dist c d + dist b c * dist a d
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inr
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 a b * dist c d + dist b c * dist a d

Tactic:
]

Goal state after:
case inr.inr.inr
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 a b * dist c d + dist b c * dist a d
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2) ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) = sinh (r / 2)

Tactic:
]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case inr.inr.inr
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)) ≤
    (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))

Tactic:
]

Goal state after:
case inr.inr.inr
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)) ≤
    (dist a b * dist c d + dist b c * dist a d) / (dist b a * (dist c a * dist d a))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w ^ 2 / (2 ^ 2 * (z.im * w.im)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * (z.im * w.im)) = sinh (r / 2) ^ 2

pp: z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ z.im * w.im

pp: case ha
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

pp: case hb
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)

Tactic:
]

Goal state after:
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ dist ↑z ↑w ^ 2 / (2 ^ 2 * (z.im * w.im)) = sinh (r / 2) ^ 2 ↔ dist ↑z ↑w ^ 2 / (4 * (z.im * w.im)) = sinh (r / 2) ^ 2

z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ z.im * w.im

case ha
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

case hb
z w : ℍ
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ sinh (r / 2)
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

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

Tactic:
]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (fun x ↦ dist c (inversion c R x)) (𝓝[≠] c) atTop
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝[≠] c) (𝓝 0) ∧ ∀ᶠ (n : P) in 𝓝[≠] c, dist c n ∈ Ioi 0

Tactic:
]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝[≠] c) (𝓝 0) ∧ ∀ᶠ (n : P) in 𝓝[≠] c, dist c n ∈ Ioi 0
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝 c) (𝓝 (dist c c))

Tactic:
]

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
R : ℝ
hR : R ≠ 0
⊢ Tendsto (dist c) (𝓝 c) (𝓝 (dist c c))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) / (2 * √(a.im * c.im)) ≤
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im))

pp: a b c : ℍ
⊢ 0 < dist (↑b) ((starRingEnd ℂ) ↑b)

Tactic:
]

Goal state after:
a b c : ℍ
⊢ dist ↑a ↑c * dist (↑b) ((starRingEnd ℂ) ↑b) / (2 * √(a.im * c.im)) ≤
    (dist ↑a ↑b * dist (↑c) ((starRingEnd ℂ) ↑b) + dist ↑b ↑c * dist (↑a) ((starRingEnd ℂ) ↑b)) / (2 * √(a.im * c.im))

a b c : ℍ
⊢ 0 < dist (↑b) ((starRingEnd ℂ) ↑b)
Module: Mathlib.Geometry.Euclidean.Inversion.Basic

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

Tactic:
]

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

Goal state before:
pp: a b c : ℍ
⊢ ¬(↑b).im = 0

Tactic:
]

Goal state after:
a b c : ℍ
⊢ ¬(↑b).im = 0
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))

Tactic:
]

Goal state after:
z w : ℍ
⊢ 0 ≤ dist ↑z ↑w / (2 * √(z.im * w.im))
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

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

Tactic:
]

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

Goal state before:
pp: z w : ℍ
r : ℝ
⊢ √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2) =
    √(2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp x + cexp (-x)) * 2⁻¹ = (cexp x + cexp (-x)) * 2⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case e'_9
x : ℂ
⊢ (cexp x + -cexp (-x)) * 2⁻¹ = (cexp x + -cexp (-x)) * 2⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: ⊢ ∀ (x : ℝ), 0 < cosh x

Tactic:
]

Goal state after:
⊢ ∀ (x : ℝ), 0 < cosh x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

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

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x

Tactic:
]

Goal state after:
x : ℝ
hx : 0 < x
⊢ 0 < deriv cosh x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + ?inr✝) ?inr✝ =
    cmp (2 * z.im * w.im * (Real.cosh (dist z w) - Real.cosh r) + (w.im * Real.sinh r) ^ 2) ((w.im * Real.sinh r) ^ 2)

pp: case inr
z w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
hr₀ : 0 ≤ r
hr₀' : 0 ≤ w.im * Real.sinh r
hzw₀ : 0 < 2 * z.im * w.im
⊢ ℝ

Tactic:
]

Goal state after: