mathlib-initiative/mathlib-tactics huggingface dataset:
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
E : Subcomplex C
⊢ ∀ (n : ℕ) (i : ↑(E.I n)),
    ∃ I, MapsTo (↑(map n ↑i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m ↑j) '' closedBall 0 1)

Tactic:
intro n

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
⊢ ∀ (i : ↑(E.I n)),
    ∃ I, MapsTo (↑(map n ↑i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m ↑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
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
⊢ ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
intro n

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
A : Set X
hA : A ⊆ ↑E
h : (∀ (n : ℕ) (j : ↑(E.I n)), IsClosed[t] (A ∩ ↑(map n ↑j) '' closedBall 0 1)) ∧ IsClosed[t] (A ∩ D)
n : ℕ
⊢ 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
⊢ ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty

Tactic:
have claim6 : ∀ P ∈ C2, (P : Set (Ultrafilter X)).Nonempty := by
    suffices ∀ P ∈ C2, P ∈ C0 ∨ ∃ Q ∈ C0, P = AA ∩ Q by
      intro P hP
      rcases this P hP with h | h
      · exact claim2 _ h
      · rcases h with ⟨Q, hQ, rfl⟩
        exact claim3 _ hQ
    intro P hP
    exact claim5.finiteInterClosure_insert _ hP

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
⊢ ∀ (T : fsu), ι T ⊆ C1 → (⋂₀ ι T).Nonempty
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
⊢ Injective (closedCell 0)

Tactic:
by
  intro x y h
  rw [closedCell_zero_eq_singleton, closedCell_zero_eq_singleton, singleton_eq_singleton_iff] at h
  exact injective_map_zero C h

Goal state after:
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 : ℕ) (i_1 : cell C i), D ∩ openCell i i_1 = ∅

Tactic:
intro n

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
⊢ ∀ (i : cell C n), D ∩ openCell n i = ∅
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
inst✝ : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (n + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j
m : ℕ
mlt : m < n + 1
⊢ IsClosed[t] (⋃ i ∈ I ↑⟨m, mlt⟩, A ∩ closedCell (↑⟨m, mlt⟩) i)

Tactic:
rw [← iUnion_subtype (fun i ↦ i ∈ I m) (fun i ↦ A ∩ closedCell m i.1)]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (n + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j
m : ℕ
mlt : m < n + 1
⊢ IsClosed[t] (⋃ x, A ∩ closedCell m ↑x)
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
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
⊢ ∀ (n : ℕ) (j : cell C n), IsClosed[t] (A ∩ closedCell n j)

Tactic:
intro n

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
⊢ ∀ (j : cell C n), IsClosed[t] (A ∩ closedCell n j)
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
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
j : cell C n
⊢ IsClosed[t] (A ∩ closedCell n j)

Tactic:
induction n using Nat.case_strong_induction_on with

Goal state after:
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
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
⊢ ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
intro n

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
h : ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint A (openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
n : ℕ
⊢ 0 < n → ∀ (j : cell C n), IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
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
i : I
⊢ (if ord I i = o then true else if ord I i < o then x i else false) = x i

Tactic:
split_ifs with hi h

Goal state after:
case pos
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
i : I
hi : ord I i = o
⊢ true = x i

case pos
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
i : I
hi : ¬ord I i = o
h : ord I i < o
⊢ x i = x i

case neg
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
i : I
hi : ¬ord I i = o
h : ¬ord I i < o
⊢ false = x i
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
n : ℕ
i : cell C n
⊢ ∃ I, cellFrontier n i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, openCell m j

Tactic:
induction n using Nat.case_strong_induction_on with

Goal state after:
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
⊢ isGood (π C fun x ↦ ord I x < o) l ↔ ∃ o' < o, isGood (π C fun x ↦ ord I x < o') l

Tactic:
by
  refine ⟨fun h ↦ ?_, fun ⟨o', ⟨ho', hl⟩⟩ ↦ isGood_mono C (le_of_lt ho') hl⟩
  use Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a))
  have hslt : Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) < o := by
    simp only [Finset.sup_lt_iff ho.bot_lt, List.mem_toFinset]
    exact fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)
  refine ⟨hslt, fun he ↦ h ?_⟩
  have hlt : ∀ i ∈ l.val, ord I i < Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) := by
    intro i hi
    simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]
    exact ⟨i, hi, le_rfl⟩
  rwa [eval_πs_image' C (le_of_lt hslt) hlt, ← eval_πs' C (le_of_lt hslt) hlt,
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)]

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

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
⊢ ∀ (n : ℕ), 0 < n → ∀ (j : cell C n), Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

Tactic:
intro n

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : D ∪ ⋃ n, ⋃ j, openCell n ↑j = E
hEC : E ⊆ C
n : ℕ
⊢ 0 < n → ∀ (j : cell C n), Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n 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 m : ℕ∞
h : m ≤ n
⊢ D ∪ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
apply union_subset_union_right

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
⊢ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ 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 : ℕ
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 ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j

