awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.MulAction
Goal:
G : Type u_1
P : Type u_2
inst : AddGroup G
inst_1 : AddTorsor G P
inst_2 : TopologicalSpace G
inst_3 : PreconnectedSpace G
inst_4 : TopologicalSpace P
inst_5 : ContinuousVAdd G P
h :
  Eq.{u_2 + 1} (α := Set P) Set.univ
    (Set.range.{u_2, u_1 + 1} (ι := G) (⇑(Equiv.vaddConst (Classical.arbitrary P)) : (a : G) → P))
h₁ h₂ : Eq.{u_2 + 1} (α := Set P) Set.univ Set.univ
⊢ Eq.{u_2 + 1} (α := Set P) Set.univ
    (Set.image.{u_1, u_2} (α := G) (⇑(Equiv.vaddConst (Classical.arbitrary P)) : (a : G) → P) Set.univ)

Tactic:
rw [Set.image_univ, Equiv.range_eq_univ]

Premises used: Set.image_univ, Equiv.range_eq_univ
-- Module: Mathlib.Topology.Algebra.MvPolynomial
Goal:
X : Type u_1
σ : Type u_2
inst : TopologicalSpace X
inst_1 : CommSemiring X
inst_2 : IsTopologicalSemiring X
p : MvPolynomial σ X
⊢ Continuous (Y := X) fun (x : σ → X) ↦ (eval x : (a : MvPolynomial σ X) → X) p

Tactic:
continuity
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsTopologicalSemiring A
s : NonUnitalStarSubalgebra R A
⊢ IsTopologicalSemiring.{u_2} ↥s

Tactic:
s.toNonUnitalSubalgebra.instIsTopologicalSemiring

Premises used: Set.Mem, NonUnitalStarSubalgebra.toNonUnitalSubalgebra, NonUnitalSubalgebra.instIsTopologicalSemiring
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalSemiring A
s : NonUnitalStarSubalgebra R A
⊢ IsSemitopologicalSemiring.{u_2} ↥s

Tactic:
s.toNonUnitalSubalgebra.instIsSemitopologicalSemiring

Premises used: Set.Mem, NonUnitalSubalgebra.instIsSemitopologicalSemiring, NonUnitalStarSubalgebra.toNonUnitalSubalgebra
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalSemiring A
s : NonUnitalStarSubalgebra R A
⊢ s ≤ s.topologicalClosure

Tactic:
subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalSemiring A
s : NonUnitalStarSubalgebra R A
⊢ IsClosed (↑s.topologicalClosure : Set A)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalSemiring A
s t : NonUnitalStarSubalgebra R A
h : s ≤ t
ht : IsClosed (↑t : Set A)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalSemiring A
s t : NonUnitalStarSubalgebra R A
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : TopologicalSpace B
inst_9 : Star B
inst_10 : NonUnitalSemiring B
inst_11 : Module R B
inst_12 : IsSemitopologicalSemiring B
inst_13 : ContinuousConstSMul R B
inst_14 : ContinuousStar B
s : NonUnitalStarSubalgebra R A
φ : A →⋆ₙₐ[R] B
hφ : Continuous.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
⊢ LE.le (α := NonUnitalStarSubalgebra R B) (map φ s.topologicalClosure) (topologicalClosure (map φ s))

Tactic:
image_closure_subset_closure_image hφ

Premises used: Set.Mem, setOf, Set.Subset, closure, image_closure_subset_closure_image, Set.image, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : TopologicalSpace B
inst_9 : Star B
inst_10 : NonUnitalSemiring B
inst_11 : Module R B
inst_12 : IsSemitopologicalSemiring B
inst_13 : ContinuousConstSMul R B
inst_14 : ContinuousStar B
s : NonUnitalStarSubalgebra R A
φ : A →⋆ₙₐ[R] B
hφ : IsClosedMap.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
⊢ LE.le (α := NonUnitalStarSubalgebra R B) (topologicalClosure (map φ s)) (map φ s.topologicalClosure)

Tactic:
hφ.closure_image_subset _

Premises used: IsClosedMap.closure_image_subset, Set.Mem, setOf, Set.Subset, closure, Set.image, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : TopologicalSpace A
inst_2 : Star A
inst_3 : NonUnitalSemiring A
inst_4 : Module R A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalSemiring A
inst_8 : TopologicalSpace B
inst_9 : Star B
inst_10 : NonUnitalSemiring B
inst_11 : Module R B
inst_12 : IsSemitopologicalSemiring B
inst_13 : ContinuousConstSMul R B
inst_14 : ContinuousStar B
s : NonUnitalStarSubalgebra R A
φ : A →⋆ₙₐ[R] B
hφ : IsClosedMap.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
hφ' : Continuous.{u_2, u_3} (X := A) (Y := B) (⇑φ : (a : A) → B)
⊢ Eq (α := NonUnitalStarSubalgebra R B) (topologicalClosure (map φ s)) (map φ s.topologicalClosure)

Tactic:
SetLike.coe_injective <| hφ.closure_image_eq_of_continuous hφ' _

Premises used: SetLike.coe_injective, IsClosedMap.closure_image_eq_of_continuous
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_4
A : Type u_5
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TopologicalSpace A
inst_3 : NonUnitalSemiring A
inst_4 : StarRing A
inst_5 : Module R A
inst_6 : IsSemitopologicalSemiring A
inst_7 : ContinuousStar A
inst_8 : ContinuousConstSMul R A
inst_9 : IsScalarTower R A A
inst_10 : SMulCommClass R A A
inst_11 : StarModule R A
inst_12 : T2Space A
s : Set A
⊢ LE.le (α := NonUnitalStarSubalgebra R A) (topologicalClosure (adjoin R s))
    (centralizer R (↑(centralizer R s) : Set A))

Tactic:
topologicalClosure_minimal _ (adjoin_le_centralizer_centralizer R s) (Set.isClosed_centralizer _)

Premises used: NonUnitalStarSubalgebra.topologicalClosure_minimal, Set.isClosed_centralizer, NonUnitalStarAlgebra.adjoin_le_centralizer_centralizer
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Star A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsTopologicalRing A
s : NonUnitalStarSubalgebra R A
⊢ IsTopologicalRing.{u_2} ↥s

Tactic:
s.toNonUnitalSubring.instIsTopologicalRing

Premises used: NonUnitalSubring.instIsTopologicalRing, Set.Mem, NonUnitalStarSubalgebra.toNonUnitalSubring
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : TopologicalSpace A
inst_2 : NonUnitalRing A
inst_3 : Module R A
inst_4 : Star A
inst_5 : ContinuousStar A
inst_6 : ContinuousConstSMul R A
inst_7 : IsSemitopologicalRing A
s : NonUnitalStarSubalgebra R A
⊢ IsSemitopologicalRing.{u_2} ↥s

Tactic:
s.toNonUnitalSubring.instIsSemitopologicalRing

Premises used: Set.Mem, NonUnitalSubring.instIsSemitopologicalRing, NonUnitalStarSubalgebra.toNonUnitalSubring
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : TopologicalSpace A
inst_9 : IsSemitopologicalSemiring A
inst_10 : ContinuousConstSMul R A
inst_11 : ContinuousStar A
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (elemental R x) x

Tactic:
le_topologicalClosure _ <| self_mem_adjoin_singleton R x

Premises used: Set.Mem, NonUnitalStarSubalgebra.le_topologicalClosure, NonUnitalStarAlgebra.self_mem_adjoin_singleton
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : TopologicalSpace A
inst_9 : IsSemitopologicalSemiring A
inst_10 : ContinuousConstSMul R A
inst_11 : ContinuousStar A
x : A
⊢ Membership.mem (γ := NonUnitalStarSubalgebra R A) (elemental R x) (star x)

Tactic:
le_topologicalClosure _ <| star_self_mem_adjoin_singleton R x

Premises used: Set.Mem, NonUnitalStarSubalgebra.le_topologicalClosure, NonUnitalStarAlgebra.star_self_mem_adjoin_singleton
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : TopologicalSpace A
inst_9 : IsSemitopologicalSemiring A
inst_10 : ContinuousConstSMul R A
inst_11 : ContinuousStar A
x : A
s : NonUnitalStarSubalgebra R A
hs : IsClosed (↑s : Set A)
hx : x ∈ s
⊢ {x} ⊆ (↑s : Set A)

Tactic:
simpa using hx
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : TopologicalSpace A
inst_9 : IsSemitopologicalSemiring A
inst_10 : ContinuousConstSMul R A
inst_11 : ContinuousStar A
x : A
s : NonUnitalStarSubalgebra R A
hs : IsClosed (↑s : Set A)
⊢ elemental R x ≤ s ↔ x ∈ s

Tactic:
⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

Premises used: NonUnitalStarAlgebra.elemental.self_mem, Iff.intro, NonUnitalStarAlgebra.elemental.le_of_mem
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : TopologicalSpace A
inst_9 : IsSemitopologicalSemiring A
inst_10 : ContinuousConstSMul R A
inst_11 : ContinuousStar A
x : A
⊢ IsClosed (↑(elemental R x) : Set A)

