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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
⊢ ∀ (n : ℕ), ((fun n ↦ ⋃ m, U (Nat.pair n m)) n).Infinite

pp: case refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
⊢ Pairwise (Disjoint on fun n ↦ ⋃ m, U (Nat.pair n m))

Tactic:
· refine fun n ↦ infinite_iUnion fun i j hij ↦ ?_
      suffices n.pair i = n.pair j by simpa
      apply hd.eq
      simpa [hij, onFun] using (hne _).ne_empty

Goal state after:
case refine_2
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : Infinite X
U : ℕ → Set X
hne : ∀ (n : ℕ), (U n).Nonempty
ho : ∀ (n : ℕ), IsOpen[inst✝²] (U n)
hd : Pairwise (Disjoint on U)
⊢ Pairwise (Disjoint on fun n ↦ ⋃ m, U (Nat.pair n m))
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsClosed[inst✝¹] ↑(lowerClosure s)

Tactic:
rw [isClosed_iff_isLower]

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsLowerSet ↑(lowerClosure s)
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case mp
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ ∃ S ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s}, U = ⋃₀ S

Tactic:
(Mathlib.Tactic.useSyntax
 "use"
 []
 (group)
 [(choice
   («term{_}» "{" [`U] "}")
   (Term.structInst
    "{"
    []
    (Term.structInstFields [(Term.structInstField (Term.structInstLVal `U []) [])])
    (Term.optEllipsis [])
    []
    "}"))])

Goal state after:
case h
α : Type u_1
inst✝¹ : CompleteLinearOrder α
t : TopologicalSpace α
inst✝ : IsLower α
U : Set α
hU : ¬U = univ
hO : IsOpen[t] U
a : α
ha : (Ici a)ᶜ = U
⊢ {U} ⊆ insert univ {s | ∃ a, (Ici a)ᶜ = s} ∧ U = ⋃₀ {U}
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ IsOpen[t] sᶜ ↔ DirSupClosedOn D s

Tactic:
isOpen_iff_dirSupInaccOn hDL,

Goal state after:
α : Type u_1
s : Set α
D : Set (Set α)
inst✝¹ : Preorder α
t : TopologicalSpace α
inst✝ : IsScottHausdorff α D
hDL : IsLowerSet D
⊢ DirSupInaccOn D sᶜ ↔ DirSupClosedOn D s
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
x y : α
h : Inseparable x y
⊢ Iic x = Iic y

Tactic:
simpa only [inseparable_iff_closure_eq, IsScott.closure_singleton] using h

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsUpper α
⊢ inst✝¹ = upper α

Tactic:
exact IsUpper.topology_eq α

Goal state after:
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_1
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α (range fun c ↦ range ⇑c)
f : α → Prop
⊢ ωScottContinuous f ↔ Continuous[inst✝¹, _] f

