case nil
c✝ c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ h, c.snd < List.get [] { val := c.fst, isLt := h }

case cons
c✝ : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
c : ℕ × ℕ
⊢ c ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, c.snd < List.get (w_hd :: w_tl) { val := c.fst, isLt := h }
w : List ℕ
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens w ↔ ∃ h, c.snd < List.get w { val := c.fst, isLt := h }
induction' w with w_hd w_tl w_ih generalizing c <;> rw [YoungDiagram.cellsOfRowLens]
no goals
case nil
c✝ c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ h, c.snd < List.get [] { val := c.fst, isLt := h }
simp [YoungDiagram.cellsOfRowLens]
case cons.mk.zero
c : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
snd✝ : ℕ
⊢ (Nat.zero, snd✝) ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, (Nat.zero, snd✝).snd < List.get (w_hd :: w_tl) { val := (Nat.zero, snd✝).fst, isLt := h }

case cons.mk.succ
c : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
snd✝ n✝ : ℕ
⊢ (Nat.succ n✝, snd✝) ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, (Nat.succ n✝, snd✝).snd < List.get (w_hd :: w_tl) { val := (Nat.succ n✝, snd✝).fst, isLt := h }
case cons
c✝ : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
c : ℕ × ℕ
⊢ c ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, c.snd < List.get (w_hd :: w_tl) { val := c.fst, isLt := h }
rcases c with ⟨⟨_, _⟩, _⟩
no goals
case cons.mk.zero
c : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
snd✝ : ℕ
⊢ (Nat.zero, snd✝) ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, (Nat.zero, snd✝).snd < List.get (w_hd :: w_tl) { val := (Nat.zero, snd✝).fst, isLt := h }
simp
no goals
case cons.mk.succ
c : ℕ × ℕ
w_hd : ℕ
w_tl : List ℕ
w_ih : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens w_tl ↔ ∃ h, c.snd < List.get w_tl { val := c.fst, isLt := h }
snd✝ n✝ : ℕ
⊢ (Nat.succ n✝, snd✝) ∈
      {0} ×ˢ Finset.range w_hd ∪
        Finset.map (Embedding.prodMap { toFun := Nat.succ, inj' := Nat.succ_injective } (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens w_tl) ↔
    ∃ h, (Nat.succ n✝, snd✝).snd < List.get (w_hd :: w_tl) { val := (Nat.succ n✝, snd✝).fst, isLt := h }
simp [w_ih, -Finset.singleton_product, Nat.succ_lt_succ_iff]