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 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
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l
have neg : ∀ (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'
-- 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'
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l
have pos : ∀ (b' : β a),
  map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a b' :: l)) <+ 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 : α
l : List (Sigma β)
b' : β a
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a b' :: l)) <+ Sigma.mk (β := β) a b' :: l
have pos : Sigma.mk (β := β) a b' :: map (Sigma.mk (β := β) a) (lookupAll (β := β) a l) <+ Sigma.mk (β := β) a b' :: l
Tactic: simp only [lookupAll_cons_eq, List.map]
-- 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'
⊢ map (Sigma.mk (β := β) a) (lookupAll (β := β) a (Sigma.mk (β := β) a' b' :: l)) <+ Sigma.mk (β := β) a' b' :: l
have neg : map (Sigma.mk (β := β) a) (lookupAll (β := β) a l) <+ Sigma.mk (β := β) a' b' :: l
Tactic: simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ (lookupAll (β := β) a l).length ≤ 1
have this : (map (Sigma.fst (β := β)) (map (Sigma.mk (β := β) a) (lookupAll (β := β) a l))).Nodup
Tactic: have := Nodup.sublist ((lookupAll_sublist a l).map _) h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
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
⊢ (lookupAll (β := β) a l).length ≤ 1
have this₁ : (map (Sigma.fst (β := β) ∘ Sigma.mk (β := β) a) (lookupAll (β := β) a l)).Nodup
Tactic: rw [map_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ (lookupAll (β := β) a l).length ≤ 1
have rwa : (replicate (lookupAll (β := β) a l).length a).Nodup
Tactic: rwa [← nodup_replicate, ← map_const]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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₂ : α
⊢ (lookupAll (β := β) a l).length ≤ 1
have rwa₃ : (map (Function.const (β a) a) (lookupAll (β := β) a l)).Nodup
Tactic: rwa [← nodup_replicate, ← map_const]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ lookupAll (β := β) a l = (dlookup (β := β) a l).toList
have rw : lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
Tactic: rw [← head?_lookupAll]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
have h1 : (lookupAll (β := β) a l).length ≤ 1
Tactic: have h1 := lookupAll_length_le_one a h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
h1 : (lookupAll (β := β) a l).length ≤ 1
⊢ lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
have revert : ∀ (h1 : (lookupAll (β := β) a l).length ≤ 1), lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
Tactic: revert h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ ∀ (h1 : (lookupAll (β := β) a l).length ≤ 1), lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
have nil : ∀ (h1 : length.{v} (α := β a) [] ≤ 1), Eq.{v + 1} (α := List (β a)) [] (Option.toList (head? []))
Tactic: rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩)
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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? []))
⊢ ∀ (h1 : (lookupAll (β := β) a l).length ≤ 1), lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
have cons : ∀ (b : β a) (h1 : [b].length ≤ 1), [b] = [b].head?.toList
Tactic: rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩)
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ ∀ (h1 : (lookupAll (β := β) a l).length ≤ 1), lookupAll (β := β) a l = (lookupAll (β := β) a l).head?.toList
have cons₁ : ∀ (b c : β a) (l : List (β a)) (h1 : (b :: c :: l).length ≤ 1), b :: c :: l = (b :: c :: l).head?.toList
Tactic: rcases lookupAll a l with (_ | ⟨b, _ | ⟨c, l⟩⟩)
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : l.NodupKeys (β := β)
⊢ (lookupAll (β := β) a l).Nodup
have rw : (dlookup (β := β) a l).toList.Nodup
Tactic: rw [lookupAll_eq_dlookup a h]
-- 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₂
⊢ lookupAll (β := β) a l₁ = lookupAll (β := β) 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 : α
b : β a
l : List (Sigma β)
nd : l.NodupKeys (β := β)
h : Sigma.mk (β := β) a b ∈ l
⊢ kreplace (β := β) a b l = l
have 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
Tactic: refine (lookmap_congr ?_).trans (lookmap_id' (Option.guard fun (s : Sigma β) => a = s.1) ?_ _)
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ kreplace (β := β) a b l = l
have refine_2 : ∀ (a_1 b : Sigma β), b ∈ Option.guard (fun (s : Sigma β) ↦ decide (a = s.fst (β := β))) a_1 → a_1 = b
Tactic: refine (lookmap_congr ?_).trans (lookmap_id' (Option.guard fun (s : Sigma β) => a = s.1) ?_ _)
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ (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')
have 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
Tactic: dsimp [Option.guard]
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ (if a = a' then some (Sigma.mk (β := β) a b) else none) =
    if decide (a = a') = true then some (Sigma.mk (β := β) a' b') else none
have pos : a = a' → decide (a = a') = true → some (Sigma.mk (β := β) a b) = some (Sigma.mk (β := β) a' b')
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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')
⊢ (if a = a' then some (Sigma.mk (β := β) a b) else none) =
    if decide (a = a') = true then some (Sigma.mk (β := β) a' b') else none
have neg : a = a' → ¬decide (a = a') = true → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ (if a = a' then some (Sigma.mk (β := β) a b) else none) =
    if decide (a = a') = true then some (Sigma.mk (β := β) a' b') else none
have pos₁ : ¬a = a' → decide (a = a') = true → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ (if a = a' then some (Sigma.mk (β := β) a b) else none) =
    if decide (a = a') = true then some (Sigma.mk (β := β) a' b') else none
have neg₁ : ¬a = a' → ¬decide (a = a') = true → Eq (α := Option (Sigma β)) none none
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ some (Sigma.mk (β := β) a b) = some (Sigma.mk (β := β) a' b')
have pos : ∀ (b' : β a) (h' : Sigma.mk (β := β) a b' ∈ l),
  decide (a = a) = true → some (Sigma.mk (β := β) a b) = some (Sigma.mk (β := β) a b')
Tactic: subst a'
Cleared hypotheses: a', b', h', h_1, h_2
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a₁ : α
b₂_1 : β a₁
a₂ : α
b₂ : β 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 (β := β)
have dsimp : (Sigma.mk (β := β) a₂ b₂ ∈ if a = a₁ then some (Sigma.mk (β := β) a b) else none) → a₁ = a₂
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
a₁ : α
b₂_1 : β a₁
a₂ : α
b₂ : β a₂
⊢ (Sigma.mk (β := β) a₂ b₂ ∈ if a = a₁ then some (Sigma.mk (β := β) a b) else none) → a₁ = a₂
have pos : ∀ (h : a = a₁), Sigma.mk (β := β) a₂ b₂ ∈ some (Sigma.mk (β := β) a b) → a₁ = a₂
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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₂
⊢ (Sigma.mk (β := β) a₂ b₂ ∈ if a = a₁ then some (Sigma.mk (β := β) a b) else none) → a₁ = a₂
have neg : ∀ (h : ¬a = a₁), Membership.mem (γ := Option (Sigma β)) none (Sigma.mk (β := β) a₂ b₂) → a₁ = a₂
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
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₁
have 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
Tactic: refine nd.pairwise_ne.imp ?_
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
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
⊢ x = y ∧ z = w
have 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
Tactic: split_ifs at h₁ h₂ with h_2 h_1
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
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
⊢ x = y ∧ z = w
have 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
Tactic: split_ifs at h₁ h₂ with h_2 h_1
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
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
⊢ x = y ∧ z = w
have 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
Tactic: split_ifs at h₁ h₂ with h_2 h_1
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
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
⊢ x = y ∧ z = w
have 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
Tactic: split_ifs at h₁ h₂ with h_2 h_1
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
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)
⊢ x = y ∧ z = w
have pos : x = y ∧ Sigma.mk (β := β) a b = w
Tactic: cases h₁
Cleared hypotheses: z, h₁
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
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
⊢ x = y ∧ z = w
have neg : x = y ∧ Sigma.mk (β := β) a b = w
Tactic: cases h₁
Cleared hypotheses: z, h₁
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
l₁ l₂ : List (Sigma β)
nd : l₁.NodupKeys (β := β)
x y : Sigma β
h : x.fst (β := β) ≠ y.fst (β := β)
w : Sigma β
h_2 : a = x.fst (β := β)
h_1 : a = y.fst (β := β)
h₂ : w ∈ some (Sigma.mk (β := β) a b)
⊢ x = y ∧ Sigma.mk (β := β) a b = w
have pos : x = y ∧ Sigma.mk (β := β) a b = Sigma.mk (β := β) a b
Tactic: cases h₂
Cleared hypotheses: w, h₂
-- Lean 4 proof step from Mathlib.Data.List.Sigma (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
head : Sigma β
tail : List (Sigma β)
ih : ∀ (h : ¬a ∈ tail.keys (β := β)), kerase (β := β) a tail = tail
h : ¬a ∈ (head :: tail).keys (β := β)
⊢ kerase (β := β) a (head :: tail) = head :: tail
have h₁ : ¬a = head.fst (β := β) ∧ ¬a ∈ tail.keys (β := β)
Tactic: simp [not_or] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : ¬a ∈ l.keys (β := β)
⊢ kerase (β := β) a l = l
have nil : ∀ (h : ¬Membership.mem (γ := List α) (keys (β := β) []) a), Eq (α := List (Sigma β)) (kerase (β := β) a []) []
Tactic: induction l with
  | nil => rfl
  | cons _ _ ih => simp [not_or] at h; simp [h.1, ih h.2]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
l : List (Sigma β)
h : ¬a ∈ l.keys (β := β)
nil : ∀ (h : ¬Membership.mem (γ := List α) (keys (β := β) []) a), Eq (α := List (Sigma β)) (kerase (β := β) a []) []
⊢ kerase (β := β) a l = l
have cons : ∀ (head : Sigma β) (tail : List (Sigma β)) (ih : ∀ (h : ¬a ∈ tail.keys (β := β)), kerase (β := β) a tail = tail)
  (h : ¬a ∈ (head :: tail).keys (β := β)), kerase (β := β) a (head :: tail) = head :: tail
Tactic: induction l with
  | nil => rfl
  | cons _ _ ih => simp [not_or] at h; simp [h.1, ih h.2]
Cleared hypotheses: l, h
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys (β := β)
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
have pos : ∀ (e : a = hd.fst (β := β)),
  ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
Tactic: by_cases e : a = hd.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys (β := β)
pos :
  ∀ (e : a = hd.fst (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
have neg : ∀ (e : ¬a = hd.fst (β := β)),
  ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
Tactic: by_cases e : a = hd.1
-- Lean 4 proof step from Mathlib.Data.List.Sigma (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
hd : Sigma β
tl : List (Sigma β)
ih :
  ∀ (h : a ∈ tl.keys (β := β)),
    ∃ (b : β a),
      ∃ (l₁ : List (Sigma β)),
        ∃ (l₂ : List (Sigma β)),
          ¬a ∈ l₁.keys (β := β) ∧ tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a tl = l₁ ++ l₂
h : a ∈ (hd :: tl).keys (β := β)
e : a = hd.fst (β := β)
⊢ ∃ (b : β a),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬a ∈ l₁.keys (β := β) ∧ hd :: tl = l₁ ++ Sigma.mk (β := β) a b :: l₂ ∧ kerase (β := β) a (hd :: tl) = l₁ ++ l₂
have pos : ∀
  (ih :
    ∀ (h : hd.fst (β := β) ∈ tl.keys (β := β)),
      ∃ (b : β (hd.fst (β := β))),
        ∃ (l₁ : List (Sigma β)),
          ∃ (l₂ : List (Sigma β)),
            ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
              tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧ kerase (β := β) (hd.fst (β := β)) tl = l₁ ++ l₂)
  (h : hd.fst (β := β) ∈ (hd :: tl).keys (β := β)),
  ∃ (b : β (hd.fst (β := β))),
    ∃ (l₁ : List (Sigma β)),
      ∃ (l₂ : List (Sigma β)),
        ¬hd.fst (β := β) ∈ l₁.keys (β := β) ∧
          hd :: tl = l₁ ++ Sigma.mk (β := β) (hd.fst (β := β)) b :: l₂ ∧
            kerase (β := β) (hd.fst (β := β)) (hd :: tl) = l₁ ++ l₂
Tactic: subst e
Cleared hypotheses: a, ih, h, e