awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
Goal:
introv introv₁ introv₂ introv₃ :
  ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T] (h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)),
    Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
⊢ ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
    [inst_4 : Algebra R T],
    Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T) →
      Function.Surjective (α := S) (β := S ⊗[R] T) (⇑(algebraMap S (S ⊗[R] T)) : (a : S) → S ⊗[R] T)
have introv₄ : ∀ ⦃R S T : Type u_1⦄ [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] (h : Function.Surjective (α := R) (β := T) (⇑(algebraMap R T) : (a : R) → T)) (x : S ⊗[R] T),
  ∃ (a : S), (algebraMap S (S ⊗[R] T) : (a : S) → S ⊗[R] T) a = x
Tactic: classical
  introv h x
  induction x with
  | zero => exact ⟨0, map_zero _⟩
  | tmul x y =>
    obtain ⟨y, rfl⟩ := h y; use y • x; dsimp
    rw [TensorProduct.smul_tmul, Algebra.algebraMap_eq_smul_one]
  | add x y ex ey => obtain ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩ := ex, ey; exact ⟨x + y, map_add _ x y⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
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
⊢ Membership.mem (γ := Set S) (Set.range (ι := R) (⇑f : (a : R) → S)) x
have H₁ : ∀ (r : (↑s : Type u_1)),
  ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
Tactic: apply Submodule.mem_of_span_eq_top_of_smul_pow_mem
    (LinearMap.range (Algebra.linearMap R S)) s e
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
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)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
have H₁ : ∀ (a : Localization.Away (↑r : R))
  (e' :
    Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
      ((Localization.awayMap f (↑r : R) :
            (a : Localization.Away (↑r : R)) → Localization.Away ((f : (a : R) → S) (↑r : R)))
          a :
        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)))
          x :
        Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
  ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
Tactic: obtain ⟨a, e'⟩ := H r (algebraMap _ _ x)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
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)
a : Localization.Away (↑r : R)
e' :
  Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
    ((Localization.awayMap f (↑r : R) :
          (a : Localization.Away (↑r : R)) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        a :
      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)))
        x :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
have H₁ : ∀ (b : R) (n : ℕ)
  (e' :
    Eq (α := Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
      ((Localization.awayMap f (↑r : R) :
            (a : Localization.Away (↑r : R)) → Localization.Away ((f : (a : R) → S) (↑r : R)))
          (IsLocalization.mk' (Localization.Away (↑r : R)) b
            (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
              ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) sorry)) :
        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)))
          x :
        Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))),
  ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
Tactic: obtain ⟨b, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.exists_mk'_eq (Submonoid.powers (r : R)) a
Cleared hypotheses: a, e'
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (hypothesis)
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))
    ((Localization.awayMap f (↑r : R) :
          (a : Localization.Away (↑r : R)) → Localization.Away ((f : (a : R) → S) (↑r : R)))
        (IsLocalization.mk' (Localization.Away (↑r : R)) b
          (Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Submonoid R) (Submonoid.powers (↑r : R)) x)
            ((fun (x : ℕ) ↦ (↑r : R) ^ x) n) ⋯)) :
      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)))
        x :
      Localization.Away (M := S) ((f : (a : R) → S) (↑r : R) : S))
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
have 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) sorry) :
                    R))
                sorry) :
            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))
Tactic: rw [Localization.awayMap, IsLocalization.Away.map, IsLocalization.map_mk', eq_comm,
    IsLocalization.eq_mk'_iff_mul_eq, Subtype.coe_mk, Subtype.coe_mk, ← map_mul] at e'
Cleared hypotheses: e'
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (goal)
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 : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
have H₁ : ∀ (n' : ℕ)
  (e'' :
    (↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((f : (a : R) → S) (↑r : R) : S) x) n') sorry) :
          S) *
        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) sorry) :
                      R))
                  sorry) :
              S) :
            S) =
      HMul.hMul (β := S)
        (↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.powers ((f : (a : R) → S) (↑r : R)) : Submonoid S) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := S) ((f : (a : R) → S) (↑r : R) : S) x) n') sorry) :
          S)
        ((f : (a : R) → S) b : S)),
  ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
