-- Module: Mathlib.RingTheory.Grassmannian
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 : 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
z : C ⊗[R] M
h :
  Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) 0)
    (((↑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))
      0)
h₁ :
  ∀ (c : C) (m : M),
    Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (c ⊗ₜ[R] m) : 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))
          (c ⊗ₜ[R] m) :
        C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
h₂ :
  ∀ (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))
⊢ Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    ((fAC : (a : C ⊗[R] M) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) z : 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))
        z :
      C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))

Tactic:
induction z using TensorProduct.induction_on with
    | zero => simp [fAC, fBC, e]
    | tmul c m =>
      simp only [fAC, fBC, e, baseChangeMkQ, LinearMap.comp_apply, cancelBaseChange_symm_tmul,
         LinearMap.baseChange_tmul, Submodule.mkQ_apply, LinearEquiv.coe_trans, LinearEquiv.coe_coe,
         LinearEquiv.coe_baseChange, LinearMap.quotKerEquivOfSurjective_apply_mk]
      simp [fAB, baseChangeMkQ]
    | add x y hx hy =>
      simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, map_add] at *
      rw [hx, hy]

Premises used: LinearEquiv.coe_baseChange, Module.Grassmannian.baseChangeMkQ, LinearMap.comp_apply, map_add, Submodule.mkQ_apply, LinearMap.coe_comp, TensorProduct.AlgebraTensorModule.cancelBaseChange_symm_tmul, Function.comp_apply, TensorProduct.tmul, LinearEquiv.coe_trans, LinearMap.baseChange_tmul, LinearMap.quotKerEquivOfSurjective_apply_mk, LinearEquiv.coe_coe