awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
R : Type u_2
M : Type u_3
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis n R M
inst_4 : DecidableEq n
A : Matrix n n R
hA : IsUnit A.det
x : M
simp_rw :
  ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) A ∘ₗ (toLin b b : (a : Matrix n n R) → M →ₗ[R] M) A⁻¹ : (a : M) → M) x =
    x
simp_rw₁ : (((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (A * A⁻¹) : M →ₗ[R] M) : (a : M) → M) x = x
simp_rw₂ : ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) 1 : (a : M) → M) x = x
simp_rw₃ : (LinearMap.id : (a : M) → M) x = x
⊢ (((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) A : M →ₗ[R] M) : (a : M) → M)
      ((((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) A⁻¹ : M →ₗ[R] M) : (a : M) → M) x : M) =
    x

Tactic:
simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.mul_nonsing_inv _ hA,
      toLin_one, LinearMap.id_apply]

Premises used: LinearMap.id_apply, LinearMap.comp_apply, Matrix.toLin_mul, Matrix.toLin_one, Matrix.mul_nonsing_inv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
R : Type u_2
M : Type u_3
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis n R M
inst_4 : DecidableEq n
A : Matrix n n R
hA : IsUnit A.det
⊢ Eq.{u_3 + 1} (α := Submodule R M)
    (ker (R₂ := R) (M₂ := M) (τ₁₂ := RingHom.id R) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) A)) ⊥

Tactic:
ker_eq_bot.mpr (toLinearEquiv b A hA).injective

Premises used: Iff.mpr, LinearMap.ker_eq_bot, Matrix.toLinearEquiv, LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
R : Type u_2
M : Type u_3
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
b : Basis n R M
inst_4 : DecidableEq n
A : Matrix n n R
hA : IsUnit A.det
⊢ Eq.{u_3 + 1} (α := Submodule R M)
    (range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) A)) ⊤

Tactic:
range_eq_top.mpr (toLinearEquiv b A hA).surjective

Premises used: Iff.mpr, LinearEquiv.surjective, LinearMap.range_eq_top, Matrix.toLinearEquiv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
mp : (∃ (v : n → K), v ≠ 0 ∧ M *ᵥ v = 0) → M.det = 0
mpr : M.det = 0 → ∃ (v : n → K), v ≠ 0 ∧ M *ᵥ v = 0
⊢ (∃ (v : n → K), v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
v : n → K
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
mp : ∀ (hv : M.det ≠ 0), v = 0
⊢ M.det = 0

Tactic:
contrapose! hv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
v : n → K
mul_eq : M *ᵥ v = 0
hv : M.det ≠ 0
⊢ v = 0

Tactic:
eq_zero_of_mulVec_eq_zero hv mul_eq

Premises used: Matrix.eq_zero_of_mulVec_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
v : n → K
mul_eq : M *ᵥ v = 0
hv : M.det ≠ 0
⊢ v = 0

Tactic:
exact eq_zero_of_mulVec_eq_zero hv mul_eq

Premises used: Matrix.eq_zero_of_mulVec_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
mpr : (∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0) → M.det ≠ 0
⊢ M.det = 0 → ∃ (v : n → K), v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
contrapose!
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
⊢ Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)

Tactic:
simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h

Premises used: LinearMap.ker_eq_bot, Matrix.ker_toLin'_eq_bot_iff, not_imp_not
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
⊢ Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)

