awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Update (goal)
Goal:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst : DecidableEq ι
s t : Finset ι
y : (i : ↥s) → π (↑i : ι)
z : (i : ↥t) → π (↑i : ι)
h : s = t
⊢ updateFinset (π := π) x s y =
    updateFinset (π := π) x t fun (i : ↥t) ↦ y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) ⋯)
have subst : ∀ {z : (i : ↥s) → π (↑i : ι)},
  updateFinset (π := π) x s y =
    updateFinset (π := π) x s fun (i : ↥s) ↦ y (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) sorry)
Tactic: subst h
Cleared hypotheses: t, z, h
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
⊢ (List.map Prod.toSigma f.graph.toList).NodupKeys (β := fun (_x : α) ↦ M)
have rw : ∀ x ∈ f.graph.toList, ∀ y ∈ f.graph.toList, x.1 = y.1 → x = y
Tactic: rw [List.NodupKeys, List.keys, List.map_map, Prod.fst_comp_toSigma, List.nodup_map_iff_inj_on]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
rw : ∀ x ∈ f.graph.toList, ∀ y ∈ f.graph.toList, x.1 = y.1 → x = y
⊢ (List.map Prod.toSigma f.graph.toList).NodupKeys (β := fun (_x : α) ↦ M)
have rw₁ : f.graph.toList.Nodup
Tactic: rw [List.NodupKeys, List.keys, List.map_map, Prod.fst_comp_toSigma, List.nodup_map_iff_inj_on]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
b : α
m : M
hb : (b, m) ∈ f.graph.toList
n : M
hc : (b, n) ∈ f.graph.toList
⊢ (b, m) = (b, n)
have rw : ∀ (hb : (f : (a : α) → M) (b, m).1 = (b, m).2 ∧ (b, m).2 ≠ 0) (n : M)
  (hc : (f : (a : α) → M) (b, n).1 = (b, n).2 ∧ (b, n).2 ≠ 0), (b, m) = (b, n)
Tactic: rw [Finset.mem_toList, Finsupp.mem_graph_iff] at hb hc
Cleared hypotheses: hb, n, hc
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
b : α
m : M
hb : (f : (a : α) → M) b = m ∧ ¬m = 0
n : M
hc : (f : (a : α) → M) b = n ∧ ¬n = 0
⊢ (b, m) = (b, n)
have rw : (b, m) = (b, (f : (a : α) → M) b)
Tactic: rw [← hc.1, hb.1]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
b : α
m : M
hb : (f : (a : α) → M) b = m ∧ ¬m = 0
n : M
hc : (f : (a : α) → M) b = n ∧ ¬n = 0
rw : (b, m) = (b, (f : (a : α) → M) b)
⊢ (b, m) = (b, n)
have rw₁ : (b, m) = (b, m)
Tactic: rw [← hc.1, hb.1]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
⊢ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset = f.support
have h : ∀ (a : α), a ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ a ∈ f.support
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
have rw : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
rw : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
have rw₁ : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
rw : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
rw₁ : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
have rw₂ : x ∈ f.support ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
rw : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
rw₁ : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
rw₂ : x ∈ f.support ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
have rw₃ : Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
have classical : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
classical : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
have classical₁ : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
classical : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
classical₁ :
  x ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
have classical₂ : x ∈ f.support ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
x : α
classical : x ∈ f.toAList.keys (β := fun (_x : α) ↦ M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
classical₁ :
  x ∈ f.toAList.keys (β := fun (_x : α) ↦ M).toFinset ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
classical₂ : x ∈ f.support ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
⊢ x ∈ f.toAList ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
have classical₃ : Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M) ↔ Ne.{u_2 + 1} (α := M) ((f : (a : α) → M) x : M) (0 : M)
Tactic: classical rw [AList.mem_keys, ← List.mem_toFinset, toAList_keys_toFinset, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
⊢ Finset α
have haveI : (this : DecidableEq α) → Finset α
Tactic: haveI := Classical.decEq α
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
this : DecidableEq α
⊢ Finset α
have haveI : (this : DecidableEq M) → Finset α
Tactic: haveI := Classical.decEq M
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
⊢ a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
              (l.entries (β := fun (_x : α) ↦ M))).keys
          (β := fun (_x : α) ↦ M).toFinset ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
