awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a (s :: tail)) =
    find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) (s :: tail)
have pos : s.fst (β := β) = a →
  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
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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)
⊢ Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a (s :: tail)) =
    find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) (s :: tail)
have neg : ¬s.fst (β := β) = a →
  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
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
⊢ Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a l) = find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) l
have nil : Eq (α := Option (Sigma β)) (Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a []))
  (find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) [])
Tactic: induction l with
  | nil => grind
  | cons s _ _ => by_cases s.fst = a <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β))) [])
⊢ Option.map (Sigma.mk (β := β) a) (dlookup (β := β) a l) = find? (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) l
have 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)
Tactic: induction l with
  | nil => grind
  | cons s _ _ => by_cases s.fst = a <;> grind
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys (β := β)
p : l₁ ~ l₂
⊢ dlookup (β := β) a l₁ = dlookup (β := β) a l₂
have nd₂ : l₂.NodupKeys (β := β)
Tactic: have nd₂ := (perm_nodupKeys p).mp nd₁
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l₁ l₂ : List (Sigma β)
nd₁ : l₁.NodupKeys (β := β)
p : l₁ ~ l₂
nd₂ : l₂.NodupKeys (β := β)
⊢ dlookup (β := β) a l₁ = dlookup (β := β) a l₂
have a₁ : ∀ (b : β a), dlookup (β := β) a l₁ = some b ↔ dlookup (β := β) a l₂ = some b
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
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)
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
    Option.map (g a) (dlookup (β := β) a (s :: tail))
have this : ∀ (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
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 (β := β')
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
    Option.map (g a) (dlookup (β := β) a (s :: tail))
have pos : a = s.fst (β := β) →
  dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
    Option.map (g a) (dlookup (β := β) a (s :: tail))
Tactic: by_cases a = s.fst
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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))
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
    Option.map (g a) (dlookup (β := β) a (s :: tail))
have neg : ¬a = s.fst (β := β) →
  dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) (s :: tail)) =
    Option.map (g a) (dlookup (β := β) a (s :: tail))
Tactic: by_cases a = s.fst
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 : α
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) l) = Option.map (g a) (dlookup (β := β) a l)
have nil : dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) []) = Option.map (g a) (dlookup (β := β) a [])
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 [])
⊢ dlookup (β := β') (f a) (map (Sigma.map (β₁ := β) (β₂ := β') f g) l) = Option.map (g a) (dlookup (β := β) a l)
have 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))
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]
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
α' : Type u'
inst : DecidableEq α
inst_1 : DecidableEq α'
β : Type v
l : List ((_ : α) × β)
f : α → α'
hf : Function.Injective f
a : α
⊢ dlookup (β := fun (x : α') ↦ β) (f a)
      (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) l) =
    dlookup (β := fun (x : α) ↦ β) a l
have 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)
Tactic: have := dlookup_map (β' := fun _ => β) (f := f) (g := fun _ => id)
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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 : α) ↦ β)
⊢ NodupKeys (β := fun (x : α') ↦ β)
    (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) (hd :: tl))
have 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)
Tactic: simp only [map_cons, nodupKeys_cons] at nd ⊢
Cleared hypotheses: nd
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
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)
⊢ hd.fst (β := fun (x : α) ↦ β) ∈ tl.keys (β := fun (x : α) ↦ β)
have 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
Tactic: simp only [keys, map_map] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ hd.fst (β := fun (x : α) ↦ β) ∈ map (Sigma.fst (β := fun (x : α) ↦ β)) tl
have 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
Tactic: obtain ⟨x, hm, he⟩ := mem_map.mp h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
α' : Type u'
β : Type v
f : α → α'
hf : Function.Injective f
l : List ((_ : α) × β)
nd : l.NodupKeys (β := fun (x : α) ↦ β)
⊢ NodupKeys (β := fun (x : α') ↦ β)
    (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) l)
have nil : ∀ (nd : NodupKeys (β := fun (x : α) ↦ β) []),
  NodupKeys (β := fun (x : α') ↦ β)
    (map (α := (_ : α) × β) (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) [])
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⟩
Cleared hypotheses: l, nd
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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) [])
⊢ NodupKeys (β := fun (x : α') ↦ β)
    (map (Sigma.map (β₁ := fun (x : α) ↦ β) (β₂ := fun (x : α') ↦ β) f fun (x : α) ↦ id) l)
have 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))
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⟩
Cleared hypotheses: l, nd
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type u_1
β' : α → Type u_2
f : (a : α) → β a → β' a
l : List ((a : α) × β a)
⊢ (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) l).keys (β := β') = l.keys (β := fun (a : α) ↦ β a)
have nil : (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) []).keys (β := β') = keys (β := fun (a : α) ↦ β a) []
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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) []
⊢ (map (Sigma.map (β₁ := fun (a : α) ↦ β a) (β₂ := β') id f) l).keys (β := β') = l.keys (β := fun (a : α) ↦ β a)
have 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)
Tactic: induction l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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₂)
⊢ dlookup (β := β) a (s :: tail ++ l₂) = (dlookup (β := β) a (s :: tail)).or (dlookup (β := β) a l₂)
have pos : a = s.fst (β := β) → dlookup (β := β) a (s :: tail ++ l₂) = (dlookup (β := β) a (s :: tail)).or (dlookup (β := β) a l₂)
Tactic: by_cases a = s.fst
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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₂)
⊢ dlookup (β := β) a (s :: tail ++ l₂) = (dlookup (β := β) a (s :: tail)).or (dlookup (β := β) a l₂)
have neg : ¬a = s.fst (β := β) → dlookup (β := β) a (s :: tail ++ l₂) = (dlookup (β := β) a (s :: tail)).or (dlookup (β := β) a l₂)
Tactic: by_cases a = s.fst
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
a : α
⊢ dlookup (β := β) a (l₁ ++ l₂) = (dlookup (β := β) a l₁).or (dlookup (β := β) a l₂)
have nil : dlookup (β := β) a ([] ++ l₂) = Option.or (dlookup (β := β) a []) (dlookup (β := β) a l₂)
Tactic: induction l₁ with
  | nil => rfl
  | cons s _ _ => by_cases a = s.fst <;> grind
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
l₁ l₂ : List (Sigma β)
a : α
nil : dlookup (β := β) a ([] ++ l₂) = Option.or (dlookup (β := β) a []) (dlookup (β := β) a l₂)
⊢ dlookup (β := β) a (l₁ ++ l₂) = (dlookup (β := β) a l₁).or (dlookup (β := β) a l₂)
have 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₂)
Tactic: induction l₁ with
  | nil => rfl
  | cons s _ _ => by_cases a = s.fst <;> grind
Cleared hypotheses: l₁
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l) = [] ↔
    ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a' b :: l
have pos : ∀ (h : a = a'),
  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'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l) = [] ↔
    ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a' b :: l
have neg : ∀ (h : ¬a = a'),
  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'
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
have pos : ∀ (b : β a),
  lookupAll (β := β) a (Sigma.mk (β := β) a b :: l) = [] ↔
    ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a b :: l
Tactic: subst a'
Cleared hypotheses: a', b, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ lookupAll (β := β) a (Sigma.mk (β := β) a b :: l) = [] ↔
    ∀ (b_1 : β a), ¬Sigma.mk (β := β) a b_1 ∈ Sigma.mk (β := β) a b :: l
have pos : ∃ (x : β a), ¬x = b → Sigma.mk (β := β) a x ∈ 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]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
b : β a
⊢ ∃ (x : β a), ¬x = b → Sigma.mk (β := β) a x ∈ l
have h : ¬b = b → Sigma.mk (β := β) a b ∈ l
Tactic: use b
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
⊢ (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)
have pos : ∀ (h : a = a'),
  (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: 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 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)
⊢ (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)
have neg : ∀ (h : ¬a = a'),
  (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: 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 a' : α
b : β a'
l : List (Sigma β)
h : a = a'
⊢ (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)
have pos : ∀ (b : β a), (lookupAll (β := β) a (Sigma.mk (β := β) a b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a b :: l)
Tactic: subst h
Cleared hypotheses: a', b, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ (lookupAll (β := β) a (Sigma.mk (β := β) a' b :: l)).head? = dlookup (β := β) a (Sigma.mk (β := β) a' b :: l)
have neg : a ≠ (Sigma.mk (β := β) a' b).fst (β := β)
Tactic: rw [lookupAll_cons_ne, dlookup_cons_ne, head?_lookupAll a l]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a' : α
b' : β a'
l : List (Sigma β)
⊢ b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: l
have pos : ∀ (h : a = a'),
  b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: 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
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
⊢ b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: l
have neg : ∀ (h : ¬a = a'),
  b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a' b' :: 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
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
have pos : ∀ (b' : β a),
  b ∈ lookupAll (β := β) a (Sigma.mk (β := β) a b' :: l) ↔ Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) a b' :: l
Tactic: subst h
Cleared hypotheses: a', b', h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l
have pos : ∀ (h : a = a'),
  map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l
Tactic: by_cases h : a = a'