awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  (M.map (⇑(algebraMap A K) : (a : A) → K) *ᵥ
        Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) ⋯)
      i =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
⊢ (algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) ⋯) i) =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
have mpr₁ : ((fun (j : n) ↦ M.map (⇑(algebraMap A K) : (a : A) → K) i j) ⬝ᵥ
    Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) sorry) =
  (fun (j : n) ↦ (RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i j) ⬝ᵥ
    HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v
Tactic: simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  (M.map (⇑(algebraMap A K) : (a : A) → K) *ᵥ
        Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) ⋯)
      i =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
mpr₁ :
  ((fun (j : n) ↦ M.map (⇑(algebraMap A K) : (a : A) → K) i j) ⬝ᵥ
      Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) ⋯) =
    (fun (j : n) ↦ (RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i j) ⬝ᵥ
      HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v
⊢ (algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) ⋯) i) =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
have mpr₂ : Eq.{u_5 + 1} (α := K)
  (∑ x : n,
    HMul.hMul (α := K) (M.map (⇑(algebraMap A K) : (a : A) → K) i x)
      (Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) (fun (i : n) ↦ f (v i) sorry)
        x))
  (∑ x : n,
    HMul.hMul (α := K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i x : K)
      (HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v x))
Tactic: simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  (M.map (⇑(algebraMap A K) : (a : A) → K) *ᵥ
        Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) ⋯)
      i =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
mpr₁ :
  ((fun (j : n) ↦ M.map (⇑(algebraMap A K) : (a : A) → K) i j) ⬝ᵥ
      Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) ⋯) =
    (fun (j : n) ↦ (RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i j) ⬝ᵥ
      HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v
mpr₂ :
  Eq.{u_5 + 1} (α := K)
    (∑ x : n,
      HMul.hMul (α := K) (M.map (⇑(algebraMap A K) : (a : A) → K) i x)
        (Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) (fun (i : n) ↦ f (v i) ⋯)
          x))
    (∑ x : n,
      HMul.hMul (α := K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i x : K)
        (HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v x))
⊢ (algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) ⋯) i) =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
have mpr₃ : Eq.{u_5 + 1} (α := K)
  (∑ x : n,
    HMul.hMul (α := K) (β := K) (M.map (⇑(algebraMap A K) : (a : A) → K) i x : K)
      ((algebraMap A K : (a : A) → K) (f (v x) sorry) : K))
  (∑ x : n,
    HMul.hMul (α := K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M i x : K)
      (HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v x))
Tactic: simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
⊢ ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i =
    0
have mpr : HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K)
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) i =
  0
Tactic: rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K)
      ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) i =
    0
⊢ ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i =
    0
have mpr₁ : HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K) 0 i = 0
Tactic: rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K)
      ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) i =
    0
mpr₁ : HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K) 0 i = 0
⊢ ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i =
    0
have mpr₂ : HSMul.hSMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (0 i) = 0
Tactic: rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K)
      ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) i =
    0
mpr₁ : HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K) 0 i = 0
mpr₂ : HSMul.hSMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (0 i) = 0
⊢ ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i =
    0
have mpr₃ : HSMul.hSMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) 0 = 0
Tactic: rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K)
      ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) i =
    0
mpr₁ : HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K) 0 i = 0
mpr₂ : HSMul.hSMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (0 i) = 0
mpr₃ : HSMul.hSMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) 0 = 0
⊢ ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i =
    0
have mpr₄ : Eq.{u_5 + 1} (α := K) 0 0
Tactic: rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate ↔ M.det ≠ 0
have refine : M.Nondegenerate → M.det ≠ 0
Tactic: refine ⟨?_, nondegenerate_of_det_ne_zero⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate → M.det ≠ 0
have rw : M.Nondegenerate → ¬∃ (v : n → A), v ≠ 0 ∧ v ᵥ* M = 0
Tactic: rw [ne_eq, ← exists_vecMul_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate → ¬∃ (v : n → A), v ≠ 0 ∧ v ᵥ* M = 0
have push : M.Nondegenerate → ∀ (v : n → A) (_ : v ≠ 0), v ᵥ* M ≠ 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
hM : M.Nondegenerate
v : n → A
hv : v ≠ 0
hMv : v ᵥ* M = 0
⊢ False
have obtain : ∀ (w : n → A) (hwMv : v ⬝ᵥ M *ᵥ w ≠ 0), False
Tactic: obtain ⟨w, hwMv⟩ := hM.exists_not_ortho_of_ne_zero hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ M.SeparatingLeft ↔ M.det ≠ 0
have refine : ∀ (h : M.SeparatingLeft) (hc : M.det = 0), False
Tactic: refine ⟨fun h hc ↦ ?_, fun h ↦ (nondegenerate_of_det_ne_zero h).1⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingLeft
hc : M.det = 0
⊢ False
have obtain : ∀ (v : n → A) (hvne : v ≠ 0) (hv : v ᵥ* M = 0), False
Tactic: obtain ⟨v, hvne, hv⟩ := exists_vecMul_eq_zero_iff.mpr hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingLeft
hc : M.det = 0
v : n → A
hvne : v ≠ 0
hv : v ᵥ* M = 0
⊢ False
have refine : ∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0
Tactic: refine hvne (separatingLeft_def.mp h v ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ M.SeparatingRight ↔ M.det ≠ 0
have refine : ∀ (h : M.SeparatingRight) (hc : M.det = 0), False
Tactic: refine ⟨fun h hc ↦ ?_, fun h ↦ (nondegenerate_of_det_ne_zero h).2⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingRight
hc : M.det = 0
⊢ False
have obtain : ∀ (v : n → A) (hvne : v ≠ 0) (hv : M *ᵥ v = 0), False
Tactic: obtain ⟨v, hvne, hv⟩ := exists_mulVec_eq_zero_iff.mpr hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
h : M.SeparatingRight
hc : M.det = 0
v : n → A
hvne : v ≠ 0
hv : M *ᵥ v = 0
⊢ False
have refine : ∀ (v_1 : n → A), v_1 ⬝ᵥ M *ᵥ v = 0
Tactic: refine hvne (separatingRight_def.mp h v ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : N.Nondegenerate
⊢ (M * N).Nondegenerate ↔ M.Nondegenerate
have simp : ∀ (h : N.det ≠ 0), M.det * N.det ≠ 0 ↔ M.det ≠ 0
Tactic: simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : N.Nondegenerate
⊢ (M * N).Nondegenerate ↔ M.Nondegenerate
have simp : ∀ (h : N.det ≠ 0), M.det * N.det ≠ 0 ↔ M.det ≠ 0
Tactic: classical
  simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
  exact mul_ne_zero_iff_right h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : M.Nondegenerate
⊢ (M * N).Nondegenerate ↔ N.Nondegenerate
have simp : ∀ (h : M.det ≠ 0), M.det * N.det ≠ 0 ↔ N.det ≠ 0
Tactic: simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M N : Matrix n n A
h : M.Nondegenerate
⊢ (M * N).Nondegenerate ↔ N.Nondegenerate
have simp : ∀ (h : M.det ≠ 0), M.det * N.det ≠ 0 ↔ N.det ≠ 0
Tactic: classical
  simp only [nondegenerate_iff_det_ne_zero, det_mul] at h ⊢
  exact mul_ne_zero_iff_left h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Finite n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M : Matrix n n A
t : A
h : t ≠ 0
⊢ (t • M).Nondegenerate ↔ M.Nondegenerate
have have : ∀ (this : (α : Type u_1) → [Finite α] → Fintype α), (t • M).Nondegenerate ↔ M.Nondegenerate
Tactic: have := Fintype.ofFinite
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Finite n
A : Type u_4
inst_1 : CommRing A
inst_2 : IsDomain A
M : Matrix n n A
t : A
h : t ≠ 0
this : (α : Type u_1) → [Finite α] → Fintype α
⊢ (t • M).Nondegenerate ↔ M.Nondegenerate
have rw : ((∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → v = 0) ∧
    ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ (t • M) *ᵥ w = 0) → w = 0) ↔
  (∀ (v : n → A), (∀ (w : n → A), v ⬝ᵥ M *ᵥ w = 0) → v = 0) ∧ ∀ (w : n → A), (∀ (v : n → A), v ⬝ᵥ M *ᵥ w = 0) → w = 0
Tactic: rw [nondegenerate_def, nondegenerate_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, A i j)
⊢ A.det ≠ 0
have inl : IsEmpty n → A.det ≠ 0
Tactic: cases isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, A i j)
inl : IsEmpty n → A.det ≠ 0
⊢ A.det ≠ 0
have inr : Nonempty n → A.det ≠ 0
Tactic: cases isEmpty_or_nonempty n
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h2 : ∀ (j : n), LT.lt.{u_2} (α := S) 0 (∑ i : n, A i j)
h : Nonempty n
⊢ A.det ≠ 0
have inr : ∀ (h2 : A.det = 0), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
Tactic: contrapose! h2
Cleared hypotheses: h2
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
inst_1 : DecidableEq n
S : Type u_2
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
A : Matrix n n S
h1 : Pairwise fun (i j : n) ↦ A i j < 0
h : Nonempty n
h2 : A.det = 0
⊢ ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
have inr : ∀ (v : n → S) (h_vnz : v ≠ 0) (h_vA : v ᵥ* A = 0), ∃ (j : n), LE.le.{u_2} (α := S) (∑ i : n, A i j) 0
Tactic: obtain ⟨v, ⟨h_vnz, h_vA⟩⟩ := Matrix.exists_vecMul_eq_zero_iff.mpr h2