awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
inl : ∀ (h : i1 = i2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
have inr : ∀ (h : i1 < i2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
Tactic: rcases eq_or_lt_of_le hi with h | h
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
have inl : LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
i j1 j2 : ℕ
hj : j1 < j2
hcell : (i, j2) ∈ μ
⊢ (if (i, j1) ∈ μ then i else 0) ≤ if (i, j2) ∈ μ then i else 0
have rw : (if (i, j1) ∈ μ then i else 0) ≤ i
Tactic: rw [if_pos hcell, if_pos (μ.up_left_mem (by rfl) (le_of_lt hj) hcell)]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
i j1 j2 : ℕ
hj : j1 < j2
hcell : (i, j2) ∈ μ
rw : (if (i, j1) ∈ μ then i else 0) ≤ i
⊢ (if (i, j1) ∈ μ then i else 0) ≤ if (i, j2) ∈ μ then i else 0
have rw₁ : i ≤ i
Tactic: rw [if_pos hcell, if_pos (μ.up_left_mem (by rfl) (le_of_lt hj) hcell)]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.SemistandardTableau (goal)
Goal:
μ : YoungDiagram
i1 i2 j : ℕ
hi : i1 < i2
hcell : (i2, j) ∈ μ
⊢ (if (i1, j) ∈ μ then i1 else 0) < if (i2, j) ∈ μ then i2 else 0
have rwa : (if (i1, j) ∈ μ then i1 else 0) < i2
Tactic: rwa [if_pos hcell, if_pos (μ.up_left_mem (le_of_lt hi) (by rfl) hcell)]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
h :
  Eq (α := Set (ℕ × ℕ)) ((fun (y : YoungDiagram) ↦ (↑y.cells : Set (ℕ × ℕ))) μ)
    ((fun (y : YoungDiagram) ↦ (↑y.cells : Set (ℕ × ℕ))) ν)
⊢ μ = ν
have rwa : μ.cells = ν.cells
Tactic: rwa [YoungDiagram.ext_iff, ← Finset.coe_inj]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
⊢ IsLowerSet (↑(μ.cells ∪ ν.cells) : Set (ℕ × ℕ))
have rw : IsLowerSet ((↑μ.cells : Set (ℕ × ℕ)) ∪ (↑ν.cells : Set (ℕ × ℕ)))
Tactic: rw [Finset.coe_union]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
⊢ IsLowerSet (↑(μ.cells ∩ ν.cells) : Set (ℕ × ℕ))
have rw : IsLowerSet ((↑μ.cells : Set (ℕ × ℕ)) ∩ (↑ν.cells : Set (ℕ × ℕ)))
Tactic: rw [Finset.coe_inter]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
a b : ℕ × ℕ
h_1 : b ≤ a
h : a ∈ (↑∅ : Set (ℕ × ℕ))
⊢ b ∈ (↑∅ : Set (ℕ × ℕ))
have simp : False
Tactic: simp only [Finset.coe_empty, Set.mem_empty_iff_false]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
⊢ (↑⊥ : Set (ℕ × ℕ)) = ∅
have h : ∀ (x : ℕ × ℕ), x ∈ (↑⊥ : Set (ℕ × ℕ)) ↔ Membership.mem (γ := Set (ℕ × ℕ)) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
x x_1 : ℕ × ℕ
h : x_1 ≤ x
⊢ x ∈
      (↑(((Equiv.prodComm ℕ ℕ).finsetCongr : (a : Finset (ℕ × ℕ)) → Finset (ℕ × ℕ)) μ.cells : Finset (ℕ × ℕ)) :
        Set (ℕ × ℕ)) →
    x_1 ∈
      (↑(((Equiv.prodComm ℕ ℕ).finsetCongr : (a : Finset (ℕ × ℕ)) → Finset (ℕ × ℕ)) μ.cells : Finset (ℕ × ℕ)) :
        Set (ℕ × ℕ))
have simp : Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x : ℕ × ℕ) →
  Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x_1 : ℕ × ℕ)
Tactic: simp only [Finset.mem_coe, Equiv.finsetCongr_apply, Finset.mem_map_equiv]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
x x_1 : ℕ × ℕ
h : x_1 ≤ x
hcell : Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x : ℕ × ℕ)
⊢ Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x_1 : ℕ × ℕ)
have apply : LE.le (α := ℕ × ℕ) (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x_1 : ℕ × ℕ)
  (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x : ℕ × ℕ)
Tactic: apply μ.isLowerSet _ hcell
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
⊢ μ.transpose.transpose = μ
have cells : ∀ (x : ℕ × ℕ), x ∈ μ.transpose.transpose.cells ↔ x ∈ μ.cells
Tactic: ext x
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
⊢ μ.transpose = ν ↔ μ = ν.transpose
have mp : μ.transpose = ν → μ = ν.transpose
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
mp : μ.transpose = ν → μ = ν.transpose
⊢ μ.transpose = ν ↔ μ = ν.transpose
have mpr : μ = ν.transpose → μ.transpose = ν
Tactic: constructor
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
⊢ μ.transpose = ν.transpose ↔ μ = ν
have rw : μ = ν.transpose.transpose ↔ μ = ν
Tactic: rw [transpose_eq_iff_eq_transpose]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ
⊢ c ∈ ν.transpose
have simp : c.swap ∈ ν
Tactic: simp only [mem_transpose]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ
⊢ c.swap ∈ ν
have a : c.swap ∈ μ.transpose
Tactic: apply h_le
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
⊢ μ ≤ ν
have h₁ : ν = ν.transpose.transpose
Tactic: convert! YoungDiagram.le_of_transpose_le h
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (hypothesis)
Goal:
μ ν : YoungDiagram
h : μ ≤ ν
⊢ μ.transpose ≤ ν.transpose
have h₁ : μ.transpose.transpose ≤ ν
Tactic: rw [← transpose_transpose μ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i x : ℕ
h_1 : x ∈ Prod.mk i ⁻¹' (↑μ.cells : Set (ℕ × ℕ))
x_1 : ℕ
h_2 : x_1 ∈ Prod.mk i ⁻¹' (↑μ.cells : Set (ℕ × ℕ))
h : (i, x) = (i, x_1)
⊢ x = x_1
have refl : x ∈ Prod.mk i ⁻¹' (↑μ.cells : Set (ℕ × ℕ)) → x = x
Tactic: cases h
Cleared hypotheses: x_1, h_2, h
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i : ℕ
⊢ ∃ (j : ℕ), (i, j) ∉ μ
have obtain : ∀ (j : ℕ) (hj : j ∉ μ.cells.preimage (Prod.mk i) sorry), ∃ (j : ℕ), (i, j) ∉ μ
Tactic: obtain ⟨j, hj⟩ :=
    Infinite.exists_notMem_finset
      (μ.cells.preimage (Prod.mk i) fun _ _ _ _ h => by
        cases h
        rfl)
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (hypothesis)
Goal:
μ : YoungDiagram
i j : ℕ
hj : j ∉ μ.cells.preimage (Prod.mk i) ⋯
⊢ ∃ (j : ℕ), (i, j) ∉ μ
have hj₁ : (i, j) ∉ μ.cells
Tactic: rw [Finset.mem_preimage] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ j < μ.rowLen i
have rw : (i, j) ∈ μ ↔ ∀ m ≤ j, ¬(i, m) ∉ μ
Tactic: rw [rowLen, Nat.lt_find_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, ¬(i, m) ∉ μ
have push : (i, j) ∈ μ ↔ ∀ m ≤ j, (i, m) ∈ μ
Tactic: push Not
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i : ℕ
⊢ μ.row i = SProd.sprod (α := Finset ℕ) {i} (Finset.range (μ.rowLen i))
have h : ∀ (a b : ℕ), (a, b) ∈ μ.row i ↔ (a, b) ∈ SProd.sprod (α := Finset ℕ) {i} (Finset.range (μ.rowLen i))
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i a b : ℕ
⊢ (a, b) ∈ μ.row i ↔ (a, b) ∈ SProd.sprod (α := Finset ℕ) {i} (Finset.range (μ.rowLen i))
have h : a = i → (b < μ.rowLen a ↔ b < μ.rowLen i)
Tactic: simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_row_iff,
    mem_iff_lt_rowLen, and_comm, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
⊢ μ.rowLen i2 ≤ μ.rowLen i1
have by_contra! : ∀ (h_lt : μ.rowLen i1 < μ.rowLen i2), False
Tactic: by_contra! h_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
⊢ False
have rw : μ.rowLen i1 < μ.rowLen i1
Tactic: rw [← lt_self_iff_false (μ.rowLen i1)]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
⊢ μ.rowLen i1 < μ.rowLen i1
have rw : ∀ (h_lt : (i2, μ.rowLen i1) ∈ μ), (i1, μ.rowLen i1) ∈ μ
Tactic: rw [← mem_iff_lt_rowLen] at h_lt ⊢
Cleared hypotheses: h_lt
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
j : ℕ
⊢ ∃ (i : ℕ), (i, j) ∉ μ.cells
have h : Eq (α := ℕ → Prop) (fun (i : ℕ) ↦ (i, j) ∉ μ.cells) fun (j_1 : ℕ) ↦ (j, j_1) ∉ μ.transpose
Tactic: convert! μ.transpose.exists_notMem_row j using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ i < μ.colLen j
have rw : (i, j) ∈ μ ↔ (j, i) ∈ μ.transpose
Tactic: rw [← rowLen_transpose, ← mem_iff_lt_rowLen]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
j : ℕ
⊢ μ.col j = SProd.sprod (β := Finset ℕ) (Finset.range (μ.colLen j)) {j}
have h : ∀ (a b : ℕ), (a, b) ∈ μ.col j ↔ (a, b) ∈ SProd.sprod (β := Finset ℕ) (Finset.range (μ.colLen j)) {j}
Tactic: ext ⟨a, b⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
j a b : ℕ
⊢ (a, b) ∈ μ.col j ↔ (a, b) ∈ SProd.sprod (β := Finset ℕ) (Finset.range (μ.colLen j)) {j}
have h : b = j → (a < μ.colLen b ↔ a < μ.colLen j)
Tactic: simp only [Finset.mem_product, Finset.mem_singleton, Finset.mem_range, mem_col_iff,
    mem_iff_lt_colLen, and_comm, and_congr_right_iff]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j2 ≤ μ.colLen j1
have h : μ.colLen j2 = μ.transpose.rowLen j2
Tactic: convert! μ.transpose.rowLen_anti j1 j2 hj using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
h : μ.colLen j2 = μ.transpose.rowLen j2
⊢ μ.colLen j2 ≤ μ.colLen j1
have h₁ : μ.colLen j1 = μ.transpose.rowLen j1
Tactic: convert! μ.transpose.rowLen_anti j1 j2 hj using 1
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (hypothesis)
Goal:
μ : YoungDiagram
x : ℕ
hx : x ∈ μ.rowLens
⊢ 0 < x
have hx₁ : ∃ a ∈ List.range (μ.colLen 0), μ.rowLen a = x
Tactic: rw [rowLens, List.mem_map] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
x : ℕ
hx : ∃ a ∈ List.range (μ.colLen 0), μ.rowLen a = x
⊢ 0 < x
have obtain : ∀ (i : ℕ) (hi : i ∈ List.range (μ.colLen 0)), 0 < μ.rowLen i
Tactic: obtain ⟨i, hi, rfl : μ.rowLen i = x⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i : ℕ
hi : i ∈ List.range (μ.colLen 0)
⊢ 0 < μ.rowLen i
have rwa : ∀ (hi : i < μ.colLen 0), 0 < μ.rowLen i
Tactic: rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i : ℕ
hi : i ∈ List.range (μ.colLen 0)
rwa : ∀ (hi : i < μ.colLen 0), 0 < μ.rowLen i
⊢ 0 < μ.rowLen i
have rwa₁ : ∀ (hi : (i, 0) ∈ μ), 0 < μ.rowLen i
Tactic: rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i : ℕ
hi : i ∈ List.range (μ.colLen 0)
rwa : ∀ (hi : i < μ.colLen 0), 0 < μ.rowLen i
rwa₁ : ∀ (hi : (i, 0) ∈ μ), 0 < μ.rowLen i
⊢ 0 < μ.rowLen i
have rwa₂ : ∀ (hi : 0 < μ.rowLen i), 0 < μ.rowLen i
Tactic: rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
w : List ℕ
c : ℕ × ℕ
⊢ c ∈ YoungDiagram.cellsOfRowLens w ↔
    ∃ (h : c.1 < w.length), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w c.1 h
have nil : ∀ {c : ℕ × ℕ},
  c ∈ YoungDiagram.cellsOfRowLens [] ↔
    ∃ (h : c.1 < List.length (α := ℕ) []), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] c.1 h
Tactic: induction w generalizing c
Cleared hypotheses: w, c
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
w : List ℕ
c : ℕ × ℕ
nil :
  ∀ {c : ℕ × ℕ},
    c ∈ YoungDiagram.cellsOfRowLens [] ↔
      ∃ (h : c.1 < List.length (α := ℕ) []), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] c.1 h
