-- Lean 4 proof step from Mathlib.RingTheory.Grassmannian (goal)
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
f : A →ₐ[R] B
C : Type w
inst_7 : CommRing C
inst_8 : Algebra R C
g : B →ₐ[R] C
N : G(k, A ⊗[R] M; A)
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
this : IsScalarTower A B C := ⋯
fAB : B ⊗[R] M →ₗ[B] B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ B N.toSubmodule
fAC : C ⊗[R] M →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) := baseChangeMkQ C N.toSubmodule
fBC : C ⊗[R] M →ₗ[C] C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) := baseChangeMkQ C fAB.ker
hfAB :
  Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule) :=
  LinearEquiv.baseChange B C (B ⊗[R] M ⧸ fAB.ker) (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (fAB.quotKerEquivOfSurjective hfAB) ≪≫ₗ
    cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule)
x_1 : C ⊗[R] M
hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker
hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker
x y : C ⊗[R] M
hx :
  Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) x : C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (((↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC :
          (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
        x :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
hy :
  Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) y : C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (((↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC :
          (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
        y :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
⊢ Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (x + y) : C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (((↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC :
          (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
        (x + y) :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
have h : HAdd.hAdd (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (β := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) x : C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) y : C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) =
  HAdd.hAdd (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (β := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((e : (a : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker)) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
        ((fBC : (a : C ⊗[R] M) → C ⊗[B] (B ⊗[R] M ⧸ fAB.ker)) x) :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((e : (a : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker)) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
        ((fBC : (a : C ⊗[R] M) → C ⊗[B] (B ⊗[R] M ⧸ fAB.ker)) y) :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
Tactic: simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_add] at *