awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (hypothesis)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p)) ((b : (a : ι) → P) i : P)
have hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
Tactic: have hAi : ∑ j, A i j = 1 := by
    calc
      ∑ j, A i j = ∑ j, A i j * ∑ l, b.toMatrix p j l := by simp
      _ = ∑ j, ∑ l, A i j * b.toMatrix p j l := by simp_rw [Finset.mul_sum]
      _ = ∑ l, ∑ j, A i j * b.toMatrix p j l := by rw [Finset.sum_comm]
      _ = ∑ l, (A * b.toMatrix p) i l := rfl
      _ = 1 := by simp [hA, Matrix.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
⊢ Eq.{u₄ + 1} (α := P) ((b : (a : ι) → P) i : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)
have apply : ∀ (i_1 : ι),
  Eq.{u₂ + 1} (α := k) ((b.coord i_1 : (a : P) → k) ((b : (a : ι) → P) i : P) : k)
    ((b.coord i_1 : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P) : k)
Tactic: apply b.ext_elem
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
j : ι
⊢ Eq.{u₂ + 1} (α := k) ((b.coord j : (a : P) → k) ((b : (a : ι) → P) i : P) : k)
    ((b.coord j : (a : P) → k) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P) : k)
have rw : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0)
  (∑ i_1 : ι', HSMul.hSMul (β := k) (A i i_1) (((⇑(b.coord j) : (a : P) → k) ∘ p) i_1))
Tactic: rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
      Finset.univ.affineCombination_eq_linear_combination _ _ hAi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
j : ι
⊢ Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0)
    (∑ i_1 : ι', HSMul.hSMul (β := k) (A i i_1) (((⇑(b.coord j) : (a : P) → k) ∘ p) i_1))
have change : (if j = i then 1 else 0) = (A * b.toMatrix p) i j
Tactic: change _ = (A * b.toMatrix p) i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
j : ι
⊢ (if j = i then 1 else 0) = (A * b.toMatrix p) i j
have simp_rw : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (1 i j)
Tactic: simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
j : ι
simp_rw : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (1 i j)
⊢ (if j = i then 1 else 0) = (A * b.toMatrix p) i j
have simp_rw₁ : Eq.{u₂ + 1} (α := k) (if j = i then 1 else 0) (if i = j then 1 else 0)
Tactic: simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (hypothesis)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p)) ((b : (a : ι) → P) i : P)
have hbi : Eq.{u₄ + 1} (α := P) ((b : (a : ι) → P) i : P) ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)
Tactic: have hbi : b i = Finset.univ.affineCombination k p (A i) := by
    apply b.ext_elem
    intro j
    rw [b.coord_apply, Finset.univ.map_affineCombination _ _ hAi,
      Finset.univ.affineCombination_eq_linear_combination _ _ hAi]
    change _ = (A * b.toMatrix p) i j
    simp_rw [hA, Matrix.one_apply, @eq_comm _ i j]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
ι' : Type u_1
inst_4 : Finite ι
inst_5 : Fintype ι'
inst_6 : DecidableEq ι
inst_7 : Nontrivial k
p : ι' → P
A : Matrix ι ι' k
hA : A * b.toMatrix p = 1
val : Fintype ι
i : ι
hAi : Eq.{u₂ + 1} (α := k) (∑ j : ι', A i j) 1
hbi :
  Eq.{u₄ + 1} (α := P) ((b : (a : ι) → P) i : P)
    ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)
⊢ Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p)) ((b : (a : ι) → P) i : P)
have intro : Membership.mem (α := P) (γ := AffineSubspace k P) (affineSpan k (range p))
  ((Finset.affineCombination k Finset.univ p : (a : ι' → k) → P) (A i) : P)
Tactic: rw [hbi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
x : P
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) = (b.coords : (a : P) → ι → k) x
have h : ∀ (j : ι),
  vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
    (b.coords : (a : P) → ι → k) x j
Tactic: ext j
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
    (b.coords : (a : P) → ι → k) x j
have h : vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j = (b.coord j : (a : P) → k) x
Tactic: change _ = b.coord j x
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
| ((b.coord j : (a : P) → k) x : k)
have rw : ((b.coord j : (a : P) → k)
    ((Finset.affineCombination k Finset.univ (⇑b₂ : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b₂.coord i : (a : P) → k) x :
      P) :
  k)
Tactic: rw [← b₂.affineCombination_coord_eq_self x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j = (b.coord j : (a : P) → k) x
have h : vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
  (b.coord j : (a : P) → k)
    ((Finset.affineCombination k Finset.univ (⇑b₂ : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
        (b₂.coord i : (a : P) → k) x :
      P)
Tactic: conv_rhs => rw [← b₂.affineCombination_coord_eq_self x]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
x : P
j : ι
⊢ vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
    (b.coord j : (a : P) → k)
      ((Finset.affineCombination k Finset.univ (⇑b₂ : (a : ι) → P) : (a : ι → k) → P) fun (i : ι) ↦
          (b₂.coord i : (a : P) → k) x :
        P)
have h : vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) j =
  (Finset.affineCombination k Finset.univ
        (Function.comp.{u₁ + 1, u₄ + 1, u₂ + 1} (β := P) (⇑(b.coord j) : (a : P) → k) (⇑b₂ : (a : ι) → P)) :
      (a : ι → k) → k)
    fun (i : ι) ↦ (b₂.coord i : (a : P) → k) x
Tactic: rw [Finset.map_affineCombination _ _ _ (b₂.sum_coord_apply_eq_one x)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
⊢ HMul.hMul (α := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b₂.toMatrix (⇑b : (a : ι) → P)) = 1
have a : ∀ (l m : ι),
  HMul.hMul (α := Matrix ι ι k) (β := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b₂.toMatrix (⇑b : (a : ι) → P)) l
      m =
    1 l m
Tactic: ext l m
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
l m : ι
⊢ HMul.hMul (α := Matrix ι ι k) (β := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b₂.toMatrix (⇑b : (a : ι) → P)) l
      m =
    1 l m
have a : vecMul (m := ι) ((b.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P)) (b₂.toMatrix (⇑b : (a : ι) → P)) m = 1 l m
Tactic: change (b.coords (b₂ l) ᵥ* b₂.toMatrix b) m = _
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
l m : ι
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P)) (b₂.toMatrix (⇑b : (a : ι) → P)) m = 1 l m
have a : Eq.{u₂ + 1} (α := k) ((b₂.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P) m : k) (1 l m : k)
Tactic: rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
l m : ι
a : Eq.{u₂ + 1} (α := k) ((b₂.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P) m : k) (1 l m : k)
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P)) (b₂.toMatrix (⇑b : (a : ι) → P)) m = 1 l m
have a₁ : Eq.{u₂ + 1} (α := k) ((b₂.coord m : (a : P) → k) ((b₂ : (a : ι) → P) l : P) : k) (1 l m : k)
Tactic: rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
l m : ι
a : Eq.{u₂ + 1} (α := k) ((b₂.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P) m : k) (1 l m : k)
a₁ : Eq.{u₂ + 1} (α := k) ((b₂.coord m : (a : P) → k) ((b₂ : (a : ι) → P) l : P) : k) (1 l m : k)
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P)) (b₂.toMatrix (⇑b : (a : ι) → P)) m = 1 l m
have a₂ : b₂.toMatrix (⇑b₂ : (a : ι) → P) l m = 1 l m
Tactic: rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
b₂ : AffineBasis ι k P
inst_5 : DecidableEq ι
l m : ι
a : Eq.{u₂ + 1} (α := k) ((b₂.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P) m : k) (1 l m : k)
a₁ : Eq.{u₂ + 1} (α := k) ((b₂.coord m : (a : P) → k) ((b₂ : (a : ι) → P) l : P) : k) (1 l m : k)
a₂ : b₂.toMatrix (⇑b₂ : (a : ι) → P) l m = 1 l m
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) ((b₂ : (a : ι) → P) l : P)) (b₂.toMatrix (⇑b : (a : ι) → P)) m = 1 l m
have a₃ : Eq.{u₂ + 1} (α := k) (1 l m) (1 l m)
Tactic: rw [toMatrix_vecMul_coords, coords_apply, ← toMatrix_apply, toMatrix_self]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
⊢ IsUnit (b.toMatrix p) ↔ AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
have mp : IsUnit (b.toMatrix p) → AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
mp : IsUnit (b.toMatrix p) → AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
⊢ IsUnit (b.toMatrix p) ↔ AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
have mpr : AffineIndependent k p ∧ Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤ → IsUnit (b.toMatrix p)
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : Ring k
inst_3 : Module k V
b : AffineBasis ι k P
inst_4 : Fintype ι
inst_5 : DecidableEq ι
inst_6 : Nontrivial k
p : ι → P
h_tot : AffineIndependent k p
h_ind : Eq (α := AffineSubspace k P) (affineSpan k (range p)) ⊤
b' : AffineBasis ι k P := { toFun := p, ind' := h_tot, tot' := h_ind }
⊢ IsUnit (b.toMatrix p)
have mpr : IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b' : (a : ι) → P))
Tactic: change IsUnit (b.toMatrix b')
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (hypothesis)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ = (b₂.coords : (a : P) → ι → k) x
have hu : IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P))
Tactic: have hu := b.isUnit_toMatrix b₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (hypothesis)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P))
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ = (b₂.coords : (a : P) → ι → k) x
have hu₁ : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
Tactic: rw [Matrix.isUnit_iff_isUnit_det] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ = (b₂.coords : (a : P) → ι → k) x
have rw : vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) ᵥ*
    (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
  (b₂.coords : (a : P) → ι → k) x
Tactic: rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
    Matrix.vecMul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
rw :
  vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) ᵥ*
      (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (b₂.coords : (a : P) → ι → k) x
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ = (b₂.coords : (a : P) → ι → k) x
have rw₁ : (b₂.coords : (a : P) → ι → k) x ᵥ*
    HMul.hMul (α := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
  (b₂.coords : (a : P) → ι → k) x
Tactic: rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
    Matrix.vecMul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
rw :
  vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) ᵥ*
      (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (b₂.coords : (a : P) → ι → k) x
rw₁ :
  (b₂.coords : (a : P) → ι → k) x ᵥ*
      HMul.hMul (α := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (b₂.coords : (a : P) → ι → k) x
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ = (b₂.coords : (a : P) → ι → k) x
have rw₂ : Eq (α := ι → k) (vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) 1) ((b₂.coords : (a : P) → ι → k) x)
Tactic: rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
    Matrix.vecMul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
rw :
  vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P)) ᵥ*
      (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (b₂.coords : (a : P) → ι → k) x
rw₁ :
  (b₂.coords : (a : P) → ι → k) x ᵥ*
      HMul.hMul (α := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P)) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (b₂.coords : (a : P) → ι → k) x
