mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.cons.rel.hl
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ ∀ (x : ℝ),
    0 < basis_hd x →
      (basis_hd ^ (exp2 - exp1) * (toFun m2 basis_tl * (toFun m1 basis_tl)⁻¹)) x =
        (fun x ↦ basis_hd x ^ exp2 * toFun m2 basis_tl x / (basis_hd x ^ exp1 * toFun m1 basis_tl x)) x

Tactic:
intro x

Goal state after:
case cons.cons.cons.rel.hl
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
x : ℝ
⊢ 0 < basis_hd x →
    (basis_hd ^ (exp2 - exp1) * (toFun m2 basis_tl * (toFun m1 basis_tl)⁻¹)) x =
      (fun x ↦ basis_hd x ^ exp2 * toFun m2 basis_tl x / (basis_hd x ^ exp1 * toFun m1 basis_tl x)) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_coef : 0 < t.coef
⊢ ∀ (x : ℝ), 0 < t.unit.toFun basis x → 0 < (t.coef • t.unit.toFun basis) x

Tactic:
intro x

Goal state after:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_coef : 0 < t.coef
x : ℝ
⊢ 0 < t.unit.toFun basis x → 0 < (t.coef • t.unit.toFun basis) x
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
⊢ ∀ (x : ℚ), ¬↑x = ↑q ^ (↑a / ↑b)

Tactic:
intro x

Goal state after:
q : ℚ
a b : ℕ
h : ∀ (p : ℚ), q ^ a ≠ p ^ b
hb : 0 < b
hq : 0 ≤ q
x : ℚ
⊢ ¬↑x = ↑q ^ (↑a / ↑b)
Module: Mathlib.Tactic.NormNum.NatSqrt

Goal state before:
pp: x y r : ℕ
hr : y * y + r = x
hle : r.ble (2 * y) = true
⊢ x.sqrt = y

Tactic:
rw [← hr, ← pow_two]
  rw [two_mul] at hle
  exact Nat.sqrt_add_eq' _ (Nat.le_of_ble_eq_true hle)

Goal state after:
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a b m : ℕ
⊢ a ^ b * a ^ b * a % m = a ^ b % m * (a ^ b * a % m) % m

Tactic:
← Nat.mul_mod,

Goal state after:
a b m : ℕ
⊢ a ^ b * a ^ b * a % m = a ^ b * (a ^ b * a) % m
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
⊢ applyId ((y, z) :: xs) x = if y = x then z else applyId xs x

Tactic:
by
  simp only [List.applyId, List.dlookup, eq_rec_constant, Prod.toSigma, List.map]
  split_ifs <;> rfl

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
⊢ Injective (List.applyId (xs.zip ys))

Tactic:
intro x

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
⊢ ∀ ⦃a₂ : α⦄, List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) a₂ → x = a₂
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous fun x ↦ ⇑↑x
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U (interior W)}
h1 : T.Nonempty
h2 : T ⊆ S2
⊢ (interior S2).Nonempty

Tactic:
have h3 : IsOpen T := isOpen_induced (ContinuousMap.isOpen_setOfPred_mapsTo hU isOpen_interior)

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous fun x ↦ ⇑↑x
hS4 : IsClosed[Pi.topologicalSpace] S4
T : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U (interior W)}
h1 : T.Nonempty
h2 : T ⊆ S2
h3 : IsOpen T
⊢ (interior S2).Nonempty
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: case hc
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
n : ℕ
g : G
hg : g ∈ s
⊢ IsCompact ((fun g ↦ g • x) '' (K n ∩ g • V))

Tactic:
apply IsCompact.image ?_ (by fun_prop)

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
n : ℕ
g : G
hg : g ∈ s
⊢ IsCompact (K n ∩ g • V)
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: M : Type u_1
inst✝³ : GroupWithZero M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousInv₀ M
inst✝ : T1Space M
⊢ IsOpen[inst✝²] (Set.range Units.val)

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

Goal state after:
M : Type u_1
inst✝³ : GroupWithZero M
inst✝² : TopologicalSpace M
inst✝¹ : ContinuousInv₀ M
inst✝ : T1Space M
⊢ Set.range Units.val = {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)
⊢ Function.Injective ⇑f

Tactic:
have f_injOn : InjOn f V := injOn_iff_injective.2 H.injective

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
⊢ Function.Injective ⇑f
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:
intro x

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 : E
⊢ 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
⊢ c • x = 0

