awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
nil :
  Eq (α := Option (Sigma β)) (Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a []))
    (find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) [])
cons :
  ∀ (s : Sigma β) (tail : List (Sigma β)),
    Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a tail) =
        find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) tail →
      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 l) = find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) l

Tactic:
induction l with
  | nil => grind
  | cons s _ _ => by_cases s.fst = a <;> 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 (β := β)
⊢ b ∈ dlookup (β := β) a l ↔ Sigma.mk (β := β) a b ∈ l

Tactic:
⟨of_mem_dlookup, mem_dlookup nd⟩

Premises used: List.mem_dlookup, Iff.intro, List.of_mem_dlookup
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys (β := β)
p : l₁ ~ l₂
⊢ l₂.NodupKeys (β := β)

Tactic:
have nd₂ := (perm_nodupKeys p).mp nd₁
-- 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 (β := β)
a₁ : ∀ (b : β a), dlookup (β := β) a l₁ = some b ↔ dlookup (β := β) a l₂ = some b
⊢ dlookup (β := β) a l₁ = dlookup (β := β) a l₂

Tactic:
ext b
-- 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 (β := β)
b : β a
⊢ dlookup (β := β) a l₁ = some b ↔ dlookup (β := β) a l₂ = some b

Tactic:
simp only [← Option.mem_def, mem_dlookup_iff nd₁, mem_dlookup_iff nd₂, p.mem_iff]

Premises used: List.mem_dlookup_iff, List.Perm.mem_iff, Option.mem_def
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₀ l₁ : List (Sigma β)
nd₀ : l₀.NodupKeys (β := β)
nd₁ : l₁.NodupKeys (β := β)
h : ∀ (x : α) (y : β x), y ∈ dlookup (β := β) x l₀ ↔ y ∈ dlookup (β := β) x l₁
⊢ l₀ ~ l₁

Tactic:
grind [_=_ mem_dlookup_iff, mem_ext]

Premises used: List.mem_ext, List.mem_dlookup_iff
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) []) = Option.map (g a) (dlookup (β := β) a [])

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih :
  dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) tail) = Option.map (g a) (dlookup (β := β) a tail)
⊢ ∀ (h : a ≠ s.fst (β := β)),
    ¬f a = (Sigma.mk (β := β') (f (s.fst (β := β))) (g (s.fst (β := β)) (s.snd (β := β)))).fst (β := β')

Tactic:
have (h : a ≠ s.fst) : ¬ f a = (⟨f s.fst, g s.fst s.snd⟩ : Sigma β').fst := fun he => h <| hf he
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih :
  dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) tail) = Option.map (g a) (dlookup (β := β) a tail)
this :
  ∀ (h : a ≠ s.fst (β := β)),
    ¬f a = (Sigma.mk (β := β') (f (s.fst (β := β))) (g (s.fst (β := β)) (s.snd (β := β)))).fst (β := β')
pos :
  a = s.fst (β := β) →
    dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
      Option.map (g a) (dlookup (β := β) a (s :: tail))
neg :
  ¬a = s.fst (β := β) →
    dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
      Option.map (g a) (dlookup (β := β) a (s :: tail))
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
    Option.map (g a) (dlookup (β := β) a (s :: tail))

Tactic:
by_cases a = s.fst

Premises used: Sigma.fst
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih :
  dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) tail) = Option.map (g a) (dlookup (β := β) a tail)
this :
  ∀ (h : a ≠ s.fst (β := β)),
    ¬f a = (Sigma.mk (β := β') (f (s.fst (β := β))) (g (s.fst (β := β)) (s.snd (β := β)))).fst (β := β')
h : a = s.fst (β := β)
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
    Option.map (g a) (dlookup (β := β) a (s :: tail))

Tactic:
grind [Sigma.map]

Premises used: Sigma.map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst : DecidableEq α
inst_1 : DecidableEq α'
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih :
  dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) tail) = Option.map (g a) (dlookup (β := β) a tail)
