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
ι : 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
refine_1 : g ∉ q
⊢ g * f i ∉ q

Tactic:
refine Ideal.IsPrime.mul_notMem hq ?_ hi

Premises used: Ideal.IsPrime.mul_notMem
-- 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
ι : 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
⊢ 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'

Premises used: PrimeSpectrum.ext_iff, PrimeSpectrum.comap_asIdeal
-- 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
ι : 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
refine_1 : IsUnit (HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n)
⊢ g ∉ q

Tactic:
rwa [← hq', Ideal.mem_comap, ← hg, Ideal.mul_unit_mem_iff_mem]

Premises used: Ideal.mul_unit_mem_iff_mem, Ideal.mem_comap
-- 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
ι : 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
⊢ IsUnit (HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n)

Tactic:
(IsLocalization.Away.algebraMap_isUnit (f i)).pow n

Premises used: IsUnit.pow, IsLocalization.Away.algebraMap_isUnit
-- 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
ι : 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
⊢ IsUnit (HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n)

Tactic:
exact (IsLocalization.Away.algebraMap_isUnit (f i)).pow n

Premises used: IsUnit.pow, IsLocalization.Away.algebraMap_isUnit
-- 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
ι : 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
rw :
  IsLocalization.Away g'
    (Localization.Away (g' * HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n))
⊢ IsLocalization.Away g' (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))

Tactic:
rw [← hg]
-- 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
ι : 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 (g' * HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n))

Tactic:
.of_associated
        (associated_mul_unit_right _ _ ((IsLocalization.Away.algebraMap_isUnit (f i)).pow n)).symm

Premises used: IsUnit.pow, Associated.symm, associated_mul_unit_right, IsLocalization.Away.of_associated, IsLocalization.Away.algebraMap_isUnit
-- 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
ι : 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 (g' * HPow.hPow (α := T i) ((algebraMap S (T i) : (a : S) → T i) (f i) : T i) n))

Tactic:
exact .of_associated
        (associated_mul_unit_right _ _ ((IsLocalization.Away.algebraMap_isUnit (f i)).pow n)).symm
-- 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
ι : 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))

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
-- 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
ι : 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
this : IsLocalization.Away g' (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))
e₁ : AlgEquiv.{u_2, u_4, u_2} S (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))
  (Localization.Away (g * f i)) :=
  IsLocalization.algEquiv (Submonoid.powers (g * f i))
    (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i)) (Localization.Away (g * f i))
e₂ : AlgEquiv.{u_1, u_4, u_2} R (Localization.Away g') (Localization.Away (g * f i)) :=
  AlgEquiv.trans
    (AlgEquiv.restrictScalars R
      (IsLocalization.algEquiv (Submonoid.powers g') (Localization.Away g')
        (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))))
    (AlgEquiv.restrictScalars R e₁)
⊢ IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (g * f i))

Tactic:
.of_algEquiv e₂

Premises used: Algebra.IsStandardOpenImmersion.of_algEquiv
-- 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
ι : 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
this : IsLocalization.Away g' (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))
e₁ : AlgEquiv.{u_2, u_4, u_2} S (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))
  (Localization.Away (g * f i)) :=
  IsLocalization.algEquiv (Submonoid.powers (g * f i))
    (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i)) (Localization.Away (g * f i))
e₂ : AlgEquiv.{u_1, u_4, u_2} R (Localization.Away g') (Localization.Away (g * f i)) :=
  AlgEquiv.trans
    (AlgEquiv.restrictScalars R
      (IsLocalization.algEquiv (Submonoid.powers g') (Localization.Away g')
        (Localization.Away (M := T i) ((algebraMap S (T i) : (a : S) → T i) g : T i))))
    (AlgEquiv.restrictScalars R e₁)
⊢ IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (g * f i))

Tactic:
exact .of_algEquiv e₂
-- 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
s : Set S
h_1 : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ x ∈ s, IsLocalIso.{u_1, u_2} R (Localization.Away x)
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.span (Set.range fun (i : (↑s : Type u_2)) ↦ (↑i : S))) ⊤

