awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι_1 : Type x
ι' : Type x'
inst : Semiring R
φ : ι_1 → Type u_1
ψ : ι_1 → Type u_2
χ : ι_1 → Type u_3
inst_1 : (i : ι_1) → AddCommMonoid (φ i)
inst_2 : (i : ι_1) → Module.{u, u_1} R (φ i)
inst_3 : (i : ι_1) → AddCommMonoid (ψ i)
inst_4 : (i : ι_1) → Module.{u, u_2} R (ψ i)
inst_5 : (i : ι_1) → AddCommMonoid (χ i)
inst_6 : (i : ι_1) → Module.{u, u_3} R (χ i)
ι : Type u_4
M : Option ι → Type u_5
inst_7 : (i : Option ι) → AddCommMonoid (M i)
inst_8 : (i : Option ι) → Module.{u, u_5} R (M i)
⊢ ∀ (m : R) (x : (i : Option ι) → M i),
    Equiv.toFun (Equiv.piOptionEquivProd (β := M)) (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) (Equiv.toFun (Equiv.piOptionEquivProd (β := M)) x)

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
S : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module S M
inst_7 : SMulCommClass R S M
f : (ι → R) →ₗ[R] M
i : ι
⊢ Eq.{v + 1} (α := M) ((piRing R M ι S : (a : (ι → R) →ₗ[R] M) → ι → M) f i : M)
    ((f : (a : ι → R) → M) (Pi.single (M := fun (a : ι) ↦ R) i 1) : M)

Tactic:
rfl

Premises used: Function.update, Pi.single, dite, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
ι : Type x
inst : Semiring R
S : Type u_4
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : Semiring S
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : Module S M
inst_7 : SMulCommClass R S M
f : ι → M
g : ι → R
⊢ Eq.{v + 1} (α := M)
    ((((symm (piRing R M ι S) : (a : ι → M) → (ι → R) →ₗ[R] M) f : (ι → R) →ₗ[R] M) : (a : ι → R) → M) g : M)
    (∑ i : ι, g i • f i : M)

Tactic:
simp [piRing, LinearMap.lsum_apply]

Premises used: LinearMap.lsum_apply, LinearEquiv.piRing
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
f g : α ⊕ β → M
fst :
  ∀ (x : α),
    ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).1 x =
      ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).1 x
snd :
  ∀ (x : β),
    ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).2 x =
      ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).2 x
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (f + g) =
    (Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
f g : α ⊕ β → M
x : α
⊢ ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).1 x =
    ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).1 x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
f g : α ⊕ β → M
x : β
⊢ ((Equiv.sumArrowEquivProdArrow α β M).toFun (f + g)).2 x =
    ((Equiv.sumArrowEquivProdArrow α β M).toFun f + (Equiv.sumArrowEquivProdArrow α β M).toFun g).2 x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
r : R
f : α ⊕ β → M
fst :
  ∀ (x : α),
    ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).1 x =
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)).1 x
snd :
  ∀ (x : β),
    ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).2 x =
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)).2 x
⊢ (Equiv.sumArrowEquivProdArrow α β M).toFun (r • f) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
r : R
f : α ⊕ β → M
x : α
⊢ ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).1 x =
    (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)).1 x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R_1
φ : ι → Type u_1
ψ : ι → Type u_2
χ : ι → Type u_3
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, u_1} R_1 (φ i)
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_2} R_1 (ψ i)
inst_5 : (i : ι) → AddCommMonoid (χ i)
inst_6 : (i : ι) → Module.{u, u_3} R_1 (χ i)
S : Type u_4
inst_7 : Fintype ι
inst_8 : DecidableEq ι
inst_9 : Semiring S
inst_10 : AddCommMonoid M_1
inst_11 : Module R_1 M_1
inst_12 : Module S M_1
inst_13 : SMulCommClass R_1 S M_1
α : Type u_5
β : Type u_6
R : Type u_7
M : Type u_8
inst_14 : Semiring R
inst_15 : AddCommMonoid M
inst_16 : Module R M
r : R
f : α ⊕ β → M
x : β
⊢ ((Equiv.sumArrowEquivProdArrow α β M).toFun (r • f)).2 x =
    (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) ((Equiv.sumArrowEquivProdArrow α β M).toFun f)).2 x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
