awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
intro : ∀ (val : Fintype D), Eq (α := Subring D) (Subring.center D) ⊤
intro₁ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n),
    Eq (α := Subring D) (Subring.center D) ⊤
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have intro₂ : ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n), InductionHyp D
Tactic: classical
  cases nonempty_fintype D
  induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
  apply InductionHyp.center_eq_top
  intro R hR x y hx hy
  suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩
  let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R
  rw [IH (Fintype.card R) _ R inferInstance rfl]
  · trivial
  rw [← hn, ← Subring.card_top D]
  convert! Set.card_lt_card hR
Cleared hypotheses: D, inst, inst_1
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
intro : ∀ (val : Fintype D), Eq (α := Subring D) (Subring.center D) ⊤
intro₁ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n),
    Eq (α := Subring D) (Subring.center D) ⊤
intro₂ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n), InductionHyp D
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have intro₃ : ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
  ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R), x * y = y * x
Tactic: classical
  cases nonempty_fintype D
  induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
  apply InductionHyp.center_eq_top
  intro R hR x y hx hy
  suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩
  let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R
  rw [IH (Fintype.card R) _ R inferInstance rfl]
  · trivial
  rw [← hn, ← Subring.card_top D]
  convert! Set.card_lt_card hR
Cleared hypotheses: D, inst, inst_1
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
intro : ∀ (val : Fintype D), Eq (α := Subring D) (Subring.center D) ⊤
intro₁ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n),
    Eq (α := Subring D) (Subring.center D) ⊤
intro₂ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n), InductionHyp D
intro₃ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
    ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R), x * y = y * x
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have intro₄ : ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
  ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R),
  Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
Tactic: classical
  cases nonempty_fintype D
  induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
  apply InductionHyp.center_eq_top
  intro R hR x y hx hy
  suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩
  let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R
  rw [IH (Fintype.card R) _ R inferInstance rfl]
  · trivial
  rw [← hn, ← Subring.card_top D]
  convert! Set.card_lt_card hR
Cleared hypotheses: D, inst, inst_1
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : DivisionRing D
inst_1 : Finite D
intro : ∀ (val : Fintype D), Eq (α := Subring D) (Subring.center D) ⊤
intro₁ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n),
    Eq (α := Subring D) (Subring.center D) ⊤
intro₂ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n), InductionHyp D
intro₃ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
    ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R), x * y = y * x
intro₄ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
    ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R),
    Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
intro₅ :
  ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
    ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R),
    Membership.mem (γ := Subring ↥R) (Subring.center ↥R) (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
⊢ Eq (α := Subring D) (Subring.center D) ⊤
have intro₆ : ∀ (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] [Finite D] (val : Fintype D) (hn : card D = n) {R : Subring D} (hR : R < ⊤)
  ⦃x y : D⦄ (hx : x ∈ R) (hy : y ∈ R),
  let R_dr : DivisionRing ↥R := divisionRingOfIsDomain ↥R;
  Membership.mem (γ := Subring ↥R) ⊤ (Subtype.mk (p := fun (x : D) ↦ x ∈ R) y hy)
Tactic: classical
  cases nonempty_fintype D
  induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH
  apply InductionHyp.center_eq_top
  intro R hR x y hx hy
  suffices (⟨y, hy⟩ : R) ∈ Subring.center R by
    rw [Subring.mem_center_iff] at this
    simpa using this ⟨x, hx⟩
  let R_dr : DivisionRing R := Fintype.divisionRingOfIsDomain R
  rw [IH (Fintype.card R) _ R inferInstance rfl]
  · trivial
  rw [← hn, ← Subring.card_top D]
  convert! Set.card_lt_card hR
Cleared hypotheses: D, inst, inst_1
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : Finite D
inst_1 : Ring D
inst_2 : IsDomain D
⊢ IsField D
have intro : ∀ (val : Fintype D), IsField D
Tactic: cases nonempty_fintype D
-- Lean 4 proof step from Mathlib.RingTheory.LittleWedderburn (goal)
Goal:
D : Type u_1
inst : Finite D
inst_1 : Ring D
inst_2 : IsDomain D
⊢ IsField D
have intro : ∀ (val : Fintype D), IsField D
Tactic: classical
  cases nonempty_fintype D
  let _ := Fintype.divisionRingOfIsDomain D
  let _ := littleWedderburn D
  exact Field.toIsField D
-- 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
inst_3 : IsLocalIso R S
⊢ Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤
have by_contra : ∀
  (hne :
    ¬Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤),
  False
Tactic: by_contra hne
-- 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
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)}) ⊤
⊢ False
have obtain : ∀ (m : Ideal S) (hm : m.IsMaximal)
  (hms : Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)} ≤ m), False
Tactic: obtain ⟨m, hm, hms⟩ := Ideal.exists_le_maximal _ hne
-- 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
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
⊢ False
have obtain : ∀ (g : S) (hgm : g ∉ m) (hstd : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)), False
Tactic: obtain ⟨g, hgm, hstd⟩ :=
    Algebra.IsLocalIso.exists_notMem_isStandardOpenImmersion (R := R) m
-- 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
⊢ IsLocalIso R S ↔
    Eq.{u_2 + 1} (α := Ideal S) (Ideal.span {g : S | IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)}) ⊤
have 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)
Tactic: refine ⟨fun _ ↦ span_isStandardOpenImmersion_eq_top R S, fun h ↦ ⟨fun q 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
inst_3 : IsStandardOpenImmersion R S
q : Ideal S
hq : q.IsPrime
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have right : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (M := S) 1)
Tactic: use 1, hq.one_notMem
-- 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 : 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
have refine : ∀ (q : Ideal S) (hq : q.IsPrime), ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
Tactic: refine ⟨fun q 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 : 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 : ι), f i ∉ q
have 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
Tactic: rw [← PrimeSpectrum.iSup_basicOpen_eq_top_iff] at h
Cleared hypotheses: h, T, inst_3, inst_4, inst_5, inst_6, inst_7, inst_8, q, hq
-- 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 : 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
⊢ ∃ (i : ι), f i ∉ q
have this : 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]
-- 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 : 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
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have obtain : ∀ (i : ι) (hi : f i ∉ q), ∃ 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
-- 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 : 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
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have this : 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
-- 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 : 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 }
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have 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 }
Tactic: rw [← SetLike.mem_coe, ← PrimeSpectrum.localization_away_comap_range (T i)] at this
Cleared hypotheses: this
-- 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 : 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 }
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have 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)
Tactic: obtain ⟨q', hq'⟩ := this
Cleared hypotheses: this
-- 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 : 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 ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have 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)
Tactic: obtain ⟨g', hg', h⟩ := exists_notMem_isStandardOpenImmersion (R := R) q'.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
ι : 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')
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have 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)
Tactic: obtain ⟨n, g, hg⟩ := IsLocalization.Away.surj (f i) g'
-- 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
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have refine_1 : g * f i ∉ q
Tactic: refine ⟨g * (f i), ?_, ?_⟩
-- 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
refine_1 : g * f i ∉ q
⊢ ∃ g ∉ q, IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away g)
have refine_2 : IsStandardOpenImmersion.{u_1, u_2} R (Localization.Away (g * f i))
Tactic: refine ⟨g * (f i), ?_, ?_⟩
-- 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
⊢ g * f i ∉ q
have refine_1 : g ∉ q
Tactic: refine Ideal.IsPrime.mul_notMem hq ?_ hi