mathlib-initiative/mathlib-tactics huggingface dataset:
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 : 𝓝 0 ⊓ 𝓟 V = 𝓝 0 ⊓ 𝓟 V
⊢ t₁ = t₂

Tactic:
classical
  -- For `i = 1, 2`, denote by `𝓕ᵢ` the filter of neighborhoods of `0` for the topology `tᵢ`.
  set 𝓕₁ := @nhds E t₁ 0
  set 𝓕₂ := @nhds E t₂ 0
  -- Note that, because `V ∈ 𝓕₁`, `H` may be rewritten as `𝓕₁ = 𝓕₂ ⊓ 𝓟 V`.
  replace H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V := by simpa [← H]
  -- Because both `t₁` and `t₂` are additive group topologies, it is enough to show `𝓕₁ = 𝓕₂`.
  suffices 𝓕₁ = 𝓕₂ by rwa [IsTopologicalAddGroup.ext_iff] <;> infer_instance
  -- If we can show that `V ∈ 𝓕₂` we are done, because then `𝓕₁ = 𝓕₂ ⊓ 𝓟 V = 𝓕₂`.
  suffices V ∈ 𝓕₂ by simpa [H]
  -- Hence, let us show that `V ∈ 𝓕₂`. Fix a scalar `c` with `0 < ‖c‖ < 1`.
  obtain ⟨c, hc₀, hc₁⟩ := NormedField.exists_norm_lt_one 𝕜₁
  have c_ne : c ≠ 0 := norm_pos_iff.mp hc₀
  -- We know that `c • V ∈ 𝓕₁ = 𝓕₂ ⊓ 𝓟 V`.
  have cV_mem : c • V ∈ 𝓕₂ ⊓ 𝓟 V := by
    simpa [← H, 𝓕₁, set_smul_mem_nhds_zero_iff c_ne]
  -- Furthermore, we know that `𝓕₂` has a basis of balanced sets
  have basis_𝓕₂ : HasBasis 𝓕₂ (fun (s : Set E) ↦ s ∈ 𝓕₂ ∧ Balanced 𝕜₁ s) id :=
    let := t₂; nhds_basis_balanced 𝕜₁ E
  -- Hence, we get a balanced set `W ∈ 𝓕₂` such that `W ∩ V ⊆ c • V`.
  obtain ⟨W, ⟨W_mem_𝓕₂, W_bal⟩, hW⟩ := basis_𝓕₂.inf_principal V |>.mem_iff.mp cV_mem
  -- We claim that `W ⊆ V`. This will conclude the proof, since `W ∈ 𝓕₂`.
  suffices W ⊆ V from mem_of_superset W_mem_𝓕₂ this
  -- Let `w ∈ W` be arbitrary.
  intro w w_in_W
  -- Because `V` is a `t₁`-neighborhood of `0`, we have `c ^ n • w ∈ V` for some natural number `n`.
  obtain ⟨n, hn⟩ : ∃ n : ℕ, c ^ n • w ∈ V :=
    let := t₁
    tendsto_pow_atTop_nhds_zero_of_norm_lt_one hc₁ |>.zero_smul_const w
      |>.eventually_mem V_mem |>.exists
  -- We will conclude by reducing `c ^ n • w ∈ V` to `w = c ^ 0 • w ∈ V` inductively.
  suffices c ^ 0 • w ∈ V by simpa
  apply Nat.decreasingInduction (motive := fun (k : ℕ) _ ↦ c^k • w ∈ V) ?_ hn n.zero_le
  -- To do so, we show that if `k : ℕ` is such that `c ^ (k + 1) • w ∈ V` then `c ^ k • w ∈ V`.
  intro k _ (hk : c ^ (k + 1) • w ∈ V)
  -- Indeed, because `W` is balanced, we have `c ^ (k + 1) • w ∈ W ∩ V ⊆ c • V`
  have : c ^ (k + 1) • w ∈ c • V :=
    hW ⟨W_bal.smul_mem (by grw [norm_pow, hc₁.le, one_pow]) w_in_W, hk⟩
  -- Cancelling `c`, we get `c ^ k • w ∈ V` as we claimed.
  rwa [pow_add, pow_one, mul_comm, mul_smul, smul_mem_smul_set_iff₀ c_ne V] at this

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x : WithConv (E →L[R] F)
⊢ star (star x) = x

Tactic:
ext

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x : WithConv (E →L[R] F)
x✝ : E
⊢ (star (star x)).ofConv x✝ = x.ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : InvolutiveStar R
inst✝¹² : AddCommMonoid E
inst✝¹¹ : Module R E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : StarModule R E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module R F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : StarModule R F
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : ContinuousStar E
inst✝¹ : ContinuousStar F
inst✝ : ContinuousAdd F
x y : WithConv (E →L[R] F)
⊢ star (x + y) = star x + star y

Tactic:
ext

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : InvolutiveStar R
inst✝¹² : AddCommMonoid E
inst✝¹¹ : Module R E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : StarModule R E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module R F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : StarModule R F
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : ContinuousStar E
inst✝¹ : ContinuousStar F
inst✝ : ContinuousAdd F
x y : WithConv (E →L[R] F)
x✝ : E
⊢ (star (x + y)).ofConv x✝ = (star x + star y).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : WithConv (E →L[R] F)
g : WithConv (G →L[R] E)
⊢ star (toConv (f.ofConv ∘SL g.ofConv)) = toConv ((star f).ofConv ∘SL (star g).ofConv)

Tactic:
ext

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : WithConv (E →L[R] F)
g : WithConv (G →L[R] E)
x✝ : G
⊢ (star (toConv (f.ofConv ∘SL g.ofConv))).ofConv x✝ = (toConv ((star f).ofConv ∘SL (star g).ofConv)).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : E →L[R] F
g : G →L[R] E
⊢ star (toConv (f ∘SL g)) = toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)

