awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this :
  (∃ (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
⊢ (∃ (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 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
Tactic: constructor
-- 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
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
have mp : ∀ (h : Eq (α := n → K) (fun (i : n) ↦ (algebraMap A K : (a : A) → K) (v i)) 0) (i : n), v i = 0 i
Tactic: refine ⟨fun i => algebraMap _ _ (v i), mt (fun h => funext fun i => ?_) hv, ?_⟩
-- 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
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
⊢ ∃ (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₁ : 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: refine ⟨fun i => algebraMap _ _ (v i), mt (fun h => funext fun i => ?_) hv, ?_⟩
-- 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
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
⊢ 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
have 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)
Tactic: ext i
-- 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
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)
have mp : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ v) i) : K) (0 i : K)
Tactic: refine (RingHom.map_mulVec _ _ _ i).symm.trans ?_
-- 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
hv : v ≠ 0
mul_eq : M *ᵥ v = 0
i : n
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ v) i) : K) (0 i : K)
have mp : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (0 i) : K) (0 i : K)
Tactic: rw [mul_eq, Pi.zero_apply, map_zero, Pi.zero_apply]
-- 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
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)
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ v) i) : K) (0 i : K)
have mp₁ : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) 0 : K) (0 i : K)
Tactic: rw [mul_eq, Pi.zero_apply, map_zero, Pi.zero_apply]
-- 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
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)
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ v) i) : K) (0 i : K)
have mp₂ : Eq.{u_5 + 1} (α := K) 0 (0 i)
Tactic: rw [mul_eq, Pi.zero_apply, map_zero, Pi.zero_apply]
-- 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
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)
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ v) i) : K) (0 i : K)
have mp₃ : Eq.{u_5 + 1} (α := K) 0 0
Tactic: rw [mul_eq, Pi.zero_apply, map_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
⊢ ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0
have mpr : ∀ (b : A) (hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b)
  (ba_eq :
    ∀ a ∈ Finset.image v Finset.univ,
      IsLocalization.IsInteger A
        ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b
                hb) :
            A) •
          a)),
  ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0
Tactic: obtain ⟨⟨b, hb⟩, ba_eq⟩ :=
      IsLocalization.exist_integer_multiples_of_finset (nonZeroDivisors A) (Finset.univ.image v)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
ba_eq :
  ∀ a ∈ Finset.image v Finset.univ,
    IsLocalization.IsInteger A
      ((↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a)
⊢ ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0
have mpr : ∀ (f : (a : K) → a ∈ Finset.image v Finset.univ → A)
  (hf :
    ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
      (algebraMap A K : (a : A) → K) (f a a_1) =
        (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
            A) •
          a),
  ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0
Tactic: choose f hf using ba_eq
Cleared hypotheses: ba_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
⊢ ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0
have mpr : ∀ (h : Eq (α := n → A) (fun (i : n) ↦ f (v i) sorry) 0) (i : n), v i = 0 i
Tactic: refine
      ⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩),
        mt (fun h => funext fun i => ?_) hv, ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
mpr : ∀ (h : Eq (α := n → A) (fun (i : n) ↦ f (v i) ⋯) 0) (i : n), v i = 0 i
⊢ ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0
have mpr₁ : (M *ᵥ fun (i : n) ↦ f (v i) sorry) = 0
Tactic: refine
      ⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩),
        mt (fun h => funext fun i => ?_) hv, ?_⟩
-- 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_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
h : Eq (α := n → A) (fun (i : n) ↦ f (v i) ⋯) 0
i : n
⊢ v i = 0 i
have this₁ : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (f (v i) sorry) : K) ((algebraMap A K : (a : A) → K) (0 i) : K)
Tactic: have := congr_arg (algebraMap A K) (congr_fun h i)
-- 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_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this_2 : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
h : Eq (α := n → A) (fun (i : n) ↦ f (v i) ⋯) 0
i : n
this : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (f (v i) ⋯) : K) ((algebraMap A K : (a : A) → K) (0 i) : K)
⊢ v i = 0 i
have this₁ : b = 0 ∨ v i = 0
Tactic: rw [hf, Subtype.coe_mk, Pi.zero_apply, map_zero, Algebra.smul_def, mul_eq_zero,
        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_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
⊢ (M *ᵥ fun (i : n) ↦ f (v i) ⋯) = 0
have mpr : ∀ (i : n), (M *ᵥ fun (i : n) ↦ f (v i) sorry) i = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
⊢ (M *ᵥ fun (i : n) ↦ f (v i) ⋯) i = 0 i
have mpr : Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) sorry) i) : K)
  ((algebraMap A K : (a : A) → K) (0 i) : K)
Tactic: refine IsFractionRing.injective A K ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) ⋯) i) : K)
    ((algebraMap A K : (a : A) → K) (0 i) : K)
have mpr : (algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) sorry) i) =
  ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
      HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
    i
Tactic: calc
        algebraMap A K ((M *ᵥ (fun i : n => f (v i) _)) i) =
            ((algebraMap A K).mapMatrix M *ᵥ algebraMap _ K b • v) i := ?_
        _ = 0 := ?_
        _ = algebraMap A K 0 := (map_zero _).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  (algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) ⋯) i) =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) ⋯) i) : K)
    ((algebraMap A K : (a : A) → K) (0 i) : K)
have mpr₁ : ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
      HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
    i =
  0
Tactic: calc
        algebraMap A K ((M *ᵥ (fun i : n => f (v i) _)) i) =
            ((algebraMap A K).mapMatrix M *ᵥ algebraMap _ K b • v) i := ?_
        _ = 0 := ?_
        _ = algebraMap A K 0 := (map_zero _).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.ToLinearEquiv (goal)
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
K : Type u_5
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : Nontrivial A
inst_4 : Field K
inst_5 : Algebra A K
inst_6 : IsFractionRing A K
M : Matrix n n A
this_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
⊢ (algebraMap A K : (a : A) → K) ((M *ᵥ fun (i : n) ↦ f (v i) ⋯) i) =
    ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i
have mpr : (M.map (⇑(algebraMap A K) : (a : A) → K) *ᵥ
      Function.comp.{u_1 + 1, u_4 + 1, u_5 + 1} (β := A) (⇑(algebraMap A K) : (a : A) → K) fun (i : n) ↦ f (v i) sorry)
    i =
  ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
      HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
    i
Tactic: simp_rw [RingHom.map_mulVec, mulVec, dotProduct, Function.comp_apply, hf,
          RingHom.mapMatrix_apply, Pi.smul_apply, smul_eq_mul, Algebra.smul_def]