awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
refine_1 :
  ∀ (l₁ l₂ : List (Sigma β)) (p : l₁ ≈ l₂)
    (h₁ :
      Part.Dom.{u_1} (α := γ)
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₁))
    (h₂ :
      Part.Dom.{u_1} (α := γ)
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₂)),
    Part.get
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₁)
        h₁ =
      Part.get
        ((fun (l : List (Sigma β)) ↦
            ({ Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) } :
              Part γ))
          l₂)
        h₂
⊢ γ
have refine_2 : Part.Dom.{u_1} (α := γ)
  (Quotient.liftOn (s.entries (β := β))
    (fun (l : List (Sigma β)) ↦
      { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
    sorry)
Tactic: refine
    (Quotient.liftOn s.entries
      (fun (l : List (Sigma β)) => (⟨_, fun nd => f ⟨l, nd⟩⟩ : Part γ))
      (fun l₁ l₂ p => Part.ext' (perm_nodupKeys p) ?_) : Part γ).get ?_
-- Lean 4 proof step from Mathlib.Data.Finmap (hypothesis)
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
⊢ Part.Dom.{u_1} (α := γ)
    (Quotient.liftOn (s.entries (β := β))
      (fun (l : List (Sigma β)) ↦
        { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
      ⋯)
have this : s.entries (β := β).NodupKeys (β := β)
Tactic: have := s.nodupKeys
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
this : s.entries (β := β).NodupKeys (β := β)
⊢ Part.Dom.{u_1} (α := γ)
    (Quotient.liftOn (s.entries (β := β))
      (fun (l : List (Sigma β)) ↦
        { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
      ⋯)
have refine_2 : ∀ (this : s.entries (β := β).NodupKeys (β := β)),
  Part.Dom.{u_1} (α := γ)
    (Quotient.liftOn (s.entries (β := β))
      (fun (l : List (Sigma β)) ↦
        { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
      sorry)
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : Finmap β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
⊢ ∀ (this : s.entries (β := β).NodupKeys (β := β)),
    Part.Dom.{u_1} (α := γ)
      (Quotient.liftOn (s.entries (β := β))
        (fun (l : List (Sigma β)) ↦
          { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
        ⋯)
have refine_2 : ∀ (x : Multiset (Sigma β)) (l : List (Sigma β))
  (this : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)),
  Part.Dom.{u_1} (α := γ)
    (Quotient.liftOn (s := isSetoid (Sigma β))
      (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)
      (fun (l : List (Sigma β)) ↦
        { Dom := l.NodupKeys (β := β), get := fun (nd : l.NodupKeys (β := β)) ↦ f (AList.mk (β := β) l nd) })
      sorry)
Tactic: rcases s.entries with ⟨l⟩
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s : AList β
f : AList β → γ
H : ∀ (a b : AList β), a.entries (β := β) ~ b.entries (β := β) → f a = f b
⊢ s.toFinmap (β := β).liftOn (β := β) f H = f s
have mk : ∀ (entries : List (Sigma β)) (nodupKeys : entries.NodupKeys (β := β)),
  (AList.mk (β := β) entries nodupKeys).toFinmap (β := β).liftOn (β := β) f H = f (AList.mk (β := β) entries nodupKeys)
Tactic: cases s
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finmap (hypothesis)
Goal:
α : Type u
β : α → Type v
γ : Type u_1
s₁ s₂ : Finmap β
f : AList β → AList β → γ
H :
  ∀ (a₁ b₁ a₂ b₂ : AList β),
    a₁.entries (β := β) ~ a₂.entries (β := β) → b₁.entries (β := β) ~ b₂.entries (β := β) → f a₁ b₁ = f a₂ b₂
a₁ a₂ : AList β
p : a₁.entries (β := β) ~ a₂.entries (β := β)
⊢ Eq.{u_1 + 1} (α := γ) ((fun (l₁ : AList β) ↦ s₂.liftOn (β := β) (f l₁) ⋯) a₁)
    ((fun (l₁ : AList β) ↦ s₂.liftOn (β := β) (f l₁) ⋯) a₂)
have H' : f a₁ = f a₂
Tactic: have H' : f a₁ = f a₂ := funext fun _ => H _ _ _ _ p (Perm.refl _)
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
C : Finmap β → Prop
s : Finmap β
H : ∀ (a : AList β), C (a.toFinmap (β := β))
⊢ C s
have mk : ∀ (entries : Multiset (Sigma β)) (a : List (Sigma β))
  (h : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) a)),
  C (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) a) h)
Tactic: rcases s with ⟨⟨a⟩, h⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : List (Sigma β)
⊢ lookup (β := β) a (s.toFinmap (β := β)) = dlookup (β := β) a s
have rw : lookup (β := β) a (s.toAList (β := β).toFinmap (β := β)) = dlookup (β := β) a s
Tactic: rw [List.toFinmap, lookup_toFinmap, lookup_to_alist]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : List (Sigma β)
rw : lookup (β := β) a (s.toAList (β := β).toFinmap (β := β)) = dlookup (β := β) a s
⊢ lookup (β := β) a (s.toFinmap (β := β)) = dlookup (β := β) a s
have rw₁ : AList.lookup (β := β) a (s.toAList (β := β)) = dlookup (β := β) a s
Tactic: rw [List.toFinmap, lookup_toFinmap, lookup_to_alist]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : List (Sigma β)
rw : lookup (β := β) a (s.toAList (β := β).toFinmap (β := β)) = dlookup (β := β) a s
rw₁ : AList.lookup (β := β) a (s.toAList (β := β)) = dlookup (β := β) a s
⊢ lookup (β := β) a (s.toFinmap (β := β)) = dlookup (β := β) a s
have rw₂ : dlookup (β := β) a s = dlookup (β := β) a s
Tactic: rw [List.toFinmap, lookup_toFinmap, lookup_to_alist]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
a : α
b : β a
⊢ b ∈ lookup (β := β) a s ↔ Sigma.mk (β := β) a b ∈ s.entries (β := β)
have mk : ∀ (entries : Multiset (Sigma β)) (l : List (Sigma β))
  (hl : Multiset.NodupKeys (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l)),
  b ∈ lookup (β := β) a (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l) hl) ↔
    Sigma.mk (β := β) a b ∈
      (mk (β := β) (Quot.mk (⇑(isSetoid (Sigma β)) : List (Sigma β) → List (Sigma β) → Prop) l) hl).entries (β := β)
Tactic: rcases s with ⟨⟨l⟩, hl⟩
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
⊢ (s.keys (β := β).sigma (α := β) fun (i : α) ↦ (lookup (β := β) i s).toFinset) =
    { val := s.entries (β := β), nodup := ⋯ : Finset ((i : α) × β i) }
have h : ∀ (x : (i : α) × β i),
  Membership.mem (γ := Finset ((i : α) × β i))
      (s.keys (β := β).sigma (α := β) fun (i : α) ↦ (lookup (β := β) i s).toFinset) x ↔
    x ∈ { val := s.entries (β := β), nodup := sorry : Finset ((i : α) × β i) }
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finmap (hypothesis)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s : Finmap β
x : (i : α) × β i
⊢ Membership.mem (γ := Finset ((i : α) × β i))
      (s.keys (β := β).sigma (α := β) fun (i : α) ↦ (lookup (β := β) i s).toFinset) x ↔
    x ∈ { val := s.entries (β := β), nodup := ⋯ : Finset ((i : α) × β i) }
have this : x ∈ s.entries (β := β) → x.fst (β := fun (i : α) ↦ β i) ∈ s.keys (β := β)
Tactic: have : x ∈ s.entries → x.1 ∈ s.keys := Multiset.mem_map_of_mem _
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
⊢ lookup (β := β) a (singleton (β := β) a b) = some b
have rw : lookup (β := β) a ((AList.singleton (β := β) a b).toFinmap (β := β)) = some b
Tactic: rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
rw : lookup (β := β) a ((AList.singleton (β := β) a b).toFinmap (β := β)) = some b
⊢ lookup (β := β) a (singleton (β := β) a b) = some b
have rw₁ : AList.lookup (β := β) a (AList.singleton (β := β) a b) = some b
Tactic: rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
rw : lookup (β := β) a ((AList.singleton (β := β) a b).toFinmap (β := β)) = some b
rw₁ : AList.lookup (β := β) a (AList.singleton (β := β) a b) = some b
⊢ lookup (β := β) a (singleton (β := β) a b) = some b
have rw₂ : AList.lookup (β := β) a (AList.mk (β := β) [Sigma.mk (β := β) a b] sorry) = some b
Tactic: rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
rw : lookup (β := β) a ((AList.singleton (β := β) a b).toFinmap (β := β)) = some b
rw₁ : AList.lookup (β := β) a (AList.singleton (β := β) a b) = some b
rw₂ : AList.lookup (β := β) a (AList.mk (β := β) [Sigma.mk (β := β) a b] ⋯) = some b
⊢ lookup (β := β) a (singleton (β := β) a b) = some b
have rw₃ : dlookup (β := β) a ((AList.mk (β := β) [Sigma.mk (β := β) a b] sorry).entries (β := β)) = some b
Tactic: rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
b : β a
rw : lookup (β := β) a ((AList.singleton (β := β) a b).toFinmap (β := β)) = some b
rw₁ : AList.lookup (β := β) a (AList.singleton (β := β) a b) = some b
rw₂ : AList.lookup (β := β) a (AList.mk (β := β) [Sigma.mk (β := β) a b] ⋯) = some b
rw₃ : dlookup (β := β) a ((AList.mk (β := β) [Sigma.mk (β := β) a b] ⋯).entries (β := β)) = some b
⊢ lookup (β := β) a (singleton (β := β) a b) = some b
have rw₄ : some b = some b
Tactic: rw [singleton, lookup_toFinmap, AList.singleton, AList.lookup, dlookup_cons_eq]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup (β := β) x (s₁.entries (β := β)) = dlookup (β := β) x (s₂.entries (β := β))
⊢ s₁.toFinmap (β := β) = s₂.toFinmap (β := β)
have rw : s₁.entries (β := β) ~ s₂.entries (β := β)
Tactic: rw [AList.toFinmap_eq]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup (β := β) x (s₁.entries (β := β)) = dlookup (β := β) x (s₂.entries (β := β))
⊢ s₁.entries (β := β) ~ s₂.entries (β := β)
have apply : ∀ (x : α) (y : β x), y ∈ dlookup (β := β) x (s₁.entries (β := β)) ↔ y ∈ dlookup (β := β) x (s₂.entries (β := β))
Tactic: apply lookup_ext s₁.nodupKeys s₂.nodupKeys
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
s₁_1 s₂_1 : Finmap β
s₁ s₂ : AList β
h : ∀ (x : α), dlookup (β := β) x (s₁.entries (β := β)) = dlookup (β := β) x (s₂.entries (β := β))
x : α
y : β x
⊢ y ∈ dlookup (β := β) x (s₁.entries (β := β)) ↔ y ∈ dlookup (β := β) x (s₂.entries (β := β))
have rw : y ∈ dlookup (β := β) x (s₂.entries (β := β)) ↔ y ∈ dlookup (β := β) x (s₂.entries (β := β))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ Multiset.NodupKeys (β := β)
    (Finset.val
      ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
        ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
have refine : ∀ (x : (a : α) × β a),
  Membership.mem (γ := Multiset ((a : α) × β a))
      (Finset.val
        ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
          ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
      x →
    ∀ (y : (a : α) × β a),
      Membership.mem (γ := Multiset ((a : α) × β a))
          (Finset.val
            ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
              ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
          y →
        x.fst (β := fun (a : α) ↦ β a) = y.fst (β := fun (a : α) ↦ β a) → x = y
Tactic: refine Multiset.nodup_keys.1 ((Finset.nodup _).map_on ?_)
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
⊢ ∀ (x : (a : α) × β a),
    Membership.mem (γ := Multiset ((a : α) × β a))
        (Finset.val
          ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
            ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
        x →
      ∀ (y : (a : α) × β a),
        Membership.mem (γ := Multiset ((a : α) × β a))
            (Finset.val
              ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
            y →
          x.fst (β := fun (a : α) ↦ β a) = y.fst (β := fun (a : α) ↦ β a) → x = y
have simp : ∀ (x : (a : α) × β a),
  x.fst (β := fun (i : α) ↦ β i) ∈ (↑f : Finset α × ((a : α) → Option (β a))).1 ∧
      (↑f : Finset α × ((a : α) → Option (β a))).2 (x.fst (β := fun (i : α) ↦ β i)) =
        some (x.snd (β := fun (i : α) ↦ β i)) →
    ∀ (y : (a : α) × β a),
      y.fst (β := fun (i : α) ↦ β i) ∈ (↑f : Finset α × ((a : α) → Option (β a))).1 ∧
          (↑f : Finset α × ((a : α) → Option (β a))).2 (y.fst (β := fun (i : α) ↦ β i)) =
            some (y.snd (β := fun (i : α) ↦ β i)) →
        x.fst (β := fun (i : α) ↦ β i) = y.fst (β := fun (i : α) ↦ β i) → x = y
Tactic: simp only [Finset.mem_val, Finset.mem_sigma, Option.mem_toFinset, Option.mem_def]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
x : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
s : Finset α
f : (a : α) → Option (β a)
hf : ∀ (i : α), (f i).isSome = true ↔ i ∈ s
⊢ Eq (α := { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 })
    ((fun (s : Finmap β) ↦
        (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
            (s.keys (β := β), fun (i : α) ↦ lookup (β := β) i s) ⋯ :
          { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }))
      ((fun (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) ↦
          mk (β := β)
            (Finset.val
              ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
            ⋯)
        (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
          (s, f) hf)))
    (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s, f)
      hf)
have a : ∀ (a : α),
  Membership.mem (γ := Finset α)
      (↑((fun (s : Finmap β) ↦
                (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                    ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s.keys (β := β), fun (i : α) ↦ lookup (β := β) i s) sorry :
                  { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }))
              ((fun (f : { f : Finset α × ((a : α) → Option (β a)) // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }) ↦
                  mk (β := β)
                    (Finset.val
                      ((↑f : Finset α × ((a : α) → Option (β a))).1.sigma (α := β) fun (i : α) ↦
                        ((↑f : Finset α × ((a : α) → Option (β a))).2 i).toFinset))
                    sorry)
                (Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦
                  ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1) (s, f) hf))) :
          Finset α × ((a : α) → Option (β a))).1
      a ↔
    a ∈
      (↑(Subtype.mk (p := fun (f : Finset α × ((a : α) → Option (β a))) ↦ ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1)
              (s, f) hf) :
          Finset α × ((a : α) → Option (β a))).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x : Bool
x_1 : α
x_2 : β x_1
x_3 : α
simp_rw simp_rw₁ : ∀ (b₂ : β x_3), (x || f x_1 x_2 || f x_3 b₂) = (x || f x_3 b₂ || f x_1 x_2)
⊢ ∀ (b₂ : β x_3),
    Eq (α := Bool)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) x x_1 x_2) x_3
        b₂)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) x x_3 b₂) x_1
        x_2)
have simp_rw₂ : ∀ (b₂ : β x_3), (x || (f x_1 x_2 || f x_3 b₂)) = (x || (f x_3 b₂ || f x_1 x_2))
Tactic: simp_rw [Bool.or_assoc, Bool.or_comm, imp_true_iff]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x : Bool
x_1 : α
x_2 : β x_1
x_3 : α
simp_rw simp_rw₁ : ∀ (b₂ : β x_3), (x || f x_1 x_2 || f x_3 b₂) = (x || f x_3 b₂ || f x_1 x_2)
simp_rw₂ : ∀ (b₂ : β x_3), (x || (f x_1 x_2 || f x_3 b₂)) = (x || (f x_3 b₂ || f x_1 x_2))
⊢ ∀ (b₂ : β x_3),
    Eq (α := Bool)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) x x_1 x_2) x_3
        b₂)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x || f y z) x x_3 b₂) x_1
        x_2)
