awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
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
rw : ∀ (K : Set β), IsCompact K → TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop K
⊢ HasProdLocallyUniformly f g

Tactic:
rw [HasProdLocallyUniformly, tendstoLocallyUniformly_iff_forall_isCompact]

Premises used: HasProdLocallyUniformly, tendstoLocallyUniformly_iff_forall_isCompact
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
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
⊢ ∀ (K : Set β), IsCompact K → TendstoUniformlyOn (fun (x1 : Finset ι) (x2 : β) ↦ ∏ i ∈ x1, f i x2) g atTop K

Tactic:
simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn] using h

Premises used: hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : ∀ (x : β), ∃ t ∈ 𝓝 x, MultipliableUniformlyOn f t
⊢ MultipliableLocallyUniformly f

Tactic:
hasProdLocallyUniformly_of_of_forall_exists_nhds
    (fun x => (h x).imp fun _ ht => ⟨ht.1, ht.2.hasProdUniformlyOn⟩)
    |>.multipliableLocallyUniformly

Premises used: HasProdLocallyUniformly.multipliableLocallyUniformly, hasProdLocallyUniformly_of_of_forall_exists_nhds, Exists.imp, And.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
g : β → α
x : β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : HasProdLocallyUniformly f g
⊢ HasProd (fun (x_1 : ι) ↦ f x_1 x) (g x)

Tactic:
h.tendstoLocallyUniformlyOn.tendsto_at (Set.mem_univ x)

Premises used: iInf, HasProd, TendstoLocallyUniformly.tendstoLocallyUniformlyOn, Filter.atTop, TendstoLocallyUniformlyOn.tendsto_at, Set.mem_univ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
x : β
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : MultipliableLocallyUniformly f
⊢ Multipliable.{u_1, u_3} (α := α) fun (x_1 : ι) ↦ f x_1 x

Tactic:
h.choose_spec.hasProd.multipliable

Premises used: Exists.choose_spec, HasProdLocallyUniformly.hasProd, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
h : MultipliableLocallyUniformly f
⊢ HasProdLocallyUniformly f fun (x : β) ↦ ∏' (i : ι), f i x

Tactic:
h.elim fun _ hg => hg.congr_inseparable_right fun _ =>
    tendsto_nhds_unique_inseparable hg.hasProd hg.hasProd.multipliable.hasProd

Premises used: TendstoLocallyUniformly.congr_inseparable_right, HasProdLocallyUniformly.hasProd, tendsto_nhds_unique_inseparable, Multipliable.hasProd, HasProd.multipliable, Exists.elim
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
inst : CommMonoid α
f : ι → β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
⊢ MultipliableLocallyUniformly f ↔ HasProdLocallyUniformly f fun (x : β) ↦ ∏' (i : ι), f i x

Tactic:
⟨MultipliableLocallyUniformly.hasProdLocallyUniformly,
    HasProdLocallyUniformly.multipliableLocallyUniformly⟩

Premises used: HasProdLocallyUniformly.multipliableLocallyUniformly, MultipliableLocallyUniformly.hasProdLocallyUniformly, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.UniformOn
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
g : β → α
inst_1 : UniformSpace α
inst_2 : TopologicalSpace β
f : ℕ → β → α
h : HasProdLocallyUniformly f g
⊢ TendstoLocallyUniformly (fun (x1 : ℕ) (x2 : β) ↦ ∏ i ∈ Finset.range x1, f i x2) g atTop

Tactic:
simpa only [tendstoLocallyUniformlyOn_univ] using
    (h.hasProdLocallyUniformlyOn (s := .univ)).tendstoLocallyUniformlyOn_finsetRange

Premises used: HasProdLocallyUniformlyOn.tendstoLocallyUniformlyOn_finsetRange, tendstoLocallyUniformlyOn_univ, HasProdLocallyUniformly.hasProdLocallyUniformlyOn
-- Module: Mathlib.Topology.Algebra.IntermediateField
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : TopologicalSpace L
inst_4 : IsTopologicalRing L
X : Type u_3
inst_5 : TopologicalSpace X
inst_6 : MulAction L X
inst_7 : ContinuousSMul L X
M_1 M : IntermediateField K L
⊢ ContinuousSMul.{u_2, u_3} (↥M) X

Tactic:
M.toSubfield.continuousSMul X

Premises used: Set.Mem, Subfield.continuousSMul, IntermediateField.toSubfield
-- Module: Mathlib.Topology.Algebra.IntermediateField
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : TopologicalSpace L
inst_4 : IsTopologicalRing L
X : Type u_3
inst_5 : TopologicalSpace X
inst_6 : MulAction L X
inst_7 : ContinuousSMul L X
M_1 M : IntermediateField K L
⊢ ContinuousSMul.{u_2, u_2} ↥⊥ ↥M

Tactic:
Topology.IsInducing.continuousSMul (X := L) (N := (⊥ : IntermediateField K L)) (Y := M)
    (M := (⊥ : IntermediateField K L)) Topology.IsInducing.subtypeVal continuous_id rfl

Premises used: Topology.IsInducing.continuousSMul, continuous_id, rfl, Topology.IsInducing.subtypeVal
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
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

Tactic:
⟨Units.isEmbedding_val₀, ?_⟩

Premises used: Units.isEmbedding_val₀, Topology.IsOpenEmbedding.mk
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
refine : IsOpen[inst_1] (Set.range (ι := Mˣ) Units.val)
⊢ IsOpenEmbedding.{u_1, u_1} (X := Mˣ) Units.val

Tactic:
refine ⟨Units.isEmbedding_val₀, ?_⟩
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
⊢ IsOpen[inst_1] {0}ᶜ

