awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
inst_1 : Zero N
g : (i : ι) → Finsupp.{u_12, u_5} (αs i) M → N
hg : ∀ (i : ι) (x : Finsupp.{u_12, u_5} (αs i) M), x = 0 ↔ g i x = 0
i : ι
rw : l.split (αs := αs) i ≠ 0 ↔ g i (l.split (αs := αs) i) ≠ 0
rw₁ : l.split (αs := αs) i = 0 ↔ g i (l.split (αs := αs) i) = 0
⊢ i ∈ l.splitSupport (αs := αs) ↔ g i (l.split (αs := αs) i) ≠ 0
have rw₂ : g i (l.split (αs := αs) i) = 0 ↔ g i (l.split (αs := αs) i) = 0
Tactic: rw [mem_splitSupport_iff_nonzero, not_iff_not, hg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
⊢ l.support = l.splitSupport (αs := αs).sigma (α := αs) fun (i : ι) ↦ (l.split (αs := αs) i).support
have simp_rw : ∀ (a : ι) (b : αs a),
  Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
    (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
Tactic: simp_rw [Finset.ext_iff, splitSupport, split, comapDomain, Sigma.forall, mem_sigma, mem_image,
    mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
tauto tauto₁ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
⊢ ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
have mp : ∀ (a : ι) (b : αs a),
  Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
    (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
tauto tauto₁ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
⊢ ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
have mpr : ∀ (a : ι) (b : αs a),
  (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support →
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
tauto tauto₁ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mpr :
  ∀ (a : ι) (b : αs a),
    (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₁ mp₂ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
⊢ ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
have mp₃ : ∀ (a : ι) (b : αs a),
  Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
tauto tauto₁ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mpr :
  ∀ (a : ι) (b : αs a),
    (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₁ mp₂ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp₃ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
⊢ ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
have mp₄ : ∀ (a : ι) (b : αs a), Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → Sigma.mk (β := αs) a b ∈ l.support
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
tauto tauto₁ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mpr :
  ∀ (a : ι) (b : αs a),
    (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₁ mp₂ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp₃ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
mp₄ : ∀ (a : ι) (b : αs a), Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → Sigma.mk (β := αs) a b ∈ l.support
⊢ ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
have mpr₁ : ∀ (a : ι) (b : αs a),
  Sigma.mk (β := αs) a b ∈ l.support →
    ∀ w ∈ l.support, w.fst (β := fun (i : ι) ↦ αs i) = a → Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
tauto tauto₁ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mpr :
  ∀ (a : ι) (b : αs a),
    (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₁ mp₂ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp₃ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
mp₄ : ∀ (a : ι) (b : αs a), Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → Sigma.mk (β := αs) a b ∈ l.support
mpr₁ mpr₂ mpr₃ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := αs) a b ∈ l.support →
      ∀ w ∈ l.support, w.fst (β := fun (i : ι) ↦ αs i) = a → Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₅ mp₆ mp₇ mp₈ mp₉ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
⊢ ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
have mp₁₀ : ∀ (a : ι) (b : αs a),
  Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ∧
      (Sigma.mk (β := fun (a : ι) ↦ αs a) a b).fst (β := fun (i : ι) ↦ αs i) = a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
tauto tauto₁ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mpr :
  ∀ (a : ι) (b : αs a),
    (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₁ mp₂ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      (∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
mp₃ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
mp₄ : ∀ (a : ι) (b : αs a), Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → Sigma.mk (β := αs) a b ∈ l.support
mpr₁ mpr₂ mpr₃ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := αs) a b ∈ l.support →
      ∀ w ∈ l.support, w.fst (β := fun (i : ι) ↦ αs i) = a → Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support
mp₅ mp₆ mp₇ mp₈ mp₉ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → ∃ a_2 ∈ l.support, a_2.fst (β := fun (i : ι) ↦ αs i) = a
mp₁₀ :
  ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support →
      Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ∧
        (Sigma.mk (β := fun (a : ι) ↦ αs a) a b).fst (β := fun (i : ι) ↦ αs i) = a
⊢ ∀ (a : ι) (b : αs a),
    Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support ↔
      (∃ a_1 ∈ l.support, a_1.fst (β := fun (i : ι) ↦ αs i) = a) ∧ Sigma.mk (β := αs) a b ∈ l.support
have mp₁₁ : (a : ι) → (b : αs a) → Sigma.mk (β := fun (a : ι) ↦ αs a) a b ∈ l.support → (i : ι) × αs i
Tactic: tauto
-- 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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs : η → Type u_14
inst_2 : Zero α
f : (j : η) × ιs j →₀ α
⊢ (fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
        (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
            (fun (ji : (j : η) × ιs j) ↦
              (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
            ⋯ :
          (j : η) × ιs j →₀ α))
      (f.split (αs := ιs)) =
    f
have h : ∀ (a : (j : η) × ιs j),
  Eq.{u_1 + 1} (α := α)
    (((fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
              (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
                  (fun (ji : (j : η) × ιs j) ↦
                    (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
                  sorry :
                (j : η) × ιs j →₀ α))
            (f.split (αs := ιs)) :
          (a : (j : η) × ιs j) → α)
        a :
      α)
    ((f : (a : (j : η) × ιs j) → α) a : α)
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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs : η → Type u_14
inst_2 : Zero α
f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α
⊢ split (αs := ιs)
      ((fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
          (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
              (fun (ji : (j : η) × ιs j) ↦
                (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
              ⋯ :
            (j : η) × ιs j →₀ α))
        f) =
    f
have h : ∀ (x : η) (a : ιs x),
  Eq.{u_1 + 1} (α := α)
    ((split (αs := ιs)
            ((fun (f : (j : η) → Finsupp.{u_14, u_1} (ιs j) α) ↦
                (onFinset (Finset.sigma (α := ιs) univ fun (j : η) ↦ (f j).support)
                    (fun (ji : (j : η) × ιs j) ↦
                      (f (ji.fst (β := fun (j : η) ↦ ιs j)) : (a : ιs ji.fst) → α) (ji.snd (β := fun (j : η) ↦ ιs j)))
                    sorry :
                  (j : η) × ιs j →₀ α))
              f)
            x :
          (a : ιs x) → α)
        a :
      α)
    ((f x : (a : ιs x) → α) a : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α_1 : 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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
η : Type u_13
inst_1 : Fintype η
ιs_1 : η → Type u_14
inst_2 : Zero α_1
α : Type u_15
ιs : η → Type u_16
inst_3 : AddMonoid α
f g : (j : η) × ιs j →₀ α
⊢ Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) (f + g) =
    Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) f + Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) g
have h : ∀ (x : η) (a : ιs x),
  Eq.{u_15 + 1} (α := α) ((Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) (f + g) x : (a : ιs x) → α) a : α)
    (((Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) f + Equiv.toFun (sigmaFinsuppEquivPiFinsupp (ιs := ιs)) g)
            x :
          (a : ιs x) → α)
        a :
      α)
Tactic: ext
-- 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
⊢ Membership.mem (γ := Set (β →₀ M)) (Set.range (embDomain f)) x ↔
    (↑x.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
have h : Eq (α := (α →₀ M) → β →₀ M) (embDomain f) (mapDomain (⇑f : (a : α) → β))
Tactic: convert! mem_range_mapDomain_iff _ f.injective _
-- 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
h : Eq (α := (α →₀ M) → β →₀ M) (embDomain f) (mapDomain (⇑f : (a : α) → β))
⊢ Membership.mem (γ := Set (β →₀ M)) (Set.range (embDomain f)) x ↔
    (↑x.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)
have h₁ : (↑x.support : Set β) ⊆ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β) ↔
  ∀ b ∉ Set.range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β), Eq.{u_5 + 1} (α := M) ((x : (a : β) → M) b : M) (0 : M)
Tactic: convert! mem_range_mapDomain_iff _ f.injective _
-- 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
⊢ Eq (α := (α →₀ M) → β →₀ M) (embDomain f) (mapDomain (⇑f : (a : α) → β))
have h : ∀ (x : α →₀ M) (a : β),
  Eq.{u_5 + 1} (α := M) ((embDomain f x : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) x : (a : β) → M) a : M)
Tactic: ext
-- 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
x_1 : α →₀ M
a : β
⊢ Eq.{u_5 + 1} (α := M) ((embDomain f x_1 : (a : β) → M) a : M) ((mapDomain (⇑f : (a : α) → β) x_1 : (a : β) → M) a : M)
have h : Eq.{u_5 + 1} (α := M) ((mapDomain (⇑f : (a : α) → β) x_1 : (a : β) → M) a : M)
  ((mapDomain (⇑f : (a : α) → β) x_1 : (a : β) → M) a : M)
Tactic: rw [embDomain_eq_mapDomain]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
⊢ (mapDomain f x).support = image f x.support
have h : ∀ (t : β), t ∈ (mapDomain f x).support ↔ t ∈ image f x.support
Tactic: ext t
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
⊢ t ∈ (mapDomain f x).support ↔ t ∈ image f x.support
have h : ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) ↔ ∃ a ∈ x.support, f a = t
Tactic: rw [mem_support_iff, ne_eq, Finset.mem_image]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) ↔ ∃ a ∈ x.support, f a = t
have h : ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) → ∃ a ∈ x.support, f a = t
Tactic: refine ⟨?_, fun ⟨i, i_in, hi⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : DecidableEq β
inst_1 : AddCommMonoid M
f : α → β
inst_2 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
t : β
h : ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) → ∃ a ∈ x.support, f a = t
⊢ ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M) ↔ ∃ a ∈ x.support, f a = t
have h₁ : (∃ a ∈ x.support, f a = t) →
  ∀ (i : α) (i_in : i ∈ x.support) (hi : f i = t), ¬Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) t : M) (0 : M)
Tactic: refine ⟨?_, fun ⟨i, i_in, hi⟩ ↦ ?_⟩
-- 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 : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
h : x = 0
⊢ mapDomain f x = 0
have rw : Eq (α := β →₀ M) (mapDomain f 0) 0
Tactic: rw [h, mapDomain_zero]
-- 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 : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
h : x = 0
rw : Eq (α := β →₀ M) (mapDomain f 0) 0
⊢ mapDomain f x = 0
have rw₁ : Eq (α := β →₀ M) 0 0
Tactic: rw [h, mapDomain_zero]
-- 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 : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
⊢ mapDomain f x = 0 ↔ x = 0
have refine : ∀ (h : mapDomain f x = 0) (i : α), Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
Tactic: refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
-- 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 : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
h : mapDomain f x = 0
i : α
⊢ Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
have h₁ : Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f i) : M) ((0 : (a : β) → M) (f i) : M)
Tactic: replace h := Finsupp.ext_iff.mp h (f i)
Cleared hypotheses: h
-- 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 : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
i : α
h : Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f i) : M) ((0 : (a : β) → M) (f i) : M)
⊢ Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
have h₁ : ∀ (i_1 : α),
  ¬Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M) →
    f i_1 = f i → Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M)