Tactic:
← f_injOn.eq_iff hc (mem_of_mem_nhds V_mem),

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 : E
hx : x ∈ f.ker
c : 𝕜₁
hc : c • x ∈ V
c_ne : c ≠ 0
⊢ f (c • x) = f 0
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⦄, x ⊆ a • ↑V → x ⊆ b • ↑V → x = ∅

Tactic:
intro x

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
⊢ x ⊆ a • ↑V → x ⊆ b • ↑V → x = ∅
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ IsOpen ↑I ↔ I ≠ ⊥

Tactic:
refine ⟨?_, IsDedekindDomain.isOpen_of_ne_bot⟩

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ IsOpen ↑I → I ≠ ⊥
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst✝¹, inst✝] f
hf2 : Function.Injective f
⊢ f '' derivedSet A ⊆ derivedSet (f '' A)

Tactic:
intro x

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous[inst✝¹, inst✝] f
hf2 : Function.Injective f
x : β
⊢ x ∈ f '' derivedSet A → x ∈ derivedSet (f '' A)
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ J m, openCell m j
⊢ ↑(map n ↑i) '' sphere 0 1 ⊆
    D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ (J m).preimage Subtype.val ⋯) m, ↑(map m ↑j) '' closedBall 0 1

Tactic:
intro x

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ J m, openCell m j
x : X
⊢ x ∈ ↑(map n ↑i) '' sphere 0 1 →
    x ∈ D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ (J m).preimage Subtype.val ⋯) m, ↑(map m ↑j) '' closedBall 0 1
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : ¬U.Nontrivial
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
· apply isPreconnected_closed_iff.mp hs
    · simp
    · simp
    · trans derivedSet U
      · apply hs.preperfect_of_nontrivial hu
      · rw [← derivedSet_union]
        exact derivedSet_mono _ _ h
    · exact ha
    · exact hb

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : ¬U.Nontrivial
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
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
h : ∀ (i : ι), J i → K i
x✝ : (i : ↑K) → X ↑i
hx : x✝ ∈ obj C K
⊢ (precomp (Set.inclusion h)) x✝ ∈ obj C J

Tactic:
obtain ⟨y, hy⟩ := hx
    rw [← hy.2]
    exact ⟨y, hy.1, rfl⟩

Goal state after:
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 : ι → Prop
⊢ Function.Surjective ⇑(π_app C J)

Tactic:
intro x

Goal state after:
ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J : ι → Prop
x : ↑(obj C J)
⊢ ∃ a, (π_app C J) a = x
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
f : ↑(π C fun x ↦ x ∈ s) → ↥s → Bool := fun x j ↦ ↑x ↑j
x : I → Bool
hx : x ∈ C
y : I → Bool
hy : y ∈ C
h : f ⟨Proj (fun x ↦ x ∈ s) x, ⋯⟩ = f ⟨Proj (fun x ↦ x ∈ s) y, ⋯⟩
i : I
hi : i ∉ s
⊢ ↑⟨Proj (fun x ↦ x ∈ s) x, ⋯⟩ i = ↑⟨Proj (fun x ↦ x ∈ s) y, ⋯⟩ i

Tactic:
· simp only [Proj, if_neg hi]

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
⊢ Injective (closedCell 0)

Tactic:
intro x

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x : cell C 0
⊢ ∀ ⦃a₂ : cell C 0⦄, closedCell 0 x = closedCell 0 a₂ → x = a₂
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
⊢ Injective (openCell 0)

Tactic:
intro x

Goal state after:
X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
x : cell C 0
⊢ ∀ ⦃a₂ : cell C 0⦄, openCell 0 x = openCell 0 a₂ → x = a₂
Module: Mathlib.Topology.Category.Compactum

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

Tactic:
rw [t2_iff_ultrafilter]
  intro _ _ F hx hy
  rw [← str_eq_of_le_nhds _ _ hx, ← str_eq_of_le_nhds _ _ hy]

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
⊢ ∀ (x : X.A) (g : Ultrafilter X.A),
    ↑g ≤ 𝓝 x → Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))

Tactic:
intro x

Goal state after:
X Y : Compactum
f : X ⟶ Y
x : X.A
⊢ ∀ (g : Ultrafilter X.A), ↑g ≤ 𝓝 x → Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hsC : x i = true → ord I i < Order.succ o
hi✝ : o ≤ ord I i
hi : o < ord I i
⊢ false = x i

Tactic:
← not_imp_not

Goal state after:
case inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hsC : ¬ord I i < Order.succ o → ¬x i = true
hi✝ : o ≤ ord I i
hi : o < ord I i
⊢ false = x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ f default • eval {fun x ↦ false} nil = f

Tactic:
simp only [eval, List.map, List.prod_nil, zsmul_eq_mul, mul_one, Products.nil]

Goal state after:
I : Type u_1
inst✝ : LinearOrder I
f : LocallyConstant ↑{fun x ↦ false} ℤ
a✝ : f ∈ ⊤
⊢ ↑(f default) = f
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hsC : x i = true → ord I i < Order.succ o
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
⊢ false = x i

Tactic:
← not_imp_not

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C1 C ho
i : I
hsC : ¬ord I i < Order.succ o → ¬x i = true
hi : ¬ord I i = o
h : o ≤ ord I i
h' : o < ord I i
⊢ false = x i
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n.succ i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell m j
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) := ⋯
⊢ cellFrontier (n + 1) i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell m j

Tactic:
intro x

Goal state after:
case h
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ
i : cell C (n + 1)
J : (m : ℕ) → Finset (cell C m)
hJ : cellFrontier n.succ i ⊆ D ∪ ⋃ m, ⋃ (_ : m < n.succ), ⋃ j ∈ J m, closedCell m j
p : (m : ℕ) → m ≤ n → cell C m → (m : ℕ) → Finset (cell C m)
hp :
  ∀ (m : ℕ) (a : m ≤ n) (i : cell C m), cellFrontier m i ⊆ D ∪ ⋃ m_1, ⋃ (_ : m_1 < m), ⋃ j ∈ p m a i m_1, openCell m_1 j
I : (m : ℕ) → Finset (cell C m) :=
  fun m ↦ J m ∪ (Finset.range n.succ).biUnion fun l ↦ (J l).biUnion fun y ↦ if h : l ≤ n then p l h y m else ∅
x : X
⊢ x ∈ cellFrontier (n + 1) i → x ∈ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, openCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
⊢ ∀ (x : I → Bool) (hx : x ∈ C0 C ho ∩ π (C1 C ho) fun x ↦ ord I x < o),
    (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f) ⟨x, ⋯⟩ =
      (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⟨x, ⋯⟩

Tactic:
intro x

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
f : LocallyConstant ↑C ℤ
hf :
  ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₁ C hsC ho, continuous_toFun := ⋯ }) f) =
    ⇑((LocallyConstant.comapₗ ℤ { toFun := CC'₀ C ho, continuous_toFun := ⋯ }) f)
C₀C : ↑(C0 C ho) → ↑C := fun x ↦ ⟨↑x, ⋯⟩
h₀ : Continuous C₀C
C₁C : ↑(π (C1 C ho) fun x ↦ ord I x < o) → ↑C := fun x ↦ ⟨SwapTrue o ↑x, ⋯⟩
h₁ : Continuous C₁C
x : I → Bool
⊢ ∀ (hx : x ∈ C0 C ho ∩ π (C1 C ho) fun x ↦ ord I x < o),
    (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f) ⟨x, ⋯⟩ =
      (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⟨x, ⋯⟩
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ contained (π C fun x ↦ ord I x < o) o

Tactic:
intro x

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x : I → Bool
⊢ (x ∈ π C fun x ↦ ord I x < o) → ∀ (i : I), x i = true → ord I i < o
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o) '' {m | m < l})

Tactic:
rwa [eval_πs_image' C (le_of_lt hslt) hlt, ← eval_πs' C (le_of_lt hslt) hlt,
    Submodule.apply_mem_span_image_iff_mem_span (injective_πs' C _)]

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 m : ℕ∞
h : m ≤ n
⊢ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
intro x

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n m : ℕ∞
h : m ≤ n
x : X
⊢ x ∈ ⋃ m_1, ⋃ (_ : ↑m_1 < m), ⋃ j, closedCell m_1 j → x ∈ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j
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
⊢ closedCell n j ⊆ ↑(skeletonLT C (↑n + 1))

Tactic:
intro x

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
⊢ x ∈ closedCell n j → x ∈ ↑(skeletonLT C (↑n + 1))