awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian.{u_1, u_2} K (V ⧸ A)
eqOn_A : Set.EqOn.{u_2, u_4} (β := V₂) (⇑u : (a : V) → V₂) (⇑v : (a : V) → V₂) (↑A : Set V)
⊢ A ≤ eqLocus u v

Tactic:
have A_le : A ≤ eqLocus u v := le_eqLocus.mpr eqOn_A
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian.{u_1, u_2} K (V ⧸ A)
eqOn_A : Set.EqOn.{u_2, u_4} (β := V₂) (⇑u : (a : V) → V₂) (⇑v : (a : V) → V₂) (↑A : Set V)
A_le : A ≤ eqLocus u v
rw : IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))
⊢ u ≈ v

Tactic:
rw [equiv_iff_isNoetherian_quotient_eqLocus]

Premises used: LinearMap.FiniteRangeSetoid.equiv_iff_isNoetherian_quotient_eqLocus
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian.{u_1, u_2} K (V ⧸ A)
eqOn_A : Set.EqOn.{u_2, u_4} (β := V₂) (⇑u : (a : V) → V₂) (⇑v : (a : V) → V₂) (↑A : Set V)
A_le : A ≤ eqLocus u v
⊢ Eq (α := Submodule K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v)))
    (range (A.mapQ (eqLocus u v) id A_le)) ⊤

Tactic:
simp [range_mapQ]

Premises used: Submodule.range_mapQ
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
u v : V →ₗ[K] V₂
A : Submodule K V
quot_A_noeth : IsNoetherian.{u_1, u_2} K (V ⧸ A)
eqOn_A : Set.EqOn.{u_2, u_4} (β := V₂) (⇑u : (a : V) → V₂) (⇑v : (a : V) → V₂) (↑A : Set V)
A_le : A ≤ eqLocus u v
⊢ IsNoetherian.{u_1, u_2} K (HasQuotient.Quotient V (B := Submodule K V) (eqLocus u v))

Tactic:
refine isNoetherian_of_surjective (A.mapQ (eqLocus u v) id A_le) (by simp [range_mapQ])

Premises used: LinearMap.id, isNoetherian_of_surjective, LinearMap.eqLocus, Submodule.mapQ
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : IsNoetherianRing K
u v : V →ₗ[K] V₂
A : Submodule K V
A_coFG : A.CoFG
eqOn_A : Set.EqOn.{u_2, u_4} (β := V₂) (⇑u : (a : V) → V₂) (⇑v : (a : V) → V₂) (↑A : Set V)
⊢ u ≈ v

Tactic:
equiv_iff_eqLocus_coFG.mpr <| A_coFG.of_le <| le_eqLocus.mpr eqOn_A

