awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
    (D ∪
      ⋃ (m : ℕ),
        ⋃ (_ : m < n),
          ⋃ (j : cell m),
            ⋃ (_ :
              Membership.mem (γ := Finset (cell m))
                ((fun (m : ℕ) ↦ (Finite.toFinset (s := univ) ⋯ : Finset (cell m))) m) j),
              (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
have h : MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
  (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
Tactic: simp only [Finite.mem_toFinset, mem_univ, iUnion_true]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
⊢ IsClosed[inst_2] A
have rw : IsClosed[inst_2] (A ∩ C)
Tactic: rw [← inter_eq_left.2 asubc]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (hypothesis)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u + 1} (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
⊢ IsClosed[inst_2] (A ∩ C)
have eventually_isEmpty_cell₁ : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u + 1} (cell b)
Tactic: simp_rw [Filter.eventually_atTop, ge_iff_le] at eventually_isEmpty_cell
Cleared hypotheses: eventually_isEmpty_cell
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
eventually_isEmpty_cell : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u + 1} (cell b)
⊢ IsClosed[inst_2] (A ∩ C)
have obtain : ∀ (N : ℕ) (hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)), IsClosed[inst_2] (A ∩ C)
Tactic: obtain ⟨N, hN⟩ := eventually_isEmpty_cell
Cleared hypotheses: eventually_isEmpty_cell
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
⊢ IsClosed[inst_2] (A ∩ C)
have h₁ : C =
  D ∪ ⋃ (n : { n : ℕ // n < N }), ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1
Tactic: convert! this using 2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
⊢ C =
    D ∪
      ⋃ (n : { n : ℕ // n < N }), ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1
have h₁ : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 =
  D ∪
    ⋃ (x : ℕ),
      ⋃ (hx : x < N),
        ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) x hx) : ℕ)),
          (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) x hx) : ℕ) j) : (Fin (↑⟨x, hx⟩ : ℕ) → ℝ) → X) ''
            closedBall 0 1
Tactic: rw [← union', iUnion_subtype]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
⊢ D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 =
    D ∪
      ⋃ (x : ℕ),
        ⋃ (hx : x < N),
          ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) x hx) : ℕ)),
            (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) x hx) : ℕ) j) : (Fin (↑⟨x, hx⟩ : ℕ) → ℝ) → X) ''
              closedBall 0 1
have h₁ : ∀ (n : ℕ),
  Eq.{u + 1} (α := Set X) (⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)
    (⋃ (hx : n < N),
      ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
        (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1)
Tactic: congrm D ∪ ⋃ n, ?_
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
n : ℕ
⊢ Eq.{u + 1} (α := Set X) (⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)
    (⋃ (hx : n < N),
      ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
        (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1)
have h₁ : Subset.{u} (α := Set X) (⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)
  (⋃ (hx : n < N),
    ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
      (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1)
Tactic: refine subset_antisymm ?_ (iUnion_subset (fun i ↦ by rfl))
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
n : ℕ
⊢ Subset.{u} (α := Set X) (⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)
    (⋃ (hx : n < N),
      ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
        (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1)
have h₁ : ∀ (i : cell n),
  (↑(map n i) : (Fin n → ℝ) → X) '' closedBall 0 1 ⊆
    ⋃ (hx : n < N),
      ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
        (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1
Tactic: apply iUnion_subset
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (hypothesis)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
this :
  IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
n : ℕ
i : cell n
⊢ (↑(map n i) : (Fin n → ℝ) → X) '' closedBall 0 1 ⊆
    ⋃ (hx : n < N),
      ⋃ (j : cell (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ)),
        (↑(map (↑(Subtype.mk (p := fun (x : ℕ) ↦ x < N) n hx) : ℕ) j) : (Fin (↑⟨n, hx⟩ : ℕ) → ℝ) → X) '' closedBall 0 1
have this₁ : n < N
Tactic: have : n < N := Decidable.byContradiction fun h ↦ (hN n (Nat.ge_of_not_lt h)).false i
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
⊢ IsClosed[inst_2] (A ∩ C)
have suffices : IsClosed[inst_2]
  (A ∩
    (D ∪
      ⋃ (n : { n : ℕ // n < N }),
        ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
Tactic: suffices IsClosed (A ∩ (D ∪ ⋃ (n : {n : ℕ // n < N}), ⋃ j, ↑(map n j) '' closedBall 0 1)) by
      convert! this using 2
      rw [← union', iUnion_subtype]
      congrm D ∪ ⋃ n, ?_
      refine subset_antisymm ?_ (iUnion_subset (fun i ↦ by rfl))
      apply iUnion_subset
      intro i
      have : n < N := Decidable.byContradiction fun h ↦ (hN n (Nat.ge_of_not_lt h)).false i
      exact subset_iUnion₂ (s := fun _ i ↦ (map n i) '' closedBall 0 1) this i
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X_1 : Type u_1
inst : TopologicalSpace X_1
C_1 D_1 : Set X_1
inst_1 : RelCWComplex C_1 D_1
X : Type u
inst_2 : TopologicalSpace X
C D : Set X
cell : (n : ℕ) → Type u
map : (n : ℕ) → (i : cell n) → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite.{u + 1} (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i) : (Fin n → ℝ) → X) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm : X → Fin n → ℝ) (map n i).target
pairwiseDisjoint' :
  PairwiseDisjoint (α := Set X) univ fun (ni : (n : ℕ) × cell n) ↦
    (↑(map (ni.fst (β := fun (n : ℕ) ↦ cell n)) (ni.snd (β := fun (n : ℕ) ↦ cell n))) : (Fin ni.fst → ℝ) → X) ''
      ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint ((↑(map n i) : (Fin n → ℝ) → X) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n),
    MapsTo (↑(map n i) : (Fin n → ℝ) → X) (sphere 0 1)
      (D ∪ ⋃ (m : ℕ), ⋃ (_ : m < n), ⋃ (j : cell m), (↑(map m j) : (Fin m → ℝ) → X) '' closedBall 0 1)
isClosedBase : IsClosed[inst_2] D
union' : D ∪ ⋃ (n : ℕ), ⋃ (j : cell n), (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h :
  (∀ (n : ℕ) (j : cell n), IsClosed[inst_2] (A ∩ (↑(map n j) : (Fin n → ℝ) → X) '' closedBall 0 1)) ∧
    IsClosed[inst_2] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty.{u + 1} (cell b)
⊢ IsClosed[inst_2]
    (A ∩
      (D ∪
        ⋃ (n : { n : ℕ // n < N }),
          ⋃ (j : cell (↑n : ℕ)), (↑(map (↑n : ℕ) j) : (Fin (↑n : ℕ) → ℝ) → X) '' closedBall 0 1))
have simp_rw : IsClosed[inst_2]
  (A ∩ D ∪
    ⋃ (i : { n : ℕ // n < N }),
      ⋃ (i_1 : cell (↑i : ℕ)), A ∩ (↑(map (↑i : ℕ) i_1) : (Fin (↑i : ℕ) → ℝ) → X) '' closedBall 0 1)
Tactic: simp_rw [inter_union_distrib_left, inter_iUnion]