have simp_rw : (∃ b ∈ lookup (β := fun (_x : α) ↦ M) a l, decide (b ≠ 0) = true) ↔ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
Tactic: simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
⊢ (∃ b ∈ lookup (β := fun (_x : α) ↦ M) a l, decide (b ≠ 0) = true) ↔ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
have none : (∃ (b : M), Membership.mem (γ := Option M) none b ∧ decide (b ≠ 0) = true) ↔
  Ne.{u_2 + 1} (α := M) (Option.getD none 0) 0
Tactic: cases lookup a l
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
none :
  (∃ (b : M), Membership.mem (γ := Option M) Option.none b ∧ decide (b ≠ 0) = true) ↔
    Ne.{u_2 + 1} (α := M) (Option.getD Option.none 0) 0
⊢ (∃ b ∈ lookup (β := fun (_x : α) ↦ M) a l, decide (b ≠ 0) = true) ↔ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
have some : ∀ (val : M), (∃ b ∈ some val, decide (b ≠ 0) = true) ↔ (some val).getD 0 ≠ 0
Tactic: cases lookup a l
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
⊢ a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
              (l.entries (β := fun (_x : α) ↦ M))).keys
          (β := fun (_x : α) ↦ M).toFinset ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
have simp_rw : a ∈
    (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
          (l.entries (β := fun (_x : α) ↦ M))).keys
      (β := fun (_x : α) ↦ M) ↔
  (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
Tactic: classical
      simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
      cases lookup a l <;> simp
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
simp_rw :
  a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
            (l.entries (β := fun (_x : α) ↦ M))).keys
        (β := fun (_x : α) ↦ M) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
⊢ a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
              (l.entries (β := fun (_x : α) ↦ M))).keys
          (β := fun (_x : α) ↦ M).toFinset ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
have simp_rw₁ : (∃ (b : M),
    Sigma.mk (β := fun (_x : α) ↦ M) a b ∈
      filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0)) (l.entries (β := fun (_x : α) ↦ M))) ↔
  (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
Tactic: classical
      simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
      cases lookup a l <;> simp
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
simp_rw :
  a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
            (l.entries (β := fun (_x : α) ↦ M))).keys
        (β := fun (_x : α) ↦ M) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
simp_rw₁ :
  (∃ (b : M),
      Sigma.mk (β := fun (_x : α) ↦ M) a b ∈
        filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
          (l.entries (β := fun (_x : α) ↦ M))) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
⊢ a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
              (l.entries (β := fun (_x : α) ↦ M))).keys
          (β := fun (_x : α) ↦ M).toFinset ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
have simp_rw₂ : (∃ (b : M), Sigma.mk (β := fun (_x : α) ↦ M) a b ∈ l.entries (β := fun (_x : α) ↦ M) ∧ decide (b ≠ 0) = true) ↔
  (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
Tactic: classical
      simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
      cases lookup a l <;> simp
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
simp_rw :
  a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
            (l.entries (β := fun (_x : α) ↦ M))).keys
        (β := fun (_x : α) ↦ M) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
simp_rw₁ :
  (∃ (b : M),
      Sigma.mk (β := fun (_x : α) ↦ M) a b ∈
        filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
          (l.entries (β := fun (_x : α) ↦ M))) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
simp_rw₂ :
  (∃ (b : M), Sigma.mk (β := fun (_x : α) ↦ M) a b ∈ l.entries (β := fun (_x : α) ↦ M) ∧ decide (b ≠ 0) = true) ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
