awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_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
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
⊢ ∃ (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)

Premises used: Finset.univ, nonZeroDivisors, IsLocalization.exist_integer_multiples_of_finset, Finset.image
-- 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_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)
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
⊢ ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
choose f hf using ba_eq
-- 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_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

Tactic:
⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩),
        mt (fun h => funext fun i => ?_) hv, ?_⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, mt, funext, And.intro, Exists.intro, rfl
-- 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_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
mpr₁ : (M *ᵥ fun (i : n) ↦ f (v i) ⋯) = 0
⊢ ∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0

Tactic:
refine
      ⟨fun i => f _ (Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩),
        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_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
⊢ Eq.{u_5 + 1} (α := K) ((algebraMap A K : (a : A) → K) (f (v i) ⋯) : K) ((algebraMap A K : (a : A) → K) (0 i) : K)

Tactic:
have := congr_arg (algebraMap A K) (congr_fun h 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_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)
⊢ 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

Premises used: Subtype.coe_mk, Pi.zero_apply, map_zero, IsFractionRing.to_map_eq_zero_iff, mul_eq_zero, Algebra.smul_def
-- 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_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 : b = 0 ∨ v i = 0
⊢ v i = 0 i

Tactic:
this.resolve_left (nonZeroDivisors.ne_zero hb)

Premises used: Or.resolve_left, nonZeroDivisors.ne_zero
-- 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_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 : b = 0 ∨ v i = 0
⊢ v i = 0 i

Tactic:
exact this.resolve_left (nonZeroDivisors.ne_zero hb)

Premises used: Or.resolve_left, nonZeroDivisors.ne_zero
-- 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_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 : ∀ (i : n), (M *ᵥ fun (i : n) ↦ f (v i) ⋯) i = 0 i
⊢ (M *ᵥ fun (i : n) ↦ f (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_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

Tactic:
IsFractionRing.injective A K ?_

Premises used: IsFractionRing.injective
-- 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_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 :
  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)
⊢ (M *ᵥ fun (i : n) ↦ f (v i) ⋯) i = 0 i

Tactic:
refine IsFractionRing.injective A K ?_

Premises used: IsFractionRing.injective
-- 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_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

Tactic:
?_
-- 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_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
⊢ ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i =
    0

Tactic:
?_
-- 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_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) (0 : K) ((algebraMap A K : (a : A) → K) 0 : K)

Tactic:
(map_zero _).symm

Premises used: map_zero, Eq.symm
-- 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_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
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
⊢ 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)

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

Premises used: Algebra.algebraMap, map_zero, RingHom.mapMatrix, HSMul.hSMul, OfNat.ofNat, Eq.symm, Matrix.mulVec, 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_1 :
  (∃ (v : n → K),
      v ≠ 0 ∧ Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0) ↔
    M.det = 0
v : n → K
hv : v ≠ 0
mul_eq : Eq (α := n → K) ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) 0
this : DecidableEq K := Classical.decEq K
b : A
hb : Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) b
f : (a : K) → a ∈ Finset.image v Finset.univ → A
hf :
  ∀ (a : K) (a_1 : a ∈ Finset.image v Finset.univ),
    (algebraMap A K : (a : A) → K) (f a a_1) =
      (↑(Subtype.mk (p := fun (x : A) ↦ Membership.mem (γ := Submonoid A) (nonZeroDivisors A : Submonoid A) x) b hb) :
          A) •
        a
i : n
mpr :
  HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K)
      ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ v) i =
    0
mpr₁ : HSMul.hSMul (α := K) (β := n → K) ((algebraMap A K : (a : A) → K) b : K) 0 i = 0
mpr₂ : HSMul.hSMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) (0 i) = 0
mpr₃ : HSMul.hSMul (α := K) (β := K) ((algebraMap A K : (a : A) → K) b : K) 0 = 0
mpr₄ mpr₅ : Eq.{u_5 + 1} (α := K) 0 0
⊢ ((RingHom.mapMatrix (algebraMap A K) : (a : Matrix n n A) → Matrix n n K) M *ᵥ
        HSMul.hSMul (α := K) ((algebraMap A K : (a : A) → K) b : K) v)
      i =
    0

Tactic:
rw [mulVec_smul, mul_eq, Pi.smul_apply, Pi.zero_apply, smul_zero]

Premises used: smul_zero, Pi.zero_apply, Matrix.mulVec_smul, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ (∃ (v : n → A), v ≠ 0 ∧ M *ᵥ v = 0) ↔ M.det = 0

Tactic:
exists_mulVec_eq_zero_iff' (FractionRing A)

Premises used: FractionRing, _private.0.Matrix.exists_mulVec_eq_zero_iff'
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ (∃ (v : n → A), v ≠ 0 ∧ v ᵥ* M = 0) ↔ M.det = 0

Tactic:
simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff

Premises used: Matrix.mulVec_transpose, Matrix.det_transpose, Matrix.exists_mulVec_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ M.Nondegenerate ↔ M.det ≠ 0

Tactic:
⟨?_, nondegenerate_of_det_ne_zero⟩

Premises used: Matrix.nondegenerate_of_det_ne_zero, Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
refine : M.Nondegenerate → M.det ≠ 0
⊢ M.Nondegenerate ↔ M.det ≠ 0

Tactic:
refine ⟨?_, nondegenerate_of_det_ne_zero⟩
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
rw : M.Nondegenerate → ¬∃ (v : n → A), v ≠ 0 ∧ v ᵥ* M = 0
⊢ M.Nondegenerate → M.det ≠ 0

Tactic:
rw [ne_eq, ← exists_vecMul_eq_zero_iff]

Premises used: ne_eq, Matrix.exists_vecMul_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
push : M.Nondegenerate → ∀ (v : n → A) (_ : v ≠ 0), v ᵥ* M ≠ 0
⊢ M.Nondegenerate → ¬∃ (v : n → A), v ≠ 0 ∧ v ᵥ* M = 0

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
hM : M.Nondegenerate
v : n → A
hv : v ≠ 0
hMv : v ᵥ* M = 0
obtain : ∀ (w : n → A) (hwMv : v ⬝ᵥ M *ᵥ w ≠ 0), False
⊢ False

Tactic:
obtain ⟨w, hwMv⟩ := hM.exists_not_ortho_of_ne_zero hv

Premises used: Matrix.Nondegenerate.exists_not_ortho_of_ne_zero
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
hM : M.Nondegenerate
v : n → A
hv : v ≠ 0
hMv : v ᵥ* M = 0
w : n → A
hwMv : v ⬝ᵥ M *ᵥ w ≠ 0
⊢ False

Tactic:
simp [dotProduct_mulVec, hMv, zero_dotProduct, ne_eq] at hwMv

Premises used: zero_dotProduct, ne_eq, Matrix.dotProduct_mulVec
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
⊢ M.SeparatingLeft ↔ M.det ≠ 0

Tactic:
⟨fun h hc ↦ ?_, fun h ↦ (nondegenerate_of_det_ne_zero h).1⟩

Premises used: Matrix.nondegenerate_of_det_ne_zero, Iff.intro, Matrix.Nondegenerate.separatingLeft
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
A : Type u_4
inst_1 : DecidableEq n
inst_2 : CommRing A
inst_3 : IsDomain A
M : Matrix n n A
refine : ∀ (h : M.SeparatingLeft) (hc : M.det = 0), False
⊢ M.SeparatingLeft ↔ M.det ≠ 0

Tactic:
refine ⟨fun h hc ↦ ?_, fun h ↦ (nondegenerate_of_det_ne_zero h).1⟩