mathlib-initiative/mathlib-tactics huggingface dataset:
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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ (⇑(Linear_CC' C hsC ho) ∘ fun l ↦ Products.eval C ↑l) = fun l ↦ Products.eval (C' C ho) (↑l).Tail

Tactic:
ext1 l

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
⊢ (⇑(Linear_CC' C hsC ho) ∘ fun l ↦ Products.eval C ↑l) l = Products.eval (C' C ho) (↑l).Tail
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
⊢ TotallyBounded A

Tactic:
refine totallyBounded_of_finite_discretization fun ε ε0 => ?_

Goal state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
⊢ ∃ β_1 x F, ∀ (x y : ↑A), F x = F y → dist ↑x ↑y < ε
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_2
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ ↑B := Set.Infinite.natEmbedding B hB
x : ℕ → E := Subtype.val ∘ ⇑f
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
⊢ map x atTop ≤ 𝓟 B

Tactic:
· exact tendsto_principal.mpr <| Eventually.of_forall fun n => (f n).2

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

Goal state before:
pp: E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
this : ∃ a ∈ range x ∩ A, MapClusterPt a cofinite x
⊢ ∃ a ∈ A, MapClusterPt a cofinite x

Tactic:
by aesop

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

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ γ (qRight (t, 0)) = y

Tactic:
conv_rhs => rw [← γ.target]

Goal state after:
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ γ (qRight (t, 0)) = γ 1
Module: Mathlib.Topology.Instances.PNat

Goal state before:
pp: n : ℕ+
r : ℝ
⊢ IsCompact (val ⁻¹' Set.Icc ⌈↑↑n - r⌉₊ ⌊↑↑n + r⌋₊)

Tactic:
exact ((Set.finite_Icc _ _).preimage PNat.coe_injective.injOn).isCompact

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝² : Zero R
inst✝¹ : Add R
inst✝ : LE R
d x✝ : PseudoMetric X R
⊢ ∀ ⦃a₂ : PseudoMetric X R⦄, x✝.toFun = a₂.toFun → x✝ = a₂

Tactic:
by aesop

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

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ (if x✝ = j then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))
    else if x✝ = i then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)) else y✝ x✝) =
    if x✝ = i then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))
    else if x✝ = j then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)) else y✝ x✝

Tactic:
apply ite_ite_comm

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ (if x✝ = j then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)
    else if x✝ = i then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)) else y✝ x✝) =
    if x✝ = i then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))
    else if x✝ = j then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1) else y✝ x✝

Tactic:
apply ite_ite_comm

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ (if x✝ = j then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))
    else if x✝ = i then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1) else y✝ x✝) =
    if x✝ = i then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)
    else if x✝ = j then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)) else y✝ x✝

Tactic:
apply ite_ite_comm

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ (if x✝ = j then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)
    else if x✝ = i then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1) else y✝ x✝) =
    if x✝ = i then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)
    else if x✝ = j then Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1) else y✝ x✝

Tactic:
apply ite_ite_comm

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h : packingNumber ε A ≠ ⊤
hA : A = ∅
⊢ ∃ C ⊆ A, C.Finite ∧ IsSeparated (↑ε) C ∧ C.encard = packingNumber ε A

Tactic:
simp [hA, packingNumber]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ IsTopologicalBasis (lowerBasis α)

Tactic:
convert! isTopologicalBasis_of_subbasis (topology_eq α)

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLower α
⊢ lowerBasis α = (fun f ↦ ⋂₀ f) '' {f | f.Finite ∧ f ⊆ {s | ∃ a, (Ici a)ᶜ = s}}
Module: Mathlib.Topology.Order.UpperLowerSetTopology

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst✝³, inst✝²] f
a b : α
hab : a ∈ closure[inst✝³] {b}
⊢ a ∈ closure[inst✝³] (f ⁻¹' {f b})

Tactic:
apply mem_of_mem_of_subset hab

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : Topology.IsUpperSet α
inst✝ : Topology.IsUpperSet β
f : α → β
hf : Continuous[inst✝³, inst✝²] f
a b : α
hab : a ∈ closure[inst✝³] {b}
⊢ closure[inst✝³] {b} ⊆ closure[inst✝³] (f ⁻¹' {f b})
Module: Mathlib.Topology.Order.LowerUpperTopology

Goal state before:
pp: ⊢ sierpinskiSpace = upper Prop

Tactic:
Topology.upper,

Goal state after:
⊢ sierpinskiSpace = generateFrom {s | ∃ a, (Iic a)ᶜ = s}
Module: Mathlib.Topology.Order.Category.FrameAdjunction

Goal state before:
pp: case h
L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x | x (f t a)} = t
⊢ {x | ⨆ i, ⨆ (i_1 : i ∈ S), x (f i i_1)} = ⋃₀ S

Tactic:
iSup_Prop_eq,

Goal state after:
case h
L : Type u_1
inst✝ : CompleteLattice L
S : Set (Set (PT L))
f : (t : Set (PT L)) → t ∈ S → L
hf : ∀ (t : Set (PT L)) (a : t ∈ S), {x | x (f t a)} = t
⊢ {x | ∃ i, ∃ (i_1 : i ∈ S), x (f i i_1)} = ⋃₀ S
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Iio c)

