awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
c : S
f : ι → M'
⊢ linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) =
    HSMul.hSMul (α := S) (β := M →ₗ[R] M') ((RingHom.id S : (a : S) → S) c : S)
      (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))

Tactic:
b.ext fun i => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
c : S
f : ι → M'
refine :
  ∀ (i : ι),
    Eq.{u_7 + 1} (α := M')
      ((linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → M')
          ((b : (a : ι) → M) i : M) :
        M')
      ((HSMul.hSMul (α := S) (β := M →ₗ[R] M') ((RingHom.id S : (a : S) → S) c : S)
              (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)) :
            (a : M) → M')
          ((b : (a : ι) → M) i : M) :
        M')
⊢ linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) =
    HSMul.hSMul (α := S) (β := M →ₗ[R] M') ((RingHom.id S : (a : S) → S) c : S)
      (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R))

Tactic:
refine b.ext fun i => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
c : S
f : ι → M'
i : ι
⊢ Eq.{u_7 + 1} (α := M')
    ((linearCombination R id ∘ₗ lmapDomain R R (c • f) ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
    ((HSMul.hSMul (α := S) (β := M →ₗ[R] M') ((RingHom.id S : (a : S) → S) c : S)
            (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)) :
          (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f : ι → M'
h :
  ∀ (x : ι),
    (fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M'))
        ((fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M')) f)
        x =
      f x
⊢ (fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M'))
      ((fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M')) f) =
    f

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f : ι → M'
x : ι
⊢ (fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M'))
      ((fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M')) f)
      x =
    f x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f : M →ₗ[R] M'
⊢ (fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M'))
      ((fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')) f) =
    f

Tactic:
b.ext fun i => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f : M →ₗ[R] M'
refine :
  ∀ (i : ι),
    Eq.{u_7 + 1} (α := M')
      (((fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M'))
              ((fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')) f) :
            (a : M) → M')
          ((b : (a : ι) → M) i : M) :
        M')
      ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')
⊢ (fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M'))
      ((fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')) f) =
    f

Tactic:
refine b.ext fun i => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι_1 : Type u_1
ι' : Type u_2
R_1 : Type u_3
R₂ : Type u_4
K : Type u_5
M_1 : Type u_6
M' : Type u_7
M'' : Type u_8
V : Type u
V' : Type u_9
inst : Semiring R_1
inst_1 : AddCommMonoid M_1
inst_2 : Module R_1 M_1
inst_3 : AddCommMonoid M'
inst_4 : Module R_1 M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_5 : Semiring R
inst_6 : AddCommMonoid M
inst_7 : Module R M
b : Basis ι R M
inst_8 : Module R M'
S : Type u_13
inst_9 : Semiring S
inst_10 : Module S M'
inst_11 : SMulCommClass R S M'
f : M →ₗ[R] M'
i : ι
⊢ Eq.{u_7 + 1} (α := M')
    (((fun (f : ι → M') ↦ (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M'))
            ((fun (f : M →ₗ[R] M') (i : ι) ↦ ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')) f) :
          (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
    ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
⊢ Eq (α := M →ₗ[R] M') ((b.constr S : (a : ι → M') → M →ₗ[R] M') f : M →ₗ[R] M')
    (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R) : M →ₗ[R] M')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
simp :
  Eq (α := M') (sum (mapDomain f (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x)) fun (i : M') (a : R) ↦ a • id i)
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
⊢ Eq.{u_7 + 1} (α := M') ((((b.constr S : (a : ι → M') → M →ₗ[R] M') f : M →ₗ[R] M') : (a : M) → M') x : M')
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b : M')

Tactic:
simp only [constr_def, LinearMap.comp_apply, lmapDomain_apply, linearCombination_apply]

Premises used: LinearMap.comp_apply, Finsupp.linearCombination_apply, Module.Basis.constr_def, Finsupp.lmapDomain_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
rw :
  Eq.{u_7 + 1} (α := M') (sum (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x) fun (a : ι) (m : R) ↦ m • id (f a))
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)
h_zero : ∀ (b : M'), HSMul.hSMul.{u_11, u_7, u_7} (α := R) 0 (id b) = 0
h_add : ∀ (b : M') (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
⊢ Eq (α := M') (sum (mapDomain f (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x)) fun (i : M') (a : R) ↦ a • id i)
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)

Tactic:
rw [Finsupp.sum_mapDomain_index]

Premises used: Finsupp.sum_mapDomain_index
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
⊢ Eq.{u_7 + 1} (α := M') (sum (((↑b.repr : M →ₗ[R] ι →₀ R) : (a : M) → ι →₀ R) x) fun (a : ι) (m : R) ↦ m • id (f a))
    (sum ((b.repr : (a : M) → ι →₀ R) x) fun (b : ι) (a : R) ↦ a • f b)

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ∀ (b : M'), HSMul.hSMul.{u_11, u_7, u_7} (α := R) 0 (id b) = 0

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
x : M
⊢ ∀ (b : M') (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b

Tactic:
simp [add_smul]

Premises used: add_smul
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : M →ₗ[R] M'
i : ι
⊢ Eq.{u_7 + 1} (α := M') ((LinearEquiv.symm (b.constr S) : (a : M →ₗ[R] M') → ι → M') f i : M')
    ((f : (a : M) → M') ((b : (a : ι) → M) i : M) : M')

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
i : ι
⊢ (((b.constr S : (a : ι → M') → M →ₗ[R] M') f : M →ₗ[R] M') : (a : M) → M') ((b : (a : ι) → M) i : M) = f i

Tactic:
simp [Basis.constr_apply, b.repr_self]

Premises used: Module.Basis.constr_apply, Module.Basis.repr_self
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
g : ι → M'
f : M →ₗ[R] M'
h : ∀ (i : ι), g i = (f : (a : M) → M') ((b : (a : ι) → M) i : M)
⊢ (b.constr S : (a : ι → M') → M →ₗ[R] M') g = f

Tactic:
b.ext fun i => (b.constr_basis S g i).trans (h i)

Premises used: Module.Basis.constr_basis, Module.Basis.ext, Eq.trans
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : M →ₗ[R] M'
⊢ ((b.constr S : (a : ι → M') → M →ₗ[R] M') fun (i : ι) ↦ (f : (a : M) → M') ((b : (a : ι) → M) i : M)) = f

Tactic:
b.constr_eq S fun _ => rfl

Premises used: rfl, Module.Basis.constr_eq
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : ι → M'
rw :
  Eq (α := Submodule R M') (LinearMap.range (linearCombination R id ∘ₗ lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)))
    (span R (range f))
rw₁ :
  Eq (α := Submodule R M') (map (linearCombination R id) (lmapDomain R R f ∘ₗ (↑b.repr : M →ₗ[R] ι →₀ R)).range)
    (span R (range f))
rw₂ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (↑b.repr : M →ₗ[R] ι →₀ R).range))
    (span R (range f))
rw₃ : Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) ⊤)) (span R (range f))
rw₄ :
  Eq (α := Submodule R M') (map (linearCombination R id) (map (lmapDomain R R f) (supported R R univ)))
    (span R (range f))
rw₅ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (range f))
rw₆ : Eq (α := Submodule R M') (map (linearCombination R id) (supported R R (f '' univ))) (span R (f '' univ))
rw₇ : Eq (α := Submodule R M') (span R (id '' f '' univ)) (span R (f '' univ))
rw₈ rw₉ : Eq (α := Submodule R M') (span R (f '' univ)) (span R (f '' univ))
⊢ Eq (α := Submodule R M')
    (LinearMap.range.{u_11, u_11, u_12, u_7} (R := R) (M := M) (τ₁₂ := RingHom.id R)
      ((b.constr S : (a : ι → M') → M →ₗ[R] M') f))
    (span R (range f))

Tactic:
rw [b.constr_def S f, LinearMap.range_comp, LinearMap.range_comp, LinearEquiv.range, ←
    Finsupp.supported_univ, Finsupp.lmapDomain_supported, ← Set.image_univ, ←
    Finsupp.span_image_eq_map_linearCombination, Set.image_id]

Premises used: Set.image_univ, Finsupp.span_image_eq_map_linearCombination, Finsupp.supported_univ, LinearMap.range_comp, Module.Basis.constr_def, Set.image_id, LinearEquiv.range, Finsupp.lmapDomain_supported
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
S : Type u_13
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
f : M' →ₗ[R] M'
v : ι → M'
i : ι
⊢ Eq.{u_7 + 1} (α := M')
    ((((b.constr S : (a : ι → M') → M →ₗ[R] M') ((⇑f : (a : M') → M') ∘ v) : M →ₗ[R] M') : (a : M) → M')
        ((b : (a : ι) → M) i : M) :
      M')
    ((f ∘ₗ (b.constr S : (a : ι → M') → M →ₗ[R] M') v : (a : M) → M') ((b : (a : ι) → M) i : M) : M')

Tactic:
simp only [Basis.constr_basis, LinearMap.comp_apply, Function.comp]

Premises used: LinearMap.comp_apply, Function.comp, Module.Basis.constr_basis
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R M'
S : Type u_14
inst_5 : Semiring S
inst_6 : Module S M'
inst_7 : SMulCommClass R S M'
inst_8 : Fintype ι
b : Basis ι R M
f : ι → M'
x : M
⊢ Eq.{u_7 + 1} (α := M') ((((b.constr S : (a : ι → M') → M →ₗ[R] M') f : M →ₗ[R] M') : (a : M) → M') x : M')
    (∑ i : ι, HSMul.hSMul.{u_11, u_7, u_7} (α := R) ((b.equivFun : (a : M) → ι → R) x i : R) (f i) : M')

Tactic:
simp [b.constr_apply, b.equivFun_apply, Finsupp.sum_fintype]

Premises used: Finsupp.sum_fintype, Module.Basis.equivFun_apply, Module.Basis.constr_apply
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
i : ι
b' : Basis ι' R M'
e : ι ≃ ι'
⊢ Eq.{u_7 + 1} (α := M') ((b.equiv b' e : (a : M) → M') ((b : (a : ι) → M) i : M) : M')
    ((b' : (a : ι') → M') ((e : (a : ι) → ι') i : ι') : M')

Tactic:
simp [Basis.equiv]

Premises used: Module.Basis.equiv
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_11
M : Type u_12
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
i : ι
⊢ Eq (α := M) ((b.equiv b (Equiv.refl ι) : (a : M) → M) ((b : (a : ι) → M) i : M) : M)
    ((LinearEquiv.refl R M : (a : M) → M) ((b : (a : ι) → M) i : M) : M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι'
⊢ Eq.{u_7 + 1} (α := M')
    ((b.equiv b' e : (a : M) → M') (((b.equiv b' e).symm : (a : M') → M) ((b' : (a : ι') → M') i : M') : M) : M')
    ((b.equiv b' e : (a : M) → M') ((b'.equiv b e.symm : (a : M') → M) ((b' : (a : ι') → M') i : M') : M) : M')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
b : Basis ι R M
inst_4 : Module R M'
M'' : Type u_13
b' : Basis ι' R M'
inst_5 : AddCommMonoid M''
inst_6 : Module R M''
ι'' : Type u_14
b'' : Basis ι'' R M''
e : ι ≃ ι'
e' : ι' ≃ ι''
i : ι
⊢ Eq.{u_13 + 1} (α := M'') ((b.equiv b' e ≪≫ₗ b'.equiv b'' e' : (a : M) → M'') ((b : (a : ι) → M) i : M) : M'')
    ((b.equiv b'' (e.trans e') : (a : M) → M'') ((b : (a : ι) → M) i : M) : M'')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
a :
  ∀ (i : ι),
    Eq.{u_7 + 1} (α := M') ((b.map (b.equiv b' e) : (a : ι) → M') i : M') ((b'.reindex e.symm : (a : ι) → M') i : M')
⊢ b.map (b.equiv b' e) = b'.reindex e.symm

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
M' : Type u_7
inst : AddCommMonoid M'
ι : Type u_10
R : Type u_11
M : Type u_12
inst_1 : Semiring R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι
⊢ Eq.{u_7 + 1} (α := M') ((b.map (b.equiv b' e) : (a : ι) → M') i : M') ((b'.reindex e.symm : (a : ι) → M') i : M')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
ι : Type u_10
R : Type u_14
M : Type u_15
M' : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst_5 : SMulCommClass R R M'
f : M → M'
g : M' → M
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set M') (range.{u_16, u_2 + 1} (ι := ι') (⇑b' : (a : ι') → M')) (f ((b : (a : ι) → M) i))
hg :
  ∀ (i : ι'),
    Membership.mem (γ := Set M) (range.{u_15, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) (g ((b' : (a : ι') → M') i))
hgf : ∀ (i : ι), g (f ((b : (a : ι) → M) i)) = (b : (a : ι) → M) i
hfg : ∀ (i : ι'), f (g ((b' : (a : ι') → M') i)) = (b' : (a : ι') → M') i
i : ι
⊢ (b.equiv' b' f g hf hg hgf hfg : (a : M) → M') ((b : (a : ι) → M) i : M) = f ((b : (a : ι) → M) i)

Tactic:
b.constr_basis R _ _

Premises used: Module.Basis.constr_basis
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι' : Type u_2
ι : Type u_10
R : Type u_14
M : Type u_15
M' : Type u_16
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid M'
inst_4 : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
inst_5 : SMulCommClass R R M'
f : M → M'
g : M' → M
hf :
  ∀ (i : ι),
    Membership.mem (γ := Set M') (range.{u_16, u_2 + 1} (ι := ι') (⇑b' : (a : ι') → M')) (f ((b : (a : ι) → M) i))
hg :
  ∀ (i : ι'),
    Membership.mem (γ := Set M) (range.{u_15, u_10 + 1} (ι := ι) (⇑b : (a : ι) → M)) (g ((b' : (a : ι') → M') i))
hgf : ∀ (i : ι), g (f ((b : (a : ι) → M) i)) = (b : (a : ι) → M) i
hfg : ∀ (i : ι'), f (g ((b' : (a : ι') → M') i)) = (b' : (a : ι') → M') i
i : ι'
⊢ ((b.equiv' b' f g hf hg hgf hfg).symm : (a : M') → M) ((b' : (a : ι') → M') i : M') = g ((b' : (a : ι') → M') i)

Tactic:
b'.constr_basis R _ _

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, Module.Basis.constr_basis, Finset.sum
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
rw :
  (((b.repr : (a : M) → ι →₀ R)
          (∑ i : ι',
            HSMul.hSMul.{u_14, u_15, u_15} (α := R) (β := M)
              ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) i : R) ((b' : (a : ι') → M) i : M)) :
        (a : ι) → R)
      i :
    R)
| ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
rw [← b'.sum_repr x]

Premises used: Module.Basis.sum_repr
-- Module: Mathlib.LinearAlgebra.Basis.Defs
Goal:
ι : Type u_10
R : Type u_14
M : Type u_15
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
b : Basis ι R M
ι' : Type u_17
inst_3 : Fintype ι'
b' : Basis ι' R M
x : M
i : ι
conv_rhs :
  Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
        HMul.hMul (α := R) (β := R)
          ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
          ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) :
      R)
    (((b.repr : (a : M) → ι →₀ R)
            (∑ i : ι',
              HSMul.hSMul.{u_14, u_15, u_15} (α := R) (β := M)
                ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) i : R) ((b' : (a : ι') → M) i : M)) :
          (a : ι) → R)
        i :
      R)
⊢ Eq.{u_14 + 1} (α := R)
    (∑ j : ι',
        HMul.hMul (α := R) (β := R)
          ((((b.repr : (a : M) → ι →₀ R) ((b' : (a : ι') → M) j) : ι →₀ R) : (a : ι) → R) i : R)
          ((((b'.repr : (a : M) → ι' →₀ R) x : ι' →₀ R) : (a : ι') → R) j : R) :
      R)
    ((((b.repr : (a : M) → ι →₀ R) x : ι →₀ R) : (a : ι) → R) i : R)

Tactic:
conv_rhs => rw [← b'.sum_repr x]

Premises used: Module.Basis.sum_repr