mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
⊢ Function.Injective (ι S)

Tactic:
·

Goal state after:
case hf
S : Profinite
⊢ Function.Injective (ι S)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case pos
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 : ℕ
x✝ : 0 < n
j : cell C n
h : j ∈ I n
⊢ Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

pp: case neg
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 : ℕ
x✝ : 0 < n
j : cell C n
h : j ∉ I n
⊢ Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

Tactic:
·

Goal state after:
case pos
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 : ℕ
x✝ : 0 < n
j : cell C n
h : j ∈ I n
⊢ Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case refine_2
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 : Products I
h : Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
⊢ Products.isGood C l

Tactic:
·

Goal state after:
case refine_2
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 : Products I
h : Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
⊢ Products.isGood C l
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case neg
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 : ℕ
x✝ : 0 < n
j : cell C n
h : j ∉ I n
⊢ Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)

Tactic:
·

Goal state after:
case neg
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 : ℕ
x✝ : 0 < n
j : cell C n
h : j ∉ I n
⊢ Disjoint E (openCell n j) ∨ IsClosed[t] (E ∩ closedCell n j)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case top
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m : ℕ
⊢ ↑m < ⊤ + 1 ↔ ↑m ≤ ⊤

pp: case coe
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m a✝ : ℕ
⊢ ↑m < ↑a✝ + 1 ↔ ↑m ≤ ↑a✝

Tactic:
·

Goal state after:
case top
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m : ℕ
⊢ ↑m < ⊤ + 1 ↔ ↑m ≤ ⊤
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case coe
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m a✝ : ℕ
⊢ ↑m < ↑a✝ + 1 ↔ ↑m ≤ ↑a✝

Tactic:
·

Goal state after:
case coe
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m a✝ : ℕ
⊢ ↑m < ↑a✝ + 1 ↔ ↑m ≤ ↑a✝
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
h : (interior D ∩ closedCell n j).Nonempty
⊢ False

Tactic:
← closure_openCell_eq_closedCell,

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
h : (interior D ∩ closure[t] (openCell n j)).Nonempty
⊢ False
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case pos
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∃ n, s n = ∅
⊢ ∃ n, dissipate s n = ∅

pp: case neg
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∀ (n : ℕ), (s n).Nonempty
⊢ ∃ n, dissipate s n = ∅

Tactic:
·

Goal state after:
case pos
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∃ n, s n = ∅
⊢ ∃ n, dissipate s n = ∅
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case neg
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∀ (n : ℕ), (s n).Nonempty
⊢ ∃ n, dissipate s n = ∅

Tactic:
·

Goal state after:
case neg
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert ∅ S
hd : ⋂ i, s i = ∅
g : ∀ (n : ℕ), (s n).Nonempty
⊢ ∃ n, dissipate s n = ∅
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
⊢ IsCompactSystem (insert Set.univ S)

Tactic:
rcases isEmpty_or_nonempty α with hα | _

Goal state after:
case inl
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
hα : IsEmpty α
⊢ IsCompactSystem (insert Set.univ S)

case inr
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
h✝ : Nonempty α
⊢ IsCompactSystem (insert Set.univ S)
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case inl
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
hα : IsEmpty α
⊢ IsCompactSystem (insert Set.univ S)

pp: case inr
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
h✝ : Nonempty α
⊢ IsCompactSystem (insert Set.univ S)

Tactic:
·

Goal state after:
case inl
α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
hα : IsEmpty α
⊢ IsCompactSystem (insert Set.univ S)
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case pos
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∀ (n : ℕ), s n ∉ S
⊢ (⋂ i, s i).Nonempty

pp: case neg
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
⊢ (⋂ i, s i).Nonempty

Tactic:
·

Goal state after:
case pos
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∀ (n : ℕ), s n ∉ S
⊢ (⋂ i, s i).Nonempty
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case zero.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
j :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨0, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨0, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨0, j⟩.fst, ⟨0, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

pp: case succ.zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨0, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨0, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨0, i⟩.fst, ⟨0, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

pp: case succ.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

Tactic:
·

Goal state after:
case zero.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
j :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨0, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨0, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨0, j⟩.fst, ⟨0, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case succ.zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨0, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨0, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨0, i⟩.fst, ⟨0, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

pp: case succ.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

Tactic:
·

Goal state after:
case succ.zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨0, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨0, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨0, i⟩.fst, ⟨0, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case succ.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

Tactic:
·

Goal state after:
case succ.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
x : X
⊢ x ∈ D →
    x ∈
      ⋃ i,
        ⋃ j,
          ↑(match i, j with
              | 0, i => PartialEquiv.single ![] ↑i
              | n.succ, i => PEmpty.elim i) ''
            closedBall 0 1

Tactic:
xD

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
x : X
xD : x ∈ D
⊢ x ∈
    ⋃ i,
      ⋃ j,
        ↑(match i, j with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => PEmpty.elim i) ''
          closedBall 0 1
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case refine_1
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : IsCompactSystem (insert ∅ S)
C : ℕ → Set α
hdi : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
hi : ∀ (i : ℕ), C i ∈ S
⊢ ⋂ i, C i = ∅ → ∃ n, C n = ∅

pp: case refine_2
α : 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 : ⋂ i, C i = ∅
⊢ ∃ n, dissipate C n = ∅

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : IsCompactSystem (insert ∅ S)
C : ℕ → Set α
hdi : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
hi : ∀ (i : ℕ), C i ∈ S
⊢ ⋂ i, C i = ∅ → ∃ n, C n = ∅
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: 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
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
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 1

pp: 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
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
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ¬∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 0

pp: 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
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
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ¬∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ 0 = 1

Tactic:
·

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
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
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 1
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 = ∅

pp: case neg
α : 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:
·

Goal state after:
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 = ∅
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
⊢ 0 < Fintype.card ι

Tactic:
by lia

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

Goal state before:
pp: case neg
α : 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:
·

Goal state after:
case neg
α : 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 = ∅
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: 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
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
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ 1 - 0 = 1

pp: case pos.hnc
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
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ ¬↑x (term I ho) = true

Tactic:
·

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
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
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
⊢ 1 - 0 = 1
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case inl
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
h :
  ∀ {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
hy : Finite (ConnectedComponents X)
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

pp: case inr
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
h :
  ∀ {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
hy : Infinite (ConnectedComponents X)
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
·

Goal state after:
case inl
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
h :
  ∀ {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
hy : Finite (ConnectedComponents X)
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard