awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
ι : Type u_3
f : ι → S
h_1 : Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
T : ι → Type u_4
inst_3 : (i : ι) → CommSemiring (T i)
inst_4 : (i : ι) → Algebra.{u_1, u_4} R (T i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} S (T i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_4} R S (T i)
inst_7 : ∀ (i : ι), IsLocalization.Away.{u_2, u_4} (f i) (T i)
inst_8 : ∀ (i : ι), IsLocalIso.{u_1, u_4} R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq : PrimeSpectrum S }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion.{u_1, u_4} R (Localization.Away g')
n : ℕ
g : S
hg :
  g' * HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n =
    (algebraMap S (T i) : (a : S) → T i) g
⊢ g ∉ q
have hq'₁ : Ideal.comap (F := RingHom.{u_2, u_4} S (T i)) (algebraMap S (T i)) q'.asIdeal = q
Tactic: simp only [PrimeSpectrum.ext_iff, PrimeSpectrum.comap_asIdeal] at hq'
Cleared hypotheses: hq'
-- 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
ι : Type u_3
f : ι → S
h_1 : Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
T : ι → Type u_4
inst_3 : (i : ι) → CommSemiring (T i)
inst_4 : (i : ι) → Algebra.{u_1, u_4} R (T i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} S (T i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_4} R S (T i)
inst_7 : ∀ (i : ι), IsLocalization.Away.{u_2, u_4} (f i) (T i)
inst_8 : ∀ (i : ι), IsLocalIso.{u_1, u_4} R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion.{u_1, u_4} R (Localization.Away g')
n : ℕ
g : S
hg :
  g' * HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n =
    (algebraMap S (T i) : (a : S) → T i) g
hq' : Ideal.comap (F := RingHom.{u_2, u_4} S (T i)) (algebraMap S (T i)) q'.asIdeal = q
⊢ g ∉ q
have refine_1 : IsUnit (HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n)
Tactic: rwa [← hq', Ideal.mem_comap, ← hg, Ideal.mul_unit_mem_iff_mem]
-- 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
ι : Type u_3
f : ι → S
h_1 : Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
T : ι → Type u_4
inst_3 : (i : ι) → CommSemiring (T i)
inst_4 : (i : ι) → Algebra.{u_1, u_4} R (T i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} S (T i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_4} R S (T i)
inst_7 : ∀ (i : ι), IsLocalization.Away.{u_2, u_4} (f i) (T i)
inst_8 : ∀ (i : ι), IsLocalIso.{u_1, u_4} R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq : PrimeSpectrum S }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion.{u_1, u_4} R (Localization.Away g')
n : ℕ
g : S
hg :
  g' * HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n =
    (algebraMap S (T i) : (a : S) → T i) g
⊢ IsLocalization.Away g' (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))
have rw : IsLocalization.Away g'
  (Localization.Away (g' * HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n))
Tactic: rw [← hg]
-- 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
ι : Type u_3
f : ι → S
h_1 : Eq (α := Ideal S) (Ideal.span (Set.range f)) ⊤
T : ι → Type u_4
inst_3 : (i : ι) → CommSemiring (T i)
inst_4 : (i : ι) → Algebra.{u_1, u_4} R (T i)
inst_5 : (i : ι) → Algebra.{u_2, u_4} S (T i)
inst_6 : ∀ (i : ι), IsScalarTower.{u_1, u_2, u_4} R S (T i)
inst_7 : ∀ (i : ι), IsLocalization.Away.{u_2, u_4} (f i) (T i)
inst_8 : ∀ (i : ι), IsLocalIso.{u_1, u_4} R (T i)
q : Ideal S
hq : q.IsPrime
i : ι
hi : f i ∉ q
q' : PrimeSpectrum (T i)
hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq : PrimeSpectrum S }
g' : T i
hg' : g' ∉ q'.asIdeal
h : IsStandardOpenImmersion.{u_1, u_4} R (Localization.Away g')
n : ℕ
g : S
hg :
  g' * HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n =
    (algebraMap S (T i) : (a : S) → T i) g
⊢ IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (g * f i))
have this : IsLocalization.Away g' (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))
Tactic: have : IsLocalization.Away g' (Localization.Away (algebraMap S (T i) g)) := by
      rw [← hg]
      exact .of_associated
        (associated_mul_unit_right _ _ ((IsLocalization.Away.algebraMap_isUnit (f i)).pow n)).symm
-- 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
s : Set S
h_1 : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ x ∈ s, IsLocalIso.{u_1, u_2} R (Localization.Away x)
⊢ IsLocalIso R S
have heq : Eq.{u_2 + 1} (α := Ideal S) (Ideal.span (Set.range fun (i : (↑s : Type u_2)) ↦ (↑i : S))) ⊤
Tactic: have heq : Ideal.span (Set.range fun i : s ↦ i.1) = ⊤ := by simpa
-- 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
s : Set S
h_1 : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ x ∈ s, IsLocalIso.{u_1, u_2} R (Localization.Away x)
heq : Eq.{u_2 + 1} (α := Ideal S) (Ideal.span (Set.range fun (i : (↑s : Type u_2)) ↦ (↑i : S))) ⊤
⊢ IsLocalIso R S
have this : ∀ (i : (↑s : Type u_2)), IsLocalIso.{u_1, u_2} R (Localization.Away (↑i : S))
Tactic: have (i : s) : IsLocalIso R (Localization.Away i.1) := h _ i.property
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (goal)
Goal:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → CommRing (S i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (S i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), IsLocalIso.{u_4, u_5} R (S i)
this : (i : ι) → Algebra ((i : ι) → S i) (S i) :=
  fun (i : ι) ↦ RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i))
i : ι
⊢ IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)
have he : IsIdempotentElem (M := (j : ι) → S j) (Pi.single (M := S) i 1)
Tactic: apply IsLocalization.away_of_isIdempotentElem
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (goal)
Goal:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → CommRing (S i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (S i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), IsLocalIso.{u_4, u_5} R (S i)
this : (i : ι) → Algebra ((i : ι) → S i) (S i) :=
  fun (i : ι) ↦ RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i))
i : ι
he : IsIdempotentElem (M := (j : ι) → S j) (Pi.single (M := S) i 1)
⊢ IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)
have H : Eq (α := Ideal ((j : ι) → S j)) (RingHom.ker (F := ((j : ι) → S j) →+* S i) (algebraMap ((j : ι) → S j) (S i)))
  (Ideal.span {HSub.hSub (α := (j : ι) → S j) 1 (Pi.single (M := S) i 1)})
Tactic: apply IsLocalization.away_of_isIdempotentElem
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (goal)
Goal:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → CommRing (S i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (S i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), IsLocalIso.{u_4, u_5} R (S i)
this : (i : ι) → Algebra ((i : ι) → S i) (S i) :=
  fun (i : ι) ↦ RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i))
i : ι
he : IsIdempotentElem (M := (j : ι) → S j) (Pi.single (M := S) i 1)
H :
  Eq (α := Ideal ((j : ι) → S j)) (RingHom.ker (F := ((j : ι) → S j) →+* S i) (algebraMap ((j : ι) → S j) (S i)))
    (Ideal.span {HSub.hSub (α := (j : ι) → S j) 1 (Pi.single (M := S) i 1)})
⊢ IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)
have H' : Function.Surjective (α := (j : ι) → S j) (β := S i) (⇑(algebraMap ((j : ι) → S j) (S i)) : (a : (j : ι) → S j) → S i)
Tactic: apply IsLocalization.away_of_isIdempotentElem
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (hypothesis)
Goal:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → CommRing (S i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (S i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), IsLocalIso.{u_4, u_5} R (S i)
this : (i : ι) → Algebra ((i : ι) → S i) (S i) :=
  fun (i : ι) ↦ RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i))
⊢ IsLocalIso R ((i : ι) → S i)
have this₁ : ∀ (i : ι), IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)
Tactic: have (i : ι) : IsLocalization.Away (Pi.single i (1 : S i)) (S i) := by
    apply IsLocalization.away_of_isIdempotentElem
    · simp [IsIdempotentElem, ← Pi.single_mul_left]
    · apply RingHom.ker_evalRingHom
    · apply (Pi.evalRingHom S i).surjective
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (goal)
Goal:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → CommRing (S i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (S i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), IsLocalIso.{u_4, u_5} R (S i)
this_1 : (i : ι) → Algebra ((i : ι) → S i) (S i) :=
  fun (i : ι) ↦ RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i))