Tactic:
simpa
-- 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
s : Set S
h_1 : Eq (α := Ideal S) (Ideal.span s) ⊤
h : ∀ x ∈ s, IsLocalIso.{u_1, u_2} R (Localization.Away x)
⊢ 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
-- 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
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))) ⊤
⊢ ∀ (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
-- 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
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))) ⊤
this : ∀ (i : (↑s : Type u_2)), IsLocalIso.{u_1, u_2} R (Localization.Away (↑i : S))
⊢ IsLocalIso R S

Tactic:
.of_span_range_eq_top _ heq fun i ↦ Localization.Away i.1

Premises used: Algebra.IsLocalIso.of_span_range_eq_top, Localization.Away, 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
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))) ⊤
this : ∀ (i : (↑s : Type u_2)), IsLocalIso.{u_1, u_2} R (Localization.Away (↑i : S))
⊢ IsLocalIso R S

Tactic:
exact .of_span_range_eq_top _ heq fun i ↦ Localization.Away i.1
-- Module: Mathlib.RingTheory.LocalIso
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)})
H' :
  Function.Surjective (α := (j : ι) → S j) (β := S i) (⇑(algebraMap ((j : ι) → S j) (S i)) : (a : (j : ι) → S j) → S i)
⊢ IsLocalization.Away (R := (j : ι) → S j) (Pi.single (M := S) i 1) (S i)

Tactic:
apply IsLocalization.away_of_isIdempotentElem

Premises used: IsLocalization.away_of_isIdempotentElem
-- Module: Mathlib.RingTheory.LocalIso
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 : ι
⊢ IsIdempotentElem (M := (j : ι) → S j) (Pi.single (M := S) i 1)

Tactic:
simp [IsIdempotentElem, ← Pi.single_mul_left]

Premises used: IsIdempotentElem, Pi.single_mul_left
-- Module: Mathlib.RingTheory.LocalIso
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 : ι
⊢ 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 RingHom.ker_evalRingHom

Premises used: RingHom.ker_evalRingHom
-- Module: Mathlib.RingTheory.LocalIso
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 : ι
⊢ Function.Surjective (α := (j : ι) → S j) (β := S i) (⇑(algebraMap ((j : ι) → S j) (S i)) : (a : (j : ι) → S j) → S i)

Tactic:
apply (Pi.evalRingHom S i).surjective

Premises used: Pi.evalRingHom, RingHom.surjective
-- Module: Mathlib.RingTheory.LocalIso
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)

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
-- Module: Mathlib.RingTheory.LocalIso
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)
apply : Eq (α := Ideal ((j : ι) → S j)) (Ideal.span (Set.range fun (i : ι) ↦ Pi.single (M := S) i 1)) ⊤
⊢ IsLocalIso R ((i : ι) → S i)

Tactic:
apply of_span_range_eq_top (fun i ↦ Pi.single i (1 : S i)) _ fun i ↦ S i

Premises used: Algebra.IsLocalIso.of_span_range_eq_top, Pi.single, OfNat.ofNat
-- Module: Mathlib.RingTheory.LocalIso
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)
⊢ Eq (α := Ideal ((j : ι) → S j)) (Ideal.span (Set.range fun (i : ι) ↦ Pi.single (M := S) i 1)) ⊤

Tactic:
Ideal.span_single_eq_top _

Premises used: Ideal.span_single_eq_top
-- Module: Mathlib.RingTheory.LocalIso
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)
⊢ Eq (α := Ideal ((j : ι) → S j)) (Ideal.span (Set.range fun (i : ι) ↦ Pi.single (M := S) i 1)) ⊤

Tactic:
exact Ideal.span_single_eq_top _

Premises used: Ideal.span_single_eq_top
-- Module: Mathlib.RingTheory.LocalIso
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)
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)) ⊤
⊢ 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 _

Premises used: Ideal.span_single_eq_top