mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

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

Tactic:
]

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

Goal state before:
pp: z : ℍ
r : ℝ
⊢ |(↑(z.center r)).im - (↑z).im| = z.im * Real.cosh r - z.im

Tactic:
]

Goal state after:
z : ℍ
r : ℝ
⊢ |(↑(z.center r)).im - (↑z).im| = z.im * Real.cosh r - z.im
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x ↦ sinh x - x) x

Tactic:
]

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ 0 < deriv (fun x ↦ sinh x - x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case refine_2
x : ℝ
hx : 0 < x
⊢ x ≠ 0

pp: case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

pp: case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x

Tactic:
]

Goal state after:
case refine_2
x : ℝ
hx : 0 < x
⊢ x ≠ 0

case refine_2.hf
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ sinh x

case refine_2.hg
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ (fun x ↦ x) x
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) sinh = iteratedDeriv n cosh
⊢ deriv (iteratedDeriv n cosh) = deriv (iteratedDeriv n cosh)

Tactic:
]

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

Goal state before:
pp: case succ
n : ℕ
ih : iteratedDeriv (n + 1) cosh = iteratedDeriv n sinh
⊢ deriv (iteratedDeriv n sinh) = deriv (iteratedDeriv n sinh)

Tactic:
]

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

Goal state before:
pp: x✝ : ℂ
⊢ sinh x✝ / cosh x✝ = sinh x✝ / cosh x✝

Tactic:
]

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

Goal state before:
pp: x✝ : ℝ
⊢ sinh x✝ / cosh x✝ = sinh x✝ / cosh x✝

Tactic:
]

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

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|

pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z).re = (↑(w.center |log (z.im / w.im)|)).re

Tactic:
]

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|

z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ (↑z).re = (↑(w.center |log (z.im / w.im)|)).re
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = |w.im| * |(z.im / w.im - w.im / z.im) / 2|

Tactic:
]

Goal state after:
z w : ℍ
h : z.re = w.re
h₀ : 0 < z.im / w.im
⊢ dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = |w.im| * |(z.im / w.im - w.im / z.im) / 2|
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ log z.im - log w.im ≤ dist z w

Tactic:
]

Goal state after:
z w : ℍ
⊢ log z.im - log w.im ≤ dist z w
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
⊢ w.im * (rexp (dist z w) - 1) = w.im * (rexp (dist z w) - 1)

Tactic:
]

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

Goal state before:
pp: z w : ℍ
⊢ w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)

Tactic:
]

Goal state after:
z w : ℍ
⊢ w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case refine_2
z✝ w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 ↑z)

Tactic:
]

Goal state after:
case refine_2
z✝ w : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
⊢ 𝓝 z ≤ comap UpperHalfPlane.coe (𝓝 ↑z)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case refine_2
z✝ w✝ : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
w : ℍ
hw : w ∈ ball z (log (R / z.im + 1))
⊢ dist w z < log (R / z.im + 1)

Tactic:
]

Goal state after:
case refine_2
z✝ w✝ : ℍ
r : ℝ
this : MetricSpace ℍ := metricSpaceAux
z : ℍ
R : ℝ
hR : 0 < R
h₁ : 1 < R / z.im + 1
h₀ : 0 < R / z.im + 1
w : ℍ
hw : w ∈ ball z (log (R / z.im + 1))
⊢ dist w z < log (R / z.im + 1)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z : ℍ
r : ℝ
w : ℂ
h : dist w ↑(z.center r) ≤ z.im * Real.sinh r
⊢ dist w ↑(z.center r) ≤ z.im * Real.sinh r

Tactic:
]

Goal state after:
z : ℍ
r : ℝ
w : ℂ
h : dist w ↑(z.center r) ≤ z.im * Real.sinh r
⊢ dist w ↑(z.center r) ≤ z.im * Real.sinh r
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Epi (↾⇑(ConcreteCategory.hom f))
⊢ Epi f

Tactic:
]

Goal state after:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
hf : Epi (↾⇑(ConcreteCategory.hom f))
⊢ Epi f
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono (↾⇑(ConcreteCategory.hom f)) → Mono f

Tactic:
]