Premises used: Iff.mpr, LinearMap.FiniteRangeSetoid.equiv_iff_eqLocus_coFG, Submodule.CoFG.of_le, LinearMap.le_eqLocus
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u : V →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h' : v ≈ v'
rw : ∀ (h' : (v - v').HasNoetherianRange), (v ∘ₗ u - v' ∘ₗ u).HasNoetherianRange
⊢ v ∘ₗ u ≈ v' ∘ₗ u

Tactic:
rw [equiv_iff_hasNoetherianRange] at *

Premises used: LinearMap.FiniteRangeSetoid.equiv_iff_hasNoetherianRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u : V →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h' : (v - v').HasNoetherianRange
⊢ (v ∘ₗ u - v' ∘ₗ u).HasNoetherianRange

Tactic:
h'.comp_right u

Premises used: LinearMap.HasNoetherianRange.comp_right
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u : V →ₗ[K] V₂
v v' : V₂ →ₗ[K] V₃
h' : (v - v').HasNoetherianRange
⊢ (v ∘ₗ u - v' ∘ₗ u).HasNoetherianRange

Tactic:
exact h'.comp_right u

Premises used: LinearMap.HasNoetherianRange.comp_right
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u v : V →ₗ[K] V₂
u' : V₂ →ₗ[K] V₃
h : u ≈ v
rw : ∀ (h : (u - v).HasNoetherianRange), (u' ∘ₗ u - u' ∘ₗ v).HasNoetherianRange
⊢ u' ∘ₗ u ≈ u' ∘ₗ v

Tactic:
rw [equiv_iff_hasNoetherianRange] at *

Premises used: LinearMap.FiniteRangeSetoid.equiv_iff_hasNoetherianRange
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u v : V →ₗ[K] V₂
u' : V₂ →ₗ[K] V₃
h : (u - v).HasNoetherianRange
⊢ (u' ∘ₗ u - u' ∘ₗ v).HasNoetherianRange

Tactic:
simpa only [LinearMap.comp_sub] using h.comp_left u'

Premises used: LinearMap.HasNoetherianRange.comp_left, LinearMap.comp_sub
-- Module: Mathlib.Algebra.Module.LinearMap.FiniteRange
Goal:
K : Type u_1
V : Type u_2
V₂ : Type u_4
V₃ : Type u_6
inst : CommRing K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : AddCommGroup V₂
inst_4 : Module K V₂
inst_5 : AddCommGroup V₃
inst_6 : Module K V₃
u v : V →ₗ[K] V₂
u' v' : V₂ →ₗ[K] V₃
h : u ≈ v
h' : u' ≈ v'
grw : v' ∘ₗ u ≈ v' ∘ₗ v
grw₁ grw₂ : (setoid : (V →ₗ[K] V₃) → (V →ₗ[K] V₃) → Prop) (v' ∘ₗ v) (v' ∘ₗ v)
⊢ u' ∘ₗ u ≈ v' ∘ₗ v

Tactic:
grw [equiv_comp_right h', equiv_comp_left h]

Premises used: LinearMap.FiniteRangeSetoid.equiv_comp_right, LinearMap.FiniteRangeSetoid.equiv_comp_left
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M : Matrix m n R
i : m
c : n → R
⊢ (eval c : (a : MvPolynomial n R) → R) (M.toMvPolynomial i) = (M *ᵥ c) i

Tactic:
simp only [toMvPolynomial, map_sum, eval_monomial, pow_zero, Finsupp.prod_single_index, pow_one,
    mulVec, dotProduct]

Premises used: dotProduct, Matrix.toMvPolynomial, map_sum, MvPolynomial.eval_monomial, pow_zero, pow_one, Matrix.mulVec, Finsupp.prod_single_index
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
S : Type u_5
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : CommSemiring S
f : R →+* S
M : Matrix m n R
i : m
⊢ Eq (α := MvPolynomial n S) (toMvPolynomial (M.map (⇑f : (a : R) → S)) i)
    ((MvPolynomial.map f : (a : MvPolynomial n R) → MvPolynomial n S) (M.toMvPolynomial i))

Tactic:
simp only [toMvPolynomial, map_apply, map_sum, map_monomial]

Premises used: Matrix.map_apply, Matrix.toMvPolynomial, map_sum, MvPolynomial.map_monomial
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M : Matrix m n R
i : m
h :
  ∀ (i_1 : n),
    Membership.mem (γ := Finset n) Finset.univ i_1 →
      IsHomogeneous.{u_2, u_4} (σ := n) (R := R)
        ((monomial (Finsupp.single i_1 1) : (a : R) → MvPolynomial n R) (M i i_1)) 1
⊢ IsHomogeneous (M.toMvPolynomial i) 1

Tactic:
apply MvPolynomial.IsHomogeneous.sum

Premises used: MvPolynomial.IsHomogeneous.sum
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M : Matrix m n R
i : m
j : n
apply : Eq (α := ℕ) ((Finsupp.degree : (a : n →₀ ℕ) → ℕ) (Finsupp.single j 1) : ℕ) (1 : ℕ)
⊢ IsHomogeneous.{u_2, u_4} (σ := n) (R := R) ((monomial (Finsupp.single j 1) : (a : R) → MvPolynomial n R) (M i j)) 1

Tactic:
apply MvPolynomial.isHomogeneous_monomial _ _

Premises used: MvPolynomial.isHomogeneous_monomial
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M : Matrix m n R
i : m
j : n
⊢ Eq (α := ℕ) ((Finsupp.degree : (a : n →₀ ℕ) → ℕ) (Finsupp.single j 1) : ℕ) (1 : ℕ)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M : Matrix m n R
i : m
⊢ totalDegree (M.toMvPolynomial i) ≤ 1

Tactic:
apply (toMvPolynomial_isHomogeneous _ _).totalDegree_le

Premises used: MvPolynomial.IsHomogeneous.totalDegree_le, Matrix.toMvPolynomial_isHomogeneous
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M : Matrix m n R
i : m
⊢ Eq.{u_4 + 1} (α := R) ((constantCoeff : (a : MvPolynomial n R) → R) (M.toMvPolynomial i) : R) (0 : R)

Tactic:
simp only [toMvPolynomial, ← C_mul_X_eq_monomial, map_sum, map_mul, constantCoeff_X,
    mul_zero, Finset.sum_const_zero]

Premises used: MvPolynomial.C_mul_X_eq_monomial, Matrix.toMvPolynomial, map_sum, Finset.sum_const_zero, MulZeroClass.mul_zero, MvPolynomial.constantCoeff_X, map_mul
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
h : ∀ (x : m) (m_1 : n →₀ ℕ), Eq.{u_4 + 1} (α := R) (coeff m_1 (toMvPolynomial 0 x)) (coeff m_1 (0 x))
⊢ Eq (α := (i : m) → MvPolynomial n R) (toMvPolynomial 0) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
x : m
m_1 : n →₀ ℕ
⊢ Eq.{u_4 + 1} (α := R) (coeff m_1 (toMvPolynomial 0 x)) (coeff m_1 (0 x))

Tactic:
simp only [toMvPolynomial, zero_apply, map_zero, Finset.sum_const_zero, Pi.zero_apply]

Premises used: Matrix.zero_apply, Pi.zero_apply, map_zero, Matrix.toMvPolynomial, Finset.sum_const_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
h : ∀ (i : n), Eq (α := MvPolynomial n R) (toMvPolynomial 1 i) (X i)
⊢ Eq (α := (i : n) → MvPolynomial n R) (toMvPolynomial 1) X

Tactic:
ext i : 1
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
i : n
h : Eq (α := MvPolynomial n R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial n R) (1 i i)) (X i)
h₁ :
  ∀ (b : n),
    Membership.mem (γ := Finset n) Finset.univ b →
      b ≠ i → Eq (α := MvPolynomial n R) ((monomial (Finsupp.single b 1) : (a : R) → MvPolynomial n R) (1 i b)) 0
h₂ :
  i ∉ Finset.univ → Eq (α := MvPolynomial n R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial n R) (1 i i)) 0