⊢ c ∈ YoungDiagram.cellsOfRowLens w ↔
    ∃ (h : c.1 < w.length), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w c.1 h
have cons : ∀ (head : ℕ) (tail : List ℕ),
  (∀ {c : ℕ × ℕ},
      c ∈ YoungDiagram.cellsOfRowLens tail ↔
        ∃ (h : c.1 < tail.length), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail c.1 h) →
    ∀ {c : ℕ × ℕ},
      c ∈ YoungDiagram.cellsOfRowLens (head :: tail) ↔
        ∃ (h : c.1 < (head :: tail).length),
          c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) c.1 h
Tactic: induction w generalizing c
Cleared hypotheses: w, c
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
head : ℕ
tail : List ℕ
tail_ih :
  ∀ {c : ℕ × ℕ},
    c ∈ YoungDiagram.cellsOfRowLens tail ↔
      ∃ (h : c.1 < tail.length), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail c.1 h
c : ℕ × ℕ
⊢ c ∈
      SProd.sprod (α := Finset ℕ) {0} (Finset.range head) ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail) ↔
    ∃ (h : c.1 < (head :: tail).length),
      c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) c.1 h
have cons : ∀ (snd : ℕ),
  (0, snd) ∈
      SProd.sprod (α := Finset ℕ) {0} (Finset.range head) ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail) ↔
    ∃ (h : (0, snd).1 < (head :: tail).length),
      (0, snd).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) (0, snd).1 h
