awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u_3)),
          (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
            (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) f
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u_3)),
          (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
            (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) f

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
_ :
  ∀ [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u_3)),
          (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
            (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) f
⊢ ∀ [inst_1 : CommRing S] (f : R →+* S) (s : Set S),
    Eq (α := Ideal S) (Ideal.span s) ⊤ →
      (∀ (r : (↑s : Type u_3)),
          (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
            (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)) →
        (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) f

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
rw : ∀ (q : PrimeSpectrum S), Algebra.IsUnramifiedAt R q.asIdeal
⊢ f.FormallyUnramified

Tactic:
rw [FormallyUnramified, Algebra.formallyUnramified_iff_forall]

Premises used: Algebra.formallyUnramified_iff_forall, RingHom.FormallyUnramified
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
⊢ ∃ r ∈ s, Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x

Tactic:
simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
      (TopologicalSpace.Opens.mem_top x)

Premises used: Iff.mpr, TopologicalSpace.Opens.mem_top, Eq.ge, PrimeSpectrum.iSup_basicOpen_eq_top_iff'
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
obtain :
  ∀ (r : S) (hr : r ∈ s)
    (hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x),
    Algebra.IsUnramifiedAt R x.asIdeal
⊢ Algebra.IsUnramifiedAt R x.asIdeal

Tactic:
obtain ⟨r, hr, hrx⟩ : ∃ r ∈ s, x ∈ PrimeSpectrum.basicOpen r := by
    simpa using (PrimeSpectrum.iSup_basicOpen_eq_top_iff'.mpr hs).ge
      (TopologicalSpace.Opens.mem_top x)
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
⊢ Algebra.IsUnramifiedAt R x.asIdeal

Tactic:
Algebra.basicOpen_subset_unramifiedLocus_iff.mpr ?_ hrx

Premises used: Iff.mpr, Algebra.basicOpen_subset_unramifiedLocus_iff, Set.Mem, setOf, Algebra.unramifiedLocus
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
refine : Algebra.FormallyUnramified R (Localization.Away r)
⊢ Algebra.IsUnramifiedAt R x.asIdeal

Tactic:
refine Algebra.basicOpen_subset_unramifiedLocus_iff.mpr ?_ hrx

Premises used: Iff.mpr, Algebra.basicOpen_subset_unramifiedLocus_iff
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
⊢ (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
    (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S)) _ _
    (RingHom.comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f)

Tactic:
H ⟨r, hr⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
a :
  Algebra.FormallyUnramified R (Localization.Away r) ↔
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S)) _ _
      (RingHom.comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f)
⊢ Algebra.FormallyUnramified R (Localization.Away r)

Tactic:
convert! H ⟨r, hr⟩

Premises used: Subtype.mk
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
a :
  Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r) (RingHom.comp (algebraMap S (Localization.Away r)) f)
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S)) _ _
      (RingHom.comp (algebraMap S (Localization.Away (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) r hr) : S))) f)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_3)),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) _
      (Localization.Away (↑r : S)) _ _ (RingHom.comp (algebraMap S (Localization.Away (↑r : S))) f)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
r : S
hr : r ∈ s
hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x
a :
  Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r)
      (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S (Localization.Away r)) (algebraMap R S))
a₁ :
  Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r) (algebraMap R (Localization.Away r))
a₂ a₃ : Algebra.FormallyUnramified R (Localization.Away r) ↔ Algebra.FormallyUnramified R (Localization.Away r)
⊢ Algebra.FormallyUnramified R (Localization.Away r) ↔
    FormallyUnramified (S := Localization.Away r) (RingHom.comp (algebraMap S (Localization.Away r)) f)

Tactic:
rw [← algebraMap_toAlgebra f, ← IsScalarTower.algebraMap_eq,
    formallyUnramified_algebraMap]

Premises used: RingHom.formallyUnramified_algebraMap, IsScalarTower.algebraMap_eq, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
localizationAwayPreserves :
  LocalizationAwayPreserves.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
ofLocalizationSpanTarget :
  OfLocalizationSpanTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
ofLocalizationSpan : OfLocalizationSpan.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
StableUnderCompositionWithLocalizationAwayTarget :
  RingHom.StableUnderCompositionWithLocalizationAwayTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦
    FormallyUnramified