Goal state after:
case mpr
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
⊢ Mono (↾⇑(ConcreteCategory.hom f)) → Mono f
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ ∀ (s : Set ((fun X ↦ ↑X.toTop) X)), IsClosed s → IsClosed (⇑E.symm ⁻¹' s)

Tactic:
]

Goal state after:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
⊢ ∀ (s : Set ((fun X ↦ ↑X.toTop) X)), IsClosed s → IsClosed (⇑E.symm ⁻¹' s)
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
S : Set ((fun X ↦ ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E '' S)

Tactic:
]

Goal state after:
P : TopCat → Prop
X Y : CompHausLike P
f : X ⟶ Y
bij : Function.Bijective ⇑(ConcreteCategory.hom f)
E : (fun X ↦ ↑X.toTop) X ≃ (fun X ↦ ↑X.toTop) Y := Equiv.ofBijective (⇑(ConcreteCategory.hom f)) bij
S : Set ((fun X ↦ ↑X.toTop) X)
hS : IsClosed S
⊢ IsClosed (⇑E '' S)
Module: Mathlib.Topology.Category.CompHausLike.Basic

Goal state before:
pp: P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget (CompHausLike P)).map f))
⊢ IsIso f

Tactic:
]

Goal state after:
P : TopCat → Prop
X : Type u
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : T2Space X
inst✝ : HasProp P X
A B : CompHausLike P
f : A ⟶ B
hf : Function.Bijective ⇑(ConcreteCategory.hom ((forget (CompHausLike P)).map f))
⊢ IsIso f
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
s : Set α
⊢ IsOpen {u | s ∈ u}ᶜ

Tactic:
]

Goal state after:
α : Type u
s : Set α
⊢ IsOpen {u | s ∈ u}ᶜ
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x

Tactic:
]

Goal state after:
α : Type u
u : Ultrafilter (Ultrafilter α)
x : Ultrafilter α
⊢ ↑u ≤ 𝓝 x ↔ ↑(joinM u) ≤ ↑x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z✝ w : ℍ
r✝ : ℝ
z : ℍ
r : ℝ
⊢ IsCompact (closedBall (↑(z.center r)) (z.im * Real.sinh r))

Tactic:
]

Goal state after:
z✝ w : ℍ
r✝ : ℝ
z : ℍ
r : ℝ
⊢ IsCompact (closedBall (↑(z.center r)) (z.im * Real.sinh r))
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
⊢ ∀ (x : Ultrafilter α), connectedComponent x = {x}

Tactic:
]

Goal state after:
α : Type u
⊢ ∀ (x : Ultrafilter α), connectedComponent x = {x}
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ ↑B ≤ ↑A

Tactic:
]

Goal state after:
α : Type u
A B : Ultrafilter α
hB : B ∈ connectedComponent A
⊢ ↑B ≤ ↑A
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: a y₁ y₂ : ℝ
⊢ dist (log { coe := { re := a, im := rexp y₁ }, coe_im_pos := ⋯ }.im)
      (log { coe := { re := a, im := rexp y₂ }, coe_im_pos := ⋯ }.im) =
    dist y₁ y₂

pp: a y₁ y₂ : ℝ
⊢ { coe := { re := a, im := rexp y₁ }, coe_im_pos := ⋯ }.re = { coe := { re := a, im := rexp y₂ }, coe_im_pos := ⋯ }.re

Tactic:
]

Goal state after:
a y₁ y₂ : ℝ
⊢ dist (log { coe := { re := a, im := rexp y₁ }, coe_im_pos := ⋯ }.im)
      (log { coe := { re := a, im := rexp y₂ }, coe_im_pos := ⋯ }.im) =
    dist y₁ y₂

a y₁ y₂ : ℝ
⊢ { coe := { re := a, im := rexp y₁ }, coe_im_pos := ⋯ }.re = { coe := { re := a, im := rexp y₂ }, coe_im_pos := ⋯ }.re
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
A B : Ultrafilter α
hB : ∀ (i : { s // IsClopen s ∧ A ∈ s }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B

Tactic:
]

Goal state after:
α : Type u
A B : Ultrafilter α
hB : ∀ (i : { s // IsClopen s ∧ A ∈ s }), B ∈ ↑i
s : Set α
hs : s ∈ ↑A
⊢ s ∈ ↑B
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ b = joinM (map pure b)

Tactic:
]

Goal state after:
α : Type u
b : Ultrafilter α
⊢ b = joinM (map pure b)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
⊢ comap pure (⨅ s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 s) ≤ ↑b

Tactic:
]

Goal state after:
α : Type u
b : Ultrafilter α
⊢ comap pure (⨅ s ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 s) ≤ ↑b
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ 𝓟 s

Tactic:
]