rw₂ : Eq (α := ι → k) (vecMul (m := ι) ((b₂.coords : (a : P) → ι → k) x) 1) ((b₂.coords : (a : P) → ι → k) x)
⊢ vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ = (b₂.coords : (a : P) → ι → k) x
have rw₃ : Eq (α := ι → k) ((b₂.coords : (a : P) → ι → k) x : ι → k) ((b₂.coords : (a : P) → ι → k) x : ι → k)
Tactic: rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu,
    Matrix.vecMul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (hypothesis)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
⊢ HSMul.hSMul (β := ι → k) (det (b.toMatrix (⇑b₂ : (a : ι) → P))) ((b₂.coords : (a : P) → ι → k) x : ι → k) =
    (cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k)
have hu : IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P))
Tactic: have hu := b.isUnit_toMatrix b₂
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (hypothesis)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (M := Matrix ι ι k) (b.toMatrix (⇑b₂ : (a : ι) → P))
⊢ HSMul.hSMul (β := ι → k) (det (b.toMatrix (⇑b₂ : (a : ι) → P))) ((b₂.coords : (a : P) → ι → k) x : ι → k) =
    (cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k)
have hu₁ : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
Tactic: rw [Matrix.isUnit_iff_isUnit_det] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
⊢ HSMul.hSMul (β := ι → k) (det (b.toMatrix (⇑b₂ : (a : ι) → P))) ((b₂.coords : (a : P) → ι → k) x : ι → k) =
    (cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k)
have rw : det (b.toMatrix (⇑b₂ : (a : ι) → P)) •
    vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
  (cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k)
Tactic: rw [← b.toMatrix_inv_vecMul_toMatrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose _ _ hu]
-- Lean 4 proof step from Mathlib.LinearAlgebra.AffineSpace.Matrix (goal)
Goal:
ι : Type u₁
k : Type u₂
V : Type u₃
P : Type u₄
inst : AddCommGroup V
inst_1 : AffineSpace V P
inst_2 : CommRing k
inst_3 : Module k V
inst_4 : DecidableEq ι
inst_5 : Fintype ι
b b₂ : AffineBasis ι k P
x : P
hu : IsUnit (det (b.toMatrix (⇑b₂ : (a : ι) → P)))
rw :
  det (b.toMatrix (⇑b₂ : (a : ι) → P)) •
      vecMul (m := ι) ((b.coords : (a : P) → ι → k) x) (b.toMatrix (⇑b₂ : (a : ι) → P))⁻¹ =
    (cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k)
⊢ HSMul.hSMul (β := ι → k) (det (b.toMatrix (⇑b₂ : (a : ι) → P))) ((b₂.coords : (a : P) → ι → k) x : ι → k) =
    (cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k)
have rw₁ : Eq (α := ι → k)
  ((cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k) : ι → k)
  ((cramer (b.toMatrix (⇑b₂ : (a : ι) → P))ᵀ : (a : ι → k) → ι → k) ((b.coords : (a : P) → ι → k) x : ι → k) : ι → k)
Tactic: rw [← b.toMatrix_inv_vecMul_toMatrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose _ _ hu]