Tactic:
· have : IsOpen (⋃ a ∈ c.left, Iio a) := isOpen_biUnion fun _ _ ↦ isOpen_Iio
    convert this
    ext
    simp [principal_lt_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T : Set α
ι : Sort v
s : ι → α
⊢ hull T (iSup s) = ⋂ i, hull T (s i)

Tactic:
by aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
T S : Set α
⊢ hull T (sSup S) = ⋂₀ {x | ∃ a ∈ S, hull T a = x}

Tactic:
by aesop

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

Goal state before:
pp: case neg
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
p q : NonemptyCompacts ↥(lp (fun n ↦ ℝ) ∞)
hp : ⟦p⟧ = toGHSpace X
hq : ⟦q⟧ = toGHSpace Y
h : ¬hausdorffDist ↑p ↑q < diam univ + 1 + diam univ
⊢ hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) ≤ hausdorffDist ↑p ↑q

Tactic:
· 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:
Module: Mathlib.Topology.Order.LawsonTopology

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed[L] s ↔ DirSupClosed s

Tactic:
by
  rw [lawsonClosed_iff_scottClosed_of_isLowerSet L S _ h,
    @IsScott.isClosed_iff_isLowerSet_and_dirSupClosed]
  simp_all

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

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

Tactic:
LowerSet.coe_Iic,

Goal state after:
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : TopologicalSpace α
inst✝ : IsLawson α
a : α
⊢ IsClosed[WithLawson.instTopologicalSpace] (Iic a)
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.{w, v} C
inst✝ : HasTerminal C
A : C
U V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∉ unop W
⊢ (if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) =
    (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) ≫
      if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop V then A else ⊤_ C)

Tactic:
rw [dif_neg hW]

Goal state after:
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 V W : (Opens ↑X)ᵒᵖ
iVU : U ⟶ V
iWV : V ⟶ W
hW : p₀ ∉ unop W
⊢ (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C) =
    (if h : p₀ ∈ unop V then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop U then A else ⊤_ C)) ≫
      if h : p₀ ∈ unop W then eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from (if p₀ ∈ unop V then A else ⊤_ C)
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 : TopCat
inst✝¹ : Preorder ↑X
inst✝ : Topology.IsUpperSet ↑X
F : ↑X ⥤ C
α : Type v
Us : α → Opens ↑X
S : Cone ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op ⋙ principalsKanExtension F)
V : Opens ↑X
i : α
hV : V ≤ Us i
left✝ : Discrete PUnit.{1}
x : ↑X
f : (fromPUnit (Opposite.op V)).obj left✝ ⟶ (principals ↑X).obj x
e : principalOpen x ≤ V
VV : OpensLeCover Us := { obj := V, property := ⋯ }
xx : OpensLeCover Us := { obj := principalOpen x, property := ⋯ }
ee : xx ⟶ VV := ObjectProperty.homMk e.hom
⊢ {
            pt :=
              limit
                (StructuredArrow.proj ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op.obj (Opposite.op VV))
                    (principals ↑X) ⋙
                  F),
            π :=
              {
                app := fun g ↦
                  limit.π
                    (StructuredArrow.proj ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op.obj (Opposite.op VV))
                        (principals ↑X) ⋙
                      F)
                    ((StructuredArrow.map ((ObjectProperty.ι fun V ↦ ∃ i, V ≤ Us i).op.map ee.op)).obj g),
                naturality := ⋯ } }.π.app
      { left := { as := PUnit.unit }, right := x, hom := 𝟙 (Opposite.op (principalOpen x)) } =
    limit.π (StructuredArrow.proj (Opposite.op V) (principals ↑X) ⋙ F) { left := left✝, right := x, hom := f }

Tactic:
by aesop

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

Goal state before:
pp: case h
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
W : Opens ↑X
hyW : ↑y ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW : (ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.map ιWV.op)) f
z : ↥U
hz : z ∈ Subtype.val ⁻¹' ↑W
⊢ (ConcreteCategory.hom (F.germ U ↑z ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑z ⋯)) f

Tactic:
← F.germ_res_apply ιWU z hz,