Tactic:
isClosed_topologicalClosure _

Premises used: NonUnitalStarSubalgebra.isClosed_topologicalClosure
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A_1 : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A_1
inst_3 : StarRing A_1
inst_4 : Module R A_1
inst_5 : IsScalarTower R A_1 A_1
inst_6 : SMulCommClass R A_1 A_1
inst_7 : StarModule R A_1
inst_8 : TopologicalSpace A_1
inst_9 : IsSemitopologicalSemiring A_1
inst_10 : ContinuousConstSMul R A_1
inst_11 : ContinuousStar A_1
A : Type u_3
inst_12 : UniformSpace A
inst_13 : CompleteSpace A
inst_14 : NonUnitalSemiring A
inst_15 : StarRing A
inst_16 : IsSemitopologicalSemiring A
inst_17 : ContinuousStar A
inst_18 : Module R A
inst_19 : IsScalarTower R A A
inst_20 : SMulCommClass R A A
inst_21 : StarModule R A
inst_22 : ContinuousConstSMul R A
x : A
⊢ CompleteSpace.{u_3} ↥(elemental R x)

Tactic:
isClosed_closure.completeSpace_coe

Premises used: Set.Mem, setOf, closure, IsClosed.completeSpace_coe, Set.sInter
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : TopologicalSpace A
inst_9 : IsSemitopologicalSemiring A
inst_10 : ContinuousConstSMul R A
inst_11 : ContinuousStar A
x : A
⊢ IsClosed.{u_2} (X := A)
    (Set.range (ι := ↥(elemental R x))
      (Subtype.val (p := fun (x_1 : A) ↦ Membership.mem (γ := NonUnitalStarSubalgebra R A) (elemental R x) x_1)))

Tactic:
simpa using isClosed R x

Premises used: NonUnitalStarAlgebra.elemental.isClosed
-- Module: Mathlib.Topology.Algebra.NonUnitalStarAlgebra
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : NonUnitalSemiring A
inst_3 : StarRing A
inst_4 : Module R A
inst_5 : IsScalarTower R A A
inst_6 : SMulCommClass R A A
inst_7 : StarModule R A
inst_8 : TopologicalSpace A
inst_9 : IsSemitopologicalSemiring A
inst_10 : ContinuousConstSMul R A
inst_11 : ContinuousStar A
inst_12 : T2Space A
x : A
⊢ LE.le (α := NonUnitalStarSubalgebra R A) (elemental R x) (centralizer R (↑(centralizer R {x}) : Set A))

Tactic:
topologicalClosure_adjoin_le_centralizer_centralizer ..

Premises used: NonUnitalStarSubalgebra.topologicalClosure_adjoin_le_centralizer_centralizer, Set.Mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
this : ∀ (i j : ℕ), ∃ (k : ℕ), I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
⊢ ∀ (i j : ℕ),
    ∃ (k : ℕ),
      HSMul.hSMul (β := Ideal R) (I ^ k) ⊤ ≤ HSMul.hSMul (β := Ideal R) (I ^ i) ⊤ ⊓ HSMul.hSMul (β := Ideal R) (I ^ j) ⊤

Tactic:
simpa only [smul_eq_mul, mul_top, Algebra.algebraMap_self, map_id, le_inf_iff] using this

Premises used: Algebra.algebraMap_self, Ideal.map_id, le_inf_iff, smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
suffices : ∀ (i j : ℕ), ∃ (k : ℕ), I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j
⊢ ∀ (i j : ℕ),
    ∃ (k : ℕ),
      HSMul.hSMul (β := Ideal R) (I ^ k) ⊤ ≤ HSMul.hSMul (β := Ideal R) (I ^ i) ⊤ ⊓ HSMul.hSMul (β := Ideal R) (I ^ j) ⊤

Tactic:
suffices ∀ i j : ℕ, ∃ k, I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j by
        simpa only [smul_eq_mul, mul_top, Algebra.algebraMap_self, map_id, le_inf_iff] using this
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
i j : ℕ
⊢ ∃ (k : ℕ), I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j

Tactic:
⟨max i j, pow_le_pow_right (le_max_left i j), pow_le_pow_right (le_max_right i j)⟩

Premises used: le_max_right, Ideal.pow_le_pow_right, Max.max, And.intro, Exists.intro, le_max_left
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
i j : ℕ
⊢ ∃ (k : ℕ), I ^ k ≤ I ^ i ∧ I ^ k ≤ I ^ j

