awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Tiling.Tile
Goal:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst : Group G
inst_1 : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
simp_rw : x ∈ (↑(g⁻¹ • pt) : Set X) ↔ g • x ∈ (↑pt : Set X)
simp_rw₁ : x ∈ g⁻¹ • (↑pt : Set X) ↔ g • x ∈ (↑pt : Set X)
⊢ x ∈ g⁻¹ • pt ↔ g • x ∈ pt

Tactic:
simp_rw [← mem_coe, coe_smul, Set.mem_inv_smul_set_iff]

Premises used: DiscreteTiling.PlacedTile.mem_coe, Set.mem_inv_smul_set_iff, DiscreteTiling.PlacedTile.coe_smul
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : T.entry = T'.entry
mk :
  ∀ (entry : ℕ → ℕ → ℕ) (row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2)
    (col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j)
    (zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0)
    (h :
      { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
            SemistandardYoungTableau μ }.entry =
        T'.entry),
    { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
        SemistandardYoungTableau μ } =
      T'
⊢ T = T'

Tactic:
cases T
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T' : SemistandardYoungTableau μ
entry : ℕ → ℕ → ℕ
row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2
col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j
zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0
h :
  { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
        SemistandardYoungTableau μ }.entry =
    T'.entry
mk :
  ∀ (entry_1 : ℕ → ℕ → ℕ) (row_weak'_1 : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry_1 i j1 ≤ entry_1 i j2)
    (col_strict'_1 : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry_1 i1 j < entry_1 i2 j)
    (zeros'_1 : ∀ {i j : ℕ}, (i, j) ∉ μ → entry_1 i j = 0)
    (h :
      { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
            SemistandardYoungTableau μ }.entry =
        { entry := entry_1, row_weak' := @row_weak'_1, col_strict' := @col_strict'_1, zeros' := @zeros'_1 :
            SemistandardYoungTableau μ }.entry),
    { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
        SemistandardYoungTableau μ } =
      { entry := entry_1, row_weak' := @row_weak'_1, col_strict' := @col_strict'_1, zeros' := @zeros'_1 }
⊢ { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
      SemistandardYoungTableau μ } =
    T'

Tactic:
cases T'
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
entry : ℕ → ℕ → ℕ
row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2
col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j
zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0
entry_1 : ℕ → ℕ → ℕ
row_weak'_1 : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry_1 i j1 ≤ entry_1 i j2
col_strict'_1 : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry_1 i1 j < entry_1 i2 j
zeros'_1 : ∀ {i j : ℕ}, (i, j) ∉ μ → entry_1 i j = 0
h :
  { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
        SemistandardYoungTableau μ }.entry =
    { entry := entry_1, row_weak' := @row_weak'_1, col_strict' := @col_strict'_1, zeros' := @zeros'_1 :
        SemistandardYoungTableau μ }.entry
⊢ { entry := entry, row_weak' := @row_weak', col_strict' := @col_strict', zeros' := @zeros' :
      SemistandardYoungTableau μ } =
    { entry := entry_1, row_weak' := @row_weak'_1, col_strict' := @col_strict'_1, zeros' := @zeros'_1 }

Tactic:
congr
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
⊢ T.entry = (⇑T : (a : ℕ) → ℕ → ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : ∀ (i j : ℕ), Eq (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j : ℕ) ((T' : (a : ℕ) → ℕ → ℕ) i j : ℕ)
x : ℕ
h₁ : ∀ (x_1 : ℕ), Eq (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) x x_1 : ℕ) ((T' : (a : ℕ) → ℕ → ℕ) x x_1 : ℕ)
⊢ Eq (α := ℕ → ℕ) ((T : (a : ℕ) → ℕ → ℕ) x : ℕ → ℕ) ((T' : (a : ℕ) → ℕ → ℕ) x : ℕ → ℕ)

Tactic:
funext
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T T' : SemistandardYoungTableau μ
h : ∀ (i j : ℕ), Eq (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j : ℕ) ((T' : (a : ℕ) → ℕ → ℕ) i j : ℕ)
x x_1 : ℕ
⊢ Eq (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) x x_1 : ℕ) ((T' : (a : ℕ) → ℕ → ℕ) x x_1 : ℕ)

Tactic:
apply h
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
entry' : ℕ → ℕ → ℕ
h : entry' = (⇑T : (a : ℕ) → ℕ → ℕ)
⊢ (⇑(T.copy entry' h) : (a : ℕ) → ℕ → ℕ) = entry'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
entry' : ℕ → ℕ → ℕ
h : entry' = (⇑T : (a : ℕ) → ℕ → ℕ)
⊢ T.copy entry' h = T

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 < j2
hcell : (i, j2) ∈ μ
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)

Tactic:
T.row_weak' hj hcell

Premises used: SemistandardYoungTableau.row_weak'
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 < i2
hcell : (i2, j) ∈ μ
⊢ LT.lt (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)

Tactic:
T.col_strict' hi hcell

Premises used: SemistandardYoungTableau.col_strict'
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j : ℕ
not_cell : (i, j) ∉ μ
⊢ Eq (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j : ℕ) (0 : ℕ)

Tactic:
T.zeros' not_cell

Premises used: SemistandardYoungTableau.zeros'
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
inl : ∀ (h : j1 = j2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
inr : ∀ (h : j1 < j2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)

Tactic:
rcases eq_or_lt_of_le hj with h | h

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
inl inl₁ : LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)

Tactic:
T.row_weak h cell

Premises used: SemistandardYoungTableau.row_weak
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j1 : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i j2 : ℕ)

Tactic:
exact T.row_weak h cell

Premises used: SemistandardYoungTableau.row_weak
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
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 : ℕ)
inr : ∀ (h : i1 < i2), LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)

Tactic:
rcases eq_or_lt_of_le hi with h | h

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
inl inl₁ : LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)
⊢ LE.le (α := ℕ) ((T : (a : ℕ) → ℕ → ℕ) i1 j : ℕ) ((T : (a : ℕ) → ℕ → ℕ) i2 j : ℕ)

Tactic:
rw [h]
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
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 : ℕ)

Tactic:
le_of_lt (T.col_strict h cell)

Premises used: SemistandardYoungTableau.col_strict, le_of_lt
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
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 : ℕ)

Tactic:
exact le_of_lt (T.col_strict h cell)

Premises used: SemistandardYoungTableau.col_strict, le_of_lt
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
i j1 j2 : ℕ
hj : j1 < j2
hcell : (i, j2) ∈ μ
⊢ i ≤ i

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
i j1 j2 : ℕ
hj : j1 < j2
hcell : (i, j2) ∈ μ
rw : (if (i, j1) ∈ μ then i else 0) ≤ i
rw₁ rw₂ : i ≤ i
⊢ (if (i, j1) ∈ μ then i else 0) ≤ if (i, j2) ∈ μ then i else 0

Tactic:
rw [if_pos hcell, if_pos (μ.up_left_mem (by rfl) (le_of_lt hj) hcell)]

Premises used: le_of_lt, if_pos, YoungDiagram.up_left_mem
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
i1 i2 j : ℕ
hi : i1 < i2
hcell : (i2, j) ∈ μ
⊢ j ≤ j

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
i1 i2 j : ℕ
hi : i1 < i2
hcell : (i2, j) ∈ μ
rwa : (if (i1, j) ∈ μ then i1 else 0) < i2
rwa₁ rwa₂ rwa₃ rwa₄ : i1 < i2
⊢ (if (i1, j) ∈ μ then i1 else 0) < if (i2, j) ∈ μ then i2 else 0

Tactic:
rwa [if_pos hcell, if_pos (μ.up_left_mem (le_of_lt hi) (by rfl) hcell)]

Premises used: le_of_lt, if_pos, YoungDiagram.up_left_mem
-- Module: Mathlib.Combinatorics.Young.SemistandardTableau
Goal:
μ : YoungDiagram
i j : ℕ
⊢ (highestWeight μ : (a : ℕ) → ℕ → ℕ) i j = if (i, j) ∈ μ then i else 0

Tactic:
rfl

Premises used: rfl, ite
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h :
  Eq (α := Set (ℕ × ℕ)) ((fun (y : YoungDiagram) ↦ (↑y.cells : Set (ℕ × ℕ))) μ)
    ((fun (y : YoungDiagram) ↦ (↑y.cells : Set (ℕ × ℕ))) ν)
rwa : μ.cells = ν.cells
rwa₁ rwa₂ rwa₃ rwa₄ : (↑μ.cells : Set (ℕ × ℕ)) = (↑ν.cells : Set (ℕ × ℕ))
⊢ μ = ν

Tactic:
rwa [YoungDiagram.ext_iff, ← Finset.coe_inj]

Premises used: YoungDiagram.ext_iff, Finset.coe_inj
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
c : ℕ × ℕ
⊢ c ∈ μ.cells ↔ c ∈ μ

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
c : ℕ × ℕ
cells : Finset (ℕ × ℕ)
isLowerSet : IsLowerSet (↑cells : Set (ℕ × ℕ))
⊢ c ∈ { cells := cells, isLowerSet := isLowerSet : YoungDiagram } ↔ c ∈ cells

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i1 i2 j1 j2 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
hcell : (i2, j2) ∈ μ
⊢ (i1, j1) ∈ μ

Tactic:
μ.isLowerSet (Prod.mk_le_mk.mpr ⟨hi, hj⟩) hcell

Premises used: Iff.mpr, Set.Mem, YoungDiagram.isLowerSet, And.intro, Prod.mk_le_mk
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ μ.cells ⊆ ν.cells ↔ μ ≤ ν

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ μ.cells ⊂ ν.cells ↔ μ < ν

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Set.Subset
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
rw : IsLowerSet ((↑μ.cells : Set (ℕ × ℕ)) ∪ (↑ν.cells : Set (ℕ × ℕ)))
⊢ IsLowerSet (↑(μ.cells ∪ ν.cells) : Set (ℕ × ℕ))

Tactic:
rw [Finset.coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ IsLowerSet ((↑μ.cells : Set (ℕ × ℕ)) ∪ (↑ν.cells : Set (ℕ × ℕ)))

Tactic:
μ.isLowerSet.union ν.isLowerSet

Premises used: YoungDiagram.isLowerSet, IsLowerSet.union
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ IsLowerSet ((↑μ.cells : Set (ℕ × ℕ)) ∪ (↑ν.cells : Set (ℕ × ℕ)))

Tactic:
exact μ.isLowerSet.union ν.isLowerSet

Premises used: YoungDiagram.isLowerSet, IsLowerSet.union
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ (μ ⊔ ν).cells = μ.cells ∪ ν.cells

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ (↑(μ ⊔ ν) : Set (ℕ × ℕ)) = (↑μ : Set (ℕ × ℕ)) ∪ (↑ν : Set (ℕ × ℕ))

Tactic:
Finset.coe_union _ _

Premises used: setOf, Finset.coe_union
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ μ ⊔ ν ↔ x ∈ μ ∨ x ∈ ν

Tactic:
Finset.mem_union

Premises used: Set.Mem, setOf, Finset.mem_union
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
rw : IsLowerSet ((↑μ.cells : Set (ℕ × ℕ)) ∩ (↑ν.cells : Set (ℕ × ℕ)))
⊢ IsLowerSet (↑(μ.cells ∩ ν.cells) : Set (ℕ × ℕ))

Tactic:
rw [Finset.coe_inter]

Premises used: Finset.coe_inter
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ IsLowerSet ((↑μ.cells : Set (ℕ × ℕ)) ∩ (↑ν.cells : Set (ℕ × ℕ)))

Tactic:
μ.isLowerSet.inter ν.isLowerSet

Premises used: YoungDiagram.isLowerSet, IsLowerSet.inter
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ IsLowerSet ((↑μ.cells : Set (ℕ × ℕ)) ∩ (↑ν.cells : Set (ℕ × ℕ)))

Tactic:
exact μ.isLowerSet.inter ν.isLowerSet

Premises used: YoungDiagram.isLowerSet, IsLowerSet.inter
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ (μ ⊓ ν).cells = μ.cells ∩ ν.cells

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ (↑(μ ⊓ ν) : Set (ℕ × ℕ)) = (↑μ : Set (ℕ × ℕ)) ∩ (↑ν : Set (ℕ × ℕ))

Tactic:
Finset.coe_inter _ _

Premises used: setOf, Finset.coe_inter
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ μ ⊓ ν ↔ x ∈ μ ∧ x ∈ ν

Tactic:
Finset.mem_inter

Premises used: Set.Mem, setOf, Finset.mem_inter
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
a b : ℕ × ℕ
_ : b ≤ a → a ∈ (↑∅ : Set (ℕ × ℕ)) → b ∈ (↑∅ : Set (ℕ × ℕ))
⊢ b ≤ a → a ∈ (↑∅ : Set (ℕ × ℕ)) → b ∈ (↑∅ : Set (ℕ × ℕ))

Tactic:
_
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
a b : ℕ × ℕ
h_1 : b ≤ a
h : a ∈ (↑∅ : Set (ℕ × ℕ))
simp : False
⊢ b ∈ (↑∅ : Set (ℕ × ℕ))

Tactic:
simp only [Finset.coe_empty, Set.mem_empty_iff_false]

Premises used: Finset.coe_empty, Set.mem_empty_iff_false
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
a b : ℕ × ℕ
h_1 : b ≤ a
h : a ∈ (↑∅ : Set (ℕ × ℕ))
⊢ False

Tactic:
simp only [Finset.coe_empty, Set.mem_empty_iff_false] at h

Premises used: Finset.coe_empty, Set.mem_empty_iff_false
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
x : YoungDiagram
x_1 : ℕ × ℕ
y : x_1 ∈ { cells := ∅, isLowerSet := instOrderBot._proof_1 : YoungDiagram }
⊢ x_1 ∈ x

Tactic:
simp only [mem_mk, Finset.notMem_empty] at y

Premises used: Finset.notMem_empty, YoungDiagram.mem_mk
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
⊢ cells ⊥ = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
x : ℕ × ℕ
⊢ x ∉ ⊥

Tactic:
Finset.notMem_empty x

Premises used: Set.Mem, setOf, Finset.notMem_empty
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
h : ∀ (x : ℕ × ℕ), x ∈ (↑⊥ : Set (ℕ × ℕ)) ↔ Membership.mem (γ := Set (ℕ × ℕ)) ∅ x
⊢ (↑⊥ : Set (ℕ × ℕ)) = ∅

Tactic:
ext
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
x : ℕ × ℕ
⊢ x ∈ (↑⊥ : Set (ℕ × ℕ)) ↔ Membership.mem (γ := Set (ℕ × ℕ)) ∅ x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h rwa rwa₁ rwa₂ rwa₃ : μ.cells = ν.cells
⊢ μ = ν

Tactic:
rwa [YoungDiagram.ext_iff]

Premises used: YoungDiagram.ext_iff
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
x x_1 : ℕ × ℕ
h : x_1 ≤ x
simp :
  Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x : ℕ × ℕ) →
    Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x_1 : ℕ × ℕ)
⊢ x ∈
      (↑(((Equiv.prodComm ℕ ℕ).finsetCongr : (a : Finset (ℕ × ℕ)) → Finset (ℕ × ℕ)) μ.cells : Finset (ℕ × ℕ)) :
        Set (ℕ × ℕ)) →
    x_1 ∈
      (↑(((Equiv.prodComm ℕ ℕ).finsetCongr : (a : Finset (ℕ × ℕ)) → Finset (ℕ × ℕ)) μ.cells : Finset (ℕ × ℕ)) :
        Set (ℕ × ℕ))

Tactic:
simp only [Finset.mem_coe, Equiv.finsetCongr_apply, Finset.mem_map_equiv]

Premises used: Equiv.finsetCongr_apply, Finset.mem_map_equiv, Finset.mem_coe
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
x x_1 : ℕ × ℕ
h : x_1 ≤ x
hcell : Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x : ℕ × ℕ)
apply :
  LE.le (α := ℕ × ℕ) (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x_1 : ℕ × ℕ)
    (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x : ℕ × ℕ)
⊢ Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x_1 : ℕ × ℕ)

Tactic:
apply μ.isLowerSet _ hcell

Premises used: YoungDiagram.isLowerSet
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
x x_1 : ℕ × ℕ
h : x_1 ≤ x
hcell : Membership.mem (α := ℕ × ℕ) μ.cells (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x : ℕ × ℕ)
⊢ LE.le (α := ℕ × ℕ) (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x_1 : ℕ × ℕ)
    (((Equiv.prodComm ℕ ℕ).symm : (a : ℕ × ℕ) → ℕ × ℕ) x : ℕ × ℕ)

Tactic:
simp [h]
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
c : ℕ × ℕ
⊢ c ∈ μ.transpose ↔ c.swap ∈ μ

Tactic:
simp [transpose]

Premises used: YoungDiagram.transpose
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
cells : ∀ (x : ℕ × ℕ), x ∈ μ.transpose.transpose.cells ↔ x ∈ μ.cells
⊢ μ.transpose.transpose = μ

Tactic:
ext x
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
x : ℕ × ℕ
⊢ x ∈ μ.transpose.transpose.cells ↔ x ∈ μ.cells

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
mp : μ.transpose = ν → μ = ν.transpose
mpr : μ = ν.transpose → μ.transpose = ν
⊢ μ.transpose = ν ↔ μ = ν.transpose

Tactic:
constructor
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
⊢ μ = μ.transpose.transpose

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
ν : YoungDiagram
⊢ ν.transpose.transpose = ν

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
rw : μ = ν.transpose.transpose ↔ μ = ν
⊢ μ.transpose = ν.transpose ↔ μ = ν

Tactic:
rw [transpose_eq_iff_eq_transpose]

Premises used: YoungDiagram.transpose_eq_iff_eq_transpose
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
⊢ μ = ν.transpose.transpose ↔ μ = ν

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ
simp : c.swap ∈ ν
⊢ c ∈ ν.transpose

Tactic:
simp only [mem_transpose]

Premises used: YoungDiagram.mem_transpose
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ
a : c.swap ∈ μ.transpose
⊢ c.swap ∈ ν

Tactic:
apply h_le
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h_le : μ.transpose ≤ ν
c : ℕ × ℕ
hc : c ∈ μ
⊢ c.swap ∈ μ.transpose

Tactic:
simpa
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
⊢ μ ≤ ν.transpose.transpose

Tactic:
YoungDiagram.le_of_transpose_le h

Premises used: YoungDiagram.le_of_transpose_le
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
h₁ : ν = ν.transpose.transpose
⊢ μ ≤ ν

Tactic:
convert! YoungDiagram.le_of_transpose_le h

Premises used: YoungDiagram.le_of_transpose_le
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h : μ.transpose ≤ ν.transpose
⊢ ν = ν.transpose.transpose

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h : μ ≤ ν
⊢ μ.transpose.transpose ≤ ν

Tactic:
rw [← transpose_transpose μ] at h

Premises used: YoungDiagram.transpose_transpose
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h : μ.transpose.transpose ≤ ν
⊢ μ.transpose ≤ ν.transpose

Tactic:
YoungDiagram.le_of_transpose_le h

Premises used: YoungDiagram.le_of_transpose_le
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h : μ.transpose.transpose ≤ ν
⊢ μ.transpose ≤ ν.transpose

Tactic:
exact YoungDiagram.le_of_transpose_le h

Premises used: YoungDiagram.le_of_transpose_le
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ ν : YoungDiagram
h_le : μ ≤ ν
⊢ μ.transpose ≤ ν.transpose

Tactic:
transpose_le_iff.mpr h_le

Premises used: Iff.mpr, YoungDiagram.transpose_le_iff
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
x : YoungDiagram
⊢ x.transpose.transpose = x

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
⊢ ∀ {a b : YoungDiagram},
    LE.le (α := YoungDiagram)
        (({ toFun := transpose, invFun := transpose, left_inv := ⋯, right_inv := ⋯ : YoungDiagram ≃ YoungDiagram } :
              (a : YoungDiagram) → YoungDiagram)
            a :
          YoungDiagram)
        (({ toFun := transpose, invFun := transpose, left_inv := ⋯, right_inv := ⋯ : YoungDiagram ≃ YoungDiagram } :
              (a : YoungDiagram) → YoungDiagram)
            b :
          YoungDiagram) ↔
      a ≤ b

Tactic:
simp
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i : ℕ
c : ℕ × ℕ
⊢ c ∈ μ.row i ↔ c ∈ μ ∧ c.1 = i

Tactic:
simp [row]

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

Tactic:
simp [row]

Premises used: YoungDiagram.row
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
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)
refl : x ∈ Prod.mk i ⁻¹' (↑μ.cells : Set (ℕ × ℕ)) → x = x
⊢ x = x_1

Tactic:
cases h
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i x : ℕ
h h_1 : x ∈ Prod.mk i ⁻¹' (↑μ.cells : Set (ℕ × ℕ))
⊢ x = x

Tactic:
rfl
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i : ℕ
obtain : ∀ (j : ℕ) (hj : j ∉ μ.cells.preimage (Prod.mk i) ⋯), ∃ (j : ℕ), (i, j) ∉ μ
⊢ ∃ (j : ℕ), (i, j) ∉ μ

Tactic:
obtain ⟨j, hj⟩ :=
    Infinite.exists_notMem_finset
      (μ.cells.preimage (Prod.mk i) fun _ _ _ _ h => by
        cases h
        rfl)

Premises used: YoungDiagram.cells, Prod.mk, Infinite.exists_notMem_finset, Finset.preimage
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
hj : j ∉ μ.cells.preimage (Prod.mk i) ⋯
⊢ (i, j) ∉ μ.cells

Tactic:
rw [Finset.mem_preimage] at hj

Premises used: Finset.mem_preimage
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
hj : (i, j) ∉ μ.cells
⊢ ∃ (j : ℕ), (i, j) ∉ μ

Tactic:
⟨j, hj⟩

Premises used: Exists.intro
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
hj : (i, j) ∉ μ.cells
⊢ ∃ (j : ℕ), (i, j) ∉ μ

Tactic:
exact ⟨j, hj⟩
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
rw : (i, j) ∈ μ ↔ ∀ m ≤ j, ¬(i, m) ∉ μ
⊢ (i, j) ∈ μ ↔ j < μ.rowLen i

Tactic:
rw [rowLen, Nat.lt_find_iff]

Premises used: YoungDiagram.rowLen, Nat.lt_find_iff
-- Module: Mathlib.Combinatorics.Young.YoungDiagram
Goal:
μ : YoungDiagram
i j : ℕ
push : (i, j) ∈ μ ↔ ∀ m ≤ j, (i, m) ∈ μ
⊢ (i, j) ∈ μ ↔ ∀ m ≤ j, ¬(i, m) ∉ μ

Tactic:
push Not

Premises used: Not