awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
ι : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
⊢ Free R (ι →₀ M)

Tactic:
.of_basis (Finsupp.basis fun _ => Module.Free.chooseBasis R M)

Premises used: Module.Free.of_basis, Finsupp.basis, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
ι : Type u_3
inst : Semiring R
⊢ Eq (α := (a : ι) → ι →₀ R) (⇑Finsupp.basisSingleOne : (a : ι) → ι →₀ R) fun (i : ι) ↦ single i 1

Tactic:
funext fun _ => Basis.apply_eq_iff.mpr rfl

Premises used: Iff.mpr, funext, Module.Basis.apply_eq_iff, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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)
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))
⊢ IsCompl (α := Submodule R (ι →₀ R)) (LinearMap.range (lmapDomain R R u))
    (span R (Set.range fun (x : β) ↦ single (v x) 1))

Tactic:
rw [range_lmapDomain]

Premises used: Finsupp.range_lmapDomain
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 ((⇑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
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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))
rwa₂ rwa₃ rwa₄ 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))
⊢ 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

Premises used: Set.range_comp, Function.comp_def
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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
rw :
  LinearIndependent (ι := (_ : ι) × PUnit.{1}) R (M := ι →₀ M)
    ((fun (i : ι) ↦ single i (v i)) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))
⊢ LinearIndependent R (M := ι →₀ M) fun (i : ι) ↦ single i (v i)

Tactic:
rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]

Premises used: Equiv.sigmaPUnit, linearIndependent_equiv
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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
⊢ ∀ (i : ι), LinearIndependent.{0, u_1, u_2} (ι := Unit) R (M := M) ((fun (i : ι) (x : Unit) ↦ v i) i)

Tactic:
simp +contextual [hv]
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 (ι := (_ : ι) × PUnit.{1}) R (M := ι →₀ M)
    ((fun (i : ι) ↦ single i (v i)) ∘ (⇑(Equiv.sigmaPUnit ι) : (a : (_ : ι) × PUnit.{1}) → ι))

Tactic:
exact linearIndependent_single (f := fun i (_ : Unit) ↦ v i) <| by simp +contextual [hv]

Premises used: Finsupp.linearIndependent_single
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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) ⋯ ⋯)

Tactic:
Finsupp.basisSingleOne.ext fun i ↦ ?_

Premises used: Finsupp.basisSingleOne, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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)
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) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
        α →₀ R)
⊢ 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) ⋯ ⋯)

Tactic:
refine Finsupp.basisSingleOne.ext fun i ↦ ?_

Premises used: Finsupp.basisSingleOne, Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : ι
rw : Membership.mem (γ := Set ι) ⊤ i
⊢ i ∈ Set.range u ⊔ Set.range v

Tactic:
rw [codisjoint_iff.mp h.2]

Premises used: codisjoint_iff, Iff.mp, IsCompl.codisjoint
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : ι
⊢ Membership.mem (γ := Set ι) ⊤ i

Tactic:
trivial
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : ι
inl :
  ∀ (i : α),
    Eq (α := α →₀ R)
      ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
      (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
                (lmapDomain R R u) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
        α →₀ R)
inr :
  ∀ (i : β),
    Eq (α := α →₀ R)
      ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
      (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
                (lmapDomain R R u) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) :
        α →₀ R)
⊢ 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) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
      α →₀ R)

Tactic:
obtain ⟨i, rfl⟩ | ⟨i, rfl⟩ : i ∈ Set.range u ⊔ .range v := by rw [codisjoint_iff.mp h.2]; trivial

Premises used: Set.range, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : α
⊢ Eq (α := ι →₀ R) (single (u i) 1) ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : α
⊢ Eq (α := ι →₀ R) (single (u i) 1) ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1))

Tactic:
have : single (u i) 1 = lmapDomain R R u (.single i 1) := by simp
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : α
this : Eq (α := ι →₀ R) (single (u i) 1) ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1))
inl :
  Eq (α := α →₀ R) (single i 1)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
            (lmapDomain R R u) ⋯ ⋯ :
          (ι →₀ R) →ₗ[R] α →₀ R) :
        (a : ι →₀ R) → α →₀ R)
      (single (u i) 1))
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
      α →₀ R)

Tactic:
simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_single]

Premises used: Finsupp.comapDomain_single, Finsupp.lcomapDomain_apply, Finsupp.coe_basisSingleOne
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : α
this : Eq (α := ι →₀ R) (single (u i) 1) ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1))
inl :
  Eq (α := α →₀ R) (single i 1)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
            (lmapDomain R R u) ⋯ ⋯ :
          (ι →₀ R) →ₗ[R] α →₀ R) :
        (a : ι →₀ R) → α →₀ R)
      ((lmapDomain R R u : (a : α →₀ R) → ι →₀ R) (single i 1)))