Tactic: obtain ⟨⟨_, n', rfl⟩, e''⟩ := (IsLocalization.eq_iff_exists (Submonoid.powers (f r)) _).mp e'
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Surjective (hypothesis)
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)
⊢ ∃ (n : ℕ), Membership.mem (γ := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) ((↑r : R) ^ n • x)
have e''₁ : 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''
Cleared hypotheses: e''
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ FormallyUnramified (algebraMap R S) ↔ Algebra.FormallyUnramified R S
have rw : Algebra.FormallyUnramified R S ↔ Algebra.FormallyUnramified R S
Tactic: rw [FormallyUnramified, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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
⊢ FormallyUnramified (algebraMap R S) ↔ Algebra.FormallyUnramified R S
have rw₁ : Algebra.FormallyUnramified R S ↔ Algebra.FormallyUnramified R S
Tactic: rw [FormallyUnramified, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (hypothesis)
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
⊢ g.FormallyUnramified
have algebraizeInst : Algebra.FormallyUnramified R T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (hypothesis)
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
⊢ (g.comp f).FormallyUnramified
have algebraizeInst : Algebra.FormallyUnramified R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (hypothesis)
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
⊢ (g.comp f).FormallyUnramified
have algebraizeInst₁ : Algebra.FormallyUnramified S T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
⊢ RespectsIso.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
have refine : ∀ {R S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S), e.toRingHom.FormallyUnramified
Tactic: refine stableUnderComposition.respectsIso ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
Goal:
⊢ IsStableUnderBaseChange.{u_3} fun {R S : Type u_3} [CommRing R] [CommRing S] ↦ FormallyUnramified
have 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))
Tactic: refine .mk respectsIso ?_
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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)
⊢ FormallyUnramified (S := TensorProduct R S T) (algebraMap S (TensorProduct R S T))
have rw : ∀ (H : Algebra.FormallyUnramified R T), Algebra.FormallyUnramified S (TensorProduct R S T)
Tactic: rw [formallyUnramified_algebraMap] at H ⊢
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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
⊢ FormallyUnramified (algebraMap R S)
have rw : Algebra.FormallyUnramified R S
Tactic: rw [formallyUnramified_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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
⊢ f.FormallyUnramified
have rw : ∀ (q : PrimeSpectrum S), Algebra.IsUnramifiedAt R q.asIdeal
Tactic: rw [FormallyUnramified, Algebra.formallyUnramified_iff_forall]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (hypothesis)
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 ⋯)
⊢ Algebra.IsUnramifiedAt R x.asIdeal
have this₁ : IsScalarTower R Rₓ Sₓ
Tactic: have : IsScalarTower R Rₓ Sₓ := .of_algebraMap_eq
    fun x ↦ (Localization.localRingHom_to_map _ _ _ rfl x).symm
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (hypothesis)
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.IsUnramifiedAt R x.asIdeal
have this₁ : Algebra.FormallyUnramified Rₓ Sₓ
Tactic: have : Algebra.FormallyUnramified Rₓ Sₓ := H _ _
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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
⊢ f.FormallyUnramified
have rw : ∀ (q : PrimeSpectrum S), Algebra.IsUnramifiedAt R q.asIdeal
Tactic: rw [FormallyUnramified, Algebra.formallyUnramified_iff_forall]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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
⊢ Algebra.IsUnramifiedAt R x.asIdeal
have obtain : ∀ (r : S) (hr : r ∈ s)
  (hrx : Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen r) x),
  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)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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
have refine : Algebra.FormallyUnramified R (Localization.Away r)
Tactic: refine Algebra.basicOpen_subset_unramifiedLocus_iff.mpr ?_ hrx
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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.FormallyUnramified R (Localization.Away r)
have 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)
Tactic: convert! H ⟨r, hr⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Unramified (goal)
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.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)
have a : Algebra.FormallyUnramified R (Localization.Away r) ↔
  FormallyUnramified (S := Localization.Away r) (RingHom.comp (algebraMap S (Localization.Away r)) f)
Tactic: dsimp