awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
simp : IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)
⊢ x ∈ t (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) g hg) : S)

Tactic:
simp only [Set.mem_setOf_eq, t]

Premises used: Set.mem_setOf_eq
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
⊢ IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)

Tactic:
have : IsScalarTower S (Localization.Away x) (T'' g x) :=
    IsScalarTower.to₁₃₄ _ T _ _
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
⊢ Eq.{u_3 + 1} (α := Submonoid (Localization.Away x)) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (algebraMapSubmonoid (R := T) (Localization.Away x)
      (Submonoid.powers ((algebraMap S T : (a : S) → T) g) : Submonoid T))

Tactic:
simp [IsScalarTower.algebraMap_apply S T (Localization.Away x)]

Premises used: Localization.Away, IsScalarTower.algebraMap_apply
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
⊢ Eq.{u_3 + 1} (α := Submonoid (Localization.Away x)) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (algebraMapSubmonoid (R := T) (Localization.Away x)
      (Submonoid.powers ((algebraMap S T : (a : S) → T) g) : Submonoid T))

Tactic:
have : algebraMapSubmonoid (Localization.Away x) (.powers g) =
      algebraMapSubmonoid (Localization.Away x) (.powers (algebraMap S T g)) := by
        simp [IsScalarTower.algebraMap_apply S T (Localization.Away x)]
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this_4 : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
this :
  Eq.{u_3 + 1} (α := Submonoid (Localization.Away x)) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (algebraMapSubmonoid (R := T) (Localization.Away x)
      (Submonoid.powers ((algebraMap S T : (a : S) → T) g) : Submonoid T))
rw :
  IsLocalization.{u_3, u_3} (R := Localization.Away x)
    (algebraMapSubmonoid (R := T) (Localization.Away x)
      (Submonoid.powers ((algebraMap S T : (a : S) → T) g) : Submonoid T))
    (T'' g x)
⊢ IsLocalization.{u_3, u_3} (R := Localization.Away x) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (T'' g x)

Tactic:
rw [this]
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this_4 : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
this :
  Eq.{u_3 + 1} (α := Submonoid (Localization.Away x)) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (algebraMapSubmonoid (R := T) (Localization.Away x)
      (Submonoid.powers ((algebraMap S T : (a : S) → T) g) : Submonoid T))
⊢ IsLocalization.{u_3, u_3} (R := Localization.Away x)
    (algebraMapSubmonoid (R := T) (Localization.Away x)
      (Submonoid.powers ((algebraMap S T : (a : S) → T) g) : Submonoid T))
    (T'' g x)

Tactic:
.commutes _ (T' g) _ (.powers x) (.powers (algebraMap S T g))

Premises used: Algebra.algebraMap, IsLocalization.commutes, Submonoid.powers, DFunLike.coe
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this_4 : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
this :
  Eq.{u_3 + 1} (α := Submonoid (Localization.Away x)) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (algebraMapSubmonoid (R := T) (Localization.Away x)
      (Submonoid.powers ((algebraMap S T : (a : S) → T) g) : Submonoid T))
⊢ IsLocalization.{u_3, u_3} (R := Localization.Away x)
    (algebraMapSubmonoid (R := T) (Localization.Away x)
      (Submonoid.powers ((algebraMap S T : (a : S) → T) g) : Submonoid T))
    (T'' g x)

Tactic:
exact .commutes _ (T' g) _ (.powers x) (.powers (algebraMap S T g))
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
⊢ IsLocalization.{u_3, u_3} (R := Localization.Away x) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (T'' g x)

Tactic:
have : IsLocalization (algebraMapSubmonoid (Localization.Away x) (.powers g)) (T'' g x) := by
    have : algebraMapSubmonoid (Localization.Away x) (.powers g) =
      algebraMapSubmonoid (Localization.Away x) (.powers (algebraMap S T g)) := by
        simp [IsScalarTower.algebraMap_apply S T (Localization.Away x)]
    rw [this]
    exact .commutes _ (T' g) _ (.powers x) (.powers (algebraMap S T g))
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this_4 : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
this :
  IsLocalization.{u_3, u_3} (R := Localization.Away x) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (T'' g x)
⊢ IsPushout.{u_3, u_2, u_2, u_3} S (Localization.Away x) (Localization.Away g) (T'' g x)

Tactic:
have : IsPushout S (Localization.Away x) (Localization.Away g) (T'' g x) :=
    Algebra.isPushout_of_isLocalization (.powers g) _ _ _
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this_4 : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
this_5 :
  IsLocalization.{u_3, u_3} (R := Localization.Away x) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (T'' g x)
this : IsPushout.{u_3, u_2, u_2, u_3} S (Localization.Away x) (Localization.Away g) (T'' g x)
⊢ IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)

Tactic:
.of_isPushout S (Localization.Away x) _ _

Premises used: Localization.Away, Algebra.IsStandardOpenImmersion.of_isPushout
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
T : Type u_3
inst_3 : CommSemiring T
inst_4 : Algebra S T
inst_5 : Algebra R T
inst_6 : IsScalarTower R S T
inst_7 : IsLocalIso R S
inst_8 : IsLocalIso S T
s : Set S := {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}
T' : (g : S) → Type u_3 := fun (g : S) ↦ Localization.Away (M := T) ((algebraMap S T : (a : S) → T) g : T)
this_1 : (g : S) → Algebra.{u_2, u_3} (Localization.Away g) (T' g) :=
  fun (g : S) ↦ localizationAlgebra (Submonoid.powers g) T
T'' : (g : S) → (x : T) → Type u_3 :=
  fun (g : S) (x : T) ↦ Localization.Away (M := T' g) ((algebraMap T (T' g) : (a : T) → T' g) x : T' g)
t : (g : S) → Set T := fun (g : S) ↦ {x : T | IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)}
ι : Type (max u_3 u_2) := (i : (↑s : Type u_2)) × (↑(t (↑i : S)) : Type u_3)
this_2 :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_2, u_3}
      (Localization.Away (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S))
      (T'' (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S)
        (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))
h1 :
  Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    ⊤
g : S
hg : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
x : T
hx : IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away x)
this_3 : Algebra (Localization.Away x) (T'' g x) := localizationAlgebra (Submonoid.powers x) (T' g)
this_4 : IsScalarTower.{u_2, u_3, u_3} S (Localization.Away x) (T'' g x)
this_5 :
  IsLocalization.{u_3, u_3} (R := Localization.Away x) (algebraMapSubmonoid (Localization.Away x) (Submonoid.powers g))
    (T'' g x)
this : IsPushout.{u_3, u_2, u_2, u_3} S (Localization.Away x) (Localization.Away g) (T'' g x)
⊢ IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)

Tactic:
exact .of_isPushout S (Localization.Away x) _ _