awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
f g : End A (ι → M)
a :
  ∀ (i j : ι) (x : M),
    Eq (α := M)
      (({ toFun := fun (x : M) ↦ (f * g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
              map_smul' := ⋯ } :
            (a : M) → M)
          x :
        M)
      ((HMul.hMul (α := Matrix.{u_1, u_1, u_4} ι ι (End A M)) (β := Matrix.{u_1, u_1, u_4} ι ι (End A M))
              (fun (i j : ι) ↦
                { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                  map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
              (fun (i j : ι) ↦
                { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                  map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
              i j :
            (a : M) → M)
          x :
        M)
⊢ (fun (i j : ι) ↦
      { toFun := fun (x : M) ↦ (f * g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
        map_smul' := ⋯ }) =
    HMul.hMul (α := Matrix.{u_1, u_1, u_4} ι ι (End A M))
      (fun (i j : ι) ↦
        { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
          map_smul' := ⋯ : M →ₗ[A] M })
      fun (i j : ι) ↦
      { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
        map_smul' := ⋯ : M →ₗ[A] M }

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
f g : End A (ι → M)
i j : ι
x : M
a :
  Eq.{u_4 + 1} (α := M)
    ((f : (a : ι → M) → ι → M) ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) : ι → M) i : M)
    (∑ x_1 : ι,
        (f : (a : ι → M) → ι → M)
          (Pi.single (M := fun (a : ι) ↦ M) x_1 ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) x_1))
          i :
      M)
⊢ Eq (α := M)
    (({ toFun := fun (x : M) ↦ (f * g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
            map_smul' := ⋯ } :
          (a : M) → M)
        x :
      M)
    ((HMul.hMul (α := Matrix.{u_1, u_1, u_4} ι ι (End A M)) (β := Matrix.{u_1, u_1, u_4} ι ι (End A M))
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
            i j :
          (a : M) → M)
        x :
      M)

Tactic:
simp only [Module.End.mul_apply, LinearMap.coe_mk, AddHom.coe_mk, Matrix.mul_apply,
      LinearMap.coe_sum, Finset.sum_apply]

Premises used: LinearMap.coe_mk, Finset.sum_apply, Matrix.mul_apply, LinearMap.coe_sum, Module.End.mul_apply, AddHom.coe_mk
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
f g : End A (ι → M)
i j : ι
x : M
a :
  Eq.{u_4 + 1} (α := M)
    ((f : (a : ι → M) → ι → M) ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) : ι → M) i : M)
    ((f : (a : ι → M) → (a : ι) → M)
        (∑ x_1 : ι,
          Pi.single (M := fun (a : ι) ↦ M) x_1 ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) x_1))
        i :
      M)
⊢ Eq.{u_4 + 1} (α := M)
    ((f : (a : ι → M) → ι → M) ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) : ι → M) i : M)
    (∑ x_1 : ι,
        (f : (a : ι → M) → ι → M)
          (Pi.single (M := fun (a : ι) ↦ M) x_1 ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) x_1))
          i :
      M)

Tactic:
rw [← Fintype.sum_apply, ← map_sum]

Premises used: map_sum, Fintype.sum_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
f g : End A (ι → M)
i j : ι
x : M
⊢ Eq (α := ι → M) ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) : ι → M)
    (∑ x_1 : ι,
        Pi.single (M := fun (a : ι) ↦ M) x_1 ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) x_1) :
      ι → M)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
f g : End A (ι → M)
i j : ι
x : M
⊢ Eq.{u_4 + 1} (α := M)
    ((f : (a : ι → M) → ι → M) ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) : ι → M) i : M)
    ((f : (a : ι → M) → (a : ι) → M)
        (∑ x_1 : ι,
          Pi.single (M := fun (a : ι) ↦ M) x_1 ((g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) x_1))
        i :
      M)

Tactic:
exact congr_arg₂ _ (by aesop) rfl

Premises used: rfl, congr_arg₂
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
f g : End A (ι → M)
a :
  ∀ (i j : ι) (x : M),
    Eq (α := M)
      (({ toFun := fun (x : M) ↦ (f + g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
              map_smul' := ⋯ } :
            (a : M) → M)
          x :
        M)
      ((HAdd.hAdd (α := Matrix.{u_1, u_1, u_4} ι ι (End A M)) (β := Matrix.{u_1, u_1, u_4} ι ι (End A M))
              (fun (i j : ι) ↦
                { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                  map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
              (fun (i j : ι) ↦
                { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                  map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
              i j :
            (a : M) → M)
          x :
        M)
⊢ (fun (i j : ι) ↦
      { toFun := fun (x : M) ↦ (f + g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
        map_smul' := ⋯ }) =
    HAdd.hAdd (α := Matrix.{u_1, u_1, u_4} ι ι (End A M))
      (fun (i j : ι) ↦
        { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
          map_smul' := ⋯ : M →ₗ[A] M })
      fun (i j : ι) ↦
      { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
        map_smul' := ⋯ : M →ₗ[A] M }

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
f g : End A (ι → M)
i j : ι
x : M
⊢ Eq (α := M)
    (({ toFun := fun (x : M) ↦ (f + g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i, map_add' := ⋯,
            map_smul' := ⋯ } :
          (a : M) → M)
        x :
      M)
    ((HAdd.hAdd (α := Matrix.{u_1, u_1, u_4} ι ι (End A M)) (β := Matrix.{u_1, u_1, u_4} ι ι (End A M))
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (f : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
            (fun (i j : ι) ↦
              { toFun := fun (x : M) ↦ (g : (a : ι → M) → ι → M) (Pi.single (M := fun (a : ι) ↦ M) j x) i,
                map_add' := ⋯, map_smul' := ⋯ : M →ₗ[A] M })
            i j :
          (a : M) → M)
        x :
      M)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
r : R
a :
  ∀ (i j : ι) (x : M),
    Eq (α := M)
      ((Equiv.toFun (RingEquiv.toEquiv (endVecRingEquivMatrixEnd ι A M))
              ((algebraMap R (End A (ι → M)) : (a : R) → End A (ι → M)) r) i j :
            (a : M) → M)
          x :
        M)
      ((((algebraMap R (Matrix.{u_1, u_1, u_4} ι ι (End A M)) : (a : R) → Matrix ι ι (End A M)) r i j : End A M) :
            (a : M) → M)
          x :
        M)
⊢ Eq (α := Matrix.{u_1, u_1, u_4} ι ι (End A M))
    (Equiv.toFun (RingEquiv.toEquiv (endVecRingEquivMatrixEnd ι A M))
      ((algebraMap R (End A (ι → M)) : (a : R) → End A (ι → M)) r))
    ((algebraMap R (Matrix.{u_1, u_1, u_4} ι ι (End A M)) : (a : R) → Matrix ι ι (End A M)) r)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
r : R
i j : ι
x : M
a : (if i = j then r • x else 0) = (if i = j then HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id else 0 : (a : M) → M) x
⊢ Eq (α := M)
    ((Equiv.toFun (RingEquiv.toEquiv (endVecRingEquivMatrixEnd ι A M))
            ((algebraMap R (End A (ι → M)) : (a : R) → End A (ι → M)) r) i j :
          (a : M) → M)
        x :
      M)
    ((((algebraMap R (Matrix.{u_1, u_1, u_4} ι ι (End A M)) : (a : R) → Matrix ι ι (End A M)) r i j : End A M) :
          (a : M) → M)
        x :
      M)

Tactic:
simp only [endVecRingEquivMatrixEnd, RingEquiv.toEquiv_eq_coe, Module.algebraMap_end_eq_smul_id,
      Equiv.toFun_as_coe, EquivLike.coe_coe, RingEquiv.coe_mk, Equiv.coe_fn_mk,
      LinearMap.smul_apply, id_coe, id_eq, Pi.smul_apply, Pi.single_apply, smul_ite, smul_zero,
      LinearMap.coe_mk, AddHom.coe_mk, algebraMap_matrix_apply]

Premises used: LinearMap.coe_mk, endVecRingEquivMatrixEnd, LinearMap.smul_apply, Equiv.toFun_as_coe, LinearMap.id_coe, Pi.single_apply, smul_zero, RingEquiv.coe_mk, Module.algebraMap_end_eq_smul_id, smul_ite, RingEquiv.toEquiv_eq_coe, Equiv.coe_fn_mk, AddHom.coe_mk, EquivLike.coe_coe, Matrix.algebraMap_matrix_apply, id_eq, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
r : R
i j : ι
x : M
pos : i = j → r • x = (HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id : (a : M) → M) x
neg : ¬i = j → Eq (α := M) (0 : M) ((0 : (a : M) → M) x : M)
⊢ (if i = j then r • x else 0) = (if i = j then HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id else 0 : (a : M) → M) x

Tactic:
split_ifs
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
r : R
i j : ι
x : M
h : i = j
⊢ r • x = (HSMul.hSMul (β := M →ₗ[A] M) r LinearMap.id : (a : M) → M) x

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
ι : Type u_1
inst : Fintype ι
inst_1 : DecidableEq ι
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
r : R
i j : ι
x : M
h : ¬i = j
⊢ Eq (α := M) (0 : M) ((0 : (a : M) → M) x : M)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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))
simp_rw₁ :
  (∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (End A (Fin n → A))ᵐᵒᵖ) ↔
    ∀ (n : ℕ), IsDedekindFiniteMonoid.{u_3} (End A (Fin n → A))
⊢ IsStablyFiniteRing 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]

Premises used: matrixRingEquivEndVecMulOpposite, MulEquivClass.isDedekindFiniteMonoid_iff, isStablyFiniteRing_iff, MulOpposite.isDedekindFiniteMonoid_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
have : ∀ (this : Fintype ι), IsStablyFiniteRing (End A (ι → A))
⊢ IsStablyFiniteRing (End A (ι → A))

Tactic:
have := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 ι
rw : IsStablyFiniteRing (Matrix ι ι A)
⊢ IsStablyFiniteRing (End A (ι → A))

Tactic:
rw [← MulOpposite.isStablyFiniteRing_iff,
    ← RingEquiv.isStablyFiniteRing_iff (matrixRingEquivEndVecMulOpposite (ι := ι) (A := A))]

Premises used: matrixRingEquivEndVecMulOpposite, RingEquiv.isStablyFiniteRing_iff, MulOpposite.isStablyFiniteRing_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 ι
classical : IsStablyFiniteRing (Matrix ι ι A)
⊢ IsStablyFiniteRing (End A (ι → A))

Tactic:
classical rw [← MulOpposite.isStablyFiniteRing_iff,
    ← RingEquiv.isStablyFiniteRing_iff (matrixRingEquivEndVecMulOpposite (ι := ι) (A := A))]

Premises used: MulOpposite.isStablyFiniteRing_iff
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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 (Matrix ι ι A)

Tactic:
infer_instance
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
A : Type u_3
inst : Semiring A
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)
⊢ 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)

Tactic:
simp_rw [isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd, isDedekindFiniteMonoid_iff]

Premises used: isDedekindFiniteMonoid_iff, isStablyFiniteRing_iff_isDedekindFiniteMonoid_moduleEnd
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)

Tactic:
⟨fun h n f surj ↦ ?_, fun h n f g eq ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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
⊢ (∀ (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:
refine ⟨fun h n f surj ↦ ?_, fun h n f g eq ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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)
⊢ 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
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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:
injective_of_comp_eq_id _ _ (h _ eq)

Premises used: LinearMap.injective_of_comp_eq_id
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
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:
exact injective_of_comp_eq_id _ _ (h _ eq)

Premises used: LinearMap.injective_of_comp_eq_id
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
⊢ Surjective (α := Fin n → A) (β := Fin n → A) (⇑f : (a : Fin n → A) → Fin n → A)

Tactic:
have surj := surjective_of_comp_eq_id _ _ eq
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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)
⊢ (↑(LinearEquiv.symm (LinearEquiv.ofBijective f ⋯)) : (Fin n → A) →ₗ[A] Fin n → A) ∘ₗ
      (↑(LinearEquiv.ofBijective f ⋯) : (Fin n → A) →ₗ[A] Fin n → A) =
    LinearMap.id

Tactic:
have := (LinearEquiv.ofBijective f ⟨h _ _ surj, surj⟩).symm_comp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
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
refine_2 refine_2₁ refine_2₂ refine_2₃ :
  (↑(LinearEquiv.symm (LinearEquiv.ofBijective f ⋯)) : (Fin n → A) →ₗ[A] Fin n → A) * f = 1
⊢ g * f = 1

Tactic:
rwa [← left_inv_eq_right_inv this eq]

Premises used: left_inv_eq_right_inv
-- Module: Mathlib.LinearAlgebra.Matrix.ToLin
Goal:
A : Type u_3
inst : Semiring A
inst_1 : IsStablyFiniteRing A
n : ℕ
f : End A (Fin n → A)
hf : 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:
isStablyFiniteRing_iff_injective_of_surjective.mp ‹_› n f hf

Premises used: isStablyFiniteRing_iff_injective_of_surjective, Iff.mp
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
R : Type u_2
inst_1 : CommRing R
inst_2 : DecidableEq n
P : Matrix n n R
h : Invertible P
⊢ (↑(P.toLinearEquiv' h) : (n → R) →ₗ[R] n → R) = (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) P

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.ToLinearEquiv
Goal:
n : Type u_1
inst : Fintype n
R : Type u_2
inst_1 : CommRing R
inst_2 : DecidableEq n
P : Matrix n n R
h : Invertible P
⊢ (↑(P.toLinearEquiv' h).symm : (n → R) →ₗ[R] n → R) =
    (toLin' : (a : Matrix n n R) → (n → R) →ₗ[R] n → R) (@Invertible.invOf _ instMulOfFintypeOfAddCommMonoid one P _)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Matrix.mulVec, Finset.sum, rfl
-- 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.nonsing_inv_mul _ hA,
      toLin_one, LinearMap.id_apply]

Premises used: LinearMap.id_apply, LinearMap.comp_apply, Matrix.nonsing_inv_mul, Matrix.toLin_mul, Matrix.toLin_one