mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2.groupElts
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ }.groupElts ≍ { index := i₁, groupElts := g₂ }.groupElts

Tactic:
·

Goal state after:
case refine_2.groupElts
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
i₁ : ιₚ
g₁ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₁ : ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts
g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
hg₂ : ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    ∃ g, ⟦g⟧ = { index := i₁, groupElts := g₁ }.groupElts ∧ ⟦g⟧ = { index := i₁, groupElts := g₂ }.groupElts
⊢ { index := i₁, groupElts := g₁ }.groupElts ≍ { index := i₁, groupElts := g₂ }.groupElts
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ : YoungDiagram
i j : ℕ
⊢ (i, j) ∈ μ ↔ i < μ.colLen j

Tactic:
by
  rw [← rowLen_transpose, ← mem_iff_lt_rowLen]
  simp

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
h : pt₁ = pt₂
⊢ pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}

pp: case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
x✝ :
  pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}
hi : pt₁.index = pt₂.index
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
      {pt₁.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
      {pt₂.groupElts}
⊢ pt₁ = pt₂

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
h : pt₁ = pt₂
⊢ pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
x✝ :
  pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}
hi : pt₁.index = pt₂.index
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
      {pt₁.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
      {pt₂.groupElts}
⊢ pt₁ = pt₂

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
pt₁ pt₂ : PlacedTile ps
x✝ :
  pt₁.index = pt₂.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
        {pt₁.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
        {pt₂.groupElts}
hi : pt₁.index = pt₂.index
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₁.index)).subtype (↑ps pt₁.index).symmetries)) ⁻¹'
      {pt₁.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps pt₂.index)).subtype (↑ps pt₂.index).symmetries)) ⁻¹'
      {pt₂.groupElts}
⊢ pt₁ = pt₂
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: case refine_2.groupElts
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
i₁ : ιₚ
g₁ g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₂ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₂ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₂ }.groupElts}
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₂ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₂ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₂ }.groupElts}
⊢ { index := i₁, groupElts := g₁ }.groupElts ≍ { index := i₁, groupElts := g₂ }.groupElts

Tactic:
·

Goal state after:
case refine_2.groupElts
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
i₁ : ιₚ
g₁ g₂ : G ⧸ Subgroup.map (MulAction.stabilizer G ↑(↑ps i₁)).subtype (↑ps i₁).symmetries
x✝ :
  { index := i₁, groupElts := g₁ }.index = { index := i₁, groupElts := g₂ }.index ∧
    Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₁ }.groupElts} =
      Quotient.mk
          (QuotientGroup.leftRel
            (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₂ }.index)).subtype
              (↑ps { index := i₁, groupElts := g₂ }.index).symmetries)) ⁻¹'
        {{ index := i₁, groupElts := g₂ }.groupElts}
hq :
  Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₁ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₁ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₁ }.groupElts} =
    Quotient.mk
        (QuotientGroup.leftRel
          (Subgroup.map (MulAction.stabilizer G ↑(↑ps { index := i₁, groupElts := g₂ }.index)).subtype
            (↑ps { index := i₁, groupElts := g₂ }.index).symmetries)) ⁻¹'
      {{ index := i₁, groupElts := g₂ }.groupElts}
⊢ { index := i₁, groupElts := g₁ }.groupElts ≍ { index := i₁, groupElts := g₂ }.groupElts
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∉ (cycles.connectedComponentMk c).supp
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

pp: case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c

Tactic:
·

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∉ (cycles.connectedComponentMk c).supp
⊢ ∃ G', G'.IsAlternating M2.spanningCoe ∧ G'.IsCycles ∧ ¬G'.Adj x b ∧ G'.Adj a c ∧ G' ≤ G ⊔ edge a c
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case nil
c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]

pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈
      {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 < (head✝ :: tail✝)[c.1]

Tactic:
·

Goal state after:
case nil
c : ℕ × ℕ
⊢ c ∈ ∅ ↔ ∃ (h : c.1 < [].length), c.2 < [][c.1]
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈
      {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 < (head✝ :: tail✝)[c.1]

Tactic:
·

Goal state after:
case cons
head✝ : ℕ
tail✝ : List ℕ
tail_ih✝ : ∀ {c : ℕ × ℕ}, c ∈ YoungDiagram.cellsOfRowLens tail✝ ↔ ∃ (h : c.1 < tail✝.length), c.2 < tail✝[c.1]
c : ℕ × ℕ
⊢ c ∈
      {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 < (head✝ :: tail✝)[c.1]
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
pt : PlacedTile ps
⊢ (g • pt).index = pt.index

Tactic:
induction pt using PlacedTile.induction_on
  rfl

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ g • x ∈ g • pt ↔ x ∈ pt

Tactic:
← mem_coe,

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ g • x ∈ ↑(g • pt) ↔ x ∈ pt
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ g • pt ↔ g⁻¹ • x ∈ pt

Tactic:
← mem_coe,

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ ↑(g • pt) ↔ g⁻¹ • x ∈ ↑pt
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ g⁻¹ • pt ↔ g • x ∈ pt

Tactic:
← mem_coe,

Goal state after:
G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
g : G
x : X
pt : PlacedTile ps
⊢ x ∈ ↑(g⁻¹ • pt) ↔ g • x ∈ ↑pt
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: case inl
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ T i j1 ≤ T i j2

pp: case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ T i j1 ≤ T i j2

Tactic:
·

Goal state after:
case inl
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 = j2
⊢ T i j1 ≤ T i j2
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ T i j1 ≤ T i j2

Tactic:
·

Goal state after:
case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i j1 j2 : ℕ
hj : j1 ≤ j2
cell : (i, j2) ∈ μ
h : j1 < j2
⊢ T i j1 ≤ T i j2
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: case inl
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ T i1 j ≤ T i2 j

pp: case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ T i1 j ≤ T i2 j

Tactic:
·

Goal state after:
case inl
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 = i2
⊢ T i1 j ≤ T i2 j
Module: Mathlib.Combinatorics.Young.SemistandardTableau

Goal state before:
pp: case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ T i1 j ≤ T i2 j

Tactic:
·

Goal state after:
case inr
μ : YoungDiagram
T : SemistandardYoungTableau μ
i1 i2 j : ℕ
hi : i1 ≤ i2
cell : (i2, j) ∈ μ
h : i1 < i2
⊢ T i1 j ≤ T i2 j
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case inl
w : List ℕ
hw : w.SortedGE
j2 i1 j1 : ℕ
hj : j1 ≤ j2
hi : i1 ≤ i1
h1 : (i1, j2).1 < w.length
h2 : (i1, j2).2 < w[(i1, j2).1]
⊢ w[i1] ≤ w[i1]

pp: case inr
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 < w[(i2, j2).1]
h : i1 < i2
⊢ w[i2] ≤ w[i1]

Tactic:
·

Goal state after:
case inl
w : List ℕ
hw : w.SortedGE
j2 i1 j1 : ℕ
hj : j1 ≤ j2
hi : i1 ≤ i1
h1 : (i1, j2).1 < w.length
h2 : (i1, j2).2 < w[(i1, j2).1]
⊢ w[i1] ≤ w[i1]
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: case inr
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 < w[(i2, j2).1]
h : i1 < i2
⊢ w[i2] ≤ w[i1]

Tactic:
·

Goal state after:
case inr
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 < w[(i2, j2).1]
h : i1 < i2
⊢ w[i2] ≤ w[i1]
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case none
m n : ℕ
s : m.psub n = none
⊢ none = none ↔ m < n

pp: case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ some val✝ = none ↔ m < n

Tactic:
·

Goal state after:
case none
m n : ℕ
s : m.psub n = none
⊢ none = none ↔ m < n
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ some val✝ = none ↔ m < n

Tactic:
·

Goal state after:
case some
m n val✝ : ℕ
s : m.psub n = some val✝
⊢ some val✝ = none ↔ m < n
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case pos
m n : ℕ
h : n ≤ m
⊢ some (m - n) = m.psub n

pp: case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n

Tactic:
·

Goal state after:
case pos
m n : ℕ
h : n ≤ m
⊢ some (m - n) = m.psub n
Module: Mathlib.Data.Nat.PSub

Goal state before:
pp: case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n

Tactic:
·

Goal state after:
case neg
m n : ℕ
h : ¬n ≤ m
⊢ none = m.psub n
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) none)

Tactic:
simp [encodek]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β → σ
g : α → β
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦ encode (Option.map f (decode (encode (Option.map g (decode n))).pred))) =
    encode (Option.map (fun a ↦ f (g a)) (some val✝))

Tactic:
simp [encodek]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ (Nat.pair n_1 n).succ) (encode (decode (Nat.unpair n).2)))
      (encode none) =
    encode (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))

pp: case some
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
val✝ : α
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ (Nat.pair n_1 n).succ) (encode (decode (Nat.unpair n).2)))
      (encode (some val✝)) =
    encode ((some val✝).bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))

Tactic:
·

Goal state after:
case none
α : Type ?u.4
β : Type ?u.6
inst✝¹ : Primcodable α
inst✝ : Primcodable β
n : ℕ
⊢ Nat.rec 0 (fun n_1 n_ih ↦ Nat.rec 0 (fun n n_ih ↦ (Nat.pair n_1 n).succ) (encode (decode (Nat.unpair n).2)))
      (encode none) =
    encode (none.bind fun a ↦ Option.map (Prod.mk a) (decode (Nat.unpair n).2))
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case none
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
⊢ (Nat.casesOn (encode none) 0 fun n ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a ↦ (f a, g a)) none)

Tactic:
simp [encodek]

Goal state after:
Module: Mathlib.Computability.Primrec.Basic

Goal state before:
pp: case some
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable γ
f : α → β
g : α → γ
hf : Primrec f
hg : Primrec g
n : ℕ
val✝ : α
⊢ (Nat.casesOn (encode (some val✝)) 0 fun n ↦
      (Nat.pair (encode (Option.map f (decode n))).pred (encode (Option.map g (decode n))).pred).succ) =
    encode (Option.map (fun a ↦ (f a, g a)) (some val✝))

Tactic:
simp [encodek]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode [])) =
    some (List.casesOn [] (g a) fun b l ↦ h a (b, l))

Tactic:
simp [encodek]

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
H : Nat.Primrec fun n ↦ encode (decode n)
f : α → List β
g : α → σ
h : α → β × List β → σ
hf : Primrec f
hg : Primrec g
hh : Primrec₂ h
this✝ : Primcodable (List β) := prim H
this : Primrec fun a ↦ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (f a)))
a : α
b : β
l : List β
⊢ Option.map (fun o ↦ Option.casesOn o (g a) (h a)) (decode (encode (b :: l))) =
    some (List.casesOn (b :: l) (g a) fun b l ↦ h a (b, l))

Tactic:
simp [encodek]

Goal state after: