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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ x✝ : Products I
⊢ x✝¹ < x✝ ↔ List.Lex (fun x1 x2 ↦ x1 < x2) ↑x✝¹ ↑x✝

Tactic:
;

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ x✝ : Products I
⊢ x✝¹ < x✝ ↔ List.Lex (fun x1 x2 ↦ x1 < x2) ↑x✝¹ ↑x✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨a, ha⟩ < ⟨b, hb⟩
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})

Tactic:
;

Goal state after:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨a, ha⟩ < ⟨b, hb⟩
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨a, ha⟩ < ⟨b, hb⟩
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})

Tactic:
;

Goal state after:
case inl
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨a, ha⟩ < ⟨b, hb⟩
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < b})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨b, hb⟩ < ⟨a, ha⟩
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})

Tactic:
;

Goal state after:
case inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨b, hb⟩ < ⟨a, ha⟩
⊢ Products.eval C a ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨b, hb⟩ < ⟨a, ha⟩
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})

Tactic:
;

Goal state after:
case inr
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
a : Products I
ha : Products.isGood C a
b : Products I
hb : Products.isGood C b
h : Products.eval C a = Products.eval C b
hne : ⟨a, ha⟩ ≠ ⟨b, hb⟩
h' : ⟨b, hb⟩ < ⟨a, ha⟩
⊢ Products.eval C b ∈ Submodule.span ℤ (Products.eval C '' {m | m < a})
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 K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
x✝ : ↑(π (π C K) J)
⊢ (⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯)) x✝ = (eval (π (π C K) J) l) x✝

Tactic:
;

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝² : LinearOrder I
l : Products I
J K : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝¹ : (j : I) → Decidable (J j)
inst✝ : (j : I) → Decidable (K j)
hJK : ∀ (i : I), J i → K i
x✝ : ↑(π (π C K) J)
⊢ (⇑(eval (π C J) l) ∘ ⇑(Homeomorph.setCongr ⋯)) x✝ = (eval (π (π C K) J) l) x✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
⊢ ∀ (a : Products I), a < l ∧ eval C a = f ↔ a < l ∧ (πs C o) (eval (π C fun x ↦ ord I x < o) a) = f

Tactic:
;

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
⊢ ∀ (a : Products I), a < l ∧ eval C a = f ↔ a < l ∧ (πs C o) (eval (π C fun x ↦ ord I x < o) a) = f
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
m : Products I
⊢ m < l → (eval C m = f ↔ (πs C o) (eval (π C fun x ↦ ord I x < o) m) = f)

Tactic:
;

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
f : LocallyConstant ↑C ℤ
m : Products I
⊢ m < l → (eval C m = f ↔ (πs C o) (eval (π C fun x ↦ ord I x < o) m) = f)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
⊢ ∀ (a : Products I),
    a < l ∧ eval (π C fun x ↦ ord I x < o₂) a = f ↔ a < l ∧ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) a) = f

Tactic:
;

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
⊢ ∀ (a : Products I),
    a < l ∧ eval (π C fun x ↦ ord I x < o₂) a = f ↔ a < l ∧ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) a) = f
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
m : Products I
⊢ m < l → (eval (π C fun x ↦ ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) m) = f)

Tactic:
;

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o₁ o₂ : Ordinal.{u}
h : o₁ ≤ o₂
hl : ∀ i ∈ ↑l, ord I i < o₁
f : LocallyConstant ↑(π C fun x ↦ ord I x < o₂) ℤ
m : Products I
⊢ m < l → (eval (π C fun x ↦ ord I x < o₂) m = f ↔ (πs' C h) (eval (π C fun x ↦ ord I x < o₁) m) = f)
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}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant ↑C ℤ
hp : ∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1, ∃ (h_1 : Products.isGood (π C fun x ↦ ord I x < a) a_1), eval (π C fun x ↦ ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = p

Tactic:
obtain ⟨l, hl, rfl⟩ := hp

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
l : Products I
hl : Products.isGood C l
⊢ ∃ a,
    ∃ (h : a < o),
      ∃ x,
        (∃ a_1, ∃ (h_1 : Products.isGood (π C fun x ↦ ord I x < a) a_1), eval (π C fun x ↦ ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
          (πs C a) x = eval C ⟨l, hl⟩
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
x✝ : ↑(ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ))
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho))) x✝ = (ModuleCat.Hom.hom 0) x✝

