mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

pp: case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : ¬MemHolder r f
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
· refine le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_
    · rw [coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm, mul_comm]
    · rw [← (hf.holderWith.smul c).memHolder.coe_nnHolderNorm_eq_eHolderNorm, ← coe_div hc]
      refine HolderWith.eHolderNorm_le fun x₁ x₂ => ?_
      rw [coe_div hc, ← ENNReal.mul_div_right_comm,
        ENNReal.le_div_iff_mul_le (Or.inl <| coe_ne_zero.2 hc) <| Or.inl coe_ne_top,
        mul_comm, ← smul_eq_mul, ← ENNReal.smul_def, ← edist_smul₀, ← Pi.smul_apply,
        ← Pi.smul_apply]
      exact hf.smul.holderWith x₁ x₂

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : ¬MemHolder r f
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f
Module: Mathlib.Topology.MetricSpace.Ultra.Pi

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → PseudoMetricSpace (X i)
inst✝ : ∀ (i : ι), IsUltrametricDist (X i)
⊢ ∀ (x y z : (i : ι) → X i), dist x z ≤ max (dist x y) (dist y z)

Tactic:
intro f g h

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝² : Fintype ι
inst✝¹ : (i : ι) → PseudoMetricSpace (X i)
inst✝ : ∀ (i : ι), IsUltrametricDist (X i)
f g h : (i : ι) → X i
⊢ dist f h ≤ max (dist f g) (dist g h)
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
⊢ ∀ (x y : Snowflaking X α hα₀ hα₁), 0 ≤ dist x y

Tactic:
intro x y; cases x; cases y; rw [dist_toSnowflaking_toSnowflaking]; positivity

Goal state after:
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : X
r : ℝ
hr : 0 ≤ r
y : X
⊢ { val := y } ∈ ⇑ofSnowflaking ⁻¹' closedBall x r ↔ { val := y } ∈ closedBall (toSnowflaking x) (r ^ α)

Tactic:
simp (disch := positivity) [Real.rpow_le_rpow_iff]

Goal state after:
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ ⇑toSnowflaking ⁻¹' closedBall x r = closedBall (ofSnowflaking x) (r ^ α⁻¹)

Tactic:
preimage_toSnowflaking_closedBall _ hr

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
x : Snowflaking X α hα₀ hα₁
r : ℝ
hr : 0 ≤ r
⊢ closedBall (ofSnowflaking x) (r ^ α⁻¹) = closedBall (ofSnowflaking x) (r ^ α⁻¹)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : IsOpen[inst✝¹] s
⊢ IsLowerSet s

Tactic:
replace h := isOpen_iff_generate_Ici_compl.1 h

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
s : Set α
h : GenerateOpen {t | ∃ a, (Ici a)ᶜ = t} s
⊢ IsLowerSet s
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α univ
⊢ IsOpen[t] s ↔ DirSupInacc s

Tactic:
rw [isOpen_iff_dirSupInaccOn isLowerSet_univ, dirSupInaccOn_univ]

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: case e'_3
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ ↑(lowerClosure s) = closure[upperSet α] s

Tactic:
rw [@IsUpperSet.closure_eq_lowerClosure α _ (upperSet α) ?_ s]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α univ
⊢ Topology.IsUpperSet α
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: case right
α : Type u_1
inst✝² : CompleteLattice α
T : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
hT : ∀ p ∈ T, InfPrime p
hG : OrderGenerates T
S : Set ↑T
⊢ hull T (kernel S) ⊆ ⋂₀ {t | IsClosed[instTopologicalSpaceSubtype] t ∧ S ⊆ t}

Tactic:
simp_rw [subset_sInter_iff]
    intro R hR
    rw [← (hull_kernel_of_isClosed hT hG hR.1), ← gc_closureOperator]
    exact ClosureOperator.monotone _ hR.2

Goal state after:
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed[lawson α] (↑(upperClosure {a}) ∩ ↑(lowerClosure {a}))