this :
  ∀ (h : a ≠ s.fst (β := β)),
    ¬f a = (Sigma.mk (β := β') (f (s.fst (β := β))) (g (s.fst (β := β)) (s.snd (β := β)))).fst (β := β')
h : ¬a = s.fst (β := β)
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
    Option.map (g a) (dlookup (β := β) a (s :: tail))

Tactic:
grind [Sigma.map]

Premises used: Sigma.map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : α → Type v
β' : α' → Type v'
inst : DecidableEq α
inst_1 : DecidableEq α'
l : List (Sigma β)
f : α → α'
hf : Function.Injective f
g : (a : α) → β a → β' (f a)
a : α
nil : dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) []) = Option.map (g a) (dlookup (β := β) a [])
cons :
  ∀ (s : Sigma β) (tail : List (Sigma β)),
    dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) tail) =
        Option.map (g a) (dlookup (β := β) a tail) →
      dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
        Option.map (g a) (dlookup (β := β) a (s :: tail))
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) l) = Option.map (g a) (dlookup (β := β) a l)

Tactic:
induction l with
  | nil => grind
  | cons s _ _ =>
    have (h : a ≠ s.fst) : ¬ f a = (⟨f s.fst, g s.fst s.snd⟩ : Sigma β').fst := fun he => h <| hf he
    by_cases a = s.fst <;> grind [Sigma.map]

Premises used: List.cons, Sigma.map, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
inst : DecidableEq α
inst_1 : DecidableEq α'
β : Type v
l : List ((_ : α) × β)
f : α → α'
hf : Function.Injective f
a : α
⊢ ∀ (l : List ((x : α) × (fun (x : α') ↦ β) (f x))) (hf : Function.Injective f) (a : α),
    dlookup (β := fun (x : α') ↦ β) (f a)
        (map (Sigma.map (β₁ := fun (x : α) ↦ (fun (x : α') ↦ β) (f x)) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) l) =
      Option.map id (dlookup (β := fun (x : α) ↦ (fun (x : α') ↦ β) (f x)) a l)

Tactic:
have := dlookup_map (β' := fun _ => β) (f := f) (g := fun _ => id)
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
inst : DecidableEq α
inst_1 : DecidableEq α'
β : Type v
l : List ((_ : α) × β)
f : α → α'
hf : Function.Injective f
a : α
this :
  ∀ (l : List ((x : α) × (fun (x : α') ↦ β) (f x))) (hf : Function.Injective f) (a : α),
    dlookup (β := fun (x : α') ↦ β) (f a)
        (map (Sigma.map (β₁ := fun (x : α) ↦ (fun (x : α') ↦ β) (f x)) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) l) =
      Option.map id (dlookup (β := fun (x : α) ↦ (fun (x : α') ↦ β) (f x)) a l)
⊢ dlookup (β := fun (x : α') ↦ β) (f a)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) l) =
    dlookup (β := fun (x : α) ↦ β) a l

Tactic:
grind [Option.map_id']

Premises used: Option.map_id'
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
inst : DecidableEq α
γ : α → Type u_1
δ : α → Type u_2
l : List ((a : α) × γ a)
f : (a : α) → γ a → δ a
a : α
⊢ dlookup (β := fun (a : α) ↦ δ a) a (map (Sigma.map (β₁ := γ) (β₂ := fun (a : α) ↦ δ a) id f) l) =
    Option.map (f a) (dlookup (β := fun (a : α) ↦ γ a) a l)

Tactic:
dlookup_map l Function.injective_id _ _

Premises used: List.dlookup_map, Function.injective_id
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
nd : NodupKeys (β := fun (x : α) ↦ β) []
⊢ NodupKeys (β := fun (x : α') ↦ β)
    (map (α := (_ : α) × β) (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) [])

Tactic:
nodupKeys_nil

Premises used: List.map, List.nodupKeys_nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
nd : NodupKeys (β := fun (x : α) ↦ β) []
⊢ NodupKeys (β := fun (x : α') ↦ β)
    (map (α := (_ : α) × β) (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) [])

Tactic:
exact nodupKeys_nil

Premises used: List.nodupKeys_nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih :
  ∀ (nd : tl.NodupKeys (β := fun (x : α) ↦ β)),
    NodupKeys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)
nd : (hd :: tl).NodupKeys (β := fun (x : α) ↦ β)
cons :
  ∀ (nd : ¬hd.fst (β := fun (x : α) ↦ β) ∈ tl.keys (β := fun (x : α) ↦ β) ∧ tl.NodupKeys (β := fun (x : α) ↦ β)),
    ¬Sigma.fst (β := fun (x : α') ↦ β)
            (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd) ∈
          keys (β := fun (x : α') ↦ β)
            (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl) ∧
      NodupKeys (β := fun (x : α') ↦ β)
        (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)
⊢ NodupKeys (β := fun (x : α') ↦ β)
    (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) (hd :: tl))

Tactic:
simp only [map_cons, nodupKeys_cons] at nd ⊢

Premises used: List.map_cons, List.nodupKeys_cons
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih :
  ∀ (nd : tl.NodupKeys (β := fun (x : α) ↦ β)),
    NodupKeys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)
nd : ¬hd.fst (β := fun (x : α) ↦ β) ∈ tl.keys (β := fun (x : α) ↦ β) ∧ tl.NodupKeys (β := fun (x : α) ↦ β)
h :
  Sigma.fst (β := fun (x : α') ↦ β)
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd) ∈
    keys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)
⊢ Sigma.fst (β := fun (x : α') ↦ β)
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd) ∈
    map
      (Function.comp (β := (_ : α') × β) (Sigma.fst (β := fun (x : α') ↦ β))
        (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id))
      tl

Tactic:
simp only [keys, map_map] at h ⊢

Premises used: List.keys, List.map_map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih :
  ∀ (nd : tl.NodupKeys (β := fun (x : α) ↦ β)),
    NodupKeys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)
nd : ¬hd.fst (β := fun (x : α) ↦ β) ∈ tl.keys (β := fun (x : α) ↦ β) ∧ tl.NodupKeys (β := fun (x : α) ↦ β)
h :
  Sigma.fst (β := fun (x : α') ↦ β)
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd) ∈
    map
      (Function.comp (β := (_ : α') × β) (Sigma.fst (β := fun (x : α') ↦ β))
        (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id))
      tl
obtain :
  ∀ (x : (_ : α) × β) (hm : x ∈ tl)
    (he :
      Function.comp (β := (_ : α') × β) (Sigma.fst (β := fun (x : α') ↦ β))
          (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) x =
        Sigma.fst (β := fun (x : α') ↦ β)
          (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd)),
    hd.fst (β := fun (x : α) ↦ β) ∈ map (Sigma.fst (β := fun (x : α) ↦ β)) tl
⊢ hd.fst (β := fun (x : α) ↦ β) ∈ map (Sigma.fst (β := fun (x : α) ↦ β)) tl

Tactic:
obtain ⟨x, hm, he⟩ := mem_map.mp h

Premises used: Iff.mp, List.mem_map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih :
  ∀ (nd : tl.NodupKeys (β := fun (x : α) ↦ β)),
    NodupKeys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)
nd : ¬hd.fst (β := fun (x : α) ↦ β) ∈ tl.keys (β := fun (x : α) ↦ β) ∧ tl.NodupKeys (β := fun (x : α) ↦ β)
h :
  Sigma.fst (β := fun (x : α') ↦ β)
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd) ∈
    map
      (Function.comp (β := (_ : α') × β) (Sigma.fst (β := fun (x : α') ↦ β))
        (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id))
      tl
x : (_ : α) × β
hm : x ∈ tl
he :
  Function.comp (β := (_ : α') × β) (Sigma.fst (β := fun (x : α') ↦ β))
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) x =
    Sigma.fst (β := fun (x : α') ↦ β)
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd)
⊢ hd.fst (β := fun (x : α) ↦ β) ∈ map (Sigma.fst (β := fun (x : α) ↦ β)) tl

Tactic:
mem_map.mpr ⟨x, hm, hf he⟩

Premises used: Iff.mpr, And.intro, Exists.intro, List.mem_map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih :
  ∀ (nd : tl.NodupKeys (β := fun (x : α) ↦ β)),
    NodupKeys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)
nd : ¬hd.fst (β := fun (x : α) ↦ β) ∈ tl.keys (β := fun (x : α) ↦ β) ∧ tl.NodupKeys (β := fun (x : α) ↦ β)
h :
  Sigma.fst (β := fun (x : α') ↦ β)
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd) ∈
    map
      (Function.comp (β := (_ : α') × β) (Sigma.fst (β := fun (x : α') ↦ β))
        (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id))
      tl
x : (_ : α) × β
hm : x ∈ tl
he :
  Function.comp (β := (_ : α') × β) (Sigma.fst (β := fun (x : α') ↦ β))
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) x =
    Sigma.fst (β := fun (x : α') ↦ β)
      (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd)
⊢ hd.fst (β := fun (x : α) ↦ β) ∈ map (Sigma.fst (β := fun (x : α) ↦ β)) tl

Tactic:
exact mem_map.mpr ⟨x, hm, hf he⟩

Premises used: Iff.mpr, And.intro, Exists.intro, List.mem_map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
hd : (_ : α) × β
tl : List ((_ : α) × β)
ih :
  ∀ (nd : tl.NodupKeys (β := fun (x : α) ↦ β)),
    NodupKeys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)
nd : ¬hd.fst (β := fun (x : α) ↦ β) ∈ tl.keys (β := fun (x : α) ↦ β) ∧ tl.NodupKeys (β := fun (x : α) ↦ β)
⊢ ¬Sigma.fst (β := fun (x : α') ↦ β)
          (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f (fun (x : α) ↦ id) hd) ∈
        keys (β := fun (x : α') ↦ β)
          (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl) ∧
    NodupKeys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl)

Tactic:
exact ⟨mt (fun h => by
      simp only [keys, map_map] at h ⊢
      obtain ⟨x, hm, he⟩ := mem_map.mp h
      exact mem_map.mpr ⟨x, hm, hf he⟩) nd.1, ih nd.2⟩
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
l : List ((_ : α) × β)
nd : l.NodupKeys (β := fun (x : α) ↦ β)
nil :
  ∀ (nd : NodupKeys (β := fun (x : α) ↦ β) []),
    NodupKeys (β := fun (x : α') ↦ β)
      (map (α := (_ : α) × β) (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) [])
cons :
  ∀ (hd : (_ : α) × β) (tl : List ((_ : α) × β))
    (ih :
      ∀ (nd : tl.NodupKeys (β := fun (x : α) ↦ β)),
        NodupKeys (β := fun (x : α') ↦ β)
          (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) tl))
    (nd : (hd :: tl).NodupKeys (β := fun (x : α) ↦ β)),
    NodupKeys (β := fun (x : α') ↦ β)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) (hd :: tl))
⊢ NodupKeys (β := fun (x : α') ↦ β)
    (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) l)

Tactic:
induction l with
  | nil => exact nodupKeys_nil
  | cons hd tl ih =>
    simp only [map_cons, nodupKeys_cons] at nd ⊢
    exact ⟨mt (fun h => by
      simp only [keys, map_map] at h ⊢
      obtain ⟨x, hm, he⟩ := mem_map.mp h
      exact mem_map.mpr ⟨x, hm, hf he⟩) nd.1, ih nd.2⟩

Premises used: List.map_cons, List.nodupKeys_cons, List.cons, List.nodupKeys_nil, List.nil
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
l : List ((a : α) × β a)
nil : (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) []).keys (β := β') = keys (β := fun (a : α) ↦ β a) []
cons :
  ∀ (head : (a : α) × β a) (tail : List ((a : α) × β a)),
    (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) tail).keys (β := β') =
        tail.keys (β := fun (a : α) ↦ β a) →
      (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) (head :: tail)).keys (β := β') =
        (head :: tail).keys (β := fun (a : α) ↦ β a)
⊢ (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) l).keys (β := β') = l.keys (β := fun (a : α) ↦ β a)

Tactic:
induction l
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
⊢ (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) []).keys (β := β') = keys (β := fun (a : α) ↦ β a) []

Tactic:
grind [Sigma.map]

Premises used: Sigma.map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
head : (a : α) × β a
tail : List ((a : α) × β a)
tail_ih :
  (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) tail).keys (β := β') = tail.keys (β := fun (a : α) ↦ β a)
⊢ (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) (head :: tail)).keys (β := β') =
    (head :: tail).keys (β := fun (a : α) ↦ β a)

Tactic:
grind [Sigma.map]

Premises used: Sigma.map
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
l : List ((a : α) × β a)
nd : l.NodupKeys (β := fun (a : α) ↦ β a)
⊢ (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) l).NodupKeys (β := β')

Tactic:
simp_all [NodupKeys, map₂_keys]

Premises used: List.NodupKeys, List.map₂_keys
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₂ : List (Sigma β)
a : α
⊢ dlookup (β := β) a ([] ++ l₂) = Option.or (dlookup (β := β) a []) (dlookup (β := β) a l₂)

Tactic:
rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₂ : List (Sigma β)
a : α
s : Sigma β
tail : List (Sigma β)
tail_ih : dlookup (β := β) a (tail ++ l₂) = (dlookup (β := β) a tail).or (dlookup (β := β) a l₂)
pos :
  a = s.fst (β := β) →
    dlookup (β := β) a (s :: tail ++ l₂) = (dlookup (β := β) a (s :: tail)).or (dlookup (β := β) a l₂)
neg :
  ¬a = s.fst (β := β) →
    dlookup (β := β) a (s :: tail ++ l₂) = (dlookup (β := β) a (s :: tail)).or (dlookup (β := β) a l₂)
⊢ dlookup (β := β) a (s :: tail ++ l₂) = (dlookup (β := β) a (s :: tail)).or (dlookup (β := β) a l₂)

Tactic:
by_cases a = s.fst

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

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

Tactic:
grind
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
a : α
nil : dlookup (β := β) a ([] ++ l₂) = Option.or (dlookup (β := β) a []) (dlookup (β := β) a l₂)
cons :
  ∀ (s : Sigma β) (tail : List (Sigma β)),
    dlookup (β := β) a (tail ++ l₂) = (dlookup (β := β) a tail).or (dlookup (β := β) a l₂) →
      dlookup (β := β) a (s :: tail ++ l₂) = (dlookup (β := β) a (s :: tail)).or (dlookup (β := β) a l₂)
⊢ dlookup (β := β) a (l₁ ++ l₂) = (dlookup (β := β) a l₁).or (dlookup (β := β) a l₂)

Tactic:
induction l₁ with
  | nil => rfl
  | 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 α
l₁ l₂ : List (Sigma β)
a : α
b : β a
nd₂ : l₂.NodupKeys (β := β)
s : l₁ <+ l₂
mem : b ∈ dlookup (β := β) a l₁
⊢ b ∈ dlookup (β := β) a l₂

Tactic:
grind [Option.mem_def, => perm_dlookup, → Sublist.exists_perm_append]

Premises used: List.perm_dlookup, List.Sublist.exists_perm_append, Option.mem_def
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq.{v + 1} (α := List (β a)) (lookupAll (β := β) a []) []

Tactic:
rfl

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

Tactic:
dif_pos rfl

Premises used: dif_pos, List.lookupAll, rfl
-- Module: Mathlib.Data.List.Sigma
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
⊢ Eq.{v + 1} (α := List (β a)) (lookupAll (β := β) a []) [] ↔
    ∀ (b : β a), ¬Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)

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) = [] ↔
      ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a' b :: l
neg :
  ∀ (h : ¬a = a'),
    lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l) = [] ↔
      ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a' b :: l
⊢ lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l) = [] ↔
    ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ 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) = [] ↔
      ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a b :: l
⊢ lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l) = [] ↔
    ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a' b :: l

Tactic:
subst a'