Tactic:
by
  rw [ωScottContinuous, scottContinuousOn_iff_continuous (fun a b hab => by
    use Chain.pair a b hab; exact OmegaCompletePartialOrder.Chain.range_pair a b hab)]

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

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
q : ℚ
x✝ : (IsSuccPrelimit x → 0 ≤ q) ∧ (IsPredPrelimit x → q ≤ 0)
hx₁ : IsSuccPrelimit x → 0 ≤ q
hx₂ : IsPredPrelimit x → q ≤ 0
hq : q ≤ 0
⊢ IsOpen (⇑some ⁻¹' Iio ⟨toLex (x, q), ⋯⟩)

Tactic:
convert isOpen_Iio (a := x)
      ext
      simp [some, Prod.Lex.lt_iff, hq.not_gt]

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

Goal state before:
pp: X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝¹ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
this✝ : f (inr y) ∈ ↑q
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑p
hz : dist z (f (inr y)) < r
this : z ∈ range Φ
x : X
hx : Φ x = z
⊢ dist (Φ x) (Ψ y) = dist z (f (inr y))

Tactic:
hx

Goal state after:
X : Type u
inst✝⁵ : MetricSpace X
inst✝⁴ : CompactSpace X
inst✝³ : Nonempty X
Y : Type v
inst✝² : MetricSpace Y
inst✝¹ : CompactSpace Y
inst✝ : Nonempty Y
inhabited_h✝ : Inhabited X
inhabited_h : Inhabited Y
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
bound : hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
Φ : X → ↥(lp (fun n ↦ ℝ) ∞)
Φisom : Isometry Φ
Φrange : range Φ = ↑p
Ψ : Y → ↥(lp (fun n ↦ ℝ) ∞)
Ψisom : Isometry Ψ
Ψrange : range Ψ = ↑q
I : diam (range Φ ∪ range Ψ) ≤ 2 * diam univ + 1 + 2 * diam univ
f : X ⊕ Y → ↥(lp (fun n ↦ ℝ) ∞) :=
  fun x ↦
    match x with
    | inl y => Φ y
    | inr z => Ψ z
F : (X ⊕ Y) × (X ⊕ Y) → ℝ := fun p ↦ dist (f p.1) (f p.2)
Fgood : F ∈ candidates X Y
Fb : GromovHausdorff.Cb✝ X Y := candidatesBOfCandidates F Fgood
this✝¹ : hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ HD Fb
r : ℝ
hr : hausdorffDist ↑p ↑q < r
I1 : ∀ (x : X), ⨅ y, Fb (inl x, inr y) ≤ r
y : Y
this✝ : f (inr y) ∈ ↑q
z : ↥(lp (fun n ↦ ℝ) ∞)
zq : z ∈ ↑p
hz : dist z (f (inr y)) < r
this : z ∈ range Φ
x : X
hx : Φ x = z
⊢ dist z (Ψ y) = dist z (f (inr y))
Module: Mathlib.Topology.Separation.AlexandrovDiscrete

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
s : Set X
⊢ nhdsKer s = s

Tactic:
by
  ext; simp [mem_nhdsKer_iff_specializes]

Goal state after:
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case hc
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ p₀ ∈ unop ((OpenNhds.inclusion y).op.obj V)

pp: X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc

Tactic:
· exact h.mem_open V.unop.1.2 V.unop.2

Goal state after:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{u, v} C
A : C
inst✝ : HasTerminal C
y : ↑X
h : p₀ ⤳ y
U V : (OpenNhds y)ᵒᵖ
inc : U ⟶ V
⊢ eqToHom ⋯ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ ((Functor.const (OpenNhds y)ᵒᵖ).obj A).map inc
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: case neg
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
⊢ (𝓕.map inc ≫
      if h : p₀ ∈ unop V then 𝓕.germ (unop V) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj V)) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then c else ⊤_ C)

Tactic:
split_ifs
      exact ((if_neg hV).symm.ndrec terminalIsTerminal).hom_ext ..

Goal state after:
Module: Mathlib.Topology.Sheaves.Abelian

Goal state before:
pp: C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
F : Sheaf C X
h : ∀ (x : ↑X), IsZero ((forget C X ⋙ stalkFunctor C x).obj F)
f : F ⟶ 0 := ⋯.from_ F
⊢ IsZero F

Tactic:
have : IsIso f := by
    rw [Presheaf.isIso_iff_stalkFunctor_map_iso]
    exact fun x => isIso_of_source_target_iso_zero _ (h x).isoZero
      ((forget C X ⋙ stalkFunctor C x).map_isZero (isZero_zero _)).isoZero

Goal state after:
C : Type v
inst✝⁶ : Category.{u, v} C
inst✝⁵ : HasColimits C
inst✝⁴ : HasLimits C
FC : C → C → Type u_1
CC : C → Type u
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
instCC : ConcreteCategory C FC
inst✝² : PreservesFilteredColimits (CategoryTheory.forget C)
inst✝¹ : PreservesLimits (CategoryTheory.forget C)
inst✝ : Abelian C
X : TopCat
F : Sheaf C X
h : ∀ (x : ↑X), IsZero ((forget C X ⋙ stalkFunctor C x).obj F)
f : F ⟶ 0 := ⋯.from_ F
this : IsIso f
⊢ IsZero F
Module: Mathlib.Topology.Sheaves.Skyscraper

Goal state before:
pp: X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U : Opens ↑X
hxU : p₀ ∈ U
⊢ (toSkyscraperPresheaf p₀ f).app (op U) ≫ eqToHom ⋯ = 𝓕.germ U p₀ hxU ≫ f

Tactic:
toSkyscraperPresheaf_app,

Goal state after:
X : TopCat
p₀ : ↑X
inst✝³ : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝² : Category.{u, v} C
inst✝¹ : HasTerminal C
inst✝ : HasColimits C
𝓕 : Presheaf C X
c : C
f : 𝓕.stalk p₀ ⟶ c
U : Opens ↑X
hxU : p₀ ∈ U
⊢ (if h : p₀ ∈ unop (op U) then 𝓕.germ (unop (op U)) p₀ h ≫ f ≫ eqToHom ⋯
      else (⋯ ▸ terminalIsTerminal).from (𝓕.obj (op U))) ≫
      eqToHom ⋯ =
    𝓕.germ U p₀ hxU ≫ f
