internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
Proof 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 ψ)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
Proof 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
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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]
Proof 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)
Theorem: PolynomialMap.toFun'_eq_of_diagram
Proof 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
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
θ : 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']
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 φ))
⊢ (ψ.range.val.comp h').comp ↑(Ideal.quotientKerEquivRange φ) =
    (((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm).comp h').comp
      ↑(Ideal.quotientKerEquivRange φ)
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 φ))
⊢ (ψ.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
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 φ))
⊢ ψ.range.val.comp h' =
    ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm).comp h'
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 φ))
⊢ ψ.range.val.comp h' =
    ((ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm).comp h'
Tactic:
apply congr_arg₂ _ _ rfl
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 φ))
⊢ ψ.range.val = (ψ.range.val.comp ↑(Ideal.quotientKerEquivRange ψ)).comp ↑(Ideal.quotientKerEquivRange ψ).symm
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 φ))
⊢ ψ.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]
Proof state after:
no goals
Theorem: PolynomialMap.toFun'_eq_of_inclusion
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
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] S
q : B ⊗[R] M
h : φ.range ≤ ψ.range
hpq :
  (LinearMap.rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
⊢ ψ.range.val.comp (Subalgebra.inclusion h) = (AlgHom.id R S).comp φ.range.val
Tactic:
ext x
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
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] S
q : B ⊗[R] M
h : φ.range ≤ ψ.range
hpq :
  (LinearMap.rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
x : ↥φ.range
⊢ (ψ.range.val.comp (Subalgebra.inclusion h)) x = ((AlgHom.id R S).comp φ.range.val) x
Theorem: PolynomialMap.toFun'_eq_of_inclusion
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
B : Type u
inst✝¹ : CommRing B
inst✝ : Algebra R B
ψ : B →ₐ[R] S
q : B ⊗[R] M
h : φ.range ≤ ψ.range
hpq :
  (LinearMap.rTensor M ((Subalgebra.inclusion h).comp φ.rangeRestrict).toLinearMap) p =
    (LinearMap.rTensor M ψ.rangeRestrict.toLinearMap) q
x : ↥φ.range
⊢ (ψ.range.val.comp (Subalgebra.inclusion h)) x = ((AlgHom.id R S).comp φ.range.val) x
Tactic:
simp
Proof state after:
no goals
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
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
⊢ Function.FactorsThrough (PolynomialMap.toFunLifted f) (PolynomialMap.π R M S)
Tactic:
rintro ⟨s, p⟩ ⟨s', p'⟩ h
Proof state after:
case mk.mk
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
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
⊢ PolynomialMap.toFunLifted f ⟨s, p⟩ = PolynomialMap.toFunLifted f ⟨s', p'⟩
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk
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
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
⊢ PolynomialMap.toFunLifted f ⟨s, p⟩ = PolynomialMap.toFunLifted f ⟨s', p'⟩
Tactic:
simp only [toFunLifted]
Proof state after:
case mk.mk
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
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Theorem: PolynomialMap.toFunLifted_factorsThrough_π
Proof state before:
case mk.mk
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
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Tactic:
set u := rTensor M (φ R s).rangeRestrict.toLinearMap p with hu
Proof state after:
case mk.mk
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
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : PolynomialMap.π R M S ⟨s, p⟩ = PolynomialMap.π R M S ⟨s', p'⟩
u : ↥(PolynomialMap.φ R s).range ⊗[R] M := (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
hu : u = (LinearMap.rTensor M (PolynomialMap.φ R s).rangeRestrict.toLinearMap) p
⊢ (LinearMap.rTensor N (PolynomialMap.φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (LinearMap.rTensor N (PolynomialMap.φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')