⊢ Eq (α := MvPolynomial n R) (toMvPolynomial 1 i) (X i)

Tactic:
rw [toMvPolynomial, Finset.sum_eq_single i]

Premises used: Matrix.toMvPolynomial, Finset.sum_eq_single
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
i : n
⊢ Eq (α := MvPolynomial n R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial n R) (1 i i)) (X i)

Tactic:
simp only [one_apply_eq, ← C_mul_X_eq_monomial, C_1, one_mul]

Premises used: MvPolynomial.C_mul_X_eq_monomial, MvPolynomial.C_1, Matrix.one_apply_eq, one_mul
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
i j : n
hj : j ≠ i
⊢ Eq (α := MvPolynomial n R) ((monomial (Finsupp.single j 1) : (a : R) → MvPolynomial n R) (1 i j)) 0

Tactic:
simp only [one_apply_ne hj.symm, map_zero]

Premises used: Matrix.one_apply_ne, map_zero, Ne.symm
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
inst_2 : DecidableEq n
i : n
⊢ i ∉ Finset.univ → Eq (α := MvPolynomial n R) ((monomial (Finsupp.single i 1) : (a : R) → MvPolynomial n R) (1 i i)) 0

Tactic:
grind
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M N : Matrix m n R
h :
  ∀ (i : m),
    (M + N).toMvPolynomial i =
      HAdd.hAdd (α := (i : m) → MvPolynomial n R) (β := (i : m) → MvPolynomial n R) M.toMvPolynomial N.toMvPolynomial i
