awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
e : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
        Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y))
      (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))
this : Algebra R S := f.toAlgebra
x : S
r : (↑s : Type u_1)
b : R
n : ℕ
e' :
  Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (β := S) x
          ((↑(Subtype.mk (p := fun (x : S) ↦
                  Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
                  ((f : (a : R) → S)
                    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
                      R))
                  ⋯) :
              S) :
            S)) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        ((f : (a : R) → S) b) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n' : ℕ
e'' :
  HPow.hPow (α := S) ((f : (a : R) → S) (↑r : R) : S) n' * HMul.hMul (β := S) x ((f : (a : R) → S) ((↑r : R) ^ n) : S) =
    HMul.hMul (β := S) (HPow.hPow (α := S) ((f : (a : R) → S) (↑r : R) : S) n') ((f : (a : R) → S) b : S)
⊢ HMul.hMul (α := S) ((f : (a : R) → S) ((↑r : R) ^ (n' + n)) : S) x = (f : (a : R) → S) ((↑r : R) ^ n' * b)

Tactic:
rw [mul_comm x, ← mul_assoc, ← map_pow, ← map_mul, ← map_mul, ← pow_add] at e''

Premises used: mul_assoc, pow_add, map_pow, map_mul, mul_comm
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
e : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
        Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y))
      (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))
this : Algebra R S := f.toAlgebra
x : S
r : (↑s : Type u_1)
b : R
n : ℕ
e' :
  Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (β := S) x
          ((↑(Subtype.mk (p := fun (x : S) ↦
                  Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
                  ((f : (a : R) → S)
                    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
                      R))
                  ⋯) :
              S) :
            S)) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        ((f : (a : R) → S) b) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n' : ℕ
e'' : HMul.hMul (α := S) ((f : (a : R) → S) ((↑r : R) ^ (n' + n)) : S) x = (f : (a : R) → S) ((↑r : R) ^ n' * b)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)

Tactic:
⟨n' + n, _, e''.symm⟩

Premises used: HAdd.hAdd, Exists.intro, Eq.symm
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u_1
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
s : Set R
e : Eq (α := Ideal R) (Ideal.span s) ⊤
H :
  ∀ (r : (↑s : Type u_1)),
    (@fun {X Y : Type u_1} [CommRing X] [CommRing Y] (f : X →+* Y) ↦
        Function.Surjective (α := X) (β := Y) (⇑f : (a : X) → Y))
      (Localization.Away (↑r : R)) _ _ _ (Localization.awayMap f (↑r : R))
this : Algebra R S := f.toAlgebra
x : S
r : (↑s : Type u_1)
b : R
n : ℕ
e' :
  Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (HMul.hMul (β := S) x
          ((↑(Subtype.mk (p := fun (x : S) ↦
                  Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
                  ((f : (a : R) → S)
                    (↑(Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
                          ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯) :
                      R))
                  ⋯) :
              S) :
            S)) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((algebraMap S (Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S)) :
          (a : S) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        ((f : (a : R) → S) b) :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
n' : ℕ
e'' : HMul.hMul (α := S) ((f : (a : R) → S) ((↑r : R) ^ (n' + n)) : S) x = (f : (a : R) → S) ((↑r : R) ^ n' * b)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)

Tactic:
exact ⟨n' + n, _, e''.symm⟩
-- Module: Mathlib.RingTheory.RingHom.Surjective
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
h : Function.Surjective (α := R) (β := S) (⇑f : (a : R) → S)
P : Ideal S
inst_2 : P.IsPrime
⊢ Function.Surjective (α := Localization.AtPrime (Ideal.comap f P)) (β := Localization.AtPrime P)
    (⇑(Localization.localRingHom (Ideal.comap f P) P f ⋯) :
      (a : Localization.AtPrime (Ideal.comap f P)) → Localization.AtPrime P)

Tactic:
have : IsLocalization (Submonoid.map f (Ideal.comap f P).primeCompl) (Localization.AtPrime P) :=
    (Submonoid.map_comap_eq_of_surjective h P.primeCompl).symm ▸ Localization.isLocalization
  surjective_localizationPreserves _ _ _ _ h

Premises used: Set.Mem, Localization.AtPrime, Eq.rec, Localization.isLocalization, Ideal.comap, Ideal.primeCompl, RingHom.surjective_localizationPreserves, Eq.symm, Submonoid.map_comap_eq_of_surjective
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.FormallyUnramified R S ↔ Algebra.FormallyUnramified R S
rw₁ rw₂ : Algebra.FormallyUnramified R S ↔ Algebra.FormallyUnramified R S
⊢ FormallyUnramified (algebraMap R S) ↔ Algebra.FormallyUnramified R S

Tactic:
rw [FormallyUnramified, toAlgebra_algebraMap]

Premises used: RingHom.FormallyUnramified, toAlgebra_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
algInst : Algebra R S := f.toAlgebra
⊢ f.FormallyUnramified

Tactic:
Algebra.FormallyUnramified.of_surjective (Algebra.ofId R S) hf

Premises used: Algebra.FormallyUnramified.of_surjective, Algebra.ofId, RingHom.FormallyUnramified
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
algInst : Algebra R S := f.toAlgebra
⊢ f.FormallyUnramified

Tactic:
exact Algebra.FormallyUnramified.of_surjective (Algebra.ofId R S) hf

Premises used: Algebra.FormallyUnramified.of_surjective, Algebra.ofId
-- 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
h : (g.comp f).FormallyUnramified
⊢ Algebra.FormallyUnramified 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
h : (g.comp f).FormallyUnramified
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 T
⊢ g.FormallyUnramified

Tactic:
Algebra.FormallyUnramified.of_restrictScalars R _ _

Premises used: Algebra.FormallyUnramified.of_restrictScalars, RingHom.FormallyUnramified
-- 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
h : (g.comp f).FormallyUnramified
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 T
⊢ g.FormallyUnramified

Tactic:
exact Algebra.FormallyUnramified.of_restrictScalars R _ _

Premises used: Algebra.FormallyUnramified.of_restrictScalars
-- 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
hg : g.FormallyUnramified
⊢ 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
hg : g.FormallyUnramified
algebraizeInst : Algebra.FormallyUnramified R S
⊢ Algebra.FormallyUnramified S 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
hg : g.FormallyUnramified
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.FormallyUnramified S T
⊢ (g.comp f).FormallyUnramified

Tactic:
Algebra.FormallyUnramified.comp R S T

Premises used: Algebra.FormallyUnramified.comp, RingHom.FormallyUnramified
-- 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
hg : g.FormallyUnramified
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.FormallyUnramified S T
⊢ (g.comp f).FormallyUnramified

Tactic:
exact Algebra.FormallyUnramified.comp R S T

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

Tactic:
fun _ _ _ _ _ _ _ _ hf hg ↦ .comp hf hg

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

Tactic:
stableUnderComposition.respectsIso ?_

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.FormallyUnramified.stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
refine : ∀ {R S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified
⊢ RespectsIso.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
refine stableUnderComposition.respectsIso ?_

Premises used: RingHom.StableUnderComposition.respectsIso, RingHom.FormallyUnramified.stableUnderComposition
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
_ : ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
_ : ∀ [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified
⊢ ∀ [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ e.toRingHom.FormallyUnramified

Tactic:
.of_surjective e.surjective

Premises used: RingEquiv.surjective, RingHom.FormallyUnramified.of_surjective
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
e : R ≃+* S
⊢ e.toRingHom.FormallyUnramified

Tactic:
exact .of_surjective e.surjective
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ IsStableUnderBaseChange.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
.mk respectsIso ?_

Premises used: RingHom.IsStableUnderBaseChange.mk, RingHom.FormallyUnramified.respectsIso
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
refine :
  ∀ ⦃R S T : Type u_3⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    FormallyUnramified (algebraMap R T) →
      FormallyUnramified (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
⊢ IsStableUnderBaseChange.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
refine .mk respectsIso ?_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : FormallyUnramified (algebraMap R T)
rw : ∀ (H : Algebra.FormallyUnramified R T), Algebra.FormallyUnramified S (TensorProduct R S T)
⊢ FormallyUnramified (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))

Tactic:
rw [formallyUnramified_algebraMap] at H ⊢

Premises used: RingHom.formallyUnramified_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
inst_3 : Algebra R S
inst_4 : Algebra R T
H : Algebra.FormallyUnramified R T
⊢ Algebra.FormallyUnramified S (TensorProduct R S T)

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) (algebraMap R S)
⊢ ∀ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) (algebraMap R S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
_ :
  ∀ [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) (algebraMap R S)
⊢ ∀ [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) (algebraMap R S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
_ :
  ∀ [inst_2 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) (algebraMap R S)
⊢ ∀ [inst_2 : Algebra R S] (M : Submonoid R) [IsLocalization M S],
    (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) (algebraMap R S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
_ : ∀ [IsLocalization M S], FormallyUnramified (algebraMap R S)
⊢ ∀ [IsLocalization M S],
    (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) (algebraMap R S)

Tactic:
_
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
rw : Algebra.FormallyUnramified R S
⊢ FormallyUnramified (algebraMap R S)

Tactic:
rw [formallyUnramified_algebraMap]

Premises used: RingHom.formallyUnramified_algebraMap
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ Algebra.FormallyUnramified R S

Tactic:
.of_isLocalization M

Premises used: Algebra.FormallyUnramified.of_isLocalization
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
M : Submonoid R
inst_3 : IsLocalization M S
⊢ Algebra.FormallyUnramified R S

Tactic:
exact .of_isLocalization M
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
⊢ HoldsForLocalizationAway.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified

Tactic:
holdsForLocalization.holdsForLocalizationAway

Premises used: RingHom.FormallyUnramified.holdsForLocalization, RingHom.HoldsForLocalization.holdsForLocalizationAway
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
_ :
  ∀ [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
          (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
          (Localization.localRingHom (Ideal.comap f J) J 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),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
          (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
          (Localization.localRingHom (Ideal.comap f J) J 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),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
          (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
          (Localization.localRingHom (Ideal.comap f J) J f ⋯)) →
      (fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop)) f
⊢ ∀ [inst_1 : CommRing S] (f : R →+* S),
    (∀ (J : Ideal S) (x : J.IsPrime),
        (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
          (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
          (Localization.localRingHom (Ideal.comap f J) J 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
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J 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
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this : Algebra Rₓ Sₓ := toAlgebra (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯)
⊢ IsScalarTower R Rₓ Sₓ

Tactic:
have : IsScalarTower R Rₓ Sₓ := .of_algebraMap_eq
    fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this_1 : Algebra Rₓ Sₓ := toAlgebra (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯)
this : IsScalarTower R Rₓ Sₓ
⊢ Algebra.FormallyUnramified Rₓ Sₓ

Tactic:
have : Algebra.FormallyUnramified Rₓ Sₓ := H _ _
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this_1 : Algebra Rₓ Sₓ := toAlgebra (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯)
this_2 : IsScalarTower R Rₓ Sₓ
this : Algebra.FormallyUnramified Rₓ Sₓ
⊢ Algebra.IsUnramifiedAt R x.asIdeal

Tactic:
Algebra.FormallyUnramified.comp R Rₓ Sₓ

Premises used: Algebra.FormallyUnramified.comp
-- Module: Mathlib.RingTheory.RingHom.Unramified
Goal:
R S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
H :
  ∀ (J : Ideal S) (x : J.IsPrime),
    (@fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ (FormallyUnramified : (f : R →+* S) → Prop))
      (Localization.AtPrime (Ideal.comap f J)) (Localization.AtPrime J) _ _
      (Localization.localRingHom (Ideal.comap f J) J f ⋯)
algInst : Algebra R S := f.toAlgebra
x : PrimeSpectrum S
Rₓ : Type u_3 := Localization.AtPrime (Ideal.comap f x.asIdeal)
Sₓ : Type u_3 := Localization.AtPrime x.asIdeal
this_1 : Algebra Rₓ Sₓ := toAlgebra (Localization.localRingHom (Ideal.comap f x.asIdeal) x.asIdeal f ⋯)
this_2 : IsScalarTower R Rₓ Sₓ
this : Algebra.FormallyUnramified Rₓ Sₓ
⊢ Algebra.IsUnramifiedAt R x.asIdeal

Tactic:
exact Algebra.FormallyUnramified.comp R Rₓ Sₓ

Premises used: Algebra.FormallyUnramified.comp