Tactic:
(isClosed_singleton (X := M) (x := 0)).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
h : Eq (α := Set M) (Set.range (ι := Mˣ) Units.val) {0}ᶜ
⊢ IsOpen[inst_1] (Set.range (ι := Mˣ) Units.val)

Tactic:
convert! (isClosed_singleton (X := M) (x := 0)).isOpen_compl

Premises used: IsClosed.isOpen_compl
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
h : ∀ (x : M), Membership.mem (γ := Set M) (Set.range (ι := Mˣ) Units.val) x ↔ Membership.mem (γ := Set M) {0}ᶜ x
⊢ Eq (α := Set M) (Set.range (ι := Mˣ) Units.val) {0}ᶜ

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
x : M
⊢ (∃ (y : Mˣ), (↑y : M) = x) ↔ ¬x = 0

Tactic:
isUnit_iff_ne_zero

Premises used: IsUnit, isUnit_iff_ne_zero
-- Module: Mathlib.Topology.Algebra.IsOpenUnits
Goal:
M : Type u_1
inst : GroupWithZero M
inst_1 : TopologicalSpace M
inst_2 : ContinuousInv₀ M
inst_3 : T1Space M
x : M
⊢ (∃ (y : Mˣ), (↑y : M) = x) ↔ ¬x = 0

Tactic:
exact isUnit_iff_ne_zero

Premises used: isUnit_iff_ne_zero
-- 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 ⊥
⊢ IsOpenUnits R

Tactic:
⟨.of_continuous_injective_isOpenMap Units.continuous_val Units.val_injective ?_⟩

Premises used: IsOpenUnits.mk, Units.continuous_val, Topology.IsOpenEmbedding.of_continuous_injective_isOpenMap, Units.val_injective
-- 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 ⊥
refine : IsOpenMap.{u_1, u_1} (X := Rˣ) Units.val
⊢ IsOpenUnits R

Tactic:
refine ⟨.of_continuous_injective_isOpenMap Units.continuous_val Units.val_injective ?_⟩
-- 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 ⊥
⊢ IsOpenMap.{u_1, u_1} (X := Rˣ) Units.val

Tactic:
(IsTopologicalGroup.isOpenMap_iff_nhds_one (f := Units.coeHom R)).mpr ?_

Premises used: Iff.mpr, IsTopologicalGroup.isOpenMap_iff_nhds_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 ⊥
refine : LE.le (α := Filter R) (𝓝 1) (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R) (𝓝 1))
⊢ IsOpenMap.{u_1, u_1} (X := Rˣ) Units.val

Tactic:
refine (IsTopologicalGroup.isOpenMap_iff_nhds_one (f := Units.coeHom R)).mpr ?_

Premises used: Iff.mpr, IsTopologicalGroup.isOpenMap_iff_nhds_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 ⊥
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))))
⊢ LE.le (α := Filter R) (𝓝 1) (Filter.map (α := Rˣ) (⇑(Units.coeHom R) : (a : Rˣ) → R) (𝓝 1))

Tactic:
rw [nhds_induced, nhds_prod_eq]

Premises used: nhds_induced, nhds_prod_eq
-- 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 ⊥
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))))
⊢ 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:
simp only [Units.embedProduct_apply, Units.val_one, inv_one, MulOpposite.op_one]

Premises used: inv_one, MulOpposite.op_one, Units.val_one, Units.embedProduct_apply
-- 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
⊢ 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
-- 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)
⊢ (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))
-- 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 :
  (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)))
⊢ (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

Premises used: and_self, Homeomorph.comap_nhds_eq, Set.image_add_left, MulOpposite.op_one, Homeomorph.symm_symm, MulOpposite.opHomeomorph_apply
-- 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 :
  (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)))
⊢ ∃ (n₁ : ℕ) (n₂ : ℕ), ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s

Tactic:
simpa [Set.subset_def, forall_comm (β := Rˣ), forall_comm (β := _ = _)] using
      (((this.comap (Units.embedProduct R)).map (Units.coeHom R)).1 _).mp hs

Premises used: Units.coeHom, Set.subset_def, forall_comm, Filter.HasBasis.map, Filter.HasBasis.comap, Iff.mp, Filter.HasBasis.mem_iff', Units.embedProduct, DFunLike.coe
-- 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 :
  (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)))
⊢ ∃ (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
-- 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₁ 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
⊢ ∃ (n : ℕ), n ≠ 0 ∧ ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n → -1 + (↑u⁻¹ : R) ∈ I ^ n → (↑u : R) ∈ s

Tactic:
obtain ⟨n₁, n₂, H⟩ := 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_1 :
  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)))
n₁ n₂ : ℕ
H : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
⊢ max (max n₁ n₂) 1 ≠ 0

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_1 :
  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)))
n₁ n₂ : ℕ
H : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
u : Rˣ
h₁ : -1 + (↑u : R) ∈ I ^ max (max n₁ n₂) 1
h₂ : -1 + (↑u⁻¹ : R) ∈ I ^ max (max n₁ n₂) 1
⊢ n₁ ≤ max (max n₁ n₂) 1

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_1 :
  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)))
n₁ n₂ : ℕ
H : ∀ (u : Rˣ), -1 + (↑u : R) ∈ I ^ n₁ → -1 + (↑u⁻¹ : R) ∈ I ^ n₂ → (↑u : R) ∈ s
u : Rˣ
h₁ : -1 + (↑u : R) ∈ I ^ max (max n₁ n₂) 1
h₂ : -1 + (↑u⁻¹ : R) ∈ I ^ max (max n₁ n₂) 1
⊢ n₂ ≤ max (max n₁ n₂) 1

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_1 :
  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)))
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:
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₂)⟩