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

Goal state before:
pp: case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : ⇑f '' K ⊆ ⋃₀ t
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s

Tactic:
image_subset_iff

Goal state after:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
⊢ {g | MapsTo (⇑g) K U} ∈
    ⨅ s ∈ {s | f ∈ s ∧ s ∈ image2 (fun K t ↦ {f | MapsTo (⇑f) K (⋃₀ t)}) S {t | t.Finite ∧ t ⊆ T}}, 𝓟 s
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).concat (G i)) x ∈ U

Tactic:
concat_left hfg hxb

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
⊢ (F i) ⟨↑x, ⋯⟩ ∈ U
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ LinearIndependent ℤ (eval (C' C ho)) →
    LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ (⇑(Linear_CC' C hsC ho) ∘ fun l ↦ Products.eval C ↑l)

Tactic:
max_eq_eval_unapply C hsC ho

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
⊢ LinearIndependent ℤ (eval (C' C ho)) →
    LinearIndependent ℤ fun (l : ↑(MaxProducts C ho)) ↦ Products.eval (C' C ho) (↑l).Tail
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hB : IsCountablyCompact B
⊢ IsCountablyCompact (A ∪ B)

Tactic:
by
  rw [isCountablyCompact_iff_countable_open_cover'] at hA hB ⊢
  intro U hUo hAU
  obtain ⟨t₁, ht₁, hA_sub⟩ : ∃ (t₁ : Set ℕ), t₁.Finite ∧ A ⊆ ⋃ k ∈ t₁, U k :=
    hA U hUo (subset_union_left.trans hAU)
  obtain ⟨t₂, ht₂, hB_sub⟩ : ∃ (t₂ : Set ℕ), t₂.Finite ∧ B ⊆ ⋃ k ∈ t₂, U k :=
    hB U hUo (subset_union_right.trans hAU)
  have h : (⋃ k ∈ t₁, U k) ∪ (⋃ k ∈ t₂, U k) = ⋃ k ∈ (t₁ ∪ t₂), U k := by ext; aesop
  exact ⟨t₁ ∪ t₂, ht₁.union ht₂, h ▸ union_subset_union hA_sub hB_sub⟩

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l : Filter α
⊢ ⨅ s ∈ {s | l ∈ s ∧ s ∈ range (Iic ∘ 𝓟)}, 𝓟 s = l.lift' (Iic ∘ 𝓟)

Tactic:
simp only [mem_ofPred_eq, @and_comm (l ∈ _), iInf_and, iInf_range, Filter.lift', Filter.lift,
      (· ∘ ·), mem_Iic, le_principal_iff]

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun i ↦ {l' | s i ∈ l'}

Tactic:
by simpa only [Iic_principal] using h.nhds

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

Goal state before:
pp: case map_zero_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y),
    { toFun := G, continuous_toFun := hG }.toFun (0, x) =
      ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
          ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
        x

pp: case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ?map_zero_left,
                    map_one_left := ?map_one_left }.toFun
                (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
          x

Tactic:
· rintro ⟨x, y⟩
      exact Prod.ext (HSpace.eHmul.1.2 x) (HSpace.eHmul.1.2 y)

Goal state after:
case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ?map_one_left }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
          x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ.refine_1
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x ↦ x / 3) '' preCantorSet n)

Tactic:
simpa [f, div_eq_inv_mul] using f.isClosedEmbedding.isClosed_iff_image_isClosed.mp ih

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
⊢ List.Forall₂ (flip fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) v u

Tactic:
replace hv := hv.flip

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
this : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
hv : List.Forall₂ (fun s a ↦ IsOpen[inst✝] s ∧ a ∈ s) v l
⊢ List.Forall₂ (flip fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) v u
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ coveringNumber (2 * ε) A ≤ externalCoveringNumber ε A

Tactic:
by
  rcases Set.eq_empty_or_nonempty A with rfl | h_nonempty
  · simp
  refine (coveringNumber_le_packingNumber _ A).trans ?_
  exact packingNumber_two_mul_le_externalCoveringNumber ε A

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

Goal state before:
pp: X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
⊢ ∃ f, Continuous f ∧ Function.Surjective f

Tactic:
let g : X ≃ₜ KH := h_emb.toHomeomorph

Goal state after:
X : Type u_1
inst✝² : Nonempty X
inst✝¹ : MetricSpace X
inst✝ : CompactSpace X
this : TopologicalSpace.SeparableSpace X := TopologicalSpace.SecondCountableTopology.to_separableSpace
emb : X → ℕ → ↑unitInterval
h_emb : Topology.IsEmbedding emb
KH : Set (ℕ → ↑unitInterval) := Set.range emb
g : X ≃ₜ ↑KH := h_emb.toHomeomorph
⊢ ∃ f, Continuous f ∧ Function.Surjective f
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C : Set Y
hC_subset : C ⊆ f '' A
hC_cover : IsCover ε (f '' A) C
g : ↑C → X
hg_mem : ∀ (x : ↑C), g x ∈ A
hg : ∀ (x : ↑C), f (g x) = ↑x
⊢ C = f '' range g

Tactic:
· ext
        simp
        grind

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

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
x : α
s : Set α
⊢ ∀ i ∈ s, x ≠ i → (insert x s).einfsep ≤ edist x i

Tactic:
exact fun _ hy hxy => einfsep_le_edist_of_mem (mem_insert _ _) (mem_insert_of_mem _ hy) hxy

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

Goal state before:
pp: case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : HolderWith i r f), ↑i < b
x₁ x₂ : X
hx : ¬x₁ = x₂
b : ℝ≥0∞
hb : 0 < b
⊢ edist (f x₁) (f x₂) < b

Tactic:
obtain ⟨C, hC, hC'⟩ := h (b / edist x₁ x₂ ^ (r : ℝ))
        (ENNReal.div_pos hb.ne.symm (ENNReal.rpow_lt_top_of_nonneg zero_le_coe
          (edist_lt_top x₁ x₂).ne).ne)

Goal state after:
case neg
X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : EMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : HolderWith i r f), ↑i < b
x₁ x₂ : X
hx : ¬x₁ = x₂
b : ℝ≥0∞
hb : 0 < b
C : ℝ≥0
hC : HolderWith C r f
hC' : ↑C < b / edist x₁ x₂ ^ ↑r
⊢ edist (f x₁) (f x₂) < b
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → X i
hx : x ∈ univ.pi s
y : (i : β) → X i
hy : y ∈ univ.pi s
hxy : x ≠ y
⊢ c ≤ edist x y

Tactic:
rw [mem_univ_pi] at hx hy

Goal state after:
β : Type u_2
X : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoEMetricSpace (X b)
s : (b : β) → Set (X b)
c : ℝ≥0∞
h : ∀ (b : β), c ≤ (s b).einfsep
x : (i : β) → X i
hx : ∀ (i : β), x i ∈ s i
y : (i : β) → X i
hy : ∀ (i : β), y i ∈ s i
hxy : x ≠ y
⊢ c ≤ edist x y
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ (if s.Nontrivial then ⨅ d, uncurry dist ↑d else 0) = ⨅ d, uncurry dist ↑d

Tactic:
if_pos hs

Goal state after:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ ⨅ d, uncurry dist ↑d = ⨅ d, uncurry dist ↑d
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ IsBounded (⇑toSnowflaking ⁻¹' s) ↔ IsBounded s

Tactic:
← image_ofSnowflaking_eq_preimage,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ IsBounded (⇑ofSnowflaking '' s) ↔ IsBounded s
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set X
⊢ IsBounded (⇑toSnowflaking '' s) ↔ IsBounded s

Tactic:
← isBounded_image_ofSnowflaking_iff,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : Bornology X
s : Set X
⊢ IsBounded (⇑ofSnowflaking '' ⇑toSnowflaking '' s) ↔ IsBounded s
Module: Mathlib.Topology.MetricSpace.Snowflaking

Goal state before:
pp: X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ ediam (⇑toSnowflaking ⁻¹' s) = ediam s ^ α⁻¹

Tactic:
← image_ofSnowflaking_eq_preimage,

Goal state after:
X : Type u_1
α : ℝ
hα₀ : 0 < α
hα₁ : α ≤ 1
inst✝ : PseudoEMetricSpace X
s : Set (Snowflaking X α hα₀ hα₁)
⊢ ediam (⇑ofSnowflaking '' s) = ediam s ^ α⁻¹
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: case mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : ∀ x ∈ F, x ∈ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f ↦ ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}

Tactic:
Subtype.forall'

Goal state after:
case mpr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
F : Set (Set α)
hF : F.Finite
hs : ∀ (x : { a // a ∈ F }), ↑x ∈ {s | ∃ a, (Ici a)ᶜ = s}
this : Finite ↑F
⊢ (fun f ↦ ⋂₀ f) F ∈ {s | ∃ t, t.Finite ∧ ⋂ i ∈ t, (Ici i)ᶜ = s}
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
⊢ ScottContinuousOn D f ↔ Continuous[inst✝⁴, inst✝²] f

Tactic:
refine ⟨fun h ↦ continuous_def.2 fun u hu ↦ ?_, ?_⟩
  · rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)]
    exact ⟨(isUpperSet_of_isOpen (D := univ) hu).preimage (h.monotone D hD),
      fun t h₀ hd₁ hd₂ a hd₃ ha ↦ image_inter_nonempty_iff.mp <|
        (isOpen_iff_isUpperSet_and_dirSupInaccOn (D := univ).mp hu).2 trivial (Nonempty.image f hd₁)
        (directedOn_image.mpr (hd₂.mono @(h.monotone D hD))) (h h₀ hd₁ hd₂ hd₃) ha⟩
  · refine fun hf t h₀ d₁ d₂ a d₃ ↦
      ⟨(monotone_of_continuous (D := D) hf).mem_upperBounds_image d₃.1,
      fun b hb ↦ ?_⟩
    by_contra h
    let u := (Iic b)ᶜ
    have hu : IsOpen (f ⁻¹' u) := isClosed_Iic.isOpen_compl.preimage hf
    rw [isOpen_iff_isUpperSet_and_dirSupInaccOn (D := D)] at hu
    obtain ⟨c, hcd, hfcb⟩ := hu.2 h₀ d₁ d₂ d₃ h
    simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
      mem_ofPred] at hb
    exact hfcb <| hb _ hcd

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] s ↔ ScottContinuous fun x ↦ x ∈ s

Tactic:
rw [← scottContinuousOn_univ, scottContinuousOn_iff_continuous (fun _ _ _ ↦ by trivial)]

Goal state after:
α : Type u_1
inst✝² : Preorder α
s : Set α
inst✝¹ : TopologicalSpace α
inst✝ : IsScott α univ
⊢ IsOpen[inst✝¹] s ↔ Continuous[inst✝¹, _] fun x ↦ x ∈ s
Module: Mathlib.Topology.Order.HullKernel

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
T : Set α
inst✝ : OrderTop α
hT : ∀ p ∈ T, InfPrime p
F : Finset α
⊢ hull T (F.inf id) = T ↓∩ ⋃ a ∈ ↑F, Set.Ici a

Tactic:
induction F using Finset.cons_induction with
  | empty =>
    simp only [coe_empty, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.preimage_empty,
      inf_empty]
    by_contra hf
    rw [← Set.not_nonempty_iff_eq_empty, not_not] at hf
    obtain ⟨x, hx⟩ := hf
    exact (hT x (Subtype.coe_prop x)).1 (isMax_iff_eq_top.mpr (eq_top_iff.mpr hx))
  | cons a F' _ I4 => simp [hull_inf hT, I4]

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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y

Tactic:
have B :
    ∀ p q : NonemptyCompacts ℓ_infty_ℝ,
      ⟦p⟧ = toGHSpace X →
        ⟦q⟧ = toGHSpace Y →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            hausdorffDist (p : Set ℓ_infty_ℝ) q := by
    intro p q hp hq
    by_cases h :
      hausdorffDist (p : Set ℓ_infty_ℝ) q < diam (univ : Set X) + 1 + diam (univ : Set Y)
    · exact A p q hp hq h
    · calc
        hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤
            HD (candidatesBDist X Y) :=
          hausdorffDist_optimal_le_HD _ _ candidatesBDist_mem_candidatesB
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := HD_candidatesBDist_le
        _ ≤ hausdorffDist (p : Set ℓ_infty_ℝ) q := not_lt.1 h

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
A :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y →
        hausdorffDist ↑p ↑q < diam univ + 1 + diam univ →
          hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
B :
  ∀ (p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)),
    ⟦p⟧ = toGHSpace X →
      ⟦q⟧ = toGHSpace Y → hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = ghDist X Y
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
A : C
inst✝ : HasTerminal C
U : (Opens ↑X)ᵒᵖ
h : p₀ ∉ unop U
⊢ IsTerminal ((skyscraperSheaf p₀ A).obj.obj U)

Tactic:
dsimp
  rw [if_neg h]
  exact terminalIsTerminal

Goal state after:
Module: Mathlib.Topology.SmallInductiveDimension

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
n : ℕ
h : smallInductiveDimension X ≤ ↑n
⊢ HasSmallInductiveDimensionLE X n

Tactic:
by
  apply hasSmallInductiveDimensionLT_of_smallInductiveDimension_lt (h.trans_lt _)
  exact_mod_cast n.lt_add_one

Goal state after:
Module: Mathlib.Topology.Sion

Goal state before:
pp: case inr
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 : ∀ (x : ↑(segment ℝ ↑y1 ↑y2)), x ∉ J1 ∩ J2
hJ1_union_J2 : Subtype.val '' (J1 ∪ J2) = segment ℝ ↑y1 ↑y2
this :
  ∀ (u v : Set ↑(segment ℝ ↑y1 ↑y2)), IsClosed u → IsClosed v → univ ⊆ u ∪ v → univ ∩ (u ∩ v) = ∅ → univ ⊆ u ∨ univ ⊆ v
hJ1 : IsClosed J1
hJ2 : IsClosed J2
h_univ : univ ⊆ J1 ∪ J2
h_inter : univ ∩ (J1 ∩ J2) = ∅
h2 : univ ⊆ J2
⊢ ⟨↑y1, ⋯⟩ ∈ J1

Tactic:
grw [mem_J1_iff, monotone_sublevelLeft y1 htt'.le]

Goal state after:
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²¹ : NontriviallyNormedField 𝕜
B : Type u_3
inst✝²⁰ : TopologicalSpace B
F₁ : Type u_4
inst✝¹⁹ : NormedAddCommGroup F₁
inst✝¹⁸ : NormedSpace 𝕜 F₁
E₁ : B → Type u_5
inst✝¹⁷ : (x : B) → AddCommGroup (E₁ x)
inst✝¹⁶ : (x : B) → Module 𝕜 (E₁ x)
inst✝¹⁵ : TopologicalSpace (TotalSpace F₁ E₁)
F₂ : Type u_6
inst✝¹⁴ : NormedAddCommGroup F₂
inst✝¹³ : NormedSpace 𝕜 F₂
E₂ : B → Type u_7
inst✝¹² : (x : B) → AddCommGroup (E₂ x)
inst✝¹¹ : (x : B) → Module 𝕜 (E₂ x)
inst✝¹⁰ : TopologicalSpace (TotalSpace F₂ E₂)
inst✝⁹ : (x : B) → TopologicalSpace (E₁ x)
inst✝⁸ : FiberBundle F₁ E₁
inst✝⁷ : (x : B) → TopologicalSpace (E₂ x)
inst✝⁶ : FiberBundle F₂ E₂
e₁ e₁' : Trivialization F₁ TotalSpace.proj
e₂ e₂' : Trivialization F₂ TotalSpace.proj
inst✝⁵ : Trivialization.IsLinear 𝕜 e₁
inst✝⁴ : Trivialization.IsLinear 𝕜 e₁'
inst✝³ : Trivialization.IsLinear 𝕜 e₂
inst✝² : Trivialization.IsLinear 𝕜 e₂'
inst✝¹ : ∀ (x : B), ContinuousAdd (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
x : B
x✝ : x ∈ (continuousAlternatingMap 𝕜 ι e₁ e₂).baseSet
L L' : E₁ x [⋀^ι]→L[𝕜] E₂ x
⊢ (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L + L' }).2 =
    (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L }).2 +
      (↑(continuousAlternatingMap 𝕜 ι e₁ e₂) { proj := x, snd := L' }).2

Tactic:
ext; simp [continuousAlternatingMap, Pretrivialization.toFun']

Goal state after: