[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso f
H : P (f ≫ g)
⊢ P g
[PROOFSTEP]
convert hP.2 (f ≫ g) (asIso f).symm.commRingCatIsoToRingEquiv H
[GOAL]
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso f
H : P (f ≫ g)
⊢ g = comp (f ≫ g) (RingEquiv.toRingHom (Iso.commRingCatIsoToRingEquiv (asIso f).symm))
[PROOFSTEP]
exact (IsIso.inv_hom_id_assoc _ _).symm
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso g
H : P (f ≫ g)
⊢ P f
[PROOFSTEP]
convert hP.1 (f ≫ g) (asIso g).symm.commRingCatIsoToRingEquiv H
[GOAL]
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso g
H : P (f ≫ g)
⊢ f = comp (RingEquiv.toRingHom (Iso.commRingCatIsoToRingEquiv (asIso g).symm)) (f ≫ g)
[PROOFSTEP]
change f = f ≫ g ≫ inv g
[GOAL]
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
inst✝ : IsIso g
H : P (f ≫ g)
⊢ f = f ≫ g ≫ inv g
[PROOFSTEP]
simp
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
⊢ P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)
[PROOFSTEP]
let e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) _ _).toRingEquiv
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
⊢ P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)
[PROOFSTEP]
let e₂ : Localization.Away (f r) ≃+* S' := (IsLocalization.algEquiv (Submonoid.powers (f r)) _ _).toRingEquiv
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
⊢ P (Localization.awayMap f r) ↔ P (IsLocalization.Away.map R' S' f r)
[PROOFSTEP]
refine' (hP.cancel_left_isIso e₁.toCommRingCatIso.hom (CommRingCat.ofHom _)).symm.trans _
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
⊢ P
      ((RingEquiv.toCommRingCatIso e₁).hom ≫
        CommRingCat.ofHom
          (IsLocalization.map (Localization.Away (↑f r)) f
            (_ : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))))) ↔
    P (IsLocalization.Away.map R' S' f r)
[PROOFSTEP]
refine' (hP.cancel_right_isIso (CommRingCat.ofHom _) e₂.toCommRingCatIso.hom).symm.trans _
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
⊢ P
      (CommRingCat.ofHom
          ((RingEquiv.toCommRingCatIso e₁).hom ≫
            CommRingCat.ofHom
              (IsLocalization.map (Localization.Away (↑f r)) f
                (_ : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))))) ≫
        (RingEquiv.toCommRingCatIso e₂).hom) ↔
    P (IsLocalization.Away.map R' S' f r)
[PROOFSTEP]
rw [← eq_iff_iff]
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
⊢ P
      (CommRingCat.ofHom
          ((RingEquiv.toCommRingCatIso e₁).hom ≫
            CommRingCat.ofHom
              (IsLocalization.map (Localization.Away (↑f r)) f
                (_ : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))))) ≫
        (RingEquiv.toCommRingCatIso e₂).hom) =
    P (IsLocalization.Away.map R' S' f r)
[PROOFSTEP]
congr 1
  -- Porting Note : Here, the proof used to have a huge `simp` involving `[anonymous]`, which didn't
    -- work out anymore. The issue seemed to be that it couldn't handle a term in which Ring
    -- homomorphisms were repeatedly casted to the bundled category and back. Here we resolve the
    -- problem by converting the goal to a more straightforward form.
[GOAL]
case e_x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
⊢ CommRingCat.ofHom
        ((RingEquiv.toCommRingCatIso e₁).hom ≫
          CommRingCat.ofHom
            (IsLocalization.map (Localization.Away (↑f r)) f
              (_ : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))))) ≫
      (RingEquiv.toCommRingCatIso e₂).hom =
    IsLocalization.Away.map R' S' f r
[PROOFSTEP]
let e :=
  (e₂ : Localization.Away (f r) →+* S').comp
    (((IsLocalization.map (Localization.Away (f r)) f
            (by rintro x ⟨n, rfl⟩; use n; simp : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (f r)))) :
          Localization.Away r →+* Localization.Away (f r)).comp
      (e₁ : R' →+* Localization.Away r))
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
⊢ Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))
[PROOFSTEP]
rintro x ⟨n, rfl⟩
[GOAL]
case intro
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
n : ℕ
⊢ (fun x x_1 => x ^ x_1) r n ∈ Submonoid.comap f (Submonoid.powers (↑f r))
[PROOFSTEP]
use n
[GOAL]
case h
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
n : ℕ
⊢ (fun x x_1 => x ^ x_1) (↑f r) n = ↑f ((fun x x_1 => x ^ x_1) r n)
[PROOFSTEP]
simp
[GOAL]
case e_x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
e : R' →+* S' :=
  comp (↑e₂)
    (comp
      (IsLocalization.map (Localization.Away (↑f r)) f
        (_ : ∀ ⦃x : R⦄, x ∈ Submonoid.powers r → x ∈ Submonoid.comap f (Submonoid.powers (↑f r))))
      ↑e₁)
⊢ CommRingCat.ofHom
        ((RingEquiv.toCommRingCatIso e₁).hom ≫
          CommRingCat.ofHom
            (IsLocalization.map (Localization.Away (↑f r)) f
              (_ : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))))) ≫
      (RingEquiv.toCommRingCatIso e₂).hom =
    IsLocalization.Away.map R' S' f r
[PROOFSTEP]
suffices e = IsLocalization.Away.map R' S' f r by convert this
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
e : R' →+* S' :=
  comp (↑e₂)
    (comp
      (IsLocalization.map (Localization.Away (↑f r)) f
        (_ : ∀ ⦃x : R⦄, x ∈ Submonoid.powers r → x ∈ Submonoid.comap f (Submonoid.powers (↑f r))))
      ↑e₁)
this : e = IsLocalization.Away.map R' S' f r
⊢ CommRingCat.ofHom
        ((RingEquiv.toCommRingCatIso e₁).hom ≫
          CommRingCat.ofHom
            (IsLocalization.map (Localization.Away (↑f r)) f
              (_ : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))))) ≫
      (RingEquiv.toCommRingCatIso e₂).hom =
    IsLocalization.Away.map R' S' f r
[PROOFSTEP]
convert this
[GOAL]
case e_x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
e : R' →+* S' :=
  comp (↑e₂)
    (comp
      (IsLocalization.map (Localization.Away (↑f r)) f
        (_ : ∀ ⦃x : R⦄, x ∈ Submonoid.powers r → x ∈ Submonoid.comap f (Submonoid.powers (↑f r))))
      ↑e₁)
⊢ e = IsLocalization.Away.map R' S' f r
[PROOFSTEP]
apply IsLocalization.ringHom_ext (Submonoid.powers r) _
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
e : R' →+* S' :=
  comp (↑e₂)
    (comp
      (IsLocalization.map (Localization.Away (↑f r)) f
        (_ : ∀ ⦃x : R⦄, x ∈ Submonoid.powers r → x ∈ Submonoid.comap f (Submonoid.powers (↑f r))))
      ↑e₁)
⊢ comp e (algebraMap R R') = comp (IsLocalization.Away.map R' S' f r) (algebraMap R R')
[PROOFSTEP]
ext1 x
[GOAL]
case a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
e : R' →+* S' :=
  comp (↑e₂)
    (comp
      (IsLocalization.map (Localization.Away (↑f r)) f
        (_ : ∀ ⦃x : R⦄, x ∈ Submonoid.powers r → x ∈ Submonoid.comap f (Submonoid.powers (↑f r))))
      ↑e₁)
