mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hi.inl
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)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h1 : IsClosed[t] (A ∩ openCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

pp: case hi.inr
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)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h2 : IsClosed[t] (A ∩ closedCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

Tactic:
·

Goal state after:
case hi.inl
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)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h1 : IsClosed[t] (A ∩ openCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case hg
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (ite (ord I i = o) true)

pp: case hf
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun x ↦ x i

Tactic:
·

Goal state after:
case hg
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous (ite (ord I i = o) true)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case hf
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun x ↦ x i

Tactic:
·

Goal state after:
case hf
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
i : I
⊢ Continuous fun x ↦ x i
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ord I i = o
⊢ true = g i

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ Proj (fun x ↦ ord I x < o) g i = g i

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ord I i = o
⊢ true = g i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ Proj (fun x ↦ ord I x < o) g i = g i

Tactic:
·

Goal state after:
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ Proj (fun x ↦ ord I x < o) g i = g i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case hi.inr
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)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h2 : IsClosed[t] (A ∩ closedCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

Tactic:
·

Goal state after:
case hi.inr
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)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h2 : IsClosed[t] (A ∩ closedCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg.h₂
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ (-1 • c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * b • Products.eval (π C fun x ↦ x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
·

Goal state after:
case neg.h₂
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ (-1 • c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * b • Products.eval (π C fun x ↦ x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case inl
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 ∈ C0 C ho
i : I
hi✝ : o ≤ ord I i
hi : o < ord I i
⊢ false = x i

pp: case inr
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 ∈ C0 C ho
i : I
hi✝ : o ≤ ord I i
hi : o = ord I i
⊢ false = x i

Tactic:
·

Goal state after:
case inl
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 ∈ C0 C ho
i : I
hi✝ : o ≤ ord I i
hi : o < ord I i
⊢ false = x i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case inl
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 : ℕ
hn : 0 < n
j : cell C n
h : Disjoint A (openCell n j)
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

pp: case inr
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 : ℕ
hn : 0 < n
j : cell C n
h : IsClosed[t] (A ∩ closedCell n j)
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
·

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

Goal state before:
pp: case inr
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 ∈ C0 C ho
i : I
hi✝ : o ≤ ord I i
hi : o = ord I i
⊢ false = x i

Tactic:
·

Goal state after:
case inr
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 ∈ C0 C ho
i : I
hi✝ : o ≤ ord I i
hi : o = ord I i
⊢ false = x i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case inr
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 : ℕ
hn : 0 < n
j : cell C n
h : IsClosed[t] (A ∩ closedCell n j)
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)

Tactic:
·

Goal state after:
case inr
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 : ℕ
hn : 0 < n
j : cell C n
h : IsClosed[t] (A ∩ closedCell n j)
⊢ IsClosed[t] (A ∩ openCell n j) ∨ IsClosed[t] (A ∩ closedCell n j)
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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ord I i = o
⊢ true = x i

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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ord I i < o
⊢ x i = x i

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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ¬ord I i < o
⊢ false = x i

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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ord I i = o
⊢ true = x i
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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ord I i < o
⊢ x i = x i

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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ¬ord I i < o
⊢ false = x i

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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ord I i < o
⊢ x i = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
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
x : I → Bool
hx : x ∈ C1 C ho
i : I
hi : ¬ord I i = o
h : ¬ord I i < o
⊢ false = x i

Tactic:
·

Goal state after:
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.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.isGood C l
⊢ L l

pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : ¬Products.isGood C l
⊢ L l

Tactic:
·

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : Products.isGood C l
⊢ L l
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : ¬Products.isGood C l
⊢ L l

Tactic:
·

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
h✝ : ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
l✝ : Products I
L : Products I → Prop := fun m ↦ Products.eval C m ∈ Submodule.span ℤ (Set.range (eval C))
l : Products I
h : ∀ y < l, L y
hl : ¬Products.isGood C l
⊢ L l
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x ↦ ord I x < o))
hab : (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a = (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) b
⊢ a = b

pp: case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
hb : b ∈ range (π C fun x ↦ ord I x < o) ∧ (πs C o) b = a
⊢ ∃ a_1, (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a_1 = ⟨a, ⋯⟩

Tactic:
·

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
a b : ↑(range (π C fun x ↦ ord I x < o))
hab : (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a = (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) b
⊢ a = b
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
hb : b ∈ range (π C fun x ↦ ord I x < o) ∧ (πs C o) b = a
⊢ ∃ a_1, (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a_1 = ⟨a, ⋯⟩

Tactic:
·

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x✝ : ↑(smaller C o)
a : LocallyConstant ↑C ℤ
b : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
hb : b ∈ range (π C fun x ↦ ord I x < o) ∧ (πs C o) b = a
⊢ ∃ a_1, (fun x ↦ ⟨(πs C o) ↑x, ⋯⟩) a_1 = ⟨a, ⋯⟩
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
hJ : x ∈ D
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1

pp: case h.inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
hJ : ∃ i < n.succ, ∃ i_1 ∈ J i, x ∈ closedCell i i_1
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1

Tactic:
·

Goal state after:
case h.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
hx : x ∈ cellFrontier (n + 1) i
hJ : x ∈ D
⊢ x ∈ D ∨ ∃ i < n + 1, ∃ i_1 ∈ I i, x ∈ openCell i i_1
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
⊢ (π C fun x ↦ ord I x < o) ⊆ C0 C ho ∪ π (C1 C ho) fun x ↦ ord I x < o

pp: case refine_2
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 ∈ C0 C ho ∩ π (C1 C ho) fun x ↦ ord I x < o),
    (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f) ⟨x, ⋯⟩ =
      (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⟨x, ⋯⟩

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
⊢ (πs C o)
      (LocallyConstant.piecewise' ?refine_1 ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
        (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ?refine_2) =
    f

Tactic:
·

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
⊢ (π C fun x ↦ ord I x < o) ⊆ C0 C ho ∪ π (C1 C ho) fun x ↦ ord I x < o
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x ↦ ord I x < o₂)

pp: case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (πs C o₂) ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)) = (πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)

Tactic:
·

Goal state after:
case h.refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩) ∈ range (π C fun x ↦ ord I x < o₂)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
h : ord I i = o
⊢ term I ho = i

pp: case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
h : term I ho = i
⊢ ord I i = o

Tactic:
·

Goal state after:
case refine_1
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
h : ord I i = o
⊢ term I ho = i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
h : term I ho = i
⊢ ord I i = o

Tactic:
·

Goal state after:
case refine_2
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
i : I
h : term I ho = i
⊢ ord I i = o
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (πs C o₂) ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)) = (πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)

Tactic:
·

Goal state after:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
l : Products I
gl : Products.isGood (π C fun x ↦ ord I x < o₁) l
⊢ (πs C o₂) ((πs' C h) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)) = (πs C o₁) (eval (π C fun x ↦ ord I x < o₁) ⟨l, gl⟩)