Theorem: PolynomialMap.toFun'_eq_of_diagram (DividedPowers/PolynomialMap/Basic.lean)

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (LinearMap.rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)
Tactic:
let θ := (Ideal.quotientKerEquivRange (R := R) ψ).symm.toAlgHom.comp
  (h'.comp (Ideal.quotientKerEquivRange φ).toAlgHom)
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ (LinearMap.rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ (LinearMap.rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)
Tactic:
have ht : h.comp (φ.range.val.comp (Ideal.quotientKerEquivRange φ).toAlgHom) =
    ψ.range.val.comp ((Ideal.quotientKerEquivRange ψ).toAlgHom.comp θ) := by
  simp only [θ, ← AlgHom.comp_assoc, ← hh']
  apply congr_arg₂ _ _ rfl
  apply congr_arg₂ _ _ rfl
  simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.comp_id]
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N (h.comp φ).toLinearMap) (f.toFun' A p) = (LinearMap.rTensor N ψ.toLinearMap) (f.toFun' B q)
Tactic:
simp only [φ.factor, ψ.factor, ← AlgHom.comp_assoc]
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N
        (((h.comp φ.range.val).comp ↑(Ideal.quotientKerEquivRange φ)).comp
            (Ideal.Quotient.mkₐ R (RingHom.ker φ))).toLinearMap)
      (f.toFun' A p) =
    (LinearMap.rTensor N
        ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker ψ))).toLinearMap)
      (f.toFun' B q)

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N
        (((h.comp φ.range.val).comp ↑(Ideal.quotientKerEquivRange φ)).comp
            (Ideal.Quotient.mkₐ R (RingHom.ker φ))).toLinearMap)
      (f.toFun' A p) =
    (LinearMap.rTensor N
        ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker ψ))).toLinearMap)
      (f.toFun' B q)
Tactic:
nth_rewrite 2 [AlgHom.comp_assoc]
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N
        ((h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ))).comp
            (Ideal.Quotient.mkₐ R (RingHom.ker φ))).toLinearMap)
      (f.toFun' A p) =
    (LinearMap.rTensor N
        ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker ψ))).toLinearMap)
      (f.toFun' B q)

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N
        ((h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ))).comp
            (Ideal.Quotient.mkₐ R (RingHom.ker φ))).toLinearMap)
      (f.toFun' A p) =
    (LinearMap.rTensor N
        ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker ψ))).toLinearMap)
      (f.toFun' B q)
Tactic:
rw [ht, AlgHom.comp_assoc]
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N
        (ψ.range.val.comp
            (((↑(Ideal.quotientKerEquivRange ψ)).comp θ).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)))).toLinearMap)
      (f.toFun' A p) =
    (LinearMap.rTensor N
        ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker ψ))).toLinearMap)
      (f.toFun' B q)

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N
        (ψ.range.val.comp
            (((↑(Ideal.quotientKerEquivRange ψ)).comp θ).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ)))).toLinearMap)
      (f.toFun' A p) =
    (LinearMap.rTensor N
        ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker ψ))).toLinearMap)
      (f.toFun' B q)
Tactic:
simp only [comp_toLinearMap, rTensor_comp, LinearMap.comp_apply]
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N ψ.range.val.toLinearMap)
      ((LinearMap.rTensor N (↑(Ideal.quotientKerEquivRange ψ)).toLinearMap)
        ((LinearMap.rTensor N θ.toLinearMap)
          ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) (f.toFun' A p)))) =
    (LinearMap.rTensor N ψ.range.val.toLinearMap)
      ((LinearMap.rTensor N (↑(Ideal.quotientKerEquivRange ψ)).toLinearMap)
        ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) (f.toFun' B q)))

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N ψ.range.val.toLinearMap)
      ((LinearMap.rTensor N (↑(Ideal.quotientKerEquivRange ψ)).toLinearMap)
        ((LinearMap.rTensor N θ.toLinearMap)
          ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) (f.toFun' A p)))) =
    (LinearMap.rTensor N ψ.range.val.toLinearMap)
      ((LinearMap.rTensor N (↑(Ideal.quotientKerEquivRange ψ)).toLinearMap)
        ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) (f.toFun' B q)))
Tactic:
apply congr_arg
State after:
case h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N (↑(Ideal.quotientKerEquivRange ψ)).toLinearMap)
      ((LinearMap.rTensor N θ.toLinearMap)
        ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) (f.toFun' A p))) =
    (LinearMap.rTensor N (↑(Ideal.quotientKerEquivRange ψ)).toLinearMap)
      ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) (f.toFun' B q))

State before:
case h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N (↑(Ideal.quotientKerEquivRange ψ)).toLinearMap)
      ((LinearMap.rTensor N θ.toLinearMap)
        ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) (f.toFun' A p))) =
    (LinearMap.rTensor N (↑(Ideal.quotientKerEquivRange ψ)).toLinearMap)
      ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) (f.toFun' B q))
Tactic:
apply congr_arg
State after:
case h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N θ.toLinearMap)
      ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) (f.toFun' A p)) =
    (LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) (f.toFun' B q)

State before:
case h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor N θ.toLinearMap)
      ((LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) (f.toFun' A p)) =
    (LinearMap.rTensor N (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) (f.toFun' B q)
Tactic:
simp only [f.isCompat_apply']
State after:
case h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ f.toFun' (B ⧸ RingHom.ker ψ)
      ((LinearMap.rTensor M θ.toLinearMap)
        ((LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) p)) =
    f.toFun' (B ⧸ RingHom.ker ψ) ((LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q)

State before:
case h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ f.toFun' (B ⧸ RingHom.ker ψ)
      ((LinearMap.rTensor M θ.toLinearMap)
        ((LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) p)) =
    f.toFun' (B ⧸ RingHom.ker ψ) ((LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q)
Tactic:
apply congr_arg
State after:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor M θ.toLinearMap) ((LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) p) =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q

State before:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor M θ.toLinearMap) ((LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker φ)).toLinearMap) p) =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q
Tactic:
simp only [θ, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, AlgHom.comp_assoc]
State after:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor M
        ((↑(Ideal.quotientKerEquivRange ψ).symm).comp
            (h'.comp ((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ))))).toLinearMap)
      p =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q

State before:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor M
        ((↑(Ideal.quotientKerEquivRange ψ).symm).comp
            (h'.comp ((↑(Ideal.quotientKerEquivRange φ)).comp (Ideal.Quotient.mkₐ R (RingHom.ker φ))))).toLinearMap)
      p =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q
Tactic:
simp only [quotientKerEquivRange_mk, comp_toLinearMap, rTensor_comp, LinearMap.comp_apply]
State after:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor M (↑(Ideal.quotientKerEquivRange ψ).symm).toLinearMap)
      ((LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p)) =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q

State before:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
⊢ (LinearMap.rTensor M (↑(Ideal.quotientKerEquivRange ψ).symm).toLinearMap)
      ((LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p)) =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q
Tactic:
simp only [comp_toLinearMap, rTensor_comp, LinearMap.comp_apply] at hpq
State after:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (LinearMap.rTensor M (↑(Ideal.quotientKerEquivRange ψ).symm).toLinearMap)
      ((LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p)) =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q

State before:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (LinearMap.rTensor M (↑(Ideal.quotientKerEquivRange ψ).symm).toLinearMap)
      ((LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p)) =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q
Tactic:
simp only [hpq, ← LinearMap.comp_apply, ← rTensor_comp, ← comp_toLinearMap, AlgHom.comp_assoc]
State after:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (LinearMap.rTensor M ((↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict).toLinearMap) q =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q

State before:
case h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (LinearMap.rTensor M ((↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict).toLinearMap) q =
    (LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap) q
Tactic:
apply LinearMap.congr_fun
State after:
case h.h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ LinearMap.rTensor M ((↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict).toLinearMap =
    LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap

State before:
case h.h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ LinearMap.rTensor M ((↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict).toLinearMap =
    LinearMap.rTensor M (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap
Tactic:
apply congr_arg
State after:
case h.h.h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ ((↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict).toLinearMap =
    (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap

State before:
case h.h.h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ ((↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict).toLinearMap =
    (Ideal.Quotient.mkₐ R (RingHom.ker ψ)).toLinearMap
Tactic:
apply congr_arg
State after:
case h.h.h.h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict = Ideal.Quotient.mkₐ R (RingHom.ker ψ)

State before:
case h.h.h.h.h.h
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ (↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict = Ideal.Quotient.mkₐ R (RingHom.ker ψ)
Tactic:
ext n
State after:
case h.h.h.h.h.h.H
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
n : B
⊢ ((↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict) n = (Ideal.Quotient.mkₐ R (RingHom.ker ψ)) n

State before:
case h.h.h.h.h.h.H
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
n : B
⊢ ((↑(Ideal.quotientKerEquivRange ψ).symm).comp ψ.rangeRestrict) n = (Ideal.Quotient.mkₐ R (RingHom.ker ψ)) n
Tactic:
simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_comp, AlgHom.coe_coe, Function.comp_apply,
  Ideal.Quotient.mkₐ_eq_mk]
State after:
case h.h.h.h.h.h.H
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
n : B
⊢ (Ideal.quotientKerEquivRange ψ).symm (ψ.rangeRestrict n) = (Ideal.Quotient.mk (RingHom.ker ψ)) n

State before:
case h.h.h.h.h.h.H
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
n : B
⊢ (Ideal.quotientKerEquivRange ψ).symm (ψ.rangeRestrict n) = (Ideal.Quotient.mk (RingHom.ker ψ)) n
Tactic:
erw [Equiv.symm_apply_eq]
State after:
case h.h.h.h.h.h.H
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
n : B
⊢ ψ.rangeRestrict n =
    (Ideal.quotientKerEquivRange ψ).toRingEquiv.toMulEquiv.toEquiv ((Ideal.Quotient.mk (RingHom.ker ψ)) n)

State before:
case h.h.h.h.h.h.H
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
ht :
  h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
hpq :
  (LinearMap.rTensor M h'.toLinearMap) ((LinearMap.rTensor M φ.rangeRestrict.toLinearMap) p) =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
n : B
⊢ ψ.rangeRestrict n =
    (Ideal.quotientKerEquivRange ψ).toRingEquiv.toMulEquiv.toEquiv ((Ideal.Quotient.mk (RingHom.ker ψ)) n)
Tactic:
rfl
State after:
no goals

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ h.comp (φ.range.val.comp ↑(Ideal.quotientKerEquivRange φ)) =
    ψ.range.val.comp ((↑(Ideal.quotientKerEquivRange ψ)).comp θ)
Tactic:
simp only [θ, ← AlgHom.comp_assoc, ← hh']
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ (ψ.range.val.comp h').comp ↑(Ideal.quotientKerEquivRange φ) =
    (((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm).comp h').comp
      ↑(Ideal.quotientKerEquivRange φ)

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ (ψ.range.val.comp h').comp ↑(Ideal.quotientKerEquivRange φ) =
    (((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm).comp h').comp
      ↑(Ideal.quotientKerEquivRange φ)
Tactic:
apply congr_arg₂ _ _ rfl
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ ψ.range.val.comp h' =
    ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm).comp h'

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ ψ.range.val.comp h' =
    ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm).comp h'
Tactic:
apply congr_arg₂ _ _ rfl
State after:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ ψ.range.val = (ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm

State before:
R : Type u
inst✝¹² : CommRing R
M : Type u_1
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
N : Type u_2
inst✝⁹ : AddCommGroup N
inst✝⁸ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
A : Type u
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommRing T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq :
  (LinearMap.rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
θ : A ⧸ RingHom.ker φ →ₐ[R] B ⧸ RingHom.ker ψ :=
  (↑(Ideal.quotientKerEquivRange ψ).symm).comp (h'.comp ↑(Ideal.quotientKerEquivRange φ))
⊢ ψ.range.val = (ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm
Tactic:
simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.comp_assoc, AlgEquiv.comp_symm, AlgHom.comp_id]
State after:
no goals