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

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
𝔖_covers : ⋃₀ 𝔖 = univ
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsClosed[UniformOnFun.topologicalSpace X α 𝔖] (range (⇑(UniformOnFun.ofFun 𝔖) ∘ F)) ↔
    IsClosed[Pi.topologicalSpace] (range F)

Tactic:
simp_rw [isClosed_iff_clusterPt, ← Filter.map_top, ← mapClusterPt_def,
    mapClusterPt_iff_ultrafilter, range_comp, (UniformOnFun.ofFun 𝔖).surjective.forall,
    ← EquicontinuousOn.tendsto_uniformOnFun_iff_pi 𝔖_compact 𝔖_covers F_eqcont,
    (UniformOnFun.ofFun 𝔖).injective.mem_set_image]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
n : ℕ
⊢ ∀ (i : cell n), ↑(map n i) '' closedBall 0 1 ⊆ ⋃ (hx : n < N), ⋃ j, ↑(map (↑⟨n, hx⟩) j) '' closedBall 0 1

Tactic:
intro i

Goal state after:
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
n : ℕ
i : cell n
⊢ ↑(map n i) '' closedBall 0 1 ⊆ ⋃ (hx : n < N), ⋃ j, ↑(map (↑⟨n, hx⟩) j) '' closedBall 0 1
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝² : T2Space X
inst✝¹ : RelCWComplex C D
inst✝ : FiniteDimensional C
E : Subcomplex C
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell (↑E) n)

