awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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
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
⊢ 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₂)⟩
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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
rw : ∃ (i : ℕ), True ∧ (fun (y : R) ↦ 1 + y) '' (↑(I ^ i) : Set R) ⊆ s
⊢ Membership.mem (γ := Filter R) (𝓝 1) s

Tactic:
rw [H.1]

Premises used: Filter.HasBasis.mem_iff'
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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

Tactic:
⟨n, trivial, ?_⟩

Premises used: trivial, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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
refine : (fun (y : R) ↦ 1 + y) '' (↑(I ^ n) : Set R) ⊆ s
⊢ ∃ (i : ℕ), True ∧ (fun (y : R) ↦ 1 + y) '' (↑(I ^ i) : Set R) ⊆ s

Tactic:
refine ⟨n, trivial, ?_⟩
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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)
⊢ IsUnit (x * 1 + 1)

Tactic:
have := Ideal.mem_jacobson_bot.mp (hI (Ideal.pow_le_self hn hx)) 1
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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)
⊢ IsUnit (1 + x)

Tactic:
rw [mul_one, add_comm] at this

Premises used: add_comm, mul_one
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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) ∈ I ^ n

Tactic:
simpa using hx
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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)
refine : -1 + (↑this.unit⁻¹ : R) ∈ I ^ n
⊢ (fun (y : R) ↦ 1 + y) x ∈ s

Tactic:
refine hn' this.unit (by simpa using hx) ?_

Premises used: IsUnit.unit
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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)
trans₁ : (↑this.unit⁻¹ : R) * (-(1 + x) + 1) = -(↑this.unit⁻¹ : R) * x
⊢ -1 + (↑this.unit⁻¹ : R) = -(↑this.unit⁻¹ : R) * x

Tactic:
trans this.unit⁻¹ * (-(1 + x) + 1)

Premises used: HAdd.hAdd, IsUnit.unit, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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)
rw : -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * -(1 + x) + (↑this.unit⁻¹ : R) * 1
rw₁ : -1 + (↑this.unit⁻¹ : R) = -((↑this.unit⁻¹ : R) * (1 + x)) + (↑this.unit⁻¹ : R) * 1
rw₂ : -1 + (↑this.unit⁻¹ : R) = -1 + (↑this.unit⁻¹ : R) * 1
rw₃ rw₄ : -1 + (↑this.unit⁻¹ : R) = -1 + (↑this.unit⁻¹ : R)
⊢ -1 + (↑this.unit⁻¹ : R) = (↑this.unit⁻¹ : R) * (-(1 + x) + 1)

Tactic:
rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]

Premises used: mul_add, mul_one, IsUnit.val_inv_mul, mul_neg
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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)
⊢ (↑this.unit⁻¹ : R) * (-(1 + x) + 1) = -(↑this.unit⁻¹ : R) * x

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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

Tactic:
have : -1 + ↑this.unit⁻¹ = -this.unit⁻¹ * x := by
    trans this.unit⁻¹ * (-(1 + x) + 1)
    · rw [mul_add, mul_neg, IsUnit.val_inv_mul, mul_one]
    · simp
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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_3 : IsUnit (1 + x)
this : -1 + (↑this_3.unit⁻¹ : R) = -(↑this_3.unit⁻¹ : R) * x
rw : -(↑this_3.unit⁻¹ : R) * x ∈ I ^ n
⊢ -1 + (↑this_3.unit⁻¹ : R) ∈ I ^ n

Tactic:
rw [this]
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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_3 : IsUnit (1 + x)
this : -1 + (↑this_3.unit⁻¹ : R) = -(↑this_3.unit⁻¹ : R) * x
⊢ -(↑this_3.unit⁻¹ : R) * x ∈ I ^ n

Tactic:
Ideal.mul_mem_left _ _ hx

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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_3 : IsUnit (1 + x)
this : -1 + (↑this_3.unit⁻¹ : R) = -(↑this_3.unit⁻¹ : R) * x
⊢ -(↑this_3.unit⁻¹ : R) * x ∈ I ^ n

Tactic:
exact Ideal.mul_mem_left _ _ hx

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
a : α
nth_rw : Function.Injective (β := α × α) fun (x : α × α) ↦ (x.1 * a, x.2 * a)
⊢ comap (fun (x : α × α) ↦ (x.1 * a, x.2 * a)) (𝓤 α) = 𝓤 α

Tactic:
nth_rw 1 [← uniformity_translate_mul a, comap_map]

Premises used: Filter.comap_map, uniformity_translate_mul
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : Group α
inst_2 : IsUniformGroup α
a p₁ p₂ q₁ q₂ : α
⊢ Eq.{u_1 + 1} (α := α × α) ((fun (x : α × α) ↦ (x.1 * a, x.2 * a)) (p₁, p₂))
      ((fun (x : α × α) ↦ (x.1 * a, x.2 * a)) (q₁, q₂)) →
    (p₁, p₂) = (q₁, q₂)

Tactic:
simp only [Prod.mk.injEq, mul_left_inj, imp_self]

Premises used: mul_left_inj, imp_self, Prod.mk.injEq
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_4
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
𝓕 : Filter G
⊢ Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Tendsto (β := G) (fun (p : G × G) ↦ p.1 / p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [Cauchy, uniformity_eq_comap_nhds_one_swapped, ← tendsto_iff_comap]

Premises used: Cauchy, Filter.tendsto_iff_comap, uniformity_eq_comap_nhds_one_swapped
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_4
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
𝓕 : Filter G
⊢ Cauchy 𝓕 ↔ 𝓕.NeBot ∧ Tendsto (β := G) (fun (p : G × G) ↦ p.2 / p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [Cauchy, uniformity_eq_comap_nhds_one, ← tendsto_iff_comap]

Premises used: Cauchy, Filter.tendsto_iff_comap, uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_3
G : Type u_4
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
𝓕 : Filter ι
f : ι → G
⊢ Cauchy (map f 𝓕) ↔ 𝓕.NeBot ∧ Tendsto.{u_3, u_4} (β := G) (fun (p : ι × ι) ↦ f p.1 / f p.2) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [cauchy_map_iff, uniformity_eq_comap_nhds_one_swapped, Function.comp_def]

Premises used: cauchy_map_iff, Function.comp_def, uniformity_eq_comap_nhds_one_swapped
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
ι : Type u_3
G : Type u_4
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
𝓕 : Filter ι
f : ι → G
⊢ Cauchy (map f 𝓕) ↔ 𝓕.NeBot ∧ Tendsto.{u_3, u_4} (β := G) (fun (p : ι × ι) ↦ f p.2 / f p.1) (𝓕 ×ˢ 𝓕) (𝓝 1)

Tactic:
simp [cauchy_map_iff, uniformity_eq_comap_nhds_one, Function.comp_def]

Premises used: cauchy_map_iff, Function.comp_def, uniformity_eq_comap_nhds_one
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
⊢ f.NeBot

Tactic:
have : f.NeBot := hf.1
-- Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic
Goal:
G : Type u_3
inst : Group G
inst_1 : UniformSpace G
inst_2 : IsRightUniformGroup G
inst_3 : WeaklyLocallyCompactSpace G
f : Filter G
hf : Cauchy f
this : f.NeBot
obtain : ∀ (K : Set G) (K_compact : IsCompact K) (K_mem : Membership.mem (γ := Filter G) (𝓝 1) K), ∃ (x : G), f ≤ 𝓝 x
⊢ ∃ (x : G), f ≤ 𝓝 x

Tactic:
obtain ⟨K, K_compact, K_mem⟩ := WeaklyLocallyCompactSpace.exists_compact_mem_nhds (1 : G)

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds, OfNat.ofNat