Tactic: rcases c with ⟨⟨_, _⟩, _⟩
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
head : ℕ
tail : List ℕ
tail_ih :
  ∀ {c : ℕ × ℕ},
    c ∈ YoungDiagram.cellsOfRowLens tail ↔
      ∃ (h : c.1 < tail.length), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) tail c.1 h
c : ℕ × ℕ
cons :
  ∀ (snd : ℕ),
    (0, snd) ∈
        SProd.sprod (α := Finset ℕ) {0} (Finset.range head) ∪
          Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
            (YoungDiagram.cellsOfRowLens tail) ↔
      ∃ (h : (0, snd).1 < (head :: tail).length),
        (0, snd).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) (0, snd).1 h
⊢ c ∈
      SProd.sprod (α := Finset ℕ) {0} (Finset.range head) ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail) ↔
    ∃ (h : c.1 < (head :: tail).length),
      c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) c.1 h
have cons₁ : ∀ (snd n : ℕ),
  (n + 1, snd) ∈
      SProd.sprod (α := Finset ℕ) {0} (Finset.range head) ∪
        Finset.map ({ toFun := Nat.succ, inj' := Nat.succ_injective : ℕ ↪ ℕ }.prodMap (Embedding.refl ℕ))
          (YoungDiagram.cellsOfRowLens tail) ↔
    ∃ (h : (n + 1, snd).1 < (head :: tail).length),
      (n + 1, snd).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) (head :: tail) (n + 1, snd).1 h
Tactic: rcases c with ⟨⟨_, _⟩, _⟩
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell : (i2, j2) ∈ (↑(YoungDiagram.cellsOfRowLens w) : Set (ℕ × ℕ))
⊢ (i1, j1) ∈ (↑(YoungDiagram.cellsOfRowLens w) : Set (ℕ × ℕ))
have rw : ∀
  (hcell :
    ∃ (h : (i2, j2).1 < w.length),
      (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h),
  ∃ (h : (i1, j1).1 < w.length),
    (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 h
Tactic: rw [Finset.mem_coe, YoungDiagram.mem_cellsOfRowLens] at hcell ⊢
Cleared hypotheses: hcell
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (hypothesis)
Goal:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell :
  ∃ (h : (i2, j2).1 < w.length),
    (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h
⊢ ∃ (h : (i1, j1).1 < w.length),
    (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 h
have h1 : (i2, j2).1 < w.length
Tactic: obtain ⟨h1, h2⟩ := hcell
Cleared hypotheses: hcell
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (hypothesis)
Goal:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell :
  ∃ (h : (i2, j2).1 < w.length),
    (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h
h1 : (i2, j2).1 < w.length
⊢ ∃ (h : (i1, j1).1 < w.length),
    (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 h
have h2 : (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h1
Tactic: obtain ⟨h1, h2⟩ := hcell
Cleared hypotheses: hcell
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h1
⊢ ∃ (h : (i1, j1).1 < w.length),
    (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 h
have refine : (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 sorry
Tactic: refine ⟨hi.trans_lt h1, ?_⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h1
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 ⋯
have inl : ∀ (hi : i1 ≤ i1) (h1 : (i1, j2).1 < w.length)
  (h2 : (i1, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j2).1 h1),
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 h1 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 h1
Tactic: obtain rfl | h := eq_or_lt_of_le hi
Cleared hypotheses: i2, hi, h1, h2
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h1
inl :
  ∀ (hi : i1 ≤ i1) (h1 : (i1, j2).1 < w.length)
    (h2 : (i1, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j2).1 h1),
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 h1 ≤
      getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 h1
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 ⋯
have inr : ∀ (h : i1 < i2),
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 sorry
Tactic: obtain rfl | h := eq_or_lt_of_le hi
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h1
⊢ (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 ⋯
have j1₁ : getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1 ≤
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 sorry
Tactic: calc
      j1 ≤ j2 := hj
      _ < w[i2] := h2
      _ ≤ w[i1] := by
        obtain rfl | h := eq_or_lt_of_le hi
        · rfl
        · exact hw.getElem_ge_getElem_of_le h.le
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
w : List ℕ
hw : w.SortedGE
hpos : ∀ x ∈ w, 0 < x
⊢ (ofRowLens w hw).rowLens.length = w.length
have simp : ¬False ∧ ∀ n < w.length, ∃ (h : n < w.length), 0 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w n sorry
Tactic: simp only [length_rowLens, colLen, Nat.find_eq_iff, mem_cells, mem_ofRowLens,
    lt_self_iff_false, IsEmpty.exists_iff, Classical.not_not]
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
⊢ ofRowLens μ.rowLens ⋯ = μ
have cells : ∀ (i j : ℕ), (i, j) ∈ (ofRowLens μ.rowLens sorry).cells ↔ (i, j) ∈ μ.cells
Tactic: ext ⟨i, j⟩
-- Lean 4 proof step from Mathlib.Combinatorics.Young.YoungDiagram (goal)
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ (ofRowLens μ.rowLens ⋯).cells ↔ (i, j) ∈ μ.cells
have cells : (∃ (_ : i < μ.colLen 0), j < μ.rowLen i) ↔ (i, j) ∈ μ
Tactic: simp only [mem_cells, mem_ofRowLens, length_rowLens, get_rowLens]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
⊢ ack 0 n = n + 1
have rw : n + 1 = n + 1
Tactic: rw [ack]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m : ℕ
⊢ ack (m + 1) 0 = ack m 1
have rw : ack m 1 = ack m 1
Tactic: rw [ack]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
m n : ℕ
⊢ ack (m + 1) (n + 1) = ack m (ack (m + 1) n)
have rw : ack m (ack (m + 1) n) = ack m (ack (m + 1) n)
Tactic: rw [ack]
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
⊢ ack 1 n = n + 2
have zero : ack 1 0 = HAdd.hAdd (α := ℕ) 0 2
Tactic: induction n with
  | zero => simp
  | succ n IH => simp [IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
zero : ack 1 0 = HAdd.hAdd (α := ℕ) 0 2
⊢ ack 1 n = n + 2
have succ : ∀ (n : ℕ) (IH : ack 1 n = n + 2), ack 1 (n + 1) = n + 1 + 2
Tactic: induction n with
  | zero => simp
  | succ n IH => simp [IH]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
⊢ ack 2 n = 2 * n + 3
have zero : ack 2 0 = HMul.hMul (α := ℕ) 2 0 + 3
Tactic: induction n with
  | zero => simp
  | succ n IH => simpa [mul_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
zero : ack 2 0 = HMul.hMul (α := ℕ) 2 0 + 3
⊢ ack 2 n = 2 * n + 3
have succ : ∀ (n : ℕ) (IH : ack 2 n = 2 * n + 3), ack 2 (n + 1) = 2 * (n + 1) + 3
Tactic: induction n with
  | zero => simp
  | succ n IH => simpa [mul_succ]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Computability.Ackermann (goal)
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
⊢ ack 3 (n + 1) = HPow.hPow (α := ℕ) 2 (n + 1 + 3) - 3
have succ : HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)
Tactic: rw [ack_succ_succ, IH, ack_two, Nat.succ_add, Nat.pow_succ 2 (n + 3), mul_comm _ 2,
        Nat.mul_sub_left_distrib, ← Nat.sub_add_comm, two_mul 3, Nat.add_sub_add_right]