awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (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_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)}))
    ⊤
⊢ Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.span
      (Set.range fun (i : ι) ↦
        HMul.hMul (α := T)
          ((algebraMap S T : (a : S) → T) (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S) :
            T)
          (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T)))
    ⊤
have nth_rw : ∀ (x : T),
  Membership.mem (γ := Set T)
      (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
        {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)})
      x →
    ∀ (y : T),
      Membership.mem (γ := Set T) {g : T | IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away g)} y →
        x * y ∈
          (↑(Ideal.span
                (Set.range fun (i : ι) ↦
                  HMul.hMul (α := T)
                    ((algebraMap S T : (a : S) → T)
                        (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S) :
                      T)
                    (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))) :
            Set T)
Tactic: nth_rw 1 [_root_.eq_top_iff, ← Ideal.top_mul ⊤, ← h1, ← span_isStandardOpenImmersion_eq_top S T,
    Ideal.span_mul_span, Ideal.span_le, Set.mul_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (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_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)}))
    ⊤
⊢ ∀ (x : T),
    Membership.mem (γ := Set T)
        (Set.image.{u_2, u_3} (α := S) (⇑(algebraMap S T) : (a : S) → T)
          {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)})
        x →
      ∀ (y : T),
        Membership.mem (γ := Set T) {g : T | IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away g)} y →
          x * y ∈
            (↑(Ideal.span
                  (Set.range fun (i : ι) ↦
                    HMul.hMul (α := T)
                      ((algebraMap S T : (a : S) → T)
                          (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S) :
                        T)
                      (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T))) :
              Set T)
have simp : ∀ (a : S),
  IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away a) →
    ∀ (y : T),
      IsStandardOpenImmersion.{u_2, u_3} S (Localization.Away y) →
        Membership.mem (γ := Ideal T)
          (Ideal.span
            (Set.range fun (i : ι) ↦
              HMul.hMul (α := T)
                ((algebraMap S T : (a : S) → T)
                    (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S) :
                  T)
                (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T)))
          (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) a : T) y)
Tactic: simp only [Set.mem_image, Set.mem_setOf_eq, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (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_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)
⊢ Membership.mem (γ := Ideal T)
    (Ideal.span
      (Set.range fun (i : ι) ↦
        HMul.hMul (α := T)
          ((algebraMap S T : (a : S) → T) (↑(i.fst (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : S) :
            T)
          (↑(i.snd (β := fun (i : (↑s : Type u_2)) ↦ (↑(t (↑i : S)) : Type u_3))) : T)))
    (HMul.hMul (α := T) ((algebraMap S T : (a : S) → T) g : T) x)
have refine : x ∈ t (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) g hg) : S)
Tactic: refine Ideal.subset_span ⟨⟨⟨g, hg⟩, ⟨x, ?_⟩⟩, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (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_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)
⊢ x ∈ t (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) g hg) : S)
have simp : IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)
Tactic: simp only [Set.mem_setOf_eq, t]
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (hypothesis)
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)
⊢ IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)
have this₁ : 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 _ _
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (hypothesis)
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)
have 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))
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)]
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (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_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 (Localization.Away x) (Submonoid.powers g))
    (T'' g x)
have 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)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (hypothesis)
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)
⊢ IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)
have this₁ : 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))
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (hypothesis)
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)
⊢ IsStandardOpenImmersion.{u_2, u_3} (Localization.Away g) (T'' g x)
have this₁ : 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) _ _ _
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (hypothesis)
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 R T
e : S ≃ₐ[R] T
inst_5 : IsLocalIso R S
algInst : Algebra S T := (↑e : S →ₐ[R] T).toAlgebra
⊢ IsLocalIso R T
have this : IsStandardOpenImmersion S T
Tactic: have : IsStandardOpenImmersion S T := .of_bijective e.bijective
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (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_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalIso R S
⊢ IsLocalIso T (T ⊗[R] S)
have rw : {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} ⊆
  (↑(Ideal.comap (F := S →ₐ[R] T ⊗[R] S) TensorProduct.includeRight
        (Ideal.span {g : T ⊗[R] S | IsStandardOpenImmersion T (Localization.Away g)})) :
    Set S)
Tactic: rw [iff_span_isStandardOpenImmersion_eq_top, _root_.eq_top_iff,
    ← Ideal.map_top Algebra.TensorProduct.includeRight, ← span_isStandardOpenImmersion_eq_top R S,
    Ideal.map_le_iff_le_comap, Ideal.span_le]
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (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_3
inst_3 : CommSemiring T
inst_4 : Algebra R T
inst_5 : IsLocalIso R S
g : S
hg : Membership.mem (γ := Set S) {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} g
⊢ g ∈
    (↑(Ideal.comap (F := S →ₐ[R] T ⊗[R] S) TensorProduct.includeRight
          (Ideal.span {g : T ⊗[R] S | IsStandardOpenImmersion T (Localization.Away g)})) :
      Set S)
have a : Membership.mem (α := T ⊗[R] S) (γ := Set (T ⊗[R] S)) {g : T ⊗[R] S | IsStandardOpenImmersion T (Localization.Away g)}
  ((TensorProduct.includeRight : (a : S) → T ⊗[R] S) g : T ⊗[R] S)
Tactic: apply Ideal.subset_span