awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
A : Type u_3
inst : Semiring A
simp_rw :
  (∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (Matrix (Fin n) (Fin n) A)) ↔
    ∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (End A (Fin n → A))
⊢ IsStablyFiniteRing A ↔ ∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (End A (Fin n → A))
have simp_rw₁ : (∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (End A (Fin n → A))ᵐᵒᵖ) ↔
  ∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (End A (Fin n → A))
Tactic: simp_rw [isStablyFiniteRing_iff, MulEquivClass.isDedekindFiniteMonoid_iff
    (matrixRingEquivEndVecMulOpposite (ι := Fin _) (A := A)),
    MulOpposite.isDedekindFiniteMonoid_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
inst_1 : DecidableEq ι_1
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
ι : Type u_5
inst_9 : Finite ι
inst_10 : IsStablyFiniteRing A
⊢ IsStablyFiniteRing (End A (ι → A))
have have : ∀ (this : Fintype ι), IsStablyFiniteRing (End A (ι → A))
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
inst_1 : DecidableEq ι_1
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
ι : Type u_5
inst_9 : Finite ι
inst_10 : IsStablyFiniteRing A
this : Fintype ι
⊢ IsStablyFiniteRing (End A (ι → A))
have rw : IsStablyFiniteRing (Matrix ι ι A)
Tactic: rw [← MulOpposite.isStablyFiniteRing_iff,
    ← RingEquiv.isStablyFiniteRing_iff (matrixRingEquivEndVecMulOpposite (ι := ι) (A := A))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
ι_1 : Type u_1
inst : Fintype ι_1
inst_1 : DecidableEq ι_1
R : Type u_2
inst_2 : CommSemiring R
A : Type u_3
inst_3 : Semiring A
inst_4 : Algebra R A
M : Type u_4
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : Module A M
inst_8 : IsScalarTower R A M
ι : Type u_5
inst_9 : Finite ι
inst_10 : IsStablyFiniteRing A
this : Fintype ι
⊢ IsStablyFiniteRing (End A (ι → A))
have classical : IsStablyFiniteRing (Matrix ι ι A)
Tactic: classical rw [← MulOpposite.isStablyFiniteRing_iff,
    ← RingEquiv.isStablyFiniteRing_iff (matrixRingEquivEndVecMulOpposite (ι := ι) (A := A))]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
A : Type u_3
inst : Semiring A
⊢ IsStablyFiniteRing A ↔
    ∀ (n : ℕ) (f : End A (Fin n → A)),
      Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A) →
        Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
have simp_rw : (∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1) ↔
  ∀ (n : ℕ) (f : End A (Fin n → A)),
    Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A) →
      Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
Tactic: simp_rw [isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd, isDedekindFiniteMonoid_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
A : Type u_3
inst : Semiring A
⊢ (∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1) ↔
    ∀ (n : ℕ) (f : End A (Fin n → A)),
      Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A) →
        Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
have refine_1 : ∀ (h : ∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1) (n : ℕ) (f : End A (Fin n → A))
  (surj : Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)),
  Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
Tactic: refine ⟨fun h n f surj ↦ ?_, fun h n f g eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
A : Type u_3
inst : Semiring A
refine_1 :
  ∀ (h : ∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1) (n : ℕ) (f : End A (Fin n → A))
    (surj : Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)),
    Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
⊢ (∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1) ↔
    ∀ (n : ℕ) (f : End A (Fin n → A)),
      Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A) →
        Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
have refine_2 : ∀
  (h :
    ∀ (n : ℕ) (f : End A (Fin n → A)),
      Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A) →
        Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A))
  (n : ℕ) (f g : End A (Fin n → A)) (eq : f * g = 1), g * f = 1
Tactic: refine ⟨fun h n f surj ↦ ?_, fun h n f g eq ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
A : Type u_3
inst : Semiring A
h : ∀ (n : ℕ) {a b : End A (Fin n → A)}, a * b = 1 → b * a = 1
n : ℕ
f : End A (Fin n → A)
surj : Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
⊢ Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
have refine_1 : ∀ (g : (Fin n → A) →ₗ[A] Fin n → A) (eq : f ∘ₗ g = LinearMap.id),
  Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
Tactic: have ⟨g, eq⟩ := Module.projective_lifting_property _ .id surj
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (hypothesis)
Goal:
A : Type u_3
inst : Semiring A
h :
  ∀ (n : ℕ) (f : End A (Fin n → A)),
    Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A) →
      Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
⊢ g * f = 1
have surj : Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
Tactic: have surj := surjective_of_comp_eq_id _ _ eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (hypothesis)
Goal:
A : Type u_3
inst : Semiring A
h :
  ∀ (n : ℕ) (f : End A (Fin n → A)),
    Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A) →
      Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