x : R
⊢ ↑(comp e (algebraMap R R')) x = ↑(comp (IsLocalization.Away.map R' S' f r) (algebraMap R R')) x
[PROOFSTEP]
dsimp [IsLocalization.Away.map]
[GOAL]
case a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (↑f r) S'
e₁ : R' ≃+* Localization.Away r :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r))
e₂ : Localization.Away (↑f r) ≃+* S' :=
  AlgEquiv.toRingEquiv (IsLocalization.algEquiv (Submonoid.powers (↑f r)) (Localization.Away (↑f r)) S')
e : R' →+* S' :=
  comp (↑e₂)
    (comp
      (IsLocalization.map (Localization.Away (↑f r)) f
        (_ : ∀ ⦃x : R⦄, x ∈ Submonoid.powers r → x ∈ Submonoid.comap f (Submonoid.powers (↑f r))))
      ↑e₁)
x : R
⊢ ↑(IsLocalization.map S' (id S) (_ : Submonoid.powers (↑f r) ≤ Submonoid.comap (id S) (Submonoid.powers (↑f r))))
      (↑(IsLocalization.map (Localization.Away (↑f r)) f
            (_ : ∀ ⦃x : R⦄, x ∈ Submonoid.powers r → x ∈ Submonoid.comap f (Submonoid.powers (↑f r))))
        (↑(IsLocalization.map (Localization.Away r) (id R)
              (_ : Submonoid.powers r ≤ Submonoid.comap (id R) (Submonoid.powers r)))
          (↑(algebraMap R R') x))) =
    ↑(IsLocalization.map S' f (_ : Submonoid.powers r ≤ Submonoid.comap f (Submonoid.powers (↑f r))))
      (↑(algebraMap R R') x)
[PROOFSTEP]
simp only [IsLocalization.map_eq, id_apply, RingHomCompTriple.comp_apply]
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
⊢ RespectsIso P
[PROOFSTEP]
constructor
[GOAL]
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    P f → P (comp (RingEquiv.toRingHom e) f)
[PROOFSTEP]
introv H
[GOAL]
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P (comp (RingEquiv.toRingHom e) f)
[PROOFSTEP]
skip
[GOAL]
case left
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P (comp (RingEquiv.toRingHom e) f)
[PROOFSTEP]
apply hP
[GOAL]
case left.x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P f
case left.x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P (RingEquiv.toRingHom e)
[PROOFSTEP]
exacts [H, hP' e]
[GOAL]
case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
⊢ ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
    P f → P (comp f (RingEquiv.toRingHom e))
[PROOFSTEP]
introv H
[GOAL]
case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P (comp f (RingEquiv.toRingHom e))
[PROOFSTEP]
skip
[GOAL]
case right
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P (comp f (RingEquiv.toRingHom e))
[PROOFSTEP]
apply hP
[GOAL]
case right.x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P (RingEquiv.toRingHom e)
case right.x
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), P (RingEquiv.toRingHom e)
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P f
[PROOFSTEP]
exacts [hP' e, H]
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
⊢ StableUnderBaseChange P
[PROOFSTEP]
introv R h H
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
⊢ P (algebraMap R' S')
[PROOFSTEP]
let e := h.symm.1.equiv
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
⊢ P (algebraMap R' S')
[PROOFSTEP]
let f' := Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
⊢ P (algebraMap R' S')
[PROOFSTEP]
have : ∀ x, e x = f' x := by
  intro x
  change e.toLinearMap.restrictScalars R x = f'.toLinearMap x
  congr 1
  apply TensorProduct.ext'
  intro x y
  simp [IsBaseChange.equiv_tmul, Algebra.smul_def]
    -- Porting Note: This had a lot of implicit inferences which didn't resolve anymore.
      -- Added those in
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
⊢ ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
[PROOFSTEP]
intro x
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : TensorProduct R R' S
⊢ ↑e x = ↑f' x
[PROOFSTEP]
change e.toLinearMap.restrictScalars R x = f'.toLinearMap x
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : TensorProduct R R' S
⊢ ↑(↑R ↑e) x = ↑(AlgHom.toLinearMap f') x
[PROOFSTEP]
congr 1
[GOAL]
case e_a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : TensorProduct R R' S
⊢ ↑R ↑e = AlgHom.toLinearMap f'
[PROOFSTEP]
apply TensorProduct.ext'
[GOAL]
case e_a.H
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : TensorProduct R R' S
⊢ ∀ (x : R') (y : S), ↑(↑R ↑e) (x ⊗ₜ[R] y) = ↑(AlgHom.toLinearMap f') (x ⊗ₜ[R] y)
[PROOFSTEP]
intro x y
[GOAL]
case e_a.H
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x✝ : TensorProduct R R' S
x : R'
y : S
⊢ ↑(↑R ↑e) (x ⊗ₜ[R] y) = ↑(AlgHom.toLinearMap f') (x ⊗ₜ[R] y)
[PROOFSTEP]
simp [IsBaseChange.equiv_tmul, Algebra.smul_def]
  -- Porting Note: This had a lot of implicit inferences which didn't resolve anymore.
    -- Added those in
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
⊢ P (algebraMap R' S')
[PROOFSTEP]
convert
  h₁.1 (_ : R' →+* TensorProduct R R' S) (_ : TensorProduct R R' S ≃+* S') (h₂ H : P (_ : R' →+* TensorProduct R R' S))
[GOAL]
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
⊢ algebraMap R' S' = comp (RingEquiv.toRingHom ?m.221851) Algebra.TensorProduct.includeLeftRingHom
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
⊢ TensorProduct R R' S ≃+* S'
[PROOFSTEP]
swap
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
⊢ TensorProduct R R' S ≃+* S'
[PROOFSTEP]
refine' { e with map_mul' := fun x y => _ }
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
x y : TensorProduct R R' S
⊢ Equiv.toFun
      { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun),
        right_inv := (_ : Function.RightInverse e.invFun e.toFun) }
      (x * y) =
    Equiv.toFun
        { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun),
          right_inv := (_ : Function.RightInverse e.invFun e.toFun) }
        x *
      Equiv.toFun
        { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun),
          right_inv := (_ : Function.RightInverse e.invFun e.toFun) }
        y
[PROOFSTEP]
change e (x * y) = e x * e y
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
x y : TensorProduct R R' S
⊢ ↑e (x * y) = ↑e x * ↑e y
[PROOFSTEP]
simp_rw [this]
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
x y : TensorProduct R R' S
⊢ ↑(Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')) (x * y) =
    ↑(Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')) x *
      ↑(Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')) y
[PROOFSTEP]
exact map_mul f' _ _
[GOAL]
case h.e'_5
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
⊢ algebraMap R' S' =
    comp
      (RingEquiv.toRingHom
        {
          toEquiv :=
            { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun),
              right_inv := (_ : Function.RightInverse e.invFun e.toFun) },
          map_mul' := (_ : ∀ (x y : TensorProduct R R' S), ↑e (x * y) = ↑e x * ↑e y),
          map_add' :=
            (_ :
              ∀ (x y : TensorProduct R R' S),
                AddHom.toFun e.toAddHom (x + y) = AddHom.toFun e.toAddHom x + AddHom.toFun e.toAddHom y) })
      Algebra.TensorProduct.includeLeftRingHom
[PROOFSTEP]
ext x
[GOAL]
case h.e'_5.a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
x : R'
⊢ ↑(algebraMap R' S') x =
    ↑(comp
          (RingEquiv.toRingHom
            {
              toEquiv :=
                { toFun := e.toFun, invFun := e.invFun, left_inv := (_ : Function.LeftInverse e.invFun e.toFun),
                  right_inv := (_ : Function.RightInverse e.invFun e.toFun) },
              map_mul' := (_ : ∀ (x y : TensorProduct R R' S), ↑e (x * y) = ↑e x * ↑e y),
              map_add' :=
                (_ :
                  ∀ (x y : TensorProduct R R' S),
                    AddHom.toFun e.toAddHom (x + y) = AddHom.toFun e.toAddHom x + AddHom.toFun e.toAddHom y) })
          Algebra.TensorProduct.includeLeftRingHom)
      x
[PROOFSTEP]
change
  _ =
    e
      (x ⊗ₜ[R] 1)
        --Porting note: Had `dsimp only [e]` here, which didn't work anymore
[GOAL]
case h.e'_5.a
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T], P (algebraMap R T) → P Algebra.TensorProduct.includeLeftRingHom
R S R' S' : Type u
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R S'
inst✝³ : Algebra S S'
inst✝² : Algebra R' S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : TensorProduct R R' S ≃ₛₗ[id R'] S' :=
  IsBaseChange.equiv (_ : IsBaseChange R' (AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')))
f' : TensorProduct R R' S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
this : ∀ (x : TensorProduct R R' S), ↑e x = ↑f' x
x : R'
⊢ ↑(algebraMap R' S') x = ↑e (x ⊗ₜ[R] 1)
[PROOFSTEP]
rw [h.symm.1.equiv_tmul, Algebra.smul_def, AlgHom.toLinearMap_apply, map_one, mul_one]
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P g
⊢ P pushout.inl
[PROOFSTEP]
rw [←
  show _ = pushout.inl from colimit.isoColimitCocone_ι_inv ⟨_, CommRingCat.pushoutCoconeIsColimit f g⟩ WalkingSpan.left,
  hP'.cancel_right_isIso]
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P g
⊢ P
    (NatTrans.app
      { cocone := CommRingCat.pushoutCocone f g, isColimit := CommRingCat.pushoutCoconeIsColimit f g }.cocone.ι
      WalkingSpan.left)
[PROOFSTEP]
letI := f.toAlgebra
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P g
this : Algebra ↑R ↑S := toAlgebra f
⊢ P
    (NatTrans.app
      { cocone := CommRingCat.pushoutCocone f g, isColimit := CommRingCat.pushoutCoconeIsColimit f g }.cocone.ι
      WalkingSpan.left)
[PROOFSTEP]
letI := g.toAlgebra
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P g
this✝ : Algebra ↑R ↑S := toAlgebra f
this : Algebra ↑R ↑T := toAlgebra g
⊢ P
    (NatTrans.app
      { cocone := CommRingCat.pushoutCocone f g, isColimit := CommRingCat.pushoutCoconeIsColimit f g }.cocone.ι
      WalkingSpan.left)
[PROOFSTEP]
dsimp only [CommRingCat.pushoutCocone_inl, PushoutCocone.ι_app_left]
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P g
this✝ : Algebra ↑R ↑S := toAlgebra f
this : Algebra ↑R ↑T := toAlgebra g
⊢ P Algebra.TensorProduct.includeLeftRingHom
[PROOFSTEP]
apply hP R T S (TensorProduct R S T)
[GOAL]
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : StableUnderBaseChange P
hP' : RespectsIso P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P g
this✝ : Algebra ↑R ↑S := toAlgebra f
this : Algebra ↑R ↑T := toAlgebra g
⊢ P (algebraMap ↑R ↑T)
[PROOFSTEP]
exact H


[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
⊢ ↑(↑(toFunBilinear R A) a) p = sum p fun n r => ↑(monomial n) (a * ↑(algebraMap R A) r)
[PROOFSTEP]
simp only [toFunBilinear_apply_apply, aeval_def, eval₂_eq_sum, Polynomial.sum, Finset.smul_sum]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
⊢ (Finset.sum (support p) fun x => a • (↑(algebraMap R A[X]) (coeff p x) * X ^ x)) =
    Finset.sum (support p) fun x => ↑(monomial x) (a * ↑(algebraMap R A) (coeff p x))
[PROOFSTEP]
congr with i : 1
[GOAL]
case e_f.h
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : A
p : R[X]
i : ℕ
⊢ a • (↑(algebraMap R A[X]) (coeff p i) * X ^ i) = ↑(monomial i) (a * ↑(algebraMap R A) (coeff p i))
[PROOFSTEP]
rw [← Algebra.smul_def, ← C_mul', mul_smul_comm, C_mul_X_pow_eq_monomial, ← Algebra.commutes, ← Algebra.smul_def,
  smul_monomial]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬coeff p k = 0
a : A
⊢ (if ¬coeff p k = 0 then a * ↑(algebraMap R A) (coeff p k) else 0) = a * ↑(algebraMap R A) (coeff p k)
[PROOFSTEP]
classical split_ifs <;> simp [*]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬coeff p k = 0
a : A
⊢ (if ¬coeff p k = 0 then a * ↑(algebraMap R A) (coeff p k) else 0) = a * ↑(algebraMap R A) (coeff p k)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬coeff p k = 0
a : A
h✝ : coeff p k = 0
⊢ 0 = a * ↑(algebraMap R A) (coeff p k)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : R[X]
k : ℕ
h : Decidable ¬coeff p k = 0
a : A
h✝ : ¬coeff p k = 0
⊢ a * ↑(algebraMap R A) (coeff p k) = a * ↑(algebraMap R A) (coeff p k)
[PROOFSTEP]
simp [*]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      a₁ * ↑(algebraMap R A) (coeff p₁ x.fst) * (a₂ * ↑(algebraMap R A) (coeff p₂ x.snd))
[PROOFSTEP]
simp_rw [mul_assoc, Algebra.commutes, ← Finset.mul_sum, mul_assoc, ← Finset.mul_sum]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ a₁ * (a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k)) =
    a₁ *
      (a₂ *
        Finset.sum (Finset.Nat.antidiagonal k) fun x =>
          ↑(algebraMap R A) (coeff p₂ x.snd) * ↑(algebraMap R A) (coeff p₁ x.fst))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ ↑(algebraMap R A) (coeff (p₁ * p₂) k) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      ↑(algebraMap R A) (coeff p₂ x.snd) * ↑(algebraMap R A) (coeff p₁ x.fst)
[PROOFSTEP]
simp_rw [Algebra.commutes (coeff p₂ _), coeff_mul, map_sum, RingHom.map_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ ↑(toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = ↑(toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * ↑(toFunLinear R A) (a₂ ⊗ₜ[R] p₂)
[PROOFSTEP]
classical
simp only [toFunLinear_tmul_apply, toFunBilinear_apply_eq_sum]
ext k
simp_rw [coeff_sum, coeff_monomial, sum_def, Finset.sum_ite_eq', mem_support_iff, Ne.def]
conv_rhs => rw [coeff_mul]
simp_rw [finset_sum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne.def, mul_ite, mul_zero, ite_mul,
  zero_mul]
simp_rw [ite_mul_zero_left (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]
simp_rw [ite_mul_zero_right (¬coeff p₂ _ = 0) _ (_ * _)]
simp_rw [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ ↑(toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) = ↑(toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * ↑(toFunLinear R A) (a₂ ⊗ₜ[R] p₂)
[PROOFSTEP]
simp only [toFunLinear_tmul_apply, toFunBilinear_apply_eq_sum]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ (sum (p₁ * p₂) fun n r => ↑(monomial n) (a₁ * a₂ * ↑(algebraMap R A) r)) =
    (sum p₁ fun n r => ↑(monomial n) (a₁ * ↑(algebraMap R A) r)) *
      sum p₂ fun n r => ↑(monomial n) (a₂ * ↑(algebraMap R A) r)
[PROOFSTEP]
ext k
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ coeff (sum (p₁ * p₂) fun n r => ↑(monomial n) (a₁ * a₂ * ↑(algebraMap R A) r)) k =
    coeff
      ((sum p₁ fun n r => ↑(monomial n) (a₁ * ↑(algebraMap R A) r)) *
        sum p₂ fun n r => ↑(monomial n) (a₂ * ↑(algebraMap R A) r))
      k
[PROOFSTEP]
simp_rw [coeff_sum, coeff_monomial, sum_def, Finset.sum_ite_eq', mem_support_iff, Ne.def]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬coeff (p₁ * p₂) k = 0 then a₁ * a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k) else 0) =
    coeff
      ((Finset.sum (support p₁) fun n => ↑(monomial n) (a₁ * ↑(algebraMap R A) (coeff p₁ n))) *
        Finset.sum (support p₂) fun n => ↑(monomial n) (a₂ * ↑(algebraMap R A) (coeff p₂ n)))
      k
[PROOFSTEP]
conv_rhs => rw [coeff_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
| coeff
    ((Finset.sum (support p₁) fun n => ↑(monomial n) (a₁ * ↑(algebraMap R A) (coeff p₁ n))) *
      Finset.sum (support p₂) fun n => ↑(monomial n) (a₂ * ↑(algebraMap R A) (coeff p₂ n)))
    k
[PROOFSTEP]
rw [coeff_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
| coeff
    ((Finset.sum (support p₁) fun n => ↑(monomial n) (a₁ * ↑(algebraMap R A) (coeff p₁ n))) *
      Finset.sum (support p₂) fun n => ↑(monomial n) (a₂ * ↑(algebraMap R A) (coeff p₂ n)))
    k
[PROOFSTEP]
rw [coeff_mul]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
| coeff
    ((Finset.sum (support p₁) fun n => ↑(monomial n) (a₁ * ↑(algebraMap R A) (coeff p₁ n))) *
      Finset.sum (support p₂) fun n => ↑(monomial n) (a₂ * ↑(algebraMap R A) (coeff p₂ n)))
    k
[PROOFSTEP]
rw [coeff_mul]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬coeff (p₁ * p₂) k = 0 then a₁ * a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k) else 0) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      coeff (Finset.sum (support p₁) fun n => ↑(monomial n) (a₁ * ↑(algebraMap R A) (coeff p₁ n))) x.fst *
        coeff (Finset.sum (support p₂) fun n => ↑(monomial n) (a₂ * ↑(algebraMap R A) (coeff p₂ n))) x.snd
[PROOFSTEP]
simp_rw [finset_sum_coeff, coeff_monomial, Finset.sum_ite_eq', mem_support_iff, Ne.def, mul_ite, mul_zero, ite_mul,
  zero_mul]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬coeff (p₁ * p₂) k = 0 then a₁ * a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k) else 0) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      if ¬coeff p₂ x.snd = 0 then
        if ¬coeff p₁ x.fst = 0 then a₁ * ↑(algebraMap R A) (coeff p₁ x.fst) * (a₂ * ↑(algebraMap R A) (coeff p₂ x.snd))
        else 0
      else 0
[PROOFSTEP]
simp_rw [ite_mul_zero_left (¬coeff p₁ _ = 0) (a₁ * (algebraMap R A) (coeff p₁ _))]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬coeff (p₁ * p₂) k = 0 then a₁ * a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k) else 0) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      if ¬coeff p₂ x.snd = 0 then
        (if ¬coeff p₁ x.fst = 0 then a₁ * ↑(algebraMap R A) (coeff p₁ x.fst) else 0) *
          (a₂ * ↑(algebraMap R A) (coeff p₂ x.snd))
      else 0
[PROOFSTEP]
simp_rw [ite_mul_zero_right (¬coeff p₂ _ = 0) _ (_ * _)]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬coeff (p₁ * p₂) k = 0 then a₁ * a₂ * ↑(algebraMap R A) (coeff (p₁ * p₂) k) else 0) =
    Finset.sum (Finset.Nat.antidiagonal k) fun x =>
      (if ¬coeff p₁ x.fst = 0 then a₁ * ↑(algebraMap R A) (coeff p₁ x.fst) else 0) *
        if ¬coeff p₂ x.snd = 0 then a₂ * ↑(algebraMap R A) (coeff p₂ x.snd) else 0
[PROOFSTEP]
simp_rw [toFunLinear_mul_tmul_mul_aux_1, toFunLinear_mul_tmul_mul_aux_2]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
r : R
⊢ ↑(toFunLinear R A) (↑(algebraMap R A) r ⊗ₜ[R] 1) = ↑(algebraMap R A[X]) r
[PROOFSTEP]
rw [toFunLinear_tmul_apply, toFunBilinear_apply_apply, Polynomial.aeval_one, algebraMap_smul,
  Algebra.algebraMap_eq_smul_one, Algebra.algebraMap_eq_smul_one]
  -- porting note: had to
    -- add extra `Algebra.algebraMap_eq_smul_one`
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
p q : A[X]
⊢ invFun R A (p + q) = invFun R A p + invFun R A q
[PROOFSTEP]
simp only [invFun, eval₂_add]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A (↑(toFunAlgHom R A) x) = x
[PROOFSTEP]
refine TensorProduct.induction_on x ?_ ?_ ?_
[GOAL]
case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ invFun R A (↑(toFunAlgHom R A) 0) = 0
[PROOFSTEP]
simp [invFun]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x : A) (y : R[X]), invFun R A (↑(toFunAlgHom R A) (x ⊗ₜ[R] y)) = x ⊗ₜ[R] y
[PROOFSTEP]
intro a p
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ invFun R A (↑(toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p
[PROOFSTEP]
dsimp only [invFun]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) (↑(toFunAlgHom R A) (a ⊗ₜ[R] p)) = a ⊗ₜ[R] p
[PROOFSTEP]
rw [toFunAlgHom_apply_tmul, eval₂_sum]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (sum p fun n a_1 => eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) (↑(monomial n) (a * ↑(algebraMap R A) a_1))) = a ⊗ₜ[R] p
[PROOFSTEP]
simp_rw [eval₂_monomial, AlgHom.coe_toRingHom, Algebra.TensorProduct.tmul_pow, one_pow,
  Algebra.TensorProduct.includeLeft_apply, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul, ← Algebra.commutes, ←
  Algebra.smul_def, smul_tmul, sum_def, ← tmul_sum]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun a => coeff p a • X ^ a) = a ⊗ₜ[R] p
[PROOFSTEP]
conv_rhs => rw [← sum_C_mul_X_pow_eq p]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
| a ⊗ₜ[R] p
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq p]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
| a ⊗ₜ[R] p
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq p]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
| a ⊗ₜ[R] p
[PROOFSTEP]
rw [← sum_C_mul_X_pow_eq p]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun a => coeff p a • X ^ a) = a ⊗ₜ[R] sum p fun n a => ↑C a * X ^ n
[PROOFSTEP]
simp only [Algebra.smul_def]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
⊢ (a ⊗ₜ[R] Finset.sum (support p) fun x => ↑(algebraMap R R[X]) (coeff p x) * X ^ x) =
    a ⊗ₜ[R] sum p fun n a => ↑C a * X ^ n
[PROOFSTEP]
rfl
[GOAL]
case refine_3
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
⊢ ∀ (x y : A ⊗[R] R[X]),
    invFun R A (↑(toFunAlgHom R A) x) = x →
      invFun R A (↑(toFunAlgHom R A) y) = y → invFun R A (↑(toFunAlgHom R A) (x + y)) = x + y
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine_3
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A ⊗[R] R[X]
hp : invFun R A (↑(toFunAlgHom R A) p) = p
hq : invFun R A (↑(toFunAlgHom R A) q) = q
⊢ invFun R A (↑(toFunAlgHom R A) (p + q)) = p + q
[PROOFSTEP]
simp only [AlgHom.map_add, invFun_add, hp, hq]
[GOAL]
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ↑(toFunAlgHom R A) (invFun R A x) = x
[PROOFSTEP]
refine Polynomial.induction_on' x ?_ ?_
[GOAL]
case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (p q : A[X]),
    ↑(toFunAlgHom R A) (invFun R A p) = p →
      ↑(toFunAlgHom R A) (invFun R A q) = q → ↑(toFunAlgHom R A) (invFun R A (p + q)) = p + q
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine_1
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x p q : A[X]
hp : ↑(toFunAlgHom R A) (invFun R A p) = p
hq : ↑(toFunAlgHom R A) (invFun R A q) = q
⊢ ↑(toFunAlgHom R A) (invFun R A (p + q)) = p + q
[PROOFSTEP]
simp only [invFun_add, AlgHom.map_add, hp, hq]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
⊢ ∀ (n : ℕ) (a : A), ↑(toFunAlgHom R A) (invFun R A (↑(monomial n) a)) = ↑(monomial n) a
[PROOFSTEP]
intro n a
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ ↑(toFunAlgHom R A) (invFun R A (↑(monomial n) a)) = ↑(monomial n) a
[PROOFSTEP]
rw [invFun_monomial, Algebra.TensorProduct.tmul_pow, one_pow, Algebra.TensorProduct.tmul_mul_tmul, mul_one, one_mul,
  toFunAlgHom_apply_tmul, X_pow_eq_monomial, sum_monomial_index]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ ↑(monomial n) (a * ↑(algebraMap R A) 1) = ↑(monomial n) a
[PROOFSTEP]
simp
[GOAL]
case refine_2.hf
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A[X]
n : ℕ
a : A
⊢ ↑(monomial n) (a * ↑(algebraMap R A) 0) = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ ↑matPolyEquiv (stdBasisMatrix i j (↑(monomial k) x)) = ↑(monomial k) (stdBasisMatrix i j x)
[PROOFSTEP]
simp only [matPolyEquiv, AlgEquiv.trans_apply, matrixEquivTensor_apply_std_basis]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ ↑(AlgEquiv.symm (polyEquivTensor R (Matrix n n R)))
      (↑(Algebra.TensorProduct.comm R R[X] (Matrix n n R)) (↑(monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1)) =
    ↑(monomial k) (stdBasisMatrix i j x)
[PROOFSTEP]
apply (polyEquivTensor R (Matrix n n R)).injective
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ ↑(polyEquivTensor R (Matrix n n R))
      (↑(AlgEquiv.symm (polyEquivTensor R (Matrix n n R)))
        (↑(Algebra.TensorProduct.comm R R[X] (Matrix n n R)) (↑(monomial k) x ⊗ₜ[R] stdBasisMatrix i j 1))) =
    ↑(polyEquivTensor R (Matrix n n R)) (↑(monomial k) (stdBasisMatrix i j x))
[PROOFSTEP]
simp only [AlgEquiv.apply_symm_apply, Algebra.TensorProduct.comm_tmul, polyEquivTensor_apply, eval₂_monomial]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] ↑(monomial k) x = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] X ^ k
[PROOFSTEP]
simp only [Algebra.TensorProduct.tmul_mul_tmul, one_pow, one_mul, Matrix.mul_one, Algebra.TensorProduct.tmul_pow,
  Algebra.TensorProduct.includeLeft_apply]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ stdBasisMatrix i j 1 ⊗ₜ[R] ↑(monomial k) x = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)
[PROOFSTEP]
rw [← smul_X_eq_monomial, ← TensorProduct.smul_tmul]
[GOAL]
case a
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
⊢ (x • stdBasisMatrix i j 1) ⊗ₜ[R] (X ^ k) = ↑↑includeLeft (stdBasisMatrix i j x) * 1 ⊗ₜ[R] (X ^ k)
[PROOFSTEP]
congr with i'
[GOAL]
case a.e_m.a.h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
i' x✝ : n
⊢ (x • stdBasisMatrix i j 1) i' x✝ = ↑(LinearMap.mulLeft R (stdBasisMatrix i j x, 1).fst) (1, X ^ k).fst i' x✝
[PROOFSTEP]
simp [stdBasisMatrix]
[GOAL]
case a.e_n.a
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
k : ℕ
x : R
i' : ℕ
⊢ coeff (X ^ k) i' = coeff (↑(LinearMap.mulLeft R (stdBasisMatrix i j x, 1).snd) (1, X ^ k).snd) i'
[PROOFSTEP]
simp [stdBasisMatrix]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)
[PROOFSTEP]
refine Polynomial.induction_on' p ?_ ?_
[GOAL]
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (p q : R[X]),
    coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k) →
      coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k) →
        coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k = stdBasisMatrix i j (coeff (p + q) k)
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)
hq : coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k)
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k = stdBasisMatrix i j (coeff (p + q) k)
[PROOFSTEP]
ext
[GOAL]
case refine_1.a.h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p✝ : R[X]
k : ℕ
p q : R[X]
hp : coeff (↑matPolyEquiv (stdBasisMatrix i j p)) k = stdBasisMatrix i j (coeff p k)
hq : coeff (↑matPolyEquiv (stdBasisMatrix i j q)) k = stdBasisMatrix i j (coeff q k)
i✝ x✝ : n
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (p + q))) k i✝ x✝ = stdBasisMatrix i j (coeff (p + q) k) i✝ x✝
[PROOFSTEP]
simp [hp, hq, coeff_add, DMatrix.add_apply, stdBasisMatrix_add]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k : ℕ
⊢ ∀ (n_1 : ℕ) (a : R),
    coeff (↑matPolyEquiv (stdBasisMatrix i j (↑(monomial n_1) a))) k = stdBasisMatrix i j (coeff (↑(monomial n_1) a) k)
