mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ TopologicalSpace.induced (⇑e.symm.toHomeomorph) inst =
    TopologicalSpace.induced (fun x1 x2 ↦ (B' x1) x2) Pi.topologicalSpace

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ TopologicalSpace.induced (⇑e.symm.toHomeomorph) inst =
    TopologicalSpace.induced (fun x1 x2 ↦ (B' x1) x2) Pi.topologicalSpace
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
⊢ 𝓝 1 ≤
    Filter.map (⇑(Units.coeHom R))
      (Filter.comap (⇑(Units.embedProduct R)) (𝓝 ((Units.embedProduct R) 1).1 ×ˢ 𝓝 ((Units.embedProduct R) 1).2))

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
⊢ 𝓝 1 ≤
    Filter.map (⇑(Units.coeHom R))
      (Filter.comap (⇑(Units.embedProduct R)) (𝓝 ((Units.embedProduct R) 1).1 ×ˢ 𝓝 ((Units.embedProduct R) 1).2))
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ ∑' (c : ↑(mulFiber x)), (L (f (↑((mulFiber_swapEquiv x) c)).1)) (g (↑((mulFiber_swapEquiv x) c)).2) =
    ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)

Tactic:
]

Goal state after:
M : Type u_1
S : Type u_2
E : Type u_3
inst✝⁴ : CommMonoid M
inst✝³ : CommSemiring S
inst✝² : AddCommMonoid E
inst✝¹ : Module S E
inst✝ : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL : ∀ (x y : E), (L x) y = (L y) x
x : M
⊢ ∑' (c : ↑(mulFiber x)), (L (f (↑((mulFiber_swapEquiv x) c)).1)) (g (↑((mulFiber_swapEquiv x) c)).2) =
    ∑' (ab : ↑(mulFiber x)), (L (g (↑ab).1)) (f (↑ab).2)
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ ⨅ y, ?m.355 y =
    ⨅ i,
      TopologicalSpace.induced (fun x ↦ ((((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B) x) i) inferInstance

pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ ∀ (x : F),
    ?m.355 (f.toEquiv x) = TopologicalSpace.induced (fun x_1 ↦ ((fun x1 x2 ↦ (B x1) x2) ∘ ⇑e.symm) x_1 x) inferInstance

pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ F' → TopologicalSpace E'

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ ∀ (x : F),
    TopologicalSpace.induced (fun x_1 ↦ ((((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B) x_1) (f.toEquiv x))
        inferInstance =
      TopologicalSpace.induced (fun x_1 ↦ ((fun x1 x2 ↦ (B x1) x2) ∘ ⇑e.symm) x_1 x) inferInstance
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
⊢ ∃ i, True ∧ (fun y ↦ 1 + y) '' ↑(I ^ i) ⊆ s

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
⊢ ∃ i, True ∧ (fun y ↦ 1 + y) '' ↑(I ^ i) ⊆ s
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ (fun y ↦ 1 + y) x ∈ s

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ (fun y ↦ 1 + y) x ∈ s
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ((fun x1 x2 ↦ (B x1) x2) ∘ fun p ↦ p.1 + p.2)

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousAdd 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ((fun x1 x2 ↦ (B x1) x2) ∘ fun p ↦ p.1 + p.2)
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
⊢ 1 ≤ 1

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousSMul 𝕜 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ((fun x1 x2 ↦ (B x1) x2) ∘ fun p ↦ p.1 • p.2)

Tactic:
]

Goal state after:
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁶ : CommSemiring 𝕜
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝ : ContinuousSMul 𝕜 𝕜
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ Continuous[instTopologicalSpaceProd, Pi.topologicalSpace] ((fun x1 x2 ↦ (B x1) x2) ∘ fun p ↦ p.1 • p.2)
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_7
E : Type u_8
F : Type u_9
inst✝⁷ : CommRing 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd 𝕜
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ ∀ (i : F),
    Continuous[TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace, inst✝⁶] fun a ↦
      ((fun x1 x2 ↦ (B x1) x2) ∘ fun a ↦ -a) a i

Tactic:
]

Goal state after:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
inst✝⁷ : CommRing 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommGroup F
inst✝² : Module 𝕜 F
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousAdd 𝕜
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
t₁ : TopologicalSpace E := TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace
this : B.IsWeak
⊢ ∀ (i : F),
    Continuous[TopologicalSpace.induced (fun x1 x2 ↦ (B x1) x2) Pi.topologicalSpace, inst✝⁶] fun a ↦
      ((fun x1 x2 ↦ (B x1) x2) ∘ fun a ↦ -a) a i
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ -1 + ↑this.unit⁻¹ = -1 + ↑this.unit⁻¹

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
this : c ^ k • w ∈ V
⊢ c ^ k • w ∈ V

Tactic:
]

Goal state after:
𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
c : 𝕜₁
hc₀ : 0 < ‖c‖
hc₁ : ‖c‖ < 1
c_ne : c ≠ 0
cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V
basis_𝓕₂ : 𝓕₂.HasBasis (fun s ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id
W : Set E
hW : id W ∩ V ⊆ c • V
W_mem_𝓕₂ : W ∈ 𝓕₂
W_bal : Balanced 𝕜₁ W
w : E
w_in_W : w ∈ W
n : ℕ
hn : c ^ n • w ∈ V
k : ℕ
h✝ : k < n
hk : c ^ (k + 1) • w ∈ V
this : c ^ k • w ∈ V
⊢ c ^ k • w ∈ V
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝² :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝¹ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this✝ : IsUnit (1 + x)
this : -1 + ↑this✝.unit⁻¹ = -↑this✝.unit⁻¹ * x
⊢ -↑this✝.unit⁻¹ * x ∈ I ^ n

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝² :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝¹ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this✝ : IsUnit (1 + x)
this : -1 + ↑this✝.unit⁻¹ = -↑this✝.unit⁻¹ * x
⊢ -↑this✝.unit⁻¹ * x ∈ I ^ n
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
E : Type u_3
inst✝⁶ : NontriviallyNormedField 𝕜₁
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜₁ E
t₁ t₂ : TopologicalSpace E
inst✝³ : IsTopologicalAddGroup E
inst✝² : IsTopologicalAddGroup E
inst✝¹ : ContinuousSMul 𝕜₁ E
inst✝ : ContinuousSMul 𝕜₁ E
V : Set E
V_mem : V ∈ 𝓝 0
H : TopologicalSpace.induced Subtype.val t₁ = TopologicalSpace.induced Subtype.val t₂
o : ↑V := ⟨0, ⋯⟩
⊢ map Subtype.val (𝓝 o) = map Subtype.val (𝓝 o)

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
⊢ inst✝⁶ = TopologicalSpace.induced (⇑f) inst✝⁵

Tactic:
]

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
⊢ inst✝⁶ = TopologicalSpace.induced (⇑f) inst✝⁵
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsInducing (V.domRestrict ⇑f)
this✝ : IsTopologicalAddGroup E
this : ContinuousSMul 𝕜₁ E
⊢ instTopologicalSpaceSubtype = instTopologicalSpaceSubtype

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
⊢ ∀ x ∈ f.ker, x = 0

Tactic:
]

Goal state after:
𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
⊢ ∀ x ∈ f.ker, x = 0
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
f_injOn : InjOn (⇑f) V
x : E
hx : x ∈ f.ker
c : 𝕜₁
hc : c • x ∈ V
c_ne : c ≠ 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Goal state before:
pp: case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ ↑V
hsb : b⁻¹ * s ∈ ↑V
⊢ False

Tactic:
]

Goal state after:
case h
G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
a b : G
h : a ≠ b
u v : Set G
left✝ : IsOpen u
open_v : IsOpen v
mem_u : a⁻¹ * b ∈ u
mem_v : 1 ∈ v
dis : Disjoint u v
V : OpenSubgroup G
hV : ↑V ⊆ v
x : Set G
mem_aV : x ⊆ a • ↑V
mem_bV : x ⊆ b • ↑V
s : G
hs : s ∈ x
hsa : a⁻¹ * s ∈ ↑V
hsb : b⁻¹ * s ∈ ↑V
⊢ False
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑(x * x)).arg| < π / 2 ^ (n + 1)
⊢ |(↑x).arg| < π / 2 ^ (n + 1 + 1)

Tactic:
]

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑(x * x)).arg| < π / 2 ^ (n + 1)
⊢ |(↑x).arg| < π / 2 ^ (n + 1 + 1)