⊢ (M + N).toMvPolynomial = HAdd.hAdd (α := (i : m) → MvPolynomial n R) M.toMvPolynomial N.toMvPolynomial

Tactic:
ext i : 1
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
R : Type u_4
inst : Fintype n
inst_1 : CommSemiring R
M N : Matrix m n R
i : m
⊢ (M + N).toMvPolynomial i =
    HAdd.hAdd (α := (i : m) → MvPolynomial n R) (β := (i : m) → MvPolynomial n R) M.toMvPolynomial N.toMvPolynomial i

Tactic:
simp only [toMvPolynomial, add_apply, map_add, Finset.sum_add_distrib, Pi.add_apply]

Premises used: Matrix.add_apply, Finset.sum_add_distrib, Matrix.toMvPolynomial, map_add, Pi.add_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
m : Type u_1
n : Type u_2
o : Type u_3
R : Type u_4
inst : Fintype n
inst_1 : Fintype o
inst_2 : CommSemiring R
M : Matrix m n R
N : Matrix n o R
i : m
⊢ Eq (α := MvPolynomial o R) ((M * N).toMvPolynomial i)
    ((bind₁ N.toMvPolynomial : (a : MvPolynomial n R) → MvPolynomial o R) (M.toMvPolynomial i))

Tactic:
simp only [toMvPolynomial, mul_apply, map_sum, Finset.sum_comm (γ := o), bind₁, aeval,
    AlgHom.coe_mk, coe_eval₂Hom, eval₂_monomial, algebraMap_apply, Algebra.algebraMap_self,
    RingHom.id_apply, C_apply, pow_zero, Finsupp.prod_single_index, pow_one, Finset.mul_sum,
    monomial_mul, zero_add]

Premises used: Finset.mul_sum, AlgHom.coe_mk, RingHom.id_apply, MvPolynomial.aeval, Algebra.algebraMap_self, MvPolynomial.C_apply, Matrix.mul_apply, Matrix.toMvPolynomial, MvPolynomial.algebraMap_apply, map_sum, MvPolynomial.coe_eval₂Hom, zero_add, pow_zero, MvPolynomial.bind₁, MvPolynomial.monomial_mul, pow_one, MvPolynomial.eval₂_monomial, Finset.sum_comm, Finsupp.prod_single_index
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
c : ι₁ →₀ R
rw :
  Eq.{u_1 + 1} (α := R)
    ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R)
        (Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) i) :
      R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
rw₁ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
        (⇑c : (a : ι₁) → R) i :
      R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)
rw₂ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
      (⇑c : (a : ι₁) → R) i)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
      (⇑((b₁.repr : (a : M₁) → ι₁ →₀ R) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c) : ι₁ →₀ R) : (a : ι₁) → R) i)
rw₃ rw₄ :
  Eq.{u_1 + 1} (α := R)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
      (⇑c : (a : ι₁) → R) i)
    (Matrix.mulVec.{u_1, u_5, u_4} (n := ι₁) ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)
      (⇑c : (a : ι₁) → R) i)
⊢ Eq.{u_1 + 1} (α := R) ((eval (⇑c : (a : ι₁) → R) : (a : MvPolynomial ι₁ R) → R) (toMvPolynomial b₁ b₂ f i) : R)
    ((((b₂.repr : (a : M₂) → ι₂ →₀ R) ((f : (a : M₁) → M₂) ((b₁.repr.symm : (a : ι₁ →₀ R) → M₁) c : M₁)) : ι₂ →₀ R) :
          (a : ι₂) → R)
        i :
      R)