[PROOFSTEP]
intro k x
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i j (↑(monomial k) x))) k✝ = stdBasisMatrix i j (coeff (↑(monomial k) x) k✝)
[PROOFSTEP]
simp only [matPolyEquiv_coeff_apply_aux_1, coeff_monomial]
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
⊢ (if k = k✝ then stdBasisMatrix i j x else 0) = stdBasisMatrix i j (if k = k✝ then x else 0)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : k = k✝
⊢ stdBasisMatrix i j x = stdBasisMatrix i j x
[PROOFSTEP]
funext
[GOAL]
case pos.h.h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : k = k✝
x✝¹ x✝ : n
⊢ stdBasisMatrix i j x x✝¹ x✝ = stdBasisMatrix i j x x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : ¬k = k✝
⊢ 0 = stdBasisMatrix i j 0
[PROOFSTEP]
funext
[GOAL]
case neg.h.h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
i j : n
p : R[X]
k✝ k : ℕ
x : R
h✝ : ¬k = k✝
x✝¹ x✝ : n
⊢ OfNat.ofNat 0 x✝¹ x✝ = stdBasisMatrix i j 0 x✝¹ x✝
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ coeff (↑matPolyEquiv m) k i j = coeff (m i j) k
[PROOFSTEP]
refine Matrix.induction_on' m ?_ ?_ ?_
[GOAL]
case refine_1
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ coeff (↑matPolyEquiv 0) k i j = coeff (OfNat.ofNat 0 i j) k
[PROOFSTEP]
simp
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ ∀ (p q : Matrix n n R[X]),
    coeff (↑matPolyEquiv p) k i j = coeff (p i j) k →
      coeff (↑matPolyEquiv q) k i j = coeff (q i j) k → coeff (↑matPolyEquiv (p + q)) k i j = coeff ((p + q) i j) k
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine_2
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
p q : Matrix n n R[X]
hp : coeff (↑matPolyEquiv p) k i j = coeff (p i j) k
hq : coeff (↑matPolyEquiv q) k i j = coeff (q i j) k
⊢ coeff (↑matPolyEquiv (p + q)) k i j = coeff ((p + q) i j) k
[PROOFSTEP]
simp [hp, hq]
[GOAL]
case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j : n
⊢ ∀ (i_1 j_1 : n) (x : R[X]),
    coeff (↑matPolyEquiv (stdBasisMatrix i_1 j_1 x)) k i j = coeff (stdBasisMatrix i_1 j_1 x i j) k
