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

Goal state before:
pp: case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg✝ : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg✝ :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : ↑x ≤ b
⊢ (F i) ⟨↑x, ⋯⟩ ∈ U

Tactic:
refine hf ⟨x, ⟨x, ⟨hx, hxb⟩, rfl⟩, ?_⟩

Goal state after:
case pos
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg✝ : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg✝ :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
hg : MapsTo (⇑(G i)) K₂ U
hfg : (F i) ⊤ = (G i) ⊥
x : ↑(Icc a c)
hx : x ∈ K
hxb : ↑x ≤ b
⊢ projIccCM ↑x = ⟨↑x, ⋯⟩
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: θ : ↑I
⊢ ↑θ ≤ 1

Tactic:
exact le_one _

Goal state after:
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: t : ↑I
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1

Tactic:
split_ifs

Goal state after:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 2 * ↑t

case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 1
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
n : ℕ
⊢ (if 0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3 then
      3 * (Stream'.iterate cantorStep x).get n
    else 3 * (Stream'.iterate cantorStep x).get n - 2) =
    3 *
      ((Stream'.iterate cantorStep x).get n -
        3 ^ n *
          (↑↑(if 0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3 then 0
                else 2) *
            (↑3 ^ (n + 1))⁻¹))

Tactic:
split_ifs

Goal state after:
case pos
x : ℝ
n : ℕ
h✝ : 0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3
⊢ 3 * (Stream'.iterate cantorStep x).get n =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (↑↑0 * (↑3 ^ (n + 1))⁻¹))

case neg
x : ℝ
n : ℕ
h✝ : ¬(0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3)
⊢ 3 * (Stream'.iterate cantorStep x).get n - 2 =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (↑↑2 * (↑3 ^ (n + 1))⁻¹))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = q ((Cube.insertAt i) (x✝, y✝))

Tactic:
apply H.apply_one

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (↑(if ↑(x✝ i) ≤ 1 / 2 then (Path.extend (toLoop i f)) (2 * ↑(x✝ i)) else (Path.extend (toLoop i g)) (2 * ↑(x✝ i) - 1))
      fun j ↦ x✝ ↑j) =
    if ↑(x✝ i) ≤ 1 / 2 then f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))
    else g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))

Tactic:
split_ifs

Goal state after:
case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ↑(x✝ i) ≤ 1 / 2
⊢ (↑((Path.extend (toLoop i f)) (2 * ↑(x✝ i))) fun j ↦ x✝ ↑j) =
    f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))

case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ¬↑(x✝ i) ≤ 1 / 2
⊢ (↑((Path.extend (toLoop i g)) (2 * ↑(x✝ i) - 1)) fun j ↦ x✝ ↑j) =
    g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (insert x s).einfsep = min (⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y) s.einfsep

Tactic:
refine le_antisymm (le_min einfsep_insert_le (einfsep_anti (subset_insert _ _))) ?_
  simp_rw [le_einfsep_iff, inf_le_iff, mem_insert_iff]
  rintro y (rfl | hy) z (rfl | hz) hyz
  · exact False.elim (hyz rfl)
  · exact Or.inl (iInf_le_of_le _ (iInf₂_le hz hyz))
  · rw [edist_comm]
    exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))
  · exact Or.inr (einfsep_le_edist_of_mem hy hz hyz)

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

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s

Tactic:
rw [← isBounded_preimage_toSnowflaking_iff, Metric.isBounded_iff, Metric.isBounded_iff]

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoMetricSpace X
aux : PseudoMetricSpace (Snowflaking X α hα₀ hα₁) := PseudoEMetricSpace.toPseudoMetricSpaceOfDist dist ⋯ ⋯
s : Set (Snowflaking X α hα₀ hα₁)
⊢ (∃ C, ∀ ⦃x : X⦄, x ∈ ⇑toSnowflaking ⁻¹' s → ∀ ⦃y : X⦄, y ∈ ⇑toSnowflaking ⁻¹' s → dist x y ≤ C) ↔
    ∃ C, ∀ ⦃x : Snowflaking X α hα₀ hα₁⦄, x ∈ s → ∀ ⦃y : Snowflaking X α hα₀ hα₁⦄, y ∈ s → dist x y ≤ C
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIicTopology α
⊢ ∀ s ∈ {s | ∃ a, (Iic a)ᶜ = s}, IsOpen[inst✝¹] (⇑toUpper ⁻¹' s)

Tactic:
by rintro _ ⟨a, rfl⟩; exact isClosed_Iic.isOpen_compl

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]
    infer_instance

Goal state after:
Module: Mathlib.Topology.Specialization

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
s : Set (WithUpperSet (Specialization α))
⊢ IsOpen[inst✝¹] (⇑(toEquiv.trans toUpperSet) ⁻¹' s) ↔ IsOpen[instTopologicalSpace] s

Tactic:
by simp [Set.preimage_comp]

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
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)

Tactic:
let Ψ := F ∘ optimalGHInjr X Y

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
F : OptimalGHCoupling X Y → ↥(lp (fun x ↦ ℝ) ∞) := kuratowskiEmbedding (OptimalGHCoupling X Y)
Φ : X → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjl X Y
Ψ : Y → ↥(lp (fun x ↦ ℝ) ∞) := F ∘ optimalGHInjr X Y
⊢ ∃ Φ Ψ, Isometry Φ ∧ Isometry Ψ ∧ ghDist X Y = hausdorffDist (range Φ) (range Ψ)
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.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (𝟙 (skyscraperPresheaf p₀ a)).app (op U)

Tactic:
split_ifs

Goal state after:
case pos
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
h✝ : p₀ ∈ U
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (𝟙 (skyscraperPresheaf p₀ a)).app (op U)

