awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : β
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) a : M)
    ((x : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M)
have conv_lhs : Eq.{u_5 + 1} (α := M)
  ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) ((f : (a : α) → β) ((f.symm : (a : β) → α) a : α) : β) : M)
  ((x : (a : α) → M) ((f.symm : (a : β) → α) a : α) : M)
Tactic: conv_lhs => rw [← f.apply_symm_apply a]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
⊢ (s.support.biUnion fun (x : α) ↦ {f x}) ⊆ image f s.support
have rw : image f s.support ⊆ image f s.support
Tactic: rw [Finset.biUnion_singleton]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have rw : Eq.{u_5 + 1} (α := M) (∑ a_1 ∈ x.support, ((single (f a_1) ((x : (a : α) → M) a_1) : β →₀ M) : (a : β) → M) (f a) : M)
  ((x : (a : α) → M) a : M)
Tactic: rw [mapDomain, sum_apply, sum]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ Eq.{u_5 + 1} (α := M) (∑ a_1 ∈ x.support, ((single (f a_1) ((x : (a : α) → M) a_1) : β →₀ M) : (a : β) → M) (f a) : M)
    ((x : (a : α) → M) a : M)
have simp_rw : Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
  ((x : (a : α) → M) a : M)
Tactic: simp_rw [single_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
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
have pos : ∀ (hax : a ∈ x.support),
  Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
Tactic: by_cases hax : a ∈ x.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
pos :
  ∀ (hax : a ∈ x.support),
    Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
      ((x : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
have neg : ∀ (hax : a ∉ x.support),
  Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
Tactic: by_cases hax : a ∈ x.support
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
have pos : HAdd.hAdd (α := M) (β := M) ((x : (a : α) → M) a : M)
    (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M) =
  (x : (a : α) → M) a
Tactic: rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ HAdd.hAdd (α := M) (β := M) ((x : (a : α) → M) a : M)
      (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M) =
    (x : (a : α) → M) a
have h : Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0
Tactic: convert! add_zero (x a)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∈ x.support
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support.erase a, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0
have h : ∀ (i : α) (hi : i ∈ x.support.erase a), ¬f i = f a
Tactic: refine Finset.sum_eq_zero fun i hi => if_neg ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
have neg : Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0
Tactic: rw [notMem_support_iff.1 hax]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
hax : a ∉ x.support
⊢ Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0) 0
have neg : ∀ (i : α) (hi : i ∈ x.support), ¬f i = f a
Tactic: refine Finset.sum_eq_zero fun i hi => if_neg ?_
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have rw : Eq.{u_5 + 1} (α := M) ((x.sum fun (a : α) ↦ single (f a) : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
Tactic: classical
    rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
rw : Eq.{u_5 + 1} (α := M) ((x.sum fun (a : α) ↦ single (f a) : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have rw₁ : Eq (α := M) (x.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
Tactic: classical
    rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
rw : Eq.{u_5 + 1} (α := M) ((x.sum fun (a : α) ↦ single (f a) : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₁ : Eq (α := M) (x.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have rw₂ : Eq.{u_5 + 1} (α := M) (∑ a_1 ∈ x.support, ((single (f a_1) ((x : (a : α) → M) a_1) : β →₀ M) : (a : β) → M) (f a) : M)
  ((x : (a : α) → M) a : M)
Tactic: classical
    rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
rw : Eq.{u_5 + 1} (α := M) ((x.sum fun (a : α) ↦ single (f a) : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₁ : Eq (α := M) (x.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₂ rw₃ rw₄ :
  Eq.{u_5 + 1} (α := M) (∑ a_1 ∈ x.support, ((single (f a_1) ((x : (a : α) → M) a_1) : β →₀ M) : (a : β) → M) (f a) : M)
    ((x : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have rw₅ : Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
  ((x : (a : α) → M) a : M)
Tactic: classical
    rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
rw : Eq.{u_5 + 1} (α := M) ((x.sum fun (a : α) ↦ single (f a) : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₁ : Eq (α := M) (x.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₂ rw₃ rw₄ :
  Eq.{u_5 + 1} (α := M) (∑ a_1 ∈ x.support, ((single (f a_1) ((x : (a : α) → M) a_1) : β →₀ M) : (a : β) → M) (f a) : M)
    ((x : (a : α) → M) a : M)
rw₅ :
  Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have pos : ∀ (hax : a ∈ x.support),
  Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
Tactic: classical
    rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
S : Set α
f : α → β
x : α →₀ M
hS : (↑x.support : Set α) ⊆ S
hf : Set.InjOn f S
a : α
ha : a ∈ S
rw : Eq.{u_5 + 1} (α := M) ((x.sum fun (a : α) ↦ single (f a) : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₁ : Eq (α := M) (x.sum fun (a₁ : α) (b : M) ↦ (single (f a₁) b : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
rw₂ rw₃ rw₄ :
  Eq.{u_5 + 1} (α := M) (∑ a_1 ∈ x.support, ((single (f a_1) ((x : (a : α) → M) a_1) : β →₀ M) : (a : β) → M) (f a) : M)
    ((x : (a : α) → M) a : M)
rw₅ :
  Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
pos :
  ∀ (hax : a ∈ x.support),
    Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
      ((x : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f a) : M) ((x : (a : α) → M) a : M)
have neg : ∀ (hax : a ∉ x.support),
  Eq.{u_5 + 1} (α := M) (∑ x_1 ∈ x.support, if f x_1 = f a then (x : (a : α) → M) x_1 else 0 : M)
    ((x : (a : α) → M) a : M)
Tactic: classical
    rw [mapDomain, sum_apply, sum]
    simp_rw [single_apply]
    by_cases hax : a ∈ x.support
    · rw [← Finset.add_sum_erase _ _ hax, if_pos rfl]
      convert! add_zero (x a)
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact (hf.mono hS).ne (Finset.mem_of_mem_erase hi) hax (Finset.ne_of_mem_erase hi)
    · rw [notMem_support_iff.1 hax]
      refine Finset.sum_eq_zero fun i hi => if_neg ?_
      exact hf.ne (hS hi) ha (ne_of_mem_of_not_mem hi hax)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
x : β
hx : x ∈ image f s.support
⊢ x ∈ (mapDomain f s).support
have hx₁ : ∃ (a : α), ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) a : M) (0 : M) ∧ f a = x
Tactic: simp only [mem_image, mem_support_iff, Ne] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
x : β
hx : ∃ (a : α), ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) a : M) (0 : M) ∧ f a = x
⊢ x ∈ (mapDomain f s).support
have rcases : ∀ (hx_w : α) (hx_h_left : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)), f hx_w ∈ (mapDomain f s).support
Tactic: rcases hx with ⟨hx_w, hx_h_left, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
⊢ f hx_w ∈ (mapDomain f s).support
have simp : ¬Eq.{u_5 + 1} (α := M) ((mapDomain f s : (a : β) → M) (f hx_w) : M) (0 : M)
Tactic: simp only [mem_support_iff, Ne]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left rw : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f s : (a : β) → M) (f hx_w) : M) (0 : M)
have rw₁ : hx_w ∈ (↑s.support : Set α)
Tactic: rw [mapDomain_apply' (↑s.support : Set _) _ _ hf]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
inst_1 : DecidableEq β
f : α → β
s : α →₀ M
hf : Set.InjOn f (↑s.support : Set α)
hx_w : α
hx_h_left rw : ¬Eq.{u_5 + 1} (α := M) ((s : (a : α) → M) hx_w : M) (0 : M)
rw₁ : hx_w ∈ (↑s.support : Set α)
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f s : (a : β) → M) (f hx_w) : M) (0 : M)
have rw₂ : (↑s.support : Set α) ⊆ (↑s.support : Set α)
Tactic: rw [mapDomain_apply' (↑s.support : Set _) _ _ hf]
-- 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 : α ↪ β
v : α →₀ M
⊢ embDomain f v = mapDomain (⇑f : (a : α) → β) v
have h : ∀ (a : β),
  Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
Tactic: ext a
-- 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 : α ↪ β
v : α →₀ M
a : β
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
have pos : ∀ (h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a),
  Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
Tactic: by_cases h : a ∈ Set.range f
-- 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 : α ↪ β
v : α →₀ M
a : β
pos :
  ∀ (h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a),
    Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
have neg : ∀ (h : a ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)),
  Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
Tactic: by_cases h : a ∈ Set.range f
-- 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 : α ↪ β
v : α →₀ M
a : β
h : Membership.mem (γ := Set β) (Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) a
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) a : M)
have pos : ∀ (a : α),
  Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
Tactic: rcases h with ⟨a, rfl⟩
Cleared hypotheses: a, h
-- 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 : α ↪ β
v : α →₀ M
a : α
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
have pos : Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
Tactic: rw [mapDomain_apply f.injective, embDomain_apply_self]
-- 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 : α ↪ β
v : α →₀ M
a : α
pos : Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M) ((v : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
    ((mapDomain (⇑f : (a : α) → β) v : (a : β) → M) ((f : (a : α) → β) a : β) : M)
have pos₁ : Eq.{u_5 + 1} (α := M) ((v : (a : α) → M) a : M) ((v : (a : α) → M) a : M)
Tactic: rw [mapDomain_apply f.injective, embDomain_apply_self]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
⊢ (mapDomain f s).prod h = s.prod fun (a : α) (b : M) ↦ h (f a) b
have rw : prod (mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) s) h =
  s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b
Tactic: rw [← Function.Embedding.coeFn_mk f hf, ← embDomain_eq_mapDomain, prod_embDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
rw :
  prod (mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) s) h =
    s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b
⊢ (mapDomain f s).prod h = s.prod fun (a : α) (b : M) ↦ h (f a) b
have rw₁ : (embDomain { toFun := f, inj' := hf : α ↪ β } s).prod h =
  s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b
Tactic: rw [← Function.Embedding.coeFn_mk f hf, ← embDomain_eq_mapDomain, prod_embDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
N : Type u_6
inst : AddCommMonoid M
inst_1 : CommMonoid N
f : α → β
s : α →₀ M
h : β → M → N
hf : Injective f
rw :
  prod (mapDomain (⇑{ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) s) h =
    s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b
rw₁ :
  (embDomain { toFun := f, inj' := hf : α ↪ β } s).prod h =
    s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b
⊢ (mapDomain f s).prod h = s.prod fun (a : α) (b : M) ↦ h (f a) b
have rw₂ : Eq.{u_6 + 1} (α := N) (s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b)
  (s.prod fun (a : α) (b : M) ↦ h (({ toFun := f, inj' := hf : α ↪ β } : (a : α) → β) a) b)
Tactic: rw [← Function.Embedding.coeFn_mk f hf, ← embDomain_eq_mapDomain, prod_embDomain]
-- 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
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
have h : ∀ (a : α), Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
Tactic: ext a
-- 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
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ Eq.{u_5 + 1} (α := M) ((mapDomain f v₁ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)
have rw : Eq.{u_5 + 1} (α := M) ((mapDomain f v₂ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
have this : Eq.{u_5 + 1} (α := M) ((mapDomain f v₁ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)
Tactic: have : mapDomain f v₁ (f a) = mapDomain f v₂ (f a) := by rw [eq]
-- 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
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : Eq.{u_5 + 1} (α := M) ((mapDomain f v₁ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
have h : ∀ (this : Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)),
  Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
Tactic: rwa [mapDomain_apply hf, mapDomain_apply hf] at this
Cleared hypotheses: this
-- 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
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : Eq.{u_5 + 1} (α := M) ((mapDomain f v₁ : (a : β) → M) (f a) : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)
h :
  ∀ (this : Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((mapDomain f v₂ : (a : β) → M) (f a) : M)),
    Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
⊢ Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
have h₁ : ∀ (this : Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)),
  Eq.{u_5 + 1} (α := M) ((v₁ : (a : α) → M) a : M) ((v₂ : (a : α) → M) a : M)
Tactic: rwa [mapDomain_apply hf, mapDomain_apply hf] at this
Cleared hypotheses: this
-- 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 : Surjective f
x : β →₀ M
⊢ ∃ (a : α →₀ M), mapDomain f a = x
have h : mapDomain f (mapDomain (surjInv hf) x) = x
Tactic: use mapDomain (surjInv hf) x