awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Monoid (goal)
Goal:
X : Type u_6
inst : Semigroup X
inst_1 : TopologicalSpace X
inst_2 : SeparatelyContinuousMul X
x y : X
⊢ Eq (α := C(X, X)) (ContinuousMap.mulLeft (x * y)) (comp (ContinuousMap.mulLeft x) (ContinuousMap.mulLeft y))
have h : ∀ (a : X),
  Eq (α := X) ((ContinuousMap.mulLeft (x * y) : (a : X) → X) a : X)
    ((comp (ContinuousMap.mulLeft x) (ContinuousMap.mulLeft y) : (a : X) → X) a : X)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_5
N : Type u_6
α : Type u_7
inst : Monoid N
inst_1 : SMul M N
inst_2 : MulAction N α
inst_3 : SMul M α
inst_4 : IsScalarTower M N α
inst_5 : TopologicalSpace M
inst_6 : TopologicalSpace N
inst_7 : TopologicalSpace α
inst_8 : ContinuousSMul M N
inst_9 : ContinuousSMul N α
⊢ Continuous[instTopologicalSpaceProd, inst_7] fun (p : M × α) ↦ p.1 • p.2
have suffices : Continuous[instTopologicalSpaceProd, inst_7] fun (p : M × α) ↦ HSMul.hSMul (β := N) p.1 1 • p.2
Tactic: suffices Continuous (fun p : M × α ↦ (p.1 • (1 : N)) • p.2) by simpa
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Semiring R
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module R β
inst_6 : TopologicalSpace R
inst_7 : LinearMapClass F R α β
tβ : TopologicalSpace β
inst_8 : ContinuousSMul R β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ ContinuousSMul R α
have refine : Continuous[instTopologicalSpaceProd, tβ] (Function.comp (β := α) (⇑f : (a : α) → β) fun (p : R × α) ↦ p.1 • p.2)
Tactic: refine ⟨continuous_induced_rng.2 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst : FunLike F α β
inst_1 : Semiring R
inst_2 : AddCommMonoid α
inst_3 : AddCommMonoid β
inst_4 : Module R α
inst_5 : Module R β
inst_6 : TopologicalSpace R
inst_7 : LinearMapClass F R α β
tβ : TopologicalSpace β
inst_8 : ContinuousSMul R β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f : (a : α) → β) tβ
⊢ Continuous[instTopologicalSpaceProd, tβ] (Function.comp (β := α) (⇑f : (a : α) → β) fun (p : R × α) ↦ p.1 • p.2)
have simp : Continuous[instTopologicalSpaceProd, tβ] fun (x : R × α) ↦ HSMul.hSMul (β := β) x.1 ((f : (a : α) → β) x.2 : β)
Tactic: simp only [Function.comp_def, map_smul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
α : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : SMul M X
inst_4 : ContinuousSMul M X
f : Y → M
g : Y → X
b : Y
s : Set Y
inst_5 : SMul.{u_1, u_2} Mᵐᵒᵖ X
inst_6 : IsCentralScalar M X
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : Prod.{u_1, u_2} Mᵐᵒᵖ X) ↦ p.1 • p.2
have suffices : Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × X) ↦ MulOpposite.op p.1 • p.2
Tactic: suffices Continuous fun p : M × X => MulOpposite.op p.fst • p.snd from
      this.comp (MulOpposite.continuous_unop.prodMap continuous_id)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : SMul M X
inst_3 : ContinuousSMul M X
k : Set M
u : Set X
hk : IsCompact k
hu : IsCompact u
⊢ IsCompact (k • u)
have rw : IsCompact.{u_2} (X := X) ((fun (x : M × X) ↦ x.1 • x.2) '' k ×ˢ u)
Tactic: rw [← Set.image_smul_prod]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
⊢ ContinuousSMul M X ↔ ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
have refine : ∀ (h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)),
  Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × X) ↦ p.1 • p.2