Tactic:
apply union_subset_union_right

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
⊢ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j ⊆ ⋃ m, ⋃ (_ : ↑m < ↑n), ⋃ j, closedCell m j
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
⊢ ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard

Tactic:
intro n

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
⊢ ∀ (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ ∀ (i : ConnectedComponents Y), IsClopen (f ⁻¹' mk ⁻¹' {i})

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ Pairwise (Disjoint on fun y ↦ f ⁻¹' mk ⁻¹' {y})

pp: case refine_3
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ ⋃ i, f ⁻¹' mk ⁻¹' {i} = Set.univ

Tactic:
· exact fun y ↦ (isClopen_discrete {y}).preimage (continuous_coe.comp hfc)

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ Pairwise (Disjoint on fun y ↦ f ⁻¹' mk ⁻¹' {y})

case refine_3
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h✝ : ∀ (y : Y), (f ⁻¹' {y}).Finite
h : ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
⊢ ⋃ i, f ⁻¹' mk ⁻¹' {i} = Set.univ
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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
⊢ m q • Products.eval (C' C ho) q = (Linear_CC' C hsC ho) (m q • (List.map (e C) (term I ho :: ↑q)).prod)

Tactic:
map_smul

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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
q : Products I
hq : q ∈ m.support
⊢ m q • Products.eval (C' C ho) q = m q • (Linear_CC' C hsC ho) (List.map (e C) (term I ho :: ↑q)).prod
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case h₁
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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ (πs C o) (w q • eval (π C fun x ↦ ord I x < o) q) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
map_smul

Goal state after:
case h₁
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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
q : { l // Products.isGood (π C fun x ↦ ord I x < o) l }
a✝ : w q ≠ 0
⊢ w q • (πs C o) (eval (π C fun x ↦ ord I x < o) q) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
⊢ False

Tactic:
have hdir : Directed (· ≥ ·) fun i => 𝓟 (A \ U i) :=
    fun i j => (hdU i j).imp fun _ ⟨hi, hj⟩ => ⟨principal_mono.mpr <| sdiff_subset_sdiff_right hi,
      principal_mono.mpr <| sdiff_subset_sdiff_right hj⟩

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun x1 x2 ↦ x1 ≥ x2) fun i ↦ 𝓟 (A \ U i)
⊢ False
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case empty
ι : Type u_1
E : Type u_2
inst✝ : TopologicalSpace E
f : ι → Set E
hf : ∀ i ∈ ∅, IsCountablyCompact (f i)
⊢ IsCountablyCompact (⋃ i ∈ ∅, f i)

Tactic:
simpa using isCountablyCompact_empty

Goal state after:
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
j : ι
⊢ ∀ (f : C(X j, X i₁ × X i₂)),
    Continuous[inst✝⁴ j, inst✝¹]
      ((fun x ↦
          match x with
          | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
        ⇑f)

Tactic:
p

Goal state after:
case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
j : ι
p : C(X j, X i₁ × X i₂)
⊢ Continuous[inst✝⁴ j, inst✝¹]
    ((fun x ↦
        match x with
        | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
      ⇑p)
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
⊢ t ≤ ⨅ u, induced (fun x ↦ x ∈ u) sierpinskiSpace

Tactic:
rw [le_iInf_iff]
    exact fun u => Continuous.le_induced (isOpen_iff_continuous_mem.mp u.2)

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: a b : ℝ≥0∞
⊢ edist a b = ∞ ↔ a ≠ b ∧ (a = ∞ ∨ b = ∞)

Tactic:
by
  cases a <;> cases b <;> simp only [ne_eq, not_true_eq_false, or_self, and_true, iff_false,
    top_ne_coe, not_false_eq_true, coe_ne_top, or_false, and_self, or_true, and_self, iff_true,
    coe_inj, and_false, iff_false]
  · exact zero_ne_top
  · rfl
  · rfl
  · exact edist_ne_top _ _

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
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
y : M → ↑I
x✝ : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ y (e.symm (e m)) = 0 ∨ y (e.symm (e m)) = 1

Tactic:
by simpa using hm

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ ⋂ n, preCantorSet n = ⋂ i, preCantorSet (i + 1)

Tactic:
exact (preCantorSet_antitone.iInter_nat_add _).symm

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: case pos
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
j : ι
h : j ∈ S
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ a.2 ⟨j, h⟩

pp: case neg
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
j : ι
h : j ∉ S
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ ↑a.1 ⟨j, h⟩

Tactic:
· fun_prop

Goal state after:
case neg
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
j : ι
h : j ∉ S
⊢ Continuous[instTopologicalSpaceProd, inst✝ j] fun a ↦ ↑a.1 ⟨j, h⟩
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1.a
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)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N

pp: case refine_1.hx
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)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N

Tactic:
all_goals apply Cube.insertAt_boundary; right; exact ⟨i, iH⟩

Goal state after: