awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
a : A
b : B
z w : A ⊗[R] B
hz : (z * a ⊗ₜ[R] b) • m = z • HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m
hw : (w * a ⊗ₜ[R] b) • m = w • HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m
⊢ ((z + w) * a ⊗ₜ[R] b) • m = (z + w) • HSMul.hSMul (α := A ⊗[R] B) (a ⊗ₜ[R] b) m
have refine_3 : Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((z + w) * a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M)
  ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M)
      ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (a ⊗ₜ[R] b) : M →ₗ[R] M) : (a : M) → M) m : M) :
    M)
Tactic: simp only [(· • ·)] at hz hw ⊢
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
x y : A ⊗[R] B
m : M
u v : A ⊗[R] B
h : ∀ (x y : A ⊗[R] B), (x * u) • m = x • u • m → (y * u) • m = y • u • m → ((x + y) * u) • m = (x + y) • u • m
h_1 : ∀ (x y : A ⊗[R] B), (x * v) • m = x • v • m → (y * v) • m = y • v • m → ((x + y) * v) • m = (x + y) • v • m
z w : A ⊗[R] B
hz : (z * (u + v)) • m = z • (u + v) • m
hw : (w * (u + v)) • m = w • (u + v) • m
⊢ ((z + w) * (u + v)) • m = (z + w) • (u + v) • m
have refine_3 : Eq (α := M) ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) ((z + w) * (u + v)) : M →ₗ[R] M) : (a : M) → M) m : M)
  ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (z + w) : M →ₗ[R] M) : (a : M) → M)
      ((((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (u + v) : M →ₗ[R] M) : (a : M) → M) m : M) :
    M)
Tactic: simp only [(· • ·)] at hz hw ⊢
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Module A M
inst_6 : Module B M
inst_7 : Algebra R A
inst_8 : Algebra R B
inst_9 : IsScalarTower R A M
inst_10 : IsScalarTower R B M
inst_11 : SMulCommClass A B M
m : M
⊢ HSMul.hSMul (α := A ⊗[R] B) 1 m = m
have simp : (((moduleAux : (a : A ⊗[R] B) → M →ₗ[R] M) (1 ⊗ₜ[R] 1) : M →ₗ[R] M) : (a : M) → M) m = m
Tactic: simp only [(· • ·), Algebra.TensorProduct.one_def]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
⊢ Eq (α := R ⊗[R] R →ₗ[R] A ⊗[R] B) (Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R)
    (map (Algebra.linearMap R A) (Algebra.linearMap R B))
have a : Eq (α := A ⊗[R] B)
  ((((AlgebraTensorModule.curry (Algebra.linearMap R (A ⊗[R] B) ∘ₗ LinearMap.mul' R R) : R →ₗ[R] R →ₗ[R] A ⊗[R] B) :
          (a : R) → R →ₗ[R] A ⊗[R] B)
        1 :
      (a : R) → A ⊗[R] B)
    1)
  ((((AlgebraTensorModule.curry (map (Algebra.linearMap R A) (Algebra.linearMap R B)) : R →ₗ[R] R →ₗ[R] A ⊗[R] B) :
          (a : R) → R →ₗ[R] A ⊗[R] B)
        1 :
      (a : R) → A ⊗[R] B)
    1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
⊢ map (↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) (range (rTensor Q I.subtype)) = HSMul.hSMul (β := Submodule R Q) I ⊤
have rw : range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype) = HSMul.hSMul (β := Submodule R Q) I ⊤
Tactic: rw [← map_top, ← Submodule.map_comp, map_top]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
Q : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid Q
inst_2 : Module R Q
I : Submodule R R
⊢ range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype) = HSMul.hSMul (β := Submodule R Q) I ⊤
have refine : range ((↑(TensorProduct.lid R Q) : R ⊗[R] Q →ₗ[R] Q) ∘ₗ rTensor Q I.subtype) ≤ HSMul.hSMul (β := Submodule R Q) I ⊤
Tactic: refine le_antisymm ?_ fun q h ↦ Submodule.smul_induction_on h
    (fun r hr q _ ↦ ⟨⟨r, hr⟩ ⊗ₜ q, by simp⟩) (by simp +contextual [add_mem])
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ Function.Surjective (α := M) (β := S ⊗[R] M) (⇑((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1) : (a : M) → S ⊗[R] M)
have rw : {t : S ⊗[R] M | ∃ (m : S) (n : M), m ⊗ₜ[R] n = t} ⊆
  (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
    Set (S ⊗[R] M))
Tactic: rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
x : S
y : M
⊢ x ⊗ₜ[R] y ∈
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))
have obtain : ∀ (x : R),
  Membership.mem (α := S ⊗[R] M)
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))
    ((algebraMap R S : (a : R) → S) x ⊗ₜ[R] y : S ⊗[R] M)
