awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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 : Field K := inferInstance
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have a : 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: apply FaithfulSMul.algebraMap_injective R K
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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 : Field K := inferInstance
⊢ 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)
have 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)
Tactic: have := det_ofField (f.baseChange K) (1 ⊗ₜ[R] v)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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)
⊢ 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)
have 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)
Tactic: rw [← transvection.baseChange, det_baseChange,
    ← algebraMap.coe_one (R := R) (A := K)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have 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)
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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)
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have 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)
Tactic: rcases subsingleton_or_nontrivial R with hR | hR
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have 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)
Tactic: set n := finrank R V
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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)
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have this : IsDomain S
Tactic: have : IsDomain S := inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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 γ
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have x : IsScalarTower S R V
Tactic: have _ : IsScalarTower S R V := IsScalarTower.of_compHom S R V
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have ibc : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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)
have rw : HSMul.hSMul (α := S) (β := V) 1 ((b : (a : Fin n) → V) i : V) = (b : (a : Fin n) → V) i
Tactic: rw [Fintype.linearCombination_apply_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ 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)
have rw₁ : Eq.{u_4 + 1} (α := V) ((b : (a : Fin n) → V) i : V) ((b : (a : Fin n) → V) i : V)
Tactic: rw [Fintype.linearCombination_apply_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have 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)
Tactic: have hε (i) : ε (Pi.single i 1) = b i := by
    rw [Fintype.linearCombination_apply_single, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
have 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)
Tactic: apply b.ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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.{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)
have rw : Eq (α := R) ((γ : (a : S) → R) (MvPolynomial.X (Sum.inl i)) : 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ε]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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)
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have hf : (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ (ε : (a : Fin n → S) → V) vM = v
have rw : Eq (α := Fin n → R) ((⇑(algebraMap S R) : (a : S) → R) ∘ vM) ((b.equivFun : (a : V) → Fin n → R) v)
Tactic: rw [of_fintype_basis_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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
⊢ Eq (α := Fin n → R) ((⇑(algebraMap S R) : (a : S) → R) ∘ vM) ((b.equivFun : (a : V) → Fin n → R) v)
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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) (((⇑(algebraMap S R) : (a : S) → R) ∘ vM) i : R) ((b.equivFun : (a : V) → Fin n → R) v i : R)
have h : Eq (α := R) (((⇑γ : (a : S) → R) ∘ vM) i : R) ((b.equivFun : (a : V) → Fin n → R) v i : R)
Tactic: rw [RingHom.algebraMap_toAlgebra]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
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) (((⇑γ : (a : S) → R) ∘ vM) i : R) ((b.equivFun : (a : V) → Fin n → R) v i : R)
have 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)
Tactic: simp only [vM, γ, Function.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
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
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have hv : (ε : (a : Fin n → S) → V) vM = v
Tactic: have hv : ε vM = v := by
    rw [of_fintype_basis_eq]
    ext i
    rw [RingHom.algebraMap_toAlgebra]
    simp only [vM, γ, Function.comp_apply]
    apply MvPolynomial.aeval_X