Module: Mathlib.Topology.MetricSpace.GromovHausdorff

Goal state before:
pp: case refine_1
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)⌋₊, ⋯⟩⟩
⊢ Fintype ((k : Fin (K n).succ) × (Fin ↑k → Fin ↑k → Fin M.succ))

pp: case refine_2
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)⌋₊, ⋯⟩⟩
⊢ ∀ (x y : ↑t), (fun p ↦ F ↑p) x = (fun p ↦ F ↑p) y → dist ↑x ↑y < δ

Tactic:
· infer_instance

Goal state after:
case refine_2
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)⌋₊, ⋯⟩⟩
⊢ ∀ (x y : ↑t), (fun p ↦ F ↑p) x = (fun p ↦ F ↑p) y → dist ↑x ↑y < δ
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: case h
X : TopCat
U : Opens ↑X
F G : Sheaf AddCommGrpCat X
g : F ⟶ G
s : ↑(G.obj.obj (op U))
c : Set (Under g s)
h : IsChain (fun x y ↦ Nonempty (y ⟶ x)) c
f : ↑c → Opens ↑X := ⋯
t : ToType (F.obj.obj (op (iSup f)))
ht : IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) t
right✝ :
  ∀ (y : ToType (F.obj.obj (op (iSup f)))),
    (fun s_1 ↦ IsGluing F.obj f (fun x ↦ (StructuredArrow.right ↑x).snd) s_1) y → y = t
le₁ : iSup f ≤ U
le₂ : ∀ i ∈ c, unop (StructuredArrow.right i).fst ≤ iSup f
⊢ ∀ a ∈ c,
    Nonempty
      (StructuredArrow.mk
          (CategoryOfElements.homMk ⟨op U, s⟩
            ((NatTrans.mapElements (Functor.whiskerRight g.hom (CategoryTheory.forget AddCommGrpCat))).obj
              ⟨op (iSup f), t⟩)
            (homOfLE le₁).op ⋯) ⟶
        a)

Tactic:
exact fun i hi => Nonempty.intro (StructuredArrow.homMk (CategoryOfElements.homMk _ _
    (homOfLE (le₂ i hi)).op (ht ⟨i, hi⟩)) (by cat_disch))

Goal state after:
Module: Mathlib.Topology.Sheaves.Flasque

Goal state before:
pp: X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
⊢ x ∈ U → x ∈ unop (StructuredArrow.right t).fst

Tactic:
hx

Goal state after:
X : TopCat
U : Opens ↑X
S : ShortComplex (Sheaf AddCommGrpCat X)
hS : S.ShortExact
inst✝ : S.X₁.IsFlasque
s : ↑(S.X₃.obj.obj (op U))
t : Under S.g s
ht : ∀ (a : Under S.g s), Nonempty (a ⟶ t) → Nonempty (t ⟶ a)
tle : unop (StructuredArrow.right t).fst ≤ U
tcomp :
  (s |_ unop (StructuredArrow.right t).fst) tle =
    (ConcreteCategory.hom (S.g.hom.app (StructuredArrow.right t).fst)) (StructuredArrow.right t).snd
x : ↑X
hx : x ∈ U
⊢ x ∈ unop (StructuredArrow.right t).fst
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ x, ⨅ y, f (inl x, inr y) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g
x✝ : X
x y : ℝ
⊢ x ≤ y → (id + fun x ↦ dist f g) x ≤ (id + fun x ↦ dist f g) y

Tactic:
hx

Goal state after:
case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ x, ⨅ y, f (inl x, inr y) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g
x✝ : X
x y : ℝ
hx : x ≤ y
⊢ (id + fun x ↦ dist f g) x ≤ (id + fun x ↦ dist f g) y
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ x, ⨅ y, f (inl x, inr y) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ y, g (inl x, inr y)) + dist f g = ⨅ y, g (inl x, inr y) + dist f g
x y : ℝ
⊢ x ≤ y → (id + fun x ↦ dist f g) x ≤ (id + fun x ↦ dist f g) y

Tactic:
hx

Goal state after:
case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ x, ⨅ y, f (inl x, inr y) ≤ ⨆ x, ⨅ y, g (inl x, inr y) + dist f g
E1 : ∀ (x : X), (⨅ y, g (inl x, inr y)) + dist f g = ⨅ y, g (inl x, inr y) + dist f g
x y : ℝ
hx : x ≤ y
⊢ (id + fun x ↦ dist f g) x ≤ (id + fun x ↦ dist f g) y
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g
y✝ : Y
x y : ℝ
⊢ x ≤ y → (id + fun x ↦ dist f g) x ≤ (id + fun x ↦ dist f g) y