inl₁ inl₂ : Eq (α := α →₀ R) (single i 1) (single i 1)
⊢ Eq (α := α →₀ R) (single i 1)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
            (lmapDomain R R u) ⋯ ⋯ :
          (ι →₀ R) →ₗ[R] α →₀ R) :
        (a : ι →₀ R) → α →₀ R)
      (single (u i) 1))

Tactic:
rw [this, LinearMap.linearProjOfIsCompl_apply_left]

Premises used: LinearMap.linearProjOfIsCompl_apply_left
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : β
inr :
  Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (0 : α →₀ R)
inr₁ :
  Membership.mem (α := ι →₀ R) (γ := Submodule R (ι →₀ R)) (span R (Set.range fun (x : β) ↦ single (v x) 1))
    ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i) : ι →₀ R)
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
              (lmapDomain R R u) ⋯ ⋯ :
            (ι →₀ R) →ₗ[R] α →₀ R) :
          (a : ι →₀ R) → α →₀ R)
        ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) :
      α →₀ R)

Tactic:
rw [LinearMap.linearProjOfIsCompl_apply_right']

Premises used: LinearMap.linearProjOfIsCompl_apply_right'
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : β
inr :
  ∀ (j : α),
    Eq.{u_1 + 1} (α := R)
      ((((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R) :
            (a : α) → R)
          j :
        R)
      ((0 : (a : α) → R) j : R)
⊢ Eq (α := α →₀ R)
    ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
    (0 : α →₀ R)

Tactic:
ext j
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : β
j : α
inr : v i = u j → Eq.{u_1 + 1} (α := R) 1 0
⊢ Eq.{u_1 + 1} (α := R)
    ((((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R) :
          (a : α) → R)
        j :
      R)
    ((0 : (a : α) → R) j : R)

Tactic:
simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_apply, single_apply,
        coe_zero, Pi.zero_apply, ite_eq_right_iff]

Premises used: Pi.zero_apply, Finsupp.lcomapDomain_apply, Finsupp.comapDomain_apply, Finsupp.coe_basisSingleOne, ite_eq_right_iff, Finsupp.single_apply, Finsupp.coe_zero
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : β
j : α
hij : v i = u j
⊢ Eq.{u_1 + 1} (α := R) 1 0

Tactic:
(Set.disjoint_range_iff.mp h.1 j i hij.symm).elim

Premises used: False.elim, Iff.mp, Eq.symm, IsCompl.disjoint, Set.disjoint_range_iff
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : β
j : α
hij : v i = u j
⊢ Eq.{u_1 + 1} (α := R) 1 0

Tactic:
exact (Set.disjoint_range_iff.mp h.1 j i hij.symm).elim

Premises used: False.elim, Iff.mp, Eq.symm, IsCompl.disjoint, Set.disjoint_range_iff
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : β
⊢ Membership.mem (α := ι →₀ R) (γ := Submodule R (ι →₀ R)) (span R (Set.range fun (x : β) ↦ single (v x) 1))
    ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i) : ι →₀ R)

Tactic:
Submodule.subset_span ⟨i, rfl⟩

Premises used: Exists.intro, Submodule.subset_span, rfl
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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 : β
⊢ Membership.mem (α := ι →₀ R) (γ := Submodule R (ι →₀ R)) (span R (Set.range fun (x : β) ↦ single (v x) 1))
    ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i) : ι →₀ R)

Tactic:
exact Submodule.subset_span ⟨i, rfl⟩
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
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)
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) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) i) :
        α →₀ R)
inl :
  ∀ (i : α),
    Eq (α := α →₀ R)
      ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) : α →₀ R)
      (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
                (lmapDomain R R u) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (u i)) :
        α →₀ R)
inr inr₁ :
  ∀ (i : β),
    Eq (α := α →₀ R)
      ((lcomapDomain u hu : (a : ι →₀ R) → α →₀ R) ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) : α →₀ R)
      (((LinearMap.linearProjOfIsCompl (E := ι →₀ R) (span R (Set.range fun (x : β) ↦ single (v x) 1)) (F := α →₀ R)
                (lmapDomain R R u) ⋯ ⋯ :
              (ι →₀ R) →ₗ[R] α →₀ R) :
            (a : ι →₀ R) → α →₀ R)
          ((Finsupp.basisSingleOne : (a : ι) → ι →₀ R) (v i)) :
        α →₀ R)
⊢ 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) ⋯ ⋯)

