awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
h₁ : comapDomain Sum.inr (u + v) ⋯ = y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y
have h₂ : comapDomain Sum.inr (x.sumElim y) sorry = y
Tactic: rw [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_inr_sumElim]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Antidiagonal (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type u_1
inst_1 : DecidableEq β
x : α →₀ ℕ
y : β →₀ ℕ
u v : α ⊕ β →₀ ℕ
h : u + v = x.sumElim y
h₁ : comapDomain Sum.inr (u + v) ⋯ = y
h₂ : comapDomain Sum.inr (x.sumElim y) ⋯ = y
⊢ comapDomain Sum.inr u ⋯ + comapDomain Sum.inr v ⋯ = y
have h₃ : y = y
Tactic: rw [← comapDomain_add_of_injective Sum.inr_injective, h, comapDomain_inr_sumElim]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
m : M
f : α →₀ M
⊢ (a, m) ∈ f.graph ↔ (f : (a : α) → M) a = m ∧ m ≠ 0
have simp_rw : (∃ (a_1 : α),
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
      ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } : (a : α) → α × M) a_1 = (a, m)) ↔
  (f : (a : α) → M) a = m ∧ m ≠ 0
Tactic: simp_rw [graph, mem_map, mem_support_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
m : M
f : α →₀ M
⊢ (∃ (a_1 : α),
      Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
        ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_1 = (a, m)) ↔
    (f : (a : α) → M) a = m ∧ m ≠ 0
have mp : (∃ (a_1 : α),
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
      ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } : (a : α) → α × M) a_1 = (a, m)) →
  (f : (a : α) → M) a = m ∧ m ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
a : α
m : M
f : α →₀ M
mp :
  (∃ (a_1 : α),
      Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
        ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_1 = (a, m)) →
    (f : (a : α) → M) a = m ∧ m ≠ 0
⊢ (∃ (a_1 : α),
      Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_1 : M) (0 : M) ∧
        ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M) a_1 = (a, m)) ↔
    (f : (a : α) → M) a = m ∧ m ≠ 0
have mpr : (f : (a : α) → M) a = m ∧ m ≠ 0 →
  ∃ (a_2 : α),
    Ne.{u_5 + 1} (α := M) ((f : (a : α) → M) a_2 : M) (0 : M) ∧
      ({ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } : (a : α) → α × M) a_2 = (a, m)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
c : α × M
f : α →₀ M
⊢ c ∈ f.graph ↔ (f : (a : α) → M) c.1 = c.2 ∧ c.2 ≠ 0
have mk : ∀ (fst : α) (snd : M), (fst, snd) ∈ f.graph ↔ (f : (a : α) → M) (fst, snd).1 = (fst, snd).2 ∧ (fst, snd).2 ≠ 0
Tactic: cases c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support
have simp_rw : image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } f.support) = f.support
Tactic: simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
⊢ image Prod.fst f.graph = f.support
have simp_rw₁ : image (α := α × M) Prod.fst
    (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } : (a : α) → α × M) f.support) =
  f.support
Tactic: simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
simp_rw₁ :
  image (α := α × M) Prod.fst
      (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M)
        f.support) =
    f.support
⊢ image Prod.fst f.graph = f.support
have simp_rw₂ : image
    (comp (β := α × M) Prod.fst
      (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } : (a : α) → α × M))
    f.support =
  f.support
Tactic: simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
simp_rw₁ :
  image (α := α × M) Prod.fst
      (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M)
        f.support) =
    f.support
simp_rw₂ :
  image
      (comp (β := α × M) Prod.fst
        (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M))
      f.support =
    f.support
⊢ image Prod.fst f.graph = f.support
have simp_rw₃ : image (comp (β := α × M) Prod.fst fun (a : α) ↦ (a, (f : (a : α) → M) a)) f.support = f.support
Tactic: simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
simp_rw₁ :
  image (α := α × M) Prod.fst
      (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M)
        f.support) =
    f.support
simp_rw₂ :
  image
      (comp (β := α × M) Prod.fst
        (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M))
      f.support =
    f.support
simp_rw₃ : image (comp (β := α × M) Prod.fst fun (a : α) ↦ (a, (f : (a : α) → M) a)) f.support = f.support
⊢ image Prod.fst f.graph = f.support
have simp_rw₄ : image (fun (x : α) ↦ x) f.support = f.support
Tactic: simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support
have simp_rw : image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } f.support) = f.support
Tactic: classical
  simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
⊢ image Prod.fst f.graph = f.support
have simp_rw₁ : image (α := α × M) Prod.fst
    (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } : (a : α) → α × M) f.support) =
  f.support
Tactic: classical
  simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
simp_rw₁ :
  image (α := α × M) Prod.fst
      (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M)
        f.support) =
    f.support
⊢ image Prod.fst f.graph = f.support
have simp_rw₂ : image
    (comp (β := α × M) Prod.fst
      (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := sorry : α ↪ α × M } : (a : α) → α × M))
    f.support =
  f.support
Tactic: classical
  simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
simp_rw₁ :
  image (α := α × M) Prod.fst
      (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M)
        f.support) =
    f.support
simp_rw₂ :
  image
      (comp (β := α × M) Prod.fst
        (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M))
      f.support =
    f.support
⊢ image Prod.fst f.graph = f.support
have simp_rw₃ : image (comp (β := α × M) Prod.fst fun (a : α) ↦ (a, (f : (a : α) → M) a)) f.support = f.support
Tactic: classical
  simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
inst_1 : DecidableEq α
f : α →₀ M
simp_rw :
  image Prod.fst (map { toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } f.support) = f.support
simp_rw₁ :
  image (α := α × M) Prod.fst
      (image (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M)
        f.support) =
    f.support
