awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : IsDomain R
f : Dual R V
v : V
K : Type u_3 := FractionRing R
this_1 : Field K := inferInstance
this :
  (LinearMap.det : (a : K ⊗[R] V →ₗ[K] K ⊗[R] V) → K)
      (transvection ((Dual.baseChange K : (a : Dual R V) → Dual K (K ⊗[R] V)) f) (1 ⊗ₜ[R] v)) =
    HAdd.hAdd (α := K) (β := K) (1 : K)
      ((((Dual.baseChange K : (a : Dual R V) → Dual K (K ⊗[R] V)) f : Dual K (K ⊗[R] V)) : (a : K ⊗[R] V) → K)
          (1 ⊗ₜ[R] v) :
        K)
⊢ (algebraMap R K : (a : R) → K) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v)) =
    HAdd.hAdd (α := K) (β := K) ((↑1 : K) : K)
      ((((Dual.baseChange K : (a : Dual R V) → Dual K (K ⊗[R] V)) f : Dual K (K ⊗[R] V)) : (a : K ⊗[R] V) → K)
          ((↑1 : K) ⊗ₜ[R] v) :
        K)

Tactic:
rw [← transvection.baseChange, det_baseChange,
    ← algebraMap.coe_one (R := R) (A := K)] at this

Premises used: algebraMap.coe_one, LinearMap.det_baseChange, LinearMap.transvection.baseChange
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
inst_5 : IsDomain R
f : Dual R V
v : V
K : Type u_3 := FractionRing R
this_1 : Field K := inferInstance
this :
  (algebraMap R K : (a : R) → K) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v)) =
    HAdd.hAdd (α := K) (β := K) ((↑1 : K) : K)
      ((((Dual.baseChange K : (a : Dual R V) → Dual K (K ⊗[R] V)) f : Dual K (K ⊗[R] V)) : (a : K ⊗[R] V) → K)
          ((↑1 : K) ⊗ₜ[R] v) :
        K)
⊢ Eq (α := K) ((algebraMap R K : (a : R) → K) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v)) : K)
    ((algebraMap R K : (a : R) → K) (HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)) : K)

Tactic:
simpa [Algebra.algebraMap_eq_smul_one, add_smul] using this

Premises used: Algebra.algebraMap_eq_smul_one, add_smul
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
inl :
  ∀ (hR : Subsingleton R),
    (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
      HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
inr :
  ∀ (hR : Nontrivial R),
    (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
      HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)

Tactic:
rcases subsingleton_or_nontrivial R with hR | hR

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Subsingleton R
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)

Tactic:
subsingleton
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
b : Basis (Fin (finrank R V)) R V := finBasis R V
inr :
  let n := finrank R V;
  ∀ (b : Basis (Fin n) R V),
    (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
      HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)

Tactic:
set n := finrank R V

Premises used: Module.finrank
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
⊢ IsDomain S

Tactic:
have : IsDomain S := inferInstance
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
⊢ IsScalarTower S R V

Tactic:
have _ : IsScalarTower S R V := IsScalarTower.of_compHom S R V
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
⊢ IsBaseChange.{0, u_4, u_3, 0} (M := Fin n → S) (N := V) R (Fintype.linearCombination S (⇑b : (a : Fin n) → V))

Tactic:
have ibc := IsBaseChange.of_fintype_basis S b
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ibc : IsBaseChange.{0, u_4, u_3, 0} (M := Fin n → S) (N := V) R (Fintype.linearCombination S (⇑b : (a : Fin n) → V))
⊢ let ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i;
  IsBaseChange R ε

Tactic:
set ε := Fintype.linearCombination S (fun i ↦ b i)

Premises used: Fintype.linearCombination, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
i : Fin n
rw : HSMul.hSMul (α := S) (β := V) 1 ((b : (a : Fin n) → V) i : V) = (b : (a : Fin n) → V) i
rw₁ rw₂ : Eq.{u_4 + 1} (α := V) ((b : (a : Fin n) → V) i : V) ((b : (a : Fin n) → V) i : V)
⊢ Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)

Tactic:
rw [Fintype.linearCombination_apply_single, one_smul]

Premises used: one_smul, Fintype.linearCombination_apply_single
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
⊢ ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)