Tactic:
classical
  refine Finsupp.basisSingleOne.ext fun i ↦ ?_
  obtain ⟨i, rfl⟩ | ⟨i, rfl⟩ : i ∈ Set.range u ⊔ .range v := by rw [codisjoint_iff.mp h.2]; trivial
  · have : single (u i) 1 = lmapDomain R R u (.single i 1) := by simp
    simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_single]
    rw [this, LinearMap.linearProjOfIsCompl_apply_left]
  · rw [LinearMap.linearProjOfIsCompl_apply_right']
    · ext j
      simp only [coe_basisSingleOne, lcomapDomain_apply, comapDomain_apply, single_apply,
        coe_zero, Pi.zero_apply, ite_eq_right_iff]
      intro hij
      exact (Set.disjoint_range_iff.mp h.1 j i hij.symm).elim
    · exact Submodule.subset_span ⟨i, rfl⟩

Premises used: Finsupp.basisSingleOne, Pi.zero_apply, Finsupp.comapDomain_single, Finsupp.lcomapDomain_apply, Finsupp.comapDomain_apply, Finsupp.coe_basisSingleOne, ite_eq_right_iff, LinearMap.linearProjOfIsCompl_apply_right', Finsupp.single_apply, Set.range, LinearMap.linearProjOfIsCompl_apply_left, Module.Basis.ext, rfl, Finsupp.coe_zero
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : Free S M
inst_8 : Free R S
⊢ Free R M

Tactic:
let e : (ChooseBasisIndex S M →₀ S) ≃ₗ[R] ChooseBasisIndex S M →₀ (ChooseBasisIndex R S →₀ R) :=
    Finsupp.mapRange.linearEquiv (chooseBasis R S).repr
  let e : M ≃ₗ[R] ChooseBasisIndex S M →₀ (ChooseBasisIndex R S →₀ R) :=
    (chooseBasis S M).repr.restrictScalars R ≪≫ₗ e
  .of_equiv e.symm

Premises used: LinearEquiv.symm, LinearEquiv.restrictScalars, Finsupp.mapRange.linearEquiv, Module.Basis.repr, Module.Free.of_equiv, LinearEquiv.trans, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
n : Type u_3
inst : DecidableEq n
inst_1 : Semiring R
inst_2 : Fintype n
a : R
i : n
⊢ Eq (α := n →₀ R) (∑ x : n, Finsupp.single x (if i = x then a else 0)) (Finsupp.single i a)

Tactic:
simp only [apply_ite (Finsupp.single _), Finsupp.single_zero, Finset.sum_ite_eq,
    if_pos (Finset.mem_univ _)]

Premises used: Finset.mem_univ, apply_ite, if_pos, Finsupp.single_zero, Finset.sum_ite_eq, Finsupp.single
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
n : Type u_3
inst : DecidableEq n
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Finite n
b : Basis n R M
i : n
intro :
  ∀ (val : Fintype n),
    Eq.{u_2 + 1} (α := M) ((b.equivFun.symm : (a : n → R) → M) (Pi.single (M := fun (a : n) ↦ R) i 1) : M)
      ((b : (a : n) → M) i : M)
⊢ Eq.{u_2 + 1} (α := M) ((b.equivFun.symm : (a : n → R) → M) (Pi.single (M := fun (a : n) ↦ R) i 1) : M)
    ((b : (a : n) → M) i : M)

Tactic:
cases nonempty_fintype n

Premises used: nonempty_fintype
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
M : Type u_2
n : Type u_3
inst : DecidableEq n
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Finite n
b : Basis n R M
i : n
val : Fintype n
⊢ Eq.{u_2 + 1} (α := M) ((b.equivFun.symm : (a : n → R) → M) (Pi.single (M := fun (a : n) ↦ R) i 1) : M)
    ((b : (a : n) → M) i : M)

Tactic:
simp [Pi.single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : Ring S
inst_2 : Algebra R S
ι : Type u_3
B : Basis ι R S
i : ι
r : R
s : S
rw :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₁ :
  (((B.repr : (a : S) → ι →₀ R) (HSMul.hSMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₂ :
  (((B.repr : (a : S) → ι →₀ R) (r • s) : ι →₀ R) : (a : ι) → R) i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₃ :
  (HSMul.hSMul (β := ι →₀ R) r ((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
rw₄ rw₅ :
  HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R) =
    HSMul.hSMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)
⊢ (((B.repr : (a : S) → ι →₀ R) (HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) r : S) s) : ι →₀ R) : (a : ι) → R)
      i =
    HMul.hMul (β := R) r ((((B.repr : (a : S) → ι →₀ R) s : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
rw [← smul_eq_mul, ← smul_eq_mul, algebraMap_smul, map_smul, Finsupp.smul_apply]

Premises used: algebraMap_smul, Finsupp.smul_apply, smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
M : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : Free R S
⊢ Free R S[M]

Tactic:
.finsupp ..

Premises used: Module.Free.finsupp, AddMonoidAlgebra
-- Module: Mathlib.LinearAlgebra.Finsupp.VectorSpace
Goal:
M : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : Module R S
inst_3 : Free R S
⊢ Free R S[M]

Tactic:
.finsupp ..

Premises used: Module.Free.finsupp, MonoidAlgebra