Tactic: simp [mapDomain_apply_eq_sum] at h
Cleared hypotheses: 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 : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
⊢ mapDomain f x = 0 ↔ x = 0
have refine : ∀ (h : mapDomain f x = 0) (i : α), Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
Tactic: classical
  refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
  replace h := Finsupp.ext_iff.mp h (f i)
  simp [mapDomain_apply_eq_sum] at h; grind
-- 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 : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
refine : ∀ (h : mapDomain f x = 0) (i : α), Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
⊢ mapDomain f x = 0 ↔ x = 0
have refine₁ : ∀ (i : α) (h : Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f i) : M) ((0 : (a : β) → M) (f i) : M)),
  Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
Tactic: classical
  refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
  replace h := Finsupp.ext_iff.mp h (f i)
  simp [mapDomain_apply_eq_sum] at h; grind
-- 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 : α → β
inst_1 : Subsingleton.{u_5 + 1} (AddUnits M)
x : α →₀ M
refine : ∀ (h : mapDomain f x = 0) (i : α), Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
refine₁ :
  ∀ (i : α) (h : Eq.{u_5 + 1} (α := M) ((mapDomain f x : (a : β) → M) (f i) : M) ((0 : (a : β) → M) (f i) : M)),
    Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
⊢ mapDomain f x = 0 ↔ x = 0
have refine₂ : ∀ (i : α)
  (h :
    ∀ (i_1 : α),
      ¬Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M) →
        f i_1 = f i → Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i_1 : M) (0 : M)),
  Eq.{u_5 + 1} (α := M) ((x : (a : α) → M) i : M) ((0 : (a : α) → M) i : M)
Tactic: classical
  refine ⟨fun h ↦ Finsupp.ext (fun i ↦ ?_), fun h ↦ by rw [h, mapDomain_zero]⟩
  replace h := Finsupp.ext_iff.mp h (f i)
  simp [mapDomain_apply_eq_sum] at h; grind
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ tl
⊢ (hd :: tl).sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)
have cons : (hd + tl.sum).support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ (hd :: tl)
Tactic: simp only [List.sum_cons]
-- Lean 4 proof step from Mathlib.Data.Finsupp.BigOperators (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : DecidableEq ι
inst_1 : AddZeroClass M
l : List (ι →₀ M)
⊢ l.sum.support ⊆ foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ l
have nil : Subset.{u_1} (α := Finset ι) (Finsupp.support.{u_1, u_2} (M := M) (sum []))
  (foldr (fun (x1 : ι →₀ M) (x2 : Finset ι) ↦ x1.support ⊔ x2) ∅ [])
Tactic: induction l with
  | nil => simp
  | cons hd tl IH =>
    simp only [List.sum_cons]
    exact Finsupp.support_add.trans (Finset.union_subset_union Finset.Subset.rfl IH)
Cleared hypotheses: l