awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
rw rw₁ rw₂ :
  (∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x) ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
⊢ x ∈ iSup p ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
have rw₃ : (∃ (f : ι →₀ N),
    (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x) →
  ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
Tactic: classical
  rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
rw rw₁ rw₂ :
  (∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x) ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
rw₃ :
  (∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x) →
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
⊢ x ∈ iSup p ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
have rw₄ : ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)),
  ∃ (f_1 : Π₀ (i : ι), ↥(p i)),
    Eq (α := N) (f_1.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N))
      (f.sum fun (_i : ι) (xi : N) ↦ xi)
Tactic: classical
  rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
rw rw₁ rw₂ :
  (∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x) ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
rw₃ :
  (∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x) →
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
rw₄ :
  ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)),
    ∃ (f_1 : Π₀ (i : ι), ↥(p i)),
      Eq (α := N) (f_1.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N))
        (f.sum fun (_i : ι) (xi : N) ↦ xi)
⊢ x ∈ iSup p ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
have refine_1 : ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)),
  support (β := fun (i : ι) ↦ ↥(p i))
      (DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
        Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) sorry) =
    f.support
Tactic: classical
  rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
p : ι → Submodule R N
x : N
rw rw₁ rw₂ :
  (∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x) ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
rw₃ :
  (∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x) →
    ∃ (f : Π₀ (i : ι), ↥(p i)), (f.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) = x
rw₄ :
  ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)),
    ∃ (f_1 : Π₀ (i : ι), ↥(p i)),
      Eq (α := N) (f_1.sum (β := fun (i : ι) ↦ ↥(p i)) fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N))
        (f.sum fun (_i : ι) (xi : N) ↦ xi)
refine_1 :
  ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)),
    support (β := fun (i : ι) ↦ ↥(p i))
        (DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
          Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) ⋯) =
      f.support
⊢ x ∈ iSup p ↔
    ∃ (f : ι →₀ N),
      (∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) ∧ (f.sum fun (_i : ι) (xi : N) ↦ xi) = x
have refine_2 : ∀ (f : ι →₀ N) (hf : ∀ (i : ι), Membership.mem (α := N) (p i) ((f : (a : ι) → N) i : N)) (i : ι) (hi : i ∈ f.support),
  Eq.{u_6 + 1} (α := N)
    ((fun (x : ι) (xi : ↥(p x)) ↦ (↑xi : N)) i
      ((DFinsupp.mk (β := fun (i : ι) ↦ ↥(p i)) f.support fun (i : (↑(↑f.support : Set ι) : Type u_1)) ↦
            Subtype.mk (p := fun (x : N) ↦ x ∈ p (↑i : ι)) ((f : (a : ι) → N) (↑i : ι)) sorry :
          (a : ι) → ↥(p a))
        i))
    ((fun (_i : ι) (xi : N) ↦ xi) i ((f : (a : ι) → N) i))
Tactic: classical
  rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ Membership.mem (γ := Submodule R N) (⨆ i ∈ s, p i) a ↔ ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
have rw : (∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
    (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a) ↔
  ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
Tactic: rw [Submodule.mem_iSup_iff_exists_dfinsupp']
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
⊢ (∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
      (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a) ↔
    ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
have mp : (∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
    (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a) →
  ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
mp :
  (∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
      (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a) →
    ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
⊢ (∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
      (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a) ↔
    ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
have mpr : (∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a) →
  ∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
    (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
⊢ ∃ (μ : (i : ι) → ↥(p i)), ∑ i ∈ s, (↑(μ i) : N) = a
have h : ∑ i ∈ s,
    (↑((fun (i : ι) ↦
            (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) sorry : ↥(p i)))
          i) :
      N) =
  a
Tactic: use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
⊢ ∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N) =
    a
have h : Eq (α := N)
  (∑ i ∈ s,
    (↑((fun (i : ι) ↦
            (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) sorry : ↥(p i)))
          i) :
      N))
  (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))
Tactic: rw [← hμ]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
⊢ Eq (α := N)
    (∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N))
    (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))
have h : Eq (α := N) (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))
  (∑ i ∈ s,
    (↑((fun (i : ι) ↦
            (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) sorry : ↥(p i)))
          i) :
      N))
Tactic: symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
⊢ Eq (α := N) (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))
    (∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N))
have h : μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) ⊆ s
Tactic: apply Finset.sum_subset
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
h : μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) ⊆ s
⊢ Eq (α := N) (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N))
    (∑ i ∈ s,
      (↑((fun (i : ι) ↦
              (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) i) : N) ⋯ : ↥(p i)))
            i) :
        N))