Tactic:
rw [toMvPolynomial, Matrix.toMvPolynomial_eval_eq_apply,
    ← LinearMap.toMatrix_mulVec_repr b₁ b₂, LinearEquiv.apply_symm_apply]

Premises used: LinearMap.toMvPolynomial, LinearMap.toMatrix_mulVec_repr, Matrix.toMvPolynomial_eval_eq_apply, LinearEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
A : Type u_6
inst_8 : CommRing A
inst_9 : Algebra R A
⊢ Eq (α := MvPolynomial ι₁ A)
    (toMvPolynomial (M₁ := TensorProduct R A M₁) (M₂ := TensorProduct R A M₂) (basis A b₁) (basis A b₂) (baseChange A f)
      i)
    ((MvPolynomial.map (algebraMap R A) : (a : MvPolynomial ι₁ R) → MvPolynomial ι₁ A) (toMvPolynomial b₁ b₂ f i))

Tactic:
simp only [toMvPolynomial, toMatrix_baseChange, Matrix.toMvPolynomial_map]

Premises used: LinearMap.toMatrix_baseChange, Matrix.toMvPolynomial_map, LinearMap.toMvPolynomial
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
⊢ (toMvPolynomial b₁ b₂ f i).IsHomogeneous 1

Tactic:
Matrix.toMvPolynomial_isHomogeneous _ _

Premises used: LinearMap.toMvPolynomial, Matrix.toMvPolynomial_isHomogeneous
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
⊢ (toMvPolynomial b₁ b₂ f i).totalDegree ≤ 1

Tactic:
Matrix.toMvPolynomial_totalDegree_le _ _

Premises used: Matrix.toMvPolynomial_totalDegree_le, LinearMap.toMvPolynomial
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f : M₁ →ₗ[R] M₂
i : ι₂
⊢ Eq.{u_1 + 1} (α := R) ((constantCoeff : (a : MvPolynomial ι₁ R) → R) (toMvPolynomial b₁ b₂ f i) : R) (0 : R)

Tactic:
Matrix.toMvPolynomial_constantCoeff _ _

Premises used: LinearMap.toMvPolynomial, Matrix.toMvPolynomial_constantCoeff
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
⊢ Eq (α := (i : ι₂) → MvPolynomial ι₁ R)
    (fun (i : ι₂) ↦ Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) 0) i) 0

Tactic:
simp only [map_zero, Matrix.toMvPolynomial_zero]

Premises used: map_zero, Matrix.toMvPolynomial_zero
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
ι₁ : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : Fintype ι₁
inst_4 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
⊢ Eq (α := (i : ι₁) → MvPolynomial ι₁ R)
    (fun (i : ι₁) ↦ Matrix.toMvPolynomial ((toMatrix b₁ b₁ : (a : M₁ →ₗ[R] M₁) → Matrix ι₁ ι₁ R) id) i) X

Tactic:
simp only [toMatrix_id, Matrix.toMvPolynomial_one]

Premises used: Matrix.toMvPolynomial_one, LinearMap.toMatrix_id
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f g : M₁ →ₗ[R] M₂
unfold :
  (fun (i : ι₂) ↦ Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) (f + g)) i) =
    HAdd.hAdd (α := (i : ι₂) → MvPolynomial ι₁ R)
      (fun (i : ι₂) ↦ Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) i) fun (i : ι₂) ↦
      Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) g) i
⊢ toMvPolynomial b₁ b₂ (f + g) = toMvPolynomial b₁ b₂ f + toMvPolynomial b₁ b₂ g

Tactic:
unfold toMvPolynomial