have simp_rw₃ : ∀ (b₂ : β x_3), True
Tactic: simp_rw [Bool.or_assoc, Bool.or_comm, imp_true_iff]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x : Bool
x_1 : α
x_2 : β x_1
x_3 : α
simp_rw simp_rw₁ : ∀ (b₂ : β x_3), (x && f x_1 x_2 && f x_3 b₂) = (x && f x_3 b₂ && f x_1 x_2)
⊢ ∀ (b₂ : β x_3),
    Eq (α := Bool)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) x x_1 x_2) x_3
        b₂)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) x x_3 b₂) x_1
        x_2)
have simp_rw₂ : ∀ (b₂ : β x_3), (x && (f x_1 x_2 && f x_3 b₂)) = (x && (f x_3 b₂ && f x_1 x_2))
Tactic: simp_rw [Bool.and_assoc, Bool.and_comm, imp_true_iff]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
f : (x : α) → β x → Bool
s : Finmap β
x : Bool
x_1 : α
x_2 : β x_1
x_3 : α
simp_rw simp_rw₁ : ∀ (b₂ : β x_3), (x && f x_1 x_2 && f x_3 b₂) = (x && f x_3 b₂ && f x_1 x_2)
simp_rw₂ : ∀ (b₂ : β x_3), (x && (f x_1 x_2 && f x_3 b₂)) = (x && (f x_3 b₂ && f x_1 x_2))
⊢ ∀ (b₂ : β x_3),
    Eq (α := Bool)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) x x_1 x_2) x_3
        b₂)
      ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) ((fun (x : Bool) (y : α) (z : β y) ↦ x && f y z) x x_3 b₂) x_1
        x_2)
