awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
have h : ∀ (a : (i : ι) × φ i) (i : ι),
  (((linearCombination R fun (ix : (i : ι) × φ i) ↦
                single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
                  (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))) ∘ₗ
              Finsupp.lsingle a :
            (a : R) → Π₀ (i : ι), M i)
          1 :
        (a : ι) → M a)
      i =
    ((((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
                  linearCombination R (f i)) ∘ₗ
                (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R)) ∘ₗ
              Finsupp.lsingle a :
            (a : R) → Π₀ (i : ι), M i)
          1 :
        (a : ι) → M a)
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
have this : Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
  (linearCombination R fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
  ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
      linearCombination R (f i)) ∘ₗ
    (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
Tactic: have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
this :
  Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
⊢ LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
have rw : Function.Injective (α := (i : ι) × φ i →₀ R) (β := Π₀ (i : ι), M i)
  (⇑((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
          linearCombination R (f i)) ∘ₗ
        (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R)) :
    (a : (i : ι) × φ i →₀ R) → Π₀ (i : ι), M i)
Tactic: rw [LinearIndependent, this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
have have : Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
  (linearCombination R fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
  ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
      linearCombination R (f i)) ∘ₗ
    (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
Tactic: classical
  have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp
  rw [LinearIndependent, this]
  exact ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
ι : Type u_1
R : Type u_2
M : ι → Type u_3
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_2, u_3} R (M i)
inst_3 : DecidableEq ι
φ : ι → Type u_4
f : (i : ι) → φ i → M i
hf : ∀ (i : ι), LinearIndependent R (f i)
have :
  Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
    (linearCombination R fun (ix : (i : ι) × φ i) ↦
      single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
        (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
    ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
        linearCombination R (f i)) ∘ₗ
      (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))
⊢ LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
have have₁ : ∀
  (this :
    Eq (α := ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), M i)
      (linearCombination R fun (ix : (i : ι) × φ i) ↦
        single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
          (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
      ((mapRange.linearMap (β₁ := fun (i : ι) ↦ Finsupp.{u_4, u_2} (φ i) R) (β₂ := M) fun (i : ι) ↦
          linearCombination R (f i)) ∘ₗ
        (↑(sigmaFinsuppLequivDFinsupp R (η := φ)) : ((i : ι) × φ i →₀ R) →ₗ[R] Π₀ (i : ι), φ i →₀ R))),
  LinearIndependent R (M := Π₀ (i : ι), M i) fun (ix : (i : ι) × φ i) ↦
    single (β := M) (ix.fst (β := fun (i : ι) ↦ φ i))
      (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
Tactic: classical
  have : linearCombination R (fun ix : Σ i, φ i ↦ single ix.1 (f ix.1 ix.2)) =
    DFinsupp.mapRange.linearMap (fun i ↦ linearCombination R (f i)) ∘ₗ
    (sigmaFinsuppLequivDFinsupp R).toLinearMap := by ext; simp
  rw [LinearIndependent, this]
  exact ((DFinsupp.mapRange_injective _ fun _ ↦ map_zero _).mpr hf).comp (Equiv.injective _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R (M := ι →₀ M) fun (ix : (i : ι) × φ i) ↦
    single (ix.fst (β := fun (i : ι) ↦ φ i)) (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
have h : ∀ (x : (i : ι) × φ i),
  Eq (α := ι →₀ M)
    (single (x.fst (β := fun (i : ι) ↦ φ i)) (f (x.fst (β := fun (i : ι) ↦ φ i)) (x.snd (β := fun (i : ι) ↦ φ i))))
    (Function.comp (β := Π₀ (i : ι), M)
      (⇑(↑(LinearEquiv.symm (finsuppLequivDFinsupp R)) : (Π₀ (x : ι), M) →ₗ[R] ι →₀ M) : (a : Π₀ (i : ι), M) → ι →₀ M)
      (fun (ix : (i : ι) × φ i) ↦
        DFinsupp.single (β := fun (i : ι) ↦ M) (ix.fst (β := fun (i : ι) ↦ φ i))
          (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
      x)
Tactic: convert!
    (DFinsupp.linearIndependent_single _ hf).map_injOn _
      (finsuppLequivDFinsupp R).symm.injective.injOn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
f : (i : ι) → φ i → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R (M := ι →₀ M) fun (ix : (i : ι) × φ i) ↦
    single (ix.fst (β := fun (i : ι) ↦ φ i)) (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i)))
have h : ∀ (x : (i : ι) × φ i),
  Eq (α := ι →₀ M)
    (single (x.fst (β := fun (i : ι) ↦ φ i)) (f (x.fst (β := fun (i : ι) ↦ φ i)) (x.snd (β := fun (i : ι) ↦ φ i))))
    (Function.comp (β := Π₀ (i : ι), M)
      (⇑(↑(LinearEquiv.symm (finsuppLequivDFinsupp R)) : (Π₀ (x : ι), M) →ₗ[R] ι →₀ M) : (a : Π₀ (i : ι), M) → ι →₀ M)
      (fun (ix : (i : ι) × φ i) ↦
        DFinsupp.single (β := fun (i : ι) ↦ M) (ix.fst (β := fun (i : ι) ↦ φ i))
          (f (ix.fst (β := fun (i : ι) ↦ φ i)) (ix.snd (β := fun (i : ι) ↦ φ i))))
      x)
Tactic: classical
  convert!
    (DFinsupp.linearIndependent_single _ hf).map_injOn _
      (finsuppLequivDFinsupp R).symm.injective.injOn
  simp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
x_1 : (i : ι) × φ i
i : ι
x : φ i
⊢ Eq (α := (i : ι) × φ i →₀ R)
    (((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
        (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
          ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
            ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
      (i : ι) × φ i →₀ R)
    (single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (i : ι) × φ i →₀ R)
have h : ∀ (j : ι) (y : φ j),
  Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
Tactic: ext ⟨j, y⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
x_1 : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
⊢ Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
have pos : ∀ (h : i = j),
  Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
x_1 : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
pos :
  ∀ (h : i = j),
    Eq.{u_1 + 1} (α := R)
      (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
                (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                  ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                    ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
              (i : ι) × φ i →₀ R) :
            (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
        R)
      ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
          (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
        R)
⊢ Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
have neg : ∀ (h : ¬i = j),
  Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis.{u_4, u_1, u_2} (φ i) R M
x_1 : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
⊢ Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) j y) :
      R)
have pos : ∀ (y : φ i),
  Eq.{u_1 + 1} (α := R)
    (((((Finsupp.basis (φ := φ) b).repr : (a : ι →₀ M) → (i : ι) × φ i →₀ R)
              (single ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i))
                ((b ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).fst (β := fun (i : ι) ↦ φ i)) : (a : φ ⟨i, x⟩.fst) → M)
                  ((Sigma.mk (β := fun (i : ι) ↦ φ i) i x).snd (β := fun (i : ι) ↦ φ i)))) :
            (i : ι) × φ i →₀ R) :
          (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) i y) :
      R)
    ((single (Sigma.mk (β := fun (i : ι) ↦ φ i) i x) 1 : (a : (i : ι) × φ i) → R)
        (Sigma.mk (β := fun (i : ι) ↦ φ i) i y) :
      R)
Tactic: cases h
Cleared hypotheses: j, y, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
⊢ IsCompl (α := Submodule R (ι →₀ R)) (LinearMap.range (lmapDomain R R u))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))
have rw : IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
  (span R (Set.range fun (x : β) ↦ single (v x) 1))
Tactic: rw [range_lmapDomain]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (hypothesis)
Goal:
R : Type u_1
ι : Type u_3
inst : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
⊢ IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))
have this : IsCompl (α := Submodule R (ι →₀ R)) (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range u))
  (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range v))