Tactic:
exact ⟨max i j, pow_le_pow_right (le_max_left i j), pow_le_pow_right (le_max_right i j)⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
this : ∀ (a : R) (i : ℕ), ∃ (j : ℕ), a • I ^ j ≤ I ^ i
⊢ ∀ (a : R) (i : ℕ), ∃ (j : ℕ), a • HSMul.hSMul (β := Ideal R) (I ^ j) ⊤ ≤ HSMul.hSMul (β := Ideal R) (I ^ i) ⊤

Tactic:
simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using this

Premises used: Ideal.smul_top_eq_map, Algebra.algebraMap_self, Ideal.map_id
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
suffices : ∀ (a : R) (i : ℕ), ∃ (j : ℕ), a • I ^ j ≤ I ^ i
⊢ ∀ (a : R) (i : ℕ), ∃ (j : ℕ), a • HSMul.hSMul (β := Ideal R) (I ^ j) ⊤ ≤ HSMul.hSMul (β := Ideal R) (I ^ i) ⊤

Tactic:
suffices ∀ (a : R) (i : ℕ), ∃ j : ℕ, a • I ^ j ≤ I ^ i by
        simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using this
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
r : R
n : ℕ
h : r • I ^ n ≤ I ^ n
⊢ ∃ (j : ℕ), r • I ^ j ≤ I ^ n

Tactic:
use n
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
r : R
n : ℕ
x : R
hx : x ∈ (↑(I ^ n) : Set R)
⊢ Membership.mem (α := R) (I ^ n) ((DistribSMul.toLinearMap R R r : (a : R) → R) x : R)

Tactic:
(I ^ n).smul_mem r hx

Premises used: Set.Mem, HPow.hPow, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
r : R
n : ℕ
x : R
hx : x ∈ (↑(I ^ n) : Set R)
⊢ Membership.mem (α := R) (I ^ n) ((DistribSMul.toLinearMap R R r : (a : R) → R) x : R)

Tactic:
exact (I ^ n).smul_mem r hx

Premises used: HPow.hPow, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
this : ∀ (i : ℕ), ∃ (j : ℕ), (↑(I ^ j) : Set R) * (↑(I ^ j) : Set R) ⊆ (↑(I ^ i) : Set R)
⊢ ∀ (i : ℕ),
    ∃ (j : ℕ),
      (↑(HSMul.hSMul (β := Ideal R) (I ^ j) ⊤) : Set R) * (↑(HSMul.hSMul (β := Ideal R) (I ^ j) ⊤) : Set R) ⊆
        (↑(HSMul.hSMul (β := Ideal R) (I ^ i) ⊤) : Set R)

Tactic:
simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using this

Premises used: Ideal.smul_top_eq_map, Algebra.algebraMap_self, Ideal.map_id
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
suffices : ∀ (i : ℕ), ∃ (j : ℕ), (↑(I ^ j) : Set R) * (↑(I ^ j) : Set R) ⊆ (↑(I ^ i) : Set R)
⊢ ∀ (i : ℕ),
    ∃ (j : ℕ),
      (↑(HSMul.hSMul (β := Ideal R) (I ^ j) ⊤) : Set R) * (↑(HSMul.hSMul (β := Ideal R) (I ^ j) ⊤) : Set R) ⊆
        (↑(HSMul.hSMul (β := Ideal R) (I ^ i) ⊤) : Set R)

Tactic:
suffices ∀ i : ℕ, ∃ j : ℕ, (↑(I ^ j) * ↑(I ^ j) : Set R) ⊆ (↑(I ^ i) : Set R) by
        simpa only [smul_top_eq_map, Algebra.algebraMap_self, map_id] using this
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
h : (↑(I ^ n) : Set R) * (↑(I ^ n) : Set R) ⊆ (↑(I ^ n) : Set R)
⊢ ∃ (j : ℕ), (↑(I ^ j) : Set R) * (↑(I ^ j) : Set R) ⊆ (↑(I ^ n) : Set R)

Tactic:
use n
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : R
_hx : x ∈ (↑(I ^ n) : Set R)
b : R
hb : b ∈ (↑(I ^ n) : Set R)
⊢ (fun (x1 x2 : R) ↦ x1 * x2) x b ∈ (↑(I ^ n) : Set R)

Tactic:
(I ^ n).smul_mem x hb

Premises used: Set.Mem, HPow.hPow, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
x : R
_hx : x ∈ (↑(I ^ n) : Set R)
b : R
hb : b ∈ (↑(I ^ n) : Set R)
⊢ (fun (x1 x2 : R) ↦ x1 * x2) x b ∈ (↑(I ^ n) : Set R)