Tactic:
← WithLawson.isClosed_preimage_ofLawson

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace] (⇑WithLawson.ofLawson ⁻¹' (↑(upperClosure {a}) ∩ ↑(lowerClosure {a})))
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace] (Iic a)

Tactic:
← WithLawson.isClosed_preimage_ofLawson

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace] (⇑WithLawson.ofLawson ⁻¹' Iic a)
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q

Tactic:
have hb : Isometry ((↑) : q → X) := isometry_subtype_coe

Goal state after:
X : Type u
inst✝ : MetricSpace X
p q : NonemptyCompacts X
ha : Isometry Subtype.val
hb : Isometry Subtype.val
⊢ dist p.toGHSpace q.toGHSpace ≤ dist p q
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case pos
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
A : C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U V : (Opens ↑X)ᵒᵖ
inc : U ⟶ V
hV : p₀ ∈ unop V
hU : p₀ ∈ unop U
⊢ 𝓕.map inc ≫ 𝓕.germ (unop V) p₀ hV ≫ f ≫ eqToHom ⋯ = (𝓕.germ (unop U) p₀ hU ≫ f ≫ eqToHom ⋯) ≫ eqToHom ⋯

Tactic:
rw [← Category.assoc, 𝓕.germ_res' inc, Category.assoc, Category.assoc, eqToHom_trans]

Goal state after:
Module: Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasProducts C
X : TopCat
F : Presheaf C X
ι : Type v'
U : ι → Opens ↑X
G : Presheaf C X
α : F ≅ G
⊢ ∀ {X_1 Y : WalkingParallelPair} (f : X_1 ⟶ Y),
    (diagram F U).map f ≫ (WalkingParallelPair.casesOn Y (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom =
      (WalkingParallelPair.casesOn X_1 (piOpens.isoOfIso U α) (piInters.isoOfIso U α)).hom ≫ (diagram G U).map f

Tactic:
rintro ⟨⟩ ⟨⟩ ⟨⟩
      · simp
      · dsimp
        refine Pi.hom_ext _ _ fun b ↦ ?_
        simp [leftRes]
      · dsimp [diagram]
        refine Pi.hom_ext _ _ fun b ↦ ?_
        simp [rightRes]
      · simp

Goal state after:
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
⊢ BddAbove (range fun x ↦ ⨅ y, f (inl x, inr y) + C)

Tactic:
refine ⟨Cf + C, forall_mem_range.2 fun x => ?_⟩

Goal state after:
X : Type u
Y : Type v
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : Nonempty Y
f : Cb X Y
C Cf : ℝ
hCf : Cf ∈ upperBounds (range ⇑f)
x : X
⊢ ⨅ y, f (inl x, inr y) + C ≤ Cf + C
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this✝ : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
this : ⌊ε⁻¹ * dist x y⌋₊ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
⊢ ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋

Tactic:
have D : 0 ≤ ⌊ε⁻¹ * dist x y⌋ :=
          floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos.2 εpos)) dist_nonneg)

Goal state after:
t : Set GHSpace
C : ℝ
u : ℕ → ℝ
K : ℕ → ℕ
ulim : Tendsto u atTop (𝓝 0)
hdiam : ∀ p ∈ t, diam univ ≤ C
hcov : ∀ p ∈ t, ∀ (n : ℕ), ∃ s, #↑s ≤ ↑(K n) ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)
δ : ℝ
δpos : δ > 0
ε : ℝ := 1 / 5 * δ
εpos : 0 < ε
n : ℕ
hn : ∀ n_1 ≥ n, dist (u n_1) 0 < ε
u_le_ε : u n ≤ ε
s : (p : GHSpace) → Set p.Rep
N : GHSpace → ℕ
hN : ∀ (p : GHSpace), N p ≤ K n
E : (p : GHSpace) → ↑(s p) ≃ Fin (N p)
hs : ∀ p ∈ t, univ ⊆ ⋃ x ∈ s p, ball x (u n)
M : ℕ := ⌊ε⁻¹ * max C 0⌋₊
F : GHSpace → (k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ) :=
  fun p ↦ ⟨⟨N p, ⋯⟩, fun a b ↦ ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊, ⋯⟩⟩
p : GHSpace
pt : p ∈ t
q : GHSpace
qt : q ∈ t
hpq : (fun p ↦ F ↑p) ⟨p, pt⟩ = (fun p ↦ F ↑p) ⟨q, qt⟩
Npq : N p = N q
Ψ : ↑(s p) → ↑(s q) := fun x ↦ (E q).symm (Fin.cast Npq ((E p) x))
Φ : ↑(s p) → q.Rep := fun x ↦ ↑(Ψ x)
x y : ↑(s p)
this✝ : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y)
i : ℕ := ↑((E p) x)
hip : i < N p
hiq : i < N q
i' : i = ↑((E q) (Ψ x))
j : ℕ := ↑((E p) y)
hjp : j < N p
hjq : j < N q
j' : j = ↑((E q) (Ψ y))
Ap : ↑((F p).snd ⟨i, hip⟩ ⟨j, hjp⟩) = ⌊ε⁻¹ * dist x y⌋₊
Aq : ↑((F q).snd ⟨i, hiq⟩ ⟨j, hjq⟩) = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
this : ⌊ε⁻¹ * dist x y⌋₊ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊
D : 0 ≤ ⌊ε⁻¹ * dist x y⌋
⊢ ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
hle : HasSmallInductiveDimensionLE X n
hlt : ¬HasSmallInductiveDimensionLT X n
⊢ smallInductiveDimension X = ↑n

Tactic:
apply (smallInductiveDimension_le_iff.2 hle).antisymm

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
hle : HasSmallInductiveDimensionLE X n
hlt : ¬HasSmallInductiveDimensionLT X n
⊢ ↑n ≤ smallInductiveDimension X
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
x : X
n✝ : ℕ
a✝ : (concat (fun x_1 ↦ x) fun x_1 ↦ refl x) = refl x
⊢ (concat (fun x_1 ↦ x) fun x_1 ↦ refl x) = refl x

Tactic:
concat_succ

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
x : X
n✝ : ℕ
a✝ : (concat (fun x_1 ↦ x) fun x_1 ↦ refl x) = refl x
⊢ (concat ((fun x_1 ↦ x) ∘ castSucc) fun k ↦ refl x).trans (refl x) = refl x
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ n : ℕ
ih :
  (p : Fin (n + 1) → X) →
    (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
      ((k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
p : Fin (n + 1 + 1) → X
F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
H : (k : Fin (n + 1)) → (F k).Homotopy (G k)
⊢ ((concat (p ∘ castSucc) fun k ↦ F k.castSucc).trans (F (last n))).Homotopy (concat p G)

Tactic:
concat_succ

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ n : ℕ
ih :
  (p : Fin (n + 1) → X) →
    (F G : (k : Fin n) → Path (p k.castSucc) (p k.succ)) →
      ((k : Fin n) → (F k).Homotopy (G k)) → (concat p F).Homotopy (concat p G)
p : Fin (n + 1 + 1) → X
F G : (k : Fin (n + 1)) → Path (p k.castSucc) (p k.succ)
H : (k : Fin (n + 1)) → (F k).Homotopy (G k)
⊢ ((concat (p ∘ castSucc) fun k ↦ F k.castSucc).trans (F (last n))).Homotopy
    ((concat (p ∘ castSucc) fun k ↦ G k.castSucc).trans (G (last n)))
Module: Mathlib.Topology.Subpath

Goal state before:
pp: case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ : ℕ
γ : Path a b
n : ℕ
ih :
  (t : Fin (n + 1) → ↑I) →
    (concat (⇑γ ∘ t) fun k ↦ γ.subpath (t k.castSucc) (t k.succ)).Homotopy (γ.subpath (t 0) (t (last n)))
t : Fin (n + 1 + 1) → ↑I
⊢ (concat (⇑γ ∘ t) fun k ↦ γ.subpath (t k.castSucc) (t k.succ)).Homotopy (γ.subpath (t 0) (t (last (n + 1))))

Tactic:
concat_succ

Goal state after:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
a b : X
n✝ : ℕ
γ : Path a b
n : ℕ
ih :
  (t : Fin (n + 1) → ↑I) →
    (concat (⇑γ ∘ t) fun k ↦ γ.subpath (t k.castSucc) (t k.succ)).Homotopy (γ.subpath (t 0) (t (last n)))
t : Fin (n + 1 + 1) → ↑I
⊢ ((concat ((⇑γ ∘ t) ∘ castSucc) fun k ↦ γ.subpath (t k.castSucc.castSucc) (t k.castSucc.succ)).trans
        (γ.subpath (t (last n).castSucc) (t (last n).succ))).Homotopy
    (γ.subpath (t 0) (t (last (n + 1))))
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ IsUltraUniformity X

Tactic:
refine .mk_of_hasBasis (h.hasBasis.inf h'.hasBasis) ?_ ?_ <;>
  · dsimp
    rintro _ ⟨⟨_, _, _⟩, _, _, _⟩
    infer_instance

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ultra.Completion

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : SeparationQuotient.mk b = SeparationQuotient.mk c
⊢ (b, c) ∈ U

Tactic:
SeparationQuotient.mk_eq_mk,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : UniformSpace X
inst✝¹ : UniformSpace Y
inst✝ : IsUltraUniformity X
this :
  (𝓤 (SeparationQuotient X)).HasBasis (fun s ↦ s ∈ 𝓤 X ∧ s.IsSymm ∧ s.IsTrans) fun i ↦
    Prod.map SeparationQuotient.mk SeparationQuotient.mk '' id i
U : SetRel X X
hU' : U ∈ 𝓤 X
left✝ : U.IsSymm
hU : U.IsTrans
a b : X
hab : (a, b) ∈ U
c d : X
hcd : (c, d) ∈ U
hc : Inseparable b c
⊢ (b, c) ∈ U
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
X : Set E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := ⋯
hrec : s ⊆ Y → (∀ x ∈ X', ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
hx' : x ∉ X'
⊢ t < f x b

Tactic:
rw [← not_le]

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝¹¹ : LinearOrder β
Y : Set F
f : E → F → β
inst✝¹⁰ : TopologicalSpace E
inst✝⁹ : AddCommGroup E
inst✝⁸ : Module ℝ E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : ContinuousSMul ℝ E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
cY : Convex ℝ Y
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
s✝ : Set F
t : β
b : F
s : Set F
a✝ : b ∉ s
hs : s.Finite
X : Set E
ne_X : X.Nonempty
kX : IsCompact X
hfy : ∀ y ∈ Y, LowerSemicontinuousOn (fun x ↦ f x y) X
hfy' : ∀ y ∈ Y, QuasiconvexOn ℝ X fun x ↦ f x y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
cX : Convex ℝ X
hsY : insert b s ⊆ Y
ht : ∀ x ∈ X, ∃ y ∈ insert b s, t < f x y
hb : b ∈ Y
X' : Set E := X ∩ (fun x ↦ f x b) ⁻¹' Iic t
hrec : s ⊆ Y → (∀ x ∈ X', ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X', t < f x y0
X'_ne : X'.Nonempty
hX'X : X' ⊆ X
kX' : IsCompact X'
cX' : Convex ℝ X'
ht_lt : ∀ x ∈ X', ∃ y ∈ s, t < f x y
y1 : F
hy1 : y1 ∈ Y
hty1 : ∀ x ∈ X', t < f x y1
x : E
hx : x ∈ X
hx' : x ∉ X'
⊢ ¬f x b ≤ t