Premises used: LinearMap.toMvPolynomial
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
ι₁ : Type u_4
ι₂ : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : Module R M₁
inst_4 : Module R M₂
inst_5 : Fintype ι₁
inst_6 : Finite ι₂
inst_7 : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
f g : M₁ →ₗ[R] M₂
⊢ (fun (i : ι₂) ↦ Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) (f + g)) i) =
    HAdd.hAdd (α := (i : ι₂) → MvPolynomial ι₁ R)
      (fun (i : ι₂) ↦ Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f) i) fun (i : ι₂) ↦
      Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) g) i

Tactic:
simp only [map_add, Matrix.toMvPolynomial_add]

Premises used: Matrix.toMvPolynomial_add, map_add
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
ι₁ : Type u_5
ι₂ : Type u_6
ι₃ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Fintype ι₁
inst_8 : Fintype ι₂
inst_9 : Finite ι₃
inst_10 : DecidableEq ι₁
inst_11 : DecidableEq ι₂
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
b₃ : Basis ι₃ R M₃
g : M₂ →ₗ[R] M₃
f : M₁ →ₗ[R] M₂
i : ι₃
simp :
  Eq (α := MvPolynomial ι₁ R)
    ((bind₁ (Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)) :
          (a : MvPolynomial ι₂ R) → MvPolynomial ι₁ R)
        (Matrix.toMvPolynomial ((toMatrix b₂ b₃ : (a : M₂ →ₗ[R] M₃) → Matrix ι₃ ι₂ R) g) i) :
      MvPolynomial ι₁ R)
    ((bind₁ (toMvPolynomial b₁ b₂ f) : (a : MvPolynomial ι₂ R) → MvPolynomial ι₁ R)
        (Matrix.toMvPolynomial ((toMatrix b₂ b₃ : (a : M₂ →ₗ[R] M₃) → Matrix ι₃ ι₂ R) g) i) :
      MvPolynomial ι₁ R)
⊢ toMvPolynomial b₁ b₃ (g ∘ₗ f) i =
    (bind₁ (toMvPolynomial b₁ b₂ f) : (a : MvPolynomial ι₂ R) → MvPolynomial ι₁ R) (toMvPolynomial b₂ b₃ g i)

Tactic:
simp only [toMvPolynomial, toMatrix_comp b₁ b₂ b₃, Matrix.toMvPolynomial_mul]

Premises used: LinearMap.toMvPolynomial, LinearMap.toMatrix_comp, Matrix.toMvPolynomial_mul
-- Module: Mathlib.Algebra.Module.LinearMap.Polynomial
Goal:
R : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
ι₁ : Type u_5
ι₂ : Type u_6
ι₃ : Type u_7
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : AddCommGroup M₂
inst_3 : AddCommGroup M₃
inst_4 : Module R M₁
inst_5 : Module R M₂
inst_6 : Module R M₃
inst_7 : Fintype ι₁
inst_8 : Fintype ι₂
inst_9 : Finite ι₃
inst_10 : DecidableEq ι₁
inst_11 : DecidableEq ι₂
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
b₃ : Basis ι₃ R M₃
g : M₂ →ₗ[R] M₃
f : M₁ →ₗ[R] M₂
i : ι₃
⊢ Eq (α := MvPolynomial ι₁ R)
    ((bind₁ (Matrix.toMvPolynomial ((toMatrix b₁ b₂ : (a : M₁ →ₗ[R] M₂) → Matrix ι₂ ι₁ R) f)) :
          (a : MvPolynomial ι₂ R) → MvPolynomial ι₁ R)
        (Matrix.toMvPolynomial ((toMatrix b₂ b₃ : (a : M₂ →ₗ[R] M₃) → Matrix ι₃ ι₂ R) g) i) :
      MvPolynomial ι₁ R)
    ((bind₁ (toMvPolynomial b₁ b₂ f) : (a : MvPolynomial ι₂ R) → MvPolynomial ι₁ R)
        (Matrix.toMvPolynomial ((toMatrix b₂ b₃ : (a : M₂ →ₗ[R] M₃) → Matrix ι₃ ι₂ R) g) i) :
      MvPolynomial ι₁ R)

Tactic:
rfl