have h₁ : ∀ x ∈ s,
  x ∉ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) →
    Eq.{u_6 + 1} (α := N)
      ((fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) x ((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x)) 0
Tactic: apply Finset.sum_subset
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
⊢ x ∈ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) → x ∈ s
have h : x ∉ s → x ∉ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
Tactic: contrapose
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
hx : x ∉ s
⊢ x ∉ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
have h : (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0
Tactic: rw [mem_support_iff, not_ne_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
hx : x ∉ s
⊢ (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0
have h : (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x) : N) = (↑0 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
hx : x ∉ s
⊢ (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x) : N) = (↑0 : N)
have h : Membership.mem (γ := Submodule R N) ⊥ (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x) : N)
Tactic: rw [coe_zero, ← mem_bot R]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
hx : x ∉ s
⊢ Membership.mem (γ := Submodule R N) ⊥ (↑((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x) : N)
have h : Eq.{u_6 + 1} (α := Submodule R N) ⊥ (⨆ (_ : x ∈ s), p x)
Tactic: suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
h : x ∈ s
hx : x ∉ μ.support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
⊢ Eq.{u_6 + 1} (α := N)
    ((fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) x ((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x)) 0
have hx₁ : (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0
Tactic: rw [mem_support_iff, not_ne_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)
hμ : (μ.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
x : ι
h : x ∈ s
hx : (μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x = 0
⊢ Eq.{u_6 + 1} (α := N)
    ((fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) x ((μ : (a : ι) → ↥(⨆ (_ : a ∈ s), p a)) x)) 0
have h : Eq.{u_6 + 1} (α := N) ((fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) x 0) 0
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
⊢ ∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
    (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
have mpr : (i : (↑(↑s : Set ι) : Type u_1)) → ↥(⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι))
Tactic: refine ⟨DFinsupp.mk s ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
mpr : (i : (↑(↑s : Set ι) : Type u_1)) → ↥(⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι))
⊢ ∃ (f : Π₀ (i : ι), ↥(⨆ (_ : i ∈ s), p i)),
    (f.sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) = a
have mpr₁ : (sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
    (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
      Subtype.casesOn (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) (motive := fun (x : (↑(↑s : Set ι) : Type u_1)) ↦
        ↥(⨆ (_ : (↑x : ι) ∈ s), p (↑x : ι))) i fun (i : ι) (hi : i ∈ (↑s : Set ι)) ↦
        Subtype.mk (p := fun (x : N) ↦
          Membership.mem (γ := Submodule R N)
            (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
              p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
            x)
          (↑(μ i) : N) sorry)
    fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) =
  a
Tactic: refine ⟨DFinsupp.mk s ?_, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
⊢ ↥(⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
      p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
have mpr : Membership.mem (γ := Submodule R N)
  (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
    p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
  (↑(μ i) : N)
Tactic: refine ⟨μ i, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
⊢ Membership.mem (γ := Submodule R N)
    (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
      p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
    (↑(μ i) : N)
have mpr : (↑(μ i) : N) ∈ p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι)
Tactic: rw [iSup_pos]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
i : ι
hi : i ∈ (↑s : Set ι)
mpr : (↑(μ i) : N) ∈ p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι)
⊢ Membership.mem (γ := Submodule R N)
    (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
      p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
    (↑(μ i) : N)
have mpr₁ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s
Tactic: rw [iSup_pos]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
⊢ (sum (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
      (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
        Subtype.casesOn (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) (motive := fun (x : (↑(↑s : Set ι) : Type u_1)) ↦
          ↥(⨆ (_ : (↑x : ι) ∈ s), p (↑x : ι))) i fun (i : ι) (hi : i ∈ (↑s : Set ι)) ↦
          Subtype.mk (p := fun (x : N) ↦
            Membership.mem (γ := Submodule R N)
              (⨆ (_ : (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι) ∈ s),
                p (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ (↑s : Set ι)) i hi) : ι))
              x)
            (↑(μ i) : N) ⋯)
      fun (x : ι) (xi : ↥(⨆ (_ : x ∈ s), p x)) ↦ (↑xi : N)) =
    a
have mpr : ∑
    x ∈
      support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
        (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
          Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
            (↑(μ (↑i : ι)) : N) sorry),
    (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
              Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                (↑(μ (↑i : ι)) : N) sorry :
            (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
          x) :
      N) =
  a
Tactic: simp only [DFinsupp.sum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
s : Finset ι
p : ι → Submodule R N
a : N
μ : (i : ι) → ↥(p i)
hμ : ∑ i ∈ s, (↑(μ i) : N) = a
⊢ ∑
      x ∈
        support (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i))
          (DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
            Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
              (↑(μ (↑i : ι)) : N) ⋯),
      (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
                Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                  (↑(μ (↑i : ι)) : N) ⋯ :
              (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
            x) :
        N) =
    a
have mpr : Eq.{u_6 + 1} (α := N)
  (∑ x ∈ s,
    (↑((DFinsupp.mk (β := fun (i : ι) ↦ ↥(⨆ (_ : i ∈ s), p i)) s fun (i : (↑(↑s : Set ι) : Type u_1)) ↦
              Subtype.mk (p := fun (x : N) ↦ Membership.mem (γ := Submodule R N) (⨆ (_ : (↑i : ι) ∈ s), p (↑i : ι)) x)
                (↑(μ (↑i : ι)) : N) sorry :
            (a : ι) → ↥(⨆ (_ : a ∈ s), p a))
          x) :
      N))
  (∑ i ∈ s, (↑(μ i) : N))
Tactic: rw [Finset.sum_subset support_mk_subset, ← hμ]