awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
i' : ι
h : single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
⊢ Eq.{u_3 + 1} (α := M) (∑ j_1 : ι, single i j r i' j_1 • v j_1 : M)
    (Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i' : M)
have rw : ∀ (j' : ι) (hj : j' ≠ j), single i j r i' j' • v j' = 0
Tactic: rw [Fintype.sum_eq_single j fun j' hj => ?_]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
i' : ι
⊢ single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
have h : single i j r i j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i
Tactic: obtain rfl | hi := eq_or_ne i i'
Cleared hypotheses: i'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
i j : ι
r : R
v : ι → M
i' : ι
h : single i j r i j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i
⊢ single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
have h₁ : ∀ (hi : i ≠ i'), single i j r i' j • v j = Pi.single (M := fun (j : ι) ↦ M) i (r • v j) i'
Tactic: obtain rfl | hi := eq_or_ne i i'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
r : R
v : ι → M
⊢ HSMul.hSMul (α := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) v = r • v
have h : ∀ (i : ι), HSMul.hSMul (α := Matrix ι ι R) (diagonal fun (x : ι) ↦ r) v i = (r • v) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
S : Type u_6
inst_9 : Ring S
inst_10 : SMul R S
inst_11 : Module S M
inst_12 : IsScalarTower R S M
x : R
x_1 : Matrix ι ι S
x_2 : ι → M
⊢ (x • x_1) • x_2 = x • x_1 • x_2
have h : ∀ (x_3 : ι), ((x • x_1) • x_2) x_3 = (x • x_1 • x_2) x_3
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
f : M →ₗ[R] N
x : Matrix ι ι R
x_1 : ι → M
⊢ (f.compLeft ι : (a : ι → M) → ι → N) (x • x_1) =
    HSMul.hSMul (α := Matrix ι ι R) (β := ι → N)
      ((RingHom.id (Matrix ι ι R) : (a : Matrix ι ι R) → Matrix ι ι R) x : Matrix ι ι R)
      ((f.compLeft ι : (a : ι → M) → ι → N) x_1 : ι → N)
have h : ∀ (x_2 : ι),
  (f.compLeft ι : (a : ι → M) → ι → N) (x • x_1) x_2 =
    HSMul.hSMul (α := Matrix ι ι R) (β := ι → N)
      ((RingHom.id (Matrix ι ι R) : (a : Matrix ι ι R) → Matrix ι ι R) x : Matrix ι ι R)
      ((f.compLeft ι : (a : ι → M) → ι → N) x_1 : ι → N) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
⊢ Eq (α := LinearMap (R := Matrix ι ι R) (RingHom.id (Matrix ι ι R)) (ι → M) (ι → M)) (mapMatrixModule ι id) id
have h : ∀ (x : ι → M) (x_1 : ι),
  Eq.{u_3 + 1} (α := M) ((mapMatrixModule ι id : (a : ι → M) → ι → M) x x_1 : M) ((id : (a : ι → M) → ι → M) x x_1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Module (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
P : Type u_5
inst : Ring R
inst_1 : Fintype ι
inst_2 : DecidableEq ι
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : AddCommGroup N
inst_6 : Module R N
inst_7 : AddCommGroup P
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ mapMatrixModule ι (g ∘ₗ f) = mapMatrixModule ι g ∘ₗ mapMatrixModule ι f
have h : ∀ (x : ι → M) (x_1 : ι),
  Eq.{u_5 + 1} (α := P) ((mapMatrixModule ι (g ∘ₗ f) : (a : ι → M) → ι → P) x x_1 : P)
    ((mapMatrixModule ι g ∘ₗ mapMatrixModule ι f : (a : ι → M) → ι → P) x x_1 : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.MvPolynomial (hypothesis)
Goal:
m : Type u_1
R : Type u_3
inst : DecidableEq m
inst_1 : Fintype m
inst_2 : CommRing R
inst_3 : Nontrivial R
h_det : Eq (α := MvPolynomial.{u_1, u_3} (m × m) R) (det (mvPolynomialX m m R)) 0
⊢ False
have this : Eq.{u_3 + 1} (α := R)
  (det.{u_3, u_1} (n := m)
    ((RingHom.mapMatrix (MvPolynomial.eval fun (p : m × m) ↦ 1 p.1 p.2) :
        (a : Matrix m m (MvPolynomial (m × m) R)) → Matrix m m R)
      (mvPolynomialX m m R)))
  (det.{u_3, u_1} (n := m) 1)
Tactic: have := congr_arg Matrix.det (mvPolynomialX_mapMatrix_eval (1 : Matrix m m R))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.MvPolynomial (hypothesis)
Goal:
m : Type u_1
R : Type u_3
inst : DecidableEq m
inst_1 : Fintype m
inst_2 : CommRing R
inst_3 : Nontrivial R
h_det : Eq (α := MvPolynomial.{u_1, u_3} (m × m) R) (det (mvPolynomialX m m R)) 0
this :
  Eq.{u_3 + 1} (α := R)
    (det.{u_3, u_1} (n := m)
      ((RingHom.mapMatrix (MvPolynomial.eval fun (p : m × m) ↦ 1 p.1 p.2) :
          (a : Matrix m m (MvPolynomial (m × m) R)) → Matrix m m R)
        (mvPolynomialX m m R)))
    (det.{u_3, u_1} (n := m) 1)
⊢ False
have this₁ : Eq.{u_3 + 1} (α := R) 0 1
Tactic: rw [det_one, ← RingHom.map_det, h_det, map_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ M.SeparatingRight ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
have refine_1 : ∀ (w : n → R) (hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) (hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) (v : m → R),
  v ⬝ᵥ M *ᵥ w = 0
Tactic: refine forall_congr' fun w ↦ ⟨fun hM hw ↦ hM ?_, fun hM hw ↦ hM ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
refine_1 :
  ∀ (w : n → R) (hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) (hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) (v : m → R),
    v ⬝ᵥ M *ᵥ w = 0
⊢ M.SeparatingRight ↔ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
have refine_2 : ∀ (w : n → R) (hM : (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) (hw : ∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) (v : m → R),
  v ⬝ᵥ M *ᵥ w = 0
Tactic: refine forall_congr' fun w ↦ ⟨fun hM hw ↦ hM ?_, fun hM hw ↦ hM ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ M.SeparatingLeft ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
have refine_1 : ∀ (v : m → R) (hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) (hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) (w : n → R),
  v ⬝ᵥ M *ᵥ w = 0
Tactic: refine forall_congr' fun v ↦ ⟨fun hM hv ↦ hM ?_, fun hM hv ↦ hM ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
refine_1 :
  ∀ (v : m → R) (hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) (hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) (w : n → R),
    v ⬝ᵥ M *ᵥ w = 0
⊢ M.SeparatingLeft ↔ ∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0
have refine_2 : ∀ (v : m → R) (hM : (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) (hv : ∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) (w : n → R),
  v ⬝ᵥ M *ᵥ w = 0
Tactic: refine forall_congr' fun v ↦ ⟨fun hM hv ↦ hM ?_, fun hM hv ↦ hM ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
⊢ M.Nondegenerate ↔
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
have mp : M.Nondegenerate →
  (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : CommRing R
inst_1 : Fintype m
inst_2 : Fintype n
M : Matrix m n R
mp :
  M.Nondegenerate →
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
⊢ M.Nondegenerate ↔
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0
have mpr : ((∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M *ᵥ w = 0) → w = 0) →
  M.Nondegenerate
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
⊢ M.Nondegenerate
have refine_1 : ∀ (v : m → A) (h : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0), v = 0
Tactic: refine nondegenerate_def.mpr ⟨fun v h ↦ ?_, fun w h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
refine_1 : ∀ (v : m → A) (h : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0), v = 0
⊢ M.Nondegenerate
have refine_2 : ∀ (w : m → A) (h : ∀ (v : m → A), v ⬝ᵥ M *ᵥ w = 0), w = 0
Tactic: refine nondegenerate_def.mpr ⟨fun v h ↦ ?_, fun w h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
h : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0
⊢ v = 0
have refine_1 : ∀ (i : m), v i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (hypothesis)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
h : ∀ (w : m → A), v ⬝ᵥ M *ᵥ w = 0
i : m
⊢ v i = 0 i
have h₁ : v ⬝ᵥ M *ᵥ (M.cramer : (a : m → A) → m → A) (Pi.single (M := fun (a : m) ↦ A) i 1) = 0
Tactic: specialize h (M.cramer (Pi.single i 1))
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
h : ∀ (v : m → A), v ⬝ᵥ M *ᵥ w = 0
⊢ w = 0
have refine_2 : ∀ (i : m), w i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
h : ∀ (v : m → A), v ⬝ᵥ M *ᵥ w = 0
i : m
⊢ w i = 0 i
have refine_2 : ∀ (h : w i ≠ 0 i), ∃ (v : m → A), v ⬝ᵥ M *ᵥ w ≠ 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
i : m
h : w i ≠ 0 i
⊢ ∃ (v : m → A), v ⬝ᵥ M *ᵥ w ≠ 0
have h₁ : Pi.single (M := fun (a : m) ↦ A) i 1 ᵥ* M.adjugate ⬝ᵥ M *ᵥ w ≠ 0
Tactic: use Pi.single i 1 ᵥ* M.adjugate
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
w : m → A
i : m
h : w i ≠ 0 i
⊢ Pi.single (M := fun (a : m) ↦ A) i 1 ᵥ* M.adjugate ⬝ᵥ M *ᵥ w ≠ 0
have h₁ : Pi.single (M := fun (a : m) ↦ A) i 1 ᵥ* HSMul.hSMul (β := Matrix m m A) M.det 1 ⬝ᵥ w ≠ 0
Tactic: rw [dotProduct_mulVec, vecMul_vecMul, adjugate_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : v ᵥ* M = 0
w : m → A
⊢ v ⬝ᵥ M *ᵥ w = 0
have rw : v ᵥ* M ⬝ᵥ w = 0
Tactic: rw [dotProduct_mulVec, hv, zero_dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : v ᵥ* M = 0
w : m → A
rw : v ᵥ* M ⬝ᵥ w = 0
⊢ v ⬝ᵥ M *ᵥ w = 0
have rw₁ : 0 ⬝ᵥ w = 0
Tactic: rw [dotProduct_mulVec, hv, zero_dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
m : Type u_1
A : Type u_4
inst : Fintype m
inst_1 : CommRing A
inst_2 : IsDomain A
inst_3 : DecidableEq m
M : Matrix m m A
hM : M.det ≠ 0
v : m → A
hv : v ᵥ* M = 0
w : m → A
rw : v ᵥ* M ⬝ᵥ w = 0
rw₁ : 0 ⬝ᵥ w = 0
⊢ v ⬝ᵥ M *ᵥ w = 0
have rw₂ : Eq.{u_4 + 1} (α := A) 0 0
Tactic: rw [dotProduct_mulVec, hv, zero_dotProduct]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : LinearIndependent R v
A : Matrix κ ι R
hA : A.Nondegenerate
⊢ LinearIndependent.{u_2, u_3, u_4} R (M := M) fun (i : κ) ↦ ∑ j : ι, A i j • v j
have have : ∀ (this : Fintype κ), LinearIndependent.{u_2, u_3, u_4} R (M := M) fun (i : κ) ↦ ∑ j : ι, A i j • v j
Tactic: have : Fintype κ := Fintype.ofFinite _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : LinearIndependent R v
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
⊢ LinearIndependent.{u_2, u_3, u_4} R (M := M) fun (i : κ) ↦ ∑ j : ι, A i j • v j
have rw : ∀ (hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0) {A : Matrix κ ι R}
  (hA : A.Nondegenerate) (this : Fintype κ) (g : κ → R),
  Eq.{u_4 + 1} (α := M) (∑ i : κ, HSMul.hSMul (β := M) (g i) (∑ j : ι, A i j • v j)) 0 → ∀ (i : κ), g i = 0
Tactic: rw [Fintype.linearIndependent_iff] at hv ⊢
Cleared hypotheses: hv, A, hA, this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (goal)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ i : κ, HSMul.hSMul (β := M) (w i) (∑ j : ι, A i j • v j)) 0
⊢ ∀ (i : κ), w i = 0
have suffices : w = 0
Tactic: suffices w = 0 by aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ i : κ, HSMul.hSMul (β := M) (w i) (∑ j : ι, A i j • v j)) 0
⊢ w = 0
have hw₁ : Eq.{u_4 + 1} (α := M) (∑ x : κ, ∑ x_1 : ι, (w x • A x x_1) • v x_1) 0
Tactic: simp_rw [Finset.smul_sum, ← smul_assoc] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : κ, ∑ x_1 : ι, (w x • A x x_1) • v x_1) 0
⊢ w = 0
have hw₁ : Eq.{u_4 + 1} (α := M) (∑ y : ι, ∑ x : κ, (w x • A x y) • v y) 0
Tactic: rw [Finset.sum_comm] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ y : ι, ∑ x : κ, (w x • A x y) • v y) 0
⊢ w = 0
have hw₁ : Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0
Tactic: simp_rw [← Finset.sum_smul] at hw
Cleared hypotheses: hw
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
hv : ∀ (g : ι → R), Eq.{u_4 + 1} (α := M) (∑ i : ι, g i • v i) 0 → ∀ (i : ι), g i = 0
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0
⊢ w = 0
have hv₁ : w ᵥ* A = 0
Tactic: replace hv : w ᵥ* A = 0 := funext <| hv _ hw
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
κ : Type u_2
R : Type u_3
M : Type u_4
inst : Fintype ι
inst_1 : Finite κ
inst_2 : CommRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
v : ι → M
A : Matrix κ ι R
hA : A.Nondegenerate
this : Fintype κ
w : κ → R
hw : Eq.{u_4 + 1} (α := M) (∑ x : ι, HSMul.hSMul.{u_3, u_4, u_4} (α := R) (∑ i : κ, w i • A i x) (v x)) 0
hv : w ᵥ* A = 0
⊢ w = 0
have hv₁ : ∀ (w' : ι → R), w ⬝ᵥ A *ᵥ w' = 0
Tactic: replace hv (w' : ι → R) : w ⬝ᵥ A *ᵥ w' = 0 := by
    simpa [Matrix.dotProduct_mulVec] using congr_arg (fun x ↦ dotProduct x w') hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
inst_3 : Invertible A.det
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate * A = 1
have rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A.adjugate * A) = 1
Tactic: rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
inst_3 : Invertible A.det
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A.adjugate * A) = 1
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate * A = 1
have rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
Tactic: rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
inst_3 : Invertible A.det
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A.adjugate * A) = 1
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate * A = 1
have rw₂ : HSMul.hSMul (β := Matrix n n α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ * A.det) 1 = 1
Tactic: rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
inst_3 : Invertible A.det
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A.adjugate * A) = 1
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
rw₂ : HSMul.hSMul (β := Matrix n n α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ * A.det) 1 = 1
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate * A = 1
have rw₃ : HSMul.hSMul (α := α) (β := Matrix n n α) 1 1 = 1
Tactic: rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
inst_3 : Invertible A.det
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A.adjugate * A) = 1
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
rw₂ : HSMul.hSMul (β := Matrix n n α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ * A.det) 1 = 1
rw₃ : HSMul.hSMul (α := α) (β := Matrix n n α) 1 1 = 1
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate * A = 1
have rw₄ : Eq (α := Matrix n n α) 1 1
Tactic: rw [smul_mul_assoc, adjugate_mul, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
inst_3 : Invertible A.det
⊢ A * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate = 1
have rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A * A.adjugate) = 1
Tactic: rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
inst_3 : Invertible A.det
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A * A.adjugate) = 1
⊢ A * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate = 1
have rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
Tactic: rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.NonsingularInverse (goal)
Goal:
l : Type u_1
m : Type u
n : Type u'
α : Type v
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : CommRing α
A B : Matrix n n α
inst_3 : Invertible A.det
rw : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • (A * A.adjugate) = 1
rw₁ : @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • HSMul.hSMul (β := Matrix n n α) A.det 1 = 1
⊢ A * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ • A.adjugate = 1
have rw₂ : HSMul.hSMul (β := Matrix n n α) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne A.det _ * A.det) 1 = 1
Tactic: rw [mul_smul_comm, mul_adjugate, smul_smul, invOf_mul_self, one_smul]