awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
p : l₁ ~ l₂
l : List (Sigma β)
nil : ∀ (l : List (Sigma β)), kunion (β := β) [] l ~ kunion (β := β) [] l
cons :
  ∀ (hd : Sigma β) {l₁ l₂ : List (Sigma β)},
    l₁ ~ l₂ →
      ∀ (ih : ∀ (l : List (Sigma β)), l₁.kunion (β := β) l ~ l₂.kunion (β := β) l) (l : List (Sigma β)),
        (hd :: l₁).kunion (β := β) l ~ (hd :: l₂).kunion (β := β) l
swap :
  ∀ (s₁ s₂ : Sigma β) (l : List (Sigma β)) (l_1 : List (Sigma β)),
    (s₂ :: s₁ :: l).kunion (β := β) l_1 ~ (s₁ :: s₂ :: l).kunion (β := β) l_1
⊢ l₁.kunion (β := β) l ~ l₂.kunion (β := β) l
have trans : ∀ {l₁ l₂ l₃ : List (Sigma β)},
  l₁ ~ l₂ →
    l₂ ~ l₃ →
      ∀ (ih₁₂ : ∀ (l : List (Sigma β)), l₁.kunion (β := β) l ~ l₂.kunion (β := β) l)
        (ih₂₃ : ∀ (l : List (Sigma β)), l₂.kunion (β := β) l ~ l₃.kunion (β := β) l) (l : List (Sigma β)),
        l₁.kunion (β := β) l ~ l₃.kunion (β := β) l
Tactic: induction p generalizing l with
  | nil => rfl
  | cons hd _ ih =>
    simp [ih (List.kerase _ _)]
  | swap s₁ s₂ l => simp [kerase_comm, Perm.swap]
  | trans _ _ ih₁₂ ih₂₃ => exact Perm.trans (ih₁₂ l) (ih₂₃ l)
Cleared hypotheses: p, l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ (s :: tail).keys (β := β)
⊢ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)
have h₁ : a = s.fst (β := β) ∨ a ∈ tail.keys (β := β)
Tactic: simp only [keys_cons, mem_cons] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a = s.fst (β := β) ∨ a ∈ tail.keys (β := β)
⊢ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)
have cons : ∀
  (ih :
    ∀ {l₂ : List (Sigma β)} (h : s.fst (β := β) ∈ tail.keys (β := β)),
      dlookup (β := β) (s.fst (β := β)) (tail.kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) tail),
  dlookup (β := β) (s.fst (β := β)) ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) (s :: tail)
Tactic: rcases h with rfl | h
Cleared hypotheses: a, ih, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a = s.fst (β := β) ∨ a ∈ tail.keys (β := β)
cons :
  ∀
    (ih :
      ∀ {l₂ : List (Sigma β)} (h : s.fst (β := β) ∈ tail.keys (β := β)),
        dlookup (β := β) (s.fst (β := β)) (tail.kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) tail),
    dlookup (β := β) (s.fst (β := β)) ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) (s :: tail)
⊢ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)
have cons₁ : ∀ (h : a ∈ tail.keys (β := β)), dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)
Tactic: rcases h with rfl | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Sigma β
tail : List (Sigma β)
l₂ : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : s.fst (β := β) ∈ tail.keys (β := β)),
    dlookup (β := β) (s.fst (β := β)) (tail.kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) tail
⊢ dlookup (β := β) (s.fst (β := β)) ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) (s.fst (β := β)) (s :: tail)
have cons : ∀ (a' : α) (snd : β a')
  (ih :
    ∀ {l₂ : List (Sigma β)} (h : (Sigma.mk (β := β) a' snd).fst (β := β) ∈ tail.keys (β := β)),
      dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) (tail.kunion (β := β) l₂) =
        dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) tail),
  dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) =
    dlookup (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) (Sigma.mk (β := β) a' snd :: tail)
Tactic: obtain ⟨a'⟩ := s
Cleared hypotheses: s, ih
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
⊢ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)
have cons : ∀ (a' : α) (snd : β a'),
  dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
