-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.TensorProduct (goal)
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
A : Type u_4
B : Type u_5
inst : DecidableEq ι
inst_1 : AddMonoid ι
inst_2 : CommSemiring R
inst_3 : CommSemiring S
inst_4 : Semiring A
inst_5 : Semiring B
inst_6 : Algebra R A
inst_7 : Algebra S B
𝒜 : ι → Submodule R A
ℬ : ι → Submodule S B
inst_8 : GradedAlgebra 𝒜
inst_9 : GradedAlgebra ℬ
inst_10 : Algebra R S
inst_11 : Algebra R B
inst_12 : IsScalarTower R S B
f : GradedAlgHom.{u_2, u_4, u_5, u_1} R (B := B) 𝒜 fun (x : ι) ↦ Submodule.restrictScalars R (ℬ x)
i : ι
x : TensorProduct.{u_2, u_3, u_4} R S ↥(𝒜 i)
hx :
  Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
    (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A)
zero :
  ∀
    (hx :
      Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) 0) : S ⊗[R] A)),
    Membership.mem (α := B) (ℬ i)
      ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
            (a : S ⊗[R] A) → B)
          (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) 0) : S ⊗[R] A) :
        B)
add :
  ∀ (x y : TensorProduct.{u_2, u_3, u_4} R S ↥(𝒜 i)),
    (∀
        (hx :
          Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
            (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A)),
        Membership.mem (α := B) (ℬ i)
          ((AlgHom.toRingHom (R := S)
                  ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
                (a : S ⊗[R] A) → B)
              (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A) :
            B)) →
      (∀
          (hx :
            Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
              (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) y) : S ⊗[R] A)),
          Membership.mem (α := B) (ℬ i)
            ((AlgHom.toRingHom (R := S)
                    ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
                  (a : S ⊗[R] A) → B)
                (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) y) : S ⊗[R] A) :
              B)) →
        ∀
          (hx :
            Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
              (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (x + y)) : S ⊗[R] A)),
          Membership.mem (α := B) (ℬ i)
            ((AlgHom.toRingHom (R := S)
                    ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
                  (a : S ⊗[R] A) → B)
                (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (x + y)) : S ⊗[R] A) :
              B)
⊢ Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) x) : S ⊗[R] A) :
      B)
have tmul : ∀ (r : S) (x : ↥(𝒜 i))
  (hx :
    Membership.mem (γ := Submodule S (S ⊗[R] A)) (baseChange S (𝒜 i))
      (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (r ⊗ₜ[R] x)) : S ⊗[R] A)),
  Membership.mem (α := B) (ℬ i)
    ((AlgHom.toRingHom (R := S) ((AlgHom.liftEquiv R S A B : (a : A →ₐ[R] B) → S ⊗[R] A →ₐ[S] B) (↑f : A →ₐ[R] B)) :
          (a : S ⊗[R] A) → B)
        (↑((toBaseChange S (𝒜 i) : (a : S ⊗[R] ↥(𝒜 i)) → ↥(baseChange S (𝒜 i))) (r ⊗ₜ[R] x)) : S ⊗[R] A) :
      B)
Tactic: induction x with
        | zero => simp
        | add => simp_all [add_mem]
        | tmul r x => simpa using smul_mem _ _ <| by exact f.map_mem x.2
Cleared hypotheses: x, hx