Tactic:
have : Function.Injective (Matrix.toLin' M) := by
      simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
this :
  Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
⊢ HMul.hMul (β := Matrix n n K) M
      ((toMatrix' : (a : (n → K) →ₗ[K] n → K) → Matrix n n K)
          (↑(LinearEquiv.symm
                (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                  ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this)) :
            (n → K) →ₗ[K] n → K) :
        Matrix n n K) =
    1

Tactic:
Matrix.toLin'.injective (LinearMap.ext fun v => ?_)

Premises used: LinearMap.ext, Matrix.toLin', LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
this :
  Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
refine :
  ∀ (v : n → K),
    Eq (α := n → K)
      ((((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K)
                (HMul.hMul (β := Matrix n n K) M
                  ((toMatrix' : (a : (n → K) →ₗ[K] n → K) → Matrix n n K)
                      (↑(LinearEquiv.symm
                            (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                              ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this)) :
                        (n → K) →ₗ[K] n → K) :
                    Matrix n n K)) :
              (n → K) →ₗ[K] n → K) :
            (a : n → K) → n → K)
          v :
        n → K)
      (((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) 1 : (a : n → K) → n → K) v : n → K)
⊢ HMul.hMul (β := Matrix n n K) M
      ((toMatrix' : (a : (n → K) →ₗ[K] n → K) → Matrix n n K)
          (↑(LinearEquiv.symm
                (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                  ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this)) :
            (n → K) →ₗ[K] n → K) :
        Matrix n n K) =
    1

Tactic:
refine Matrix.toLin'.injective (LinearMap.ext fun v => ?_)

Premises used: LinearMap.ext, Matrix.toLin', LinearEquiv.injective
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
this :
  Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
v : n → K
rw :
  Eq (α := n → K)
    ((((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
        ((((↑(LinearEquiv.symm
                      (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                        ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this)) :
                  (n → K) →ₗ[K] n → K) :
                (n → K) →ₗ[K] n → K) :
              (a : n → K) → n → K)
            v :
          n → K) :
      n → K)
    ((LinearMap.id : (a : n → K) → n → K) v : n → K)
⊢ Eq (α := n → K)
    ((((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K)
              (HMul.hMul (β := Matrix n n K) M
                ((toMatrix' : (a : (n → K) →ₗ[K] n → K) → Matrix n n K)
                    (↑(LinearEquiv.symm
                          (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                            ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this)) :
                      (n → K) →ₗ[K] n → K) :
                  Matrix n n K)) :
            (n → K) →ₗ[K] n → K) :
          (a : n → K) → n → K)
        v :
      n → K)
    (((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) 1 : (a : n → K) → n → K) v : n → K)

Tactic:
rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]

Premises used: LinearMap.comp_apply, Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix'
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
this :
  Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
v : n → K
⊢ Eq (α := n → K)
    ((((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
        ((((↑(LinearEquiv.symm
                      (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                        ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this)) :
                  (n → K) →ₗ[K] n → K) :
                (n → K) →ₗ[K] n → K) :
              (a : n → K) → n → K)
            v :
          n → K) :
      n → K)
    ((LinearMap.id : (a : n → K) → n → K) v : n → K)

Tactic:
(LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).apply_symm_apply v

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.toLin', LinearEquiv.apply_symm_apply, LinearEquiv.ofInjectiveEndo, Matrix.mulVec, DFunLike.coe, Finset.sum
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
this :
  Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
v : n → K
⊢ Eq (α := n → K)
    ((((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
        ((((↑(LinearEquiv.symm
                      (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                        ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this)) :
                  (n → K) →ₗ[K] n → K) :
                (n → K) →ₗ[K] n → K) :
              (a : n → K) → n → K)
            v :
          n → K) :
      n → K)
    ((LinearMap.id : (a : n → K) → n → K) v : n → K)

Tactic:
exact (LinearEquiv.ofInjectiveEndo (Matrix.toLin' M) this).apply_symm_apply v

Premises used: Matrix.toLin', LinearEquiv.apply_symm_apply, LinearEquiv.ofInjectiveEndo, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
this :
  Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
⊢ HMul.hMul (β := Matrix n n K) M
      ((toMatrix' : (a : (n → K) →ₗ[K] n → K) → Matrix n n K)
          (↑(LinearEquiv.symm
                (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                  ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this)) :
            (n → K) →ₗ[K] n → K) :
        Matrix n n K) =
    1

Tactic:
have : M * (LinearEquiv.ofInjectiveEndo _ this).symm.toMatrix' = 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
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
this_1 :
  Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
this :
  HMul.hMul (β := Matrix n n K) M
      ((toMatrix' : (a : (n → K) →ₗ[K] n → K) → Matrix n n K)
          (↑(LinearEquiv.symm
                (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                  ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this_1)) :
            (n → K) →ₗ[K] n → K) :
        Matrix n n K) =
    1
⊢ M.det ≠ 0

Tactic:
Matrix.det_ne_zero_of_right_inverse this

Premises used: Matrix.det_ne_zero_of_right_inverse
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
K : Type u_4
inst_1 : DecidableEq n
inst_2 : Field K
M : Matrix n n K
h : ∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0
this_1 :
  Function.Injective (α := n → K) (β := n → K)
    (⇑((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M : (n → K) →ₗ[K] n → K) : (a : n → K) → n → K)
this :
  HMul.hMul (β := Matrix n n K) M
      ((toMatrix' : (a : (n → K) →ₗ[K] n → K) → Matrix n n K)
          (↑(LinearEquiv.symm
                (LinearEquiv.ofInjectiveEndo (K := K) (V := n → K)
                  ((toLin' : (a : Matrix n n K) → (n → K) →ₗ[K] n → K) M) this_1)) :
            (n → K) →ₗ[K] n → K) :
        Matrix n n K) =
    1
⊢ M.det ≠ 0

Tactic:
exact Matrix.det_ne_zero_of_right_inverse this

Premises used: Matrix.det_ne_zero_of_right_inverse
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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
⊢ (∃ (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) ↔
    Eq.{u_5 + 1} (α := K)
      (det.{u_5, u_1} (n := n) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M)) 0

Tactic:
have : (∃ v ≠ 0, (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ _ :=
    exists_mulVec_eq_zero_iff_aux
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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) ↔
    Eq.{u_5 + 1} (α := K)
      (det.{u_5, u_1} (n := n) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M)) 0
⊢ (∃ (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

Tactic:
rw [← RingHom.map_det, IsFractionRing.to_map_eq_zero_iff] at this

Premises used: IsFractionRing.to_map_eq_zero_iff, RingHom.map_det
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A), v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0

Tactic:
Iff.trans ?_ this

Premises used: Iff.trans
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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
refine :
  (∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0) ↔
    ∃ (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
⊢ (∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0

Tactic:
refine Iff.trans ?_ this

Premises used: Iff.trans
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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
mp :
  (∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0) →
    ∃ (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
mpr :
  (∃ (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) →
    ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0
⊢ (∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0) ↔
    ∃ (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

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
⊢ ∃ (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

Tactic:
⟨fun i => algebraMap _ _ (v i), mt (fun h => funext fun i => ?_) hv, ?_⟩

Premises used: Algebra.algebraMap, mt, funext, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
mp : ∀ (h : Eq (α := n → K) (fun (i : n) ↦ (algebraMap A K : (a : A) → K) (v i)) 0) (i : n), v i = 0 i
mp₁ :
  Eq (α := n → K)
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ fun (i : n) ↦
      (algebraMap A K : (a : A) → K) (v i))
    0
⊢ ∃ (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

Tactic:
refine ⟨fun i => algebraMap _ _ (v i), mt (fun h => funext fun i => ?_) hv, ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
h : Eq (α := n → K) (fun (i : n) ↦ (algebraMap A K : (a : A) → K) (v i)) 0
i : n
⊢ v i = 0 i

Tactic:
IsFractionRing.to_map_eq_zero_iff.mp (congr_fun h i)

Premises used: IsFractionRing.to_map_eq_zero_iff, Iff.mp, congr_fun
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
h : Eq (α := n → K) (fun (i : n) ↦ (algebraMap A K : (a : A) → K) (v i)) 0
i : n
⊢ v i = 0 i

Tactic:
exact IsFractionRing.to_map_eq_zero_iff.mp (congr_fun h i)

Premises used: IsFractionRing.to_map_eq_zero_iff, Iff.mp, congr_fun
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
mp :
  ∀ (i : n),
    Eq.{u_5 + 1} (α := K)
      (((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ fun (i : n) ↦
          (algebraMap A K : (a : A) → K) (v i))
        i)
      (0 i)
⊢ Eq (α := n → K)
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ fun (i : n) ↦
      (algebraMap A K : (a : A) → K) (v i))
    0

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
i : n
⊢ Eq.{u_5 + 1} (α := K)
    (((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ fun (i : n) ↦
        (algebraMap A K : (a : A) → K) (v i))
      i)
    (0 i)

Tactic:
(RingHom.map_mulVec _ _ _ i).symm.trans ?_

Premises used: RingHom.map_mulVec, Matrix.map, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
i : n
mp : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ v) i) : K) (0 i : K)
⊢ Eq.{u_5 + 1} (α := K)
    (((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ fun (i : n) ↦
        (algebraMap A K : (a : A) → K) (v i))
      i)
    (0 i)

Tactic:
refine (RingHom.map_mulVec _ _ _ i).symm.trans ?_

Premises used: RingHom.map_mulVec, Eq.symm, Eq.trans
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
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 :
  (∃ (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 → A
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
i : n
mp : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (0 i) : K) (0 i : K)
mp₁ : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) 0 : K) (0 i : K)
mp₂ : Eq.{u_5 + 1} (α := K) 0 (0 i)
mp₃ mp₄ : Eq.{u_5 + 1} (α := K) 0 0
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ v) i) : K) (0 i : K)

Tactic:
rw [mul_eq, Pi.zero_apply, map_zero, Pi.zero_apply]

Premises used: Pi.zero_apply, map_zero