awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u_2 + 1} (@cell _ inst C D _ n)
have simp : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
Tactic: simp only [Filter.eventually_atTop, ge_iff_le]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
have inl : IsEmpty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n) →
  ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
Tactic: cases isEmpty_or_nonempty (Σ n, cell C n)
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
inl :
  IsEmpty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n) →
    ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
have inr : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n) →
  ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
Tactic: cases isEmpty_or_nonempty (Σ n, cell C n)
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
have inr : ∀ (x : Fintype ((n : ℕ) × @cell _ inst C D _ n)), ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
Tactic: have _ := Fintype.ofFinite (Σ n, cell C n)
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
have h : ∀ (b : ℕ), A.max' sorry + 1 ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
Tactic: use A.max' (Finset.image_nonempty.2 Finset.univ_nonempty) + 1
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
m : ℕ
h_1 : A.max' ⋯ + 1 ≤ m
⊢ IsEmpty.{u_2 + 1} (@cell _ inst C D _ m)
have h : ∀ (h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)), False
Tactic: by_contra! h'
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
m : ℕ
h_1 : A.max' ⋯ + 1 ≤ m
h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)
⊢ m ∈ A
have simp : ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
Tactic: simp only [Finset.mem_image, Finset.mem_univ, true_and, A]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
m : ℕ
h_1 : A.max' ⋯ + 1 ≤ m
h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)
⊢ ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
have h'₁ : ∃ (x : @cell _ inst C D _ m), True
Tactic: simp only [← exists_true_iff_nonempty] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
m : ℕ
h_1 : A.max' ⋯ + 1 ≤ m
h' : ∃ (x : @cell _ inst C D _ m), True
⊢ ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
have obtain : ∀ (j : @cell _ inst C D _ m),
  True → ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