Goal state after:
α : Type u
b : Ultrafilter α
s : Set α
hs : s ∈ ↑b
⊢ ⨅ i ∈ {s | b ∈ s ∧ s ∈ ultrafilterBasis α}, 𝓟 (pure ⁻¹' i) ≤ 𝓟 s
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case e_a
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ |↑a| * dist ↑y₁ ↑y₂ / (|↑a| * (2 * √(y₁.im * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))

Tactic:
]

Goal state after:
case e_a
a : { x // 0 < x }
y₁ y₂ : ℍ
⊢ |↑a| * dist ↑y₁ ↑y₂ / (|↑a| * (2 * √(y₁.im * y₂.im))) = dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ ↑(Ultrafilter.map f b)

Tactic:
]

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
⊢ univ ∈ ↑(Ultrafilter.map f b)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)

Tactic:
]

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
⊢ ↑(Ultrafilter.map f b) ≤ 𝓝 (Ultrafilter.extend f b)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map f ↑b

Tactic:
]

Goal state after:
α : Type u
γ : Type u_1
inst✝² : TopologicalSpace γ
inst✝¹ : T2Space γ
inst✝ : CompactSpace γ
f : α → γ
b : Ultrafilter α
c : γ
h : Ultrafilter.extend f b = c
b' : Ultrafilter (Ultrafilter α) := Ultrafilter.map pure b
t : ↑b' ≤ 𝓝 b
this : Tendsto (Ultrafilter.extend f) (𝓝 b) (𝓝 (Ultrafilter.extend f b))
⊢ ↑(Ultrafilter.map f b) ≤ map f ↑b
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g >>= pure = joinM (Ultrafilter.map pure (g >>= pure))

Tactic:
]

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x : α
g : Ultrafilter α
gx : ↑g ≤ 𝓝 x
⊢ g >>= pure = joinM (Ultrafilter.map pure (g >>= pure))
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
⊢ ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)

Tactic:
]

Goal state after:
case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
⊢ ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ map g ↑G ≤ 𝓝 (g x)

Tactic:
]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ map g ↑G ≤ 𝓝 (g x)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
h :
  (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
𝒰 : Ultrafilter (G × X)
x₁ x₂ : X
h' : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
gx : G × X
hgx2 : ↑𝒰 ≤ 𝓝 gx
hgx1 : gx.1 • gx.2 = x₁ ∧ gx.2 = x₂
⊢ x₁ = x₁

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ map g ↑F ≤ 𝓝 (g x)

Tactic:
]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
F G : Ultrafilter α
x : α
hF : map g ↑F ≤ 𝓝 (g x)
hG : map g ↑G ≤ 𝓝 (g x)
⊢ map g ↑F ≤ 𝓝 (g x)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

Tactic:
]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : preStoneCechUnit a = preStoneCechUnit b
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
⊢ (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
⊢ (Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)) ∧
    ∀ ⦃𝒰 : Ultrafilter (G × X)⦄ ⦃y : X × X⦄,
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 y) → ∃ x, (x.1 • x.2, x.2) = y ∧ ↑𝒰 ≤ 𝓝 x
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: z w : ℍ
r : ℝ
g : SL(2, ℝ)
y₁ y₂ : ℍ
h₁ : 0 ≤ y₁.im * y₂.im
h₂ : ‖↑y₁ * ↑y₂‖ ≠ 0
⊢ 2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im))) = 2 * arsinh (dist ↑y₁ ↑y₂ / (2 * √(y₁.im * y₂.im)))

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : Relation.EqvGen (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure a) (pure b)
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)

