mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.refine_2
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ succ ↑k * α' + (ω0 ^ ↑k * α' * ↑m + R) = (ω0 ^ ↑k * α' + R) * α' + (ω0 ^ ↑k * α' + R) * ↑m

Tactic:
congr 1

Goal state after:
case succ.refine_2.e_a
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ succ ↑k * α' = (ω0 ^ ↑k * α' + R) * α'

case succ.refine_2.e_a
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ ↑k * α' * ↑m + R = (ω0 ^ ↑k * α' + R) * ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ ((ω ^ a0.repr) ^ ω) ^ b'.repr *
      ((ω ^ a0.repr) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr) =
    ((ω ^ a0.repr) ^ ω) ^ b'.repr * ((ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr + ↑m))

Tactic:
congr 1

Goal state after:
case oadd.succ.e_a
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (ω ^ a0.repr) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr) + (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ k * (ω ^ a0.repr * ↑↑n + a'.repr + ↑m)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
⊢ nil.tail = nil

Tactic:
simp [tail, nil]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h.nil
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
hF : h_opf.unfold s.head = none
⊢ (op nil).destruct =
    Option.map ((fun x ↦ (x.1, ↑x.2 s.tail)) ∘ fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)

Tactic:
specialize hT nil

Goal state after:
case h.nil
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  (op nil).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, opf, op') => (hd, ↑op' (↑opf nil.tail)))
      (T nil.head)
s : Stream'.Seq α
hF : h_opf.unfold s.head = none
⊢ (op nil).destruct =
    Option.map ((fun x ↦ (x.1, ↑x.2 s.tail)) ∘ fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_neg : ms.leadingExp < 0
h_approx : ms.Approximates
⊢ Tendsto ms.toFun atTop (𝓝 0)

Tactic:
cases ms

Goal state after:
case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
h_neg : (mk Multiseries.nil f✝).leadingExp < 0
h_approx : (mk Multiseries.nil f✝).Approximates
⊢ Tendsto (mk Multiseries.nil f✝).toFun atTop (𝓝 0)

case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
h_neg : (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).leadingExp < 0
h_approx : (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).Approximates
⊢ Tendsto (mk (Multiseries.cons exp✝ coef✝ tl✝) f✝).toFun atTop (𝓝 0)
Module: Mathlib.Tactic.Polynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
a : R
n : ℕ
⊢ (Polynomial.monomial n) a = a • Polynomial.X ^ n

Tactic:
← Polynomial.C_mul_X_pow_eq_monomial,

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
a : R
n : ℕ
⊢ Polynomial.C a * Polynomial.X ^ n = a • Polynomial.X ^ n
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ (Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m)).getD y = (List.dlookup x m).getD y

Tactic:
congr 1

Goal state after:
case e_opt
α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
a : α
A : List ((_ : α) × β)
y od : β
hval : ⟨a, od⟩ ∈ A.dedupKeys
hod : (decide ¬od = 0) = true
this : od ∈ List.dlookup a A.dedupKeys
⊢ List.dlookup a A = some od

Tactic:
simpa [List.dlookup_dedupKeys]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : ∀ i_1 ∈ A, (i, j) ∈ {ij | (F ij.1 i_1, F ij.2 i_1) ∈ V}
x a : X
ha : a ∈ A
hax : x ∈ Ω a
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U

Tactic:
exact hVU <| SetRel.prodMk_mem_comp (SetRel.prodMk_mem_comp (SetRel.symm V <| hax i) (hij a ha))
      (hax j)

Goal state after:
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: 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
⊢ Continuous[inst✝⁹, inst✝⁸] fun g ↦ g • x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ (Subgroup.closure s).toSubmonoid ≤ (Submonoid.closure s).topologicalClosure

Tactic:
Subgroup.closure_toSubmonoid,

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
s : Set G
⊢ Submonoid.closure (s ∪ s⁻¹) ≤ (Submonoid.closure s).topologicalClosure
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
α : Type u_7
inst✝ : TopologicalSpace α
f : α → E
x✝ : Continuous[inst✝, inst] f
⊢ ∀ (y : F), Continuous[inst✝, inst✝⁵] fun x ↦ (B (f x)) y

