awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
h : (i, j) ∈ μ
x : ℕ
hmj : x ≤ j
⊢ i ≤ i

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
h : ∀ m ≤ j, (i, m) ∈ μ
⊢ j ≤ j

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, (i, m) ∈ μ

Tactic:
exact ⟨fun h _ hmj => μ.up_left_mem (by rfl) hmj h, fun h => h _ (by rfl)⟩
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i : ℕ
h : ∀ (a b : ℕ), (a, b) ∈ μ.row i ↔ (a, b) ∈ SProd.sprod (α := Finset ℕ) {i} (Finset.range (μ.rowLen i))
⊢ μ.row i = SProd.sprod (α := Finset ℕ) {i} (Finset.range (μ.rowLen i))

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i a b : ℕ
h : a = i → (b < μ.rowLen a ↔ b < μ.rowLen i)
⊢ (a, b) ∈ μ.row i ↔ (a, b) ∈ SProd.sprod (α := Finset ℕ) {i} (Finset.range (μ.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]

Premises used: Finset.mem_singleton, YoungDiagram.mem_row_iff, YoungDiagram.mem_iff_lt_rowLen, and_congr_right_iff, Finset.mem_range, and_comm, Finset.mem_product
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
a b : ℕ
⊢ b < μ.rowLen a ↔ b < μ.rowLen a

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i : ℕ
⊢ μ.rowLen i = (μ.row i).card

Tactic:
simp [row_eq_prod]

Premises used: YoungDiagram.row_eq_prod
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
by_contra! : ∀ (h_lt : μ.rowLen i1 < μ.rowLen i2), False
⊢ μ.rowLen i2 ≤ μ.rowLen i1

Tactic:
by_contra! h_lt
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
rw : μ.rowLen i1 < μ.rowLen i1
⊢ False

Tactic:
rw [← lt_self_iff_false (μ.rowLen i1)]

Premises used: lt_self_iff_false, YoungDiagram.rowLen
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : μ.rowLen i1 < μ.rowLen i2
rw : ∀ (h_lt : (i2, μ.rowLen i1) ∈ μ), (i1, μ.rowLen i1) ∈ μ
⊢ μ.rowLen i1 < μ.rowLen i1

Tactic:
rw [← mem_iff_lt_rowLen] at h_lt ⊢

Premises used: YoungDiagram.mem_iff_lt_rowLen
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ μ.rowLen i1 ≤ μ.rowLen i1

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i1 i2 : ℕ
hi : i1 ≤ i2
h_lt : (i2, μ.rowLen i1) ∈ μ
⊢ (i1, μ.rowLen i1) ∈ μ

Tactic:
exact μ.up_left_mem hi (by rfl) h_lt

Premises used: YoungDiagram.up_left_mem
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j : ℕ
c : ℕ × ℕ
⊢ c ∈ μ.col j ↔ c ∈ μ ∧ c.2 = j

Tactic:
simp [col]

Premises used: YoungDiagram.col
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ.col j ↔ (i, j) ∈ μ

Tactic:
simp [col]

Premises used: YoungDiagram.col
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j : ℕ
⊢ ∃ (j_1 : ℕ), (j, j_1) ∉ μ.transpose

Tactic:
μ.transpose.exists_notMem_row j

Premises used: YoungDiagram.transpose, YoungDiagram.exists_notMem_row
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j : ℕ
h : Eq (α := ℕ → Prop) (fun (i : ℕ) ↦ (i, j) ∉ μ.cells) fun (j_1 : ℕ) ↦ (j, j_1) ∉ μ.transpose
⊢ ∃ (i : ℕ), (i, j) ∉ μ.cells

Tactic:
convert! μ.transpose.exists_notMem_row j using 1

Premises used: YoungDiagram.transpose, YoungDiagram.exists_notMem_row
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j : ℕ
⊢ Eq (α := ℕ → Prop) (fun (i : ℕ) ↦ (i, j) ∉ μ.cells) fun (j_1 : ℕ) ↦ (j, j_1) ∉ μ.transpose

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j : ℕ
⊢ μ.transpose.colLen j = μ.rowLen j

Tactic:
simp [rowLen, colLen]

Premises used: YoungDiagram.rowLen, YoungDiagram.colLen
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i : ℕ
⊢ μ.transpose.rowLen i = μ.colLen i

Tactic:
simp [rowLen, colLen]

Premises used: YoungDiagram.rowLen, YoungDiagram.colLen
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
rw : (i, j) ∈ μ ↔ (j, i) ∈ μ.transpose
⊢ (i, j) ∈ μ ↔ i < μ.colLen j

Tactic:
rw [← rowLen_transpose, ← mem_iff_lt_rowLen]

Premises used: YoungDiagram.mem_iff_lt_rowLen, YoungDiagram.rowLen_transpose
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ (j, i) ∈ μ.transpose

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j : ℕ
h : ∀ (a b : ℕ), (a, b) ∈ μ.col j ↔ (a, b) ∈ SProd.sprod (β := Finset ℕ) (Finset.range (μ.colLen j)) {j}
⊢ μ.col j = SProd.sprod (β := Finset ℕ) (Finset.range (μ.colLen j)) {j}

Tactic:
ext ⟨a, b⟩
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j a b : ℕ
h : b = j → (a < μ.colLen b ↔ a < μ.colLen j)
⊢ (a, b) ∈ μ.col j ↔ (a, b) ∈ SProd.sprod (β := Finset ℕ) (Finset.range (μ.colLen j)) {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]

Premises used: Finset.mem_singleton, and_congr_right_iff, Finset.mem_range, and_comm, YoungDiagram.mem_iff_lt_colLen, YoungDiagram.mem_col_iff, Finset.mem_product
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
a b : ℕ
⊢ a < μ.colLen b ↔ a < μ.colLen b

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j : ℕ
⊢ μ.colLen j = (μ.col j).card

Tactic:
simp [col_eq_prod]

Premises used: YoungDiagram.col_eq_prod
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.transpose.rowLen j2 ≤ μ.transpose.rowLen j1

Tactic:
μ.transpose.rowLen_anti j1 j2 hj

Premises used: YoungDiagram.transpose, YoungDiagram.rowLen_anti
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
h : μ.colLen j2 = μ.transpose.rowLen j2
h₁ : μ.colLen j1 = μ.transpose.rowLen j1
⊢ μ.colLen j2 ≤ μ.colLen j1

Tactic:
convert! μ.transpose.rowLen_anti j1 j2 hj using 1

Premises used: YoungDiagram.transpose, YoungDiagram.rowLen_anti
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j2 = μ.transpose.rowLen j2

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
j1 j2 : ℕ
hj : j1 ≤ j2
⊢ μ.colLen j1 = μ.transpose.rowLen j1

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i : ℕ
h : i < μ.rowLens.length
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) μ.rowLens i h = μ.rowLen i

Tactic:
simp only [rowLens, List.getElem_range, List.getElem_map]

Premises used: List.getElem_range, YoungDiagram.rowLens, List.getElem_map
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
⊢ μ.rowLens.length = μ.colLen 0

Tactic:
simp only [rowLens, List.length_map, List.length_range]

Premises used: List.length_range, YoungDiagram.rowLens, List.length_map
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
⊢ μ.rowLens.SortedGE

Tactic:
(List.pairwise_le_range.map _ μ.rowLen_anti).sortedGE

Premises used: List.Pairwise.sortedGE, List.pairwise_le_range, YoungDiagram.rowLens, List.Pairwise.map
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
x : ℕ
hx : x ∈ μ.rowLens
⊢ ∃ a ∈ List.range (μ.colLen 0), μ.rowLen a = x

Tactic:
rw [rowLens, List.mem_map] at hx

Premises used: YoungDiagram.rowLens, List.mem_map
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
x : ℕ
hx : ∃ a ∈ List.range (μ.colLen 0), μ.rowLen a = x
obtain : ∀ (i : ℕ) (hi : i ∈ List.range (μ.colLen 0)), 0 < μ.rowLen i
⊢ 0 < x

Tactic:
obtain ⟨i, hi, rfl : μ.rowLen i = x⟩ := hx

Premises used: rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i : ℕ
hi : i ∈ List.range (μ.colLen 0)
rwa : ∀ (hi : i < μ.colLen 0), 0 < μ.rowLen i
rwa₁ : ∀ (hi : (i, 0) ∈ μ), 0 < μ.rowLen i
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (hi : 0 < μ.rowLen i), 0 < μ.rowLen i
⊢ 0 < μ.rowLen i

Tactic:
rwa [List.mem_range, ← mem_iff_lt_colLen, mem_iff_lt_rowLen] at hi

Premises used: List.mem_range, YoungDiagram.mem_iff_lt_rowLen, YoungDiagram.mem_iff_lt_colLen
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
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
⊢ c ∈ YoungDiagram.cellsOfRowLens w ↔
    ∃ (h : c.1 < w.length), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w c.1 h

Tactic:
induction w generalizing c
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
c : ℕ × ℕ
⊢ Membership.mem (γ := Finset (ℕ × ℕ)) ∅ c ↔
    ∃ (h : c.1 < List.length (α := ℕ) []), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) [] c.1 h

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
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
⊢ 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

Tactic:
rcases c with ⟨⟨_, _⟩, _⟩
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
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:
simp_all
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
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:
simp_all
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell : (i2, j2) ∈ (↑(YoungDiagram.cellsOfRowLens w) : Set (ℕ × ℕ))
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
⊢ (i1, j1) ∈ (↑(YoungDiagram.cellsOfRowLens w) : Set (ℕ × ℕ))

Tactic:
rw [Finset.mem_coe, YoungDiagram.mem_cellsOfRowLens] at hcell ⊢

Premises used: YoungDiagram.mem_cellsOfRowLens, Finset.mem_coe
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
⊢ (i2, j2).1 < w.length

Tactic:
obtain ⟨h1, h2⟩ := hcell
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
⊢ (i2, j2).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i2, j2).1 h1

Tactic:
obtain ⟨h1, h2⟩ := hcell
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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

Tactic:
⟨hi.trans_lt h1, ?_⟩

Premises used: Exists.intro, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
refine : (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 ⋯
⊢ ∃ (h : (i1, j1).1 < w.length),
    (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 h

Tactic:
refine ⟨hi.trans_lt h1, ?_⟩
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
⊢ j1 ≤ j2

Tactic:
hj
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
⊢ j2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1

Tactic:
h2
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
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 ⋯
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 ⋯

Tactic:
obtain rfl | h := eq_or_lt_of_le hi

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
w : List ℕ
hw : w.SortedGE
j2 i1 j1 : ℕ
hj : j1 ≤ j2
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:
rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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 < i2
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 ⋯

Tactic:
hw.getElem_ge_getElem_of_le h.le

Premises used: LT.lt.le, List.SortedGE.getElem_ge_getElem_of_le
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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 < i2
⊢ getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 ⋯

Tactic:
exact hw.getElem_ge_getElem_of_le h.le

Premises used: LT.lt.le, List.SortedGE.getElem_ge_getElem_of_le
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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
j1₁ :
  getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i2 h1 ≤
    getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w i1 ⋯
⊢ (i1, j1).2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w (i1, j1).1 ⋯

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
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
w : List ℕ
hw : w.SortedGE
c : ℕ × ℕ
⊢ c ∈ ofRowLens w hw ↔
    ∃ (h : c.1 < w.length), c.2 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w c.1 h

Tactic:
YoungDiagram.mem_cellsOfRowLens

Premises used: Set.Mem, setOf, YoungDiagram.mem_cellsOfRowLens
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
w : List ℕ
hw : w.SortedGE
hpos : ∀ x ∈ w, 0 < x
simp :
  ¬False ∧ ∀ n < w.length, ∃ (h : n < w.length), 0 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w n ⋯
⊢ (ofRowLens w hw).rowLens.length = w.length

Tactic:
simp only [length_rowLens, colLen, Nat.find_eq_iff, mem_cells, mem_ofRowLens,
    lt_self_iff_false, IsEmpty.exists_iff, Classical.not_not]

Premises used: YoungDiagram.mem_ofRowLens, YoungDiagram.mem_cells, Classical.not_not, YoungDiagram.length_rowLens, IsEmpty.exists_iff, lt_self_iff_false, YoungDiagram.colLen, Nat.find_eq_iff
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
w : List ℕ
hw : w.SortedGE
hpos : ∀ x ∈ w, 0 < x
⊢ ¬False ∧ ∀ n < w.length, ∃ (h : n < w.length), 0 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w n ⋯

Tactic:
⟨not_false, fun n hn => ⟨hn, hpos _ (List.getElem_mem hn)⟩⟩

Premises used: Iff.mpr, Iff.of_eq, GetElem.getElem, not_false, List.getElem_mem, And.intro, LT.lt, Exists.intro, Eq.refl, List.length
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
w : List ℕ
hw : w.SortedGE
hpos : ∀ x ∈ w, 0 < x
⊢ ¬False ∧ ∀ n < w.length, ∃ (h : n < w.length), 0 < getElem (valid := fun (as : List ℕ) (i : ℕ) ↦ i < as.length) w n ⋯

Tactic:
exact ⟨not_false, fun n hn => ⟨hn, hpos _ (List.getElem_mem hn)⟩⟩
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
w : List ℕ
hw : w.SortedGE
i : Fin w.length
⊢ (ofRowLens w hw).rowLen (↑i : ℕ) =
    getElem (valid := fun (xs : List ℕ) (i : Fin w.length) ↦ (↑i : ℕ) < xs.length) w i ⋯

Tactic:
simp [rowLen, Nat.find_eq_iff, mem_ofRowLens]

Premises used: YoungDiagram.mem_ofRowLens, YoungDiagram.rowLen, Nat.find_eq_iff
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
cells : ∀ (i j : ℕ), (i, j) ∈ (ofRowLens μ.rowLens ⋯).cells ↔ (i, j) ∈ μ.cells
⊢ ofRowLens μ.rowLens ⋯ = μ

Tactic:
ext ⟨i, j⟩
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
cells : (∃ (_ : i < μ.colLen 0), j < μ.rowLen i) ↔ (i, j) ∈ μ
⊢ (i, j) ∈ (ofRowLens μ.rowLens ⋯).cells ↔ (i, j) ∈ μ.cells

Tactic:
simp only [mem_cells, mem_ofRowLens, length_rowLens, get_rowLens]

Premises used: YoungDiagram.mem_ofRowLens, YoungDiagram.mem_cells, YoungDiagram.length_rowLens, YoungDiagram.get_rowLens
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (∃ (_ : i < μ.colLen 0), j < μ.rowLen i) ↔ (i, j) ∈ μ

Tactic:
simpa [← mem_iff_lt_colLen, mem_iff_lt_rowLen] using j.zero_le.trans_lt

Premises used: Nat.zero_le, YoungDiagram.mem_iff_lt_rowLen, YoungDiagram.mem_iff_lt_colLen, LE.le.trans_lt
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
w : List ℕ
hw : w.SortedGE
hpos : ∀ x ∈ w, 0 < x
⊢ (ofRowLens w hw).rowLens = w

Tactic:
List.ext_get (rowLens_length_ofRowLens hpos) fun i h₁ h₂ =>
    (get_rowLens (h := h₁)).trans <| rowLen_ofRowLens ⟨i, h₂⟩

Premises used: Fin.mk, List.ext_get, YoungDiagram.get_rowLens, YoungDiagram.rowLen_ofRowLens, YoungDiagram.rowLens_length_ofRowLens, Eq.trans
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
rw rw₁ : n + 1 = n + 1
⊢ ack 0 n = n + 1

Tactic:
rw [ack]

Premises used: ack
-- Module: Mathlib.Computability.Ackermann
Goal:
m : ℕ
rw rw₁ : ack m 1 = ack m 1
⊢ ack (m + 1) 0 = ack m 1

Tactic:
rw [ack]

Premises used: ack
-- Module: Mathlib.Computability.Ackermann
Goal:
m n : ℕ
rw rw₁ : ack m (ack (m + 1) n) = ack m (ack (m + 1) n)
⊢ ack (m + 1) (n + 1) = ack m (ack (m + 1) n)

Tactic:
rw [ack]

Premises used: ack
-- Module: Mathlib.Computability.Ackermann
Goal:
⊢ ack 1 0 = HAdd.hAdd (α := ℕ) 0 2

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
IH : ack 1 n = n + 2
⊢ ack 1 (n + 1) = n + 1 + 2

Tactic:
simp [IH]
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
zero : ack 1 0 = HAdd.hAdd (α := ℕ) 0 2
succ : ∀ (n : ℕ) (IH : ack 1 n = n + 2), ack 1 (n + 1) = n + 1 + 2
⊢ ack 1 n = n + 2

Tactic:
induction n with
  | zero => simp
  | succ n IH => simp [IH]

Premises used: Nat.zero, Nat.succ
-- Module: Mathlib.Computability.Ackermann
Goal:
⊢ ack 2 0 = HMul.hMul (α := ℕ) 2 0 + 3

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
IH : ack 2 n = 2 * n + 3
⊢ ack 2 (n + 1) = 2 * (n + 1) + 3

Tactic:
simpa [mul_succ]

Premises used: Nat.mul_succ
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
zero : ack 2 0 = HMul.hMul (α := ℕ) 2 0 + 3
succ : ∀ (n : ℕ) (IH : ack 2 n = 2 * n + 3), ack 2 (n + 1) = 2 * (n + 1) + 3
⊢ ack 2 n = 2 * n + 3

Tactic:
induction n with
  | zero => simp
  | succ n IH => simpa [mul_succ]

Premises used: Nat.mul_succ, Nat.zero, Nat.succ
-- Module: Mathlib.Computability.Ackermann
Goal:
⊢ ack 3 0 = HPow.hPow (α := ℕ) 2 (HAdd.hAdd (α := ℕ) 0 3) - 3

Tactic:
simp
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
succ : HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) 2 (n + 3)
⊢ ack 3 (n + 1) = HPow.hPow (α := ℕ) 2 (n + 1 + 3) - 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]

Premises used: Nat.mul_sub_left_distrib, Nat.sub_add_comm, two_mul, Nat.pow_succ, ack_succ_succ, HAdd.hAdd, ack_two, mul_comm, Nat.add_sub_add_right, Nat.succ_add, OfNat.ofNat
-- Module: Mathlib.Computability.Ackermann
Goal:
n : ℕ
IH : ack 3 n = HPow.hPow (α := ℕ) 2 (n + 3) - 3
⊢ HMul.hMul (α := ℕ) 2 3 ≤ 2 * HPow.hPow (α := ℕ) (β := ℕ) 2 3

Tactic:
simp