awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
have refine_1 : Eq (α := Ideal S') (Ideal.span ((⇑(algebraMap S S') : (a : S) → S') '' s)) ⊤
Tactic: rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
refine_1 : Eq (α := Ideal S') (Ideal.span ((⇑(algebraMap S S') : (a : S) → S') '' s)) ⊤
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
have refine_1₁ : Eq (α := Ideal S') (Ideal.map (F := S →+* S') (algebraMap S S') (Ideal.span s)) ⊤
Tactic: rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
refine_1 : Eq (α := Ideal S') (Ideal.span ((⇑(algebraMap S S') : (a : S) → S') '' s)) ⊤
refine_1₁ : Eq (α := Ideal S') (Ideal.map (F := S →+* S') (algebraMap S S') (Ideal.span s)) ⊤
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
have refine_1₂ : Eq (α := Ideal S') (Ideal.map (R := S) (F := S →+* S') (algebraMap S S') ⊤) ⊤
Tactic: rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
refine_1 : Eq (α := Ideal S') (Ideal.span ((⇑(algebraMap S S') : (a : S) → S') '' s)) ⊤
refine_1₁ : Eq (α := Ideal S') (Ideal.map (F := S →+* S') (algebraMap S S') (Ideal.span s)) ⊤
refine_1₂ : Eq (α := Ideal S') (Ideal.map (R := S) (F := S →+* S') (algebraMap S S') ⊤) ⊤
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤
have refine_1₃ : Eq.{u + 1} (α := Ideal S') ⊤ ⊤
Tactic: rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
a : (↑s : Type u)
⊢ IsLocalization.Away.{u, u} (R := S') ((fun (a : (↑s : Type u)) ↦ ((algebraMap S S' : (a : S) → S') (↑a : S) : S')) a)
    (Sₐ a)
have h : Eq (α := Submonoid S')
  (Submonoid.powers ((fun (a : (↑s : Type u)) ↦ ((algebraMap S S' : (a : S) → S') (↑a : S) : S')) a))
  (Algebra.algebraMapSubmonoid S' (Submonoid.powers (↑a : S)))
Tactic: convert!
    IsLocalization.commutes (T := Sₐ a) (M₁ := M.map f) (S₁ := S') (S₂ := Localization.Away a.val)
      (M₂ := Submonoid.powers a.val)
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
a : (↑s : Type u)
⊢ P (R := R') (S := Sₐ a)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₐ a)) (IsLocalization.map S' f ⋯))
have refine_3 : P (R := R') (S := Sₐ a)
  (IsLocalization.map (M := M) (P := Localization.Away (↑a : S)) (T :=
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M))
    (Sₐ a) (comp (algebraMap S (Localization.Away (↑a : S))) f) sorry)
Tactic: rw [algebraMap_toAlgebra, IsLocalization.map_comp_map]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.Locally (goal)
Goal:
P : {R S : Type u} → [inst : CommRing R] → [inst_8 : CommRing S] → (R →+* S) → Prop
hPl : LocalizationPreserves.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ P
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
M : Submonoid R
R' S' : Type u
inst_2 : CommRing R'
inst_3 : CommRing S'
inst_4 : Algebra R R'
inst_5 : Algebra S S'
inst_6 : IsLocalization M R'
inst_7 : IsLocalization (Submonoid.map f M) S'
s : Set S
hsone : Eq (α := Ideal S) (Ideal.span s) ⊤
hs :
  ∀ t ∈ s,
    (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (P : (R →+* S) → Prop)) _ (Localization.Away t) _ _
      (comp (algebraMap S (Localization.Away t)) f)
Mₐ : (a : (↑s : Type u)) → Submonoid (Localization.Away (↑a : S)) :=
  fun (a : (↑s : Type u)) ↦
    Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
      (Submonoid.map f M)
Sₐ : (a : (↑s : Type u)) → Type u := fun (a : (↑s : Type u)) ↦ Localization (Mₐ a)
hM :
  ∀ (a : (↑s : Type u)),
    Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M = Mₐ a
this_1 :
  ∀ (a : (↑s : Type u)),
    IsLocalization
      (Submonoid.map (F := R →+* Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f) M)
      (Sₐ a)
this_2 :
  ∀ (a : (↑s : Type u)),
    IsLocalization (R := Localization.Away (↑a : S))
      (Algebra.algebraMapSubmonoid (Localization.Away (↑a : S)) (Submonoid.map f M)) (Sₐ a)
this_3 : (a : (↑s : Type u)) → Algebra S' (Sₐ a) :=
  fun (a : (↑s : Type u)) ↦
    toAlgebra
      (IsLocalization.map (M := Submonoid.map f M) (T :=
        Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
          (Submonoid.map f M))
        (Sₐ a) (algebraMap S (Localization.Away (↑a : S))) ⋯)
this : ∀ (a : (↑s : Type u)), IsScalarTower S S' (Sₐ a)
a : (↑s : Type u)
⊢ P (R := R') (S := Sₐ a)
    (IsLocalization.map (M := M) (P := Localization.Away (↑a : S)) (T :=
      Submonoid.map (F := S →+* Localization.Away (↑a : S)) (algebraMap S (Localization.Away (↑a : S)))
        (Submonoid.map f M))
      (Sₐ a) (comp (algebraMap S (Localization.Away (↑a : S))) f) ⋯)
have refine_3 : P (S := Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f)
Tactic: apply hPl
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.LocallyStandardSmooth (hypothesis)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
⊢ f.Smooth
have algebraizeInst : Algebra.IsStandardSmooth R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.LocallyStandardSmooth (hypothesis)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
have algebraizeInst : Algebra.Smooth R S
Tactic: algebraize [f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.LocallyStandardSmooth (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.Smooth R S
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
have obtain : ∀ (s : Set S) (hs : Eq (α := Ideal S) (Ideal.span s) ⊤) (h : ∀ x ∈ s, Algebra.IsStandardSmooth R (Localization.Away x)),
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
Tactic: obtain ⟨s, hs, h⟩ := Algebra.Smooth.exists_span_eq_top_isStandardSmooth R S
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.LocallyStandardSmooth (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.Smooth R S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ x ∈ s, Algebra.IsStandardSmooth R (Localization.Away x)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
have refine : ∀ (t : S) (ht : t ∈ s),
  (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (IsStandardSmooth : (f : R →+* S) → Prop)) _ (Localization.Away t) _
    _ (RingHom.comp (algebraMap S (Localization.Away t)) f)
Tactic: refine ⟨s, hs, fun t ht ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.LocallyStandardSmooth (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.Smooth R S
s : Set S
hs : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ x ∈ s, Algebra.IsStandardSmooth R (Localization.Away x)
t : S
ht : t ∈ s
⊢ IsStandardSmooth (S := Localization.Away t) (RingHom.comp (algebraMap S (Localization.Away t)) f)
have rw : Algebra.IsStandardSmooth R (Localization.Away t)
Tactic: rw [← f.algebraMap_toAlgebra, ← IsScalarTower.algebraMap_eq, isStandardSmooth_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.LocallyStandardSmooth (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
⊢ f.Smooth ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
have refine : ∀ (hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f), f.Smooth
Tactic: refine ⟨fun hf ↦ hf.locally_isStandardSmooth, fun hf ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.LocallyStandardSmooth (goal)
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f
⊢ f.Smooth
have rw : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Smooth) f
Tactic: rw [← locally_iff_of_localizationSpanTarget Smooth.propertyIsLocal.respectsIso
    Smooth.ofLocalizationSpanTarget]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ IsStandardOpenImmersion R S
have rw : ∃ (r : R), Away r S
Tactic: rw [Algebra.isStandardOpenImmersion_iff]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
h : Function.Bijective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
⊢ ∃ (r : R), Away r S
have h₁ : Away.{u_1, u_2} (R := R) 1 S
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
h : IsStandardOpenImmersion R S
⊢ IsStandardOpenImmersion R T
have rw : ∀ (h : ∃ (r : R), Away r S), ∃ (r : R), Away r T
Tactic: rw [Algebra.isStandardOpenImmersion_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
h : ∃ (r : R), Away r S
⊢ ∃ (r : R), Away r T
have obtain : ∀ (r : R) (hr : Away r S), ∃ (r : R), Away r T
Tactic: obtain ⟨r, hr⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_4
inst_3 : CommSemiring T
inst_4 : Algebra R T
e : S ≃ₐ[R] T
r : R
hr : Away r S
⊢ ∃ (r : R), Away r T
have h : Away r T
Tactic: use r
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
⊢ IsStandardOpenImmersion (algebraMap R S) ↔ Algebra.IsStandardOpenImmersion R S
have rw : Algebra.IsStandardOpenImmersion R S ↔ Algebra.IsStandardOpenImmersion R S
Tactic: rw [IsStandardOpenImmersion, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
rw : Algebra.IsStandardOpenImmersion R S ↔ Algebra.IsStandardOpenImmersion R S
⊢ IsStandardOpenImmersion (algebraMap R S) ↔ Algebra.IsStandardOpenImmersion R S
have rw₁ : Algebra.IsStandardOpenImmersion R S ↔ Algebra.IsStandardOpenImmersion R S
Tactic: rw [IsStandardOpenImmersion, toAlgebra_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsStandardOpenImmersion
hg : g.IsStandardOpenImmersion
⊢ (g.comp f).IsStandardOpenImmersion
have algebraizeInst : Algebra.IsStandardOpenImmersion R S
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (hypothesis)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsStandardOpenImmersion
hg : g.IsStandardOpenImmersion
algebraizeInst : Algebra.IsStandardOpenImmersion R S
⊢ (g.comp f).IsStandardOpenImmersion
have algebraizeInst₁ : Algebra.IsStandardOpenImmersion S T
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.RingHom.OpenImmersion (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
inst : CommRing R
inst_1 : CommRing S
inst_2 : CommRing T
f : R →+* S
g : S →+* T
hf : f.IsStandardOpenImmersion
hg : g.IsStandardOpenImmersion
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.IsStandardOpenImmersion R S
algebraizeInst_1 : Algebra.IsStandardOpenImmersion S T
⊢ (g.comp f).IsStandardOpenImmersion
have obtain : ∀ (r : R) (hr : IsLocalization.Away r S), (g.comp f).IsStandardOpenImmersion
Tactic: obtain ⟨r, hr⟩ := hf
Cleared hypotheses: hf