Tactic:
by fun_prop

Goal state after:
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:
congr 1

Goal state after:
case e_f
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
⊢ (fun c ↦ (L (f (↑((mulFiber_swapEquiv x) c)).1)) (g (↑((mulFiber_swapEquiv x) c)).2)) = fun ab ↦
    (L (g (↑ab).1)) (f (↑ab).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
⊢ V ∈ 𝓕₂

Tactic:
obtain ⟨W, ⟨W_mem_𝓕₂, W_bal⟩, hW⟩ := basis_𝓕₂.inf_principal V |>.mem_iff.mp cV_mem

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
⊢ V ∈ 𝓕₂
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: α : Type u_1
𝕜 : 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
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
f : F
⊢ Continuous[inst, inst✝⁶] (B.flip f).toFun

Tactic:
by fun_prop

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
V_mem : V ∈ 𝓝 0
H : TopologicalSpace.induced Subtype.val t₁ = TopologicalSpace.induced Subtype.val t₂
⊢ t₁ = t₂

Tactic:
by
  apply topology_eq_of_nhds_inf_principal_eq 𝕜₁ t₁ t₂ V_mem
  set o : V := ⟨0, letI := t₁; mem_of_mem_nhds V_mem⟩
  simp_rw [← map_comap_setCoe_val, show 0 = (o : E) from rfl, ← nhds_induced]
  rw [H]

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

Goal state before:
pp: R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
f : R → R × R := fun u ↦ (star u * u, u * star u)
hf : f ⁻¹' {(1, 1)} = ↑(unitary R)
⊢ Continuous f

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance = coinduced (fun x ↦ x.fst.snd x.snd) inferInstance

Tactic:
coinduced_iSup,

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance =
    ⨆ i, coinduced (fun x ↦ x.fst.snd x.snd) (coinduced (Sigma.mk i) (inst✝ i.fst))
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
S : Set X.A
hS : S ∈ F
⊢ (basic S).Nonempty

Tactic:
exact ⟨F, hS⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x ↦ x ∈ s) z, ⋯⟩ a = true
⊢ e (π C fun x ↦ x ∈ s) a ∈ factors C s ⟨Proj (fun x ↦ x ∈ s) z, ⋯⟩

Tactic:
simp only [factors, List.mem_map, Finset.mem_sort]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
z : I → Bool
hz : z ∈ C
hx : ↑⟨Proj (fun x ↦ x ∈ s) z, ⋯⟩ a = true
⊢ ∃ a_1 ∈ s,
    (if Proj (fun x ↦ x ∈ s) z a_1 = true then e (π C fun x ↦ x ∈ s) a_1 else 1 - e (π C fun x ↦ x ∈ s) a_1) =
      e (π C fun x ↦ x ∈ s) a
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)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ 1 - e (π C fun x ↦ x ∈ s) a ∈ factors C s x

Tactic:
simp only [factors, List.mem_map, Finset.mem_sort]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
a : I
ha : ↑y a = true
hx : ↑x a = false
⊢ ∃ a_1 ∈ s,
    (if ↑x a_1 = true then e (π C fun x ↦ x ∈ s) a_1 else 1 - e (π C fun x ↦ x ∈ s) a_1) = 1 - e (π C fun x ↦ x ∈ s) a
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
⊢ ↑(map 1 e) '' sphere 0 1 = ↑(map 1 e) '' {-1, 1}

Tactic:
congr 1

Goal state after:
case e_s
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
⊢ sphere 0 1 = {-1, 1}
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
⊢ (c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * b • Products.eval (π C fun x ↦ x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
apply Submodule.finsuppSum_mem

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
⊢ ∀ (c_1 : Products I),
    c c_1 ≠ 0 →
      e (π C fun x ↦ x ∈ s) a * c c_1 • Products.eval (π C fun x ↦ x ∈ s) c_1 ∈
        Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h : ∀ (i : I), J i → K i
⊢ Proj J ∘ Proj K = Proj J

Tactic:
ext x i; dsimp [Proj]; simp_all

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

Goal state before:
pp: X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ cl A ↔ x✝ ∈ closure A

Tactic:
rw [mem_closure_iff_ultrafilter]

Goal state after:
X : Compactum
A : Set X.A
x✝ : X.A
⊢ x✝ ∈ cl A ↔ ∃ u, A ∈ u ∧ ↑u ≤ 𝓝 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
this : (fun x1 x2 ↦ x1 < x2) = fun l m ↦ List.Lex (fun x1 x2 ↦ x1 < x2) ↑l ↑m
⊢ WellFoundedLT (Products I)

Tactic:
WellFoundedLT,

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
this : (fun x1 x2 ↦ x1 < x2) = fun l m ↦ List.Lex (fun x1 x2 ↦ x1 < x2) ↑l ↑m
⊢ IsWellFounded (Products I) fun x1 x2 ↦ x1 < x2
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg.h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ (c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
apply Submodule.finsuppSum_mem

Goal state after:
case neg.h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := ⋯
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
hmap :
  ∀ (g : Products I → ℤ → LocallyConstant ↑(π C fun x ↦ x ∈ s) ℤ),
    e (π C fun x ↦ x ∈ s) a * c.sum g = c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * g a_1 b
h✝ : ¬↑x a = true
⊢ ∀ (c_1 : Products I),
    c c_1 ≠ 0 →
      c c_1 • Products.eval (π C fun x ↦ x ∈ s) c_1 ∈
        Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
⊢ LinearIndependent ℤ (Subtype.val ∘ (equiv_range C).toFun) ↔ LinearIndependent ℤ fun (p : ↑(range C)) ↦ ↑p

Tactic:
exact linearIndependent_equiv (equiv_range C)

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
x : ↑(C' C ho)
⊢ y (ProjRestrict C (fun x ↦ ord I x < o) (CC'₁ C hsC ho x)) = y (ProjRestrict C (fun x ↦ ord I x < o) (CC'₀ C ho x))

Tactic:
congr 1

Goal state after:
case e_6
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
x : ↑(C' C ho)
⊢ ProjRestrict C (fun x ↦ ord I x < o) (CC'₁ C hsC ho x) = ProjRestrict C (fun x ↦ ord I x < o) (CC'₀ C ho x)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

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

Tactic:
rw [← hx.2, hi]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

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

Tactic:
rw [← hx.2, hi]

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
⊢ P I o

Tactic:
hho

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ ∀ (C : Set (I → Bool)), IsClosed C → contained C o → LinearIndependent ℤ (eval C)
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case coe
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
x : X
m a✝ : ℕ
⊢ ↑m < ↑a✝ + 1 ↔ ↑m ≤ ↑a✝

Tactic:
· rw [← Nat.cast_one, ← Nat.cast_add, Nat.cast_lt, Nat.cast_le, Order.lt_add_one_iff]

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 : ℕ
j : cell C m
hnm : n ≤ ↑m
⊢ Disjoint (↑(skeletonLT C n)) (openCell m j)

Tactic:
simp_rw [← iUnion_openCell_eq_skeletonLT, disjoint_union_left, disjoint_iUnion_left]
  refine ⟨(disjointBase m j).symm, ?_⟩
  intro l hln i
  apply disjoint_openCell_of_ne
  intro
  simp_all only [Sigma.mk.inj_iff]
  exact (lt_self_iff_false m).mp (ENat.natCast_lt_natCast.1 (hln.trans_le hnm))

Goal state after:
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
⊢ (∀ (i : Fin n), IsClopen (U i)) →
    (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard

Tactic:
hU1

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
n : ℕ
U : Fin n → Set X
hU1 : ∀ (i : Fin n), IsClopen (U i)
⊢ (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard