-- Lean 4 proof step from Mathlib.LinearAlgebra.TensorProduct.Graded.Internal (goal)
Goal:
R : Type u_1
ι : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring ι
inst_1 : DecidableEq ι
inst_2 : CommRing R
inst_3 : Ring A
inst_4 : Ring B
inst_5 : Algebra R A
inst_6 : Algebra R B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
inst_7 : GradedAlgebra 𝒜
inst_8 : GradedAlgebra ℬ
inst_9 : Module ι (Additive ℤˣ)
C : Type u_5
inst_10 : Ring C
inst_11 : Algebra R C
F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C
⊢ (fun
          (fg :
            { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
              ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C) ((fg.2 : (a : B) → C) (↑b : B) : C) =
                  HPow.hPow (α := ℤˣ) (-1) (j * i) •
                    HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                      ((fg.1 : (a : A) → C) (↑a : A) : C) }) ↦
        (lift 𝒜 ℬ (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 ⋯ : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C))
      ((fun (F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C) ↦
          (Subtype.mk (p := fun (fg : (A →ₐ[R] C) × (B →ₐ[R] C)) ↦
              ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C) ((fg.2 : (a : B) → C) (↑b : B) : C) =
                  HPow.hPow (α := ℤˣ) (-1) (j * i) •
                    HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C) ((fg.1 : (a : A) → C) (↑a : A) : C))
              (F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)) ⋯ :
            { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
              ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C) ((fg.2 : (a : B) → C) (↑b : B) : C) =
                  HPow.hPow (α := ℤˣ) (-1) (j * i) •
                    HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                      ((fg.1 : (a : A) → C) (↑a : A) : C) }))
        F) =
    F
have a : AlgHom.toLinearMap
    ((fun
          (fg :
            { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
              ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C) ((fg.2 : (a : B) → C) (↑b : B) : C) =
                  HPow.hPow (α := ℤˣ) (-1) (j * i) •
                    HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                      ((fg.1 : (a : A) → C) (↑a : A) : C) }) ↦
        (lift 𝒜 ℬ (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).1 (↑fg : (A →ₐ[R] C) × (B →ₐ[R] C)).2 sorry : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C))
      ((fun (F : 𝒜 ᵍ⊗[R] ℬ →ₐ[R] C) ↦
          (Subtype.mk (p := fun (fg : (A →ₐ[R] C) × (B →ₐ[R] C)) ↦
              ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C) ((fg.2 : (a : B) → C) (↑b : B) : C) =
                  HPow.hPow (α := ℤˣ) (-1) (j * i) •
                    HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C) ((fg.1 : (a : A) → C) (↑a : A) : C))
              (F.comp (includeLeft 𝒜 ℬ), F.comp (includeRight 𝒜 ℬ)) sorry :
            { fg : (A →ₐ[R] C) × (B →ₐ[R] C) //
              ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)),
                HMul.hMul (α := C) (β := C) ((fg.1 : (a : A) → C) (↑a : A) : C) ((fg.2 : (a : B) → C) (↑b : B) : C) =
                  HPow.hPow (α := ℤˣ) (-1) (j * i) •
                    HMul.hMul (α := C) (β := C) ((fg.2 : (a : B) → C) (↑b : B) : C)
                      ((fg.1 : (a : A) → C) (↑a : A) : C) }))
        F)) =
  F.toLinearMap
Tactic: apply AlgHom.toLinearMap_injective