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 : (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)
⊢ ∀ (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))

Tactic:
have (i : ι) : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1 i.2) := i.2.2
-- 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))
h :
  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)))
    ⊤
⊢ ∀ (i : ι),
    IsStandardOpenImmersion.{u_1, u_3} R
      (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))

Tactic:
have (i : ι) : IsStandardOpenImmersion R (T'' i.1 i.2) :=
      have : IsScalarTower R (Localization.Away i.1.1) (T' i.1.1) :=
        IsScalarTower.to₁₃₄ _ S _ _
      have : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1.1 i.2.1) := i.2.2
      have : IsStandardOpenImmersion R (Localization.Away i.1.1) := i.1.2
      .trans _ (Localization.Away i.1.1) _
-- 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))
h :
  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)))
    ⊤
this :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_1, u_3} R
      (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))
⊢ IsLocalIso R T

Tactic:
.of_span_range_eq_top _ h fun i : ι ↦ T'' i.1 i.2

Premises used: Algebra.IsLocalIso.of_span_range_eq_top, Sigma.fst, Sigma.snd, Subtype.val
-- 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))
h :
  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)))
    ⊤
this :
  ∀ (i : ι),
    IsStandardOpenImmersion.{u_1, u_3} R
      (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))
⊢ IsLocalIso R T

Tactic:
exact .of_span_range_eq_top _ h fun i : ι ↦ T'' i.1 i.2
-- 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))
suffices :
  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)))
    ⊤
⊢ IsLocalIso R T

Tactic:
suffices h : Ideal.span (Set.range fun i : ι ↦ algebraMap S T i.1 * i.2) = ⊤ by
    have (i : ι) : IsStandardOpenImmersion R (T'' i.1 i.2) :=
      have : IsScalarTower R (Localization.Away i.1.1) (T' i.1.1) :=
        IsScalarTower.to₁₃₄ _ S _ _
      have : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1.1 i.2.1) := i.2.2
      have : IsStandardOpenImmersion R (Localization.Away i.1.1) := i.1.2
      .trans _ (Localization.Away i.1.1) _
    exact .of_span_range_eq_top _ h fun i : ι ↦ T'' i.1 i.2
-- 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))
⊢ Eq.{u_3 + 1} (α := Ideal T)
    (Ideal.map (R := S) (F := S →+* T) (algebraMap S T)
      (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    (Ideal.map (R := S) (F := S →+* T) (algebraMap S T) ⊤)

Tactic:
have h1 := congr(Ideal.map (algebraMap S T) $(span_isStandardOpenImmersion_eq_top R S))
-- 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.map (R := S) (F := S →+* T) (algebraMap S T)
      (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}))
    (Ideal.map (R := S) (F := S →+* T) (algebraMap S T) ⊤)
⊢ 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)}))
    ⊤

Tactic:
rw [Ideal.map_top, Ideal.map_span] at h1

Premises used: Ideal.map_span, Ideal.map_top
-- 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)}))
    ⊤
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)
⊢ 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)))
    ⊤

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]

Premises used: Ideal.span_le, eq_top_iff, Ideal.span_mul_span, Set.mul_subset_iff, Ideal.top_mul, Top.top, Algebra.IsLocalIso.span_isStandardOpenImmersion_eq_top
-- 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)}))
    ⊤
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)
⊢ ∀ (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:
simp only [Set.mem_image, Set.mem_setOf_eq, SetLike.mem_coe, forall_exists_index, and_imp,
    forall_apply_eq_imp_iff₂]

Premises used: and_imp, Set.mem_image, forall_exists_index, Set.mem_setOf_eq, SetLike.mem_coe, forall_apply_eq_imp_iff₂
-- 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)
⊢ 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)

Tactic:
Ideal.subset_span ⟨⟨⟨g, hg⟩, ⟨x, ?_⟩⟩, rfl⟩

Premises used: Ideal.subset_span, Subtype.mk, Exists.intro, Sigma.mk, rfl
-- 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)
refine : x ∈ t (↑(Subtype.mk (p := fun (x : S) ↦ x ∈ s) g hg) : S)
⊢ 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)

Tactic:
refine Ideal.subset_span ⟨⟨⟨g, hg⟩, ⟨x, ?_⟩⟩, rfl⟩