awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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 : (i : ι) → Submonoid (R i)
inst_3 : ∀ (i : ι), IsLocalization.{u_2, u_3} (M i) (S i)
z : (i : ι) → S i
⊢ ∃ (x : ((i : ι) → R i) × ↥(Submonoid.pi (M := R) Set.univ M)),
    HMul.hMul (β := (i : ι) → S i) z
        ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) (↑x.2 : (i : ι) → R i) :
          (i : ι) → S i) =
      (algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x.1
have choose : ∀ (rm : (i : ι) → R i × ↥(M i))
  (h :
    ∀ (i : ι),
      HMul.hMul (β := S i) (z i) ((algebraMap (R i) (S i) : (a : R i) → S i) (↑(rm i).2 : R i) : S i) =
        (algebraMap (R i) (S i) : (a : R i) → S i) (rm i).1),
  ∃ (x : ((i : ι) → R i) × ↥(Submonoid.pi (M := R) Set.univ M)),
    HMul.hMul (β := (i : ι) → S i) z
        ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) (↑x.2 : (i : ι) → R i) :
          (i : ι) → S i) =
      (algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x.1
Tactic: choose rm h using fun i ↦ surj (M := M i) (z i)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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 : (i : ι) → Submonoid (R i)
inst_3 : ∀ (i : ι), IsLocalization.{u_2, u_3} (M i) (S i)
x y : (i : ι) → R i
eq :
  Eq (α := (i : ι) → S i)
    ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) x : (i : ι) → S i)
    ((algebraMap ((i : ι) → R i) ((i : ι) → S i) : (a : (i : ι) → R i) → (i : ι) → S i) y : (i : ι) → S i)
⊢ ∃ (c : ↥(Submonoid.pi (M := R) Set.univ M)), (↑c : (i : ι) → R i) * x = (↑c : (i : ι) → R i) * y
have choose : ∀ (c : (i : ι) → ↥(M i))
  (hc :
    ∀ (i : ι),
      HMul.hMul (β := R i) (↑(c i) : R i)
          (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) x : R i) =
        HMul.hMul (β := R i) (↑(c i) : R i)
          (((Pi.evalRingHom R i : ((i : ι) → R i) →+* R i) : (a : (i : ι) → R i) → R i) y : R i)),
  ∃ (c : ↥(Submonoid.pi (M := R) Set.univ M)), (↑c : (i : ι) → R i) * x = (↑c : (i : ι) → R i) * y
Tactic: choose c hc using fun i ↦ exists_of_eq (M := M i) (congr_fun eq i)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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 : Finite ι
n : (i : ι) → R i
hn :
  Membership.mem (γ := Submonoid ((i : ι) → R i))
    (Submonoid.pi (M := R) Set.univ fun (i : ι) ↦ Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) n
⊢ ∃ m ∈ M, n ∣ m
have choose : ∀ (m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i)
  (mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i)))
  (eq :
    ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i),
      (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i),
  ∃ m ∈ M, n ∣ m
Tactic: choose m mem eq using hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
⊢ ∃ m ∈ M, n ∣ m
have have : ∀ (this : Fintype ι), ∃ m ∈ M, n ∣ m
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
this : Fintype ι
⊢ ∃ m ∈ M, n ∣ m
have refine : ∀ (i : ι), n i ∣ (∏ i : ι, m i True.intro) i
Tactic: refine ⟨∏ i, m i ⟨⟩, prod_mem fun i _ ↦ mem i _, pi_dvd_iff.mpr fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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 : Finite ι
n : (i : ι) → R i
m : (i : ι) → Membership.mem (γ := Set ι) Set.univ i → (i : ι) → R i
mem : ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), m i a ∈ (↑M : Set ((i : ι) → R i))
eq :
  ∀ (i : ι) (a : Membership.mem (γ := Set ι) Set.univ i), (Pi.evalRingHom R i : (a : (i : ι) → R i) → R i) (m i a) = n i
this : Fintype ι
i : ι
⊢ n i ∣ (∏ i : ι, m i True.intro) i
have rw : n i ∣ ∏ c : ι, m c True.intro i
Tactic: rw [Fintype.prod_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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)
⊢ Surjective (α := (i : ι) → R i) (β := (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)
have apply : ∀ (i : ι),
  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: apply Surjective.piMap (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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 : ι
⊢ 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
have pos : ∀ (h₀ : Membership.mem (γ := Submonoid (R i)) (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) 0),
  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: by_cases h₀ : (0 : R i) ∈ (M.map (Pi.evalRingHom R i))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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 : ι
pos :
  ∀
    (h₀ :
      Membership.mem (γ := Submonoid (R i)) (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) 0),
    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
⊢ 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
have neg : ∀ (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: by_cases h₀ : (0 : R i) ∈ (M.map (Pi.evalRingHom R i))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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₀ : Membership.mem (γ := Submonoid (R i)) (Submonoid.map (F := ((i : ι) → R i) →+* R i) (Pi.evalRingHom R i) M) 0
⊢ 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
have pos : ∀ (this : Unique (S i)),
  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: have := uniqueOfZeroMem h₀ (S := (S i))
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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)
⊢ ∃ (a : (i : ι) → R i), (algebraMap ((i : ι) → R i) S' : (a : (i : ι) → R i) → S') a = s
have 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)) sorry :
            (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: obtain ⟨r, hr⟩ :=
    surjective_piRingHom_algebraMap_comp_piEvalRingHom
    S M ((lift (isUnit_piRingHom_algebraMap_comp_piEvalRingHom R S M)) s)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Pi (goal)
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
have 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)) sorry :
        (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)) sorry :
        (a : S') → (i : ι) → S i)
      s :
    (i : ι) → S i)
Tactic: refine ⟨r, (bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom R S _ M).injective ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
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
⊢ 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
have 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))
Tactic: ext : 4
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
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
⊢ 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)
have 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)
Tactic: ext : 5
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
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
⊢ 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)
have 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))
Tactic: rw [LinearEquiv.symm_apply_eq, kroneckerTMulLinearEquiv_tmul,
    single_kroneckerTMul_single]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
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))
⊢ 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)
have 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))
Tactic: rw [LinearEquiv.symm_apply_eq, kroneckerTMulLinearEquiv_tmul,
    single_kroneckerTMul_single]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
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))
⊢ 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)
have 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))
Tactic: rw [LinearEquiv.symm_apply_eq, kroneckerTMulLinearEquiv_tmul,
    single_kroneckerTMul_single]
-- Lean 4 proof step from Mathlib.RingTheory.MatrixAlgebra (goal)
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 A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : DecidableEq n
inst_6 : Fintype n
a₁ a₂ : A
b₁ b₂ : Matrix n n R
⊢ (toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
    HMul.hMul (α := Matrix n n A) (β := Matrix n n A)
      ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a₁ ⊗ₜ[R] b₁) : Matrix n n A)
      ((toFunLinear n R A : (a : A ⊗[R] Matrix n n R) → Matrix n n A) (a₂ ⊗ₜ[R] b₂) : Matrix n n A)
have simp_rw : (a₁ * a₂) •
    HMul.hMul (α := Matrix n n A) (b₁.map (⇑(algebraMap R A) : (a : R) → A))
      (b₂.map (⇑(algebraMap R A) : (a : R) → A)) =
  HSMul.hSMul (β := Matrix n n A) a₁ (b₁.map (⇑(algebraMap R A) : (a : R) → A)) *
    HSMul.hSMul (β := Matrix n n A) a₂ (b₂.map (⇑(algebraMap R A) : (a : R) → A))
Tactic: simp_rw [toFunLinear, lift.tmul, toFunBilinear_apply, Matrix.map_mul]