awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S R' S' : CommRingCat
f : R ⟶ S
g : R ⟶ R'
f' : R' ⟶ S'
g' : S ⟶ S'
hsq : IsPushout g f f' g'
hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑R' : Type u) := (CommRingCat.Hom.hom g).toAlgebra
algInst_2 : Algebra (↑R' : Type u) (↑S' : Type u) := (CommRingCat.Hom.hom f').toAlgebra
algInst_3 : Algebra (↑S : Type u) (↑S' : Type u) := (CommRingCat.Hom.hom g').toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑S' : Type u) := ((CommRingCat.Hom.hom f').comp (CommRingCat.Hom.hom g)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑R' : Type u) (↑S' : Type u) := ⋯
⊢ IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑S' : Type u)

Tactic:
have : IsScalarTower R S S' := .of_algebraMap_eq fun x ↦ congr($(hsq.1.1).hom x)
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S R' S' : CommRingCat
f : R ⟶ S
g : R ⟶ R'
f' : R' ⟶ S'
g' : S ⟶ S'
hsq : IsPushout g f f' g'
hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑R' : Type u) := (CommRingCat.Hom.hom g).toAlgebra
algInst_2 : Algebra (↑R' : Type u) (↑S' : Type u) := (CommRingCat.Hom.hom f').toAlgebra
algInst_3 : Algebra (↑S : Type u) (↑S' : Type u) := (CommRingCat.Hom.hom g').toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑S' : Type u) := ((CommRingCat.Hom.hom f').comp (CommRingCat.Hom.hom g)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑R' : Type u) (↑S' : Type u) := ⋯
this : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑S' : Type u)
⊢ Algebra.IsPushout.{u, u, u, u} (↑R : Type u) (↑S : Type u) (↑R' : Type u) (↑S' : Type u)

Tactic:
have : Algebra.IsPushout R S R' S' := (CommRingCat.isPushout_iff_isPushout.mp hsq).symm
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S R' S' : CommRingCat
f : R ⟶ S
g : R ⟶ R'
f' : R' ⟶ S'
g' : S ⟶ S'
hsq : IsPushout g f f' g'
hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑R' : Type u) := (CommRingCat.Hom.hom g).toAlgebra
algInst_2 : Algebra (↑R' : Type u) (↑S' : Type u) := (CommRingCat.Hom.hom f').toAlgebra
algInst_3 : Algebra (↑S : Type u) (↑S' : Type u) := (CommRingCat.Hom.hom g').toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑S' : Type u) := ((CommRingCat.Hom.hom f').comp (CommRingCat.Hom.hom g)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑R' : Type u) (↑S' : Type u) := ⋯
this_1 : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑S' : Type u)
this : Algebra.IsPushout.{u, u, u, u} (↑R : Type u) (↑S : Type u) (↑R' : Type u) (↑S' : Type u)
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f'

Tactic:
h (R := R) (S := S) _ _ hf

Premises used: CommRingCat.carrier, RingHom.toMorphismProperty
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S R' S' : CommRingCat
f : R ⟶ S
g : R ⟶ R'
f' : R' ⟶ S'
g' : S ⟶ S'
hsq : IsPushout g f f' g'
hf : toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom f).toAlgebra
algInst_1 : Algebra (↑R : Type u) (↑R' : Type u) := (CommRingCat.Hom.hom g).toAlgebra
algInst_2 : Algebra (↑R' : Type u) (↑S' : Type u) := (CommRingCat.Hom.hom f').toAlgebra
algInst_3 : Algebra (↑S : Type u) (↑S' : Type u) := (CommRingCat.Hom.hom g').toAlgebra
algInst_4 : Algebra (↑R : Type u) (↑S' : Type u) := ((CommRingCat.Hom.hom f').comp (CommRingCat.Hom.hom g)).toAlgebra
scalarTowerInst : IsScalarTower.{u, u, u} (↑R : Type u) (↑R' : Type u) (↑S' : Type u) := ⋯
this_1 : IsScalarTower.{u, u, u} (↑R : Type u) (↑S : Type u) (↑S' : Type u)
this : Algebra.IsPushout.{u, u, u, u} (↑R : Type u) (↑S : Type u) (↑R' : Type u) (↑S' : Type u)
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f'

Tactic:
exact h (R := R) (S := S) _ _ hf

Premises used: CommRingCat.carrier
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
rwa rwa₁ rwa₂ rwa₃ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso

Tactic:
rwa [← toMorphismProperty_respectsIso_iff]

Premises used: RingHom.toMorphismProperty_respectsIso_iff
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso

Tactic:
have : (toMorphismProperty P).RespectsIso := by
    rwa [← toMorphismProperty_respectsIso_iff]
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
change :
  toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g
⊢ P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)

Tactic:
change toMorphismProperty P _ ↔ toMorphismProperty P _

Premises used: RingHom.toMorphismProperty
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
A B A' B' : CommRingCat
f : A ⟶ B
g : A' ⟶ B'
e : Arrow.mk f ≅ Arrow.mk g
this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
rw rw₁ :
  toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g ↔
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g

Tactic:
rw [MorphismProperty.arrow_mk_iso_iff (toMorphismProperty P) e]

Premises used: CategoryTheory.MorphismProperty.arrow_mk_iso_iff, RingHom.toMorphismProperty
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ 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], Q (algebraMap R S) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T)) → P (algebraMap 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'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
let : P (algebraMap R S)
⊢ P (algebraMap R S)

Tactic:
let e := h.symm.equiv
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ 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], Q (algebraMap R S) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T)) → P (algebraMap 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'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
a :
  ∀ (r : R'),
    Eq (α := R' ⊗[R] S)
      ((@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S') :
            (a : R') → R' ⊗[R] S)
          r :
        R' ⊗[R] S)
      ((algebraMap R' (R' ⊗[R] S) : (a : R') → R' ⊗[R] S) r : R' ⊗[R] S)
⊢ Eq (α := R' →+* R' ⊗[R] S)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))
    (algebraMap R' (R' ⊗[R] S))

Tactic:
ext r
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ 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], Q (algebraMap R S) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T)) → P (algebraMap 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'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
r : R'
⊢ Eq (α := R' ⊗[R] S)
    ((@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S') :
          (a : R') → R' ⊗[R] S)
        r :
      R' ⊗[R] S)
    ((algebraMap R' (R' ⊗[R] S) : (a : R') → R' ⊗[R] S) r : R' ⊗[R] S)

Tactic:
simp [e]
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ 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], Q (algebraMap R S) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T)) → P (algebraMap 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'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
⊢ Eq (α := R' →+* R' ⊗[R] S)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))
    (algebraMap R' (R' ⊗[R] S))

Tactic:
have : (e.symm : _ →+* _).comp (algebraMap R' S') = algebraMap R' (R' ⊗[R] S) := by
    ext r
    simp [e]
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ 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], Q (algebraMap R S) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T)) → P (algebraMap 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'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this :
  Eq (α := R' →+* R' ⊗[R] S)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))
    (algebraMap R' (R' ⊗[R] S))
apply : P (S := R' ⊗[R] S) (algebraMap R' (R' ⊗[R] S))
⊢ P (algebraMap R S)

Tactic:
apply h₂ hQ
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ 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], Q (algebraMap R S) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T)) → P (algebraMap 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'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this :
  Eq (α := R' →+* R' ⊗[R] S)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))
    (algebraMap R' (R' ⊗[R] S))
rw : P (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))
⊢ P (S := R' ⊗[R] S) (algebraMap R' (R' ⊗[R] S))

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ 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], Q (algebraMap R S) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T)) → P (algebraMap 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'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this :
  Eq (α := R' →+* R' ⊗[R] S)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))
    (algebraMap R' (R' ⊗[R] S))
⊢ P (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))

Tactic:
h₁.1 _ _ H

Premises used: MonoidHomClass.toMonoidHom, MulEquiv.toMonoidHom, And.left, RingHomClass.toRingHom, RingEquiv.toRingHom, Classical.choose
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_11 : CommRing S] → (R →+* S) → Prop
h₁ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ 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], Q (algebraMap R S) → P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T)) → P (algebraMap 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'
hQ : Q (algebraMap R R')
H : P (algebraMap R' S')
e : R' ⊗[R] S ≃ₐ[R'] S' := Algebra.IsPushout.equiv R R' S S'
this :
  Eq (α := R' →+* R' ⊗[R] S)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))
    (algebraMap R' (R' ⊗[R] S))
⊢ P (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))

Tactic:
exact h₁.1 _ _ H

Premises used: And.left
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hPQ :
  CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Q
h : Q (algebraMap R S)
H : P (S := S ⊗[R] T) (algebraMap S (S ⊗[R] T))
⊢ P (algebraMap R T)

Tactic:
let _ : Algebra T (S ⊗[R] T) := Algebra.TensorProduct.rightAlgebra
  hPQ h H

Premises used: Algebra.TensorProduct.rightAlgebra
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hPQ :
  CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Q
h : Q (algebraMap R T)
H : P (R := T) (S := S ⊗[R] T) (AlgHom.toRingHom Algebra.TensorProduct.includeRight)
let : P (algebraMap R S)
⊢ P (algebraMap R S)

Tactic:
let _ : Algebra T (S ⊗[R] T) := Algebra.TensorProduct.rightAlgebra
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
R S T : Type u
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : CommRing T
inst_4 : Algebra R T
hPQ :
  CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Q
h : Q (algebraMap R T)
H : P (R := T) (S := S ⊗[R] T) (AlgHom.toRingHom Algebra.TensorProduct.includeRight)
x : Algebra T (S ⊗[R] T) := Algebra.TensorProduct.rightAlgebra
⊢ P (algebraMap R S)

