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 : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
simp_rw :
  (∀ (i : ι), Disjoint (p i) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j)) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
simp_rw₁ :
  (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
⊢ iSupIndep p ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
have mp : (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) →
  ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
Tactic: classical
  simp_rw [iSupIndep_def, Submodule.disjoint_def]
  constructor
  · intro h s v hv hv0 i hi
    apply h _ _ (hv i hi)
    rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0
    rw [← Submodule.neg_mem_iff, hv0]
    exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)
  · intro h i x hx hsup
    obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
    contrapose! h
    use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
    refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
    · beta_reduce
      split_ifs with h
      · exact (p j).neg_mem (h ▸ hx)
      · simpa [h] using hf j
    · specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
simp_rw :
  (∀ (i : ι), Disjoint (p i) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j)) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
simp_rw₁ :
  (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
mp :
  (∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0) →
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
⊢ iSupIndep p ↔
    ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
have mpr : (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0) →
  ∀ (i : ι), ∀ x ∈ p i, Membership.mem (γ := Submodule R N) (⨆ (j : ι), ⨆ (_ : j ≠ i), p j) x → x = 0
Tactic: classical
  simp_rw [iSupIndep_def, Submodule.disjoint_def]
  constructor
  · intro h s v hv hv0 i hi
    apply h _ _ (hv i hi)
    rw [← s.add_sum_erase _ hi, add_eq_zero_iff_neg_eq] at hv0
    rw [← Submodule.neg_mem_iff, hv0]
    exact SetLike.le_def.mp (biSup_mono <| by grind) (Submodule.sum_mem_biSup <| by grind)
  · intro h i x hx hsup
    obtain ⟨f, hf, rfl⟩ := (Submodule.mem_iSup_iff_exists_finsupp ..).mp hsup
    contrapose! h
    use insert i f.support, fun j ↦ if j = i then -f.sum fun _ x ↦ x else f j
    refine ⟨fun j hj ↦ ?_, ?_, by grind⟩
    · beta_reduce
      split_ifs with h
      · exact (p j).neg_mem (h ▸ hx)
      · simpa [h] using hf j
    · specialize hf i
      simp at hf
      grind [Finsupp.sum, Finset.sum_congr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
⊢ iSupIndep p ↔
    ∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
have rw : (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0) ↔
  ∀ (s : Finset ι) (v w : ι → N),
    (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
Tactic: rw [iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0) ↔
    ∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
have mp : (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0) →
  ∀ (s : Finset ι) (v w : ι → N),
    (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
mp :
  (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0) →
    ∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
⊢ (∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0) ↔
    ∀ (s : Finset ι) (v w : ι → N),
      (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
have mpr : (∀ (s : Finset ι) (v w : ι → N),
    (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i) →
  ∀ (s : Finset ι) (v : ι → N), (∀ i ∈ s, v i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0 → ∀ i ∈ s, v i = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
p : ι → Submodule R N
h :
  ∀ (s : Finset ι) (v w : ι → N),
    (∀ i ∈ s, v i ∈ p i ∧ w i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, w i) → ∀ i ∈ s, v i = w i
s : Finset ι
v : ι → N
hv : ∀ i ∈ s, v i ∈ p i
hv0 : Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) 0
⊢ ∀ i ∈ s, v i = 0
have h₁ : (∀ i ∈ s, v i ∈ p i ∧ 0 i ∈ p i) → Eq.{u_6 + 1} (α := N) (∑ i ∈ s, v i) (∑ i ∈ s, 0 i) → ∀ i ∈ s, v i = 0 i
Tactic: specialize h s v 0
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
S : Type u_4
M : ι → Type u_5
N : Type u_6
inst : DecidableEq ι
inst_1 : Ring R
inst_2 : AddCommGroup N
inst_3 : Module R N
p : ι → Submodule R N
ind : iSupIndep p
iSup_top : Eq.{u_6 + 1} (α := Submodule R N) (⨆ (i : ι), p i) ⊤
⊢ Function.Surjective (α := Π₀ (i : ι), ↥(p i)) (β := N)
    (⇑((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
          fun (i : ι) ↦ (p i).subtype) :
      (a : Π₀ (i : ι), ↥(p i)) → N)
have rwa : Eq.{u_6 + 1} (α := Submodule R N)
  (LinearMap.range (R := R) (M := Π₀ (i : ι), ↥(p i)) (τ₁₂ := RingHom.id R)
    ((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
      (p i).subtype))
  ⊤
Tactic: rwa [← LinearMap.range_eq_top, ← Submodule.iSup_eq_range_dfinsupp_lsum]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R v
have rw : ∀ (l : ι →₀ R), Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N) → l = 0
Tactic: rw [linearIndependent_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
⊢ a = 0
have a₁ : Eq.{u_6 + 1} (α := N)
  (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
          (p i).subtype :
        (a : Π₀ (i : ι), ↥(p i)) → N)
      a :
    N)
  (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
          (p i).subtype :
        (a : Π₀ (i : ι), ↥(p i)) → N)
      0 :
    N)
Tactic: apply hp.dfinsupp_lsum_injective
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
⊢ Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        a :
      N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        0 :
      N)
have a₁ : ∀
  (hl :
    Eq.{u_6 + 1} (α := N)
      ((((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N)
                fun (i : ι) ↦ (p i).subtype) ∘ₗ
              (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
                  LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) sorry)) ∘ₗ
                (↑(finsuppLequivDFinsupp R) : (ι →₀ R) →ₗ[R] Π₀ (x : ι), R) :
            (a : ι →₀ R) → N)
          l :
        N)
      (0 : N)),
  let a : Π₀ (i : ι), ↥(p i) :=
    (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
          LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) sorry) :
        (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
      l.toDFinsupp;
  Eq.{u_6 + 1} (α := N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        a :
      N)
    (((lsum ℕ (M := fun (i : ι) ↦ ↥(p i)) : (a : (i : ι) → ↥(p i) →ₗ[R] N) → (Π₀ (i : ι), ↥(p i)) →ₗ[R] N) fun (i : ι) ↦
            (p i).subtype :
          (a : Π₀ (i : ι), ↥(p i)) → N)
        0 :
      N)
Tactic: rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
Cleared hypotheses: hl, a
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
⊢ l = 0
have ha : a = 0
Tactic: have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
⊢ l = 0
have h : ∀ (i : ι), Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
i : ι
⊢ Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
have h : Eq.{u_6 + 1} (α := N) ((fun (x : R) ↦ x • v i) ((l : (a : ι) → R) i)) ((fun (x : R) ↦ x • v i) ((0 : (a : ι) → R) i))
Tactic: apply smul_left_injective R (hv' i)
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
i : ι
⊢ Eq.{u_6 + 1} (α := N) ((fun (x : R) ↦ x • v i) ((l : (a : ι) → R) i)) ((fun (x : R) ↦ x • v i) ((0 : (a : ι) → R) i))
have this : HSMul.hSMul.{u_3, u_6, u_6} (α := R) ((l : (a : ι) → R) i : R) (v i) = (↑((a : (a : ι) → ↥(p a)) i) : N)
Tactic: have : l i • v i = a i := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (hypothesis)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
l : ι →₀ R
hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)
a : Π₀ (i : ι), ↥(p i) :=
  (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
        LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
      (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
    l.toDFinsupp
ha : a = 0
i : ι
this : HSMul.hSMul.{u_3, u_6, u_6} (α := R) ((l : (a : ι) → R) i : R) (v i) = (↑((a : (a : ι) → ↥(p a)) i) : N)
⊢ Eq.{u_6 + 1} (α := N) ((fun (x : R) ↦ x • v i) ((l : (a : ι) → R) i)) ((fun (x : R) ↦ x • v i) ((0 : (a : ι) → R) i))
have this₁ : Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) (0 : R) ∨ v i = 0
Tactic: simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R v
have rw : ∀ (l : ι →₀ R), Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N) → l = 0
Tactic: classical
  rw [linearIndependent_iff]
  intro l hl
  let a :=
    DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
      l.toDFinsupp
  have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
  ext i
  apply smul_left_injective R (hv' i)
  have : l i • v i = a i := rfl
  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
  simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
rw rw₁ rw₂ rw₃ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)), l = 0
rw₄ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)), l = 0
⊢ LinearIndependent R v
have rw₅ : ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
  let a : Π₀ (i : ι), ↥(p i) :=
    (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
          LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) sorry) :
        (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
      l.toDFinsupp;
  ∀ (ha : a = 0), l = 0
Tactic: classical
  rw [linearIndependent_iff]
  intro l hl
  let a :=
    DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
      l.toDFinsupp
  have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
  ext i
  apply smul_left_injective R (hv' i)
  have : l i • v i = a i := rfl
  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
  simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
rw rw₁ rw₂ rw₃ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)), l = 0
rw₄ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)), l = 0
rw₅ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
    let a : Π₀ (i : ι), ↥(p i) :=
      (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
            LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
          (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
        l.toDFinsupp;
    ∀ (ha : a = 0), l = 0
⊢ LinearIndependent R v
have h : ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
  let a : Π₀ (i : ι), ↥(p i) :=
    (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
          LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) sorry) :
        (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
      l.toDFinsupp;
  ∀ (ha : a = 0) (i : ι), Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
Tactic: classical
  rw [linearIndependent_iff]
  intro l hl
  let a :=
    DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
      l.toDFinsupp
  have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
  ext i
  apply smul_left_injective R (hv' i)
  have : l i • v i = a i := rfl
  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
  simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
R : Type u_3
N : Type u_6
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
inst_3 : IsDomain R
inst_4 : IsTorsionFree R N
ι : Type u_7
p : ι → Submodule R N
hp : iSupIndep p
v : ι → N
hv : ∀ (i : ι), v i ∈ p i
hv' : ∀ (i : ι), v i ≠ 0
rw rw₁ rw₂ rw₃ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)), l = 0
rw₄ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)), l = 0
rw₅ :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
    let a : Π₀ (i : ι), ↥(p i) :=
      (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
            LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
          (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
        l.toDFinsupp;
    ∀ (ha : a = 0), l = 0
h :
  ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
    let a : Π₀ (i : ι), ↥(p i) :=
      (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
            LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) ⋯) :
          (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
        l.toDFinsupp;
    ∀ (ha : a = 0) (i : ι), Eq.{u_3 + 1} (α := R) ((l : (a : ι) → R) i : R) ((0 : (a : ι) → R) i : R)
⊢ LinearIndependent R v
have h₁ : ∀ (l : ι →₀ R) (hl : Eq.{u_6 + 1} (α := N) ((Finsupp.linearCombination R v : (a : ι →₀ R) → N) l : N) (0 : N)),
  let a : Π₀ (i : ι), ↥(p i) :=
    (mapRange.linearMap (β₁ := fun (i : ι) ↦ R) (β₂ := fun (i : ι) ↦ ↥(p i)) fun (i : ι) ↦
          LinearMap.toSpanSingleton R (↥(p i)) (Subtype.mk (p := fun (x : N) ↦ x ∈ p i) (v i) sorry) :
        (a : Π₀ (i : ι), R) → Π₀ (i : ι), ↥(p i))
      l.toDFinsupp;
  ∀ (ha : a = 0) (i : ι),
    Eq.{u_6 + 1} (α := N) ((fun (x : R) ↦ x • v i) ((l : (a : ι) → R) i))
      ((fun (x : R) ↦ x • v i) ((0 : (a : ι) → R) i))
Tactic: classical
  rw [linearIndependent_iff]
  intro l hl
  let a :=
    DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
      l.toDFinsupp
  have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
  ext i
  apply smul_left_injective R (hv' i)
  have : l i • v i = a i := rfl
  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
  simpa
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
n : Type u_7
inst_1 : Fintype n
inst_2 : DecidableEq n
M N : Matrix n n A
⊢ (M * N).det = (N * M).det
have rw : M.det * N.det = (N * M).det
Tactic: rw [det_mul, det_mul, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Determinant (goal)
Goal:
A : Type u_5
inst : CommRing A
n : Type u_7
inst_1 : Fintype n
inst_2 : DecidableEq n
M N : Matrix n n A
rw : M.det * N.det = (N * M).det
⊢ (M * N).det = (N * M).det
have rw₁ : M.det * N.det = N.det * M.det
Tactic: rw [det_mul, det_mul, mul_comm]