Tactic:
]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
h : Relation.EqvGen (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) (pure a) (pure b)
e : Ultrafilter.extend g ∘ pure = g
⊢ Ultrafilter.extend g (pure a) = Ultrafilter.extend g (pure b)
Module: Mathlib.Analysis.Complex.UpperHalfPlane.Metric

Goal state before:
pp: case pos
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ↑g 1 0 = 0
u : { x // 0 < x }
v : ℝ
h : (fun x ↦ g • x) = (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x
⊢ Isometry ((fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x)

Tactic:
]

Goal state after:
case pos
z w : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ↑g 1 0 = 0
u : { x // 0 < x }
v : ℝ
h : (fun x ↦ g • x) = (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x
⊢ Isometry ((fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: case symm
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
a b : α
e : Ultrafilter.extend g ∘ pure = g
F G x y : Ultrafilter α
a✝ : Relation.EqvGen (fun F G ↦ ∃ x, ↑F ≤ 𝓝 x ∧ ↑G ≤ 𝓝 x) x y
h : Ultrafilter.extend g x = Ultrafilter.extend g y
⊢ Ultrafilter.extend g y = Ultrafilter.extend g y

Tactic:
]

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

Goal state before:
pp: case neg
z w✝ : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ¬↑g 1 0 = 0
u : { x // 0 < x }
v w : ℝ
h : (fun x ↦ g • x) = (fun x ↦ w +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x
⊢ Isometry ((fun x ↦ w +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x)

Tactic:
]

Goal state after:
case neg
z w✝ : ℍ
r : ℝ
g : SL(2, ℝ)
h₀ : Isometry fun z ↦ ModularGroup.S • z
hc : ¬↑g 1 0 = 0
u : { x // 0 < x }
v w : ℝ
h : (fun x ↦ g • x) = (fun x ↦ w +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x
⊢ Isometry ((fun x ↦ w +ᵥ x) ∘ (fun x ↦ ModularGroup.S • x) ∘ (fun x ↦ v +ᵥ x) ∘ fun x ↦ u • x)
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
x : α
⊢ preStoneCechExtend hg (preStoneCechUnit x) = g x

Tactic:
]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
g : α → β
hg : Continuous[inst✝³, inst✝²] g
inst✝ : CompactSpace β
x : α
⊢ preStoneCechExtend hg (preStoneCechUnit x) = g x
Module: Mathlib.Topology.Compactification.StoneCech

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous[inst✝³, inst✝²] f
h : stoneCechUnit a = stoneCechUnit b
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b

Tactic:
]

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
β : Type v
inst✝² : TopologicalSpace β
inst✝¹ : T2Space β
inst✝ : CompactSpace β
a b : α
f : α → β
hcf : Continuous[inst✝³, inst✝²] f
h : stoneCechUnit a = stoneCechUnit b
⊢ (stoneCechExtend hcf ∘ stoneCechUnit) a = (stoneCechExtend hcf ∘ stoneCechUnit) b
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝¹ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x✝ : X × X
x₁ x₂ : X
hxx : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰) (𝓝 g)
⊢ Tendsto fst (↑𝒰) (𝓝 g) ∧ Tendsto snd (↑𝒰) (𝓝 x₂)

Tactic:
]

Goal state after:
case refine_2
G : Type u_1
X : Type u_2
inst✝³ : Group G
inst✝² : MulAction G X
inst✝¹ : TopologicalSpace G
inst✝ : TopologicalSpace X
x✝¹ :
  ContinuousSMul G X ∧
    ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
      Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
cont : ContinuousSMul G X
h :
  ∀ (𝒰 : Ultrafilter (G × X)) (x₁ x₂ : X),
    Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂)) → ∃ g, g • x₂ = x₁ ∧ Tendsto fst (↑𝒰) (𝓝 g)
𝒰 : Ultrafilter (G × X)
x✝ : X × X
x₁ x₂ : X
hxx : Tendsto (fun gx ↦ (gx.1 • gx.2, gx.2)) (↑𝒰) (𝓝 (x₁, x₂))
g : G
hg1 : g • x₂ = x₁
hg2 : Tendsto fst (↑𝒰) (𝓝 g)
⊢ Tendsto fst (↑𝒰) (𝓝 g) ∧ Tendsto snd (↑𝒰) (𝓝 x₂)