Tactic:
filter_upwards [FiniteDimensional.eventually_isEmpty_cell (C := C) (D := D)] with n hn

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝² : T2Space X
inst✝¹ : RelCWComplex C D
inst✝ : FiniteDimensional C
E : Subcomplex C
n : ℕ
hn : IsEmpty (cell C n)
⊢ IsEmpty (cell (↑E) n)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), IsOpen[inst✝ i] (⇑f ⁻¹' ⇑equiv.symm ⁻¹' ⇑equiv ⁻¹' U)

Tactic:
intro i

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
U : Set Y
hU : IsOpen[tY] U
i : ι
⊢ ∀ (f : C(X i, Y)), IsOpen[inst✝ i] (⇑f ⁻¹' ⇑equiv.symm ⁻¹' ⇑equiv ⁻¹' U)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f)

Tactic:
intro i

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
⊢ ∀ (f : C(X i, Y)), Continuous[inst✝² i, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)

Tactic:
intro i

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
⊢ ∀ (f : C(X i, Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
Module: Mathlib.Topology.Convenient.ContinuousMapGeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ ∀ ⦃i : ι⦄ (f : C(X i, Y)), Continuous[inst✝² i, _] (⇑equiv.symm ∘ ⇑f)

Tactic:
intro i

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝¹ : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
i : ι
⊢ ∀ (f : C(X i, Y)), Continuous[inst✝² i, _] (⇑equiv.symm ∘ ⇑f)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
⊢ I n ⊆ J n

Tactic:
intro i

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
n : ℕ
i : cell C n
⊢ i ∈ I n → i ∈ J n
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
⊢ cellFrontier 1 e = ↑(map 1 e) '' {-1, 1}

Tactic:
by
  rw [cellFrontier]
  congr 1
  ext f
  simp only [mem_sphere_iff_norm, sub_zero, Pi.norm_def, Finset.univ_unique, Fin.default_eq_zero,
    Fin.isValue, Finset.sup_singleton, coe_nnnorm, Real.norm_eq_abs, abs_eq (zero_le_one' ℝ),
    mem_insert_iff, mem_singleton_iff]
  rw [eq_const_of_unique (f := f), ← funext_iff_of_subsingleton (x := 0) (y := 0)]
  simp [const_apply, or_comm]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
⊢ ∀ (i : I), Continuous fun a ↦ if J i then a i else false

Tactic:
intro i

Goal state after:
I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
i : I
⊢ Continuous fun a ↦ if J i then a i else false
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ ∃ a_1, (iso_map C J) a_1 = a

Tactic:
refine ⟨⟨fun i ↦ if hi : J i then a.val ⟨i, hi⟩ else false, ?_⟩, ?_⟩

Goal state after:
case refine_2.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false) ∈ π C J

case refine_2.refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (iso_map C J) ⟨fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false, ?refine_2.refine_1⟩ = a
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a : ↑(IndexFunctor.obj C J)
⊢ (fun i ↦ if hi : J i then ↑a ⟨i, hi⟩ else false) ∈ π C J

Tactic:
rcases a with ⟨_, y, hy, rfl⟩

Goal state after:
case refine_2.refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
y : (i : I) → (fun i ↦ Bool) i
hy : y ∈ C
⊢ (fun i ↦ if hi : J i then ↑⟨(precomp Subtype.val) y, ⋯⟩ ⟨i, hi⟩ else false) ∈ π C J
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ ∀ (i : I), Continuous fun a ↦ if ord I i = o then true else a i

Tactic:
intro i

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun a ↦ if ord I i = o then true else a i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
⊢ ∀ a ∈ ↑l, J a

Tactic:
intro i

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
inst✝ : (j : I) → Decidable (J j)
h : isGood (π C J) l
i : I
⊢ i ∈ ↑l → J i
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ f ∈ ℤ ∙ eval {fun x ↦ false} nil

Tactic:
rw [Submodule.mem_span_singleton]

Goal state after:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ ∃ a, a • eval {fun x ↦ false} nil = f
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
x : I → Bool
hx : x ∈ C1 C ho
⊢ SwapTrue o (Proj (fun x ↦ ord I x < o) x) = x

Tactic:
by
  ext i
  dsimp [SwapTrue, Proj]
  split_ifs with hi h
  · rw [ord_term ho] at hi
    rw [← hx.2, hi]
  · rfl
  · simp only [not_lt] at h
    have h' : o < ord I i := lt_of_le_of_ne h (Ne.symm hi)
    specialize hsC x hx.1 i
    rw [← not_imp_not] at hsC
    simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC
    exact (hsC h').symm

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case refine_1
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
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
y : I → Bool
hyC : y ∈ C
⊢ Proj (fun x ↦ ord I x < o) y ∈ C0 C ho ∨ Proj (fun x ↦ ord I x < o) y ∈ π (C1 C ho) fun x ↦ ord I x < o

Tactic:
← union_C0C1_eq C ho

Goal state after:
case refine_1
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
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
y : I → Bool
hyC : y ∈ C0 C ho ∪ C1 C ho
⊢ Proj (fun x ↦ ord I x < o) y ∈ C0 C ho ∨ Proj (fun x ↦ ord I x < o) y ∈ π (C1 C ho) fun x ↦ ord I x < o
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case refine_3
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
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx : x ∈ C
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx⟩ =
    f ⟨x, hx⟩

Tactic:
← union_C0C1_eq C ho

Goal state after:
case refine_3
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
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
hx✝ : x ∈ C
hx : x ∈ C0 C ho ∪ C1 C ho
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx✝⟩ =
    f ⟨x, hx✝⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
⊢ ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)

Tactic:
intro i

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
i : I
⊢ i ∈ ↑l → ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
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}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(GoodProducts (π C fun x ↦ ord I x < o))
x✝ : ↑C
⊢ (Products.eval C ↑l) x✝ = ((πs C o) (eval (π C fun x ↦ ord I x < o) l)) x✝

Tactic:
rw [← Products.eval_πs C (Products.prop_of_isGood _ _ l.prop)]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(GoodProducts (π C fun x ↦ ord I x < o))
x✝ : ↑C
⊢ ((πs C o) (Products.eval (π C fun x ↦ ord I x < o) ↑l)) x✝ = ((πs C o) (eval (π C fun x ↦ ord I x < o) l)) x✝
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ ↑n < ↑n + 1

Tactic:
norm_cast

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ n < n + 1
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ cellFrontier n j ⊆ ↑(skeletonLT C ↑n)

Tactic:
apply subset_trans hI

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
⊢ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j ⊆ ↑(skeletonLT C ↑n)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j✝ : cell C n
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier n j✝ ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j
x : X
i : ℕ
iltn : i < n
j : cell C i
left✝ : j ∈ I i
xmem : x ∈ closedCell i j
⊢ ↑i < ↑n

Tactic:
norm_cast

Goal state after:
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
⊢ ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i

Tactic:
intro i

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
i : I
⊢ i ∈ ↑l.Tail → ↑x i = SwapTrue o (↑x) i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case e_a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
⊢ (⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j) ∪ ⋃ j, closedCell n j = ⋃ m, ⋃ (_ : ↑m < ↑n + 1), ⋃ j, closedCell m j

Tactic:
norm_cast

Goal state after:
case e_a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
⊢ (⋃ m, ⋃ (_ : m < n), ⋃ j, closedCell m j) ∪ ⋃ j, closedCell n j = ⋃ m, ⋃ (_ : m < n + 1), ⋃ j, closedCell m j
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ ⋃ n, ↑(skeleton C ↑n) = C

Tactic:
apply subset_antisymm (iUnion_subset_iff.2 fun _ ↦ (skeleton C _).subset_complex)
  simp_rw [← union_iUnion_openCell_eq_complex, union_subset_iff, iUnion₂_subset_iff]
  exact ⟨subset_iUnion_of_subset 0 (skeleton C 0).base_subset,
    fun n i ↦ subset_iUnion_of_subset _ (openCell_subset_skeleton n i)⟩

Goal state after:
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
⊢ ∀ (a : I), (a ∈ ↑l.Tail → ↑x a = true) = (a ∈ ↑l.Tail → SwapTrue o (↑x) a = true)

Tactic:
intro i

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
i : I
⊢ (i ∈ ↑l.Tail → ↑x i = true) = (i ∈ ↑l.Tail → SwapTrue o (↑x) i = true)
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case pos
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ ⋂ n, dissipate C n = ∅
f : ∀ (n : ℕ), dissipate C n ∈ S
⊢ ∃ n, dissipate C n = ∅

Tactic:
exact h (dissipate C) directed_dissipate f this.2

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

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
V : ℕ → Set E := fun n ↦ (closure[inst✝] (x '' Ici n))ᶜ
hVmono : Monotone V
hac : ∀ a ∈ A, ∃ x_1, a ∉ closure[inst✝] (x '' Ici x_1)
hAV : A ⊆ ⋃ n, V n
t : Finset ℕ
ht : A ⊆ ⋃ i ∈ t, V i
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → x b ∈ A
m : ℕ := max N (t.sup id)
⊢ False

Tactic:
obtain ⟨j, hjt, hjV⟩ := mem_iUnion₂.mp (ht (hN m (le_max_left _ _)))

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
V : ℕ → Set E := fun n ↦ (closure[inst✝] (x '' Ici n))ᶜ
hVmono : Monotone V
hac : ∀ a ∈ A, ∃ x_1, a ∉ closure[inst✝] (x '' Ici x_1)
hAV : A ⊆ ⋃ n, V n
t : Finset ℕ
ht : A ⊆ ⋃ i ∈ t, V i
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → x b ∈ A
m : ℕ := max N (t.sup id)
j : ℕ
hjt : j ∈ t
hjV : x m ∈ V j
⊢ False