awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithBot α
bot :
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ b
have bot₁ : ∀ (a : α),
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ (↑a : WithBot α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithBot α
a : α
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ b
have coe : Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
    (Sum.elim inr inl
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y))
    (Sum.elim inr inl
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)) ↔
  (↑a : WithBot α) ≤ ⊥
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithBot α
a : α
coe :
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ ⊥
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ b
have coe₁ : ∀ (a_1 : α),
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a_1 : WithBot α), inr PUnit.unit,
          inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ ⊥
have coe : ¬(↑a : WithBot α) ≤ ⊥
Tactic: simp only [elim_inl, elim_inr, lex_inr_inl, false_iff]
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithTop α
⊢ LE.le (α := _root_.Lex (α ⊕ PUnit))
      (((Equiv.optionEquivSumPUnit α).trans toLex : (a : WithTop α) → _root_.Lex (α ⊕ PUnit)) a :
        _root_.Lex (α ⊕ PUnit))
      (((Equiv.optionEquivSumPUnit α).trans toLex : (a : WithTop α) → _root_.Lex (α ⊕ PUnit)) b :
        _root_.Lex (α ⊕ PUnit)) ↔
    a ≤ b
have simp : Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
    (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
    | Option.some x, x_1, f => f x
    | none, y, x => y)
    (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
    | Option.some x, x_1, f => f x
    | none, y, x => y) ↔
  a ≤ b
Tactic: simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk,
      Lex.toLex_le_toLex, le_refl]
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithTop α
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    a ≤ b
have top : Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
    (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
    | Option.some x, x_1, f => f x
    | none, y, x => y)
    (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
    | Option.some x, x_1, f => f x
    | none, y, x => y) ↔
  ⊤ ≤ b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithTop α
top :
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ b
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    a ≤ b
have coe : ∀ (a : α),
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ b
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithTop α
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ b
have top : Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
    (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
    | Option.some x, x_1, f => f x
    | none, y, x => y)
    (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
    | Option.some x, x_1, f => f x
    | none, y, x => y) ↔
  LE.le.{u_1} (α := WithTop α) ⊤ ⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithTop α