Tactic:
hx

Goal state after:
case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g
y✝ : Y
x y : ℝ
hx : x ≤ y
⊢ (id + fun x ↦ dist f g) x ≤ (id + fun x ↦ dist f g) y
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g
E1 : ∀ (y : Y), (⨅ x, g (inl x, inr y)) + dist f g = ⨅ x, g (inl x, inr y) + dist f g
x y : ℝ
⊢ x ≤ y → (id + fun x ↦ dist f g) x ≤ (id + fun x ↦ dist f g) y

Tactic:
hx

Goal state after:
case refine_1
X : Type u
Y : Type v
inst✝³ : MetricSpace X
inst✝² : MetricSpace Y
inst✝¹ : Nonempty X
inst✝ : Nonempty Y
f g : Cb X Y
cg : ℝ
hcg : cg ∈ lowerBounds (range ⇑g)
Hcg : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cg ≤ g x
cf : ℝ
hcf : cf ∈ lowerBounds (range ⇑f)
Hcf : ∀ (x : (X ⊕ Y) × (X ⊕ Y)), cf ≤ f x
Z : ⨆ y, ⨅ x, f (inl x, inr y) ≤ ⨆ y, ⨅ x, g (inl x, inr y) + dist f g
E1 : ∀ (y : Y), (⨅ x, g (inl x, inr y)) + dist f g = ⨅ x, g (inl x, inr y) + dist f g
x y : ℝ
hx : x ≤ y
⊢ (id + fun x ↦ dist f g) x ≤ (id + fun x ↦ dist f g) y
Module: Mathlib.Topology.Sion

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ 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
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
⊢ x ∈ sublevelLeft X f b ↑z → x ∈ sublevelLeft X f b' ↑y

Tactic:
hx

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
inst✝⁸ : LinearOrder β
X : Set E
Y : Set F
f : E → F → β
inst✝⁷ : TopologicalSpace E
inst✝⁶ : AddCommGroup E
inst✝⁵ : Module ℝ E
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : ContinuousSMul ℝ 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
inst✝² : TopologicalSpace F
inst✝¹ : AddCommGroup F
inst✝ : Module ℝ F
cY : Convex ℝ Y
hfx : ∀ x ∈ X, UpperSemicontinuousOn (fun y ↦ f x y) Y
hfx' : ∀ x ∈ X, QuasiconcaveOn ℝ Y fun y ↦ f x y
a : E
b b' : β
y y' : ↑Y
ha : ∀ x ∈ X, max (f a ↑y) (f a ↑y') ≤ max (f x ↑y) (f x ↑y')
hb : ∀ y ∈ Y, ∃ x ∈ X, f x y ≤ b
hb' : b' < max (f a ↑y) (f a ↑y')
hbb' : b < b'
J : Set ↑(segment ℝ ↑y ↑y') := setOfPred_sublevelLeft_subset X Y f b b' y y'
z : ↑(segment ℝ ↑y ↑y')
hz : ClusterPt z (𝓟 J)
x : ↑X
hx : x ∈ sublevelLeft X f b ↑z
⊢ x ∈ sublevelLeft X f b' ↑y
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 := 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'
x : E
⊢ x ∈ X' → ∃ y ∈ s, t < f x y

Tactic:
hx

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'
x : E
hx : x ∈ X'
⊢ ∃ y ∈ s, t < f x y
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
⊢ IsUltraUniformity (SeparationQuotient X)

Tactic:
by
  have := IsUltraUniformity.hasBasis.map
    (Prod.map SeparationQuotient.mk (SeparationQuotient.mk (X := X)))
  rw [← SeparationQuotient.uniformity_eq] at this
  apply mk_of_hasBasis this
  · exact fun _ ⟨_, hU, _⟩ ↦ by rw [id_eq]; infer_instance
  · rintro U ⟨hU', _, hU⟩
    constructor
    rintro x y z
    simp only [id_eq, Set.mem_image, Prod.exists, Prod.map_apply, Prod.mk.injEq,
      forall_exists_index, and_imp]
    rintro a b hab rfl rfl c d hcd hc rfl
    have hbc : (b, c) ∈ U := by
      rw [eq_comm, SeparationQuotient.mk_eq_mk, inseparable_iff_ker_uniformity,
          Filter.mem_ker] at hc
      exact hc _ hU'
    exact ⟨a, d, U.trans (U.trans hab hbc) hcd, by simp, by simp⟩

Goal state after: