awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
i : I
hi : i ∈ f.support
j : I
hj : j ∈ f.support
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
        (↑f.support : Set I) (↑f.support : Set I)))
    (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a j : (a : I) → R) i : R)
      (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) j : S) ((b : (a : I) → S) i : S)))
have h : Membership.mem (γ := Submodule R S)
  (Submodule.span R
    (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
      (↑f.support : Set I) (↑f.support : Set I)))
  (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) j : S) ((b : (a : I) → S) i : S))
Tactic: apply Submodule.smul_mem
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
i : I
hi : i ∈ f.support
j : I
hj : j ∈ f.support
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R
      (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
        (↑f.support : Set I) (↑f.support : Set I)))
    (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) j : S) ((b : (a : I) → S) i : S))
have h : Membership.mem (γ := Set S)
  (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
    (↑f.support : Set I) (↑f.support : Set I))
  (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) j : S) ((b : (a : I) → S) i : S))
Tactic: apply Submodule.subset_span
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
i : I
hi : i ∈ f.support
j : I
hj : j ∈ f.support
w : I
⊢ Membership.mem (γ := Set S)
    (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
      (↑f.support : Set I) (↑f.support : Set I))
    (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) j : S) ((b : (a : I) → S) i : S))
have left : j ∈ (↑f.support : Set I)
Tactic: use j, hj, i, hi
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
i : I
hi : i ∈ f.support
j : I
hj : j ∈ f.support
w : I
left : j ∈ (↑f.support : Set I)
w₁ : I
⊢ Membership.mem (γ := Set S)
    (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
      (↑f.support : Set I) (↑f.support : Set I))
    (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) j : S) ((b : (a : I) → S) i : S))
have left₁ : i ∈ (↑f.support : Set I)
Tactic: use j, hj, i, hi
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : FormallyUnramified R S
inst_4 : EssFiniteType R S
inst_5 : Free R S
I : Type u_2 := Free.ChooseBasisIndex R S
b : Basis I R S := Free.chooseBasis R S
f : I →₀ S
hf : Eq (α := S ⊗[R] S) (elem R S) (f.sum fun (i : I) (x : S) ↦ x ⊗ₜ[R] (b : (a : I) → S) i)
x : S
a : I → I →₀ R := fun (i : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (α := S) ((b : (a : I) → S) i : S) x)
F : I →₀ I →₀ R :=
  Finsupp.onFinset f.support
    (fun (j : I) ↦ (b.repr : (a : S) → I →₀ R) (HMul.hMul (β := S) x ((f : (a : I) → S) j : S))) ⋯
hG :
  ∀ j ∉ f.support.biUnion fun (i : I) ↦ (a i).support,
    Eq (α := I →₀ R)
      ((b.repr : (a : S) → I →₀ R)
          (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y) :
        I →₀ R)
      (0 : I →₀ R)
G : I →₀ I →₀ R :=
  Finsupp.onFinset (f.support.biUnion fun (i : I) ↦ (a i).support)
    (fun (j : I) ↦
      (b.repr : (a : S) → I →₀ R)
        (f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y))
    ⋯
this_1 : F = G
this :
  ∀ (j : I),
    HMul.hMul (β := S) x ((f : (a : I) → S) j : S) =
      f.sum fun (i : I) (y : S) ↦ HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((a i : (a : I) → R) j : R) y
i : I
hi : i ∈ f.support
j : I
hj : j ∈ f.support
w : I
left : j ∈ (↑f.support : Set I)
w₁ : I
left₁ : i ∈ (↑f.support : Set I)
⊢ Membership.mem (γ := Set S)
    (Set.image2 (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S))
      (↑f.support : Set I) (↑f.support : Set I))
    (HMul.hMul (α := S) (β := S) ((f : (a : I) → S) j : S) ((b : (a : I) → S) i : S))
have right : (fun (i j : I) ↦ HMul.hMul (α := S) (β := S) ((f : (a : I) → S) i : S) ((b : (a : I) → S) j : S)) j i =
  HMul.hMul (α := S) (β := S) ((f : (a : I) → S) j : S) ((b : (a : I) → S) i : S)
Tactic: use j, hj, i, hi
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
r : S
m : M
⊢ AddHom.toFun
      (LinearMap.toAddHom
        ((((LinearMap.flip
                    (((TensorProduct.AlgebraTensorModule.mapBilinear R S S S S S M :
                          (S →ₗ[S] S) →ₗ[S] (S →ₗ[R] M) →ₗ[R] S ⊗[R] S →ₗ[S] S ⊗[R] M) :
                        (a : S →ₗ[S] S) → (S →ₗ[R] M) →ₗ[R] S ⊗[R] S →ₗ[S] S ⊗[R] M)
                      LinearMap.id) :
                  S ⊗[R] S →ₗ[S] (S →ₗ[R] M) →ₗ[R] S ⊗[R] M) :
                (a : S ⊗[R] S) → (S →ₗ[R] M) →ₗ[R] S ⊗[R] M)
              (elem R S) :
            (S →ₗ[R] M) →ₗ[R] S ⊗[R] M) ∘ₗ
          (LinearMap.flip
              (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
            M →ₗ[R] S →ₗ[R] M)))
      (r • m) =
    HSMul.hSMul (α := S) (β := S ⊗[R] M) ((RingHom.id S : (a : S) → S) r : S)
      (AddHom.toFun
        (LinearMap.toAddHom
          ((((LinearMap.flip
                      (((TensorProduct.AlgebraTensorModule.mapBilinear R S S S S S M :
                            (S →ₗ[S] S) →ₗ[S] (S →ₗ[R] M) →ₗ[R] S ⊗[R] S →ₗ[S] S ⊗[R] M) :
                          (a : S →ₗ[S] S) → (S →ₗ[R] M) →ₗ[R] S ⊗[R] S →ₗ[S] S ⊗[R] M)
                        LinearMap.id) :
                    S ⊗[R] S →ₗ[S] (S →ₗ[R] M) →ₗ[R] S ⊗[R] M) :
                  (a : S ⊗[R] S) → (S →ₗ[R] M) →ₗ[R] S ⊗[R] M)
                (elem R S) :
              (S →ₗ[R] M) →ₗ[R] S ⊗[R] M) ∘ₗ
            (LinearMap.flip
                (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
              M →ₗ[R] S →ₗ[R] M)))
        m)
have simp : ((TensorProduct.AlgebraTensorModule.map LinearMap.id
          (((LinearMap.flip
                  (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                M →ₗ[R] S →ₗ[R] M) :
              (a : M) → S →ₗ[R] M)
            (r • m)) :
        S ⊗[R] S →ₗ[S] S ⊗[R] M) :
      (a : S ⊗[R] S) → S ⊗[R] M)
    (elem R S) =
  HSMul.hSMul (β := S ⊗[R] M) r
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (elem R S) :
      S ⊗[R] M)
Tactic: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.coe_comp, Function.comp_apply,
      LinearMap.flip_apply, TensorProduct.AlgebraTensorModule.mapBilinear_apply, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
r : S
m : M
⊢ ((TensorProduct.AlgebraTensorModule.map LinearMap.id
            (((LinearMap.flip
                    (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                  M →ₗ[R] S →ₗ[R] M) :
                (a : M) → S →ₗ[R] M)
              (r • m)) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (elem R S) =
    HSMul.hSMul (β := S ⊗[R] M) r
      (((TensorProduct.AlgebraTensorModule.map LinearMap.id
                (((LinearMap.flip
                        (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                      M →ₗ[R] S →ₗ[R] M) :
                    (a : M) → S →ₗ[R] M)
                  m) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M)
have trans : Eq (α := S ⊗[R] M)
  (((TensorProduct.AlgebraTensorModule.map LinearMap.id
            (((LinearMap.flip
                    (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                  M →ₗ[R] S →ₗ[R] M) :
                (a : M) → S →ₗ[R] M)
              (r • m)) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (elem R S) :
    S ⊗[R] M)
  (((TensorProduct.AlgebraTensorModule.map LinearMap.id
            (((LinearMap.flip
                    (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                  M →ₗ[R] S →ₗ[R] M) :
                (a : M) → S →ₗ[R] M)
              m) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) :
    S ⊗[R] M)
Tactic: trans (TensorProduct.AlgebraTensorModule.map (LinearMap.id (R := S) (M := S))
      ((LinearMap.flip (AlgHom.toLinearMap (lsmul R R M))) m)) ((1 ⊗ₜ r) * elem R S)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
r : S
m : M
trans :
  Eq (α := S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                (r • m)) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (elem R S) :
      S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) :
      S ⊗[R] M)
⊢ ((TensorProduct.AlgebraTensorModule.map LinearMap.id
            (((LinearMap.flip
                    (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                  M →ₗ[R] S →ₗ[R] M) :
                (a : M) → S →ₗ[R] M)
              (r • m)) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (elem R S) =
    HSMul.hSMul (β := S ⊗[R] M) r
      (((TensorProduct.AlgebraTensorModule.map LinearMap.id
                (((LinearMap.flip
                        (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                      M →ₗ[R] S →ₗ[R] M) :
                    (a : M) → S →ₗ[R] M)
                  m) :
              S ⊗[R] S →ₗ[S] S ⊗[R] M) :
            (a : S ⊗[R] S) → S ⊗[R] M)
          (elem R S) :
        S ⊗[R] M)
have trans₁ : ((TensorProduct.AlgebraTensorModule.map LinearMap.id
          (((LinearMap.flip
                  (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                M →ₗ[R] S →ₗ[R] M) :
              (a : M) → S →ₗ[R] M)
            m) :
        S ⊗[R] S →ₗ[S] S ⊗[R] M) :
      (a : S ⊗[R] S) → S ⊗[R] M)
    (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) =
  HSMul.hSMul (β := S ⊗[R] M) r
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (elem R S) :
      S ⊗[R] M)
Tactic: trans (TensorProduct.AlgebraTensorModule.map (LinearMap.id (R := S) (M := S))
      ((LinearMap.flip (AlgHom.toLinearMap (lsmul R R M))) m)) ((1 ⊗ₜ r) * elem R S)
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
r : S
m : M
⊢ Eq (α := S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                (r • m)) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (elem R S) :
      S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) :
      S ⊗[R] M)
have zero : Eq (α := S ⊗[R] M)
  (((TensorProduct.AlgebraTensorModule.map LinearMap.id
            (((LinearMap.flip
                    (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                  M →ₗ[R] S →ₗ[R] M) :
                (a : M) → S →ₗ[R] M)
              (r • m)) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      0 :
    S ⊗[R] M)
  (((TensorProduct.AlgebraTensorModule.map LinearMap.id
            (((LinearMap.flip
                    (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                  M →ₗ[R] S →ₗ[R] M) :
                (a : M) → S →ₗ[R] M)
              m) :
          S ⊗[R] S →ₗ[S] S ⊗[R] M) :
        (a : S ⊗[R] S) → S ⊗[R] M)
      (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) 0) :
    S ⊗[R] M)
Tactic: induction elem R S using TensorProduct.induction_on
-- Lean 4 proof step from Mathlib.RingTheory.Unramified.Finite (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
inst_7 : FormallyUnramified R S
inst_8 : EssFiniteType R S
r : S
m : M
zero :
  Eq (α := S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                (r • m)) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        0 :
      S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) 0) :
      S ⊗[R] M)
⊢ Eq (α := S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                (r • m)) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (elem R S) :
      S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (elem R S)) :
      S ⊗[R] M)
have tmul : ∀ (x y : S),
  Eq (α := S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                (r • m)) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (x ⊗ₜ[R] y) :
      S ⊗[R] M)
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (((LinearMap.flip
                      (AlgHom.toLinearMap (lsmul R R M) : LinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) S (End R M)) :
                    M →ₗ[R] S →ₗ[R] M) :
                  (a : M) → S →ₗ[R] M)
                m) :
            S ⊗[R] S →ₗ[S] S ⊗[R] M) :
          (a : S ⊗[R] S) → S ⊗[R] M)
        (HMul.hMul (α := S ⊗[R] S) (1 ⊗ₜ[R] r) (x ⊗ₜ[R] y)) :
      S ⊗[R] M)
Tactic: induction elem R S using TensorProduct.induction_on