awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a xa : α
h : ∀ (y : α), r y xa → Acc r y
iha :
  ∀ (y : α),
    r y xa →
      ∀ {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (y :: b)
b : List α
acb : Acc (Shortlex r) b
ih : ∀ (s : List α), s.length < (xa :: b).length → Acc (Shortlex r) s
intro :
  ∀ (xb : List α),
    (∀ (y : List α), Shortlex r y xb → Acc (Shortlex r) y) →
      ∀
        (ihb :
          ∀ (y : List α),
            Shortlex r y xb →
              ∀ (ih : ∀ (s : List α), s.length < (xa :: y).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: y))
        (ih : ∀ (s : List α), s.length < (xa :: xb).length → Acc (Shortlex r) s), Acc (Shortlex r) (xa :: xb)
⊢ Acc (Shortlex r) (xa :: b)

Tactic:
induction acb with
    | intro xb _ ihb =>
      refine Acc.intro (xa :: xb) fun p lt => ?_
      rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩
      · exact ih _ h1
      · cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

Premises used: List.length_cons, add_left_inj, List.Shortlex.cons, List.nil
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
a : α
b : List α
aca : Acc r a
acb : Acc (Shortlex r) b
ih : ∀ (s : List α), s.length < (a :: b).length → Acc (Shortlex r) s
intro :
  ∀ (xa : α),
    (∀ (y : α), r y xa → Acc r y) →
      ∀
        (iha :
          ∀ (y : α),
            r y xa →
              ∀ {b : List α} (acb : Acc (Shortlex r) b)
                (ih : ∀ (s : List α), s.length < (y :: b).length → Acc (Shortlex r) s), Acc (Shortlex r) (y :: b))
        {b : List α} (acb : Acc (Shortlex r) b) (ih : ∀ (s : List α), s.length < (xa :: b).length → Acc (Shortlex r) s),
        Acc (Shortlex r) (xa :: b)
⊢ Acc (Shortlex r) (a :: b)

Tactic:
induction aca generalizing b with
  | intro xa _ iha =>
    induction acb with
    | intro xb _ ihb =>
      refine Acc.intro (xa :: xb) fun p lt => ?_
      rcases shortlex_def.mp lt with h1 | ⟨h2len, h2lex⟩
      · exact ih _ h1
      · cases h2lex with
        | nil => simp at h2len
        | @cons x xs _ h =>
          simp only [length_cons, add_left_inj] at h2len
          refine ihb _ (of_lex h2len h) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl
        | @rel x xs _ _ h =>
          simp only [List.length_cons, add_left_inj] at h2len
          refine iha _ h (ih xs (by rw [h2len]; simp)) fun l hl => ?_
          apply ih
          rw [List.length_cons, ← h2len]
          exact hl

Premises used: List.length_cons, add_left_inj, List.Shortlex.cons, List.nil
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a.length = 0
⊢ a = []

Tactic:
rw [List.length_eq_zero_iff] at len_a

Premises used: List.length_eq_zero_iff
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
zero : Acc (Shortlex r) []
⊢ Acc (Shortlex r) a

Tactic:
rw [len_a]
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) []

Tactic:
Acc.intro _ <| fun _ ylt => (not_shortlex_nil_right ylt).elim

Premises used: False.elim, List.not_shortlex_nil_right, Acc.intro
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
len_a : a = []
⊢ Acc (Shortlex r) []

Tactic:
exact Acc.intro _ <| fun _ ylt => (not_shortlex_nil_right ylt).elim

Premises used: False.elim, List.not_shortlex_nil_right, Acc.intro
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
a : List α
len_a : a.length = n.succ
ind : ∀ (head : α) (tail : List α) (len_a : (head :: tail).length = n.succ), Acc (Shortlex r) (head :: tail)
⊢ Acc (Shortlex r) a

Tactic:
obtain ⟨head, tail, rfl⟩ := List.exists_of_length_succ a len_a

Premises used: List.head, List.exists_of_length_succ, List.tail, rfl
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : (head :: tail).length = n.succ
⊢ tail.length = n

Tactic:
rw [List.length_cons, add_left_inj] at len_a

Premises used: List.length_cons, add_left_inj
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
ind : ∀ (s : List α), s.length < (head :: tail).length → Acc (Shortlex r) s
⊢ Acc (Shortlex r) (head :: tail)

Tactic:
apply Acc.shortlex (WellFounded.apply h head) (ih n le_rfl tail len_a)

Premises used: le_rfl, WellFounded.apply, _private.0.Acc.shortlex
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
apply : l.length ≤ n
⊢ Acc (Shortlex r) l

Tactic:
apply ih l.length _ _ rfl

Premises used: List.length, rfl
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
rw : l.length ≤ tail.length
⊢ l.length ≤ n

Tactic:
rw [← len_a]
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ l.length ≤ tail.length

Tactic:
Nat.le_of_lt_succ ll

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
n : ℕ
ih : ∀ m ≤ n, ∀ (a : List α) (len_a : a.length = m), Acc (Shortlex r) a
head : α
tail : List α
len_a : tail.length = n
l : List α
ll : l.length < (head :: tail).length
⊢ l.length ≤ tail.length

Tactic:
exact Nat.le_of_lt_succ ll

Premises used: Nat.le_of_lt_succ
-- Module: Mathlib.Data.List.Shortlex
Goal:
α : Type u_1
r : α → α → Prop
h : WellFounded r
a : List α
induction : ∀ (x : ℕ) (len_a : a.length = x), Acc (Shortlex r) a
⊢ Acc (Shortlex r) a

Tactic:
induction len_a : a.length using Nat.caseStrongRecOn generalizing a with
  | zero =>
    rw [List.length_eq_zero_iff] at len_a
    rw [len_a]
    exact Acc.intro _ <| fun _ ylt => (not_shortlex_nil_right ylt).elim
  | ind n ih =>
    obtain ⟨head, tail, rfl⟩ := List.exists_of_length_succ a len_a
    rw [List.length_cons, add_left_inj] at len_a
    apply Acc.shortlex (WellFounded.apply h head) (ih n le_rfl tail len_a)
    intro l ll
    apply ih l.length _ _ rfl
    rw [← len_a]
    exact Nat.le_of_lt_succ ll

Premises used: List.head, List.length_cons, False.elim, add_left_inj, List.not_shortlex_nil_right, List.tail, List.length, List.length_eq_zero_iff, rfl, Acc.intro
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
⊢ Eq.{u + 1} (α := List α) (keys (β := β) []) []

Tactic:
rfl

Premises used: List.map, List.keys, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
⊢ (s :: l).keys (β := β) = s.fst (β := β) :: l.keys (β := β)

Tactic:
rfl

Premises used: List.map, List.keys, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
⊢ (l₁ ++ l₂).keys (β := β) = l₁.keys (β := β) ++ l₂.keys (β := β)

Tactic:
simp [keys]

Premises used: List.keys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
⊢ s ∈ l → s.fst (β := β) ∈ l.keys (β := β)

Tactic:
mem_map_of_mem

Premises used: List.keys, List.mem_map_of_mem
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
a : α
l : List (Sigma β)
h : a ∈ l.keys (β := β)
⊢ ∃ (a_1 : Sigma β), a_1 ∈ l ∧ a_1.fst (β := β) = a

Tactic:
have := exists_of_mem_map h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
a : α
l : List (Sigma β)
h : a ∈ l.keys (β := β)
this : ∃ (a_1 : Sigma β), a_1 ∈ l ∧ a_1.fst (β := β) = a
⊢ ∃ (b : β a), Sigma.mk (β := β) a b ∈ l

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ a ∈ l.keys (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ l

Tactic:
⟨exists_of_mem_keys, fun ⟨_, h⟩ => mem_keys_of_mem h⟩

Premises used: List.mem_keys_of_mem, _private.0.List.mem_keys.match_1, List.keys, Membership.mem, Iff.intro, List.exists_of_mem_keys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ ¬a ∈ l.keys (β := β) ↔ ∀ (b : β a), ¬Sigma.mk (β := β) a b ∈ l

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
a : α
l : List (Sigma β)
⊢ ¬a ∈ l.keys (β := β) ↔ ∀ (s : Sigma β), s ∈ l → a ≠ s.fst (β := β)

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
⊢ l.NodupKeys (β := β) ↔ Pairwise (fun (s s' : Sigma β) ↦ s.fst (β := β) ≠ s'.fst (β := β)) l

Tactic:
pairwise_map

Premises used: List.keys, List.pairwise_map, List.Nodup, List.NodupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ Pairwise (fun (s s' : Sigma β) ↦ s.fst (β := β) ≠ s'.fst (β := β)) l

Tactic:
nodupKeys_iff_pairwise.1 h

Premises used: List.nodupKeys_iff_pairwise, Iff.mp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
⊢ NodupKeys (β := β) []

Tactic:
Pairwise.nil

Premises used: List.map, List.keys, List.Nodup, List.Pairwise.nil, List.NodupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
⊢ (s :: l).NodupKeys (β := β) ↔ ¬s.fst (β := β) ∈ l.keys (β := β) ∧ l.NodupKeys (β := β)

Tactic:
simp [keys, NodupKeys]

Premises used: List.keys, List.NodupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
s : Sigma β
⊢ (l₁ ++ s :: l₂).NodupKeys (β := β) ↔ (s :: (l₁ ++ l₂)).NodupKeys (β := β)

Tactic:
simp_all [NodupKeys, keys, nodup_middle]

Premises used: List.keys, List.nodup_middle, List.NodupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
h : (s :: l).NodupKeys (β := β)
⊢ ¬s.fst (β := β) ∈ l.keys (β := β)

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
s : Sigma β
l : List (Sigma β)
h : (s :: l).NodupKeys (β := β)
⊢ l.NodupKeys (β := β)

Tactic:
(nodupKeys_cons.1 h).2

Premises used: List.nodupKeys_cons, And.right, Iff.mp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
nd : l.NodupKeys (β := β)
s s' : Sigma β
h : s ∈ l
h' : s' ∈ l
⊢ s.fst (β := β) = s'.fst (β := β) → s = s'

Tactic:
@Pairwise.forall_of_forall _ (fun s s' : Sigma β => s.1 = s'.1 → s = s') _
    (fun _ _ H h => (H h.symm).symm) (fun _ _ _ => rfl)
    ((nodupKeys_iff_pairwise.1 nd).imp fun h h' => (h h').elim) _ h _ h'

Premises used: List.Pairwise.forall_of_forall, List.nodupKeys_iff_pairwise, Iff.mp, List.Pairwise.imp, Eq.symm, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
a : α
b b' : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
h : Sigma.mk (β := β) a b ∈ l
h' : Sigma.mk (β := β) a b' ∈ l
⊢ b = b'

Tactic:
grind [NodupKeys.eq_of_fst_eq]

Premises used: List.NodupKeys.eq_of_fst_eq
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
s : Sigma β
⊢ [s].NodupKeys (β := β)

Tactic:
nodup_singleton _

Premises used: List.map, List.keys, List.nodup_singleton, List.NodupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
h : l₁ <+ l₂
⊢ l₂.NodupKeys (β := β) → l₁.NodupKeys (β := β)

Tactic:
Nodup.sublist <| h.map _

Premises used: List.Sublist.map, List.Nodup.sublist, List.NodupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l : List (Sigma β)
⊢ l.NodupKeys (β := β) → l.Nodup

Tactic:
Nodup.of_map _

Premises used: List.keys, List.Nodup.of_map, List.NodupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l₁ l₂ : List (Sigma β)
h : l₁ ~ l₂
⊢ l₁.NodupKeys (β := β) ↔ l₂.NodupKeys (β := β)

Tactic:
(h.map _).nodup_iff

Premises used: List.keys, List.Perm.nodup_iff, List.NodupKeys, List.Perm.map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
L : List (List (Sigma β))
rw :
  (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun (s s' : Sigma β) ↦ s.fst (β := β) ≠ s'.fst (β := β)) l) ∧
      Pairwise
        (fun (l₁ l₂ : List (Sigma β)) ↦
          ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst (β := β) ≠ y.fst (β := β))
        L ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys (β := β)) ∧
      Pairwise (fun (a b : List (Sigma β)) ↦ a.keys (β := β).Disjoint (b.keys (β := β))) L
⊢ L.flatten.NodupKeys (β := β) ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys (β := β)) ∧ Pairwise Disjoint (map (keys (β := β)) L)

Tactic:
rw [nodupKeys_iff_pairwise, pairwise_flatten, pairwise_map]

Premises used: List.pairwise_map, List.nodupKeys_iff_pairwise, List.pairwise_flatten
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
L : List (List (Sigma β))
l : List (Sigma β)
h : l ∈ L
⊢ Pairwise (fun (s s' : Sigma β) ↦ s.fst (β := β) ≠ s'.fst (β := β)) l ↔ l.NodupKeys (β := β)

Tactic:
simp [nodupKeys_iff_pairwise]

Premises used: List.nodupKeys_iff_pairwise
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
L : List (List (Sigma β))
refine :
  Pairwise
      (fun (l₁ l₂ : List (Sigma β)) ↦
        ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst (β := β) ≠ y.fst (β := β))
      L ↔
    Pairwise (fun (a b : List (Sigma β)) ↦ a.keys (β := β).Disjoint (b.keys (β := β))) L
⊢ (∀ (l : List (Sigma β)), l ∈ L → Pairwise (fun (s s' : Sigma β) ↦ s.fst (β := β) ≠ s'.fst (β := β)) l) ∧
      Pairwise
        (fun (l₁ l₂ : List (Sigma β)) ↦
          ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst (β := β) ≠ y.fst (β := β))
        L ↔
    (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys (β := β)) ∧
      Pairwise (fun (a b : List (Sigma β)) ↦ a.keys (β := β).Disjoint (b.keys (β := β))) L

Tactic:
refine and_congr (forall₂_congr fun l _ => by simp [nodupKeys_iff_pairwise]) ?_

Premises used: forall₂_congr, and_congr
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
L : List (List (Sigma β))
⊢ Pairwise
      (fun (l₁ l₂ : List (Sigma β)) ↦
        ∀ (x : Sigma β), x ∈ l₁ → ∀ (y : Sigma β), y ∈ l₂ → x.fst (β := β) ≠ y.fst (β := β))
      L ↔
    Pairwise (fun (a b : List (Sigma β)) ↦ a.keys (β := β).Disjoint (b.keys (β := β))) L

Tactic:
simp [keys, disjoint_iff_ne, Sigma.forall]

Premises used: List.disjoint_iff_ne, List.keys, Sigma.forall
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
l : List α
⊢ (map Prod.snd l.zipIdx).Nodup

Tactic:
simp [List.nodup_range']

Premises used: List.nodup_range', OfNat.ofNat
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
l₀ l₁ : List (Sigma β)
nd₀ : l₀.Nodup
nd₁ : l₁.Nodup
h : ∀ (x : Sigma β), x ∈ l₀ ↔ x ∈ l₁
⊢ l₀ ~ l₁

Tactic:
grind [perm_ext_iff_of_nodup]

Premises used: List.perm_ext_iff_of_nodup
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq.{v + 1} (α := Option (β a)) (dlookup (β := β) a []) none

Tactic:
rfl

Premises used: List.dlookup, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l : List (Sigma β)
a : α
b : β a
⊢ dlookup (β := β) a (Sigma.mk (β := β) a b :: l) = some b

Tactic:
dif_pos rfl

Premises used: dif_pos, List.dlookup, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Option.isSome.{v} (α := β a) (dlookup (β := β) a []) = true ↔ Membership.mem (γ := List α) (keys (β := β) []) a

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih : (dlookup (β := β) a tail).isSome = true ↔ a ∈ tail.keys (β := β)
pos : a = s.fst (β := β) → ((dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β))
neg : ¬a = s.fst (β := β) → ((dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β))
⊢ (dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β)

Tactic:
by_cases a = s.fst

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih : (dlookup (β := β) a tail).isSome = true ↔ a ∈ tail.keys (β := β)
h : a = s.fst (β := β)
⊢ (dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β)

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih : (dlookup (β := β) a tail).isSome = true ↔ a ∈ tail.keys (β := β)
h : ¬a = s.fst (β := β)
⊢ (dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β)

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nil : Option.isSome.{v} (α := β a) (dlookup (β := β) a []) = true ↔ Membership.mem (γ := List α) (keys (β := β) []) a
cons :
  ∀ (s : Sigma β) (tail : List (Sigma β)),
    ((dlookup (β := β) a tail).isSome = true ↔ a ∈ tail.keys (β := β)) →
      ((dlookup (β := β) a (s :: tail)).isSome = true ↔ a ∈ (s :: tail).keys (β := β))
⊢ (dlookup (β := β) a l).isSome = true ↔ a ∈ l.keys (β := β)

Tactic:
induction l with
  | nil => simp
  | cons s _ _ => by_cases a = s.fst <;> grind

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
⊢ dlookup (β := β) a l = none ↔ ¬a ∈ l.keys (β := β)

Tactic:
simp [← dlookup_isSome, Option.isNone_iff_eq_none]

Premises used: Option.isNone_iff_eq_none, List.dlookup_isSome
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
⊢ Membership.mem (γ := Option (β a)) (dlookup (β := β) a []) b →
    Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Sigma β
tail : List (Sigma β)
tail_ih : b ∈ dlookup (β := β) a tail → Sigma.mk (β := β) a b ∈ tail
pos : a = s.fst (β := β) → b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
neg : ¬a = s.fst (β := β) → b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
⊢ b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail

Tactic:
by_cases a = s.fst

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Sigma β
tail : List (Sigma β)
tail_ih : b ∈ dlookup (β := β) a tail → Sigma.mk (β := β) a b ∈ tail
h : a = s.fst (β := β)
⊢ b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
s : Sigma β
tail : List (Sigma β)
tail_ih : b ∈ dlookup (β := β) a tail → Sigma.mk (β := β) a b ∈ tail
h : ¬a = s.fst (β := β)
⊢ b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nil :
  Membership.mem (γ := Option (β a)) (dlookup (β := β) a []) b →
    Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)
cons :
  ∀ (s : Sigma β) (tail : List (Sigma β)),
    (b ∈ dlookup (β := β) a tail → Sigma.mk (β := β) a b ∈ tail) →
      b ∈ dlookup (β := β) a (s :: tail) → Sigma.mk (β := β) a b ∈ s :: tail
⊢ b ∈ dlookup (β := β) a l → Sigma.mk (β := β) a b ∈ l

Tactic:
induction l with
  | nil => grind
  | cons s _ _ => by_cases a = s.fst <;> grind

Premises used: List.cons, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
h : Sigma.mk (β := β) a b ∈ l
obtain :
  ∀ (b' : β ((Sigma.mk (β := β) a b).fst (β := β)))
    (h' : dlookup (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) l = some b'), b ∈ dlookup (β := β) a l
⊢ b ∈ dlookup (β := β) a l

Tactic:
obtain ⟨b', h'⟩ := Option.isSome_iff_exists.mp (dlookup_isSome.mpr (mem_keys_of_mem h))

Premises used: Iff.mpr, List.mem_keys_of_mem, Option.isSome_iff_exists, List.dlookup_isSome, Iff.mp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
h : Sigma.mk (β := β) a b ∈ l
b' : β ((Sigma.mk (β := β) a b).fst (β := β))
h' : dlookup (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) l = some b'
⊢ dlookup (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) l = some b

Tactic:
cases nd.eq_of_mk_mem h (of_mem_dlookup h')

Premises used: List.NodupKeys.eq_of_mk_mem, List.of_mem_dlookup
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
h : Sigma.mk (β := β) a b ∈ l
h' : dlookup (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) l = some b
⊢ b ∈ dlookup (β := β) a l

Tactic:
h'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
h : Sigma.mk (β := β) a b ∈ l
h' : dlookup (β := β) ((Sigma.mk (β := β) a b).fst (β := β)) l = some b
⊢ b ∈ dlookup (β := β) a l

Tactic:
exact h'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq (α := Option (Sigma β)) (Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a []))
    (find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) [])

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih :
  Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a tail) =
    find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) tail
pos :
  s.fst (β := β) = a →
    Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a (s :: tail)) =
      find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) (s :: tail)
neg :
  ¬s.fst (β := β) = a →
    Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a (s :: tail)) =
      find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) (s :: tail)
⊢ Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a (s :: tail)) =
    find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) (s :: tail)

Tactic:
by_cases s.fst = a

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih :
  Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a tail) =
    find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) tail
h : s.fst (β := β) = a
⊢ Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a (s :: tail)) =
    find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) (s :: tail)

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih :
  Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a tail) =
    find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) tail
h : ¬s.fst (β := β) = a
⊢ Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a (s :: tail)) =
    find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) (s :: tail)

Tactic:
grind