awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (N i)
P : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (P i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (P i)
inst_7 : (i : ι) → Module.{u_2, u_5} S (P i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (P i)
ε : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (N i) (P i)
ibc : ∀ (i : ι), IsBaseChange S (ε i)
⊢ IsBaseChange S (lmap (M := N) (N := P) ε)
have apply : ∀ (x : ⨁ (i : ι), N i),
  Eq (α := ⨁ (i : ι), P i)
    ((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
              (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                  sorry.equiv :
                (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
            (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
          (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
        (1 ⊗ₜ[R] x) :
      ⨁ (i : ι), P i)
    ((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i)
Tactic: classical
  apply of_equiv <| directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ (ibc i).equiv
  intros; ext
  simp [coe_directSumRight, coe_congrLinearEquiv, equiv_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u_1, u_4} R (N i)
P : ι → Type u_5
inst_5 : (i : ι) → AddCommMonoid (P i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (P i)
inst_7 : (i : ι) → Module.{u_2, u_5} S (P i)
inst_8 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_5} R S (P i)
ε : (i : ι) → LinearMap.{u_1, u_1, u_4, u_5} (RingHom.id R) (N i) (P i)
ibc : ∀ (i : ι), IsBaseChange S (ε i)
apply apply₁ apply₂ :
  ∀ (x : ⨁ (i : ι), N i),
    Eq (α := ⨁ (i : ι), P i)
      ((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
                (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                    ⋯.equiv :
                  (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
              (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
            (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
          (1 ⊗ₜ[R] x) :
        ⨁ (i : ι), P i)
      ((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i)
⊢ IsBaseChange S (lmap (M := N) (N := P) ε)
have w : ∀ (x : ⨁ (i : ι), N i) (i : ι),
  (((((directSumRight R S S N : (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≪≫ₗ
                  (congrLinearEquiv (N := fun (i : ι) ↦ TensorProduct.{u_1, u_2, u_4} R S (N i)) (P := P) fun (i : ι) ↦
                      sorry.equiv :
                    (⨁ (i : ι), TensorProduct.{u_1, u_2, u_4} R S (N i)) ≃ₗ[S] ⨁ (i : ι), P i) :
                (S ⊗[R] ⨁ (i : ι), N i) ≃ₗ[S] ⨁ (i : ι), P i) :
              (a : S ⊗[R] ⨁ (i : ι), N i) → ⨁ (i : ι), P i)
            (1 ⊗ₜ[R] x) :
          ⨁ (i : ι), P i) :
        (a : ι) → P a)
      i =
    (((lmap (M := N) (N := P) ε : (a : ⨁ (i : ι), N i) → ⨁ (i : ι), P i) x : ⨁ (i : ι), P i) : (a : ι) → P a) i
Tactic: classical
  apply of_equiv <| directSumRight R S S N ≪≫ₗ congrLinearEquiv fun i ↦ (ibc i).equiv
  intros; ext
  simp [coe_directSumRight, coe_congrLinearEquiv, equiv_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
⊢ IsBaseChange (M := ι →₀ M) S (Finsupp.mapRange.linearMap ε)
have apply : ∀ (x : ι →₀ M),
  Eq (α := ι →₀ M')
    ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
              equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) sorry ≪≫ₗ
            LinearEquiv.symm (finsuppLEquivDirectSum S M' ι) :
          (a : S ⊗[R] (ι →₀ M)) → ι →₀ M')
        (1 ⊗ₜ[R] x) :
      ι →₀ M')
    ((Finsupp.mapRange.linearMap ε : (a : ι →₀ M) → ι →₀ M') x : ι →₀ M')
Tactic: apply of_equiv <|
    LinearEquiv.baseChange R S _ _ (finsuppLEquivDirectSum ..) ≪≫ₗ
      (directSum (fun _ ↦ ibc)).equiv ≪≫ₗ (finsuppLEquivDirectSum ..).symm
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ Eq (α := ι →₀ M')
    ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
              equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ ≪≫ₗ
            LinearEquiv.symm (finsuppLEquivDirectSum S M' ι) :
          (a : S ⊗[R] (ι →₀ M)) → ι →₀ M')
        (1 ⊗ₜ[R] x) :
      ι →₀ M')
    ((Finsupp.mapRange.linearMap ε : (a : ι →₀ M) → ι →₀ M') x : ι →₀ M')
have rw : Eq (α := ⨁ (i : ι), M')
  ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
          equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) sorry :
        (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
      (1 ⊗ₜ[R] x) :
    ⨁ (i : ι), M')
  ((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') sorry x) :
    ⨁ (i : ι), M')
Tactic: rw [LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply,
    LinearEquiv.symm_apply_eq]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
x : ι →₀ M
⊢ Eq (α := ⨁ (i : ι), M')
    ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
            equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ :
          (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
        (1 ⊗ₜ[R] x) :
      ⨁ (i : ι), M')
    ((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') ⋯ x) :
      ⨁ (i : ι), M')
have w : ∀ (i : ι),
  (((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) sorry :
              (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
            (1 ⊗ₜ[R] x) :
          ⨁ (i : ι), M') :
        (a : ι) → M')
      i =
    (((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') sorry x) :
          ⨁ (i : ι), M') :
        (a : ι) → M')
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
⊢ IsBaseChange (M := ι →₀ M) S (Finsupp.mapRange.linearMap ε)
have apply : ∀ (x : ι →₀ M),
  Eq (α := ι →₀ M')
    ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
              equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) sorry ≪≫ₗ
            LinearEquiv.symm (finsuppLEquivDirectSum S M' ι) :
          (a : S ⊗[R] (ι →₀ M)) → ι →₀ M')
        (1 ⊗ₜ[R] x) :
      ι →₀ M')
    ((Finsupp.mapRange.linearMap ε : (a : ι →₀ M) → ι →₀ M') x : ι →₀ M')
Tactic: classical
  apply of_equiv <|
    LinearEquiv.baseChange R S _ _ (finsuppLEquivDirectSum ..) ≪≫ₗ
      (directSum (fun _ ↦ ibc)).equiv ≪≫ₗ (finsuppLEquivDirectSum ..).symm
  intro x
  rw [LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply,
    LinearEquiv.symm_apply_eq]
  ext
  simp [LinearEquiv.baseChange_tmul, IsBaseChange.equiv_tmul, lmap_finsuppLEquivDirectSum_eq]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
apply apply₁ :
  ∀ (x : ι →₀ M),
    Eq (α := ι →₀ M')
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ ≪≫ₗ
              LinearEquiv.symm (finsuppLEquivDirectSum S M' ι) :
            (a : S ⊗[R] (ι →₀ M)) → ι →₀ M')
          (1 ⊗ₜ[R] x) :
        ι →₀ M')
      ((Finsupp.mapRange.linearMap ε : (a : ι →₀ M) → ι →₀ M') x : ι →₀ M')
⊢ IsBaseChange (M := ι →₀ M) S (Finsupp.mapRange.linearMap ε)
have apply₂ : ∀ (x : ι →₀ M),
  Eq (α := ⨁ (i : ι), M')
    ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
            equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) sorry :
          (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
        (1 ⊗ₜ[R] x) :
      ⨁ (i : ι), M')
    ((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') sorry x) :
      ⨁ (i : ι), M')
Tactic: classical
  apply of_equiv <|
    LinearEquiv.baseChange R S _ _ (finsuppLEquivDirectSum ..) ≪≫ₗ
      (directSum (fun _ ↦ ibc)).equiv ≪≫ₗ (finsuppLEquivDirectSum ..).symm
  intro x
  rw [LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply,
    LinearEquiv.symm_apply_eq]
  ext
  simp [LinearEquiv.baseChange_tmul, IsBaseChange.equiv_tmul, lmap_finsuppLEquivDirectSum_eq]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.IsBaseChangePi (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
M : Type u_6
M' : Type u_7
inst_3 : AddCommMonoid M
inst_4 : AddCommMonoid M'
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module S M'
inst_8 : IsScalarTower R S M'
ε : M →ₗ[R] M'
ibc : IsBaseChange S ε
apply apply₁ :
  ∀ (x : ι →₀ M),
    Eq (α := ι →₀ M')
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ ≪≫ₗ
              LinearEquiv.symm (finsuppLEquivDirectSum S M' ι) :
            (a : S ⊗[R] (ι →₀ M)) → ι →₀ M')
          (1 ⊗ₜ[R] x) :
        ι →₀ M')
      ((Finsupp.mapRange.linearMap ε : (a : ι →₀ M) → ι →₀ M') x : ι →₀ M')
apply₂ :
  ∀ (x : ι →₀ M),
    Eq (α := ⨁ (i : ι), M')
      ((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
              equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) ⋯ :
            (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
          (1 ⊗ₜ[R] x) :
        ⨁ (i : ι), M')
      ((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') ⋯ x) :
        ⨁ (i : ι), M')
⊢ IsBaseChange (M := ι →₀ M) S (Finsupp.mapRange.linearMap ε)
have w : ∀ (x : ι →₀ M) (i : ι),
  (((LinearEquiv.baseChange R S (ι →₀ M) (⨁ (x : ι), M) (finsuppLEquivDirectSum R M ι) ≪≫ₗ
                equiv (f := lmap (M := fun (i : ι) ↦ M) (N := fun (i : ι) ↦ M') fun (x : ι) ↦ ε) sorry :
              (a : S ⊗[R] (ι →₀ M)) → ⨁ (i : ι), M')
            (1 ⊗ₜ[R] x) :
          ⨁ (i : ι), M') :
        (a : ι) → M')
      i =
    (((finsuppLEquivDirectSum S M' ι : (a : ι →₀ M') → ⨁ (i : ι), M') (Finsupp.mapRange (⇑ε : (a : M) → M') sorry x) :
          ⨁ (i : ι), M') :
        (a : ι) → M')
      i
Tactic: classical
  apply of_equiv <|
    LinearEquiv.baseChange R S _ _ (finsuppLEquivDirectSum ..) ≪≫ₗ
      (directSum (fun _ ↦ ibc)).equiv ≪≫ₗ (finsuppLEquivDirectSum ..).symm
  intro x
  rw [LinearEquiv.trans_apply, Finsupp.mapRange.linearMap_apply,
    LinearEquiv.symm_apply_eq]
  ext
  simp [LinearEquiv.baseChange_tmul, IsBaseChange.equiv_tmul, lmap_finsuppLEquivDirectSum_eq]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (f : (a : A ⊗[R] B) → C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a₁ ⊗ₜ[R] b₁) : C)
        ((f : (a : A ⊗[R] B) → C) (a₂ ⊗ₜ[R] b₂) : C)
x y : A ⊗[R] B
this_1 : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := ⋯
⊢ LinearMap.compr₂ (LinearMap.mul S (A ⊗[R] B)) f = (LinearMap.mul S C ∘ₗ f).compl₂ f
have a : ∀ (x : A) (x_1 : B) (x_2 : A) (x_3 : B),
  Eq.{uC + 1} (α := C)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (LinearMap.compr₂ (LinearMap.mul S (A ⊗[R] B)) f) :
                                A →ₗ[S] B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                              (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[S] C)
                            x :
                          B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                        (a : B) → A ⊗[R] B →ₗ[S] C)
                      x_1) :
                  A →ₗ[S] B →ₗ[R] C) :
                (a : A) → B →ₗ[R] C)
              x_2 :
            B →ₗ[R] C) :
          (a : B) → C)
        x_3 :
      C)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry ((LinearMap.mul S C ∘ₗ f).compl₂ f) :
                                A →ₗ[S] B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                              (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[S] C)
                            x :
                          B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                        (a : B) → A ⊗[R] B →ₗ[S] C)
                      x_1) :
                  A →ₗ[S] B →ₗ[R] C) :
                (a : A) → B →ₗ[R] C)
              x_2 :
            B →ₗ[R] C) :
          (a : B) → C)
        x_3 :
      C)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
S : Type uS
A : Type uA
B : Type uB
C : Type uC
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
f : A ⊗[R] B →ₗ[S] C
hf :
  ∀ (a₁ a₂ : A) (b₁ b₂ : B),
    (f : (a : A ⊗[R] B) → C) ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) =
      HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (a₁ ⊗ₜ[R] b₁) : C)
        ((f : (a : A ⊗[R] B) → C) (a₂ ⊗ₜ[R] b₂) : C)
x y : A ⊗[R] B
this_1 : Algebra R C := restrictScalars R S C
this : IsScalarTower R S C := ⋯
x_1 : A
x_2 : B
x_3 : A
x_4 : B
⊢ Eq.{uC + 1} (α := C)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry (LinearMap.compr₂ (LinearMap.mul S (A ⊗[R] B)) f) :
                                A →ₗ[S] B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                              (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[S] C)
                            x_1 :
                          B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                        (a : B) → A ⊗[R] B →ₗ[S] C)
                      x_2) :
                  A →ₗ[S] B →ₗ[R] C) :
                (a : A) → B →ₗ[R] C)
              x_3 :
            B →ₗ[R] C) :
          (a : B) → C)
        x_4 :
      C)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry ((LinearMap.mul S C ∘ₗ f).compl₂ f) :
                                A →ₗ[S] B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                              (a : A) → B →ₗ[R] A ⊗[R] B →ₗ[S] C)
                            x_1 :
                          B →ₗ[R] A ⊗[R] B →ₗ[S] C) :
                        (a : B) → A ⊗[R] B →ₗ[S] C)
                      x_2) :
                  A →ₗ[S] B →ₗ[R] C) :
                (a : A) → B →ₗ[R] C)
              x_3 :
            B →ₗ[R] C) :
          (a : B) → C)
        x_4 :
      C)
have a : (f : (a : A ⊗[R] B) → C) ((x_1 * x_3) ⊗ₜ[R] (x_2 * x_4)) =
  HMul.hMul (α := C) (β := C) ((f : (a : A ⊗[R] B) → C) (x_1 ⊗ₜ[R] x_2) : C)
    ((f : (a : A ⊗[R] B) → C) (x_3 ⊗ₜ[R] x_4) : C)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
a₁ a₂ : A
b₁ b₂ : B
⊢ HMul.hMul (α := C) (β := C) ((f : (a : A) → C) (a₁ * a₂) : C) ((g : (a : B) → C) (b₁ * b₂) : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
have rw : HMul.hMul (β := C) (HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((f : (a : A) → C) a₂ : C))
    ((g : (a : B) → C) (b₁ * b₂) : C) =
  HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
Tactic: rw [map_mul, map_mul, (hfg a₂ b₁).mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
a₁ a₂ : A
b₁ b₂ : B
rw :
  HMul.hMul (β := C) (HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((f : (a : A) → C) a₂ : C))
      ((g : (a : B) → C) (b₁ * b₂) : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
⊢ HMul.hMul (α := C) (β := C) ((f : (a : A) → C) (a₁ * a₂) : C) ((g : (a : B) → C) (b₁ * b₂) : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
have rw₁ : HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((f : (a : A) → C) a₂ : C) *
    HMul.hMul (α := C) (β := C) ((g : (a : B) → C) b₁ : C) ((g : (a : B) → C) b₂ : C) =
  HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
Tactic: rw [map_mul, map_mul, (hfg a₂ b₁).mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
a₁ a₂ : A
b₁ b₂ : B
rw :
  HMul.hMul (β := C) (HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((f : (a : A) → C) a₂ : C))
      ((g : (a : B) → C) (b₁ * b₂) : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
rw₁ :
  HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((f : (a : A) → C) a₂ : C) *
      HMul.hMul (α := C) (β := C) ((g : (a : B) → C) b₁ : C) ((g : (a : B) → C) b₂ : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
⊢ HMul.hMul (α := C) (β := C) ((f : (a : A) → C) (a₁ * a₂) : C) ((g : (a : B) → C) (b₁ * b₂) : C) =
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
      HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
have rw₂ : HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C) =
  HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₁ : C) ((g : (a : B) → C) b₁ : C) *
    HMul.hMul (α := C) (β := C) ((f : (a : A) → C) a₂ : C) ((g : (a : B) → C) b₂ : C)
Tactic: rw [map_mul, map_mul, (hfg a₂ b₁).mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
⊢ HMul.hMul (α := C) (β := C) ((f : (a : A) → C) 1 : C) ((g : (a : B) → C) 1 : C) = 1
have rw : HMul.hMul (α := C) (β := C) (1 : C) ((g : (a : B) → C) 1 : C) = 1
Tactic: rw [map_one, map_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Maps (goal)
Goal:
R : Type uR
R' : Type u_1
S : Type uS
T : Type u_2
A : Type uA
B : Type uB
C : Type uC
D : Type uD
E : Type uE
F : Type uF
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : Semiring A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
inst_7 : Semiring B
inst_8 : Algebra R B
inst_9 : Semiring C
inst_10 : Algebra S C
inst_11 : Semiring D
inst_12 : Algebra R D
inst_13 : Algebra R C
inst_14 : IsScalarTower R S C
f : A →ₐ[S] C
g : B →ₐ[R] C
hfg : ∀ (x : A) (y : B), Commute.{uC} (S := C) ((f : (a : A) → C) x : C) ((g : (a : B) → C) y : C)
rw : HMul.hMul (α := C) (β := C) (1 : C) ((g : (a : B) → C) 1 : C) = 1
⊢ HMul.hMul (α := C) (β := C) ((f : (a : A) → C) 1 : C) ((g : (a : B) → C) 1 : C) = 1
have rw₁ : HMul.hMul (α := C) 1 1 = 1
Tactic: rw [map_one, map_one, one_mul]