Tactic:
;

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
x✝ : ↑(ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ))
⊢ (ModuleCat.Hom.hom (ModuleCat.ofHom (πs C o) ≫ ModuleCat.ofHom (Linear_CC' C hsC ho))) x✝ = (ModuleCat.Hom.hom 0) x✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
x : I
⊢ c x = false

Tactic:
;

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
x✝¹ : 0 ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
x✝ : IsClosed C
hsC : contained C 0
c : I → Bool
hc : c ∈ C
x : I
⊢ c x = false
Module: Mathlib.Topology.Category.Profinite.Projective

Goal state before:
pp: case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
⊢ (⇑(TopCat.Hom.hom g.hom) ∘ h) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure

Tactic:
have : g.hom ∘ g' = id := hg'.comp_eq_id

Goal state after:
case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ (⇑(TopCat.Hom.hom g.hom) ∘ h) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D : Set X
inst✝¹ : T2Space X
C : Set X
inst✝ : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ⋃ n, ⋃ j, openCell n ↑j = E

Tactic:
;

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D : Set X
inst✝¹ : T2Space X
C : Set X
inst✝ : CWComplex C
E : Set X
I : (n : ℕ) → Set (cell C n)
closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), closedCell n ↑i ⊆ E
union : ⋃ n, ⋃ j, openCell n ↑j = E
⊢ ⋃ n, ⋃ j, openCell n ↑j = E
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
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) ↑l

Tactic:
;

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
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) ↑l
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑f✝.hom' ∘ ↑{ hom' := ⟨id, ⋯⟩ }.hom', ⋯⟩ } = f✝

Tactic:
;

Goal state after:
X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑f✝.hom' ∘ ↑{ hom' := ⟨id, ⋯⟩ }.hom', ⋯⟩ } = f✝
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑f✝.hom' ∘ ↑{ hom' := ⟨id, ⋯⟩ }.hom', ⋯⟩ }.hom' = f✝.hom'

Tactic:
;