Tactic:
ext

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : E →L[R] F
g : G →L[R] E
x✝ : G
⊢ (star (toConv (f ∘SL g))).ofConv x✝ = (toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
inst✝³ : StarAddMonoid E
inst✝² : StarModule R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousStar E
⊢ star (toConv (ContinuousLinearMap.id R E)) = toConv (ContinuousLinearMap.id R E)

Tactic:
ext

Goal state after:
R : Type u_1
E : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
inst✝³ : StarAddMonoid E
inst✝² : StarModule R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousStar E
x✝ : E
⊢ (star (toConv (ContinuousLinearMap.id R E))).ofConv x✝ = (toConv (ContinuousLinearMap.id R E)).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
⊢ star (toConv 0) = toConv 0

Tactic:
ext

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x✝ : E
⊢ (star (toConv 0)).ofConv x✝ = (toConv 0).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousStar E
S : Type u_4
inst✝⁷ : Semiring S
inst✝⁶ : StarAddMonoid S
inst✝⁵ : StarModule S S
inst✝⁴ : Module S E
inst✝³ : StarModule S E
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousStar S
inst✝ : ContinuousSMul S E
a : E
⊢ star (toConv (toSpanSingleton S a)) = toConv (toSpanSingleton S (star a))

Tactic:
ext

Goal state after:
E : Type u_2
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousStar E
S : Type u_4
inst✝⁷ : Semiring S
inst✝⁶ : StarAddMonoid S
inst✝⁵ : StarModule S S
inst✝⁴ : Module S E
inst✝³ : StarModule S E
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousStar S
inst✝ : ContinuousSMul S E
a : E
⊢ (star (toConv (toSpanSingleton S a))).ofConv 1 = (toConv (toSpanSingleton S (star a))).ofConv 1
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : StarAddMonoid E
inst✝¹⁵ : AddCommMonoid F
inst✝¹⁴ : StarAddMonoid F
inst✝¹³ : TopologicalSpace E
inst✝¹² : TopologicalSpace F
inst✝¹¹ : ContinuousStar E
inst✝¹⁰ : ContinuousStar F
S : Type u_4
inst✝⁹ : Semiring S
inst✝⁸ : StarAddMonoid S
inst✝⁷ : StarModule S S
inst✝⁶ : Module S E
inst✝⁵ : StarModule S E
inst✝⁴ : TopologicalSpace S
inst✝³ : ContinuousStar S
inst✝² : Module S F
inst✝¹ : StarModule S F
inst✝ : ContinuousSMul S F
f : WithConv (E →L[S] S)
x : F
⊢ star (toConv (f.ofConv.smulRight x)) = toConv ((star f).ofConv.smulRight (star x))

Tactic:
ext

Goal state after:
E : Type u_2
F : Type u_3
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : StarAddMonoid E
inst✝¹⁵ : AddCommMonoid F
inst✝¹⁴ : StarAddMonoid F
inst✝¹³ : TopologicalSpace E
inst✝¹² : TopologicalSpace F
inst✝¹¹ : ContinuousStar E
inst✝¹⁰ : ContinuousStar F
S : Type u_4
inst✝⁹ : Semiring S
inst✝⁸ : StarAddMonoid S
inst✝⁷ : StarModule S S
inst✝⁶ : Module S E
inst✝⁵ : StarModule S E
inst✝⁴ : TopologicalSpace S
inst✝³ : ContinuousStar S
inst✝² : Module S F
inst✝¹ : StarModule S F
inst✝ : ContinuousSMul S F
f : WithConv (E →L[S] S)
x : F
x✝ : E
⊢ (star (toConv (f.ofConv.smulRight x))).ofConv x✝ = (toConv ((star f).ofConv.smulRight (star x))).ofConv x✝
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : InvolutiveStar R
inst✝¹³ : AddCommMonoid E
inst✝¹² : Module R E
inst✝¹¹ : StarAddMonoid E
inst✝¹⁰ : StarModule R E
inst✝⁹ : AddCommMonoid F
inst✝⁸ : Module R F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : StarModule R F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousStar E
inst✝² : ContinuousStar F
inst✝¹ : SMulCommClass R R F
inst✝ : ContinuousConstSMul R F
x✝¹ : R
x✝ : WithConv (E →L[R] F)
⊢ star (x✝¹ • x✝) = star x✝¹ • star x✝

Tactic:
ext

Goal state after:
R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : InvolutiveStar R
inst✝¹³ : AddCommMonoid E
inst✝¹² : Module R E
inst✝¹¹ : StarAddMonoid E
inst✝¹⁰ : StarModule R E
inst✝⁹ : AddCommMonoid F
inst✝⁸ : Module R F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : StarModule R F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousStar E
inst✝² : ContinuousStar F
inst✝¹ : SMulCommClass R R F
inst✝ : ContinuousConstSMul R F
x✝² : R
x✝¹ : WithConv (E →L[R] F)
x✝ : E
⊢ (star (x✝² • x✝¹)).ofConv x✝ = (star x✝² • star x✝¹).ofConv x✝
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
⊢ closure[inst✝] A = A ∪ derivedSet A

Tactic:
ext

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
x✝ : X
⊢ x✝ ∈ closure[inst✝] A ↔ x✝ ∈ A ∪ derivedSet A
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

Tactic:
constructor

Goal state after:
case mp
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

case mpr
X : Compactum
S : Set X.A
⊢ (∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S) → IsOpen Sᶜ
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
⊢ CompactSpace X.A

Tactic:
constructor

Goal state after:
X : Compactum
⊢ IsCompact Set.univ
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ basic (A ∩ B) ↔ G ∈ basic A ∩ basic B

Tactic:
constructor

Goal state after:
case mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ basic (A ∩ B) → G ∈ basic A ∩ basic B

case mpr
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
⊢ G ∈ basic A ∩ basic B → G ∈ basic (A ∩ B)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic A ∩ basic B

Tactic:
constructor

Goal state after:
case mp.left
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic A

case mp.right
X : Compactum
A B : Set X.A
G : Ultrafilter X.A
hG : G ∈ basic (A ∩ B)
⊢ G ∈ basic B
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
⊢ ι T ⊆ C1 → (⋂₀ ι T).Nonempty

Tactic:
hT

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
C0 : ssu := {Z | ∃ B ∈ F, X.str ⁻¹' B = Z}
AA : Set (Ultrafilter X.A) := {G | A ∈ G}
C1 : ssu := insert AA C0
C2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure C1
claim1 : ∀ B ∈ C0, ∀ C ∈ C0, B ∩ C ∈ C0
claim2 : ∀ B ∈ C0, B.Nonempty
claim3 : ∀ B ∈ C0, (AA ∩ B).Nonempty
claim4 : FiniteInter (finiteInterClosure C1)
claim5 : FiniteInter C0
claim6 : ∀ P ∈ C2, P.Nonempty
T : fsu
hT : ι T ⊆ C1
⊢ (⋂₀ ι T).Nonempty
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case cond
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
T0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
T1 : ssu := ⋯
T2 : Set (Set (Ultrafilter X.A)) := ⋯
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ FiniteInter T0

Tactic:
constructor

Goal state after:
case cond.univ_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
T0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
T1 : ssu := ⋯
T2 : Set (Set (Ultrafilter X.A)) := ⋯
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ ∈ T0

case cond.inter_mem
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := ⋯
ssu : Type u_1 := ⋯
ι : fsu → ssu := ⋯
T0 : ssu := ⋯
AA : Set (Ultrafilter X.A) := ⋯
T1 : ssu := ⋯
T2 : Set (Set (Ultrafilter X.A)) := ⋯
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ ∀ ⦃s : Set (Ultrafilter X.A)⦄, s ∈ T0 → ∀ ⦃t : Set (Ultrafilter X.A)⦄, t ∈ T0 → s ∩ t ∈ T0
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
⊢ Set.univ = basic Set.univ

Tactic:
ext

Goal state after:
case h
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
S : Set (Ultrafilter X.A)
hS : S ∈ T2
x✝ : Ultrafilter X.A
⊢ x✝ ∈ Set.univ ↔ x✝ ∈ basic Set.univ
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (π_app C fun x ↦ x ∈ J) x ∈ {↑a (op J)}

Tactic:
← map_comp_π_app C h,

Goal state after:
ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K✝ : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
hc : ∀ (J : Finset ι) (s : ↑(obj C fun x ↦ x ∈ J)), IsClosed (⇑(π_app C fun x ↦ x ∈ J) ⁻¹' {s})
J K : Finset ι
h : J ⊆ K
x : ↑C
hx : (π_app C fun x ↦ x ∈ K) x ∈ {↑a (op K)}
⊢ (⇑(map C h) ∘ ⇑(π_app C (Membership.mem K))) x ∈ {↑a (op J)}
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
⊢ y = x

Tactic:
ext

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : ∀ (a : I), ↑y a = ↑x a
x✝ : I
⊢ ↑y x✝ = ↑x x✝
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case false
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y ≠ x
a : I
ha : ↑y a ≠ ↑x a
hx : ↑x a = false
⊢ ∃ a ∈ factors C s x, (LocallyConstant.evalMonoidHom y) a = 0

Tactic:
rw [hx, ne_eq, Bool.not_eq_false] at ha
    refine ⟨1 - (e (π C (· ∈ s)) a), ⟨one_sub_e_mem_of_false _ _ ha hx, ?_⟩⟩
    rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply,
      LocallyConstant.coe_one, Pi.one_apply, LocallyConstant.coe_mk, if_pos ha, sub_self]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ (∀ (n : ℕ) (j : cell C n), IsClosed[t] (C ∩ closedCell n j)) ∧ IsClosed[t] (C ∩ D)

Tactic:
constructor

Goal state after:
case left
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ ∀ (n : ℕ) (j : cell C n), IsClosed[t] (C ∩ closedCell n j)

case right
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
⊢ IsClosed[t] (C ∩ D)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
T : fsu
⊢ ↑T ⊆ T1 → (⋂₀ ι T).Nonempty

Tactic:
hT

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
T0 : ssu := {S | ∃ A ∈ F, S = basic A}
AA : Set (Ultrafilter X.A) := X.str ⁻¹' {x}
T1 : ssu := insert AA T0
T2 : Set (Set (Ultrafilter X.A)) := finiteInterClosure T1
cond : ↑F ≤ 𝓝 x
claim1 : ∀ (A : Set X.A), IsClosed A → A ∈ F → x ∈ A
claim2 : ∀ A ∈ F, x ∈ cl A
claim3 : ∀ S1 ∈ T0, ∀ S2 ∈ T0, S1 ∩ S2 ∈ T0
claim4 : ∀ S ∈ T0, (AA ∩ S).Nonempty
claim5 : ∀ S ∈ T0, S.Nonempty
claim6 : ∀ S ∈ T2, S.Nonempty
T : fsu
hT : ↑T ⊆ T1
⊢ (⋂₀ ι T).Nonempty
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
⊢ cl A = closure A

Tactic:
ext

Goal state after:
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ cl A ↔ x✝ ∈ closure A
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ cl A ↔ ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝

Tactic:
constructor

Goal state after:
case mp
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ cl A → ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝

case mpr
X : Compactum
A : Set X.A
x✝ : X.A
⊢ (∃ u, A ∈ u ∧ ↑u ≤ 𝓝 x✝) → x✝ ∈ cl A