awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
s : Set β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f : ℕ → β → α
h : TendstoLocallyUniformlyOn (fun (x1 : Finset ℕ) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop s
v : Set (α × α)
hv : v ∈ uniformity α
r : β
hr : r ∈ s
⊢ ∃ t ∈ 𝓝[s] r, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun (N : ℕ) (b : β) ↦ (∏ i ∈ Finset.range N, f i b : α)) n y) ∈ v
have obtain : ∀ (t : Set β) (ht : t ∈ 𝓝[s] r)
  (htr : ∀ᶠ (n : Finset ℕ) in atTop, ∀ y ∈ t, (g y, (fun (x1 : Finset ℕ) (x2 : β) ↦ (∏ i ∈ x1, f i x2 : α)) n y) ∈ v),
  ∃ t ∈ 𝓝[s] r, ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, (g y, (fun (N : ℕ) (b : β) ↦ (∏ i ∈ Finset.range N, f i b : α)) n y) ∈ v
Tactic: obtain ⟨t, ht, htr⟩ := h v hv r hr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
f' : ι → β → α
h : HasProdUniformly f g
hff' : ∀ᶠ (n : Finset ι) in atTop, ∀ (b : β), Eq.{u_1 + 1} (α := α) (∏ i ∈ n, f i b) (∏ i ∈ n, f' i b)
⊢ HasProdUniformly f' g
have rw : ∀ (h : TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop)
  (hff' : ∀ᶠ (n : Finset ι) in atTop, ∀ (b : β), Eq.{u_1 + 1} (α := α) (∏ i ∈ n, f i b) (∏ i ∈ n, f' i b)),
  TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f' i x2) g atTop
Tactic: rw [hasProdUniformly_iff_tendstoUniformly] at *
Cleared hypotheses: h, hff'
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdUniformly f g
⊢ HasProdLocallyUniformly f g
have h₁ : TendstoUniformly (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop
Tactic: simp only [hasProdUniformly_iff_tendstoUniformly, HasProdLocallyUniformly] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.UniformOn (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
inst_3 : LocallyCompactSpace β
h : ∀ (K : Set β), IsCompact K → HasProdUniformlyOn f g K
⊢ HasProdLocallyUniformly f g
have rw : ∀ (K : Set β), IsCompact K → TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop K
Tactic: rw [HasProdLocallyUniformly, tendstoLocallyUniformly_iff_forall_isCompact]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
⊢ IsOpenEmbedding.{u_1, u_1} (X := Mˣ) Units.val
have refine : IsOpen[inst_1] (Set.range (ι := Mˣ) Units.val)
Tactic: refine ⟨Units.isEmbedding_val₀, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
⊢ IsOpen[inst_1] (Set.range (ι := Mˣ) Units.val)
have h : Eq (α := Set M) (Set.range (ι := Mˣ) Units.val) {0}ᶜ
Tactic: convert! (isClosed_singleton (X := M) (x := 0)).isOpen_compl
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
⊢ Eq (α := Set M) (Set.range (ι := Mˣ) Units.val) {0}ᶜ
have h : ∀ (x : M), Membership.mem (γ := Set M) (Set.range (ι := Mˣ) Units.val) x ↔ Membership.mem (γ := Set M) {0}ᶜ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
⊢ IsOpenUnits R
have refine : IsOpenMap.{u_1, u_1} (X := Rˣ) Units.val
Tactic: refine ⟨.of_continuous_injective_isOpenMap Units.continuous_val Units.val_injective ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
⊢ IsOpenMap.{u_1, u_1} (X := Rˣ) Units.val
have refine : LE.le (α := Filter R) (𝓝 1) (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R) (𝓝 1))
Tactic: refine (IsTopologicalGroup.isOpenMap_iff_nhds_one (f := Units.coeHom R)).mpr ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
⊢ LE.le (α := Filter R) (𝓝 1) (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R) (𝓝 1))
have rw : LE.le (α := Filter R) (𝓝 1)
  (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
    (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
      (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 ((Units.embedProduct R : (a : Rˣ) → R × Rᵐᵒᵖ) 1).1)
        (𝓝 ((Units.embedProduct R : (a : Rˣ) → R × Rᵐᵒᵖ) 1).2))))
Tactic: rw [nhds_induced, nhds_prod_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
⊢ LE.le (α := Filter R) (𝓝 1)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 ((Units.embedProduct R : (a : Rˣ) → R × Rᵐᵒᵖ) 1).1)
          (𝓝 ((Units.embedProduct R : (a : Rˣ) → R × Rᵐᵒᵖ) 1).2))))
have simp : LE.le (α := Filter R) (𝓝 1)
  (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
    (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
      (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
Tactic: simp only [Units.embedProduct_apply, Units.val_one, inv_one, MulOpposite.op_one]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
⊢ Membership.mem (γ := Filter R) (𝓝 1) s
have H : Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦ (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
Tactic: have H := hR ▸ Ideal.hasBasis_nhds_adic I 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
⊢ Membership.mem (γ := Filter R) (𝓝 1) s
have this : (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1)
      (Filter.comap (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R) (𝓝 1))).HasBasis
  (fun (i : ℕ × ℕ) ↦ True ∧ True) fun (i : ℕ × ℕ) ↦
  SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (y : R) ↦ 1 + y) '' (↑(I ^ i.1) : Set R))
    (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
      ((fun (y : R) ↦ 1 + y) '' (↑(I ^ i.2) : Set R)))
Tactic: have := (H.prod (H.comap MulOpposite.opHomeomorph.symm))
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1)
        (Filter.comap (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R) (𝓝 1))).HasBasis
    (fun (i : ℕ × ℕ) ↦ True ∧ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (y : R) ↦ 1 + y) '' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (y : R) ↦ 1 + y) '' (↑(I ^ i.2) : Set R)))
