awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
e : S ≃+* T
H left : P f
left₁ : P e.toRingHom
⊢ P (e.toRingHom.comp f)

Tactic:
apply hP
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P f

Tactic:
H
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P e.toRingHom

Tactic:
hP' e
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
e : S ≃+* T
H : P f
⊢ P f

Tactic:
exacts [H, hP' e]
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
right : P e.toRingHom
right₁ : P f
⊢ P (f.comp e.toRingHom)

Tactic:
apply hP
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P e.toRingHom

Tactic:
hP' e
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P f

Tactic:
H
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition @P
hP' : ∀ {R S : Type u} [inst : CommRing R] [inst_3 : CommRing S] (e : R ≃+* S), P e.toRingHom
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : S →+* T
e : R ≃+* S
H : P f
⊢ P e.toRingHom

Tactic:
exacts [hP' e, H]
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : P f ∧ Q f
hg : P g ∧ Q g
⊢ P (g.comp f) ∧ Q (g.comp f)

Tactic:
⟨hP f g hf.1 hg.1, hQ f g hf.2 hg.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : StableUnderComposition.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : P f ∧ Q f
hg : P g ∧ Q g
⊢ P (g.comp f) ∧ Q (g.comp f)

Tactic:
exact ⟨hP f g hf.1 hg.1, hQ f g hf.2 hg.2⟩
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
let : P (algebraMap R' S')
⊢ P (algebraMap R' S')

Tactic:
let e := h.symm.1.equiv
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : R' ⊗[R] S
suffices :
  (↑R :
        {S M M₂ : Type u} →
          [inst : Semiring R] →
            [inst_11 : Semiring S] →
              [inst_12 : AddCommMonoid M] →
                [inst_13 : AddCommMonoid M₂] →
                  [inst_14 : Module R M] →
                    [inst_15 : Module R M₂] →
                      [inst_16 : Module S M] →
                        [inst_17 : Module S M₂] →
                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₛₗ[id S] M₂) → M →ₛₗ[id R] M₂)
      (↑e : R' ⊗[R] S →ₛₗ[id R'] S') =
    f'.toLinearMap
⊢ Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')

Tactic:
suffices e.toLinearMap.restrictScalars R = f'.toLinearMap from congr($this x)
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x_1 : R' ⊗[R] S
x : R'
y : S
⊢ Eq (α := S')
    (((↑R :
              {S M M₂ : Type u} →
                [inst : Semiring R] →
                  [inst_11 : Semiring S] →
                    [inst_12 : AddCommMonoid M] →
                      [inst_13 : AddCommMonoid M₂] →
                        [inst_14 : Module R M] →
                          [inst_15 : Module R M₂] →
                            [inst_16 : Module S M] →
                              [inst_17 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₛₗ[id S] M₂) → M →ₛₗ[id R] M₂)
            (↑e : R' ⊗[R] S →ₛₗ[id R'] S') :
          (a : R' ⊗[R] S) → S')
        (x ⊗ₜ[R] y) :
      S')
    ((f'.toLinearMap : (a : R' ⊗[R] S) → S') (x ⊗ₜ[R] y) : S')

Tactic:
simp [e, f', IsBaseChange.equiv_tmul, Algebra.smul_def]

Premises used: IsBaseChange.equiv_tmul, Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
x : R' ⊗[R] S
⊢ (↑R :
        {S M M₂ : Type u} →
          [inst : Semiring R] →
            [inst_11 : Semiring S] →
              [inst_12 : AddCommMonoid M] →
                [inst_13 : AddCommMonoid M₂] →
                  [inst_14 : Module R M] →
                    [inst_15 : Module R M₂] →
                      [inst_16 : Module S M] →
                        [inst_17 : Module S M₂] →
                          [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₛₗ[id S] M₂) → M →ₛₗ[id R] M₂)
      (↑e : R' ⊗[R] S →ₛₗ[id R'] S') =
    f'.toLinearMap

Tactic:
exact ext' fun x y ↦ by simp [e, f', IsBaseChange.equiv_tmul, Algebra.smul_def]

Premises used: TensorProduct.ext'
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
⊢ ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')

Tactic:
have hef (x : _) : e x = f' x := by
    suffices e.toLinearMap.restrictScalars R = f'.toLinearMap from congr($this x)
    exact ext' fun x y ↦ by simp [e, f', IsBaseChange.equiv_tmul, Algebra.smul_def]
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
x y : R' ⊗[R] S
simp_rw :
  (f' : (a : R' ⊗[R] S) → S') (x * y) =
    HMul.hMul (α := S') (β := S') ((f' : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') y : S')
⊢ (e : (a : R' ⊗[R] S) → S') (x * y) =
    HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')

Tactic:
simp_rw [hef, map_mul]

Premises used: map_mul
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
⊢ ∀ (x y : R' ⊗[R] S),
    (e : (a : R' ⊗[R] S) → S') (x * y) =
      HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')

Tactic:
have hemul (x y : _) : e (x * y) = e x * e y := by simp_rw [hef, map_mul]
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
hemul :
  ∀ (x y : R' ⊗[R] S),
    (e : (a : R' ⊗[R] S) → S') (x * y) =
      HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')
⊢ P
    ({ toFun := (↑e : R' ⊗[R] S →ₛₗ[id R'] S').toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯,
            map_mul' := hemul, map_add' := ⋯ : R' ⊗[R] S ≃+* S' }.toRingHom.comp
      (algebraMap R' (R' ⊗[R] S)))

Tactic:
h₁.1 _ { e with map_mul' := hemul } (h₂ H)

Premises used: LinearEquiv.right_inv, LinearEquiv.left_inv, Equiv.mk, LinearMap.toAddHom, AddHom.map_add', LinearEquiv.invFun, LinearEquiv.toLinearMap, And.left, RingEquiv.mk, AddHom.toFun
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
hemul :
  ∀ (x y : R' ⊗[R] S),
    (e : (a : R' ⊗[R] S) → S') (x * y) =
      HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')
h₃ :
  Eq (α := R' →+* S') (algebraMap R' S')
    ({ toFun := (↑e : R' ⊗[R] S →ₛₗ[id R'] S').toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯,
            map_mul' := hemul, map_add' := ⋯ : R' ⊗[R] S ≃+* S' }.toRingHom.comp
      (algebraMap R' (R' ⊗[R] S)))
⊢ P (algebraMap R' S')

Tactic:
convert! h₁.1 _ { e with map_mul' := hemul } (h₂ H)

Premises used: LinearEquiv.right_inv, LinearEquiv.left_inv, Equiv.mk, LinearMap.toAddHom, AddHom.map_add', LinearEquiv.invFun, LinearEquiv.toLinearMap, And.left, RingEquiv.mk, AddHom.toFun
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
hemul :
  ∀ (x y : R' ⊗[R] S),
    (e : (a : R' ⊗[R] S) → S') (x * y) =
      HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')
h₃ :
  ∀ (x : R'),
    Eq (α := S') ((algebraMap R' S' : (a : R') → S') x : S')
      (({ toFun := (↑e : R' ⊗[R] S →ₛₗ[id R'] S').toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯,
                    map_mul' := hemul, map_add' := ⋯ : R' ⊗[R] S ≃+* S' }.toRingHom.comp
              (algebraMap R' (R' ⊗[R] S)) :
            (a : R') → S')
          x :
        S')
⊢ Eq (α := R' →+* S') (algebraMap R' S')
    ({ toFun := (↑e : R' ⊗[R] S →ₛₗ[id R'] S').toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯,
            map_mul' := hemul, map_add' := ⋯ : R' ⊗[R] S ≃+* S' }.toRingHom.comp
      (algebraMap R' (R' ⊗[R] S)))

Tactic:
ext x
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso @P
h₂ :
  ∀ ⦃R S T : Type u⦄ [inst : CommRing R] [inst_11 : CommRing S] [inst_12 : CommRing T] [inst_13 : Algebra R S]
    [inst_14 : Algebra R T], P (algebraMap R T) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
R S R' S' : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R S
inst_5 : Algebra R R'
inst_6 : Algebra R S'
inst_7 : Algebra S S'
inst_8 : Algebra R' S'
inst_9 : IsScalarTower R S S'
inst_10 : IsScalarTower R R' S'
h : Algebra.IsPushout R S R' S'
H : P (algebraMap R S)
e : R' ⊗[R] S ≃ₛₗ[id R'] S' := IsBaseChange.equiv (f := AlgHom.toLinearMap (IsScalarTower.toAlgHom R S S')) ⋯
f' : R' ⊗[R] S →ₐ[R] S' :=
  Algebra.TensorProduct.productMap (IsScalarTower.toAlgHom R R' S') (IsScalarTower.toAlgHom R S S')
hef : ∀ (x : R' ⊗[R] S), Eq (α := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((f' : (a : R' ⊗[R] S) → S') x : S')
hemul :
  ∀ (x y : R' ⊗[R] S),
    (e : (a : R' ⊗[R] S) → S') (x * y) =
      HMul.hMul (α := S') (β := S') ((e : (a : R' ⊗[R] S) → S') x : S') ((e : (a : R' ⊗[R] S) → S') y : S')
x : R'
⊢ Eq (α := S') ((algebraMap R' S' : (a : R') → S') x : S')
    (({ toFun := (↑e : R' ⊗[R] S →ₛₗ[id R'] S').toFun, invFun := e.invFun, left_inv := ⋯, right_inv := ⋯,
                  map_mul' := hemul, map_add' := ⋯ : R' ⊗[R] S ≃+* S' }.toRingHom.comp
            (algebraMap R' (R' ⊗[R] S)) :
          (a : R') → S')
        x :
      S')

Tactic:
simp [e, h.symm.1.equiv_tmul, Algebra.smul_def]

Premises used: Algebra.IsPushout.out, IsBaseChange.equiv_tmul, Algebra.smul_def
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
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
h : P (algebraMap R S)
⊢ P (S := T ⊗[R] S) (algebraMap T (T ⊗[R] S))

Tactic:
hP _ _ _ _ h
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
hP' : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
letI : P (S := (↑(pushout f g) : Type u)) (CommRingCat.Hom.hom (pushout.inl f g))
⊢ P (S := (↑(pushout f g) : Type u)) (CommRingCat.Hom.hom (pushout.inl f g))

Tactic:
letI := f.hom.toAlgebra
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : IsStableUnderBaseChange @P
hP' : RespectsIso @P
R S T : CommRingCat
f : R ⟶ S
g : R ⟶ T
H : P (CommRingCat.Hom.hom g)
this_1 : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
this : Algebra (↑R : Type u) (↑T : Type u) := (CommRingCat.Hom.hom g).toAlgebra
rw :
  P (R := (↑S : Type u)) (S :=
    (↑(Functor.obj
          (Functor.obj (Functor.const WalkingSpan)
            (Cocone.pt (F :=
              span (X := CommRingCat.of (↑R : Type u)) (Y := CommRingCat.of (↑S : Type u)) (Z :=
                CommRingCat.of (↑T : Type u)) (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
                (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u))))
              (ColimitCocone.cocone
                { cocone := CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u),
                  isColimit := CommRingCat.pushoutCoconeIsColimit (↑R : Type u) (↑S : Type u) (↑T : Type u) :
                  ColimitCocone
                    (span (X := CommRingCat.of (↑R : Type u)) (Y := CommRingCat.of (↑S : Type u)) (Z :=
                      CommRingCat.of (↑T : Type u)) (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u)))
                      (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑T : Type u)))) })))
          WalkingSpan.left) :
      Type u))
    (CommRingCat.Hom.hom
      (NatTrans.app
        (Cocone.ι
          (ColimitCocone.cocone
            { cocone := CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u),
              isColimit := CommRingCat.pushoutCoconeIsColimit (↑R : Type u) (↑S : Type u) (↑T : Type u) }))
        WalkingSpan.left))
⊢ P (S := (↑(pushout f g) : Type u)) (CommRingCat.Hom.hom (pushout.inl f g))

Tactic:
rw [← show _ = pushout.inl f g from
      colimit.isoColimitCocone_ι_inv ⟨_, CommRingCat.pushoutCoconeIsColimit R S T⟩ WalkingSpan.left,
    CommRingCat.hom_comp, hP'.cancel_right_isIso]

Premises used: CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv, CommRingCat.pushoutCoconeIsColimit, CommRingCat.carrier, RingHom.RespectsIso.cancel_right_isIso, CategoryTheory.Limits.WalkingSpan.left, CommRingCat.hom_comp, CategoryTheory.Limits.ColimitCocone.mk, CommRingCat.pushoutCocone