Tactic: obtain ⟨a'⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
a' : α
snd : β a'
⊢ dlookup (β := β) a
      (Sigma.mk (β := β) a' snd ::
        tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
have pos : ∀ (h' : a = a'),
  dlookup (β := β) a
      (Sigma.mk (β := β) a' snd ::
        tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
Tactic: by_cases h' : a = a'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
a' : α
snd : β a'
pos :
  ∀ (h' : a = a'),
    dlookup (β := β) a
        (Sigma.mk (β := β) a' snd ::
          tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
      dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
⊢ dlookup (β := β) a
      (Sigma.mk (β := β) a' snd ::
        tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
have neg : ∀ (h' : ¬a = a'),
  dlookup (β := β) a
      (Sigma.mk (β := β) a' snd ::
        tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
Tactic: by_cases h' : a = a'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
    dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail
l₂ : List (Sigma β)
h : a ∈ tail.keys (β := β)
a' : α
snd : β a'
h' : a = a'
⊢ dlookup (β := β) a
      (Sigma.mk (β := β) a' snd ::
        tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a' snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail)
have pos : ∀ (snd : β a),
  dlookup (β := β) a
      (Sigma.mk (β := β) a snd :: tail.kunion (β := β) (kerase (β := β) ((Sigma.mk (β := β) a snd).fst (β := β)) l₂)) =
    dlookup (β := β) a (Sigma.mk (β := β) a snd :: tail)
Tactic: subst h'
Cleared hypotheses: a', snd, h'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : a ∈ l₁.keys (β := β)
⊢ dlookup (β := β) a (l₁.kunion (β := β) l₂) = dlookup (β := β) a l₁
have nil : ∀ {l₂ : List (Sigma β)} (h : Membership.mem (γ := List α) (keys (β := β) []) a),
  dlookup (β := β) a (kunion (β := β) [] l₂) = dlookup (β := β) a []
Tactic: induction l₁ generalizing l₂ with
  | nil => simp at h
  | cons s _ ih =>
    simp only [keys_cons, mem_cons] at h
    rcases h with rfl | h <;> obtain ⟨a'⟩ := s
    · simp
    · rw [kunion_cons]
      by_cases h' : a = a'
      · subst h'
        simp
      · simp [h', ih h]
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : a ∈ l₁.keys (β := β)
nil :
  ∀ {l₂ : List (Sigma β)} (h : Membership.mem (γ := List α) (keys (β := β) []) a),
    dlookup (β := β) a (kunion (β := β) [] l₂) = dlookup (β := β) a []
⊢ dlookup (β := β) a (l₁.kunion (β := β) l₂) = dlookup (β := β) a l₁
have cons : ∀ (s : Sigma β) (tail : List (Sigma β))
  (ih :
    ∀ {l₂ : List (Sigma β)} (h : a ∈ tail.keys (β := β)),
      dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a tail)
  {l₂ : List (Sigma β)} (h : a ∈ (s :: tail).keys (β := β)),
  dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) = dlookup (β := β) a (s :: tail)
Tactic: induction l₁ generalizing l₂ with
  | nil => simp at h
  | cons s _ ih =>
    simp only [keys_cons, mem_cons] at h
    rcases h with rfl | h <;> obtain ⟨a'⟩ := s
    · simp
    · rw [kunion_cons]
      by_cases h' : a = a'
      · subst h'
        simp
      · simp [h', ih h]
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : ¬a ∈ l₁.keys (β := β)
⊢ dlookup (β := β) a (l₁.kunion (β := β) l₂) = dlookup (β := β) a l₂
have nil : ∀ {l₂ : List (Sigma β)} (h : ¬Membership.mem (γ := List α) (keys (β := β) []) a),
  dlookup (β := β) a (kunion (β := β) [] l₂) = dlookup (β := β) a l₂
Tactic: induction l₁ generalizing l₂ with
  | nil => simp
  | cons _ _ ih => simp_all [not_or]
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
h : ¬a ∈ l₁.keys (β := β)
nil :
  ∀ {l₂ : List (Sigma β)} (h : ¬Membership.mem (γ := List α) (keys (β := β) []) a),
    dlookup (β := β) a (kunion (β := β) [] l₂) = dlookup (β := β) a l₂
⊢ dlookup (β := β) a (l₁.kunion (β := β) l₂) = dlookup (β := β) a l₂
have cons : ∀ (head : Sigma β) (tail : List (Sigma β))
  (ih :
    ∀ {l₂ : List (Sigma β)} (h : ¬a ∈ tail.keys (β := β)),
      dlookup (β := β) a (tail.kunion (β := β) l₂) = dlookup (β := β) a l₂)
  {l₂ : List (Sigma β)} (h : ¬a ∈ (head :: tail).keys (β := β)),
  dlookup (β := β) a ((head :: tail).kunion (β := β) l₂) = dlookup (β := β) a l₂
Tactic: induction l₁ generalizing l₂ with
  | nil => simp
  | cons _ _ ih => simp_all [not_or]
Cleared hypotheses: l₁, l₂, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Sigma β
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
⊢ b ∈ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (s :: tail) ∨ ¬a ∈ (s :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
have cons : ∀ (a' : α) (snd : β a'),
  b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
Tactic: obtain ⟨a'⟩ := s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
a' : α
snd : β a'
⊢ b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
have pos : ∀ (h₁ : a = a'),
  b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
Tactic: by_cases h₁ : a = a'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
a' : α
snd : β a'
pos :
  ∀ (h₁ : a = a'),
    b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
        ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
⊢ b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
have neg : ∀ (h₁ : ¬a = a'),
  b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
Tactic: by_cases h₁ : a = a'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
tail : List (Sigma β)
ih :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
      b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
l₂ : List (Sigma β)
a' : α
snd : β a'
h₁ : a = a'
⊢ b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a' snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a' snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a' snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
have pos : ∀ (snd : β a),
  b ∈ dlookup (β := β) a ((Sigma.mk (β := β) a snd :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (Sigma.mk (β := β) a snd :: tail) ∨
      ¬a ∈ (Sigma.mk (β := β) a snd :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
Tactic: subst h₁
Cleared hypotheses: a', snd, h₁
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
⊢ b ∈ dlookup (β := β) a (l₁.kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a l₁ ∨ ¬a ∈ l₁.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
have nil : ∀ {l₂ : List (Sigma β)},
  b ∈ dlookup (β := β) a (kunion (β := β) [] l₂) ↔
    Membership.mem (γ := Option (β a)) (dlookup (β := β) a []) b ∨
      ¬Membership.mem (γ := List α) (keys (β := β) []) a ∧ b ∈ dlookup (β := β) a l₂
Tactic: induction l₁ generalizing l₂ with
  | nil => simp
  | cons s _ ih =>
    obtain ⟨a'⟩ := s
    by_cases h₁ : a = a'
    · subst h₁
      simp
    · simp [h₁, @ih (kerase a' l₂)]
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nil :
  ∀ {l₂ : List (Sigma β)},
    b ∈ dlookup (β := β) a (kunion (β := β) [] l₂) ↔
      Membership.mem (γ := Option (β a)) (dlookup (β := β) a []) b ∨
        ¬Membership.mem (γ := List α) (keys (β := β) []) a ∧ b ∈ dlookup (β := β) a l₂
⊢ b ∈ dlookup (β := β) a (l₁.kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a l₁ ∨ ¬a ∈ l₁.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
have cons : ∀ (s : Sigma β) (tail : List (Sigma β))
  (ih :
    ∀ {l₂ : List (Sigma β)},
      b ∈ dlookup (β := β) a (tail.kunion (β := β) l₂) ↔
        b ∈ dlookup (β := β) a tail ∨ ¬a ∈ tail.keys (β := β) ∧ b ∈ dlookup (β := β) a l₂)
  {l₂ : List (Sigma β)},
  b ∈ dlookup (β := β) a ((s :: tail).kunion (β := β) l₂) ↔
    b ∈ dlookup (β := β) a (s :: tail) ∨ ¬a ∈ (s :: tail).keys (β := β) ∧ b ∈ dlookup (β := β) a l₂
Tactic: induction l₁ generalizing l₂ with
  | nil => simp
  | cons s _ ih =>
    obtain ⟨a'⟩ := s
    by_cases h₁ : a = a'
    · subst h₁
      simp
    · simp [h₁, @ih (kerase a' l₂)]
Cleared hypotheses: l₁, l₂
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
L : List α
a : α
⊢ (orderedInsert r a L).length = L.length + 1
have nil : (orderedInsert r a []).length = length.{u_1} (α := α) [] + 1
Tactic: induction L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
L : List α
a : α
nil : (orderedInsert r a []).length = length.{u_1} (α := α) [] + 1
⊢ (orderedInsert r a L).length = L.length + 1
have cons : ∀ (head : α) (tail : List α),
  (orderedInsert r a tail).length = tail.length + 1 →
    (orderedInsert r a (head :: tail)).length = (head :: tail).length + 1
Tactic: induction L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
⊢ orderedInsert r a l = takeWhile (fun (b : α) ↦ decide ¬r a b) l ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) l
have nil : orderedInsert r a [] = takeWhile (fun (b : α) ↦ decide ¬r a b) [] ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
nil :
  orderedInsert r a [] = takeWhile (fun (b : α) ↦ decide ¬r a b) [] ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) []
⊢ orderedInsert r a l = takeWhile (fun (b : α) ↦ decide ¬r a b) l ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) l
have cons : ∀ (head : α) (tail : List α),
  orderedInsert r a tail =
      takeWhile (fun (b : α) ↦ decide ¬r a b) tail ++ a :: dropWhile (fun (b : α) ↦ decide ¬r a b) tail →
    orderedInsert r a (head :: tail) =
      takeWhile (fun (b : α) ↦ decide ¬r a b) (head :: tail) ++
        a :: dropWhile (fun (b : α) ↦ decide ¬r a b) (head :: tail)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
⊢ a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l
have nil : a ∈ orderedInsert r b [] ↔ a = b ∨ Membership.mem (γ := List α) [] a
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
nil : a ∈ orderedInsert r b [] ↔ a = b ∨ Membership.mem (γ := List α) [] a
⊢ a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l
have cons : ∀ (head : α) (tail : List α),
  (a ∈ orderedInsert r b tail ↔ a = b ∨ a ∈ tail) → (a ∈ orderedInsert r b (head :: tail) ↔ a = b ∨ a ∈ head :: tail)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
l : List α
x : α
hl₁ : ∀ (a : α), a ∈ l → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ l → (r x a ↔ s (f x) (f a))
⊢ map f (orderedInsert r x l) = orderedInsert s (f x) (map f l)
have nil : ∀ (hl₁ : ∀ (a : α), Membership.mem (γ := List α) [] a → (r a x ↔ s (f a) (f x)))
  (hl₂ : ∀ (a : α), Membership.mem (γ := List α) [] a → (r x a ↔ s (f x) (f a))),
  map f (orderedInsert r x []) = orderedInsert s (f x) (map f [])
Tactic: induction l
Cleared hypotheses: l, hl₁, hl₂
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : DecidableRel r
inst_1 : DecidableRel s
f : α → β
l : List α
x : α
hl₁ : ∀ (a : α), a ∈ l → (r a x ↔ s (f a) (f x))
hl₂ : ∀ (a : α), a ∈ l → (r x a ↔ s (f x) (f a))
nil :
  ∀ (hl₁ : ∀ (a : α), Membership.mem (γ := List α) [] a → (r a x ↔ s (f a) (f x)))
    (hl₂ : ∀ (a : α), Membership.mem (γ := List α) [] a → (r x a ↔ s (f x) (f a))),
    map f (orderedInsert r x []) = orderedInsert s (f x) (map f [])
⊢ map f (orderedInsert r x l) = orderedInsert s (f x) (map f l)
have cons : ∀ (head : α) (tail : List α),
  (∀ (hl₁ : ∀ (a : α), a ∈ tail → (r a x ↔ s (f a) (f x))) (hl₂ : ∀ (a : α), a ∈ tail → (r x a ↔ s (f x) (f a))),
      map f (orderedInsert r x tail) = orderedInsert s (f x) (map f tail)) →
    ∀ (hl₁ : ∀ (a : α), a ∈ head :: tail → (r a x ↔ s (f a) (f x)))
      (hl₂ : ∀ (a : α), a ∈ head :: tail → (r x a ↔ s (f x) (f a))),
      map f (orderedInsert r x (head :: tail)) = orderedInsert s (f x) (map f (head :: tail))
Tactic: induction l
Cleared hypotheses: l, hl₁, hl₂
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
⊢ orderedInsert r a (b :: l) ~ a :: b :: l
have pos : ∀ (h : r a b), orderedInsert r a (b :: l) ~ a :: b :: l
Tactic: by_cases h : a ≼ b
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a b : α
l : List α
pos : ∀ (h : r a b), orderedInsert r a (b :: l) ~ a :: b :: l
⊢ orderedInsert r a (b :: l) ~ a :: b :: l
have neg : ∀ (h : ¬r a b), orderedInsert r a (b :: l) ~ a :: b :: l
Tactic: by_cases h : a ≼ b
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
inst_1 : DecidableEq α
L : List α
a b : α
⊢ count a (orderedInsert r b L) = count a L + if b = a then 1 else 0
have rw : (count a L + if (b == a) = true then 1 else 0) = count a L + if b = a then 1 else 0
Tactic: rw [(L.perm_orderedInsert r b).count_eq, count_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
⊢ insertionSort r l ~ l
have nil : insertionSort r [] ~ []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
l : List α
nil : insertionSort r [] ~ []
⊢ insertionSort r l ~ l
have cons : ∀ (head : α) (tail : List α), insertionSort r tail ~ tail → insertionSort r (head :: tail) ~ head :: tail
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ insertionSort r (a :: l) = a :: insertionSort r l
have rw : orderedInsert r a (insertionSort r l) = a :: insertionSort r l
Tactic: rw [insertionSort_cons]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ orderedInsert r a (b :: m) = a :: b :: m
have cons : r a b
Tactic: rw [orderedInsert_cons_of_le]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ r a b
have apply : b ∈ insertionSort r l
Tactic: apply h b <| (mem_insertionSort r).1 _
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
b : α
m : List α
hi : insertionSort r l = b :: m
⊢ b ∈ insertionSort r l
have rw : b ∈ b :: m
Tactic: rw [hi]
-- Lean 4 proof step from Mathlib.Data.List.Sort (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : DecidableRel r
a : α
l : List α
h : ∀ (b : α), b ∈ l → r a b
⊢ orderedInsert r a (insertionSort r l) = a :: insertionSort r l
have cases : ∀ (x : List α) (hi : insertionSort r l = x), orderedInsert r a x = a :: x
Tactic: cases hi : insertionSort r l with
  | nil => rfl
  | cons b m =>
    rw [orderedInsert_cons_of_le]
    apply h b <| (mem_insertionSort r).1 _
    rw [hi]
    exact mem_cons_self