Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ∀
    ⦃x :
      (n : ℕ) ×
        match n with
        | 0 => ↑D
        | n.succ => PEmpty.{u_1 + 1}⦄,
    x ∈ univ →
      ∀
        ⦃y :
          (n : ℕ) ×
            match n with
            | 0 => ↑D
            | n.succ => PEmpty.{u_1 + 1}⦄,
        y ∈ univ →
          x ≠ y →
            Disjoint
              ((fun a ↦
                  ↑(match x.fst, x.snd with
                      | 0, i => PartialEquiv.single ![] ↑i
                      | n.succ, i => i.elim)
                    a) ''
                ball 0 1)
              ((fun a ↦
                  ↑(match y.fst, y.snd with
                      | 0, i => PartialEquiv.single ![] ↑i
                      | n.succ, i => i.elim)
                    a) ''
                ball 0 1)

Tactic:
rintro ⟨_|n, j⟩ _ ⟨_|m, i⟩ _ ne

Goal state after:
case zero.zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
j :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨0, j⟩ ∈ univ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨0, i⟩ ∈ univ
ne : ⟨0, j⟩ ≠ ⟨0, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨0, j⟩.fst, ⟨0, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨0, i⟩.fst, ⟨0, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

case zero.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
j :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨0, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨0, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨0, j⟩.fst, ⟨0, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

case succ.zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨0, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨0, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨0, i⟩.fst, ⟨0, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

case succ.succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
j :
  match n + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨n + 1, j⟩ ∈ univ
m : ℕ
i :
  match m + 1 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨m + 1, i⟩ ∈ univ
ne : ⟨n + 1, j⟩ ≠ ⟨m + 1, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨n + 1, j⟩.fst, ⟨n + 1, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨m + 1, i⟩.fst, ⟨m + 1, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)