awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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 : IsEmpty.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)
⊢ ∀ (b : ℕ), 0 ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)

Tactic:
simp_all
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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 : 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:
exact ⟨0, by simp_all⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
inr :
  ∀ (x : Fintype ((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)

Tactic:
have _ := Fintype.ofFinite (Σ n, cell C n)
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
A : Finset ℕ :=
  Finset.image.{u_2, 0} (α := (n : ℕ) × @cell _ inst C D _ n) (Sigma.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n))
    Finset.univ
h : ∀ (b : ℕ), A.max' ⋯ + 1 ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)

Tactic:
use A.max' (Finset.image_nonempty.2 Finset.univ_nonempty) + 1

Premises used: Iff.mpr, Finset.image_nonempty, Finset.max', Finset.univ_nonempty
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
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 : A.max' ⋯ + 1 ≤ m → IsEmpty.{u_2 + 1} (@cell _ inst C D _ m)
⊢ A.max' ⋯ + 1 ≤ m → IsEmpty.{u_2 + 1} (@cell _ inst C D _ m)

Tactic:
_
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
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_2 : A.max' ⋯ + 1 ≤ m
h : ∀ (h' : Nonempty.{u_2 + 1} (@cell _ inst C D _ m)), False
⊢ IsEmpty.{u_2 + 1} (@cell _ inst C D _ m)

Tactic:
by_contra! h'
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
simp : ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
⊢ m ∈ A

Tactic:
simp only [Finset.mem_image, Finset.mem_univ, true_and, A]

Premises used: Finset.mem_univ, Finset.mem_image, true_and
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
⊢ ∃ (x : @cell _ inst C D _ m), True

Tactic:
simp only [← exists_true_iff_nonempty] at h'

Premises used: exists_true_iff_nonempty
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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
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
⊢ ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m

Tactic:
obtain ⟨j, _⟩ := h'
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
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_2 : A.max' ⋯ + 1 ≤ m
j : @cell _ inst C D _ m
h_3 : True
w : (n : ℕ) × @cell _ inst C D _ n
h : (Sigma.mk (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) m j).fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m
⊢ ∃ (a : (n : ℕ) × @cell _ inst C D _ n), a.fst (β := fun (n : ℕ) ↦ @cell _ inst C D _ n) = m

Tactic:
use ⟨m, j⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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

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⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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
linarith : -1 + (HAdd.hAdd (α := ℤ) (↑(A.max' ⋯) : ℤ) 1 - (↑m : ℤ)) + HSub.hSub (α := ℤ) (↑m : ℤ) (↑(A.max' ⋯) : ℤ) = 0
⊢ False

Tactic:
linarith [A.le_max' m hmA]

Premises used: Finset.le_max'
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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
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)) (hmA : m ∈ A), False
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ 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]
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
finite : Finite C (D := D)
⊢ ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty.{u_2 + 1} (@cell _ inst C D _ n)

Tactic:
have h := finite.eventually_isEmpty_cell
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
⊢ ∀ (n : ℕ), _root_.Finite.{u_2 + 1} (@cell _ inst C D _ n)

Tactic:
have _ := finite.finite_cell
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
⊢ ∃ (a : ℕ), ∀ (b : ℕ), a ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)

Tactic:
simp only [Filter.eventually_atTop, ge_iff_le] at h

Premises used: ge_iff_le, Filter.eventually_atTop
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
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)
⊢ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)

Tactic:
rcases h with ⟨n, hn⟩
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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
by_contra : ∀ (h : ¬m < n), False
⊢ m < n

Tactic:
by_contra h
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
m : ℕ
j : @cell _ inst C D _ m
h : ¬m < n
⊢ False

Tactic:
(hn m (not_lt.1 h)).false j

Premises used: IsEmpty.false
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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)
n : ℕ
hn : ∀ (b : ℕ), n ≤ b → IsEmpty.{u_2 + 1} (@cell _ inst C D _ b)
m : ℕ
j : @cell _ inst C D _ m
h : ¬m < n
⊢ False

Tactic:
exact (hn m (not_lt.1 h)).false j

Premises used: IsEmpty.false
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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

Tactic:
have (m) (j : cell C m) : m < n := by
    by_contra h
    exact (hn m (not_lt.1 h)).false j
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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
⊢ Function.LeftInverse
    (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)
    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

Tactic:
simp [Function.LeftInverse]

Premises used: Function.LeftInverse
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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
⊢ Function.RightInverse
    (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)
    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

Tactic:
simp [Function.RightInverse, Function.LeftInverse]

Premises used: Function.LeftInverse, Function.RightInverse
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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 := ⋯ }
rw : _root_.Finite.{u_2 + 1} ((m : { m : ℕ // m < n }) × @cell _ inst C D _ (↑m : ℕ))
⊢ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)

Tactic:
rw [← Equiv.finite_iff f]

Premises used: Equiv.finite_iff
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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.{u_2 + 1} ((m : { m : ℕ // m < n }) × @cell _ inst C D _ (↑m : ℕ))

Tactic:
Finite.instSigma

Premises used: Finite.instSigma
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
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.{u_2 + 1} ((m : { m : ℕ // m < n }) × @cell _ inst C D _ (↑m : ℕ))

Tactic:
exact Finite.instSigma

Premises used: Finite.instSigma
-- Module: Mathlib.Topology.CWComplex.Classical.Finite
Goal:
X : Type u_2
inst : TopologicalSpace X
C D : Set X
inst_1 : RelCWComplex C D
⊢ Finite C (D := D) ↔ _root_.Finite.{max (u_2 + 1) 1} ((n : ℕ) × @cell _ inst C D _ n)

Tactic:
⟨fun h ↦ finite_cells_of_finite (finite := h), finite_of_finite_cells⟩

Premises used: Topology.RelCWComplex.finite_of_finite_cells, Topology.RelCWComplex.finite_cells_of_finite, Iff.intro
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
x_1 : @cell _ inst C ∅ _ 1
h_1 : Membership.mem (γ := Set (@cell _ inst C ∅ _ 1)) univ x_1
x y : @cell _ inst C ∅ _ 0
h :
  (fun (x y : @cell _ inst C ∅ _ 0) ↦
      cellFrontier (C := C) (D := ∅) 1 x_1 = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y)
    x y
⊢ (fun (x y : @cell _ inst C ∅ _ 0) ↦
      cellFrontier (C := C) (D := ∅) 1 x_1 = closedCell (C := C) (D := ∅) 0 x ∪ closedCell (C := C) (D := ∅) 0 y)
    y x

Tactic:
grind
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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
⊢ 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

Premises used: Topology.RelCWComplex.closedCell_zero_eq_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) ![]}
⊢ 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

Premises used: Topology.RelCWComplex.closedCell_zero_eq_singleton
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) ![]}
⊢ 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
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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) ![]})
⊢ 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

Premises used: Function.Injective.eq_iff, Topology.RelCWComplex.injective_map_zero, Set.union_singleton, Set.pair_eq_pair_iff
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
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
inr₂ : y = z → x = w → ¬x = z → x = w
inl₃ : y = w → x = z → ¬x = z → x = w
⊢ x = z ∨ x = w

Tactic:
tauto
-- Module: Mathlib.Topology.CWComplex.Classical.Graph
Goal:
X : Type u_1
inst : TopologicalSpace X
C : Set X
inst_1 : CWComplex C
e : @cell _ inst C ∅ _ 1
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
⊢ 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

Tactic:
simp only [mem_univ, true_iff]

Premises used: true_iff, Set.mem_univ