have simp_rw₃ : ∀ (b₂ : β x_3), True
Tactic: simp_rw [Bool.and_assoc, Bool.and_comm, imp_true_iff]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
⊢ a ∉ erase (β := β) a s
have rw : a = a ∨ a ∉ s
Tactic: rw [mem_erase, not_and_or, not_not]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s : Finmap β
⊢ a = a ∨ a ∉ s
have h : a = a
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
x : Sigma β
xs : List (Sigma β)
tail_ih : a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
⊢ a ∈ (x :: xs).toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ x :: xs
have cons : ∀ (fst_i : α) (snd_i : β fst_i),
  a ∈ (Sigma.mk (β := β) fst_i snd_i :: xs).toFinmap (β := β) ↔
    ∃ (b : β a), Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) fst_i snd_i :: xs
Tactic: obtain ⟨fst_i, snd_i⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih : a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
fst_i : α
snd_i : β fst_i
⊢ a ∈ (Sigma.mk (β := β) fst_i snd_i :: xs).toFinmap (β := β) ↔
    ∃ (b : β a), Sigma.mk (β := β) a b ∈ Sigma.mk (β := β) fst_i snd_i :: xs
have cons : (a = fst_i ∨ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs) ↔
  (a = fst_i ∧ ∃ (x : β a), x ≍ snd_i) ∨ ∃ (x : β a), Sigma.mk (β := β) a x ∈ xs
