mathlib-initiative/mathlib-tactics huggingface dataset:
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 * Real.cosh (log (z.im / w.im))) = w.im * |(z.im / w.im - (z.im / w.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:
cosh_log h₀,

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 + (z.im / w.im)⁻¹) / 2)) = w.im * |(z.im / w.im - (z.im / w.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.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)

Tactic:
fun_prop

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

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

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
α : Type u_4
inst✝ : TopologicalSpace α
f : α → SL n R
hf : Continuous[inst✝, instTopologicalSpace] f
i : n
⊢ Continuous[instTopologicalSpaceMatrix, Pi.topologicalSpace] fun A ↦ A i

Tactic:
fun_prop

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
α : Type u_4
inst✝ : TopologicalSpace α
f : α → SL n R
hf : Continuous[inst✝, instTopologicalSpace] f
i : n
⊢ Continuous[inst✝, instTopologicalSpaceMatrix] fun x ↦ ↑(f x)

Tactic:
fun_prop

Goal state after:
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 : IsInducing ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] ⇑(map f)

Tactic:
fun_prop

Goal state after:
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 : IsEmbedding ⇑f
⊢ Continuous[instTopologicalSpace, instTopologicalSpace] ⇑(map f)

Tactic:
fun_prop

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)

Tactic:
fun_prop

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

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

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

Goal state before:
pp: n : Type u_1
R : Type u_2
inst✝⁵ : Fintype n
inst✝⁴ : DecidableEq n
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T0Space R
⊢ Continuous[Units.instTopologicalSpaceUnits, Units.instTopologicalSpaceUnits] ⇑GeneralLinearGroup.det

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

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

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
x₁ x₂ : X
⊢ ↑x₁ = ↑x₂ ↔ x₁ = x₂

Tactic:
rw [iff_eq_eq]

Goal state after:
X : Type u_1
x₁ x₂ : X
⊢ (↑x₁ = ↑x₂) = (x₁ = x₂)
Module: Mathlib.Topology.Category.CompHaus.Basic

Goal state before:
pp: J : Type v
inst✝ : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
x✝ : (j : J) → ↑(F.obj j).toTop
⊢ x✝ ∈ {u | ∀ {i j : J} (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) (u i) = u j} ↔
    x✝ ∈ ⋂ i, ⋂ j, ⋂ f, {u | (ConcreteCategory.hom (F.map f)) (u i) = u j}

Tactic:
simp only [Set.mem_iInter, Set.mem_ofPred_eq]

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
x₁ x₂ : X
⊢ x₁ ∈ MulAction.orbit G x₂ ↔ ∃ a, a • x₂ = x₁

Tactic:
MulAction.mem_orbit_iff

Goal state after:
case e'_3
G : Type u_1
X : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G X
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace X
inst✝ : ProperSMul G X
R : Setoid X := MulAction.orbitRel G X
π : X → Quotient R := Quotient.mk'
this : IsOpenQuotientMap (Prod.map π π)
x₁ x₂ : X
⊢ (∃ x, x • x₂ = x₁) ↔ ∃ a, a • x₂ = x₁
Module: Mathlib.Topology.Compactification.OnePoint.Basic

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_3
inst✝ : TopologicalSpace Y
f : OnePoint X → Y
⊢ Continuous[instTopologicalSpace, inst✝] f ↔
    Tendsto (fun x ↦ f ↑x) (coclosedCompact X) (𝓝 (f ∞)) ∧ Continuous[inst✝¹, inst✝] fun x ↦ f ↑x

