internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
Proof 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)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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']
Proof 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)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
Proof 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
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
Proof 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
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
Proof 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
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
Proof 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