⊢ PropertyIsLocal.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
constructor
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ LocalizationAwayPreserves.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
isStableUnderBaseChange.localizationPreserves.away

Premises used: RingHom.FormallyUnramified.isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.localizationPreserves, RingHom.LocalizationPreserves.away
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ LocalizationAwayPreserves.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
exact isStableUnderBaseChange.localizationPreserves.away

Premises used: RingHom.FormallyUnramified.isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.localizationPreserves, RingHom.LocalizationPreserves.away
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ OfLocalizationSpanTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
ofLocalizationSpanTarget

Premises used: RingHom.FormallyUnramified.ofLocalizationSpanTarget
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ OfLocalizationSpanTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
exact ofLocalizationSpanTarget

Premises used: RingHom.FormallyUnramified.ofLocalizationSpanTarget
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ OfLocalizationSpan.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
ofLocalizationSpanTarget.ofLocalizationSpan
      (stableUnderComposition.stableUnderCompositionWithLocalizationAway
          holdsForLocalizationAway).1

Premises used: RingHom.FormallyUnramified.stableUnderComposition, RingHom.OfLocalizationSpanTarget.ofLocalizationSpan, And.left, RingHom.FormallyUnramified.ofLocalizationSpanTarget, RingHom.FormallyUnramified.holdsForLocalizationAway, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ OfLocalizationSpan.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
exact ofLocalizationSpanTarget.ofLocalizationSpan
      (stableUnderComposition.stableUnderCompositionWithLocalizationAway
          holdsForLocalizationAway).1

Premises used: RingHom.FormallyUnramified.stableUnderComposition, RingHom.OfLocalizationSpanTarget.ofLocalizationSpan, And.left, RingHom.FormallyUnramified.ofLocalizationSpanTarget, RingHom.FormallyUnramified.holdsForLocalizationAway, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ StableUnderCompositionWithLocalizationAwayTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦
    FormallyUnramified

Tactic:
(stableUnderComposition.stableUnderCompositionWithLocalizationAway
        holdsForLocalizationAway).2

Premises used: RingHom.FormallyUnramified.stableUnderComposition, And.right, RingHom.FormallyUnramified.holdsForLocalizationAway, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ StableUnderCompositionWithLocalizationAwayTarget.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦
    FormallyUnramified

Tactic:
exact (stableUnderComposition.stableUnderCompositionWithLocalizationAway
        holdsForLocalizationAway).2

Premises used: RingHom.FormallyUnramified.stableUnderComposition, And.right, RingHom.FormallyUnramified.holdsForLocalizationAway, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
h : (g.comp f).FormallyEtale
⊢ Algebra.FormallyUnramified R S

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
h : (g.comp f).FormallyEtale
algebraizeInst : Algebra.FormallyUnramified R S
⊢ Algebra.FormallyEtale R T

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
h : (g.comp f).FormallyEtale
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.FormallyUnramified R S
algebraizeInst_1 : Algebra.FormallyEtale R T
⊢ g.FormallyEtale

Tactic:
Algebra.FormallyEtale.of_restrictScalars (R := R)

Premises used: Algebra.FormallyEtale.of_restrictScalars, RingHom.FormallyEtale
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
T : Type u_3
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.FormallyUnramified
h : (g.comp f).FormallyEtale
algInst : Algebra R S := f.toAlgebra
algInst_1 : Algebra S T := g.toAlgebra
algInst_2 : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower R S T := ⋯
algebraizeInst : Algebra.FormallyUnramified R S
algebraizeInst_1 : Algebra.FormallyEtale R T
⊢ g.FormallyEtale

Tactic:
exact Algebra.FormallyEtale.of_restrictScalars (R := R)

Premises used: Algebra.FormallyEtale.of_restrictScalars
-- Module: Mathlib.RingTheory.RingHomProperties
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 ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P ((CommRingCat.Hom.hom (f ≫ g)).comp (asIso f).symm.commRingCatIsoToRingEquiv.toRingHom)

