awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
S : ι → Type u_3
inst : (i : ι) → CommSemiring (R i)
inst_1 : (i : ι) → CommSemiring (S i)
inst_2 : (i : ι) → Algebra.{u_2, u_3} (R i) (S i)
M : Submonoid ((i : ι) → R i)
inst_3 :
  ∀ (i : ι), IsLocalization.{u_2, u_3} (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) (S i)
inst_4 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_5 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
i : ι
h₀ : 0 ∉ Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M
⊢ Surjective.{u_2 + 1, u_3 + 1} (α := R i) (β := S i) (↑(↑(algebraMap (R i) (S i)) : R i →* S i) : OneHom (R i) (S i)).1

Tactic:
exact (IsLocalization.atUnits _ _ (by simpa)).surjective

Premises used: IsLocalization.atUnits, AlgEquiv.surjective
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_4 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
inst_5 : IsLocalization (R := (i : ι) → R i) M S'
inst_6 : Finite ι
s : S'
S : (i : ι) → Type u_2 :=
  fun (i : ι) ↦ Localization (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M)
obtain :
  ∀ (r : (i : ι) → R i)
    (hr :
      Eq (α := (i : ι) → S i)
        ((Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i) :
              (a : (i : ι) → R i) → (i : ι) → S i)
            r :
          (i : ι) → S i)
        ((lift (R := (i : ι) → R i) (M := M) (g :=
                Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
              (a : S') → (i : ι) → S i)
            s :
          (i : ι) → S i)),
    ∃ (a : (i : ι) → R i), (algebraMap ((i : ι) → R i) S' : (a : (i : ι) → R i) → S') a = s
⊢ ∃ (a : (i : ι) → R i), (algebraMap ((i : ι) → R i) S' : (a : (i : ι) → R i) → S') a = s

Tactic:
obtain ⟨r, hr⟩ :=
    surjective_piRingHom_algebraMap_comp_piEvalRingHom
    S M ((lift (isUnit_piRingHom_algebraMap_comp_piEvalRingHom R S M)) s)

Premises used: IsLocalization.isUnit_piRingHom_algebraMap_comp_piEvalRingHom, IsLocalization.lift, IsLocalization.surjective_piRingHom_algebraMap_comp_piEvalRingHom, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_4 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
inst_5 : IsLocalization (R := (i : ι) → R i) M S'
inst_6 : Finite ι
s : S'
S : (i : ι) → Type u_2 :=
  fun (i : ι) ↦ Localization (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M)
r : (i : ι) → R i
hr :
  Eq (α := (i : ι) → S i)
    ((Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i) :
          (a : (i : ι) → R i) → (i : ι) → S i)
        r :
      (i : ι) → S i)
    ((lift (R := (i : ι) → R i) (M := M) (g :=
            Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
          (a : S') → (i : ι) → S i)
        s :
      (i : ι) → S i)
⊢ ∃ (a : (i : ι) → R i), (algebraMap ((i : ι) → R i) S' : (a : (i : ι) → R i) → S') a = s

Tactic:
⟨r, (bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom R S _ M).injective ?_⟩

Premises used: IsLocalization.bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom, Function.Bijective.injective, Exists.intro
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_4 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
inst_5 : IsLocalization (R := (i : ι) → R i) M S'
inst_6 : Finite ι
s : S'
S : (i : ι) → Type u_2 :=
  fun (i : ι) ↦ Localization (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M)
r : (i : ι) → R i
hr :
  Eq (α := (i : ι) → S i)
    ((Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i) :
          (a : (i : ι) → R i) → (i : ι) → S i)
        r :
      (i : ι) → S i)
    ((lift (R := (i : ι) → R i) (M := M) (g :=
            Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
          (a : S') → (i : ι) → S i)
        s :
      (i : ι) → S i)
refine :
  Eq (α := (i : ι) → S i)
    ((lift (R := (i : ι) → R i) (M := M) (g :=
            Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
          (a : S') → (i : ι) → S i)
        ((algebraMap ((i : ι) → R i) S' : (a : (i : ι) → R i) → S') r : S') :
      (i : ι) → S i)
    ((lift (R := (i : ι) → R i) (M := M) (g :=
            Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
          (a : S') → (i : ι) → S i)
        s :
      (i : ι) → S i)
⊢ ∃ (a : (i : ι) → R i), (algebraMap ((i : ι) → R i) S' : (a : (i : ι) → R i) → S') a = s

Tactic:
refine ⟨r, (bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom R S _ M).injective ?_⟩
-- Module: Mathlib.RingTheory.Localization.Pi
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → CommSemiring (R i)
S' : Type u_4
inst_1 : CommSemiring S'
inst_2 : Algebra ((i : ι) → R i) S'
M : Submonoid ((i : ι) → R i)
inst_3 : ∀ (i : ι), Ring.KrullDimLE.{u_2} 0 (R i)
inst_4 : ∀ (i : ι), IsLocalRing.{u_2} (R i)
inst_5 : IsLocalization (R := (i : ι) → R i) M S'
inst_6 : Finite ι
s : S'
S : (i : ι) → Type u_2 :=
  fun (i : ι) ↦ Localization (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M)
r : (i : ι) → R i
hr :
  Eq (α := (i : ι) → S i)
    ((Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i) :
          (a : (i : ι) → R i) → (i : ι) → S i)
        r :
      (i : ι) → S i)
    ((lift (R := (i : ι) → R i) (M := M) (g :=
            Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
          (a : S') → (i : ι) → S i)
        s :
      (i : ι) → S i)
rwa rwa₁ rwa₂ rwa₃ :
  Eq (α := (i : ι) → S i)
    ((Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i) :
          (a : (i : ι) → R i) → (i : ι) → S i)
        r :
      (i : ι) → S i)
    ((lift (R := (i : ι) → R i) (M := M) (g :=
            Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
          (a : S') → (i : ι) → S i)
        s :
      (i : ι) → S i)
⊢ Eq (α := (i : ι) → S i)
    ((lift (R := (i : ι) → R i) (M := M) (g :=
            Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
          (a : S') → (i : ι) → S i)
        ((algebraMap ((i : ι) → R i) S' : (a : (i : ι) → R i) → S') r : S') :
      (i : ι) → S i)
    ((lift (R := (i : ι) → R i) (M := M) (g :=
            Pi.ringHom (f := S) fun (i : ι) ↦ RingHom.comp (algebraMap (R i) (S i)) (Pi.evalRingHom R i)) ⋯ :
          (a : S') → (i : ι) → S i)
        s :
      (i : ι) → S i)

Tactic:
rwa [lift_eq (isUnit_piRingHom_algebraMap_comp_piEvalRingHom R S M) r]

Premises used: IsLocalization.lift_eq, IsLocalization.isUnit_piRingHom_algebraMap_comp_piEvalRingHom
-- Module: Mathlib.RingTheory.Localization.Rat
Goal:
q : ℚ
⊢ IsLocalization.IsInteger ℤ q ↔ Membership.mem (γ := Set ℚ) (Set.range Int.cast) q

Tactic:
simp [IsLocalization.IsInteger]

Premises used: IsLocalization.IsInteger
-- Module: Mathlib.RingTheory.Localization.Rat
Goal:
q : ℚ
⊢ Membership.mem (γ := Submonoid ℤ) (nonZeroDivisors ℤ) (↑q.den : ℤ)

Tactic:
simp
-- Module: Mathlib.RingTheory.Localization.Rat
Goal:
q : ℚ
⊢ IsRelPrime q.num
    (↑(Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) (nonZeroDivisors ℤ) x) (↑q.den : ℤ) ⋯) : ℤ)

Tactic:
simpa [isRelPrime_iff_isCoprime, Int.isCoprime_iff_nat_coprime] using q.reduced

Premises used: Rat.reduced, Int.isCoprime_iff_nat_coprime, isRelPrime_iff_isCoprime
-- Module: Mathlib.RingTheory.Localization.Rat
Goal:
q : ℚ
⊢ IsLocalization.mk' ℚ q.num
      (Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) (nonZeroDivisors ℤ) x) (↑q.den : ℤ) ⋯) =
    q

Tactic:
simp [Rat.num_div_den]

Premises used: Rat.num_div_den
-- Module: Mathlib.RingTheory.Localization.Rat
Goal:
q : ℚ
⊢ (↑(IsFractionRing.den ℤ q) : ℤ).natAbs = q.den

Tactic:
simpa [Int.associated_iff_natAbs] using q.associated_num_den.2

Premises used: Rat.associated_num_den, And.right, Int.associated_iff_natAbs
-- Module: Mathlib.RingTheory.Localization.Rat
Goal:
q : ℚ
⊢ Associated (IsFractionRing.num ℤ q) q.num

Tactic:
q.associated_num_den.1

Premises used: Rat.associated_num_den, And.left
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : Algebra R S
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Module R M
inst_10 : Module S M
inst_11 : Module R N
inst_12 : IsScalarTower R S M
inst_13 : Fintype l
inst_14 : Fintype m
inst_15 : Fintype n
inst_16 : Fintype p
inst_17 : DecidableEq l
inst_18 : DecidableEq m
inst_19 : DecidableEq n
inst_20 : DecidableEq p
h :
  ∀ (i : l × n) (j : m × p) (x : M) (x_1 : N),
    Eq (α := Matrix (l × n) (m × p) (M ⊗[R] N))
      (((((AlgebraTensorModule.curry
                      (((AlgebraTensorModule.lift (kroneckerTMulBilinear R S) :
                            Matrix l m M ⊗[R] Matrix n p N →ₗ[S] Matrix (l × n) (m × p) (M ⊗[R] N)) ∘ₗ
                          ((liftLinear R :
                                (a : l × n → m × p → M ⊗[R] N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N) →
                                  Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)
                              fun (ii : l × n) (jj : m × p) ↦
                              AlgebraTensorModule.map (singleLinearMap S ii.1 jj.1) (singleLinearMap R ii.2 jj.2) :
                            Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)) ∘ₗ
                        singleLinearMap S i j) :
                    M →ₗ[S] N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N)) :
                  (a : M) → N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N))
                x :
              N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N)) :
            (a : N) → Matrix (l × n) (m × p) (M ⊗[R] N))
          x_1 :
        Matrix (l × n) (m × p) (M ⊗[R] N))
      (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ singleLinearMap S i j) :
                    M →ₗ[S] N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N)) :
                  (a : M) → N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N))
                x :
              N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N)) :
            (a : N) → Matrix (l × n) (m × p) (M ⊗[R] N))
          x_1 :
        Matrix (l × n) (m × p) (M ⊗[R] N))
⊢ Eq (α := Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix (l × n) (m × p) (M ⊗[R] N))
    ((AlgebraTensorModule.lift (kroneckerTMulBilinear R S) :
        Matrix l m M ⊗[R] Matrix n p N →ₗ[S] Matrix (l × n) (m × p) (M ⊗[R] N)) ∘ₗ
      ((liftLinear R :
            (a : l × n → m × p → M ⊗[R] N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N) →
              Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)
          fun (ii : l × n) (jj : m × p) ↦
          AlgebraTensorModule.map (singleLinearMap S ii.1 jj.1) (singleLinearMap R ii.2 jj.2) :
        Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N))
    LinearMap.id

Tactic:
ext : 4
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : Algebra R S
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Module R M
inst_10 : Module S M
inst_11 : Module R N
inst_12 : IsScalarTower R S M
inst_13 : Fintype l
inst_14 : Fintype m
inst_15 : Fintype n
inst_16 : Fintype p
inst_17 : DecidableEq l
inst_18 : DecidableEq m
inst_19 : DecidableEq n
inst_20 : DecidableEq p
i : l × n
j : m × p
x : M
x_1 : N
⊢ Eq (α := Matrix (l × n) (m × p) (M ⊗[R] N))
    (((((AlgebraTensorModule.curry
                    (((AlgebraTensorModule.lift (kroneckerTMulBilinear R S) :
                          Matrix l m M ⊗[R] Matrix n p N →ₗ[S] Matrix (l × n) (m × p) (M ⊗[R] N)) ∘ₗ
                        ((liftLinear R :
                              (a : l × n → m × p → M ⊗[R] N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N) →
                                Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)
                            fun (ii : l × n) (jj : m × p) ↦
                            AlgebraTensorModule.map (singleLinearMap S ii.1 jj.1) (singleLinearMap R ii.2 jj.2) :
                          Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)) ∘ₗ
                      singleLinearMap S i j) :
                  M →ₗ[S] N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N)) :
                (a : M) → N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N))
              x :
            N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N)) :
          (a : N) → Matrix (l × n) (m × p) (M ⊗[R] N))
        x_1 :
      Matrix (l × n) (m × p) (M ⊗[R] N))
    (((((AlgebraTensorModule.curry (LinearMap.id ∘ₗ singleLinearMap S i j) :
                  M →ₗ[S] N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N)) :
                (a : M) → N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N))
              x :
            N →ₗ[R] Matrix (l × n) (m × p) (M ⊗[R] N)) :
          (a : N) → Matrix (l × n) (m × p) (M ⊗[R] N))
        x_1 :
      Matrix (l × n) (m × p) (M ⊗[R] N))

Tactic:
simp [single_kroneckerTMul_single]

Premises used: Matrix.single_kroneckerTMul_single
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : Algebra R S
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Module R M
inst_10 : Module S M
inst_11 : Module R N
inst_12 : IsScalarTower R S M
inst_13 : Fintype l
inst_14 : Fintype m
inst_15 : Fintype n
inst_16 : Fintype p
inst_17 : DecidableEq l
inst_18 : DecidableEq m
inst_19 : DecidableEq n
inst_20 : DecidableEq p
a :
  ∀ (i : l) (j : m) (x : M) (i_1 : n) (j_1 : p) (x_1 : N),
    Eq (α := Matrix l m M ⊗[R] Matrix n p N)
      ((((AlgebraTensorModule.curry
                        (((liftLinear R :
                              (a : l × n → m × p → M ⊗[R] N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N) →
                                Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)
                            fun (ii : l × n) (jj : m × p) ↦
                            AlgebraTensorModule.map (singleLinearMap S ii.1 jj.1) (singleLinearMap R ii.2 jj.2)) ∘ₗ
                          AlgebraTensorModule.lift (kroneckerTMulBilinear R S)) ∘ₗ
                      singleLinearMap S i j :
                    M →ₗ[S] Matrix n p N →ₗ[R] Matrix l m M ⊗[R] Matrix n p N) :
                  (a : M) → Matrix n p N →ₗ[R] Matrix l m M ⊗[R] Matrix n p N)
                x ∘ₗ
              singleLinearMap R i_1 j_1 :
            (a : N) → Matrix l m M ⊗[R] Matrix n p N)
          x_1 :
        Matrix l m M ⊗[R] Matrix n p N)
      ((((AlgebraTensorModule.curry LinearMap.id ∘ₗ singleLinearMap S i j :
                    M →ₗ[S] Matrix n p N →ₗ[R] Matrix l m M ⊗[R] Matrix n p N) :
                  (a : M) → Matrix n p N →ₗ[R] Matrix l m M ⊗[R] Matrix n p N)
                x ∘ₗ
              singleLinearMap R i_1 j_1 :
            (a : N) → Matrix l m M ⊗[R] Matrix n p N)
          x_1 :
        Matrix l m M ⊗[R] Matrix n p N)
⊢ Eq (α := Matrix l m M ⊗[R] Matrix n p N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)
    (((liftLinear R :
            (a : l × n → m × p → M ⊗[R] N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N) →
              Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)
          fun (ii : l × n) (jj : m × p) ↦
          AlgebraTensorModule.map (singleLinearMap S ii.1 jj.1) (singleLinearMap R ii.2 jj.2)) ∘ₗ
        AlgebraTensorModule.lift (kroneckerTMulBilinear R S) :
      Matrix l m M ⊗[R] Matrix n p N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)
    (LinearMap.id : Matrix l m M ⊗[R] Matrix n p N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)

Tactic:
ext : 5
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : AddCommMonoid M
inst_5 : AddCommMonoid N
inst_6 : Algebra R S
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : Module R M
inst_10 : Module S M
inst_11 : Module R N
inst_12 : IsScalarTower R S M
inst_13 : Fintype l
inst_14 : Fintype m
inst_15 : Fintype n
inst_16 : Fintype p
inst_17 : DecidableEq l
inst_18 : DecidableEq m
inst_19 : DecidableEq n
inst_20 : DecidableEq p
i : l
j : m
x : M
i_1 : n
j_1 : p
x_1 : N
⊢ Eq (α := Matrix l m M ⊗[R] Matrix n p N)
    ((((AlgebraTensorModule.curry
                      (((liftLinear R :
                            (a : l × n → m × p → M ⊗[R] N →ₗ[S] Matrix l m M ⊗[R] Matrix n p N) →
                              Matrix (l × n) (m × p) (M ⊗[R] N) →ₗ[S] Matrix l m M ⊗[R] Matrix n p N)
                          fun (ii : l × n) (jj : m × p) ↦
                          AlgebraTensorModule.map (singleLinearMap S ii.1 jj.1) (singleLinearMap R ii.2 jj.2)) ∘ₗ
                        AlgebraTensorModule.lift (kroneckerTMulBilinear R S)) ∘ₗ
                    singleLinearMap S i j :
                  M →ₗ[S] Matrix n p N →ₗ[R] Matrix l m M ⊗[R] Matrix n p N) :
                (a : M) → Matrix n p N →ₗ[R] Matrix l m M ⊗[R] Matrix n p N)
              x ∘ₗ
            singleLinearMap R i_1 j_1 :
          (a : N) → Matrix l m M ⊗[R] Matrix n p N)
        x_1 :
      Matrix l m M ⊗[R] Matrix n p N)
    ((((AlgebraTensorModule.curry LinearMap.id ∘ₗ singleLinearMap S i j :
                  M →ₗ[S] Matrix n p N →ₗ[R] Matrix l m M ⊗[R] Matrix n p N) :
                (a : M) → Matrix n p N →ₗ[R] Matrix l m M ⊗[R] Matrix n p N)
              x ∘ₗ
            singleLinearMap R i_1 j_1 :
          (a : N) → Matrix l m M ⊗[R] Matrix n p N)
        x_1 :
      Matrix l m M ⊗[R] Matrix n p N)

Tactic:
simp [single_kroneckerTMul_single]

Premises used: Matrix.single_kroneckerTMul_single
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module S M
inst_7 : Module R N
inst_8 : IsScalarTower R S M
inst_9 : Fintype l
inst_10 : Fintype m
inst_11 : Fintype n
inst_12 : Fintype p
inst_13 : DecidableEq l
inst_14 : DecidableEq m
inst_15 : DecidableEq n
inst_16 : DecidableEq p
a : Matrix l m M
b : Matrix n p N
⊢ Eq (α := Matrix (l × n) (m × p) (M ⊗[R] N))
    (((kroneckerTMulLinearEquiv l m n p R S M N :
            Matrix l m M ⊗[R] Matrix n p N ≃ₗ[S] Matrix (l × n) (m × p) (M ⊗[R] N)) :
          (a : Matrix l m M ⊗[R] Matrix n p N) → Matrix (l × n) (m × p) (M ⊗[R] N))
        (a ⊗ₜ[R] b) :
      Matrix (l × n) (m × p) (M ⊗[R] N))
    (kroneckerMap (tmul R) a b : Matrix (l × n) (m × p) (M ⊗[R] N))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, Matrix.kroneckerMap, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module S M
inst_7 : Module R N
inst_8 : IsScalarTower R S M
inst_9 : Fintype l
inst_10 : Fintype m
inst_11 : Fintype n
inst_12 : Fintype p
inst_13 : DecidableEq l
inst_14 : DecidableEq m
inst_15 : DecidableEq n
inst_16 : DecidableEq p
a : Matrix l m M
b : Matrix n p N
⊢ Eq (α := Matrix l m M ⊗[R] Matrix n p N)
    (((LinearEquiv.symm (kroneckerTMulLinearEquiv l m n p R S M N) :
            Matrix (l × n) (m × p) (M ⊗[R] N) ≃ₗ[S] Matrix l m M ⊗[R] Matrix n p N) :
          (a : Matrix (l × n) (m × p) (M ⊗[R] N)) → Matrix l m M ⊗[R] Matrix n p N)
        (kroneckerMap (tmul R) a b) :
      Matrix l m M ⊗[R] Matrix n p N)
    (a ⊗ₜ[R] b : Matrix l m M ⊗[R] Matrix n p N)

Tactic:
simp [LinearEquiv.symm_apply_eq]

Premises used: LinearEquiv.symm_apply_eq
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
l : Type u_1
m : Type u_2
n : Type u_3
p : Type u_4
R : Type u_5
S : Type u_6
M : Type u_9
N : Type u_10
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid N
inst_4 : Algebra R S
inst_5 : Module R M
inst_6 : Module S M
inst_7 : Module R N
inst_8 : IsScalarTower R S M
inst_9 : Fintype l
inst_10 : Fintype m
inst_11 : Fintype n
inst_12 : Fintype p
inst_13 : DecidableEq l
inst_14 : DecidableEq m
inst_15 : DecidableEq n
inst_16 : DecidableEq p
ia : l
ja : m
ib : n
jb : p
a : M
b : N
rw :
  Eq (α := Matrix (l × n) (m × p) (M ⊗[R] N)) (single (ia, ib) (ja, jb) (a ⊗ₜ[R] b))
    (((kroneckerTMulLinearEquiv l m n p R S M N :
          Matrix l m M ⊗[R] Matrix n p N ≃ₗ[S] Matrix (l × n) (m × p) (M ⊗[R] N)) :
        (a : Matrix l m M ⊗[R] Matrix n p N) → Matrix (l × n) (m × p) (M ⊗[R] N))
      (single ia ja a ⊗ₜ[R] single ib jb b))
rw₁ :
  Eq (α := Matrix (l × n) (m × p) (M ⊗[R] N)) (single (ia, ib) (ja, jb) (a ⊗ₜ[R] b))
    (kroneckerMap (tmul R) (single ia ja a) (single ib jb b))
rw₂ rw₃ :
  Eq (α := Matrix (l × n) (m × p) (M ⊗[R] N)) (single (ia, ib) (ja, jb) (a ⊗ₜ[R] b))
    (single (ia, ib) (ja, jb) (a ⊗ₜ[R] b))
⊢ Eq (α := Matrix l m M ⊗[R] Matrix n p N)
    (((LinearEquiv.symm (kroneckerTMulLinearEquiv l m n p R S M N) :
            Matrix (l × n) (m × p) (M ⊗[R] N) ≃ₗ[S] Matrix l m M ⊗[R] Matrix n p N) :
          (a : Matrix (l × n) (m × p) (M ⊗[R] N)) → Matrix l m M ⊗[R] Matrix n p N)
        (single (ia, ib) (ja, jb) (a ⊗ₜ[R] b)) :
      Matrix l m M ⊗[R] Matrix n p N)
    (single ia ja a ⊗ₜ[R] single ib jb b : Matrix l m M ⊗[R] Matrix n p N)

Tactic:
rw [LinearEquiv.symm_apply_eq, kroneckerTMulLinearEquiv_tmul,
    single_kroneckerTMul_single]

Premises used: LinearEquiv.symm_apply_eq, Matrix.single_kroneckerTMul_single, kroneckerTMulLinearEquiv_tmul
-- Module: Mathlib.RingTheory.MatrixAlgebra
Goal:
m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Semiring A
inst_3 : Semiring B
inst_4 : Algebra R S
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Fintype m
inst_8 : Fintype n
inst_9 : DecidableEq m
inst_10 : DecidableEq n
inst_11 : Module S A
inst_12 : IsScalarTower R S A
⊢ Eq (α := Matrix (m × n) (m × n) (A ⊗[R] B))
    (((kroneckerTMulLinearEquiv m m n n R S A B :
          Matrix m m A ⊗[R] Matrix n n B ≃ₗ[S] Matrix (m × n) (m × n) (A ⊗[R] B)) :
        (a : Matrix m m A ⊗[R] Matrix n n B) → Matrix (m × n) (m × n) (A ⊗[R] B))
      1)
    1

Tactic:
simp [Algebra.TensorProduct.one_def]

Premises used: Algebra.TensorProduct.one_def