awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.RingHom.Locally
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') ⊤) ⊤
refine_1₃ refine_1₄ : Eq.{u + 1} (α := Ideal S') ⊤ ⊤
⊢ Eq.{u + 1} (α := Ideal S')
    (Ideal.span (Set.range fun (a : (↑s : Type u)) ↦ (algebraMap S S' : (a : S) → S') (↑a : S))) ⊤

Tactic:
rw [← Set.image_eq_range, ← Ideal.map_span, hsone, Ideal.map_top]

Premises used: Ideal.map_span, Set.image_eq_range, Ideal.map_top
-- Module: Mathlib.RingTheory.RingHom.Locally
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 (Algebra.algebraMapSubmonoid S' (Submonoid.powers (↑a : S))) (Sₐ a)

Tactic:
IsLocalization.commutes (T := Sₐ a) (M₁ := M.map f) (S₁ := S') (S₂ := Localization.Away a.val)
      (M₂ := Submonoid.powers a.val)

Premises used: IsLocalization.commutes, Localization.Away, Submonoid.map, Submonoid.powers, Subtype.val
-- Module: Mathlib.RingTheory.RingHom.Locally
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)
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)))
⊢ IsLocalization.Away.{u, u} (R := S') ((fun (a : (↑s : Type u)) ↦ ((algebraMap S S' : (a : S) → S') (↑a : S) : S')) a)
    (Sₐ a)

Tactic:
convert!
    IsLocalization.commutes (T := Sₐ a) (M₁ := M.map f) (S₁ := S') (S₂ := Localization.Away a.val)
      (M₂ := Submonoid.powers a.val)

Premises used: IsLocalization.commutes, Localization.Away, Submonoid.map, Submonoid.powers, Subtype.val
-- Module: Mathlib.RingTheory.RingHom.Locally
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)
⊢ 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:
simp [Algebra.algebraMapSubmonoid]

Premises used: Algebra.algebraMapSubmonoid
-- Module: Mathlib.RingTheory.RingHom.Locally
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)
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) ⋯)
⊢ P (R := R') (S := Sₐ a)
    (@comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap S' (Sₐ a)) (IsLocalization.map S' f ⋯))

Tactic:
rw [algebraMap_toAlgebra, IsLocalization.map_comp_map]

Premises used: IsLocalization.map_comp_map, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.RingHom.Locally
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)
refine_3 : P (S := Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f)
⊢ 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) ⋯)

Tactic:
apply hPl
-- Module: Mathlib.RingTheory.RingHom.Locally
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 (S := Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f)

Tactic:
hs a.val a.property

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.RingHom.Locally
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 (S := Localization.Away (↑a : S)) (comp (algebraMap S (Localization.Away (↑a : S))) f)

Tactic:
exact hs a.val a.property

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
⊢ Algebra.IsStandardSmooth R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
algInst : Algebra R S := f.toAlgebra
algebraizeInst : Algebra.IsStandardSmooth R S
⊢ Algebra.Smooth R S

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
hf : f.Smooth
⊢ Algebra.Smooth R S

Tactic:
algebraize [f]
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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
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
⊢ 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

Premises used: Algebra.Smooth.exists_span_eq_top_isStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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

Tactic:
⟨s, hs, fun t ht ↦ ?_⟩

Premises used: RingHom.Locally, Exists.intro
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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)
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)
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f

Tactic:
refine ⟨s, hs, fun t ht ↦ ?_⟩
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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
rw : Algebra.IsStandardSmooth R (Localization.Away t)
⊢ IsStandardSmooth (S := Localization.Away t) (RingHom.comp (algebraMap S (Localization.Away t)) f)

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

Premises used: IsScalarTower.algebraMap_eq, RingHom.isStandardSmooth_algebraMap, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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
⊢ Algebra.IsStandardSmooth R (Localization.Away t)

Tactic:
h t ht
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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
⊢ Algebra.IsStandardSmooth R (Localization.Away t)

Tactic:
exact h t ht
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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

Tactic:
⟨fun hf ↦ hf.locally_isStandardSmooth, fun hf ↦ ?_⟩

Premises used: Iff.intro, RingHom.Smooth.locally_isStandardSmooth
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
Goal:
R S : Type u
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
refine : ∀ (hf : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f), f.Smooth
⊢ f.Smooth ↔ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f

Tactic:
refine ⟨fun hf ↦ hf.locally_isStandardSmooth, fun hf ↦ ?_⟩
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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
rw : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Smooth) f
⊢ f.Smooth

Tactic:
rw [← locally_iff_of_localizationSpanTarget Smooth.propertyIsLocal.respectsIso
    Smooth.ofLocalizationSpanTarget]

Premises used: RingHom.locally_iff_of_localizationSpanTarget, RingHom.Smooth.propertyIsLocal, RingHom.Smooth.ofLocalizationSpanTarget, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth
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
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ Smooth) f

Tactic:
locally_of_locally (fun hf ↦ hf.smooth) hf

Premises used: RingHom.locally_of_locally