Tactic: simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
tail_ih : a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
fst_i : α
snd_i : β fst_i
⊢ (a = fst_i ∨ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs) ↔
    (a = fst_i ∧ ∃ (x : β a), x ≍ snd_i) ∨ ∃ (x : β a), Sigma.mk (β := β) a x ∈ xs
have cons : a = fst_i → ∃ (x : β a), x ≍ snd_i
Tactic: refine (or_congr_left <| and_iff_left_of_imp ?_).symm
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
⊢ a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
have nil : Membership.mem (γ := Finmap β) (List.toFinmap (β := β) []) a ↔
  ∃ (b : β a), Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)
Tactic: induction xs with
  | nil => simp only [toFinmap_nil, notMem_empty, not_mem_nil, exists_false]
  | cons x xs =>
    obtain ⟨fst_i, snd_i⟩ := x
    simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]
    refine (or_congr_left <| and_iff_left_of_imp ?_).symm
    rintro rfl
    simp only [exists_eq, heq_iff_eq]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
xs : List (Sigma β)
nil :
  Membership.mem (γ := Finmap β) (List.toFinmap (β := β) []) a ↔
    ∃ (b : β a), Membership.mem (γ := List (Sigma β)) [] (Sigma.mk (β := β) a b)
⊢ a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs
have cons : ∀ (x : Sigma β) (xs : List (Sigma β)),
  (a ∈ xs.toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ xs) →
    (a ∈ (x :: xs).toFinmap (β := β) ↔ ∃ (b : β a), Sigma.mk (β := β) a b ∈ x :: xs)
Tactic: induction xs with
  | nil => simp only [toFinmap_nil, notMem_empty, not_mem_nil, exists_false]
  | cons x xs =>
    obtain ⟨fst_i, snd_i⟩ := x
    simp only [toFinmap_cons, *, exists_or, mem_cons, mem_insert, exists_and_left, Sigma.mk.inj_iff]
    refine (or_congr_left <| and_iff_left_of_imp ?_).symm
    rintro rfl
    simp only [exists_eq, heq_iff_eq]
Cleared hypotheses: xs
-- Lean 4 proof step from Mathlib.Data.Finmap (goal)
Goal:
α : Type u
β : α → Type v
inst : DecidableEq α
a : α
s₁ s₂ : Finmap β
h : a ∉ s₂
⊢ lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
have pos : ∀ (h' : a ∈ s₁), lookup (β := β) a (s₁ ∪ s₂) = lookup (β := β) a s₁
Tactic: by_cases h' : a ∈ s₁