Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: 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)

pp: 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)

pp: 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)

pp: 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)

Tactic:
· simp_all [Subtype.coe_injective.ne]

Goal state after:
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)