Tactic:
have hε (i) : ε (Pi.single i 1) = b i := by
    rw [Fintype.linearCombination_apply_single, one_smul]
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
apply :
  ∀ (i : Fin n),
    Eq.{u_3 + 1} (α := R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((b : (a : Fin n) → V) i : V) :
        R)
      ((f : (a : V) → R) ((b : (a : Fin n) → V) i : V) : R)
⊢ (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f

Tactic:
apply b.ext

Premises used: Module.Basis.ext
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
i : Fin n
rw :
  Eq (α := R) ((γ : (a : S) → R) (MvPolynomial.X (Sum.inl i)) : R) ((f : (a : V) → R) ((b : (a : Fin n) → V) i : V) : R)
⊢ Eq.{u_3 + 1} (α := R)
    ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R) ((b : (a : Fin n) → V) i : V) :
      R)
    ((f : (a : V) → R) ((b : (a : Fin n) → V) i : V) : R)

Tactic:
rw [← hε, toDual_comp_apply, Fintype.linearCombination_apply_single,
      one_smul, RingHom.algebraMap_toAlgebra, hε]

Premises used: one_smul, IsBaseChange.toDual_comp_apply, RingHom.algebraMap_toAlgebra, Fintype.linearCombination_apply_single
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
i : Fin n
⊢ Eq (α := R) ((γ : (a : S) → R) (MvPolynomial.X (Sum.inl i)) : R) ((f : (a : V) → R) ((b : (a : Fin n) → V) i : V) : R)

Tactic:
apply MvPolynomial.aeval_X

Premises used: MvPolynomial.aeval_X
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
⊢ (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f

Tactic:
have hf : ibc.toDual fM = f := by
    apply b.ext
    intro i
    rw [← hε, toDual_comp_apply, Fintype.linearCombination_apply_single,
      one_smul, RingHom.algebraMap_toAlgebra, hε]
    apply MvPolynomial.aeval_X
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
rw : Eq (α := Fin n → R) ((⇑(algebraMap S R) : (a : S) → R) ∘ vM) ((b.equivFun : (a : V) → Fin n → R) v)
⊢ (ε : (a : Fin n → S) → V) vM = v

Tactic:
rw [of_fintype_basis_eq]

Premises used: IsBaseChange.of_fintype_basis_eq
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h_1 : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
h :
  ∀ (i : Fin n),
    Eq (α := R) (((⇑(algebraMap S R) : (a : S) → R) ∘ vM) i : R) ((b.equivFun : (a : V) → Fin n → R) v i : R)
⊢ Eq (α := Fin n → R) ((⇑(algebraMap S R) : (a : S) → R) ∘ vM) ((b.equivFun : (a : V) → Fin n → R) v)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h_1 : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
i : Fin n
h : Eq (α := R) (((⇑γ : (a : S) → R) ∘ vM) i : R) ((b.equivFun : (a : V) → Fin n → R) v i : R)
⊢ Eq (α := R) (((⇑(algebraMap S R) : (a : S) → R) ∘ vM) i : R) ((b.equivFun : (a : V) → Fin n → R) v i : R)

Tactic:
rw [RingHom.algebraMap_toAlgebra]

Premises used: RingHom.algebraMap_toAlgebra
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h_1 : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
i : Fin n
h :
  Eq (α := R)
    (((↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
                  (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
                    (b.coord i : (a : V) → R) v) :
                MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
            S →+* R) :
          (a : S) → R)
        (MvPolynomial.X (Sum.inr i)) :
      R)
    ((b.equivFun : (a : V) → Fin n → R) v i : R)
⊢ Eq (α := R) (((⇑γ : (a : S) → R) ∘ vM) i : R) ((b.equivFun : (a : V) → Fin n → R) v i : R)

Tactic:
simp only [vM, γ, Function.comp_apply]

Premises used: Function.comp_apply
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
i : Fin n
⊢ Eq (α := R)
    (((↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
                  (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
                    (b.coord i : (a : V) → R) v) :
                MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
            S →+* R) :
          (a : S) → R)
        (MvPolynomial.X (Sum.inr i)) :
      R)
    ((b.equivFun : (a : V) → Fin n → R) v i : R)

Tactic:
apply MvPolynomial.aeval_X

Premises used: MvPolynomial.aeval_X