Tactic: obtain ⟨j, _⟩ := h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
m : ℕ
h_1 : A.max' ⋯ + 1 ≤ m
j : @cell _ inst C D _ m
h_2 : True
⊢ ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
have w : (n : ℕ) × @cell _ inst C D _ n
Tactic: use ⟨m, j⟩
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
m : ℕ
h_1 : A.max' ⋯ + 1 ≤ m
j : @cell _ inst C D _ m
h_2 : True
w : (n : ℕ) × @cell _ inst C D _ n
⊢ ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
have h : (Sigma.mk (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) m j).fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
Tactic: use ⟨m, j⟩
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
m : ℕ
h_1 : A.max' ⋯ + 1 ≤ m
h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)
⊢ False
have hmA : m ∈ A
Tactic: have hmA : m ∈ A := by
      simp only [Finset.mem_image, Finset.mem_univ, true_and, A]
      simp only [← exists_true_iff_nonempty] at h'
      obtain ⟨j, _⟩ := h'
      use ⟨m, j⟩
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
m : ℕ
h_1 : A.max' ⋯ + 1 ≤ m
h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)
hmA : m ∈ A
⊢ False
have linarith : -1 + (HAdd.hAdd (α := ℤ) (↑(A.max' sorry) : ℤ) 1 - (↑m : ℤ)) + HSub.hSub (α := ℤ) (↑m : ℤ) (↑(A.max' sorry) : ℤ) = 0
Tactic: linarith [A.le_max' m hmA]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
inr inr₁ inr₂ : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
have h : let A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ;
∀ (b : ℕ), A.max' sorry + 1 ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
Tactic: classical
    let A := (Finset.univ : Finset (Σ n, cell C n)).image Sigma.fst
    use A.max' (Finset.image_nonempty.2 Finset.univ_nonempty) + 1
    intro m _
    by_contra! h'
    have hmA : m ∈ A := by
      simp only [Finset.mem_image, Finset.mem_univ, true_and, A]
      simp only [← exists_true_iff_nonempty] at h'
      obtain ⟨j, _⟩ := h'
      use ⟨m, j⟩
    linarith [A.le_max' m hmA]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h_1 : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
inr inr₁ inr₂ : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
h h₁ :
  let A : Finset ℕ :=
    Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
      Finset.univ;
  ∀ (m : ℕ), A.max' ⋯ + 1 ≤ m → IsEmpty.{u_2 + 1} (@cell _ inst C D _ m)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
have h₂ : let A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ;
∀ (m : ℕ), A.max' sorry + 1 ≤ m → ∀ (h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)), False
Tactic: classical
    let A := (Finset.univ : Finset (Σ n, cell C n)).image Sigma.fst
    use A.max' (Finset.image_nonempty.2 Finset.univ_nonempty) + 1
    intro m _
    by_contra! h'
    have hmA : m ∈ A := by
      simp only [Finset.mem_image, Finset.mem_univ, true_and, A]
      simp only [← exists_true_iff_nonempty] at h'
      obtain ⟨j, _⟩ := h'
      use ⟨m, j⟩
    linarith [A.le_max' m hmA]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
h_1 : Nonempty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
x : Fintype ((n : ℕ) × @cell _ inst C D _ n)
inr inr₁ inr₂ : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
h h₁ :
  let A : Finset ℕ :=
    Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
      Finset.univ;
  ∀ (m : ℕ), A.max' ⋯ + 1 ≤ m → IsEmpty.{u_2 + 1} (@cell _ inst C D _ m)
h₂ :
  let A : Finset ℕ :=
    Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
      Finset.univ;
  ∀ (m : ℕ), A.max' ⋯ + 1 ≤ m → ∀ (h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)), False
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
have h₃ : let A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ;
∀ (m : ℕ), A.max' sorry + 1 ≤ m → ∀ (h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)) (hmA : m ∈ A), False
Tactic: classical
    let A := (Finset.univ : Finset (Σ n, cell C n)).image Sigma.fst
    use A.max' (Finset.image_nonempty.2 Finset.univ_nonempty) + 1
    intro m _
    by_contra! h'
    have hmA : m ∈ A := by
      simp only [Finset.mem_image, Finset.mem_univ, true_and, A]
      simp only [← exists_true_iff_nonempty] at h'
      obtain ⟨j, _⟩ := h'
      use ⟨m, j⟩
    linarith [A.le_max' m hmA]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : Finite C (D := D)
⊢ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
have h : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u_2 + 1} (@cell _ inst C D _ n)
Tactic: have h := finite.eventually_isEmpty_cell
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : Finite C (D := D)
h : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u_2 + 1} (@cell _ inst C D _ n)
⊢ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
have x : ∀ (n : ℕ), _root_.Finite.{u_2 + 1} (@cell _ inst C D _ n)
Tactic: have _ := finite.finite_cell
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : Finite C (D := D)
h : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u_2 + 1} (@cell _ inst C D _ n)
h_1 : ∀ (n : ℕ), _root_.Finite.{u_2 + 1} (@cell _ inst C D _ n)
⊢ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
have h₁ : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
Tactic: simp only [Filter.eventually_atTop, ge_iff_le] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : Finite C (D := D)
h_1 : ∀ (n : ℕ), _root_.Finite.{u_2 + 1} (@cell _ inst C D _ n)
h : ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
⊢ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
have rcases : ∀ (n : ℕ) (hn : ∀ (b : ℕ), n ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)),
  _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
Tactic: rcases h with ⟨n, hn⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : Finite C (D := D)
h : ∀ (n : ℕ), _root_.Finite.{u_2 + 1} (@cell _ inst C D _ n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
m : ℕ
j : @cell _ inst C D _ m
⊢ m < n
have by_contra : ∀ (h : ¬m < n), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (hypothesis)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : Finite C (D := D)
h : ∀ (n : ℕ), _root_.Finite.{u_2 + 1} (@cell _ inst C D _ n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
⊢ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
have this : ∀ (m : ℕ) (j : @cell _ inst C D _ m), m < n
Tactic: have (m) (j : cell C m) : m < n := by
    by_contra h
    exact (hn m (not_lt.1 h)).false j
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Finite (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : Finite C (D := D)
h : ∀ (n : ℕ), _root_.Finite.{u_2 + 1} (@cell _ inst C D _ n)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
this : ∀ (m : ℕ) (j : @cell _ inst C D _ m), m < n
f : (m : { m : ℕ // m < n }) × @cell _ inst C D _ (↑m : ℕ) ≃ (m : ℕ) × @cell _ inst C D _ m :=
  {
    toFun := fun (x : (m : { m : ℕ // m < n }) × @cell _ inst C D _ (↑m : ℕ)) ↦
      match (motive := (m : { m : ℕ // m < n }) × @cell _ inst C D _ (↑m : ℕ) → (m : ℕ) × @cell _ inst C D _ m) x with
      | ⟨m, j⟩ => Sigma.mk (β := fun (m : ℕ) ↦ @cell _ inst C D _ m) (↑m : ℕ) j,
    invFun := fun (x : (m : ℕ) × @cell _ inst C D _ m) ↦
      match (motive := (m : ℕ) × @cell _ inst C D _ m → (m : { m : ℕ // m < n }) × @cell _ inst C D _ (↑m : ℕ)) x with
      | ⟨m, j⟩ =>
        Sigma.mk (β := fun (m : { m : ℕ // m < n }) ↦ @cell _ inst C D _ (↑m : ℕ))
          (Subtype.mk (p := fun (m : ℕ) ↦ m < n) m ⋯) j,
    left_inv := ⋯, right_inv := ⋯ }
⊢ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
have rw : _root_.Finite.{u_2 + 1} ((m : { m : ℕ // m < n }) × @cell _ inst C D _ (↑m : ℕ))
Tactic: rw [← Equiv.finite_iff f]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y z w : @cell _ inst C ∅ _ 0
h1 : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
h2 : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 z ∪ closedCell (C := C) (D := ∅) 0 w
⊢ x = z ∨ x = w
have h1₁ : cellFrontier (C := C) (D := ∅) 1 e =
  {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
Tactic: simp_rw [closedCell_zero_eq_singleton] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y z w : @cell _ inst C ∅ _ 0
h1 : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
h2 : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 z ∪ closedCell (C := C) (D := ∅) 0 w
h1₁ :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
⊢ x = z ∨ x = w
have h2₁ : cellFrontier (C := C) (D := ∅) 1 e =
  {(↑(map (C := C) (D := ∅) 0 z) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 w) : (Fin 0 → ℝ) → X) ![]}
Tactic: simp_rw [closedCell_zero_eq_singleton] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y z w : @cell _ inst C ∅ _ 0
h1 :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
h2 :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 z) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 w) : (Fin 0 → ℝ) → X) ![]}
⊢ x = z ∨ x = w
have h2₁ : Eq (α := Set X)
  ({(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]})
  ({(↑(map (C := C) (D := ∅) 0 z) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 w) : (Fin 0 → ℝ) → X) ![]})
Tactic: rw [h1] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y z w : @cell _ inst C ∅ _ 0
h1 :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
h2 :
  Eq (α := Set X)
    ({(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]})
    ({(↑(map (C := C) (D := ∅) 0 z) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 w) : (Fin 0 → ℝ) → X) ![]})
⊢ x = z ∨ x = w
have h2₁ : y = w ∧ x = z ∨ y = z ∧ x = w
Tactic: simp only [(RelCWComplex.injective_map_zero C).eq_iff, union_singleton, pair_eq_pair_iff] at h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y z w : @cell _ inst C ∅ _ 0
h1 :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
h2 : y = w ∧ x = z ∨ y = z ∧ x = w
⊢ x = z ∨ x = w
have inl : y = w → x = z → x = z ∨ x = w
Tactic: tauto
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y z w : @cell _ inst C ∅ _ 0
h1 :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
h2 : y = w ∧ x = z ∨ y = z ∧ x = w
inl : y = w → x = z → x = z ∨ x = w
⊢ x = z ∨ x = w
have inr : y = z → x = w → x = z ∨ x = w
Tactic: tauto
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y z w : @cell _ inst C ∅ _ 0
h1 :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
h2 : y = w ∧ x = z ∨ y = z ∧ x = w
inl : y = w → x = z → x = z ∨ x = w
inr : y = z → x = w → x = z ∨ x = w
inl₁ : y = w → x = z → x = z ∨ x = w
inr₁ : y = z → x = w → x = z ∨ x = w
⊢ x = z ∨ x = w
have inl₂ : y = w → x = z → ¬x = z → x = w
Tactic: tauto
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y z w : @cell _ inst C ∅ _ 0
h1 :
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![]} ∪ {(↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
h2 : y = w ∧ x = z ∨ y = z ∧ x = w
inl : y = w → x = z → x = z ∨ x = w
inr : y = z → x = w → x = z ∨ x = w
inl₁ : y = w → x = z → x = z ∨ x = w
inr₁ : y = z → x = w → x = z ∨ x = w
inl₂ : y = w → x = z → ¬x = z → x = w
⊢ x = z ∨ x = w
have inr₂ : y = z → x = w → ¬x = z → x = w
Tactic: tauto
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
⊢ Membership.mem (γ := Set (@cell _ inst C ∅ _ 1)) univ e ↔
    ∃ (x : @cell _ inst C ∅ _ 0) (y : @cell _ inst C ∅ _ 0),
      cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
have simp : ∃ (x : @cell _ inst C ∅ _ 0) (y : @cell _ inst C ∅ _ 0),
  cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y
Tactic: simp only [mem_univ, true_iff]
-- Lean 4 proof step from Mathlib.Topology.CWComplex.Classical.Graph (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
x y : @cell _ inst C ∅ _ 0
⊢ IsLink (OneSkeletonGraph C) e x y ↔
    cellFrontier (C := C) (D := ∅) 1 e =
      {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
have rw : cellFrontier (C := C) (D := ∅) 1 e = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y ↔
  cellFrontier (C := C) (D := ∅) 1 e =
    {(↑(map (C := C) (D := ∅) 0 x) : (Fin 0 → ℝ) → X) ![], (↑(map (C := C) (D := ∅) 0 y) : (Fin 0 → ℝ) → X) ![]}
Tactic: rw [OneSkeletonGraph_isLink, closedCell_zero_eq_singleton, closedCell_zero_eq_singleton,
    singleton_union]