awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
      Eq (α := Subring D) (Subring.center D) ⊤
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
val : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ Membership.mem (γ := Subring ↥R) ⊤ (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)

Tactic:
trivial
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
      Eq (α := Subring D) (Subring.center D) ⊤
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
val : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
rw : card.{u_1} ↥R < card.{u_1} ↥⊤
⊢ card.{u_1} ↥R < n

Tactic:
rw [← hn, ← Subring.card_top D]

Premises used: Subring.card_top
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
      Eq (α := Subring D) (Subring.center D) ⊤
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
val : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card.{u_1} (↑(↑R : Set D) : Type u_1) < card.{u_1} (↑(↑⊤ : Set D) : Type u_1)

Tactic:
Set.card_lt_card hR

Premises used: Set.card_lt_card
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
n : ℕ
IH :
  ∀ m < n,
    ∀ (D : Type u_1) [inst : DivisionRing D] [Finite D] (val : Fintype D) (hn : card D = m),
      Eq (α := Subring D) (Subring.center D) ⊤
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
val : Fintype D
hn : card D = n
R : Subring D
hR : R < ⊤
x y : D
hx : x ∈ R
hy : y ∈ R
R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R
⊢ card.{u_1} ↥R < card.{u_1} ↥⊤

Tactic:
convert! Set.card_lt_card hR

Premises used: Set.card_lt_card
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
x y : D
⊢ x * y = y * x

Tactic:
simp [Subring.mem_center_iff.mp ?_ x, center_eq_top D]

Premises used: Subring.mem_center_iff, _private.0.LittleWedderburn.center_eq_top, Iff.mp
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
D : Type u_1
inst : Finite D
inst_1 : Ring D
inst_2 : IsDomain D
intro : ∀ (val : Fintype D), IsField D
⊢ IsField D

Tactic:
cases nonempty_fintype D

Premises used: nonempty_fintype
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
D : Type u_1
inst : Finite D
inst_1 : Ring D
inst_2 : IsDomain D
val : Fintype D
x : DivisionRing D := divisionRingOfIsDomain D
x_1 : Field D := littleWedderburn D
⊢ IsField D

Tactic:
Field.toIsField D

Premises used: Field.toIsField
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
D : Type u_1
inst : Finite D
inst_1 : Ring D
inst_2 : IsDomain D
val : Fintype D
x : DivisionRing D := divisionRingOfIsDomain D
x_1 : Field D := littleWedderburn D
⊢ IsField D

Tactic:
exact Field.toIsField D

Premises used: Field.toIsField
-- Module: Mathlib.RingTheory.LittleWedderburn
Goal:
D : Type u_1
inst : Finite D
inst_1 : Ring D
inst_2 : IsDomain D
intro : ∀ (val : Fintype D), IsField D
intro₁ intro₂ : ∀ (val : Fintype D), IsField D
⊢ IsField D

Tactic:
classical
  cases nonempty_fintype D
  let _ := Fintype.divisionRingOfIsDomain D
  let _ := littleWedderburn D
  exact Field.toIsField D

Premises used: nonempty_fintype
-- 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
inst_3 : IsLocalIso R S
by_contra :
  ∀
    (hne :
      ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤),
    False
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤

Tactic:
by_contra hne
-- 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
inst_3 : IsLocalIso R S
hne : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤
obtain :
  ∀ (m : Ideal S) (hm : m.IsMaximal)
    (hms : Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} ≤ m), False
⊢ False

Tactic:
obtain ⟨m, hm, hms⟩ := Ideal.exists_le_maximal _ hne

Premises used: Ideal.exists_le_maximal
-- 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
inst_3 : IsLocalIso R S
hne : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤
m : Ideal S
hm : m.IsMaximal
hms : Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} ≤ m
obtain : ∀ (g : S) (hgm : g ∉ m) (hstd : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)), False
⊢ False

Tactic:
obtain ⟨g, hgm, hstd⟩ :=
    Algebra.IsLocalIso.exists_notMem_isStandardOpenImmersion (R := R) m

Premises used: Algebra.IsLocalIso.exists_notMem_isStandardOpenImmersion
-- 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
inst_3 : IsLocalIso R S
hne : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤
m : Ideal S
hm : m.IsMaximal
hms : Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} ≤ m
g : S
hgm : g ∉ m
hstd : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ False