Tactic:
exact (I ^ n).smul_mem x hb

Premises used: HPow.hPow, Submodule.smul_mem
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ NonarchimedeanRing R

Tactic:
I.adic_basis.toRing_subgroups_basis.nonarchimedean

Premises used: SubmodulesRingBasis.toRing_subgroups_basis, Set.Mem, Ideal.adic_basis, RingSubgroupsBasis.nonarchimedean
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
rw :
  (∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U) ↔
    ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U
⊢ Membership.mem (γ := Filter R) (𝓝 0) U ↔ ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U

Tactic:
rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]

Premises used: Filter.HasBasis.mem_iff, AddGroupFilterBasis.nhds_zero_hasBasis, RingFilterBasis.toAddGroupFilterBasis
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
mp :
  (∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U) →
    ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U
mpr :
  (∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U) →
    ∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U
⊢ (∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U) ↔
    ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id (↑((fun (i : ℕ) ↦ (toAddSubgroup (HSMul.hSMul (β := Ideal R) (I ^ i) ⊤) : AddSubgroup R)) i) : Set R) ⊆ U
⊢ (↑(I ^ i) : Set R) ⊆ U

Tactic:
simpa using h
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : id (↑((fun (i : ℕ) ↦ (toAddSubgroup (HSMul.hSMul (β := Ideal R) (I ^ i) ⊤) : AddSubgroup R)) i) : Set R) ⊆ U
⊢ (↑(I ^ i) : Set R) ⊆ U

Tactic:
replace h : ↑(I ^ i) ⊆ U := by simpa using h
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : (↑(I ^ i) : Set R) ⊆ U
⊢ ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U

Tactic:
⟨i, trivial, h⟩

Premises used: trivial, And.intro, Exists.intro
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : (↑(I ^ i) : Set R) ⊆ U
⊢ ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U

Tactic:
exact ⟨i, trivial, h⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : (↑(I ^ i) : Set R) ⊆ U
⊢ (↑(I ^ i) : Set R) =
    (↑((fun (i : ℕ) ↦ (toAddSubgroup (HSMul.hSMul (β := Ideal R) (I ^ i) ⊤) : AddSubgroup R)) i) : Set R)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
i : ℕ
h : (↑(I ^ i) : Set R) ⊆ U
⊢ ∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U

Tactic:
exact ⟨(I ^ i : Ideal R), ⟨i, by simp⟩, h⟩
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x : R
this : TopologicalSpace R := I.adicTopology
⊢ HasBasis.{u_1, 1} (α := R) (Filter.map (fun (y : R) ↦ x + y) (𝓝 0)) (fun (_n : ℕ) ↦ True) fun (i : ℕ) ↦
    (fun (y : R) ↦ x + y) '' (↑(I ^ i) : Set R)

Tactic:
have := I.hasBasis_nhds_zero_adic.map fun y => x + y
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x : R
this_1 : TopologicalSpace R := I.adicTopology
this :
  HasBasis.{u_1, 1} (α := R) (Filter.map (fun (y : R) ↦ x + y) (𝓝 0)) (fun (_n : ℕ) ↦ True) fun (i : ℕ) ↦
    (fun (y : R) ↦ x + y) '' (↑(I ^ i) : Set R)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (this : (𝓝 x).HasBasis (fun (_n : ℕ) ↦ True) fun (i : ℕ) ↦ (fun (y : R) ↦ x + y) '' (↑(I ^ i) : Set R)),
    (𝓝 x).HasBasis (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦ (fun (y : R) ↦ x + y) '' (↑(I ^ n) : Set R)
⊢ (𝓝 x).HasBasis (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦ (fun (y : R) ↦ x + y) '' (↑(I ^ n) : Set R)

Tactic:
rwa [map_add_left_nhds_zero x] at this

Premises used: map_add_left_nhds_zero
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ IsLinearTopology R R

Tactic:
letI := I.adicTopology
  IsLinearTopology.mk_of_hasBasis _ I.hasBasis_nhds_zero_adic

Premises used: Ideal.hasBasis_nhds_zero_adic, IsLinearTopology.mk_of_hasBasis
-- Module: Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
m : M
i : ℕ
⊢ (↑(HSMul.hSMul (β := Ideal R) (I ^ i) ⊤) : Set R) =
    (↑((fun (i : ℕ) ↦ (toAddSubgroup (HSMul.hSMul (β := Ideal R) (I ^ i) ⊤) : AddSubgroup R)) i) : Set R)

Tactic:
simp