[GOAL]
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit (det A)
⊢ M ≃ₗ[R] M
[PROOFSTEP]
refine'
  { toLin b b A with
    toFun := toLin b b A
    invFun := toLin b b A⁻¹
    left_inv := fun x => _
    right_inv := fun x => _ }
[GOAL]
case refine'_1
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit (det A)
src✝ : (fun x => M →ₗ[R] M) A := ↑(toLin b b) A
x : M
⊢ ↑(↑(toLin b b) A⁻¹)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := ↑(↑(toLin b b) A),
                map_add' :=
                  (_ :
                    ∀ (x y : M),
                      AddHom.toFun src✝.toAddHom (x + y) =
                        AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
            map_smul' :=
              (_ :
                ∀ (r : R) (x : M),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        x) =
    x
[PROOFSTEP]
simp only
[GOAL]
case refine'_2
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit (det A)
src✝ : (fun x => M →ₗ[R] M) A := ↑(toLin b b) A
x : M
⊢ AddHom.toFun
      {
          toAddHom :=
            { toFun := ↑(↑(toLin b b) A),
              map_add' :=
                (_ :
                  ∀ (x y : M),
                    AddHom.toFun src✝.toAddHom (x + y) = AddHom.toFun src✝.toAddHom x + AddHom.toFun src✝.toAddHom y) },
          map_smul' :=
            (_ :
              ∀ (r : R) (x : M),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(↑(toLin b b) A⁻¹) x) =
    x
[PROOFSTEP]
simp only
[GOAL]
case refine'_1
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit (det A)
src✝ : (fun x => M →ₗ[R] M) A := ↑(toLin b b) A
x : M
⊢ ↑(↑(toLin b b) A⁻¹) (↑(↑(toLin b b) A) x) = x
[PROOFSTEP]
rw [← LinearMap.comp_apply]
[GOAL]
case refine'_2
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit (det A)
src✝ : (fun x => M →ₗ[R] M) A := ↑(toLin b b) A
x : M
⊢ ↑(↑(toLin b b) A) (↑(↑(toLin b b) A⁻¹) x) = x
[PROOFSTEP]
rw [← LinearMap.comp_apply]
[GOAL]
case refine'_1
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit (det A)
src✝ : (fun x => M →ₗ[R] M) A := ↑(toLin b b) A
x : M
⊢ ↑(comp (↑(toLin b b) A⁻¹) (↑(toLin b b) A)) x = x
[PROOFSTEP]
simp only [← Matrix.toLin_mul b b b, Matrix.nonsing_inv_mul _ hA, Matrix.mul_nonsing_inv _ hA, toLin_one,
  LinearMap.id_apply]
[GOAL]
case refine'_2
n : Type u_1
inst✝⁴ : Fintype n
R : Type u_2
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
b : Basis n R M
inst✝ : DecidableEq n
A : Matrix n n R
hA : IsUnit (det A)
src✝ : (fun x => M →ₗ[R] M) A := ↑(toLin b b) A
x : M
⊢ ↑(comp (↑(toLin b b) A) (↑(toLin b b) A⁻¹)) x = x
[PROOFSTEP]
simp only [← Matrix.toLin_mul b b b, Matrix.nonsing_inv_mul _ hA, Matrix.mul_nonsing_inv _ hA, toLin_one,
  LinearMap.id_apply]
[GOAL]
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∃ v x, mulVec M v = 0) → det M = 0
[PROOFSTEP]
rintro ⟨v, hv, mul_eq⟩
[GOAL]
case mp.intro.intro
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ det M = 0
[PROOFSTEP]
contrapose! hv
[GOAL]
case mp.intro.intro
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
v : n → K
mul_eq : mulVec M v = 0
hv : det M ≠ 0
⊢ v = 0
[PROOFSTEP]
exact eq_zero_of_mulVec_eq_zero hv mul_eq
[GOAL]
case mpr
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ det M = 0 → ∃ v x, mulVec M v = 0
[PROOFSTEP]
contrapose!
[GOAL]
case mpr
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
⊢ (∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0) → det M ≠ 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
⊢ det M ≠ 0
[PROOFSTEP]
have : Function.Injective (Matrix.toLin' M) := by
  simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h
[GOAL]
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
⊢ Function.Injective ↑(↑toLin' M)
[PROOFSTEP]
simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h
[GOAL]
case mpr
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
⊢ det M ≠ 0
[PROOFSTEP]
have : M * LinearMap.toMatrix' ((LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).symm : (n → K) →ₗ[K] n → K) = 1 :=
  by
  refine' Matrix.toLin'.injective (LinearMap.ext fun v => _)
  rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]
  exact (LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).apply_symm_apply v
[GOAL]
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
⊢ M * ↑toMatrix' ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this)) = 1
[PROOFSTEP]
refine' Matrix.toLin'.injective (LinearMap.ext fun v => _)
[GOAL]
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
v : n → K
⊢ ↑(↑toLin' (M * ↑toMatrix' ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this)))) v = ↑(↑toLin' 1) v
[PROOFSTEP]
rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]
[GOAL]
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this : Function.Injective ↑(↑toLin' M)
v : n → K
⊢ ↑(↑toLin' M) (↑↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this)) v) = ↑LinearMap.id v
[PROOFSTEP]
exact (LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).apply_symm_apply v
[GOAL]
case mpr
n : Type u_1
inst✝⁵ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M✝
inst✝² : Module R M✝
K : Type u_4
inst✝¹ : DecidableEq n
inst✝ : Field K
M : Matrix n n K
h : ∀ (v : n → K), v ≠ 0 → mulVec M v ≠ 0
this✝ : Function.Injective ↑(↑toLin' M)
this : M * ↑toMatrix' ↑(LinearEquiv.symm (LinearEquiv.ofInjectiveEndo (↑toLin' M) this✝)) = 1
⊢ det M ≠ 0
[PROOFSTEP]
exact Matrix.det_ne_zero_of_right_inverse this
[GOAL]
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
[PROOFSTEP]
have : (∃ (v : _) (_ : v ≠ 0), mulVec ((algebraMap A K).mapMatrix M) v = 0) ↔ _ := exists_mulVec_eq_zero_iff_aux
[GOAL]
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this :
  (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det (↑(RingHom.mapMatrix (algebraMap A K)) M) = 0
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
[PROOFSTEP]
rw [← RingHom.map_det, IsFractionRing.to_map_eq_zero_iff] at this 
[GOAL]
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
⊢ (∃ v x, mulVec M v = 0) ↔ det M = 0
[PROOFSTEP]
refine' Iff.trans _ this
[GOAL]
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
⊢ (∃ v x, mulVec M v = 0) ↔ ∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
⊢ (∃ v x, mulVec M v = 0) → ∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
[PROOFSTEP]
rintro ⟨v, hv, mul_eq⟩
[GOAL]
case mpr
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
⊢ (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) → ∃ v x, mulVec M v = 0
[PROOFSTEP]
rintro ⟨v, hv, mul_eq⟩
[GOAL]
case mp.intro.intro
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ ∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
[PROOFSTEP]
refine' ⟨fun i => algebraMap _ _ (v i), mt (fun h => funext fun i => _) hv, _⟩
[GOAL]
case mp.intro.intro.refine'_1
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
h : (fun i => ↑(algebraMap A K) (v i)) = 0
i : n
⊢ v i = OfNat.ofNat 0 i
[PROOFSTEP]
exact IsFractionRing.to_map_eq_zero_iff.mp (congr_fun h i)
[GOAL]
case mp.intro.intro.refine'_2
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
⊢ (mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) fun i => ↑(algebraMap A K) (v i)) = 0
[PROOFSTEP]
ext i
[GOAL]
case mp.intro.intro.refine'_2.h
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
i : n
⊢ mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (fun i => ↑(algebraMap A K) (v i)) i = OfNat.ofNat 0 i
[PROOFSTEP]
refine' (RingHom.map_mulVec _ _ _ i).symm.trans _
[GOAL]
case mp.intro.intro.refine'_2.h
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → A
hv : v ≠ 0
mul_eq : mulVec M v = 0
i : n
⊢ ↑(algebraMap A K) (mulVec (fun i j => M i j) (fun i => v i) i) = OfNat.ofNat 0 i
[PROOFSTEP]
rw [mul_eq, Pi.zero_apply, RingHom.map_zero, Pi.zero_apply]
[GOAL]
case mpr.intro.intro
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
⊢ ∃ v x, mulVec M v = 0
[PROOFSTEP]
letI := Classical.decEq K
[GOAL]
case mpr.intro.intro
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
⊢ ∃ v x, mulVec M v = 0
[PROOFSTEP]
obtain ⟨⟨b, hb⟩, ba_eq⟩ := IsLocalization.exist_integer_multiples_of_finset (nonZeroDivisors A) (Finset.univ.image v)
[GOAL]
case mpr.intro.intro.intro.mk
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
ba_eq : ∀ (a : K), a ∈ Finset.image v Finset.univ → IsLocalization.IsInteger A (↑{ val := b, property := hb } • a)
⊢ ∃ v x, mulVec M v = 0
[PROOFSTEP]
choose f hf using ba_eq
[GOAL]
case mpr.intro.intro.intro.mk
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
⊢ ∃ v x, mulVec M v = 0
[PROOFSTEP]
refine' ⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩), mt (fun h => funext fun i => _) hv, _⟩
[GOAL]
case mpr.intro.intro.intro.mk.refine'_1
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
⊢ v i = OfNat.ofNat 0 i
[PROOFSTEP]
have := congr_arg (algebraMap A K) (congr_fun h i)
[GOAL]
case mpr.intro.intro.intro.mk.refine'_1
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
this : ↑(algebraMap A K) (f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = ↑(algebraMap A K) (OfNat.ofNat 0 i)
⊢ v i = OfNat.ofNat 0 i
[PROOFSTEP]
rw [hf, Subtype.coe_mk, Pi.zero_apply, RingHom.map_zero, Algebra.smul_def, mul_eq_zero,
  IsFractionRing.to_map_eq_zero_iff] at this 
[GOAL]
case mpr.intro.intro.intro.mk.refine'_1
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝¹ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this✝ : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
h : (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
i : n
this : b = 0 ∨ v i = 0
⊢ v i = OfNat.ofNat 0 i
[PROOFSTEP]
exact this.resolve_left (nonZeroDivisors.ne_zero hb)
[GOAL]
case mpr.intro.intro.intro.mk.refine'_2
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
⊢ (mulVec M fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) = 0
[PROOFSTEP]
ext i
[GOAL]
case mpr.intro.intro.intro.mk.refine'_2.h
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i = OfNat.ofNat 0 i
[PROOFSTEP]
refine' IsFractionRing.injective A K _
[GOAL]
case mpr.intro.intro.intro.mk.refine'_2.h
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ ↑(algebraMap A K) (mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i) =
    ↑(algebraMap A K) (OfNat.ofNat 0 i)
[PROOFSTEP]
calc
  algebraMap A K (M.mulVec (fun i : n => f (v i) _) i) =
      ((algebraMap A K).mapMatrix M).mulVec (algebraMap _ K b • v) i :=
    ?_
  _ = 0 := ?_
  _ = algebraMap A K 0 := (RingHom.map_zero _).symm
[GOAL]
case mpr.intro.intro.intro.mk.refine'_2.h.calc_1
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ ↑(algebraMap A K) (mulVec M (fun i => f (v i) (_ : v i ∈ Finset.image v Finset.univ)) i) =
    mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (↑(algebraMap A K) b • v) i
[PROOFSTEP]
simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf, RingHom.mapMatrix_apply, Pi.smul_apply,
  smul_eq_mul, Algebra.smul_def]
[GOAL]
case mpr.intro.intro.intro.mk.refine'_2.h.calc_2
n : Type u_1
inst✝⁹ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M✝
inst✝⁶ : Module R M✝
A : Type u_4
K : Type u_5
inst✝⁵ : DecidableEq n
inst✝⁴ : CommRing A
inst✝³ : Nontrivial A
inst✝² : Field K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
M : Matrix n n A
this✝ : (∃ v x, mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0) ↔ det M = 0
v : n → K
hv : v ≠ 0
mul_eq : mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) v = 0
this : DecidableEq K := Classical.decEq K
b : A
hb : b ∈ nonZeroDivisors A
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf : ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ), ↑(algebraMap A K) (f a a_1) = ↑{ val := b, property := hb } • a
i : n
⊢ mulVec (↑(RingHom.mapMatrix (algebraMap A K)) M) (↑(algebraMap A K) b • v) i = 0
[PROOFSTEP]
rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]
[GOAL]
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ (∃ v x, vecMul v M = 0) ↔ det M = 0
[PROOFSTEP]
simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff
[GOAL]
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M ↔ det M ≠ 0
[PROOFSTEP]
refine' Iff.trans _ (not_iff_not.mpr exists_vecMul_eq_zero_iff)
[GOAL]
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M ↔ ¬∃ v x, vecMul v M = 0
[PROOFSTEP]
simp only [not_exists]
[GOAL]
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M ↔ ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
[PROOFSTEP]
constructor
[GOAL]
case mp
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ Nondegenerate M → ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
[PROOFSTEP]
intro hM v hv hMv
[GOAL]
case mp
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : Nondegenerate M
v : n → A
hv : v ≠ 0
hMv : vecMul v M = 0
⊢ False
[PROOFSTEP]
obtain ⟨w, hwMv⟩ := hM.exists_not_ortho_of_ne_zero hv
[GOAL]
case mp.intro
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
hM : Nondegenerate M
v : n → A
hv : v ≠ 0
hMv : vecMul v M = 0
w : n → A
hwMv : v ⬝ᵥ mulVec M w ≠ 0
⊢ False
[PROOFSTEP]
simp [dotProduct_mulVec, hMv, zero_dotProduct, ne_eq, not_true] at hwMv 
[GOAL]
case mpr
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
⊢ (∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0) → Nondegenerate M
[PROOFSTEP]
intro h v hv
[GOAL]
case mpr
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ mulVec M w = 0
⊢ v = 0
[PROOFSTEP]
refine' not_imp_not.mp (h v) (funext fun i => _)
[GOAL]
case mpr
n : Type u_1
inst✝⁶ : Fintype n
R : Type u_2
M✝ : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M✝
inst✝³ : Module R M✝
A : Type u_4
inst✝² : DecidableEq n
inst✝¹ : CommRing A
inst✝ : IsDomain A
M : Matrix n n A
h : ∀ (x : n → A), x ≠ 0 → ¬vecMul x M = 0
v : n → A
hv : ∀ (w : n → A), v ⬝ᵥ mulVec M w = 0
i : n
⊢ vecMul v M i = OfNat.ofNat 0 i
[PROOFSTEP]
simpa only [dotProduct_mulVec, dotProduct_single, mul_one] using hv (Pi.single i 1)
[GOAL]
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (j : n), 0 < ∑ i : n, A i j
⊢ det A ≠ 0
[PROOFSTEP]
cases isEmpty_or_nonempty n
[GOAL]
case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (j : n), 0 < ∑ i : n, A i j
h✝ : IsEmpty n
⊢ det A ≠ 0
[PROOFSTEP]
simp
[GOAL]
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (j : n), 0 < ∑ i : n, A i j
h✝ : Nonempty n
⊢ det A ≠ 0
[PROOFSTEP]
contrapose! h2
[GOAL]
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
⊢ ∃ j, ∑ i : n, A i j ≤ 0
[PROOFSTEP]
obtain ⟨v, ⟨h_vnz, h_vA⟩⟩ := Matrix.exists_vecMul_eq_zero_iff.mpr h2
[GOAL]
case inr.intro.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
⊢ ∃ j, ∑ i : n, A i j ≤ 0
[PROOFSTEP]
wlog h_sup : 0 < Finset.sup' Finset.univ Finset.univ_nonempty v
[GOAL]
case inr.intro.intro.inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
⊢ ∃ j, ∑ i : n, A i j ≤ 0
[PROOFSTEP]
refine this h1 inferInstance h2 (-1 • v) ?_ ?_ ?_
[GOAL]
case inr.intro.intro.inr.refine_1
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
⊢ -1 • v ≠ 0
[PROOFSTEP]
exact smul_ne_zero (by norm_num) h_vnz
[GOAL]
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
⊢ -1 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
case inr.intro.intro.inr.refine_2
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
⊢ (vecMul (-1 • v) fun i j => A i j) = 0
[PROOFSTEP]
rw [Matrix.vecMul_smul, h_vA, smul_zero]
[GOAL]
case inr.intro.intro.inr.refine_3
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
⊢ 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) (-1 • v)
[PROOFSTEP]
obtain ⟨i, hi⟩ := Function.ne_iff.mp h_vnz
[GOAL]
case inr.intro.intro.inr.refine_3.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
h_sup : ¬0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
i : n
hi : v i ≠ OfNat.ofNat 0 i
⊢ 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) (-1 • v)
[PROOFSTEP]
simp_rw [Finset.lt_sup'_iff, Finset.mem_univ, true_and] at h_sup ⊢
[GOAL]
case inr.intro.intro.inr.refine_3.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
i : n
hi : v i ≠ OfNat.ofNat 0 i
h_sup : ¬∃ b, 0 < v b
⊢ ∃ b, 0 < (-1 • v) b
[PROOFSTEP]
simp_rw [not_exists, not_lt] at h_sup 
[GOAL]
case inr.intro.intro.inr.refine_3.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
i : n
hi : v i ≠ OfNat.ofNat 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ ∃ b, 0 < (-1 • v) b
[PROOFSTEP]
refine ⟨i, ?_⟩
[GOAL]
case inr.intro.intro.inr.refine_3.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
i : n
hi : v i ≠ OfNat.ofNat 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ 0 < (-1 • v) i
[PROOFSTEP]
rw [Pi.smul_apply, neg_smul, one_smul, Left.neg_pos_iff]
[GOAL]
case inr.intro.intro.inr.refine_3.intro
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
this :
  ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {S : Type u_2} [inst_2 : LinearOrderedCommRing S]
    {A : Matrix n n S},
    (∀ (i j : n), i ≠ j → A i j < 0) →
      ∀ (h : Nonempty n),
        det A = 0 →
          ∀ (v : n → S),
            v ≠ 0 →
              vecMul v A = 0 → 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v → ∃ j, ∑ i : n, A i j ≤ 0
i : n
hi : v i ≠ OfNat.ofNat 0 i
h_sup : ∀ (x : n), v x ≤ 0
⊢ v i < 0
[PROOFSTEP]
refine Ne.lt_of_le hi (h_sup i)
[GOAL]
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
h_sup : 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
⊢ ∃ j, ∑ i : n, A i j ≤ 0
[PROOFSTEP]
obtain ⟨j₀, -, h_j₀⟩ := Finset.exists_mem_eq_sup' Finset.univ_nonempty v
[GOAL]
case intro.intro
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
h_sup : 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
j₀ : n
h_j₀ : Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v = v j₀
⊢ ∃ j, ∑ i : n, A i j ≤ 0
[PROOFSTEP]
refine ⟨j₀, ?_⟩
[GOAL]
case intro.intro
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
h_sup : 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
j₀ : n
h_j₀ : Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v = v j₀
⊢ ∑ i : n, A i j₀ ≤ 0
[PROOFSTEP]
rw [← mul_le_mul_left (h_j₀ ▸ h_sup), Finset.mul_sum, mul_zero]
[GOAL]
case intro.intro
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
h_sup : 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
j₀ : n
h_j₀ : Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v = v j₀
⊢ ∑ x : n, v j₀ * A x j₀ ≤ 0
[PROOFSTEP]
rw [show 0 = ∑ i, v i * A i j₀ from (congrFun h_vA j₀).symm]
[GOAL]
case intro.intro
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
h_sup : 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
j₀ : n
h_j₀ : Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v = v j₀
⊢ ∑ x : n, v j₀ * A x j₀ ≤ ∑ i : n, v i * A i j₀
[PROOFSTEP]
refine Finset.sum_le_sum (fun i hi => ?_)
[GOAL]
case intro.intro
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
h_sup : 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
j₀ : n
h_j₀ : Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v = v j₀
i : n
hi : i ∈ Finset.univ
⊢ v j₀ * A i j₀ ≤ v i * A i j₀
[PROOFSTEP]
by_cases h : i = j₀
[GOAL]
case pos
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
h_sup : 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
j₀ : n
h_j₀ : Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v = v j₀
i : n
hi : i ∈ Finset.univ
h : i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀
[PROOFSTEP]
rw [h]
[GOAL]
case neg
n✝ : Type u_1
inst✝³ : Fintype n✝
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h✝ : Nonempty n
h2 : det A = 0
v : n → S
h_vnz : v ≠ 0
h_vA : vecMul v A = 0
h_sup : 0 < Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v
j₀ : n
h_j₀ : Finset.sup' Finset.univ (_ : Finset.Nonempty Finset.univ) v = v j₀
i : n
hi : i ∈ Finset.univ
h : ¬i = j₀
⊢ v j₀ * A i j₀ ≤ v i * A i j₀
[PROOFSTEP]
exact (mul_le_mul_right_of_neg (h1 i j₀ h)).mpr (h_j₀ ▸ Finset.le_sup' v hi)
[GOAL]
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (i : n), 0 < ∑ j : n, A i j
⊢ det A ≠ 0
[PROOFSTEP]
rw [← Matrix.det_transpose]
[GOAL]
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (i : n), 0 < ∑ j : n, A i j
⊢ det Aᵀ ≠ 0
[PROOFSTEP]
refine det_ne_zero_of_sum_col_pos ?_ ?_
[GOAL]
case refine_1
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (i : n), 0 < ∑ j : n, A i j
⊢ ∀ (i j : n), i ≠ j → Aᵀ i j < 0
[PROOFSTEP]
simp_rw [Matrix.transpose_apply]
[GOAL]
case refine_1
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (i : n), 0 < ∑ j : n, A i j
⊢ ∀ (i j : n), i ≠ j → A j i < 0
[PROOFSTEP]
exact fun i j h => h1 j i h.symm
[GOAL]
case refine_2
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (i : n), 0 < ∑ j : n, A i j
⊢ ∀ (j : n), 0 < ∑ i : n, Aᵀ i j
[PROOFSTEP]
simp_rw [Matrix.transpose_apply]
[GOAL]
case refine_2
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
S : Type u_2
inst✝ : LinearOrderedCommRing S
A : Matrix n n S
h1 : ∀ (i j : n), i ≠ j → A i j < 0
h2 : ∀ (i : n), 0 < ∑ j : n, A i j
⊢ ∀ (j : n), 0 < ∑ x : n, A j x
[PROOFSTEP]
exact h2