⊢ Membership.mem (γ := Filter R) (𝓝 1) s
have this₁ : (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
  SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
    (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
      ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
Tactic: simp only [Homeomorph.comap_nhds_eq, Homeomorph.symm_symm, MulOpposite.opHomeomorph_apply,
    MulOpposite.op_one, and_self, Set.image_add_left] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
⊢ Membership.mem (γ := Filter R) (𝓝 1) s
have this₁ : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
Tactic: have : ∃ n₁ n₂, ∀ (u : Rˣ), (-1 + u : R) ∈ I ^ n₁ → (-1 + u⁻¹ : R) ∈ I ^ n₂ → ↑u ∈ s := by
    simpa [Set.subset_def, forall_comm (β := Rˣ), forall_comm (β := _ = _)] using
      (((this.comap (Units.embedProduct R)).map (Units.coeHom R)).1 _).mp hs
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
⊢ ∃ (n : ℕ), n ≠ 0 ∧ ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
have obtain : ∀ (n₁ n₂ : ℕ) (H : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s),
  ∃ (n : ℕ), n ≠ 0 ∧ ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
Tactic: obtain ⟨n₁, n₂, H⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
⊢ Membership.mem (γ := Filter R) (𝓝 1) s
have obtain : ∀ (n : ℕ) (hn : n ≠ 0) (hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s),
  Membership.mem (γ := Filter R) (𝓝 1) s
Tactic: obtain ⟨n, hn, hn'⟩ : ∃ n ≠ 0, ∀ (u : Rˣ), (-1 + u : R) ∈ I ^ n →
      (-1 + u⁻¹ : R) ∈ I ^ n → ↑u ∈ s := by
    obtain ⟨n₁, n₂, H⟩ := this
    exact ⟨n₁ ⊔ n₂ ⊔ 1, by simp, fun u h₁ h₂ ↦ H u
      (Ideal.pow_le_pow_right (by simp) h₁)
      (Ideal.pow_le_pow_right (by simp) h₂)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
⊢ Membership.mem (γ := Filter R) (𝓝 1) s
have rw : ∃ (i : ℕ), True ∧ (fun (y : R) ↦ 1 + y) '' (↑(I ^ i) : Set R) ⊆ s
Tactic: rw [H.1]
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
⊢ ∃ (i : ℕ), True ∧ (fun (y : R) ↦ 1 + y) '' (↑(I ^ i) : Set R) ⊆ s
have refine : (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R) ⊆ s
Tactic: refine ⟨n, trivial, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
⊢ (fun (y : R) ↦ 1 + y) x ∈ s
have this₁ : IsUnit (x * 1 + 1)
Tactic: have := Ideal.mem_jacobson_bot.mp (hI (Ideal.pow_le_self hn hx)) 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (x * 1 + 1)
⊢ (fun (y : R) ↦ 1 + y) x ∈ s
have this₁ : IsUnit (1 + x)
Tactic: rw [mul_one, add_comm] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (1 + x)
⊢ (fun (y : R) ↦ 1 + y) x ∈ s
have refine : -1 + (↑this.unit⁻¹ : R) ∈ I ^ n
Tactic: refine hn' this.unit (by simpa using hx) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (1 + x)
⊢ -1 + (↑this.unit⁻¹ : R) = -(↑this.unit⁻¹ : R) * x
have trans : -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * (-(1 + x) + 1)
Tactic: trans this.unit⁻¹ * (-(1 + x) + 1)
-- Lean 4 proof step from Mathlib.Topology.Algebra.IsOpenUnits (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ Ideal.jacobson ⊥
s : Set R
hs :
  Membership.mem (γ := Filter R)
    (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R)
      (Filter.comap (⇑(Units.embedProduct R) : (a : Rˣ) → R × Rᵐᵒᵖ)
        (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1))))
    s
H :
  Filter.HasBasis.{u_1, 1} (α := R) (𝓝 1) (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦
    (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R)
this_1 :
  (SProd.sprod (α := Filter R) (β := Filter Rᵐᵒᵖ) (𝓝 1) (𝓝 1)).HasBasis (fun (i : ℕ × ℕ) ↦ True) fun (i : ℕ × ℕ) ↦
    SProd.sprod (α := Set R) (β := Set Rᵐᵒᵖ) ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.1) : Set R))
      (Set.preimage (β := R) (⇑(Homeomorph.symm MulOpposite.opHomeomorph) : (a : Rᵐᵒᵖ) → R)
        ((fun (x : R) ↦ -1 + x) ⁻¹' (↑(I ^ i.2) : Set R)))
this_2 : ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s
x : R
hx : x ∈ (↑(I ^ n) : Set R)
this : IsUnit (1 + x)
trans : -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * (-(1 + x) + 1)
⊢ -1 + (↑this.unit⁻¹ : R) = -(↑this.unit⁻¹ : R) * x
have trans₁ : (↑this.unit⁻¹ : R) * (-(1 + x) + 1) = -(↑this.unit⁻¹ : R) * x
Tactic: trans this.unit⁻¹ * (-(1 + x) + 1)