β : Type u_6
f : α ⊕ β → M
a : α
⊢ ((sumArrowLequivProdArrow α β R M : (a : α ⊕ β → M) → (α → M) × (β → M)) f).1 a = f (Sum.inl a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
β : Type u_6
f : α ⊕ β → M
b : β
⊢ ((sumArrowLequivProdArrow α β R M : (a : α ⊕ β → M) → (α → M) × (β → M)) f).2 b = f (Sum.inr b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
β : Type u_6
f : α → M
g : β → M
a : α
⊢ (symm (sumArrowLequivProdArrow α β R M) : (a : (α → M) × (β → M)) → α ⊕ β → M) (f, g) (Sum.inl a) = f a

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
α : Type u_5
β : Type u_6
f : α → M
g : β → M
b : β
⊢ (symm (sumArrowLequivProdArrow α β R M) : (a : (α → M) × (β → M)) → α ⊕ β → M) (f, g) (Sum.inr b) = g b

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
ι : Type u_5
R : Type u_6
M : Type u_7
inst : Unique ι
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
⊢ Eq (α := (a : ι → M) → M) (⇑(funUnique ι R M) : (a : ι → M) → M) (eval (β := fun (x : ι) ↦ M) default)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
M : Fin 2 → Type v
inst_1 : (i : Fin 2) → AddCommMonoid (M i)
inst_2 : (i : Fin 2) → Module.{u, v} R (M i)
⊢ Eq (α := (a : (i : Fin 2) → M i) → M 0 × M 1) (⇑(piFinTwo R M) : (a : (i : Fin 2) → M i) → M 0 × M 1)
    fun (f : (i : Fin 2) → M i) ↦ (f 0, f 1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x ↔
    ∀ (k : ι'), x (Sum.inr k) = 0

Tactic:
⟨fun hx k ↦ ?_, fun hx ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
refine_1 :
  ∀
    (hx :
      Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
        (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x)
    (k : ι'), x (Sum.inr k) = 0
refine_2 :
  ∀ (hx : ∀ (k : ι'), x (Sum.inr k) = 0),
    Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x ↔
    ∀ (k : ι'), x (Sum.inr k) = 0

Tactic:
refine ⟨fun hx k ↦ ?_, fun hx ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x_1 : ι ⊕ ι' → R
k : ι'
x : ι ⊕ ι' → R
h : Membership.mem (γ := Set (ι ⊕ ι' → R)) (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1) x
refine_1 :
  ∀ (i : ι),
    Eq.{u + 1} (α := R)
      ((fun (i : ι) ↦ (single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1 : (j : ι ⊕ ι') → R)) i (Sum.inr k)) 0
⊢ x (Sum.inr k) = 0

Tactic:
obtain ⟨i, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
k : ι'
i : ι
⊢ Eq.{u + 1} (α := R)
    ((fun (i : ι) ↦ (single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1 : (j : ι ⊕ ι') → R)) i (Sum.inr k)) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
k : ι'
⊢ Eq.{u + 1} (α := R) (0 (Sum.inr k)) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
k : ι'
u v : ι ⊕ ι' → R
hx :
  Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) u
hy :
  Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) v
hu : u (Sum.inr k) = 0
hv : v (Sum.inr k) = 0
⊢ (u + v) (Sum.inr k) = 0

Tactic:
simp [hu, hv]
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
k : ι'
t : R
u : ι ⊕ ι' → R
hx :
  Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) u
hu : u (Sum.inr k) = 0
⊢ (t • u) (Sum.inr k) = 0

Tactic:
simp [hu]
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx :
  Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
k : ι'
refine_1 :
  ∀ (x : ι ⊕ ι' → R)
    (h :
      Membership.mem (γ := Set (ι ⊕ ι' → R)) (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
        x),
    x (Sum.inr k) = 0
refine_1₁ : Eq.{u + 1} (α := R) (0 (Sum.inr k)) 0
refine_1₂ :
  ∀ (u v : ι ⊕ ι' → R),
    Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
        (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) u →
      Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
          (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) v →
        ∀ (hu : u (Sum.inr k) = 0) (hv : v (Sum.inr k) = 0), (u + v) (Sum.inr k) = 0
refine_1₃ :
  ∀ (t : R) (u : ι ⊕ ι' → R),
    Membership.mem (γ := Submodule R (ι ⊕ ι' → R))
        (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) u →
      ∀ (hu : u (Sum.inr k) = 0), (t • u) (Sum.inr k) = 0
⊢ x (Sum.inr k) = 0

Tactic:
induction hx using span_induction with
    | mem x h => obtain ⟨i, rfl⟩ := h; simp
    | zero => simp
    | add u v _ _ hu hv => simp [hu, hv]
    | smul t u _ hu => simp [hu]

Premises used: Submodule.smul, Submodule.zero, Submodule.add, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
refine_2 :
  ∀ (this : Fintype ι),
    Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
      (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this_1 : Fintype ι
this :
  x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
rw :
  Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
    (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x

Tactic:
rw [this]
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this_1 : Fintype ι
this :
  x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
    (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))

Tactic:
sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i

Premises used: SMulMemClass.smul_mem, Set.mem_range_self, Set.Mem, Sum.inl, Submodule.subset_span, sum_mem
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this_1 : Fintype ι
this :
  x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
    (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))

Tactic:
exact sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i

Premises used: SMulMemClass.smul_mem, Set.mem_range_self, Submodule.subset_span, sum_mem
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
refine_2 :
  x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)
⊢ Membership.mem (γ := Submodule R ((j : ι ⊕ ι') → R))
    (span R (Set.range fun (i : ι) ↦ single (M := fun (a : ι ⊕ ι') ↦ R) (Sum.inl i) 1)) x

Tactic:
suffices x = ∑ i : ι, x (Sum.inl i) • Pi.single (M := fun _ ↦ R) (Sum.inl i) (1 : R) by
      rw [this]
      exact sum_mem <| fun i _ ↦ SMulMemClass.smul_mem _ <| subset_span <| Set.mem_range_self i
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
refine_2 :
  ∀ (i : ι),
    x (Sum.inl i) =
      (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
        (Sum.inl i)
refine_2₁ :
  ∀ (i : ι'),
    x (Sum.inr i) =
      (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
        (Sum.inr i)
⊢ x = ∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1)

Tactic:
ext (i | i)
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι
⊢ x (Sum.inl i) =
    (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
      (Sum.inl i)

Tactic:
simp [single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
ι' : Type x'
inst : DecidableEq ι
inst_1 : DecidableEq ι'
inst_2 : Finite ι
inst_3 : Semiring R
x : ι ⊕ ι' → R
hx : ∀ (k : ι'), x (Sum.inr k) = 0
this : Fintype ι
i : ι'
⊢ x (Sum.inr i) =
    (∑ i : ι, HSMul.hSMul (β := (j : ι ⊕ ι') → R) (x (Sum.inl i)) (single (M := fun (x : ι ⊕ ι') ↦ R) (Sum.inl i) 1))
      (Sum.inr i)

Tactic:
simp [hx i]
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
η : Type u_1
inst : Semiring R
s : ι → η
r : R
f : ι → R
⊢ extend s (r • f) 0 = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R) (extend s f 0)

Tactic:
simpa using Function.extend_smul r s f 0

Premises used: OfNat.ofNat, Function.extend_smul
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
n : ℕ
M : Fin n.succ → Type u_1
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : Fin n.succ) → Module.{u, u_1} R (M i)
x y : M 0 × ((i : Fin n) → M i.succ)
⊢ ∀ (i : Fin n), (consEquiv M).toFun (x + y) i.succ = ((consEquiv M).toFun x + (consEquiv M).toFun y) i.succ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
n : ℕ
M : Fin n.succ → Type u_1
inst : Semiring R
inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)
inst_2 : (i : Fin n.succ) → Module.{u, u_1} R (M i)
c : R
x : M 0 × ((i : Fin n) → M i.succ)
⊢ ∀ (i : Fin n),
    (consEquiv M).toFun (c • x) i.succ =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) c : R) ((consEquiv M).toFun x) i.succ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
M₃ : Type y
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₃
inst_3 : Module R M
inst_4 : Module R M₃
m : M
⊢ Eq.{y + 1} (α := Fin 0 → M₃) ((vecEmpty : (a : M) → Fin 0 → M₃) m : Fin 0 → M₃) (![] : Fin 0 → M₃)

Tactic:
rfl

Premises used: absurd, Matrix.vecEmpty, rfl, Fin.elim0
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M : Type v
M₂ : Type w
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₂
inst_3 : Module R M
inst_4 : Module R M₂
n : ℕ
f : M →ₗ[R] M₂
g : LinearMap.{u, u, v, w} (RingHom.id R) M (Fin n → M₂)
m : M
⊢ Eq.{w + 1} (α := Fin n.succ → M₂) ((f.vecCons g : (a : M) → Fin n.succ → M₂) m : Fin n.succ → M₂)
    (Matrix.vecCons ((f : (a : M) → M₂) m) ((g : (a : M) → Fin n → M₂) m) : Fin n.succ → M₂)

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
inst : Semiring R
ι : Type v
inst_1 : Finite ι
motive : (N : Type u) → [inst_4 : AddCommMonoid N] → [Module R N] → Prop
motive' : (N : Type (max u v)) → [inst_4 : AddCommMonoid N] → [Module R N] → Prop
equiv :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'] (a : N ≃ₗ[R] N'), motive N → motive' N'
equiv' :
  ∀ {N N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'] (a : N ≃ₗ[R] N'), motive' N → motive' N'
unit : motive PUnit.{u + 1}
prod :
  ∀ {N : Type u} {N' : Type (max u v)} [inst_4 : AddCommMonoid N] [inst_5 : AddCommMonoid N'] [inst_6 : Module R N]
    [inst_7 : Module R N'], motive N → motive' N' → motive' (N × N')
M : ι → Type u
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module R (M i)
h : ∀ (i : ι), motive (M i)
intro : ∀ (val : Fintype ι), motive' ((i : ι) → M i)
⊢ motive' ((i : ι) → M i)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype