awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
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
⊢ 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))
have dsimp : 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))))
            (CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u))))
        WalkingSpan.left) :
    Type u))
  (CommRingCat.Hom.hom (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))
Tactic: dsimp only [CommRingCat.pushoutCocone_inl, PushoutCocone.ι_app_left]
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
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
⊢ 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))))
              (CommRingCat.pushoutCocone (↑R : Type u) (↑S : Type u) (↑T : Type u))))
          WalkingSpan.left) :
      Type u))
    (CommRingCat.Hom.hom (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom))
have apply : P (R := (↑R : Type u)) (S := (↑T : Type u)) (algebraMap (↑R : Type u) (↑T : Type u))
Tactic: apply hP R T S (S ⊗[R] T)
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ↔
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
have refine_1 : ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : X ≅ Y)
  (f : Y ⟶ Z),
  toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
Tactic: refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
refine_1 :
  ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : X ≅ Y)
    (f : Y ⟶ Z),
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
⊢ (RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ↔
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
have refine_2 : ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : Y ≅ Z)
  (f : X ⟶ Y),
  toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)
Tactic: refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
refine_1 :
  ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : X ≅ Y)
    (f : Y ⟶ Z),
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
refine_2 :
  ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : Y ≅ Z)
    (f : X ⟶ Y),
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)
⊢ (RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ↔
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
have refine_3 : ∀ (h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso) {R S T : Type u}
  [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
  (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
Tactic: refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
refine_1 :
  ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : X ≅ Y)
    (f : Y ⟶ Z),
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (e.hom ≫ f)
refine_2 :
  ∀ (h : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {X Y Z : CommRingCat.{u}} (e : Y ≅ Z)
    (f : X ⟶ Y),
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f →
      toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) (f ≫ e.hom)
refine_3 :
  ∀ (h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso) {R S T : Type u}
    [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (e : S ≃+* T),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (e.toRingHom.comp f)
⊢ (RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) ↔
    (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
have refine_4 : ∀ (h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso) {R S T : Type u}
  [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : S →+* T) (e : R ≃+* S),
  (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) f →
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (f.comp e.toRingHom)
Tactic: refine ⟨fun h ↦ MorphismProperty.RespectsIso.mk _ ?_ ?_, fun h ↦ ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange ↔
    IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
have refine_1 : ∀ (h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange)
  (R S R' S' : Type u) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing R') (x_3 : CommRing S') (x_4 : Algebra R S)
  (x_5 : Algebra R R') (x_6 : Algebra R S') (x_7 : Algebra S S') (x_8 : Algebra R' S') (x_9 : IsScalarTower R S S')
  (x_10 : IsScalarTower R R' S') (hsq : Algebra.IsPushout R S R' S')
  (hRS : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R S)),
  (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R' S')
Tactic: refine ⟨fun h R S R' S' _ _ _ _ _ _ _ _ _ _ _ hsq hRS ↦ ?_,
      fun h ↦ ⟨fun {R} S R' S' f g f' g' hsq hf ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
refine_1 :
  ∀ (h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange)
    (R S R' S' : Type u) (x : CommRing R) (x_1 : CommRing S) (x_2 : CommRing R') (x_3 : CommRing S') (x_4 : Algebra R S)
    (x_5 : Algebra R R') (x_6 : Algebra R S') (x_7 : Algebra S S') (x_8 : Algebra R' S') (x_9 : IsScalarTower R S S')
    (x_10 : IsScalarTower R R' S') (hsq : Algebra.IsPushout R S R' S')
    (hRS : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R S)),
    (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R' S')
⊢ (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange ↔
    IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
have refine_2 : ∀ (h : IsStableUnderBaseChange.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) {R : CommRingCat.{u}}
  (S R' S' : CommRingCat.{u}) (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),
  toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f'
Tactic: refine ⟨fun h R S R' S' _ _ _ _ _ _ _ _ _ _ _ hsq hRS ↦ ?_,
      fun h ↦ ⟨fun {R} S R' S' f g f' g' hsq hf ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
h : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).IsStableUnderCobaseChange
R S R' S' : Type u
x : CommRing R
x_1 : CommRing S
x_2 : CommRing R'
x_3 : CommRing S'
x_4 : Algebra R S
x_5 : Algebra R R'
x_6 : Algebra R S'
x_7 : Algebra S S'
x_8 : Algebra R' S'
h_1 : IsScalarTower R S S'
h_2 : IsScalarTower R R' S'
hsq : Algebra.IsPushout R S R' S'
hRS : (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R S)
⊢ (fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) (algebraMap R' S')
have refine_1 : ∀
  (hsq :
    IsPushout (Z := CommRingCat.of R) (X := CommRingCat.of S) (Y := CommRingCat.of R') (P := CommRingCat.of S')
      (CommRingCat.ofHom (algebraMap R S)) (CommRingCat.ofHom (algebraMap R R')) (CommRingCat.ofHom (algebraMap S S'))
      (CommRingCat.ofHom (algebraMap R' S')))
  (hRS : P (algebraMap R S)), P (algebraMap R' S')
Tactic: rw [← CommRingCat.isPushout_iff_isPushout] at hsq
Cleared hypotheses: hsq, hRS
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (hypothesis)
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) := ⋯
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f'
have this : 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)
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (hypothesis)
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)
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f'
have this₁ : 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
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (hypothesis)
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
⊢ P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)
have this : (toMorphismProperty fun {R S : Type u} [CommRing R] [CommRing S] ↦ P).RespectsIso
Tactic: have : (toMorphismProperty P).RespectsIso := by
    rwa [← toMorphismProperty_respectsIso_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
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
⊢ P (CommRingCat.Hom.hom f) ↔ P (CommRingCat.Hom.hom g)
have 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
Tactic: change toMorphismProperty P _ ↔ toMorphismProperty P _
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
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
⊢ toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) f ↔
    toMorphismProperty (fun {R S : Type u} [CommRing R] [CommRing S] ↦ P) g
have 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
Tactic: rw [MorphismProperty.arrow_mk_iso_iff (toMorphismProperty P) e]
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
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))
have 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)
Tactic: ext r
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (hypothesis)
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'
⊢ P (algebraMap R S)
have this : 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]
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
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 (algebraMap R S)
have apply : P (S := R' ⊗[R] S) (algebraMap R' (R' ⊗[R] S))
Tactic: apply h₂ hQ
-- Lean 4 proof step from Mathlib.RingTheory.RingHomProperties (goal)
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 (S := R' ⊗[R] S) (algebraMap R' (R' ⊗[R] S))
have rw : P (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e.symm : S' →+* R' ⊗[R] S) (algebraMap R' S'))
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.RingInvo (goal)
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
⊢ e = f
have 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
Tactic: rcases e with ⟨⟨tE, _⟩, _⟩
Cleared hypotheses: e, h₁, h₂