Goal state after:
case h
X : TopCat
C : Type u
inst✝⁴ : Category.{v, u} C
CC : C → Type v
FC : C → C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : Limits.HasColimits C
F : Presheaf C X
inst✝ : Limits.PreservesFilteredColimits (forget C)
U : Opens ↑X
hF_bij : ∀ (x : ↑X) (hx : x ∈ U), Bijective ⇑(ConcreteCategory.hom (F.germ U x hx))
x : ↑X
hx : x ∈ U
y : ↥U
g : ToType (F.stalk x)
V : Opens ↑X
f : ToType (F.obj (op V))
hyV : ↑y ∈ V
hgf : (ConcreteCategory.hom (F.germ U ↑y ⋯)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.germ V ↑y ⋯)) f
W : Opens ↑X
hyW : ↑y ∈ W
ιWU : W ⟶ U
ιWV : W ⟶ V
hW : (ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g) = (ConcreteCategory.hom (F.map ιWV.op)) f
z : ↥U
hz : z ∈ Subtype.val ⁻¹' ↑W
⊢ (ConcreteCategory.hom (F.germ W (↑z) hz)) ((ConcreteCategory.hom (F.map ιWU.op)) (surjInv ⋯ g)) =
    (ConcreteCategory.hom (F.germ V ↑z ⋯)) f
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⌋₊
⊢ diam univ ≤ C

Tactic:
exact hdiam q qt

Goal state after:
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
b : β
y : ↑Y
hfy : LowerSemicontinuousOn (fun x ↦ f x ↑y) X
⊢ IsClosed (sublevelLeft X f b ↑y)

Tactic:
← lowerSemicontinuous_restrict_iff,

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
b : β
y : ↑Y
hfy : LowerSemicontinuous (X.domRestrict fun x ↦ f x ↑y)
⊢ IsClosed (sublevelLeft X f b ↑y)
Module: Mathlib.Topology.Spectral.ConstructibleTopology

Goal state before:
pp: X : Type u_1
inst✝⁴ : TopologicalSpace X
inst✝³ : CompactSpace X
inst✝² : QuasiSober X
inst✝¹ : PrespectralSpace X
inst✝ : QuasiSeparatedSpace X
𝔅 : Set (Set X) := constructibleTopologySubbasis X
𝒮 : Set (Set (Set X)) := {P | P ⊆ 𝔅 ∧ (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) ∧ ⋂₀ P = ∅}
this : 𝒮 = ∅
⊢ ∀ P ⊆ 𝔅, (∀ Q ⊆ P, Q.Finite → (⋂₀ Q).Nonempty) → (⋂₀ P).Nonempty

Tactic:
by contrapose! this; tauto

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

Goal state before:
pp: X : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X n)
inst✝ : ∀ (n : ℕ), Nonempty (X n)
⊢ CompleteSpace GHSpace

Tactic:
set d := fun n : ℕ ↦ ((1 : ℝ) / 2) ^ n

Goal state after:
X : ℕ → Type
inst✝² : (n : ℕ) → MetricSpace (X n)
inst✝¹ : ∀ (n : ℕ), CompactSpace (X n)
inst✝ : ∀ (n : ℕ), Nonempty (X n)
d : ℕ → ℝ := fun n ↦ (1 / 2) ^ n
⊢ CompleteSpace GHSpace
Module: Mathlib.Topology.UniformSpace.Ultra.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : DiscreteUniformity X
this : (Filter.principal SetRel.id).HasBasis (fun x ↦ True) fun x ↦ SetRel.id
⊢ IsUltraUniformity X

Tactic:
← DiscreteUniformity.eq_principal_setRelId

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : DiscreteUniformity X
this : (uniformity X).HasBasis (fun x ↦ True) fun x ↦ SetRel.id
⊢ IsUltraUniformity X
Module: Mathlib.Topology.VectorBundle.ContinuousAlternatingMap

Goal state before:
pp: 𝕜 : Type u_1
ι : Type u_2
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : Fintype ι
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₁)
inst✝¹² : (x : B) → TopologicalSpace (E₁ x)
inst✝¹¹ : FiberBundle F₁ E₁
inst✝¹⁰ : VectorBundle 𝕜 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✝² : VectorBundle 𝕜 F₂ E₂
inst✝¹ : ∀ (x : B), IsTopologicalAddGroup (E₂ x)
inst✝ : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)
⊢ ∀
    e ∈
      {e |
        ∃ e₁ e₂,
          ∃ (x : MemTrivializationAtlas e₁) (x_1 : MemTrivializationAtlas e₂), e = continuousAlternatingMap 𝕜 ι e₁ e₂},
    Pretrivialization.IsLinear 𝕜 e

Tactic:
rintro _ ⟨e₁, he₁, e₂, he₂, rfl⟩
    infer_instance

Goal state after: