awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
k : ℕ
toSubmodule : Submodule R M
finite_quotient : Module.Finite.{u, v} R (M ⧸ toSubmodule)
projective_quotient : Projective.{u, v} R (M ⧸ toSubmodule)
rankAtStalk_eq : ∀ (p : PrimeSpectrum R), rankAtStalk.{u, v} (M ⧸ toSubmodule) p = k
toSubmodule_1 : Submodule R M
finite_quotient_1 : Module.Finite.{u, v} R (M ⧸ toSubmodule_1)
projective_quotient_1 : Projective.{u, v} R (M ⧸ toSubmodule_1)
rankAtStalk_eq_1 : ∀ (p : PrimeSpectrum R), rankAtStalk.{u, v} (M ⧸ toSubmodule_1) p = k
h :
  { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
        rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) }.toSubmodule =
    { toSubmodule := toSubmodule_1, finite_quotient := finite_quotient_1, projective_quotient := projective_quotient_1,
        rankAtStalk_eq := rankAtStalk_eq_1 : G(k, M; R) }.toSubmodule
⊢ { toSubmodule := toSubmodule, finite_quotient := finite_quotient, projective_quotient := projective_quotient,
      rankAtStalk_eq := rankAtStalk_eq : G(k, M; R) } =
    { toSubmodule := toSubmodule_1, finite_quotient := finite_quotient_1, projective_quotient := projective_quotient_1,
      rankAtStalk_eq := rankAtStalk_eq_1 }

Tactic:
congr 1
-- Module: Mathlib.RingTheory.Grassmannian
Goal:
R : Type u
inst : CommRing R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
A : Type w
inst_3 : CommRing A
inst_4 : Algebra R A
B : Type w
inst_5 : CommRing B
inst_6 : Algebra R B
inst_7 : Algebra A B
inst_8 : IsScalarTower R A B
N : Submodule A (A ⊗[R] M)
⊢ Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N))
    (⇑(baseChangeMkQ B N) : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N))

Tactic:
(LinearMap.baseChange_surjective B (Submodule.mkQ_surjective _)).comp
    (cancelBaseChange R A B B M).symm.surjective

Premises used: TensorProduct.AlgebraTensorModule.cancelBaseChange, LinearEquiv.symm, Quotient.liftOn', AddCon.liftOn, LinearMap.baseChange_surjective, LinearEquiv.surjective, Function.Surjective.comp
-- 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
N : G(k, A ⊗[R] M; A)
this_1 : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := ⋯
equiv :
  HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
      (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)) ≃ₗ[B]
    B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
⊢ rankAtStalk
      (HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
        (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
      p =
    rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p

Tactic:
simpa using congrArg (fun g => g p) <| Module.rankAtStalk_eq_of_equiv equiv

Premises used: congrArg, Module.rankAtStalk_eq_of_equiv
-- 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
N : G(k, A ⊗[R] M; A)
this_1 : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := ⋯
equiv :
  HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
      (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)) ≃ₗ[B]
    B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
⊢ rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p =
    rankAtStalk (A ⊗[R] M ⧸ N.toSubmodule) (PrimeSpectrum.comap (algebraMap A B) p)

Tactic:
simpa using Module.rankAtStalk_baseChange ..

Premises used: Module.rankAtStalk_baseChange
-- 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
N : G(k, A ⊗[R] M; A)
this_1 : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := ⋯
equiv :
  HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
      (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)) ≃ₗ[B]
    B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
⊢ rankAtStalk (A ⊗[R] M ⧸ N.toSubmodule) (PrimeSpectrum.comap (algebraMap A B) p) = k

Tactic:
N.rankAtStalk_eq _

Premises used: Module.Grassmannian.rankAtStalk_eq
-- 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
N : G(k, A ⊗[R] M; A)
this_1 : Algebra A B := f.toAlgebra
this : IsScalarTower R A B := ⋯
equiv :
  HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
      (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)) ≃ₗ[B]
    B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)
p : PrimeSpectrum B
_ :
  rankAtStalk
      (HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
        (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
      p =
    rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p
_₁ :
  rankAtStalk (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) p =
    rankAtStalk (A ⊗[R] M ⧸ N.toSubmodule) (PrimeSpectrum.comap (algebraMap A B) p)
⊢ rankAtStalk
      (HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
        (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
      p =
    k

Tactic:
calc
        _ = rankAtStalk (R := B) (B ⊗[A] ((A ⊗[R] M) ⧸ N.toSubmodule)) p := by
          simpa using congrArg (fun g => g p) <| Module.rankAtStalk_eq_of_equiv equiv
        _ = rankAtStalk (R := A) (A ⊗[R] M ⧸ N.toSubmodule)
            (PrimeSpectrum.comap (algebraMap A B) p) := by
          simpa using Module.rankAtStalk_baseChange ..
        _ = k := N.rankAtStalk_eq _

Premises used: Module.rankAtStalk, Algebra.algebraMap, Module.Grassmannian.rankAtStalk_eq, HasQuotient.Quotient, Module.Grassmannian.toSubmodule, TensorProduct, PrimeSpectrum.comap
-- 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
N : G(k, A ⊗[R] M; A)
⊢ (map f N).toSubmodule = LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)

Tactic:
rfl
-- 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 : CommAlgCat.{u_1, u} R
N : G(k, TensorProduct.{u, u_1, v} R (↑A : Type u_1) M; (↑A : Type u_1))
h : (map (AlgHom.id R (↑A : Type u_1)) N).toSubmodule = N.toSubmodule
⊢ map (AlgHom.id R (↑A : Type u_1)) N = N

Tactic:
ext : 1
-- 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 : CommAlgCat.{u_1, u} R
N : G(k, TensorProduct.{u, u_1, v} R (↑A : Type u_1) M; (↑A : Type u_1))
⊢ (map (AlgHom.id R (↑A : Type u_1)) N).toSubmodule = N.toSubmodule

Tactic:
(ker_baseChange_comp_cancelBaseChange_symm N.mkQ).trans N.toSubmodule.ker_mkQ

Premises used: TensorProduct.AlgebraTensorModule.ker_baseChange_comp_cancelBaseChange_symm, LinearMap.ker, Submodule.comap, Module.Grassmannian.toSubmodule, Submodule.mkQ, Submodule.ker_mkQ, Eq.trans
-- 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 : CommAlgCat.{u_1, u} R
N : G(k, TensorProduct.{u, u_1, v} R (↑A : Type u_1) M; (↑A : Type u_1))
⊢ (map (AlgHom.id R (↑A : Type u_1)) N).toSubmodule = N.toSubmodule

Tactic:
exact (ker_baseChange_comp_cancelBaseChange_symm N.mkQ).trans N.toSubmodule.ker_mkQ

Premises used: TensorProduct.AlgebraTensorModule.ker_baseChange_comp_cancelBaseChange_symm, Module.Grassmannian.toSubmodule, Submodule.mkQ, Submodule.ker_mkQ, Eq.trans
-- 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
h :
  Eq (α := A →+* C) (algebraMap A C)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap A B))
⊢ IsScalarTower A B C

Tactic:
apply IsScalarTower.of_algebraMap_eq'

Premises used: IsScalarTower.of_algebraMap_eq'
-- 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
⊢ Eq (α := A →+* C) (algebraMap A C)
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap B C) (algebraMap A B))

Tactic:
rfl
-- 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
⊢ Function.Surjective (α := B ⊗[R] M) (β := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
    (⇑fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))

Tactic:
have hfAB : Function.Surjective fAB :=
    (LinearMap.baseChange_surjective B (Submodule.mkQ_surjective _)).comp
      (cancelBaseChange R A B B M).symm.surjective
-- 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)
h : ∀ (x : C ⊗[R] M), x ∈ (map (g.comp f) N).toSubmodule ↔ x ∈ (map g (map f N)).toSubmodule
⊢ map (g.comp f) N = map g (map f N)

Tactic:
ext x
-- 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
⊢ (map (g.comp f) N).toSubmodule = fAC.ker

Tactic:
have hfAC_ker_eq : (map (g.comp f) N).toSubmodule = fAC.ker := map_toSubmodule (g.comp f) N
-- 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
rw : LinearMap.ker (M₂ := C ⊗[B] (B ⊗[R] M ⧸ (map f N).toSubmodule)) (baseChangeMkQ C (map f N).toSubmodule) = fBC.ker
rw₁ rw₂ :
  LinearMap.ker (M₂ :=
      C ⊗[B]
        HasQuotient.Quotient (B ⊗[R] M) (B := Submodule B (B ⊗[R] M))
          (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule)))
      (baseChangeMkQ C (LinearMap.ker (M₂ := B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (baseChangeMkQ B N.toSubmodule))) =
    fBC.ker
⊢ (map g (map f N)).toSubmodule = fBC.ker

Tactic:
rw [map_toSubmodule g (map f N), map_toSubmodule f N]

Premises used: Module.Grassmannian.map, Module.Grassmannian.map_toSubmodule
-- 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
⊢ (map g (map f N)).toSubmodule = fBC.ker

Tactic:
have hfBC_ker_eq : (map g (map f N)).toSubmodule = fBC.ker := by
    rw [map_toSubmodule g (map f N), map_toSubmodule f N]
-- 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
h :
  ∀ (x : C ⊗[R] M),
    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))
⊢ fAC = (↑e : C ⊗[B] (B ⊗[R] M ⧸ fAB.ker) →ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ∘ₗ fBC

Tactic:
apply LinearMap.ext

Premises used: LinearMap.ext
-- 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
⊢ 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)

Tactic:
simp [fAC, fBC, e]
-- 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
c : C
m : M
h :
  Eq (α := C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (c ⊗ₜ[A] Submodule.Quotient.mk (1 ⊗ₜ[R] m))
    (((cancelBaseChange A B C C (A ⊗[R] M ⧸ N.toSubmodule) :
          C ⊗[B] (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) ≃ₗ[C] C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) :
        (a : C ⊗[B] (B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))) → C ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule))
      (c ⊗ₜ[B] (fAB : (a : B ⊗[R] M) → B ⊗[A] (A ⊗[R] M ⧸ N.toSubmodule)) (1 ⊗ₜ[R] 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))

Tactic:
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]

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