internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.φ_range
Proof state before:
case a
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
s : Finset S
x : S
⊢ x ∈ ↑s → x ∈ ↑(PolynomialMap.φ R s).range
Tactic:
simp only [Finset.mem_coe, φ, coe_range, Set.mem_range]
Proof state after:
case a
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
s : Finset S
x : S
⊢ x ∈ s → ∃ y, (aeval fun n => ↑(s.equivFin.symm n)) y = x
Theorem: PolynomialMap.φ_range
Proof state before:
case a
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
s : Finset S
x : S
⊢ x ∈ s → ∃ y, (aeval fun n => ↑(s.equivFin.symm n)) y = x
Tactic:
intro hx
Proof state after:
case a
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
s : Finset S
x : S
hx : x ∈ s
⊢ ∃ y, (aeval fun n => ↑(s.equivFin.symm n)) y = x
Theorem: PolynomialMap.φ_range
Proof state before:
case a
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
s : Finset S
x : S
hx : x ∈ s
⊢ ∃ y, (aeval fun n => ↑(s.equivFin.symm n)) y = x
Tactic:
use X (s.equivFin ⟨x, hx⟩)
Proof 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
s : Finset S
x : S
hx : x ∈ s
⊢ (aeval fun n => ↑(s.equivFin.symm n)) (X (s.equivFin ⟨x, hx⟩)) = x
Theorem: PolynomialMap.φ_range
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
s : Finset S
x : S
hx : x ∈ s
⊢ (aeval fun n => ↑(s.equivFin.symm n)) (X (s.equivFin ⟨x, hx⟩)) = x
Tactic:
simp only [aeval_X, Equiv.symm_apply_apply]
Proof state after:
no goals
Theorem: PolynomialMap.Subalgebra.FG.exists_range_eq
Proof 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
B : Subalgebra R S
hB : B.FG
⊢ ∃ s, (PolynomialMap.φ R s).range = B
Tactic:
obtain ⟨s, hs⟩ := hB
Proof state after:
case intro
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
B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = B
⊢ ∃ s, (PolynomialMap.φ R s).range = B
Theorem: PolynomialMap.Subalgebra.FG.exists_range_eq
Proof state before:
case intro
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
B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = B
⊢ ∃ s, (PolynomialMap.φ R s).range = B
Tactic:
use s
Proof 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
B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = B
⊢ (PolynomialMap.φ R s).range = B
Theorem: PolynomialMap.Subalgebra.FG.exists_range_eq
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
B : Subalgebra R S
s : Finset S
hs : Algebra.adjoin R ↑s = B
⊢ (PolynomialMap.φ R s).range = B
Tactic:
simp only [φ_range, hs]
Proof state after:
no goals
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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)
Proof 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)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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)))
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
Proof 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))