Tactic:
apply hPQ h H
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q P' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP :
  CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Q
hP' :
  CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P') fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Q
⊢ CodescendsAlong.{u} (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ P' f)
    fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q

Tactic:
fun _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ h₁ h₂ ↦ ⟨hP h₁ h₂.1, hP' h₁ h₂.2⟩

Premises used: And.right, And.left, And.intro, RingHom.CodescendsAlong
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_5 : CommRing S] → (R →+* S) → Prop
hP : HasEqualizers.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : HasEqualizers.{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
inst_3 : Algebra R S
inst_4 : Algebra R T
⊢ ∀ (f g : S →ₐ[R] T),
    (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (algebraMap R S) →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (algebraMap R T) →
        (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) _ ↥(AlgHom.equalizer f g) _ _
          (algebraMap R ↥(AlgHom.equalizer f g))

Tactic:
fun f g hf hg ↦ ⟨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_2 : CommRing S] → (R →+* S) → Prop
hP : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : HasFiniteProducts.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
R : Type u
inst : CommRing R
ι : Type u
inst_1 : _root_.Finite ι
⊢ ∀ (S : ι → Type u) [inst_2 : (i : ι) → CommRing (S i)] [inst_3 : (i : ι) → Algebra R (S i)],
    (∀ (i : ι),
        (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) _ (S i) _ _ (algebraMap R (S i))) →
      (@fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) _ ((i : ι) → S i) _ _
        (algebraMap R ((i : ι) → S i))

Tactic:
fun _ _ _ hS ↦ ⟨hP _ fun i ↦ (hS i).1, hQ _ fun i ↦ (hS i).2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.RingTheory.RingInvo
Goal:
F : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : EquivLike F R Rᵐᵒᵖ
e f : RingInvo R
h₁ : e.toFun = f.toFun
h₂ : e.invFun = f.invFun
rcases :
  ∀ (tE : R ≃ Rᵐᵒᵖ) (map_mul' : ∀ (x y : R), tE.toFun (x * y) = tE.toFun x * tE.toFun y)
    (map_add' : ∀ (x y : R), tE.toFun (x + y) = tE.toFun x + tE.toFun y)
    (involution' :
      ∀ (x : R),
        MulOpposite.unop
            ({ toEquiv := tE, map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun
              (MulOpposite.unop ({ toEquiv := tE, map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun x))) =
          x)
    (h₁ :
      { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.toFun =
        f.toFun)
    (h₂ :
      { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.invFun =
        f.invFun),
    { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R } = f
⊢ e = f

Tactic:
rcases e with ⟨⟨tE, _⟩, _⟩
-- Module: Mathlib.RingTheory.RingInvo
Goal:
F : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : EquivLike F R Rᵐᵒᵖ
f : RingInvo R
tE : R ≃ Rᵐᵒᵖ
map_mul' : ∀ (x y : R), tE.toFun (x * y) = tE.toFun x * tE.toFun y
map_add' : ∀ (x y : R), tE.toFun (x + y) = tE.toFun x + tE.toFun y
involution' :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tE, map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun
          (MulOpposite.unop ({ toEquiv := tE, map_mul' := map_mul', map_add' := map_add' : R ≃+* Rᵐᵒᵖ }.toFun x))) =
      x
h₁ :
  { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.toFun = f.toFun
h₂ :
  { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.invFun =
    f.invFun
rcases :
  ∀ (tF : R ≃ Rᵐᵒᵖ) (map_mul'_1 : ∀ (x y : R), tF.toFun (x * y) = tF.toFun x * tF.toFun y)
    (map_add'_1 : ∀ (x y : R), tF.toFun (x + y) = tF.toFun x + tF.toFun y)
    (involution'_1 :
      ∀ (x : R),
        MulOpposite.unop
            ({ toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* Rᵐᵒᵖ }.toFun
              (MulOpposite.unop
                ({ toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1 : R ≃+* Rᵐᵒᵖ }.toFun x))) =
          x)
    (h₁ :
      { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.toFun =
        { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 :
            RingInvo R }.toFun)
    (h₂ :
      { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R }.invFun =
        { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 :
            RingInvo R }.invFun),
    { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R } =
      { toEquiv := tF, map_mul' := map_mul'_1, map_add' := map_add'_1, involution' := involution'_1 }
⊢ { toEquiv := tE, map_mul' := map_mul', map_add' := map_add', involution' := involution' : RingInvo R } = f

Tactic:
rcases f with ⟨⟨tF, _⟩, _⟩
-- Module: Mathlib.RingTheory.RingInvo
Goal:
R : Type u_2
inst : Semiring R
f : RingInvo R
x : R
⊢ MulOpposite.unop ((f : (a : R) → Rᵐᵒᵖ) (MulOpposite.unop ((f : (a : R) → Rᵐᵒᵖ) x))) = x

Tactic:
f.involution' x

Premises used: RingInvo.involution'