Tactic:
hP.2 (f ≫ g).hom (asIso f).symm.commRingCatIsoToRingEquiv H

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CommRingCat.Hom.hom, And.right, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.asIso
-- Module: Mathlib.RingTheory.RingHomProperties
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 ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
h : CommRingCat.Hom.hom g = (CommRingCat.Hom.hom (f ≫ g)).comp (asIso f).symm.commRingCatIsoToRingEquiv.toRingHom
⊢ P (CommRingCat.Hom.hom g)

Tactic:
convert! hP.2 (f ≫ g).hom (asIso f).symm.commRingCatIsoToRingEquiv H

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CommRingCat.Hom.hom, And.right, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.asIso
-- Module: Mathlib.RingTheory.RingHomProperties
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 ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ CommRingCat.Hom.hom g = (CommRingCat.Hom.hom (f ≫ g)).comp (asIso f).symm.commRingCatIsoToRingEquiv.toRingHom

Tactic:
simp [← CommRingCat.hom_comp]

Premises used: CommRingCat.hom_comp
-- Module: Mathlib.RingTheory.RingHomProperties
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 ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ P ((asIso g).symm.commRingCatIsoToRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (f ≫ g)))

Tactic:
hP.1 (f ≫ g).hom (asIso g).symm.commRingCatIsoToRingEquiv H

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CommRingCat.Hom.hom, And.left, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.asIso
-- Module: Mathlib.RingTheory.RingHomProperties
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 ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
h : CommRingCat.Hom.hom f = (asIso g).symm.commRingCatIsoToRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (f ≫ g))
⊢ P (CommRingCat.Hom.hom f)

Tactic:
convert! hP.1 (f ≫ g).hom (asIso g).symm.commRingCatIsoToRingEquiv H

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CommRingCat.Hom.hom, And.left, CategoryTheory.Iso.symm, CategoryTheory.CategoryStruct.comp, CategoryTheory.asIso
-- Module: Mathlib.RingTheory.RingHomProperties
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 ((CommRingCat.Hom.hom g).comp (CommRingCat.Hom.hom f))
⊢ CommRingCat.Hom.hom f = (asIso g).symm.commRingCatIsoToRingEquiv.toRingHom.comp (CommRingCat.Hom.hom (f ≫ g))

Tactic:
simp [← CommRingCat.hom_comp]

Premises used: CommRingCat.hom_comp
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
⊢ RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f

Tactic:
⟨?_, ?_⟩

Premises used: RingHom.RespectsIso, And.intro
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ Q
refine_1 :
  ∀ {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] (f : R →+* S) ↦ P f ∧ Q f) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (e.toRingHom.comp f)
refine_2 :
  ∀ {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] (f : R →+* S) ↦ P f ∧ Q f) f →
      (fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f) (f.comp e.toRingHom)
⊢ RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) ↦ P f ∧ Q f

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso.{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
e : S ≃+* T
hf : P f ∧ Q f
⊢ P (e.toRingHom.comp f) ∧ Q (e.toRingHom.comp f)

Tactic:
⟨hP.1 f e hf.1, hQ.1 f e hf.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 : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso.{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
e : S ≃+* T
hf : P f ∧ Q f
⊢ P (e.toRingHom.comp f) ∧ Q (e.toRingHom.comp f)

Tactic:
exact ⟨hP.1 f e hf.1, hQ.1 f e hf.2⟩
-- Module: Mathlib.RingTheory.RingHomProperties
Goal:
P Q : {R S : Type u} → [inst : CommRing R] → [inst_3 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso.{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 : S →+* T
e : R ≃+* S
hf : P f ∧ Q f
⊢ P (f.comp e.toRingHom) ∧ Q (f.comp e.toRingHom)

Tactic:
⟨hP.2 f e hf.1, hQ.2 f e hf.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 : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
hQ : RespectsIso.{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 : S →+* T
e : R ≃+* S
hf : P f ∧ Q f
⊢ P (f.comp e.toRingHom) ∧ Q (f.comp e.toRingHom)

Tactic:
exact ⟨hP.2 f e hf.1, hQ.2 f e hf.2⟩
-- Module: Mathlib.RingTheory.RingHomProperties
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 e.toRingHom
left :
  ∀ {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 (e.toRingHom.comp f)
right :
  ∀ {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 (f.comp e.toRingHom)
⊢ RespectsIso @P

Tactic:
constructor