Tactic: have := (Finsupp.basisSingleOne (R := R)).linearIndependent.isCompl_span_image
     (Module.Basis.span_eq _) huv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this :
  IsCompl (α := Submodule R (ι →₀ R)) (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range u))
    (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range v))
⊢ IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))
have rwa : ∀
  (this :
    IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) ∘ u)))
      (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range v))),
  IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))
Tactic: rwa [← Set.range_comp, ← Set.range_comp, Function.comp_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this :
  IsCompl (α := Submodule R (ι →₀ R)) (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range u))
    (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range v))
rwa :
  ∀
    (this :
      IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) ∘ u)))
        (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range v))),
    IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      (span R (Set.range fun (x : β) ↦ single (v x) 1))
⊢ IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))
have rwa₁ : ∀
  (this :
    IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) ∘ u)))
      (span R (Set.range ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) ∘ v)))),
  IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))
Tactic: rwa [← Set.range_comp, ← Set.range_comp, Function.comp_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Semiring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
huv : IsCompl (Set.range u) (Set.range v)
this :
  IsCompl (α := Submodule R (ι →₀ R)) (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range u))
    (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range v))
rwa :
  ∀
    (this :
      IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) ∘ u)))
        (span R ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) '' Set.range v))),
    IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      (span R (Set.range fun (x : β) ↦ single (v x) 1))
rwa₁ :
  ∀
    (this :
      IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) ∘ u)))
        (span R (Set.range ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) ∘ v)))),
    IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
      (span R (Set.range fun (x : β) ↦ single (v x) 1))
⊢ IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))
have rwa₂ : ∀
  (this :
    IsCompl (α := Submodule R (ι →₀ R))
      (span R (Set.range fun (x : α) ↦ (Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u x)))
      (span R (Set.range ((⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) ∘ v)))),
  IsCompl (α := Submodule R (ι →₀ R)) (span R (Set.range fun (x : α) ↦ single (u x) 1))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))
Tactic: rwa [← Set.range_comp, ← Set.range_comp, Function.comp_def] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : IsDomain R
inst_3 : Module R M
inst_4 : IsTorsionFree R M
v : ι → M
hv : ∀ (i : ι), v i ≠ 0
⊢ LinearIndependent R (M := ι →₀ M) fun (i : ι) ↦ single i (v i)
have rw : LinearIndependent (ι := (_ : ι) × PUnit.{1}) R (M := ι →₀ M)
  ((fun (i : ι) ↦ single i (v i)) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))
Tactic: rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
⊢ Eq (α := (ι →₀ R) →ₗ[R] α →₀ R) (lcomapDomain u hu)
    (LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
      (lmapDomain R R u) ⋯ ⋯)
have refine : ∀ (i : ι),
  Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) sorry sorry :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
      α →₀ R)
Tactic: refine Finsupp.basisSingleOne.ext fun i ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Finsupp.VectorSpace (goal)
Goal:
R : Type u_1
ι : Type u_3
inst : Ring R
α : Type u_4
β : Type u_5
u : α → ι
v : β → ι
hu : Function.Injective u
h : IsCompl (Set.range u) (Set.range v)
i : ι
⊢ i ∈ Set.range u ⊔ Set.range v
have rw : Membership.mem (γ := Set ι) ⊤ i
Tactic: rw [codisjoint_iff.mp h.2]