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

Goal state before:
pp: case oadd.inl.none.inl.some.succ
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr

Tactic:
e,

Goal state after:
case oadd.inl.none.inl.some.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.FundamentalSequenceProp (Sum.inl (some a'))
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m'.succPNat (a'.oadd (i + 1).succPNat zero) ∧
          a.oadd m'.succPNat (a'.oadd i.succPNat zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat (a'.oadd i.succPNat zero)).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd m b ∧ ((a.oadd m b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < ((f i).oadd 1 zero).repr

Tactic:
e,

Goal state after:
case oadd.inl.none.inr.zero
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha : a.FundamentalSequenceProp (Sum.inr f)
e : a.fundamentalSequence = Sum.inr f
e' : m.natPred = 0
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        (f i).oadd 1 zero < (f (i + 1)).oadd 1 zero ∧
          (f i).oadd 1 zero < a.oadd m b ∧ ((a.oadd m b).NF → ((f i).oadd 1 zero).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < ((f i).oadd 1 zero).repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m'.succPNat ((f (i + 1)).oadd 1 zero) ∧
          a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr

Tactic:
e,

Goal state after:
case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha : a.FundamentalSequenceProp (Sum.inr f)
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ IsSuccLimit (a.oadd m b).repr ∧
    (∀ (i : ℕ),
        a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m'.succPNat ((f (i + 1)).oadd 1 zero) ∧
          a.oadd m'.succPNat ((f i).oadd 1 zero) < a.oadd m b ∧
            ((a.oadd m b).NF → (a.oadd m'.succPNat ((f i).oadd 1 zero)).NF)) ∧
      ∀ a_1 < (a.oadd m b).repr, ∃ i, a_1 < (a.oadd m'.succPNat ((f i).oadd 1 zero)).repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.inr
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsNeg exps_tl
h_eq : toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) = toFun exps_tl basis_tl
⊢ Tendsto (toFun exps_tl basis_tl) atTop (𝓝 0)

Tactic:
exact toFun_tendsto_zero_of_firstNonzeroIsNeg h_basis.tail (by simpa using h_length) h.right

Goal state after:
Module: Mathlib.Tactic.DeriveCountable

Goal state before:
pp: p : Prop
a b a' b' : ℕ
h : a = a' → b = b' → p
⊢ Nat.pair a b = Nat.pair a' b' → p

Tactic:
by
  rwa [Nat.pair_eq_pair, and_imp]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * ↑↑i.succPNat + 0 < ω ^ a.repr

Tactic:
add_zero,

Goal state after:
case oadd.inl.none.inl.some.succ.refine_2
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
this : 0 < ω ^ a'.repr
i : ℕ
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ a'.repr * ↑↑i.succPNat < ω ^ a.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ (f i).repr * ↑↑1 + 0 < ω ^ a.repr

Tactic:
add_zero,

Goal state after:
case oadd.inl.none.inr.succ
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
h1 : IsSuccLimit a.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)
h3 : ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
i : ℕ
h4 : f i < f (i + 1)
h5 : f i < a
h6 : a.NF → (f i).NF
H : (a.oadd (m' + 1).succPNat 0).NF
⊢ ω ^ (f i).repr * ↑↑1 < ω ^ a.repr
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: n k p q : ℕ
hq : 0 < q
h_coprime : p.Coprime q
h_left : k ^ q < n
h_right : n < (k + 1) ^ q
m : ℕ
⊢ ∀ (m : ℕ), n ≠ m ^ q

Tactic:
intro m

Goal state after:
n k p q : ℕ
hq : 0 < q
h_coprime : p.Coprime q
h_left : k ^ q < n
h_right : n < (k + 1) ^ q
m✝ m : ℕ
⊢ n ≠ m ^ q
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: case hb0
a : ℚ
n d : ℕ
hd : ¬IsSquare d
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

Tactic:
contrapose! hnd
    simp_all

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

Goal state before:
pp: a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ -jacobiSym (↑b) a = -r

Tactic:
neg_inj

Goal state after:
a b : ℕ
r : ℤ
ha : a % 4 = 3
hb : b % 4 = 3
hr : jacobiSymNat b a = r
⊢ jacobiSym (↑b) a = r
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}
⊢ ∃ i, (interior (F i)).Nonempty

Tactic:
by
    have : Nonempty X := ⟨x⟩
    have : Encodable s := Countable.toEncodable s_count
    apply nonempty_interior_of_iUnion_of_closed
    · rintro ⟨n, ⟨g, hg⟩⟩
      apply IsCompact.isClosed
      suffices H : IsCompact ((fun (g : G) ↦ g • x) '' (K n ∩ g • V)) by
        simpa only [F, smul_singleton] using H
      apply IsCompact.image ?_ (by fun_prop)
      exact (isCompact_compactCovering G n).inter_right (V_closed.smul g)
    · apply eq_univ_iff_forall.2 (fun y ↦ ?_)
      obtain ⟨h, rfl⟩ : ∃ h, h • x = y := exists_smul_eq G x y
      obtain ⟨n, hn⟩ : ∃ n, h ∈ K n := exists_mem_compactCovering h
      obtain ⟨g, gs, hg⟩ : ∃ g ∈ s, h ∈ g • V := exists_set_mem_of_union_eq_top s _ hs _
      simp only [F, smul_singleton, mem_iUnion, mem_image, mem_inter_iff, Prod.exists,
        Subtype.exists, exists_prop]
      exact ⟨n, g, gs, h, ⟨hn, hg⟩, rfl⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
⊢ (ConcreteCategory.hom (quotientMap f Y))
      ((ConcreteCategory.hom
          ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
        ↑t) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) ↑t)

Tactic:
have := P.cone.π.naturality g

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
x :
  (j : FiniteIndexNormalSubgroup ↑G) →
    ↑((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).obj j)
hx :
  x ∈
    {u |
      ∀ {i j : FiniteIndexNormalSubgroup ↑G} (f : i ⟶ j),
        (ConcreteCategory.hom
              ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map f))
            (u i) =
          u j}
this✝ :
  (ConcreteCategory.hom
        ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
      (x (preimage f X)) =
    x (preimage f Y)
t : ↑G
ht : ↑t = x (preimage f X)
this :
  ((Functor.const (OpenNormalSubgroup ↑P.toProfinite.toTop)).obj P.cone.pt).map g ≫ P.cone.π.app Y =
    P.cone.π.app X ≫ P.diagram.map g
⊢ (ConcreteCategory.hom (quotientMap f Y))
      ((ConcreteCategory.hom
          ((((diagram G ⋙ forget₂ ProfiniteGrp.{u} Profinite) ⋙ profiniteToCompHaus) ⋙ compHausToTop).map ⋯.hom))
        ↑t) =
    (Hom.hom (P.diagram.map g)) ((ConcreteCategory.hom (quotientMap f X)) ↑t)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
S : Set C(X, α)
hS1 : IsCompact (ContinuousMap.toFun '' S)
hS2 : Equicontinuous fun x ↦ ⇑↑x
⊢ IsCompact S

Tactic:
by
  suffices h : IsInducing (Equiv.Set.image _ S DFunLike.coe_injective) by
    rw [isCompact_iff_compactSpace] at hS1 ⊢
    exact (Equiv.toHomeomorphOfIsInducing _ h).symm.compactSpace
  rw [← IsInducing.subtypeVal.of_comp_iff, ← EquicontinuousOn.isInducing_uniformOnFun_iff_pi]
  · exact ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.isInducing.comp .subtypeVal
  · exact eq_univ_iff_forall.mpr (fun x ↦ mem_sUnion_of_mem (mem_singleton x) isCompact_singleton)
  · exact fun _ ↦ id
  · exact fun K _ ↦ hS2.equicontinuousOn K

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
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:
by
  ext; simp

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
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:
by
  ext; simp

Goal state after:
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:
by
  ext; simp

Goal state after:
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
x : EuclideanSpace ℝ (Fin n)
hx : x ∈ Metric.ball 0 1
y : EuclideanSpace ℝ (Fin n)
hy : y ∈ Metric.ball 0 1
h :
  (ConcreteCategory.hom (ballInclusion n)) { down := ⟨x, hx⟩ } =
    (ConcreteCategory.hom (ballInclusion n)) { down := ⟨y, hy⟩ }
⊢ x = y

Tactic:
by simpa [ballInclusion, disk] using h

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x : cell C 0
⊢ cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 x ↔ cellFrontier 1 e = closedCell 0 x

Tactic:
union_self

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x : cell C 0
⊢ cellFrontier 1 e = closedCell 0 x ↔ cellFrontier 1 e = closedCell 0 x
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
hA : IsClosed[inst✝] A
⊢ relDerivedSet A = derivedSet A

Tactic:
simpa using (isClosed_iff_derivedSet_subset A).mp hA

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

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
eventually_isEmpty_cell : ∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
⊢ IsClosed[inst✝] (A ∩ C)

Tactic:
simp_rw [Filter.eventually_atTop] at eventually_isEmpty_cell

Goal state after:
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
eventually_isEmpty_cell : ∃ a, ∀ (b : ℕ), a ≤ b → IsEmpty (cell b)
⊢ IsClosed[inst✝] (A ∩ C)
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ Perfect U ↔ U = derivedSet U

Tactic:
by
  rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet,
    ← subset_antisymm_iff, eq_comm]

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

Goal state before:
pp: case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := ⋯
⊢ ∀ (b : ℕ), A.max' ⋯ + 1 ≤ b → IsEmpty (cell C b)

Tactic:
intro m

Goal state after:
case h
X : Type u_2
inst✝¹ : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
finite : _root_.Finite ((n : ℕ) × cell C n)
h✝ : Nonempty ((n : ℕ) × cell C n)
x✝ : Fintype ((n : ℕ) × cell C n)
A : Finset ℕ := Finset.image Sigma.fst Finset.univ
m : ℕ
⊢ A.max' ⋯ + 1 ≤ m → IsEmpty (cell C m)
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
I J : (n : ℕ) → Set (cell C n)
hIJ : D ∪ ⋃ n, ⋃ j, openCell n ↑j = D ∪ ⋃ n, ⋃ j, openCell n ↑j
⊢ I = J

Tactic:
ext n x
  exact ⟨fun h ↦ subset_of_eq_union_iUnion I J hIJ n h,
    fun h ↦ subset_of_eq_union_iUnion J I hIJ.symm n h⟩

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

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ↑x b = true
⊢ (e (π C fun x ↦ x ∈ s) b) x = 1

Tactic:
e,

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ↑x b = true
⊢ { toFun := fun f ↦ if ↑f b = true then 1 else 0, isLocallyConstant := ⋯ } x = 1
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
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ 1 x - (e (π C fun x ↦ x ∈ s) b) x = 1

Tactic:
e,

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
x y : ↑(π C fun x ↦ x ∈ s)
h : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
hh : ¬↑x b = true
⊢ 1 x - { toFun := fun f ↦ if ↑f b = true then 1 else 0, isLocallyConstant := ⋯ } x = 1
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 = true
hx : ↑x a = false
⊢ (LocallyConstant.evalMonoidHom y) (1 - e (π C fun x ↦ x ∈ s) a) = 0

Tactic:
e,

Goal state after:
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 = true
hx : ↑x a = false
⊢ (LocallyConstant.evalMonoidHom y) (1 - { toFun := fun f ↦ if ↑f a = true then 1 else 0, isLocallyConstant := ⋯ }) = 0
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case true
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 ≠ true
hx : ↑x a = true
⊢ (e (π C fun x ↦ x ∈ s) a) y = 0

Tactic:
e,

Goal state after:
case true
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 ≠ true
hx : ↑x a = true
⊢ { toFun := fun f ↦ if ↑f a = true then 1 else 0, isLocallyConstant := ⋯ } y = 0
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_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})

Tactic:
intro m

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}
m : Products I
⊢ c m ≠ 0 →
    e (π C fun x ↦ x ∈ s) a * c m • Products.eval (π C fun x ↦ x ∈ s) m ∈
      Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ Proj J y ∈ C

Tactic:
proj_eq_self

Goal state after:
case refine_1
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ y ∈ C

case refine_1.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
x✝ : x ∈ π C J
y : I → Bool
hy : y ∈ C
h : Proj J y = x
⊢ ∀ (i : I), y i ≠ false → J i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ Proj J x = x

Tactic:
proj_eq_self

Goal state after:
case refine_2
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ x = x

case refine_2.h
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i
x : I → Bool
h : x ∈ C
⊢ ∀ (i : I), x i ≠ false → J i