simp_rw₂ :
  image
      (comp (β := α × M) Prod.fst
        (⇑{ toFun := fun (a : α) ↦ (a, (f : (a : α) → M) a), inj' := ⋯ : α ↪ α × M } : (a : α) → α × M))
      f.support =
    f.support
simp_rw₃ : image (comp (β := α × M) Prod.fst fun (a : α) ↦ (a, (f : (a : α) → M) a)) f.support = f.support
⊢ image Prod.fst f.graph = f.support
have simp_rw₄ : image (fun (x : α) ↦ x) f.support = f.support
Tactic: classical
  simp_rw [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f.support = g.support
have rw : image Prod.fst f.graph = g.support
Tactic: rw [← image_fst_graph, h, image_fst_graph]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
rw : image Prod.fst f.graph = g.support
⊢ f.support = g.support
have rw₁ : image Prod.fst g.graph = g.support
Tactic: rw [← image_fst_graph, h, image_fst_graph]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
rw : image Prod.fst f.graph = g.support
rw₁ : image Prod.fst g.graph = g.support
⊢ f.support = g.support
have rw₂ : g.support = g.support
Tactic: rw [← image_fst_graph, h, image_fst_graph]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (hypothesis)
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f = g
have hsup : f.support = g.support
Tactic: have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
hsup : f.support = g.support
⊢ f = g
have refine : ∀ (x : α) (hx : x ∈ f.support), Membership.mem (α := α × M) g.graph ((x, (g : (a : α) → M) x) : α × M)
Tactic: refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
⊢ f = g
have have : f.support = g.support
Tactic: classical
    have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
    refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
    exact mk_mem_graph _ (hsup ▸ hx)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
have : f.support = g.support
⊢ f = g
have have₁ : ∀ (hsup : f.support = g.support), f = g
Tactic: classical
    have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
    refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
    exact mk_mem_graph _ (hsup ▸ hx)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_12
M : Type u_13
inst : Zero M
f g : α →₀ M
h : f.graph = g.graph
have : f.support = g.support
have₁ : ∀ (hsup : f.support = g.support), f = g
have₂ : f.support = g.support
have₃ have₄ : ∀ (hsup : f.support = g.support), f = g
⊢ f = g
have have₅ : ∀ (hsup : f.support = g.support) (x : α) (hx : x ∈ f.support),
  Membership.mem (α := α × M) g.graph ((x, (g : (a : α) → M) x) : α × M)
Tactic: classical
    have hsup : f.support = g.support := by rw [← image_fst_graph, h, image_fst_graph]
    refine ext_iff'.2 ⟨hsup, fun x hx => apply_eq_of_mem_graph <| h.symm ▸ ?_⟩
    exact mk_mem_graph _ (hsup ▸ hx)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α ≃ β
l : α →₀ M
a : β
⊢ a ∈ map f.toEmbedding l.support ↔ Ne.{u_5 + 1} (α := M) ((l : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M) (0 : M)
have simp : l.toFun ((f.symm : (a : β) → α) a) ≠ 0 ↔
  Ne.{u_5 + 1} (α := M) ((l : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M) (0 : M)
Tactic: simp only [Finset.mem_map_equiv, mem_support_toFun]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
l : α →₀ M
⊢ equivMapDomain (Equiv.refl α) l = l
have h : ∀ (x : α), Eq.{u_5 + 1} (α := M) ((equivMapDomain (Equiv.refl α) l : (a : α) → M) x : M) ((l : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_5
inst : Zero M
⊢ Eq (α := (l : α →₀ M) → α →₀ M) (equivMapDomain (Equiv.refl α)) id
have h : ∀ (x : α →₀ M) (a : α),
  Eq.{u_5 + 1} (α := M) ((equivMapDomain (Equiv.refl α) x : (a : α) → M) a : M) ((id x : (a : α) → M) a : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : Zero M
f : α ≃ β
g : β ≃ γ
l : α →₀ M
⊢ equivMapDomain (f.trans g) l = equivMapDomain g (equivMapDomain f l)
have h : ∀ (x : γ),
  Eq.{u_5 + 1} (α := M) ((equivMapDomain (f.trans g) l : (a : γ) → M) x : M)
    ((equivMapDomain g (equivMapDomain f l) : (a : γ) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : Zero M
f : α ≃ β
g : β ≃ γ
⊢ Eq (α := (l : α →₀ M) → γ →₀ M) (equivMapDomain (f.trans g)) (equivMapDomain g ∘ equivMapDomain f)
have h : ∀ (x : α →₀ M) (a : γ),
  Eq.{u_5 + 1} (α := M) ((equivMapDomain (f.trans g) x : (a : γ) → M) a : M)
    (((equivMapDomain g ∘ equivMapDomain f) x : (a : γ) → M) a : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
a : α
b : M
⊢ Eq (α := β →₀ M) (equivMapDomain f (single a b)) (single ((f : (a : α) → β) a) b)
have h : ∀ (x : β),
  Eq.{u_5 + 1} (α := M) ((equivMapDomain f (single a b) : (a : β) → M) x : M)
    (((single ((f : (a : α) → β) a) b : β →₀ M) : (a : β) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
a : α
b : M
⊢ Eq (α := β →₀ M) (equivMapDomain f (single a b)) (single ((f : (a : α) → β) a) b)
have h : ∀ (x : β),
  Eq.{u_5 + 1} (α := M) ((equivMapDomain f (single a b) : (a : β) → M) x : M)
    (((single ((f : (a : α) → β) a) b : β →₀ M) : (a : β) → M) x : M)
Tactic: classical
    ext x
    simp only [single_apply, Equiv.apply_eq_iff_eq_symm_apply, equivMapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : Zero M
f : α ≃ β
⊢ Eq (α := β →₀ M) (equivMapDomain f 0) 0
have h : ∀ (a : β), Eq.{u_5 + 1} (α := M) ((equivMapDomain f 0 : (a : β) → M) a : M) ((0 : (a : β) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α ≃ β
⊢ (α →₀ M) ≃ (β →₀ M)
have refine_1 : ∀ (f_1 : α →₀ M), equivMapDomain f.symm (equivMapDomain f f_1) = f_1
Tactic: refine ⟨equivMapDomain f, equivMapDomain f.symm, fun f => ?_, fun f => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f : α ≃ β
refine_1 : ∀ (f_1 : α →₀ M), equivMapDomain f.symm (equivMapDomain f f_1) = f_1
⊢ (α →₀ M) ≃ (β →₀ M)
have refine_2 : ∀ (f_1 : β →₀ M), equivMapDomain f (equivMapDomain f.symm f_1) = f_1
Tactic: refine ⟨equivMapDomain f, equivMapDomain f.symm, fun f => ?_, fun f => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f_1 : α ≃ β
f : α →₀ M
⊢ equivMapDomain f_1.symm (equivMapDomain f_1 f) = f
have refine_1 : ∀ (x : α),
  Eq.{u_5 + 1} (α := M) ((equivMapDomain f_1.symm (equivMapDomain f_1 f) : (a : α) → M) x : M) ((f : (a : α) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero M
f_1 : α ≃ β
f : β →₀ M
⊢ equivMapDomain f_1 (equivMapDomain f_1.symm f) = f
have refine_2 : ∀ (x : β),
  Eq.{u_5 + 1} (α := M) ((equivMapDomain f_1 (equivMapDomain f_1.symm f) : (a : β) → M) x : M) ((f : (a : β) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have h₀ : ∀ (b : α),
  Ne.{u_5 + 1} (α := M) ((x : (a : α) → M) b : M) (0 : M) →
    b ≠ a → Eq.{u_5 + 1} (α := M) (((single (f b) ((x : (a : α) → M) b) : β →₀ M) : (a : β) → M) (f a) : M) (0 : M)
Tactic: rw [mapDomain, sum_apply, sum_eq_single a, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
h₀ :
  ∀ (b : α),
    Ne.{u_5 + 1} (α := M) ((x : (a : α) → M) b : M) (0 : M) →
      b ≠ a → Eq.{u_5 + 1} (α := M) (((single (f b) ((x : (a : α) → M) b) : β →₀ M) : (a : β) → M) (f a) : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have h₁ : Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) a : M) (0 : M) →
  Eq.{u_5 + 1} (α := M) ((single (f a) 0 : (a : β) → M) (f a) : M) (0 : M)
Tactic: rw [mapDomain, sum_apply, sum_eq_single a, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
h : Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) a : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((single (f a) 0 : (a : β) → M) (f a) : M) (0 : M)
have h₁ : Eq.{u_5 + 1} (α := M) ((0 : (a : β) → M) (f a) : M) (0 : M)
Tactic: rw [single_zero, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
h : Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) a : M) (0 : M)
h₁ : Eq.{u_5 + 1} (α := M) ((0 : (a : β) → M) (f a) : M) (0 : M)
⊢ Eq.{u_5 + 1} (α := M) ((single (f a) 0 : (a : β) → M) (f a) : M) (0 : M)
have h₂ : Eq.{u_5 + 1} (α := M) (0 (f a)) 0
Tactic: rw [single_zero, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
x : α →₀ M
a : α
h : Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) a : M) (0 : M)
h₁ : Eq.{u_5 + 1} (α := M) ((0 : (a : β) → M) (f a) : M) (0 : M)
h₂ : Eq.{u_5 + 1} (α := M) (0 (f a)) 0
⊢ Eq.{u_5 + 1} (α := M) ((single (f a) 0 : (a : β) → M) (f a) : M) (0 : M)
have h₃ : Eq.{u_5 + 1} (α := M) 0 0
Tactic: rw [single_zero, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
x : α →₀ M
b : β
hb : b ∉ f '' (↑x.support : Set α)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) b : M) (0 : M)
have rw : ∀ x_1 ∈ x.support,
  Eq.{u_5 + 1} (α := M) (((single (f x_1) ((x : (a : α) → M) x_1) : β →₀ M) : (a : β) → M) b : M) (0 : M)
Tactic: rw [mapDomain, sum_apply, sum, Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)
have refine_1 : ∀ (a : β), Eq (α := γ →₀ M) (single (g a) 0) 0
Tactic: refine ((sum_sum_index ?_ ?_).trans ?_).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
refine_1 : ∀ (a : β), Eq (α := γ →₀ M) (single (g a) 0) 0
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)
have refine_2 : ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = HAdd.hAdd (α := γ →₀ M) (single (g a) b₁) (single (g a) b₂)
Tactic: refine ((sum_sum_index ?_ ?_).trans ?_).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
refine_1 : ∀ (a : β), Eq (α := γ →₀ M) (single (g a) 0) 0
refine_2 : ∀ (a : β) (b₁ b₂ : M), single (g a) (b₁ + b₂) = HAdd.hAdd (α := γ →₀ M) (single (g a) b₁) (single (g a) b₂)
⊢ mapDomain (g ∘ f) v = mapDomain g (mapDomain f v)
have refine_3 : (v.sum fun (a : α) (b : M) ↦ sum (single (f a) b) fun (a : β) ↦ single (g a)) = mapDomain (g ∘ f) v
Tactic: refine ((sum_sum_index ?_ ?_).trans ?_).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
M : Type u_5
inst : AddCommMonoid M
v : α →₀ M
f : α → β
g : β → γ
⊢ (v.sum fun (a : α) (b : M) ↦ sum (single (f a) b) fun (a : β) ↦ single (g a)) = mapDomain (g ∘ f) v
have refine_3 : ∀ x ∈ v.support, Eq (α := γ →₀ M) (single (g (f x)) 0) 0
Tactic: refine sum_congr fun _ _ => sum_single_index ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α ≃ β
x : α →₀ M
a : β
| ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) a : M)
have rw : ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β) : M)
Tactic: rw [← f.apply_symm_apply a]