this : ∀ (i : ι), IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)
⊢ IsLocalIso R ((i : ι) → S i)
have apply : Eq (α := Ideal ((j : ι) → S j)) (Ideal.span (Set.range fun (i : ι) ↦ Pi.single (M := S) i 1)) ⊤
Tactic: apply of_span_range_eq_top (fun i ↦ Pi.single i (1 : S i)) _ fun i ↦ S i
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (goal)
Goal:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → CommRing (S i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (S i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), IsLocalIso.{u_4, u_5} R (S i)
let let₁ let₂ : IsLocalIso R ((i : ι) → S i)
⊢ IsLocalIso R ((i : ι) → S i)
have let₃ : let this : (i : ι) → Algebra ((i : ι) → S i) (S i) := fun (i : ι) ↦
  RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i));
∀ (this : ∀ (i : ι), IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)),
  IsLocalIso R ((i : ι) → S i)
Tactic: classical
  let (i : ι) : Algebra (∀ i, S i) (S i) := (Pi.evalAlgHom R S i).toAlgebra
  have (i : ι) : IsLocalization.Away (Pi.single i (1 : S i)) (S i) := by
    apply IsLocalization.away_of_isIdempotentElem
    · simp [IsIdempotentElem, ← Pi.single_mul_left]
    · apply RingHom.ker_evalRingHom
    · apply (Pi.evalRingHom S i).surjective
  apply of_span_range_eq_top (fun i ↦ Pi.single i (1 : S i)) _ fun i ↦ S i
  exact Ideal.span_single_eq_top _
-- Lean 4 proof step from Mathlib.RingTheory.LocalIso (goal)
Goal:
ι : Type u_3
R : Type u_4
S : ι → Type u_5
inst : CommSemiring R
inst_1 : (i : ι) → CommRing (S i)
inst_2 : (i : ι) → Algebra.{u_4, u_5} R (S i)
inst_3 : Finite ι
inst_4 : ∀ (i : ι), IsLocalIso.{u_4, u_5} R (S i)
let let₁ let₂ : IsLocalIso R ((i : ι) → S i)
let₃ :
  let this : (i : ι) → Algebra ((i : ι) → S i) (S i) := fun (i : ι) ↦
    RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i));
  ∀ (this : ∀ (i : ι), IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)),
    IsLocalIso R ((i : ι) → S i)
⊢ IsLocalIso R ((i : ι) → S i)
have let₄ : let this : (i : ι) → Algebra ((i : ι) → S i) (S i) := fun (i : ι) ↦
  RingHom.toAlgebra (AlgHom.toRingHom (Pi.evalAlgHom R S i));
∀ (this : ∀ (i : ι), IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)),
  Eq (α := Ideal ((j : ι) → S j)) (Ideal.span (Set.range fun (i : ι) ↦ Pi.single (M := S) i 1)) ⊤
Tactic: classical
  let (i : ι) : Algebra (∀ i, S i) (S i) := (Pi.evalAlgHom R S i).toAlgebra
  have (i : ι) : IsLocalization.Away (Pi.single i (1 : S i)) (S i) := by
    apply IsLocalization.away_of_isIdempotentElem
    · simp [IsIdempotentElem, ← Pi.single_mul_left]
    · apply RingHom.ker_evalRingHom
    · apply (Pi.evalRingHom S i).surjective
  apply of_span_range_eq_top (fun i ↦ Pi.single i (1 : S i)) _ fun i ↦ S i
  exact Ideal.span_single_eq_top _
-- 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 : (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)
⊢ IsLocalIso R T
have 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))
Tactic: have (i : ι) : IsStandardOpenImmersion (Localization.Away i.1.1) (T'' i.1 i.2) := i.2.2
-- 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 :
  ∀ (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)))
    ⊤
⊢ IsLocalIso R T
have 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))
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) _
-- 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))
⊢ IsLocalIso R T
have 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)))
  ⊤
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
-- 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 :
  ∀ (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.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 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) ⊤)
Tactic: have h1 := congr(Ideal.map (algebraMap S T) $(span_isStandardOpenImmersion_eq_top R S))
-- 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 :
  ∀ (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.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 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)}))
  ⊤
Tactic: rw [Ideal.map_top, Ideal.map_span] at h1
Cleared hypotheses: h1