Goal state after:
X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑f✝.hom' ∘ ↑{ hom' := ⟨id, ⋯⟩ }.hom', ⋯⟩ }.hom' = f✝.hom'
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑{ hom' := ⟨id, ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ } = f✝

Tactic:
;

Goal state after:
X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑{ hom' := ⟨id, ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ } = f✝
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑{ hom' := ⟨id, ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom' = f✝.hom'

Tactic:
;

Goal state after:
X✝ Y✝ : UniformSpaceCat
f✝ : X✝.Hom Y✝
⊢ { hom' := ⟨↑{ hom' := ⟨id, ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom' = f✝.hom'
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: W✝ X✝ Y✝ Z✝ : UniformSpaceCat
f✝ : W✝.Hom X✝
g✝ : X✝.Hom Y✝
h✝ : Y✝.Hom Z✝
⊢ { hom' := ⟨↑h✝.hom' ∘ ↑{ hom' := ⟨↑g✝.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom', ⋯⟩ } =
    { hom' := ⟨↑{ hom' := ⟨↑h✝.hom' ∘ ↑g✝.hom', ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }

Tactic:
;

Goal state after:
W✝ X✝ Y✝ Z✝ : UniformSpaceCat
f✝ : W✝.Hom X✝
g✝ : X✝.Hom Y✝
h✝ : Y✝.Hom Z✝
⊢ { hom' := ⟨↑h✝.hom' ∘ ↑{ hom' := ⟨↑g✝.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom', ⋯⟩ } =
    { hom' := ⟨↑{ hom' := ⟨↑h✝.hom' ∘ ↑g✝.hom', ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: W✝ X✝ Y✝ Z✝ : UniformSpaceCat
f✝ : W✝.Hom X✝
g✝ : X✝.Hom Y✝
h✝ : Y✝.Hom Z✝
⊢ { hom' := ⟨↑h✝.hom' ∘ ↑{ hom' := ⟨↑g✝.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom', ⋯⟩ }.hom' =
    { hom' := ⟨↑{ hom' := ⟨↑h✝.hom' ∘ ↑g✝.hom', ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom'

Tactic:
;

Goal state after:
W✝ X✝ Y✝ Z✝ : UniformSpaceCat
f✝ : W✝.Hom X✝
g✝ : X✝.Hom Y✝
h✝ : Y✝.Hom Z✝
⊢ { hom' := ⟨↑h✝.hom' ∘ ↑{ hom' := ⟨↑g✝.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom', ⋯⟩ }.hom' =
    { hom' := ⟨↑{ hom' := ⟨↑h✝.hom' ∘ ↑g✝.hom', ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom'
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: W✝ X✝ Y✝ Z✝ : UniformSpaceCat
f✝ : W✝.Hom X✝
g✝ : X✝.Hom Y✝
h✝ : Y✝.Hom Z✝
x✝ : W✝.carrier
⊢ ↑{ hom' := ⟨↑h✝.hom' ∘ ↑{ hom' := ⟨↑g✝.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom', ⋯⟩ }.hom' x✝ =
    ↑{ hom' := ⟨↑{ hom' := ⟨↑h✝.hom' ∘ ↑g✝.hom', ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom' x✝

Tactic:
;

Goal state after:
W✝ X✝ Y✝ Z✝ : UniformSpaceCat
f✝ : W✝.Hom X✝
g✝ : X✝.Hom Y✝
h✝ : Y✝.Hom Z✝
x✝ : W✝.carrier
⊢ ↑{ hom' := ⟨↑h✝.hom' ∘ ↑{ hom' := ⟨↑g✝.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom', ⋯⟩ }.hom' x✝ =
    ↑{ hom' := ⟨↑{ hom' := ⟨↑h✝.hom' ∘ ↑g✝.hom', ⋯⟩ }.hom' ∘ ↑f✝.hom', ⋯⟩ }.hom' 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:
;

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.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:
;

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
⊢ ∀ (a : I), (a ∈ ↑l.Tail → ↑x a = true) = (a ∈ ↑l.Tail → SwapTrue o (↑x) a = true)
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
i : I
⊢ (i ∈ ↑l.Tail → ↑x i = true) = (i ∈ ↑l.Tail → SwapTrue o (↑x) i = true)

Tactic:
;

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.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
i : I
⊢ i ∈ ↑l.Tail → (↑x i = true) = (SwapTrue o (↑x) i = true)

Tactic:
;

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) = (SwapTrue o (↑x) i = true)
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
i : I
hi : i ∈ ↑l.Tail
⊢ (↑x i = true) = (SwapTrue o (↑x) i = true)

Tactic:
;

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
hi : i ∈ ↑l.Tail
⊢ (↑x i = true) = (SwapTrue o (↑x) i = true)
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : 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
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
x✝ : α
⊢ x✝ ∈ ⋂ i, s i ↔ x✝ ∈ ⋂ i, s' i

Tactic:
;

Goal state after:
α : 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
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
x✝ : α
⊢ x✝ ∈ ⋂ i, s i ↔ x✝ ∈ ⋂ i, s' i
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : 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
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
x✝ : α
⊢ (∀ (i : ℕ), x✝ ∈ s i) ↔ ∀ (i : ℕ), x✝ ∈ s' i

Tactic:
;

Goal state after:
α : 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
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
x✝ : α
⊢ (∀ (i : ℕ), x✝ ∈ s i) ↔ ∀ (i : ℕ), x✝ ∈ s' i
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : 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
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
x✝ : α
⊢ x✝ ∈ dissipate s v ↔ x✝ ∈ dissipate s' v

Tactic:
;

Goal state after:
α : 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
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
x✝ : α
⊢ x✝ ∈ dissipate s v ↔ x✝ ∈ dissipate s' v
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : 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
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
x✝ : α
⊢ (∀ y ≤ v, x✝ ∈ s y) ↔ ∀ y ≤ v, x✝ ∈ s' y

Tactic:
;

Goal state after:
α : 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
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
j : ℕ
hj : dissipate s' j = ∅
v : ℕ
hv : n ≤ v
x✝ : α
⊢ (∀ y ≤ v, x✝ ∈ s y) ↔ ∀ y ≤ v, x✝ ∈ s' y
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
x : α
⊢ (∀ i ≤ n, x ∈ C i) → ∀ i < n, x ∈ C i

Tactic:
;

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
x : α
⊢ (∀ i ≤ n, x ∈ C i) → ∀ i < n, x ∈ C i