Tactic: refine ⟨fun _ _ ↦ stabilizer_isOpen .., fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : M × X) ↦ p.1 • p.2
have rw : ∀ (b : X), Continuous[inst, inst_1] fun (x : M) ↦ (x, b).1 • (x, b).2
Tactic: rw [continuous_prod_of_discrete_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y : X
⊢ Continuous[inst, inst_1] fun (x : M) ↦ (x, y).1 • (x, y).2
have rw : ∀ (b : X), IsOpen[inst] (Set.preimage (β := X) (fun (x : M) ↦ (x, y).1 • (x, y).2) {b})
Tactic: rw [continuous_discrete_rng]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
⊢ IsOpen[inst] U
have pos : ∀ (hU' : U ≠ ∅), IsOpen[inst] U
Tactic: by_cases hU' : U ≠ ∅
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
pos : ∀ (hU' : U ≠ ∅), IsOpen[inst] U
⊢ IsOpen[inst] U
have neg : ∀ (hU' : ¬U ≠ ∅), IsOpen[inst] U
Tactic: by_cases hU' : U ≠ ∅
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : U ≠ ∅
⊢ IsOpen[inst] U
have pos : ∀ (m : M) (hm : m • y = x), IsOpen[inst] U
Tactic: obtain ⟨m, (hm : m • y = x)⟩ := Set.nonempty_iff_empty_ne.mpr hU'.symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
⊢ IsOpen[inst] U
have h₁ : U = (fun (m' : M) ↦ m' * m⁻¹) ⁻¹' (↑(MulAction.stabilizer M x) : Set M)
Tactic: convert! (h x).preimage (by fun_prop : Continuous fun m' : M ↦ m' * m⁻¹)
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
hU' : U ≠ ∅
m : M
hm : m • y = x
⊢ U = (fun (m' : M) ↦ m' * m⁻¹) ⁻¹' (↑(MulAction.stabilizer M x) : Set M)
have h₁ : ∀ (x_1 : M),
  x_1 ∈ U ↔ Membership.mem (γ := Set M) ((fun (m' : M) ↦ m' * m⁻¹) ⁻¹' (↑(MulAction.stabilizer M x) : Set M)) x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (hypothesis)
Goal:
M : Type u_1
X : Type u_2
inst : TopologicalSpace M
inst_1 : TopologicalSpace X
inst_2 : Group M
inst_3 : IsTopologicalGroup M
inst_4 : MulAction M X
inst_5 : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst] (↑(MulAction.stabilizer M x) : Set M)
y x : X
U : Set M := {m' : M | m' • y = x}
⊢ IsOpen[inst] (Set.preimage (β := X) (fun (x : M) ↦ (x, y).1 • (x, y).2) {x})
have hU : IsOpen[inst] U
Tactic: have hU : IsOpen U := by
    by_cases hU' : U ≠ ∅
    · obtain ⟨m, (hm : m • y = x)⟩ := Set.nonempty_iff_empty_ne.mpr hU'.symm
      convert! (h x).preimage (by fun_prop : Continuous fun m' : M ↦ m' * m⁻¹)
      ext; simp [← smul_smul, U, eq_inv_smul_iff.mpr hm]
    simp_all
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s = univ
have refine : ∀ (x : X), x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s
Tactic: refine Set.eq_univ_of_forall fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (hypothesis)
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
⊢ x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s
have this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
Tactic: have : Tendsto (· • x) (𝓝 (0 : G₀)) (𝓝 0) :=
    zero_smul G₀ x ▸ tendsto_id.smul tendsto_const_nhds
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
⊢ x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s
have rcases : ∀ (c : G₀) (hc₀ : Membership.mem (γ := Set G₀) {0}ᶜ c)
  (hc : Membership.mem (γ := Set G₀) ((fun (x_1 : G₀) ↦ x_1 • x) ⁻¹' s) c),
  x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s
Tactic: rcases Filter.nonempty_of_mem (inter_mem_nhdsWithin {0}ᶜ <| mem_map.1 <| this hs)
    with ⟨c, hc₀, hc⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (hypothesis)
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
c : G₀
hc₀ : Membership.mem (γ := Set G₀) {0}ᶜ c
hc : Membership.mem (γ := Set G₀) ((fun (x_1 : G₀) ↦ x_1 • x) ⁻¹' s) c
⊢ x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s
have hc₁ : ¬c = 0
Tactic: simp only [mem_compl_iff, mem_singleton_iff] at hc₀
Cleared hypotheses: hc₀
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
s : Set X
hs : Membership.mem (γ := Filter X) (𝓝 0) s
x : X
this : Tendsto.{u_5, u_6} (β := X) (fun (x_1 : G₀) ↦ x_1 • x) (𝓝 0) (𝓝 0)
c : G₀
hc : Membership.mem (γ := Set G₀) ((fun (x_1 : G₀) ↦ x_1 • x) ⁻¹' s) c
hc₀ : ¬c = 0
⊢ x ∈ HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) univ s
have simp : ∃ (x_1 : G₀), ∃ y ∈ s, x_1 • y = x
Tactic: simp only [mem_smul, mem_univ, true_and]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
G₀ : Type u_5
X : Type u_6
inst : GroupWithZero G₀
inst_1 : Zero X
inst_2 : MulActionWithZero G₀ X
inst_3 : TopologicalSpace G₀
inst_4 : NeBot (α := G₀) (𝓝[≠] 0)
inst_5 : TopologicalSpace X
inst_6 : ContinuousSMul G₀ X
⊢ HSMul.hSMul.{u_5, u_6, u_6} (α := Filter G₀) (β := Filter X) ⊤ (𝓝 0) = ⊤
have rw : ∀ (i : Unit × Set X),
  True ∧ Membership.mem (γ := Filter X) (𝓝 0) i.2 →
    HSMul.hSMul.{u_5, u_6, u_6} (α := Set G₀) Set.univ (id i.2) = Set.univ
Tactic: rw [(hasBasis_top.smul (basis_sets _)).eq_top_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
ts : Set (TopologicalSpace X)
h : ∀ t ∈ ts, ContinuousSMul M X
x : TopologicalSpace X := sInf ts
⊢ Continuous[instTopologicalSpaceProd, sInf ts] fun (p : M × X) ↦ p.1 • p.2
have rw : Continuous[instTopologicalSpaceProd, sInf ts] fun (p : M × X) ↦ p.1 • p.2
Tactic: rw [← (sInf_singleton (a := ‹TopologicalSpace M›) :)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
⊢ ContinuousSMul M X
have rw : ContinuousSMul M X
Tactic: rw [inf_eq_iInf]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
⊢ ContinuousSMul M X
have refine : ∀ (b : Bool), ContinuousSMul M X
Tactic: refine continuousSMul_iInf fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
b : Bool
⊢ ContinuousSMul M X
have false : ContinuousSMul M X
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
Goal:
M : Type u_2
X : Type u_3
inst : TopologicalSpace M
inst_1 : SMul M X
t₁ t₂ : TopologicalSpace X
inst_2 : ContinuousSMul M X
inst_3 : ContinuousSMul M X
b : Bool
false : ContinuousSMul M X
⊢ ContinuousSMul M X
have true : ContinuousSMul M X
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
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
⊢ IsPreconnected.{u_2} (α := P) Set.univ
have h : 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: convert!
        isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
          (continuous_id.vadd continuous_const).continuousOn
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
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
⊢ 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)
have 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))
Tactic: rw [Set.image_univ, Equiv.range_eq_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.MulAction (goal)
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))
⊢ 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)
have h₁ : Eq.{u_2 + 1} (α := Set P) Set.univ Set.univ
Tactic: rw [Set.image_univ, Equiv.range_eq_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ ∀ (i j : ℕ),
    ∃ (k : ℕ),
      HSMul.hSMul (β := Ideal R) (I ^ k) ⊤ ≤ HSMul.hSMul (β := Ideal R) (I ^ i) ⊤ ⊓ HSMul.hSMul (β := Ideal R) (I ^ j) ⊤
have suffices : ∀ (i j : ℕ), ∃ (k : ℕ), I ^ k ≤ I ^ i ∧ I ^ k ≤ 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
⊢ ∀ (a : R) (i : ℕ), ∃ (j : ℕ), a • HSMul.hSMul (β := Ideal R) (I ^ j) ⊤ ≤ HSMul.hSMul (β := Ideal R) (I ^ i) ⊤
have suffices : ∀ (a : R) (i : ℕ), ∃ (j : ℕ), a • I ^ j ≤ 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
r : R
n : ℕ
⊢ ∃ (j : ℕ), r • I ^ j ≤ I ^ n
have h : r • I ^ n ≤ I ^ n
Tactic: use n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal 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)
have suffices : ∀ (i : ℕ), ∃ (j : ℕ), (↑(I ^ j) : Set R) * (↑(I ^ j) : Set 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
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
n : ℕ
⊢ ∃ (j : ℕ), (↑(I ^ j) : Set R) * (↑(I ^ j) : Set R) ⊆ (↑(I ^ n) : Set R)
have h : (↑(I ^ n) : Set R) * (↑(I ^ n) : Set R) ⊆ (↑(I ^ n) : Set R)
Tactic: use n
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
⊢ Membership.mem (γ := Filter R) (𝓝 0) U ↔ ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U
have rw : (∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U) ↔
  ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U
Tactic: rw [I.ringFilterBasis.toAddGroupFilterBasis.nhds_zero_hasBasis.mem_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
U : Set R
⊢ (∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U) ↔
    ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U
have mp : (∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U) →
  ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
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
⊢ (∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U) ↔
    ∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U
have mpr : (∃ (i : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U) →
  ∃ (i : Set R), Membership.mem (γ := AddGroupFilterBasis R) RingFilterBasis.toAddGroupFilterBasis i ∧ id i ⊆ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (hypothesis)
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 : ℕ), True ∧ (↑(I ^ i) : Set R) ⊆ U
have h₁ : (↑(I ^ i) : Set R) ⊆ U
Tactic: replace h : ↑(I ^ i) ⊆ U := by simpa using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
x : R
this : TopologicalSpace R := I.adicTopology
⊢ (𝓝 x).HasBasis (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦ (fun (y : R) ↦ x + y) '' (↑(I ^ n) : Set R)
have 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)
Tactic: have := I.hasBasis_nhds_zero_adic.map fun y => x + y
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
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)
⊢ (𝓝 x).HasBasis (fun (_n : ℕ) ↦ True) fun (n : ℕ) ↦ (fun (y : R) ↦ x + y) '' (↑(I ^ n) : Set R)
have 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)
Tactic: rwa [map_add_left_nhds_zero x] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (hypothesis)
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 : ℕ
a : R
a_in : a ∈ (↑(HSMul.hSMul (β := Ideal R) (I ^ i) ⊤) : Set R)
⊢ Membership.mem (γ := Set R) ((fun (x : R) ↦ x • m) ⁻¹' (↑(HSMul.hSMul (β := Submodule R M) (I ^ i) ⊤) : Set M)) a
have a_in₁ : a ∈ I ^ i
Tactic: replace a_in : a ∈ I ^ i := by simpa [(I ^ i).mul_top] using a_in
Cleared hypotheses: a_in
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
this : TopologicalSpace R := I.adicTopology
⊢ OpenAddSubgroup R
have refine : IsOpen[I.adicTopology]
  (AddSubsemigroup.carrier
    (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (toAddSubgroup (I ^ n))) : AddSubsemigroup R))
Tactic: refine ⟨(I ^ n).toAddSubgroup, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
this : TopologicalSpace R := I.adicTopology
⊢ IsOpen[I.adicTopology]
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (toAddSubgroup (I ^ n))) : AddSubsemigroup R))
have h : AddSubsemigroup.carrier
    (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (toAddSubgroup (I ^ n))) : AddSubsemigroup R) =
  (↑(sorry.openAddSubgroup n) : Set R)
Tactic: convert! (I.adic_basis.toRing_subgroups_basis.openAddSubgroup n).isOpen
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
I : Ideal R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
this : TopologicalSpace R := I.adicTopology
⊢ AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (AddSubgroup.toAddSubmonoid (toAddSubgroup (I ^ n))) : AddSubsemigroup R) =
    (↑(⋯.openAddSubgroup n) : Set R)
have h : (↑(I ^ n) : Set R) = (↑(HSMul.hSMul (β := Ideal R) (I ^ n) ⊤) : Set R)
Tactic: change (↑(I ^ n) : Set R) = ↑(I ^ n • (⊤ : Ideal R))
-- Lean 4 proof step from Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology (goal)
Goal:
R : Type u_1
inst : CommRing R
top : TopologicalSpace R
inst_1 : IsTopologicalRing R
J : Ideal R
⊢ IsAdic J ↔
    (∀ (n : ℕ), IsOpen[top] (↑(J ^ n) : Set R)) ∧
      ∀ (s : Set R), Membership.mem (γ := Filter R) (𝓝 0) s → ∃ (n : ℕ), (↑(J ^ n) : Set R) ⊆ s
have mp : IsAdic J →
  (∀ (n : ℕ), IsOpen[top] (↑(J ^ n) : Set R)) ∧
    ∀ (s : Set R), Membership.mem (γ := Filter R) (𝓝 0) s → ∃ (n : ℕ), (↑(J ^ n) : Set R) ⊆ s
Tactic: constructor