Tactic:
simp only [continuous_iff_continuousAt, OnePoint.forall, continuousAt_coe, continuousAt_infty',
    Function.comp_def]

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
f : G × G → G × X := Prod.map id fun g ↦ g • x
hfsurj : Function.Surjective f
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] f

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Basic

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace X
inst✝² : ContinuousSMul G X
inst✝¹ : IsTopologicalGroup G
inst✝ : IsPretransitive G X
x : X
hx : IsProperMap fun g ↦ g • x
f : G × G → G × X := Prod.map id fun g ↦ g • x
hfsurj : Function.Surjective f
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
⊢ Continuous fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
this : IsCompact ((fun gx ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ Continuous fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : Group G
inst✝⁴ : TopologicalSpace G
inst✝³ : MulAction G X
inst✝² : CompactlyGeneratedSpace (X × X)
inst✝¹ : T2Space X
inst✝ : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact {g | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
⊢ Continuous fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
tX : TopologicalSpace X
inst✝ : UCompactlyGeneratedSpace X
s : Set X
hs : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsOpen (⇑f ⁻¹' s)
⊢ IsOpen[tX] s

Tactic:
rw [eq_compactlyGenerated (X := X), TopologicalSpace.compactlyGenerated, isOpen_coinduced,
    isOpen_sigma_iff]
  exact fun ⟨S, f⟩ ↦ hs S f

Goal state after:
Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace

Goal state before:
pp: X : Type w
Y : Type x
tX : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : SequentialSpace X
s : Set X
h : ∀ (S : CompHaus) (f : C(↑S.toTop, X)), IsClosed (⇑f ⁻¹' s)
u : ℕ → X
p : X
hu : ∀ (n : ℕ), u n ∈ s
hup : Tendsto u atTop (𝓝 p)
g : ULift.{u, 0} (OnePoint ℕ) → X := ⇑(continuousMapMkNat u p hup) ∘ ULift.down
this : Tendsto OnePoint.some atTop (𝓝 ∞)
⊢ Continuous[_, tX] g

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
hf : Continuous f
⊢ Continuous (circleAverage (fun x ↦ log⁺ ‖f x‖) 0)

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous ↿fun g z ↦ ↑(↑g 0 0) * z + ↑(↑g 0 1)

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous ↿fun g z ↦ ↑(↑g 1 0) * z + ↑(↑g 1 1)

Tactic:
fun_prop

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ Continuous fun h ↦ ↑(Matrix.GeneralLinearGroup.det h)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (fun x ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (fun x ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log ↑s.card) 0 r

Tactic:
fun_prop

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

Goal state before:
pp: g : GL (Fin 2) ℝ
hg : ↑(Matrix.GeneralLinearGroup.det g) < 0
⊢ Continuous fun h ↦ ↑(Matrix.GeneralLinearGroup.det h)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic

Goal state before:
pp: case hf₁
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
⊢ Meromorphic fun x ↦ f₁ x * f₂ x

Tactic:
fun_prop

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

Goal state before:
pp: ⊢ Continuous fun g ↦ g • I

Tactic:
fun_prop

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

Goal state before:
pp: K : Set ℍ
hK : IsCompact K
A : ℝ
hA : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 0 0 ^ 2 + ↑g 0 1 ^ 2 ≤ A
A' : ℝ
hA' : ∀ (g : SL(2, ℝ)), g • I ∈ K → ↑g 1 0 ^ 2 + ↑g 1 1 ^ 2 ≤ A'
this✝² : SeminormedAddCommGroup (Matrix (Fin 2) (Fin 2) ℝ) := Matrix.seminormedAddCommGroup
this✝¹ : ProperSpace (Matrix (Fin 2) (Fin 2) ℝ)
this✝ : IsCompact {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'}
this : IsCompact (Subtype.val ⁻¹' {m | ∀ (i j : Fin 2), |m i j| ≤ max √A √A'})
⊢ Continuous fun g ↦ g • I

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ MeromorphicAt (fun x ↦ a) 0

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case h₂
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun x ↦ a) 0 ≠ 0

Tactic:
· simp only [meromorphicTrailingCoeffAt_const, ne_eq]
    grind

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : ¬MeromorphicAt f 0
a : ℂ
⊢ MeromorphicAt (fun x ↦ a) 0

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Measurable f
⊢ Measurable fun p ↦ log ‖f (circleMap 0 R p.2) - circleMap 0 1 p.1‖

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
⊢ Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
norm_sub_rev

Goal state after:
case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun x ↦ log ‖x - meromorphicTrailingCoeffAt f 0‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
a : ℂ
⊢ MeromorphicAt (fun x ↦ a) 0

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ Meromorphic (f - fun x ↦ a)

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
this : Measurable f
⊢ AEStronglyMeasurable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (Ioc 0 (2 * π))).prod (volume.restrict (Ioc 0 (2 * π))))

Tactic:
fun_prop

Goal state after:
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)

Tactic:
have (d : E) : {x | s x < d} = ⋃ f : 𝓕, U f d := by
    ext x
    simp [U, isGLB_lt_iff (h𝓕 x)]

Goal state after:
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := fun f d ↦ {x | f x < d}
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
⊢ ∃ 𝓕' ⊆ 𝓕, 𝓕'.Countable ∧ ∀ (a : X), IsGLB (Function.eval a '' 𝓕') (s a)
Module: Mathlib.Topology.Semicontinuity.Lindelof

Goal state before:
pp: case right
X : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace X
inst✝⁵ : HereditarilyLindelofSpace X
inst✝⁴ : LinearOrder E
inst✝³ : TopologicalSpace E
inst✝² : OrderClosedTopology E
inst✝¹ : DenselyOrdered E
inst✝ : SeparableSpace E
s : X → E
𝓕 : Set (X → E)
h𝓕_cont : ∀ f ∈ 𝓕, UpperSemicontinuous f
h𝓕 : ∀ (a : X), IsGLB (Function.eval a '' 𝓕) (s a)
D : Set E
D_count : D.Countable
D_dense : Dense D
U : (X → E) → E → Set X := ⋯
U_open : ∀ {f : X → E}, f ∈ 𝓕 → ∀ (d : E), IsOpen (U f d)
this : ∀ (d : E), {x | s x < d} = ⋃ f, U (↑f) d
d : E
t : Set ↑𝓕
t_count : t.Countable
ht : ⋃ i ∈ t, U (↑i) d = ⋃ i, U (↑i) d
⊢ ⋃ f, U (↑f) d = ⋃ f ∈ Subtype.val '' t, U f d

Tactic:
rw [← ht, biUnion_image]

Goal state after:
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
⊢ Sbtw R x y z ↔ Sbtw R z y x

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
⊢ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
⊢ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Sbtw R z y x

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : PartialOrder R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : IsOrderedRing R
x y z : P
⊢ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z ↔ Wbtw R z y x ∧ y ≠ z ∧ y ≠ x
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ⇑f
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
hf : Injective ⇑f
⊢ Wbtw R (f x) (f y) (f z) ∧ f y ≠ f x ∧ f y ≠ f z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn ⇑f ↑s
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁷ : Ring R
inst✝⁶ : PartialOrder R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P →ᵃ[R] P'
s : AffineSubspace R P
hf : InjOn ⇑f ↑s
hx : x ∈ s
hy : y ∈ s
hz : z ∈ s
⊢ Wbtw R (f x) (f y) (f z) ∧ f y ≠ f x ∧ f y ≠ f z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
⊢ Sbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
⊢ Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ∧ v +ᵥ y ≠ v +ᵥ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Sbtw R x y z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
⊢ Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ∧ v +ᵥ y ≠ v +ᵥ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : P
v : V
⊢ Wbtw R (v +ᵥ x) (v +ᵥ y) (v +ᵥ z) ∧ v +ᵥ y ≠ v +ᵥ x ∧ v +ᵥ y ≠ v +ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : V
p : P
⊢ Sbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : V
p : P
⊢ Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ∧ y +ᵥ p ≠ x +ᵥ p ∧ y +ᵥ p ≠ z +ᵥ p ↔ Sbtw R x y z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : V
p : P
⊢ Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ∧ y +ᵥ p ≠ x +ᵥ p ∧ y +ᵥ p ≠ z +ᵥ p ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z : V
p : P
⊢ Wbtw R (x +ᵥ p) (y +ᵥ p) (z +ᵥ p) ∧ y +ᵥ p ≠ x +ᵥ p ∧ y +ᵥ p ≠ z +ᵥ p ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ∧ p -ᵥ y ≠ p -ᵥ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Sbtw R x y z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ∧ p -ᵥ y ≠ p -ᵥ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Wbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ∧ p -ᵥ y ≠ p -ᵥ x ∧ p -ᵥ y ≠ p -ᵥ z ↔ Wbtw R x y z ∧ y ≠ x ∧ y ≠ z
Module: Mathlib.Analysis.Convex.Between

Goal state before:
pp: R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Sbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ↔ Sbtw R x y z

Tactic:
Sbtw,

Goal state after:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : Ring R
inst✝³ : PartialOrder R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y z p : P
⊢ Wbtw R (x -ᵥ p) (y -ᵥ p) (z -ᵥ p) ∧ y -ᵥ p ≠ x -ᵥ p ∧ y -ᵥ p ≠ z -ᵥ p ↔ Sbtw R x y z