Tactic:
hgm (hms (Ideal.subset_span hstd))

Premises used: Ideal.subset_span
-- 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
inst_3 : IsLocalIso R S
hne : ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤
m : Ideal S
hm : m.IsMaximal
hms : Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} ≤ m
g : S
hgm : g ∉ m
hstd : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ False

Tactic:
exact hgm (hms (Ideal.subset_span hstd))

Premises used: Ideal.subset_span
-- 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
⊢ IsLocalIso R S ↔
    Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤

Tactic:
⟨fun _ ↦ span_isStandardOpenImmersion_eq_top R S, fun h ↦ ⟨fun q hq ↦ ?_⟩⟩

Premises used: Iff.intro, Algebra.IsLocalIso.span_isStandardOpenImmersion_eq_top, Algebra.IsLocalIso.mk
-- 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
refine :
  ∀
    (h :
      Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤)
    (q : Ideal S) (hq : q.IsPrime), ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ IsLocalIso R S ↔
    Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤

Tactic:
refine ⟨fun _ ↦ span_isStandardOpenImmersion_eq_top R S, fun h ↦ ⟨fun q hq ↦ ?_⟩⟩
-- 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
h : Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤
q : Ideal S
hq : q.IsPrime
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)

Tactic:
grind [Ideal.IsPrime.ne_top, Ideal.span_le, SetLike.mem_coe]

Premises used: Ideal.span_le, SetLike.mem_coe, Ideal.IsPrime.ne_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
inst_3 : IsStandardOpenImmersion R S
q : Ideal S
hq : q.IsPrime
right : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (M := S) 1)
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)

Tactic:
use 1, hq.one_notMem

Premises used: Ideal.IsPrime.one_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
inst_3 : IsStandardOpenImmersion R S
q : Ideal S
hq : q.IsPrime
⊢ IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (M := S) 1)

Tactic:
IsStandardOpenImmersion.trans _ S _

Premises used: Algebra.IsStandardOpenImmersion.trans
-- 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
inst_3 : IsStandardOpenImmersion R S
q : Ideal S
hq : q.IsPrime
⊢ IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (M := S) 1)

Tactic:
exact IsStandardOpenImmersion.trans _ S _

Premises used: Algebra.IsStandardOpenImmersion.trans
-- 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 : 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)
⊢ IsLocalIso R S

Tactic:
⟨fun q hq ↦ ?_⟩

Premises used: Algebra.IsLocalIso.mk
-- 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 : 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)
refine : ∀ (q : Ideal S) (hq : q.IsPrime), ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ IsLocalIso R S

Tactic:
refine ⟨fun q hq ↦ ?_⟩
-- 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 : 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
rw :
  ∀ (h : Eq.{u_2 + 1} (α := TopologicalSpace.Opens (PrimeSpectrum S)) (⨆ (i : ι), PrimeSpectrum.basicOpen (f i)) ⊤)
    (T : ι → Type u_4) [inst_9 : (i : ι) → CommSemiring (T i)] [inst_10 : (i : ι) → Algebra.{u_1, u_4} R (T i)]
    [inst_11 : (i : ι) → Algebra.{u_2, u_4} S (T i)] [∀ (i : ι), IsScalarTower.{u_1, u_2, u_4} R S (T i)]
    [∀ (i : ι), IsLocalization.Away.{u_2, u_4} (f i) (T i)] [∀ (i : ι), IsLocalIso.{u_1, u_4} R (T i)] (q : Ideal S)
    (hq : q.IsPrime), ∃ (i : ι), f i ∉ q
⊢ ∃ (i : ι), f i ∉ q

Tactic:
rw [← PrimeSpectrum.iSup_basicOpen_eq_top_iff] at h

Premises used: PrimeSpectrum.iSup_basicOpen_eq_top_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
ι : Type u_3
f : ι → S
h : Eq.{u_2 + 1} (α := TopologicalSpace.Opens (PrimeSpectrum S)) (⨆ (i : ι), PrimeSpectrum.basicOpen (f i)) ⊤
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
⊢ Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (⨆ (i : ι), PrimeSpectrum.basicOpen (f i))
    { asIdeal := q, isPrime := hq : PrimeSpectrum S }

Tactic:
simp [h]
-- 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 : Eq.{u_2 + 1} (α := TopologicalSpace.Opens (PrimeSpectrum S)) (⨆ (i : ι), PrimeSpectrum.basicOpen (f i)) ⊤
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
⊢ Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (⨆ (i : ι), PrimeSpectrum.basicOpen (f i))
    { asIdeal := q, isPrime := hq : PrimeSpectrum S }

Tactic:
have : ⟨q, hq⟩ ∈ ⨆ i, PrimeSpectrum.basicOpen (f i) := by simp [h]
-- 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 : Eq.{u_2 + 1} (α := TopologicalSpace.Opens (PrimeSpectrum S)) (⨆ (i : ι), PrimeSpectrum.basicOpen (f i)) ⊤
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
this :
  Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (⨆ (i : ι), PrimeSpectrum.basicOpen (f i))
    { asIdeal := q, isPrime := hq : PrimeSpectrum S }
⊢ ∃ (i : ι), f i ∉ q

Tactic:
simpa using this
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
f : ι → S
h : 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
obtain : ∀ (i : ι) (hi : f i ∉ q), ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)

Tactic:
obtain ⟨i, hi⟩ : ∃ i, f i ∉ q := by
    rw [← PrimeSpectrum.iSup_basicOpen_eq_top_iff] at h
    have : ⟨q, hq⟩ ∈ ⨆ i, PrimeSpectrum.basicOpen (f i) := by simp [h]
    simpa using this
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
f : ι → S
h : 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
⊢ Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen (f i))
    { asIdeal := q, isPrime := hq : PrimeSpectrum S }

Tactic:
have : ⟨q, hq⟩ ∈ PrimeSpectrum.basicOpen (f i) := hi
-- 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 : 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
this :
  Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum S)) (PrimeSpectrum.basicOpen (f i))
    { asIdeal := q, isPrime := hq : PrimeSpectrum S }
⊢ Membership.mem (γ := Set (PrimeSpectrum S))
    (Set.range.{u_2, u_4 + 1} (ι := PrimeSpectrum (T i)) (PrimeSpectrum.comap (algebraMap S (T i))))
    { asIdeal := q, isPrime := hq : PrimeSpectrum S }

Tactic:
rw [← SetLike.mem_coe, ← PrimeSpectrum.localization_away_comap_range (T i)] at this

Premises used: SetLike.mem_coe, PrimeSpectrum.localization_away_comap_range
-- 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 : 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
this :
  Membership.mem (γ := Set (PrimeSpectrum S))
    (Set.range.{u_2, u_4 + 1} (ι := PrimeSpectrum (T i)) (PrimeSpectrum.comap (algebraMap S (T i))))
    { asIdeal := q, isPrime := hq : PrimeSpectrum S }
obtain :
  ∀ (q' : PrimeSpectrum (T i))
    (hq' : PrimeSpectrum.comap (algebraMap S (T i)) q' = { asIdeal := q, isPrime := hq : PrimeSpectrum S }),
    ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)

Tactic:
obtain ⟨q', hq'⟩ := this
-- Module: Mathlib.RingTheory.LocalIso
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
inst_2 : Algebra R S
ι : Type u_3
f : ι → S
h : 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 }
obtain :
  ∀ (g' : T i) (hg' : g' ∉ q'.asIdeal) (h : IsStandardOpenImmersion.{u_1, u_4} R (Localization.Away g')),
    ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)

Tactic:
obtain ⟨g', hg', h⟩ := exists_notMem_isStandardOpenImmersion (R := R) q'.1

Premises used: Algebra.IsLocalIso.exists_notMem_isStandardOpenImmersion, PrimeSpectrum.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)
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')
obtain :
  ∀ (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, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)

Tactic:
obtain ⟨n, g, hg⟩ := IsLocalization.Away.surj (f i) g'

Premises used: IsLocalization.Away.surj
-- 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
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)

Tactic:
⟨g * (f i), ?_, ?_⟩

Premises used: HMul.hMul, And.intro, Exists.intro
-- 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 * f i ∉ q
refine_2 : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (g * f i))
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)

Tactic:
refine ⟨g * (f i), ?_, ?_⟩
-- 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
⊢ g * f i ∉ q

Tactic:
Ideal.IsPrime.mul_notMem hq ?_ hi

Premises used: Ideal.IsPrime.mul_notMem