[PROOFSTEP]
intro i' j' x
[GOAL]
case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ coeff (↑matPolyEquiv (stdBasisMatrix i' j' x)) k i j = coeff (stdBasisMatrix i' j' x i j) k
[PROOFSTEP]
erw [matPolyEquiv_coeff_apply_aux_2]
[GOAL]
case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ stdBasisMatrix i' j' (coeff x k) i j = coeff (stdBasisMatrix i' j' x i j) k
[PROOFSTEP]
dsimp [stdBasisMatrix]
[GOAL]
case refine_3
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
⊢ (if i' = i ∧ j' = j then coeff x k else 0) = coeff (if i' = i ∧ j' = j then x else 0) k
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h✝ : i' = i ∧ j' = j
⊢ coeff x k = coeff x k
[PROOFSTEP]
rename_i h
[GOAL]
case neg
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h✝ : ¬(i' = i ∧ j' = j)
⊢ 0 = coeff 0 k
[PROOFSTEP]
rename_i h
[GOAL]
case pos
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : i' = i ∧ j' = j
⊢ coeff x k = coeff x k
[PROOFSTEP]
rcases h with ⟨rfl, rfl⟩
[GOAL]
case pos.intro
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i' j' : n
x : R[X]
⊢ coeff x k = coeff x k
[PROOFSTEP]
simp [stdBasisMatrix]
[GOAL]
case neg
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
k : ℕ
i j i' j' : n
x : R[X]
h : ¬(i' = i ∧ j' = j)
⊢ 0 = coeff 0 k
[PROOFSTEP]
simp [stdBasisMatrix, h]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = coeff p k i j
[PROOFSTEP]
have t : p = matPolyEquiv (matPolyEquiv.symm p) := by simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
⊢ p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
⊢ coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = coeff p k i j
[PROOFSTEP]
conv_rhs => rw [t]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
| coeff p k i j
[PROOFSTEP]
rw [t]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
| coeff p k i j
[PROOFSTEP]
rw [t]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
| coeff p k i j
[PROOFSTEP]
rw [t]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : (Matrix n n R)[X]
i j : n
k : ℕ
t : p = ↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)
⊢ coeff (↑(AlgEquiv.symm matPolyEquiv) p i j) k = coeff (↑matPolyEquiv (↑(AlgEquiv.symm matPolyEquiv) p)) k i j
[PROOFSTEP]
simp only [matPolyEquiv_coeff_apply]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
⊢ ↑matPolyEquiv (p • 1) = Polynomial.map (algebraMap R (Matrix n n R)) p
[PROOFSTEP]
ext m i j
[GOAL]
case a.a.h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ coeff (↑matPolyEquiv (p • 1)) m i j = coeff (Polynomial.map (algebraMap R (Matrix n n R)) p) m i j
[PROOFSTEP]
simp only [coeff_map, one_apply, algebraMap_matrix_apply, mul_boole, Pi.smul_apply, matPolyEquiv_coeff_apply]
[GOAL]
case a.a.h
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
⊢ coeff ((p • 1) i j) m = if i = j then ↑(algebraMap R R) (coeff p m) else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
h✝ : i = j
⊢ coeff ((p • 1) i j) m = ↑(algebraMap R R) (coeff p m)
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
h✝ : ¬i = j
⊢ coeff ((p • 1) i j) m = 0
[PROOFSTEP]
simp
[GOAL]
case pos
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
h✝ : i = j
⊢ coeff (p * OfNat.ofNat 1 i j) m = coeff p m
[PROOFSTEP]
rename_i h
[GOAL]
case neg
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
h✝ : ¬i = j
⊢ coeff (p * OfNat.ofNat 1 i j) m = 0
[PROOFSTEP]
rename_i h
[GOAL]
case pos
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
h : i = j
⊢ coeff (p * OfNat.ofNat 1 i j) m = coeff p m
[PROOFSTEP]
simp [h]
[GOAL]
case neg
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
p : R[X]
m : ℕ
i j : n
h : ¬i = j
⊢ coeff (p * OfNat.ofNat 1 i j) m = 0
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
⊢ support (m i j) ⊆ support (↑matPolyEquiv m)
[PROOFSTEP]
intro k
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ k ∈ support (m i j) → k ∈ support (↑matPolyEquiv m)
[PROOFSTEP]
contrapose
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ ¬k ∈ support (↑matPolyEquiv m) → ¬k ∈ support (m i j)
[PROOFSTEP]
simp only [not_mem_support_iff]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
⊢ coeff (↑matPolyEquiv m) k = 0 → coeff (m i j) k = 0
[PROOFSTEP]
intro hk
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : coeff (↑matPolyEquiv m) k = 0
⊢ coeff (m i j) k = 0
[PROOFSTEP]
rw [← matPolyEquiv_coeff_apply, hk]
[GOAL]
R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
m : Matrix n n R[X]
i j : n
k : ℕ
hk : coeff (↑matPolyEquiv m) k = 0
⊢ OfNat.ofNat 0 i j = 0
[PROOFSTEP]
rfl