Tactic: obtain ⟨x, rfl⟩ := h x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
M : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Semiring S
inst_4 : Algebra R S
h : Function.Surjective.{u_1 + 1, u_3 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
y : M
x : R
⊢ Membership.mem (α := S ⊗[R] M)
    (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
      Set (S ⊗[R] M))
    ((algebraMap R S : (a : R) → S) x ⊗ₜ[R] y : S ⊗[R] M)
have rw : 1 ⊗ₜ[R] (x • y) ∈
  (↑(LinearMap.range (R := R) (M := M) (τ₁₂ := RingHom.id R) ((mk R S M : (a : S) → M →ₗ[R] S ⊗[R] M) 1)) :
    Set (S ⊗[R] M))
Tactic: rw [Algebra.algebraMap_eq_smul_one, smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
⊢ Function.Surjective (α := S) (β := S ⊗[R] T)
    (⇑((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1) : (a : S) → S ⊗[R] T)
have rw : {t : S ⊗[R] T | ∃ (m : S) (n : T), m ⊗ₜ[R] n = t} ⊆
  (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
        ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
    Set (S ⊗[R] T))
Tactic: rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
s : S
t : T
⊢ s ⊗ₜ[R] t ∈
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))
have obtain : ∀ (r : R),
  Membership.mem (α := S ⊗[R] T)
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))
    (s ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)
Tactic: obtain ⟨r, rfl⟩ := h t
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
S : Type u_3
T : Type u_4
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : Algebra R S
inst_3 : Ring T
inst_4 : Algebra R T
h : Function.Surjective.{u_1 + 1, u_4 + 1} (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)
s : S
r : R
⊢ Membership.mem (α := S ⊗[R] T)
    (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
          ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
      Set (S ⊗[R] T))
    (s ⊗ₜ[R] (algebraMap R T : (a : R) → T) r : S ⊗[R] T)
have rw : (r • s) ⊗ₜ[R] 1 ∈
  (↑(LinearMap.range (R := R) (M := S) (τ₁₂ := RingHom.id R)
        ((LinearMap.flip (mk R S T) : (a : T) → S →ₗ[R] S ⊗[R] T) 1)) :
    Set (S ⊗[R] T))
Tactic: rw [Algebra.algebraMap_eq_smul_one, ← smul_tmul]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
⊢ Eq (α := TensorProduct.{u_1, u_2, u_3} R (A ⊗[R] A) (B ⊗[R] B) →ₗ[R] A ⊗[R] B)
    (LinearMap.mul' R (A ⊗[R] B) ∘ₗ
        (↑(tensorTensorTensorComm R A A B B) : A ⊗[R] A ⊗[R] (B ⊗[R] B) →ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)) :
      TensorProduct.{u_1, u_2, u_3} R (A ⊗[R] A) (B ⊗[R] B) →ₗ[R] A ⊗[R] B)
    (map (LinearMap.mul' R A) (LinearMap.mul' R B) :
      TensorProduct.{u_1, u_2, u_3} R (A ⊗[R] A) (B ⊗[R] B) →ₗ[R] A ⊗[R] B)
have a : ∀ (x x_1 : A) (x_2 x_3 : B),
  Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (AlgebraTensorModule.curry
                                    (LinearMap.mul' R (A ⊗[R] B) ∘ₗ
                                      (↑(tensorTensorTensorComm R A A B B) :
                                        A ⊗[R] A ⊗[R] (B ⊗[R] B) →ₗ[R] A ⊗[R] B ⊗[R] (A ⊗[R] B)))) :
                                A →ₗ[R] A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                              (a : A) → A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B)
                            x :
                          A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                        (a : A) → B ⊗[R] B →ₗ[R] A ⊗[R] B)
                      x_1) :
                  B →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : B) → B →ₗ[R] A ⊗[R] B)
              x_2 :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_3 :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry
                    (((((AlgebraTensorModule.curry
                                  (AlgebraTensorModule.curry (map (LinearMap.mul' R A) (LinearMap.mul' R B))) :
                                A →ₗ[R] A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                              (a : A) → A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B)
                            x :
                          A →ₗ[R] B ⊗[R] B →ₗ[R] A ⊗[R] B) :
                        (a : A) → B ⊗[R] B →ₗ[R] A ⊗[R] B)
                      x_1) :
                  B →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : B) → B →ₗ[R] A ⊗[R] B)
              x_2 :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_3 :
      A ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
a : A
b : B
⊢ Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B) (mulLeft R (A := A ⊗[R] B) (a ⊗ₜ[R] b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (map (mulLeft R a) (mulLeft R b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
have a₁ : ∀ (x : A) (x_1 : B),
  Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry (mulLeft R (A := A ⊗[R] B) (a ⊗ₜ[R] b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              x :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_1 :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry (map (mulLeft R a) (mulLeft R b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              x :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_1 :
      A ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Module R A
inst_4 : Module R B
inst_5 : SMulCommClass R A A
inst_6 : SMulCommClass R B B
inst_7 : IsScalarTower R A A
inst_8 : IsScalarTower R B B
a : A
b : B
⊢ Eq (α := A ⊗[R] B →ₗ[R] A ⊗[R] B) (mulRight R (A := A ⊗[R] B) (a ⊗ₜ[R] b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
    (map (mulRight R a) (mulRight R b) : A ⊗[R] B →ₗ[R] A ⊗[R] B)
have a₁ : ∀ (x : A) (x_1 : B),
  Eq (α := A ⊗[R] B)
    (((((AlgebraTensorModule.curry (mulRight R (A := A ⊗[R] B) (a ⊗ₜ[R] b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              x :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_1 :
      A ⊗[R] B)
    (((((AlgebraTensorModule.curry (map (mulRight R a) (mulRight R b)) : A →ₗ[R] B →ₗ[R] A ⊗[R] B) :
                (a : A) → B →ₗ[R] A ⊗[R] B)
              x :
            B →ₗ[R] A ⊗[R] B) :
          (a : B) → A ⊗[R] B)
        x_1 :
      A ⊗[R] B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ (LinearMap.liftBaseChange S
          (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
        (a : S ⊗[R] A) → B)
      (x * y) =
    HMul.hMul (α := B) (β := B)
      ((LinearMap.liftBaseChange S
              (↑f :
                [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : S ⊗[R] A) → B)
          x :
        B)
      ((LinearMap.liftBaseChange S
              (↑f :
                [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B) :
            (a : S ⊗[R] A) → B)
          y :
        B)
have rw : Eq.{u_7 + 1} (α := B)
  ((((LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
                (LinearMap.liftBaseChange S
                  (↑f :
                    [inst : FunLike (A →ₐ[R] B) A B] →
                      [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
              (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] B)
            x :
          S ⊗[R] A →ₗ[S] B) :
        (a : S ⊗[R] A) → B)
      y :
    B)
  ((((LinearMap.compl₁₂ (LinearMap.mul S B)
                (LinearMap.liftBaseChange S
                  (↑f :
                    [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                (LinearMap.liftBaseChange S
                  (↑f :
                    [inst : FunLike (A →ₐ[R] B) A B] →
                      [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
              (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] B)
            x :
          S ⊗[R] A →ₗ[S] B) :
        (a : S ⊗[R] A) → B)
      y :
    B)
Tactic: rw [← LinearMap.mul_apply_apply S, ← LinearMap.compr₂_apply,
        ← LinearMap.mul_apply_apply S, ← LinearMap.compl₁₂_apply]
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
x y : S ⊗[R] A
⊢ Eq.{u_7 + 1} (α := B)
    ((((LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
                (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] B)
              x :
            S ⊗[R] A →ₗ[S] B) :
          (a : S ⊗[R] A) → B)
        y :
      B)
    ((((LinearMap.compl₁₂ (LinearMap.mul S B)
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                  (LinearMap.liftBaseChange S
                    (↑f :
                      [inst : FunLike (A →ₐ[R] B) A B] →
                        [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)) :
                (a : S ⊗[R] A) → S ⊗[R] A →ₗ[S] B)
              x :
            S ⊗[R] A →ₗ[S] B) :
          (a : S ⊗[R] A) → B)
        y :
      B)
have e_a : Eq (α := S ⊗[R] A →ₗ[S] S ⊗[R] A →ₗ[S] B)
  (LinearMap.compr₂ (LinearMap.mul S (S ⊗[R] A))
    (LinearMap.liftBaseChange S
      (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)))
  (LinearMap.compl₁₂ (LinearMap.mul S B)
    (LinearMap.liftBaseChange S
      (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
    (LinearMap.liftBaseChange S
      (↑f : [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B)))
Tactic: congr
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : A →ₐ[R] B
⊢ (fun (f : S ⊗[R] A →ₐ[S] B) ↦ (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
      ((fun (f : A →ₐ[R] B) ↦
          (ofLinearMap
              (LinearMap.liftBaseChange S
                (↑f :
                  [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
              ⋯ ⋯ :
            S ⊗[R] A →ₐ[S] B))
        f) =
    f
have H : ∀ (x : A),
  Eq.{u_7 + 1} (α := B)
    (((fun (f : S ⊗[R] A →ₐ[S] B) ↦ (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
            ((fun (f : A →ₐ[R] B) ↦
                (ofLinearMap
                    (LinearMap.liftBaseChange S
                      (↑f :
                        [inst : FunLike (A →ₐ[R] B) A B] →
                          [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                    sorry sorry :
                  S ⊗[R] A →ₐ[S] B))
              f) :
          (a : A) → B)
        x :
      B)
    ((f : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.Basic (goal)
Goal:
R_1 : Type u_1
A_1 : Type u_2
B_1 : Type u_3
inst : CommSemiring R_1
inst_1 : NonUnitalNonAssocSemiring A_1
inst_2 : NonUnitalNonAssocSemiring B_1
inst_3 : Module R_1 A_1
inst_4 : Module R_1 B_1
inst_5 : SMulCommClass R_1 A_1 A_1
inst_6 : SMulCommClass R_1 B_1 B_1
inst_7 : IsScalarTower R_1 A_1 A_1
inst_8 : IsScalarTower R_1 B_1 B_1
R : Type u_4
S : Type u_5
A : Type u_6
B : Type u_7
inst_9 : CommSemiring R
inst_10 : CommSemiring S
inst_11 : Semiring A
inst_12 : Semiring B
inst_13 : Algebra R A
inst_14 : Algebra S B
inst_15 : Algebra R S
inst_16 : Algebra R B
inst_17 : IsScalarTower R S B
f : S ⊗[R] A →ₐ[S] B
⊢ Eq (α := A →ₐ[R] B)
    (comp (B := S ⊗[R] A)
      (restrictScalars R (S := S)
        ((fun (f : A →ₐ[R] B) ↦
            (ofLinearMap
                (LinearMap.liftBaseChange S
                  (↑f :
                    [inst : FunLike (A →ₐ[R] B) A B] → [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                ⋯ ⋯ :
              S ⊗[R] A →ₐ[S] B))
          ((fun (f : S ⊗[R] A →ₐ[S] B) ↦ (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
            f)))
      Algebra.TensorProduct.includeRight)
    (comp (restrictScalars R f) Algebra.TensorProduct.includeRight)
have H : ∀ (x : A),
  Eq.{u_7 + 1} (α := B)
    ((comp (B := S ⊗[R] A)
            (restrictScalars R (S := S)
              ((fun (f : A →ₐ[R] B) ↦
                  (ofLinearMap
                      (LinearMap.liftBaseChange S
                        (↑f :
                          [inst : FunLike (A →ₐ[R] B) A B] →
                            [SemilinearMapClass (A →ₐ[R] B) (RingHom.id R) A B] → A →ₗ[R] B))
                      sorry sorry :
                    S ⊗[R] A →ₐ[S] B))
                ((fun (f : S ⊗[R] A →ₐ[S] B) ↦
                    (comp (restrictScalars R f) Algebra.TensorProduct.includeRight : A →ₐ[R] B))
                  f)))
            Algebra.TensorProduct.includeRight :
          (a : A) → B)
        x :
      B)
    ((comp (restrictScalars R f) Algebra.TensorProduct.includeRight : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.TensorProduct.DirectLimitFG (goal)
Goal:
R : Type u
N : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
ι : Type u_3
inst_3 : Preorder ι
F : ι → Type u_4
inst_4 : (i : ι) → AddCommMonoid (F i)
inst_5 : (i : ι) → Module.{u, u_4} R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun (x x_1 : ι) (h : x ≤ x_1) ↦ (⇑(f h) : (a : F x) → F x_1)
i : ι
t : TensorProduct.{u, u_4, u_2} R (F i) N
⊢ (LinearMap.rTensor N (f ⋯) : (a : F i ⊗[R] N) → F i ⊗[R] N) t = t
have rw : Eq (α := TensorProduct.{u, u_4, u_2} R (F i) N)
  ((LinearMap.rTensor N (f sorry) : (a : F i ⊗[R] N) → F i ⊗[R] N) ((LinearMap.id : (a : F i ⊗[R] N) → F i ⊗[R] N) t) :
    TensorProduct.{u, u_4, u_2} R (F i) N)
  ((LinearMap.id : (a : F i ⊗[R] N) → F i ⊗[R] N) t : TensorProduct.{u, u_4, u_2} R (F i) N)
Tactic: rw [← id_apply (R := R) t]