⊢ a ∈
      (filter (fun (x : (_ : α) × M) ↦ decide (x.snd (β := fun (_x : α) ↦ M) ≠ 0))
              (l.entries (β := fun (_x : α) ↦ M))).keys
          (β := fun (_x : α) ↦ M).toFinset ↔
    (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
have simp_rw₃ : (∃ b ∈ lookup (β := fun (_x : α) ↦ M) a l, decide (b ≠ 0) = true) ↔ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 ≠ 0
Tactic: classical
      simp_rw [mem_toFinset, List.mem_keys, List.mem_filter, ← mem_lookup_iff]
      cases lookup a l <;> simp
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
⊢ (l.lookupFinsupp : (a : α) → M) a = (lookup (β := fun (_x : α) ↦ M) a l).getD 0
have simp : (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = (lookup (β := fun (_x : α) ↦ M) a l).getD 0
Tactic: simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
x : M
hx : x ≠ 0
⊢ (l.lookupFinsupp : (a : α) → M) a = x ↔ x ∈ lookup (β := fun (_x : α) ↦ M) a l
have rw : (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = x ↔ x ∈ lookup (β := fun (_x : α) ↦ M) a l
Tactic: rw [lookupFinsupp_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
x : M
hx : x ≠ 0
⊢ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = x ↔ x ∈ lookup (β := fun (_x : α) ↦ M) a l
have none : Option.getD none 0 = x ↔ Membership.mem (γ := Option M) none x
Tactic: rcases lookup a l with - | m
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
x : M
hx : x ≠ 0
none : Option.getD Option.none 0 = x ↔ Membership.mem (γ := Option M) Option.none x
⊢ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = x ↔ x ∈ lookup (β := fun (_x : α) ↦ M) a l
have some : ∀ (m : M), (some m).getD 0 = x ↔ x ∈ some m
Tactic: rcases lookup a l with - | m
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((l.lookupFinsupp : (a : α) → M) a : M) (0 : M) ↔ a ∉ l ∨ 0 ∈ lookup (β := fun (_x : α) ↦ M) a l
have rw : (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = 0 ↔
  lookup (β := fun (_x : α) ↦ M) a l = none ∨ 0 ∈ lookup (β := fun (_x : α) ↦ M) a l
Tactic: rw [lookupFinsupp_apply, ← lookup_eq_none]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
⊢ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = 0 ↔
    lookup (β := fun (_x : α) ↦ M) a l = none ∨ 0 ∈ lookup (β := fun (_x : α) ↦ M) a l
have none : Eq.{u_2 + 1} (α := M) (Option.getD none 0) 0 ↔
  Eq.{u_2 + 1} (α := Option M) none none ∨ Membership.mem (γ := Option M) none 0
Tactic: rcases lookup a l with - | m
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
none :
  Eq.{u_2 + 1} (α := M) (Option.getD Option.none 0) 0 ↔
    Eq.{u_2 + 1} (α := Option M) Option.none Option.none ∨ Membership.mem (γ := Option M) Option.none 0
⊢ (lookup (β := fun (_x : α) ↦ M) a l).getD 0 = 0 ↔
    lookup (β := fun (_x : α) ↦ M) a l = Option.none ∨ 0 ∈ lookup (β := fun (_x : α) ↦ M) a l
have some : ∀ (m : M), (some m).getD 0 = 0 ↔ some m = Option.none ∨ 0 ∈ some m
Tactic: rcases lookup a l with - | m
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
m : M
⊢ Eq (α := α →₀ M) (insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp (Finsupp.update l.lookupFinsupp a m)
have h : ∀ (b : α),
  Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
    ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
m : M
b : α
⊢ Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
    ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
have pos : ∀ (h : b = a),
  Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
    ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
Tactic: by_cases h : b = a
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
inst_1 : DecidableEq α
l : AList.{u_1, u_2} fun (_x : α) ↦ M
a : α
m : M
b : α
pos :
  ∀ (h : b = a),
    Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
      ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
⊢ Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
    ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
have neg : ∀ (h : ¬b = a),
  Eq.{u_2 + 1} (α := M) (((insert (β := fun (_x : α) ↦ M) a m l).lookupFinsupp : (a : α) → M) b : M)
    ((Finsupp.update l.lookupFinsupp a m : (a : α) → M) b : M)
Tactic: by_cases h : b = a
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
⊢ f.toAList.lookupFinsupp = f
have h : ∀ (a : α), Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have pos : ∀ (h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
  Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: by_cases h : f a = 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
pos :
  ∀ (h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have neg : ∀ (h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
  Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: by_cases h : f a = 0
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have pos : lookup (β := fun (_x : α) ↦ M) a f.toAList = none
Tactic: suffices f.toAList.lookup a = none by simp [h, this]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have neg : lookup (β := fun (_x : α) ↦ M) a f.toAList = some ((f : (a : α) → M) a)
Tactic: suffices f.toAList.lookup a = some (f a) by simp [this]
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)
⊢ lookup (β := fun (_x : α) ↦ M) a f.toAList = some ((f : (a : α) → M) a)
have neg : Sigma.mk (β := fun (_x : α) ↦ M) a ((f : (a : α) → M) a) ∈ f.toAList.entries (β := fun (_x : α) ↦ M)
Tactic: apply mem_lookup_iff.2
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have pos : ∀ (h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
  Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: classical
    by_cases h : f a = 0
    · suffices f.toAList.lookup a = none by simp [h, this]
      simp [lookup_eq_none, h]
    · suffices f.toAList.lookup a = some (f a) by simp [this]
      apply mem_lookup_iff.2
      simpa using h
-- Lean 4 proof step from Mathlib.Data.Finsupp.AList (goal)
Goal:
α : Type u_1
M : Type u_2
inst : Zero M
f : α →₀ M
a : α
pos :
  ∀ (h : Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
    Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have neg : ∀ (h : ¬Eq.{u_2 + 1} (α := M) ((f : (a : α) → M) a : M) (0 : M)),
  Eq.{u_2 + 1} (α := M) ((f.toAList.lookupFinsupp : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: classical
    by_cases h : f a = 0
    · suffices f.toAList.lookup a = none by simp [h, this]
      simp [lookup_eq_none, h]
    · suffices f.toAList.lookup a = some (f a) by simp [this]
      apply mem_lookup_iff.2
      simpa using h
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
f : α →₀ ℕ
p : (α →₀ ℕ) × (α →₀ ℕ)
⊢ p ∈ f.antidiagonal'.support ↔ p.1 + p.2 = f
have rcases : ∀ (p₁ p₂ : α →₀ ℕ), (p₁, p₂) ∈ f.antidiagonal'.support ↔ (p₁, p₂).1 + (p₁, p₂).2 = f
Tactic: rcases p with ⟨p₁, p₂⟩
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
⊢ Eq (α := Finset ((α →₀ ℕ) × (α →₀ ℕ))) (@antidiagonal _ instAddMonoid _ (single a n))
    (map (Function.Embedding.prodMap { toFun := single a, inj' := ⋯ } { toFun := single a, inj' := ⋯ })
      (@antidiagonal _ Nat.instAddMonoid _ n))
have h : ∀ (x y : α →₀ ℕ),
  Membership.mem (γ := Finset ((α →₀ ℕ) × (α →₀ ℕ))) (@antidiagonal _ instAddMonoid _ (single a n)) (x, y) ↔
    Membership.mem (γ := Finset ((α →₀ ℕ) × (α →₀ ℕ)))
      (map (Function.Embedding.prodMap { toFun := single a, inj' := sorry } { toFun := single a, inj' := sorry })
        (@antidiagonal _ Nat.instAddMonoid _ n))
      (x, y)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
a : α
n : ℕ
x y : α →₀ ℕ
⊢ Membership.mem (γ := Finset ((α →₀ ℕ) × (α →₀ ℕ))) (@antidiagonal _ instAddMonoid _ (single a n)) (x, y) ↔
    Membership.mem (γ := Finset ((α →₀ ℕ) × (α →₀ ℕ)))
      (map (Function.Embedding.prodMap { toFun := single a, inj' := ⋯ } { toFun := single a, inj' := ⋯ })
        (@antidiagonal _ Nat.instAddMonoid _ n))
      (x, y)
have h : x + y = single a n ↔ ∃ (a_1 : ℕ) (b : ℕ), a_1 + b = n ∧ single a a_1 = x ∧ single a b = y
Tactic: simp only [mem_antidiagonal, mem_map, mem_antidiagonal, Function.Embedding.coe_prodMap,
    Function.Embedding.coeFn_mk, Prod.map_apply, Prod.mk.injEq, Prod.exists]