top :
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ b
have top₁ : ∀ (a : α),
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ (↑a : WithTop α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithTop α
a : α
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ b
have coe : Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
    (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
    | Option.some x, x_1, f => f x
    | none, y, x => y)
    (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
    | Option.some x, x_1, f => f x
    | none, y, x => y) ↔
  (↑a : WithTop α) ≤ ⊤
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithTop α
a : α
coe :
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ ⊤
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ b
have coe₁ : ∀ (a_1 : α),
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a_1 : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Data.Sum.Order (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ (↑a : WithTop α)
have top : ¬⊤ ≤ (↑a : WithTop α)
Tactic: simp only [lex_inr_inl, false_iff]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a_1 b a : α
s : Sym α n
⊢ (a ::ₘ (↑s : Multiset α)).card = n.succ
have rw : (↑s : Multiset α).card + 1 = n.succ
Tactic: rw [Multiset.card_cons, s.2]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a_1 b a : α
s : Sym α n
rw : (↑s : Multiset α).card + 1 = n.succ
⊢ (a ::ₘ (↑s : Multiset α)).card = n.succ
have rw₁ : n + 1 = n.succ
Tactic: rw [Multiset.card_cons, s.2]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ ofVector (a ::ᵥ v) = a ::ₛ ofVector v
have mk : ∀ (val : List α) (property : val.length = n),
  Eq (α := Sym α n.succ) (ofVector (a ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
    (a ::ₛ ofVector (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property))
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ (↑(a ::ₛ ofVector v) : Multiset α) = (↑(ofVector (a ::ᵥ v)) : Multiset α)
have mk : ∀ (val : List α) (property : val.length = n),
  (↑(a ::ₛ ofVector (Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) : Multiset α) =
    (↑(ofVector (a ::ᵥ Subtype.mk (p := fun (l : List α) ↦ l.length = n) val property)) : Multiset α)
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
⊢ (m.erase a).card = n
have rw : m.card.pred = n
Tactic: rw [Multiset.card_erase_of_mem h, hc, Nat.add_one, Nat.pred_succ]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
rw : m.card.pred = n
⊢ (m.erase a).card = n
have rw₁ : (n + 1).pred = n
Tactic: rw [Multiset.card_erase_of_mem h, hc, Nat.add_one, Nat.pred_succ]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m_1 : ℕ
s : Sym α n
a_1 b : α
inst : DecidableEq α
m : Multiset α
hc : m.card = n + 1
a : α
h : a ∈ m
rw : m.card.pred = n
rw₁ : (n + 1).pred = n
rw₂ : n.succ.pred = n
⊢ (m.erase a).card = n
have rw₃ : n = n
Tactic: rw [Multiset.card_erase_of_mem h, hc, Nat.add_one, Nat.pred_succ]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_3
n : ℕ
a : α
s : Sym α n
⊢ Eq (α := Sym' α n.succ) (a :: (symEquivSym' : (a : Sym α n) → Sym' α n) s)
    ((symEquivSym' : (a : Sym α n.succ) → Sym' α n.succ) (a ::ₛ s))
have mk : ∀ (val : Multiset α) (l : List α)
  (property : Multiset.card (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l) = n),
  Eq (α := Sym' α n.succ)
    (a ::
      (symEquivSym' : (a : Sym α n) → Sym' α n)
        (Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)
          property))
    ((symEquivSym' : (a : Sym α n.succ) → Sym' α n.succ)
      (a ::ₛ
        Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) (Quot.mk (⇑(List.isSetoid α) : List α → List α → Prop) l)
          property))
Tactic: rcases s with ⟨⟨l⟩, _⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
⊢ (↑(replicate n a) : Multiset α) = Multiset.replicate n a
have rw : (↑(replicate n a) : Multiset α) = Multiset.replicate n a
Tactic: rw [val_eq_coe, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
a : α
rw : (↑(replicate n a) : Multiset α) = Multiset.replicate n a
⊢ (↑(replicate n a) : Multiset α) = Multiset.replicate n a
have rw₁ : Multiset.replicate n a = Multiset.replicate n a
Tactic: rw [val_eq_coe, coe_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ s = replicate n a ↔ ∀ b ∈ s, b = a
have rw : ((↑s : Multiset α).card = n ∧ ∀ b ∈ (↑s : Multiset α), b = a) ↔ ∀ b ∈ s, b = a
Tactic: rw [Subtype.ext_iff, val_replicate, Multiset.eq_replicate]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h : a ∈ s
⊢ ∃ (t : Sym α n), s = a ::ₛ t
have obtain : ∀ (m : Multiset α) (h : (↑s : Multiset α) = a ::ₘ m), ∃ (t : Sym α n), s = a ::ₛ t
Tactic: obtain ⟨m, h⟩ := Multiset.exists_cons_of_mem h
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (hypothesis)
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
⊢ m.card = n
have h₁ : (↑s : Multiset α).card = (a ::ₘ m).card
Tactic: apply_fun Multiset.card at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (hypothesis)
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α).card = (a ::ₘ m).card
⊢ m.card = n
have h₁ : n = m.card
Tactic: rw [s.2, Multiset.card_cons, add_left_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (hypothesis)
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
⊢ ∃ (t : Sym α n), s = a ::ₛ t
have this : m.card = n
Tactic: have : Multiset.card m = n := by
    apply_fun Multiset.card at h
    rw [s.2, Multiset.card_cons, add_left_inj] at h
    exact h.symm
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
this : m.card = n
⊢ ∃ (t : Sym α n), s = a ::ₛ t
have h₁ : s = a ::ₛ Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) m this
Tactic: use ⟨m, this⟩
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
s : Sym α (n + 1)
a : α
h_1 : a ∈ s
m : Multiset α
h : (↑s : Multiset α) = a ::ₘ m
this : m.card = n
⊢ s = a ::ₛ Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) m this
have h₁ : (↑s : Multiset α) = (↑(a ::ₛ Subtype.mk (p := fun (s : Multiset α) ↦ s.card = n) m this) : Multiset α)
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
n : ℕ
s : Sym α n.succ
⊢ ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'
have obtain : ∀ (a : α) (ha : a ∈ s), ∃ (a : α) (s' : Sym α n), s = a ::ₛ s'
Tactic: obtain ⟨a, ha⟩ := exists_mem s
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s : Sym α n_1
a b : α
inst : Subsingleton α
n : ℕ
⊢ ∀ (a b : Sym α n), a = b
have zero : ∀ (a b : Sym α 0), a = b
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s : Sym α n_1
a b : α
inst : Subsingleton α
n : ℕ
zero : ∀ (a b : Sym α 0), a = b
⊢ ∀ (a b : Sym α n), a = b
have succ : ∀ (n : ℕ) (a b : Sym α (n + 1)), a = b
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b : α
inst : Subsingleton α
n_1 : ℕ
s s' : Sym α (n_1 + 1)
⊢ s = s'
have succ : ∀ (b : α), s = s'
Tactic: obtain ⟨b, -⟩ := exists_mem s
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b_1 : α
inst : Subsingleton α
n_1 : ℕ
s s' : Sym α (n_1 + 1)
b : α
⊢ s = s'
have succ : s = replicate (n_1 + 1) b
Tactic: rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s_1 : Sym α n
a b_1 : α
inst : Subsingleton α
n_1 : ℕ
s s' : Sym α (n_1 + 1)
b : α
succ : s = replicate (n_1 + 1) b
⊢ s = s'
have succ₁ : Eq (α := Sym α (n_1 + 1)) (replicate (n_1 + 1) b) (replicate (n_1 + 1) b)
Tactic: rw [eq_replicate_of_subsingleton b s', eq_replicate_of_subsingleton b s]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n_1 n' m : ℕ
s_1 : Sym α n_1
a b : α
n : ℕ
inst : IsEmpty α
s : Sym α n.succ
⊢ False
have obtain : ∀ (a : α), False
Tactic: obtain ⟨a, -⟩ := exists_mem s
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_3
n : ℕ
s : Sym α n
⊢ map (fun (x : α) ↦ x) s = s
have h : (↑(map (fun (x : α) ↦ x) s) : Multiset α) = (↑s : Multiset α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_3
n : ℕ
s : Sym α n
⊢ map id s = s
have h : (↑(map id s) : Multiset α) = (↑s : Multiset α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ (↑(map g (map f s)) : Multiset γ) = (↑(map (g ∘ f) s) : Multiset γ)
have dsimp : Multiset.map g (Multiset.map f (↑s : Multiset α)) = Multiset.map (g ∘ f) (↑s : Multiset α)
Tactic: dsimp only [Sym.map]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym α n
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) x) = x
have rw : map (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) x = x
Tactic: rw [map_map, Equiv.symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Data.Sym.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
n n' m : ℕ
s : Sym α n
a b : α
e : α ≃ β
x : Sym α n
rw : map (comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) x = x
⊢ map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (map (⇑e : (a : α) → β) x) = x
have rw₁ : map id x = x
Tactic: rw [map_map, Equiv.symm_comp_self, map_id]