surj : Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
⊢ g * f = 1
have this : (↑(LinearEquiv.symm (LinearEquiv.ofBijective f sorry)) : (Fin n → A) →ₗ[A] Fin n → A) ∘ₗ
    (↑(LinearEquiv.ofBijective f sorry) : (Fin n → A) →ₗ[A] Fin n → A) =
  LinearMap.id
Tactic: have := (LinearEquiv.ofBijective f ⟨h _ _ surj, surj⟩).symm_comp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLin (goal)
Goal:
A : Type u_3
inst : Semiring A
h :
  ∀ (n : ℕ) (f : End A (Fin n → A)),
    Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A) →
      Injective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
n : ℕ
f g : End A (Fin n → A)
eq : f * g = 1
surj : Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)
this :
  (↑(LinearEquiv.symm (LinearEquiv.ofBijective f ⋯)) : (Fin n → A) →ₗ[A] Fin n → A) ∘ₗ
      (↑(LinearEquiv.ofBijective f ⋯) : (Fin n → A) →ₗ[A] Fin n → A) =
    LinearMap.id
⊢ g * f = 1
have refine_2 : (↑(LinearEquiv.symm (LinearEquiv.ofBijective f sorry)) : (Fin n → A) →ₗ[A] Fin n → A) * f = 1
Tactic: rwa [← left_inv_eq_right_inv this eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (((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
have 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
Tactic: simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.nonsing_inv_mul _ hA,
      toLin_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (((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
have simp_rw₁ : (((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (A⁻¹ * A) : M →ₗ[R] M) : (a : M) → M) x = x
Tactic: simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.nonsing_inv_mul _ hA,
      toLin_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (((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
have simp_rw₂ : ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) 1 : (a : M) → M) x = x
Tactic: simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.nonsing_inv_mul _ hA,
      toLin_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (((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
have simp_rw₃ : (LinearMap.id : (a : M) → M) x = x
Tactic: simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.nonsing_inv_mul _ hA,
      toLin_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (((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
have 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
Tactic: simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.mul_nonsing_inv _ hA,
      toLin_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (((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
have simp_rw₁ : (((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) (A * A⁻¹) : M →ₗ[R] M) : (a : M) → M) x = x
Tactic: simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.mul_nonsing_inv _ hA,
      toLin_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (((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
have simp_rw₂ : ((toLin b b : (a : Matrix n n R) → M →ₗ[R] M) 1 : (a : M) → M) x = x
Tactic: simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.mul_nonsing_inv _ hA,
      toLin_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (((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
have simp_rw₃ : (LinearMap.id : (a : M) → M) x = x
Tactic: simp_rw [← LinearMap.comp_apply, ← Matrix.toLin_mul b b b, Matrix.mul_nonsing_inv _ hA,
      toLin_one, LinearMap.id_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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), v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0
have mp : (∃ (v : n → K), v ≠ 0 ∧ M *ᵥ v = 0) → M.det = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ (∃ (v : n → K), v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0
have mpr : M.det = 0 → ∃ (v : n → K), v ≠ 0 ∧ M *ᵥ v = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ M.det = 0
have mp : ∀ (hv : M.det ≠ 0), v = 0
Tactic: contrapose! hv
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
⊢ M.det = 0 → ∃ (v : n → K), v ≠ 0 ∧ M *ᵥ v = 0
have mpr : (∀ (v : n → K) (_ : v ≠ 0), M *ᵥ v ≠ 0) → M.det ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (hypothesis)
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
⊢ M.det ≠ 0
have 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)
Tactic: have : Function.Injective (Matrix.toLin' M) := by
      simpa only [← LinearMap.ker_eq_bot, ker_toLin'_eq_bot_iff, not_imp_not] using h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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
have 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)
Tactic: refine Matrix.toLin'.injective (LinearMap.ext fun v => ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
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)
              (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)
have 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)
Tactic: rw [Matrix.toLin'_mul, Matrix.toLin'_one, Matrix.toLin'_toMatrix', LinearMap.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (hypothesis)
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)
⊢ M.det ≠ 0
have 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)) :
          (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (hypothesis)
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 → A), v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0
have 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
Tactic: have : (∃ v ≠ 0, (algebraMap A K).mapMatrix M *ᵥ v = 0) ↔ _ :=
    exists_mulVec_eq_zero_iff_aux
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (hypothesis)
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 → A), v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0
have 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
Tactic: rw [← RingHom.map_det, IsFractionRing.to_map_eq_zero_iff] at this
Cleared hypotheses: this
-- 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 :
  (∃ (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
have 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
Tactic: refine Iff.trans ?_ this
-- 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 :
  (∃ (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) ↔
    ∃ (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
have 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
Tactic: constructor