awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b : β a
pos : ∃ (x : β a), ¬x = b → Sigma.mk (β := β) a x ∈ l
⊢ lookupAll (β := β) a (Sigma.mk (β := β) a b :: l) = [] ↔
    ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a b :: l

Tactic:
simp only [lookupAll_cons_eq, mem_cons, Sigma.mk.inj_iff, heq_eq_eq, true_and, not_or,
        false_iff, not_forall, not_and, not_not, reduceCtorEq]

Premises used: reduceCtorEq, Classical.not_not, heq_eq_eq, false_iff, not_or, List.lookupAll_cons_eq, Sigma.mk.inj_iff, List.mem_cons, not_and, Classical.not_forall, true_and
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b : β a
h : ¬b = b → Sigma.mk (β := β) a b ∈ l
⊢ ∃ (x : β a), ¬x = b → Sigma.mk (β := β) a x ∈ l

Tactic:
use b
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ¬b = b → Sigma.mk (β := β) a b ∈ l

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l) = [] ↔
    ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a' b :: l

Tactic:
simp [h, lookupAll_eq_nil]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq.{v + 1} (α := Option (β a)) (head? (lookupAll (β := β) a [])) (dlookup (β := β) a [])

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
pos :
  ∀ (h : a = a'),
    (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)
neg :
  ∀ (h : ¬a = a'),
    (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)
⊢ (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)

Tactic:
by_cases h : a = a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : a = a'
pos :
  ∀ (b : β a),
    (lookupAll (β := β) a (Sigma.mk (β := β) a b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a b :: l)
⊢ (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)

Tactic:
subst h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ (lookupAll (β := β) a (Sigma.mk (β := β) a b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a b :: l)

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
neg neg₁ : a ≠ (Sigma.mk (β := β) a' b).fst (β := β)
⊢ (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)

Tactic:
rw [lookupAll_cons_ne, dlookup_cons_ne, head?_lookupAll a l]

Premises used: List.lookupAll_cons_ne, List.dlookup_cons_ne
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ a ≠ (Sigma.mk (β := β) a' b).fst (β := β)

Tactic:
assumption
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
⊢ Membership.mem (γ := List (β a)) (lookupAll (β := β) a []) b ↔
    Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
pos :
  ∀ (h : a = a'),
    b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: l
neg :
  ∀ (h : ¬a = a'),
    b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: l
⊢ b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: l

Tactic:
by_cases h : a = a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
pos :
  ∀ (b' : β a),
    b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a b' :: l
⊢ b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: l

Tactic:
subst h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
b' : β a
⊢ b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a b' :: l

Tactic:
simp [*, mem_lookupAll]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: l

Tactic:
simp [*, mem_lookupAll]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Sublist (α := Sigma β) (map (Sigma.mk (β := β) a) (lookupAll (β := β) a [])) []

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
pos :
  ∀ (h : a = a'),
    map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l
neg :
  ∀ (h : ¬a = a'),
    map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l

Tactic:
by_cases h : a = a'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
pos :
  ∀ (b' : β a),
    map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a b' :: l)) <+ Sigma.mk (β := β) a b' :: l
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l

Tactic:
subst h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
pos : Sigma.mk (β := β) a b' :: map (Sigma.mk (β := β) a) (lookupAll (β := β) a l) <+ Sigma.mk (β := β) a b' :: l
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a b' :: l)) <+ Sigma.mk (β := β) a b' :: l

Tactic:
simp only [lookupAll_cons_eq, List.map]

Premises used: List.map, List.lookupAll_cons_eq
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ Sigma.mk (β := β) a b' :: map (Sigma.mk (β := β) a) (lookupAll (β := β) a l) <+ Sigma.mk (β := β) a b' :: l

Tactic:
(lookupAll_sublist a l).cons_cons _

Premises used: List.Sublist.cons_cons
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ Sigma.mk (β := β) a b' :: map (Sigma.mk (β := β) a) (lookupAll (β := β) a l) <+ Sigma.mk (β := β) a b' :: l

Tactic:
exact (lookupAll_sublist a l).cons_cons _

Premises used: List.Sublist.cons_cons
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
neg : map (Sigma.mk (β := β) a) (lookupAll (β := β) a l) <+ Sigma.mk (β := β) a' b' :: l
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l

Tactic:
simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]

Premises used: List.lookupAll_cons_ne, ne_eq, not_false_iff
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a l) <+ Sigma.mk (β := β) a' b' :: l

Tactic:
(lookupAll_sublist a l).cons _

Premises used: List.Sublist.cons
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a l) <+ Sigma.mk (β := β) a' b' :: l

Tactic:
exact (lookupAll_sublist a l).cons _

Premises used: List.Sublist.cons
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ (map (Sigma.fst (β := β)) (map (Sigma.mk (β := β) a) (lookupAll (β := β) a l))).Nodup

Tactic:
have := Nodup.sublist ((lookupAll_sublist a l).map _) h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
this : (map (Sigma.fst (β := β)) (map (Sigma.mk (β := β) a) (lookupAll (β := β) a l))).Nodup
⊢ (map (Sigma.fst (β := β) ∘ Sigma.mk (β := β) a) (lookupAll (β := β) a l)).Nodup

Tactic:
rw [map_map] at this

Premises used: List.map_map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
this : (map (Sigma.fst (β := β) ∘ Sigma.mk (β := β) a) (lookupAll (β := β) a l)).Nodup
rwa : (replicate (lookupAll (β := β) a l).length a).Nodup
rwa₁ : Type u
rwa₂ : α
rwa₃ : (map (Function.const (β a) a) (lookupAll (β := β) a l)).Nodup
rwa₄ : Type u
rwa₅ : α
rwa₆ : (map (Function.const (β a) a) (lookupAll (β := β) a l)).Nodup
rwa₇ : Type u
rwa₈ : α
rwa₉ : (map (Function.const (β a) a) (lookupAll (β := β) a l)).Nodup
rwa₁₀ : Type u
rwa₁₁ : α
rwa₁₂ : (map (Function.const (β a) a) (lookupAll (β := β) a l)).Nodup
rwa₁₃ : Type u
rwa₁₄ : α
⊢ (lookupAll (β := β) a l).length ≤ 1

Tactic:
rwa [← nodup_replicate, ← map_const]

Premises used: List.map_const, List.nodup_replicate
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
rw : lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
⊢ lookupAll (β := β) a l = (dlookup (β := β) a l).toList

Tactic:
rw [← head?_lookupAll]

Premises used: List.head?_lookupAll
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ (lookupAll (β := β) a l).length ≤ 1

Tactic:
have h1 := lookupAll_length_le_one a h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
h1 : (lookupAll (β := β) a l).length ≤ 1
revert : ∀ (h1 : (lookupAll (β := β) a l).length ≤ 1), lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
⊢ lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList

Tactic:
revert h1
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
nil : ∀ (h1 : length.{v} (α := β a) [] ≤ 1), Eq.{v + 1} (α := List (β a)) [] (Option.toList (head? []))
cons : ∀ (b : β a) (h1 : [b].length ≤ 1), [b] = [b].head?.toList
cons₁ : ∀ (b c : β a) (l : List (β a)) (h1 : (b :: c :: l).length ≤ 1), b :: c :: l = (b :: c :: l).head?.toList
⊢ ∀ (h1 : (lookupAll (β := β) a l).length ≤ 1), lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList

Tactic:
rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩)

Premises used: List.lookupAll
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
h1 : length.{v} (α := β a) [] ≤ 1
⊢ Eq.{v + 1} (α := List (β a)) [] (Option.toList (head? []))

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
h1 : length.{v} (α := β a) [] ≤ 1
⊢ Eq.{v + 1} (α := List (β a)) [] (Option.toList (head? []))

Tactic:
try rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
b : β a
h1 : [b].length ≤ 1
⊢ [b] = [b].head?.toList

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
b : β a
h1 : [b].length ≤ 1
⊢ [b] = [b].head?.toList

Tactic:
try rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l_1 : List (Sigma β)
h : l_1.NodupKeys (β := β)
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ ¬(b :: c :: l).length ≤ 1

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l_1 : List (Sigma β)
h : l_1.NodupKeys (β := β)
b c : β a
l : List (β a)
h1 : (b :: c :: l).length ≤ 1
⊢ b :: c :: l = (b :: c :: l).head?.toList

Tactic:
exact absurd h1 (by simp)

Premises used: absurd
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
rw : (dlookup (β := β) a l).toList.Nodup
⊢ (lookupAll (β := β) a l).Nodup

Tactic:
rw [lookupAll_eq_dlookup a h]

Premises used: List.lookupAll_eq_dlookup
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ (dlookup (β := β) a l).toList.Nodup

Tactic:
apply Option.toList_nodup

Premises used: Option.toList_nodup
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys (β := β)
p : l₁ ~ l₂
nd₂ : l₂.NodupKeys (β := β)
⊢ lookupAll (β := β) a l₁ = lookupAll (β := β) a l₂

Tactic:
simp [lookupAll_eq_dlookup, nd₁, nd₂, perm_dlookup a nd₁ p]

Premises used: List.lookupAll_eq_dlookup, List.perm_dlookup
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
H : ∀ (b : β a), ¬Sigma.mk (β := β) a b ∈ l
⊢ ∀ (a_1 : Sigma β), a_1 ∈ l → (if a = a_1.fst (β := β) then some (Sigma.mk (β := β) a b) else none) = none

Tactic:
grind
-- 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
⊢ kreplace (β := β) a b l = l

Tactic:
(lookmap_congr ?_).trans (lookmap_id' (Option.guard fun (s : Sigma β) => a = s.1) ?_ _)

Premises used: Option.guard, List.kreplace, List.lookmap_id', Sigma.fst, List.lookmap_congr, Decidable.decide, Eq, Eq.trans
-- 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
refine_1 :
  ∀ (a_1 : Sigma β),
    a_1 ∈ l →
      (if a = a_1.fst (β := β) then some (Sigma.mk (β := β) a b) else none) =
        Option.guard (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) a_1
refine_2 : ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) a_1 → a_1 = b
⊢ kreplace (β := β) a b l = l

Tactic:
refine (lookmap_congr ?_).trans (lookmap_id' (Option.guard fun (s : Sigma β) => a = s.1) ?_ _)

Premises used: Option.guard, List.lookmap_id', Sigma.fst, List.lookmap_congr, Decidable.decide, Eq, Eq.trans
-- 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
a' : α
b' : β a'
h' : Sigma.mk (β := β) a' b' ∈ l
refine_1 :
  (if a = a' then some (Sigma.mk (β := β) a b) else none) =
    if decide (a = a') = true then some (Sigma.mk (β := β) a' b') else none
⊢ (if a = (Sigma.mk (β := β) a' b').fst (β := β) then some (Sigma.mk (β := β) a b) else none) =
    Option.guard (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) (Sigma.mk (β := β) a' b')

Tactic:
dsimp [Option.guard]

Premises used: Option.guard
-- 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
a' : α
b' : β a'
h' : Sigma.mk (β := β) a' b' ∈ l
pos : a = a' → decide (a = a') = true → some (Sigma.mk (β := β) a b) = some (Sigma.mk (β := β) a' b')
neg : a = a' → ¬decide (a = a') = true → False
pos₁ : ¬a = a' → decide (a = a') = true → False
neg₁ : ¬a = a' → ¬decide (a = a') = true → Eq (α := Option (Sigma β)) none none
⊢ (if a = a' then some (Sigma.mk (β := β) a b) else none) =
    if decide (a = a') = true then some (Sigma.mk (β := β) a' b') else none

Tactic:
split_ifs
-- 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
a' : α
b' : β a'
h' : Sigma.mk (β := β) a' b' ∈ l
h_1 : a = a'
h_2 : decide (a = a') = true
pos :
  ∀ (b' : β a) (h' : Sigma.mk (β := β) a b' ∈ l),
    decide (a = a) = true → some (Sigma.mk (β := β) a b) = some (Sigma.mk (β := β) a b')
⊢ some (Sigma.mk (β := β) a b) = some (Sigma.mk (β := β) a' b')

Tactic:
subst a'
-- 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' : β a
h' : Sigma.mk (β := β) a b' ∈ l
h_1 : decide (a = a) = true
⊢ some (Sigma.mk (β := β) a b) = some (Sigma.mk (β := β) a b')

Tactic:
simp [nd.eq_of_mk_mem h h']

Premises used: List.NodupKeys.eq_of_mk_mem
-- 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
a' : α
b' : β a'
h' : Sigma.mk (β := β) a' b' ∈ l
h_1 : a = a'
h_2 : ¬decide (a = a') = true
⊢ False

Tactic:
simp_all
-- 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
a' : α
b' : β a'
h' : Sigma.mk (β := β) a' b' ∈ l
h_1 : ¬a = a'
h_2 : decide (a = a') = true
⊢ False

Tactic:
simp_all
-- 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
a' : α
b' : β a'
h' : Sigma.mk (β := β) a' b' ∈ l
h_1 : ¬a = a'
h_2 : ¬decide (a = a') = true
⊢ Eq (α := Option (Sigma β)) none none

Tactic:
rfl
-- 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
⊢ ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) a_1 → a_1 = b

Tactic:
simp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a₁ : α
b₂_1 : β a₁
a₂ : α
b₂ : β a₂
dsimp : (Sigma.mk (β := β) a₂ b₂ ∈ if a = a₁ then some (Sigma.mk (β := β) a b) else none) → a₁ = a₂
⊢ (Sigma.mk (β := β) a₂ b₂ ∈
      if a = (Sigma.mk (β := β) a₁ b₂_1).fst (β := β) then some (Sigma.mk (β := β) a b) else none) →
    (Sigma.mk (β := β) a₁ b₂_1).fst (β := β) = (Sigma.mk (β := β) a₂ b₂).fst (β := β)

Tactic:
dsimp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a₁ : α
b₂_1 : β a₁
a₂ : α
b₂ : β a₂
pos : ∀ (h : a = a₁), Sigma.mk (β := β) a₂ b₂ ∈ some (Sigma.mk (β := β) a b) → a₁ = a₂
neg : ∀ (h : ¬a = a₁), Membership.mem (γ := Option (Sigma β)) none (Sigma.mk (β := β) a₂ b₂) → a₁ = a₂
⊢ (Sigma.mk (β := β) a₂ b₂ ∈ if a = a₁ then some (Sigma.mk (β := β) a b) else none) → a₁ = a₂

Tactic:
split_ifs with h
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a₁ : α
b₂_1 : β a₁
a₂ : α
b₂ : β a₂
h : a = a₁
⊢ Sigma.mk (β := β) a₂ b₂ ∈ some (Sigma.mk (β := β) a b) → a₁ = a₂

Tactic:
simp +contextual [h]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a₁ : α
b₂_1 : β a₁
a₂ : α
b₂ : β a₂
h : ¬a = a₁
⊢ Membership.mem (γ := Option (Sigma β)) none (Sigma.mk (β := β) a₂ b₂) → a₁ = a₂

Tactic:
simp +contextual [h]
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l : List (Sigma β)
⊢ (kreplace (β := β) a b l).NodupKeys (β := β) ↔ l.NodupKeys (β := β)

Tactic:
simp [NodupKeys, keys_kreplace]

Premises used: List.keys_kreplace, List.NodupKeys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
⊢ Pairwise
    (fun (a_1 b_1 : Sigma β) ↦
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst (β := β) then some (Sigma.mk (β := β) a b) else none) →
          ∀ (d : Sigma β),
            (d ∈ if a = b_1.fst (β := β) then some (Sigma.mk (β := β) a b) else none) → a_1 = b_1 ∧ c = d)
    l₁

Tactic:
nd.pairwise_ne.imp ?_

Premises used: List.NodupKeys.pairwise_ne, List.Pairwise.imp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
refine :
  ∀ {a_1 b_1 : Sigma β},
    a_1.fst (β := β) ≠ b_1.fst (β := β) →
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst (β := β) then some (Sigma.mk (β := β) a b) else none) →
          ∀ (d : Sigma β), (d ∈ if a = b_1.fst (β := β) then some (Sigma.mk (β := β) a b) else none) → a_1 = b_1 ∧ c = d
⊢ Pairwise
    (fun (a_1 b_1 : Sigma β) ↦
      ∀ (c : Sigma β),
        (c ∈ if a = a_1.fst (β := β) then some (Sigma.mk (β := β) a b) else none) →
          ∀ (d : Sigma β),
            (d ∈ if a = b_1.fst (β := β) then some (Sigma.mk (β := β) a b) else none) → a_1 = b_1 ∧ c = d)
    l₁

Tactic:
refine nd.pairwise_ne.imp ?_

Premises used: List.NodupKeys.pairwise_ne, List.Pairwise.imp
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
z : Sigma β
h₁ : z ∈ if a = x.fst (β := β) then some (Sigma.mk (β := β) a b) else none
w : Sigma β
h₂ : w ∈ if a = y.fst (β := β) then some (Sigma.mk (β := β) a b) else none
pos :
  ∀ (h_2 : a = x.fst (β := β)) (h₁ : z ∈ some (Sigma.mk (β := β) a b)) (h_1 : a = y.fst (β := β))
    (h₂ : w ∈ some (Sigma.mk (β := β) a b)), x = y ∧ z = w
neg :
  ∀ (h_2 : a = x.fst (β := β)) (h₁ : z ∈ some (Sigma.mk (β := β) a b)) (h_1 : ¬a = y.fst (β := β))
    (h₂ : Membership.mem (γ := Option (Sigma β)) none w), x = y ∧ z = w
pos₁ :
  ∀ (h_2 : ¬a = x.fst (β := β)) (h₁ : Membership.mem (γ := Option (Sigma β)) none z),
    a = y.fst (β := β) → ∀ (h₂ : w ∈ some (Sigma.mk (β := β) a b)), x = y ∧ z = w
neg₁ :
  ∀ (h_2 : ¬a = x.fst (β := β)) (h₁ : Membership.mem (γ := Option (Sigma β)) none z),
    ¬a = y.fst (β := β) → ∀ (h₂ : Membership.mem (γ := Option (Sigma β)) none w), x = y ∧ z = w
⊢ x = y ∧ z = w

Tactic:
split_ifs at h₁ h₂ with h_2 h_1
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
z w : Sigma β
h_2 : a = x.fst (β := β)
h₁ : z ∈ some (Sigma.mk (β := β) a b)
h_1 : a = y.fst (β := β)
h₂ : w ∈ some (Sigma.mk (β := β) a b)
pos : x = y ∧ Sigma.mk (β := β) a b = w
⊢ x = y ∧ z = w

Tactic:
cases h₁
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
z w : Sigma β
h_2 : a = x.fst (β := β)
h₁ : z ∈ some (Sigma.mk (β := β) a b)
h_1 : ¬a = y.fst (β := β)
h₂ : Membership.mem (γ := Option (Sigma β)) none w
neg : x = y ∧ Sigma.mk (β := β) a b = w
⊢ x = y ∧ z = w

Tactic:
cases h₁
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
z w : Sigma β
h_2 : ¬a = x.fst (β := β)
h₁ : Membership.mem (γ := Option (Sigma β)) none z
h_1 : a = y.fst (β := β)
h₂ : w ∈ some (Sigma.mk (β := β) a b)
⊢ x = y ∧ z = w

Tactic:
cases h₁