case neg
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
h✝ : p₀ ∉ U
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (𝟙 (skyscraperPresheaf p₀ a)).app (op U)
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 ≫
      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

Goal state after:
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 ⋯
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

Goal state after:
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 ≫ (⋯ ▸ terminalIsTerminal).from (𝓕.obj V) =
    (if h : p₀ ∈ unop U then 𝓕.germ (unop U) p₀ h ≫ f ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (𝓕.obj U)) ≫
      (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then c else ⊤_ C)
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
⊢ ∀ (x : ↑X), IsIso ((stalkFunctor C x).map f.hom)

Tactic:
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:
Module: Mathlib.Topology.Sheaves.Alexandrov

Goal state before:
pp: X : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : Preorder X
inst✝² : Topology.IsUpperSet X
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimits C
F : X ⥤ C
x y z : X
⊢ y ≤ z → y ∈ {y | x ≤ y} → z ∈ {y | x ≤ y}

Tactic:
h1

Goal state after:
X : Type v
inst✝⁴ : TopologicalSpace X
inst✝³ : Preorder X
inst✝² : Topology.IsUpperSet X
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimits C
F : X ⥤ C
x y z : X
h1 : y ≤ z
⊢ y ∈ {y | x ≤ y} → z ∈ {y | x ≤ y}
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
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (⋯ ▸ terminalIsTerminal).from (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j✝)))) ≫ eqToHom ⋯ =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝

Tactic:
comp_eqToHom_iff

Goal state after:
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
X : Presheaf C X✝
j✝ : (OpenNhds p₀)ᵒᵖ
h : p₀ ∉ (OpenNhds.inclusion p₀).obj (unop j✝)
⊢ (⋯ ▸ terminalIsTerminal).from (X.obj (op ((OpenNhds.inclusion p₀).obj (unop j✝)))) =
    colimit.ι ((OpenNhds.inclusion p₀).op ⋙ X) j✝ ≫ eqToHom ⋯
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
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
z : { x // x ∈ segment ℝ ↑y1 ↑y2 }
h1 : sublevelLeft X f t' ↑z ⊆ sublevelLeft X f t' ↑y1
⊢ sublevelLeft X f t' ↑⟨↑z, ⋯⟩ ⊆ sublevelLeft X f t' ↑y1

Tactic:
h1

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
inst✝² : DenselyOrdered β
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
t : β
hinfi_le : ∀ y0 ∈ Y, ∃ x ∈ X, f x y0 ≤ t
a : E
ha : a ∈ X
t' : β
htt' : t < t'
y1 y2 : { x // x ∈ Y }
ht : ∀ x ∈ X, t < max (f x ↑y1) (f x ↑y2)
ha' : IsMinOn (fun x ↦ max (f x ↑y1) (f x ↑y2)) X a
ht' : t' < max (f a ↑y1) (f a ↑y2)
J1 : Set ↑(segment ℝ ↑y1 ↑y2) := setOfPred_sublevelLeft_subset X Y f t t' y1 y2
mem_J1_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J1 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y1
φ : ↑(segment ℝ ↑y1 ↑y2) ≃ₜ ↑(segment ℝ ↑y2 ↑y1) := Homeomorph.setCongr ⋯
J2 : Set ↑(segment ℝ ↑y1 ↑y2) := ⇑φ ⁻¹' setOfPred_sublevelLeft_subset X Y f t t' y2 y1
mem_J2_iff : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), z ∈ J2 ↔ sublevelLeft X f t ↑z ⊆ sublevelLeft X f t' ↑y2
h_mem_Y : ∀ (z : ↑(segment ℝ ↑y1 ↑y2)), ↑z ∈ Y
hJ1J2 : J1 ∩ J2 = ∅
z : { x // x ∈ segment ℝ ↑y1 ↑y2 }
h1 : sublevelLeft X f t' ↑z ⊆ sublevelLeft X f t' ↑y1
⊢ sublevelLeft X f t' ↑y1 ⊆ sublevelLeft X f t' ↑y1
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_1
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsSymm (i.1 ∩ i.2)

Tactic:
rintro _ ⟨⟨_, _, _⟩, _, _, _⟩

Goal state after:
case refine_1
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
i✝ : SetRel X X × SetRel X X
left✝³ : i✝.1 ∈ uniformity X
left✝² : i✝.1.IsSymm
right✝¹ : i✝.1.IsTrans
left✝¹ : i✝.2 ∈ uniformity X
left✝ : i✝.2.IsSymm
right✝ : i✝.2.IsTrans
⊢ SetRel.IsSymm (i✝.1 ∩ i✝.2)
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: case refine_2
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
⊢ ∀ (i : SetRel X X × SetRel X X),
    (i.1 ∈ uniformity X ∧ i.1.IsSymm ∧ i.1.IsTrans) ∧ i.2 ∈ uniformity X ∧ i.2.IsSymm ∧ i.2.IsTrans →
      SetRel.IsTrans (i.1 ∩ i.2)

Tactic:
rintro _ ⟨⟨_, _, _⟩, _, _, _⟩

Goal state after:
case refine_2
X : Type u_1
u u' : UniformSpace X
h : IsUltraUniformity X
h' : IsUltraUniformity X
this : UniformSpace X := u ⊓ u'
i✝ : SetRel X X × SetRel X X
left✝³ : i✝.1 ∈ uniformity X
left✝² : i✝.1.IsSymm
right✝¹ : i✝.1.IsTrans
left✝¹ : i✝.2 ∈ uniformity X
left✝ : i✝.2.IsSymm
right✝ : i✝.2.IsTrans
⊢ SetRel.IsTrans (i✝.1 ∩ i✝.2)