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

Goal state before:
pp: case neg.inl
x y✝ y : ZFSet.{u}
hy : y.IsOrdinal
m : ZFSet.{u}
hmy : m ∈ y
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(m, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : m.IsOrdinal
hxy : m ⊆ y
hyx : ¬y ⊆ m
hm : m ∈ ↑y \ ↑m
hm' : ∀ x ∈ ↑y \ ↑m, x ∉ m
hmx : m ⊆ m
⊢ m = y ∨ m ∈ y

pp: case neg.inr
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
H : m ∈ x
⊢ x = y ∨ x ∈ y

Tactic:
· exact Or.inr hmy

Goal state after:
case neg.inr
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
hmx : m ⊆ x
H : m ∈ x
⊢ x = y ∨ x ∈ y
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ (e₁.oadd n✝.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
· simp only [Nat.succPNat, Nat.succ_eq_add_one, repr, PNat.mk_coe, ← succ_eq_add_one]
        rw [(tsub_eq_iff_eq_add_of_le <| le_of_lt <| Nat.lt_of_sub_eq_succ mn).1 mn, add_comm,
          Nat.cast_add, mul_add, add_assoc, add_sub_add_cancel]
        refine
          (Ordinal.sub_eq_of_add_eq <|
              add_of_omega0_opow_le h₂.snd'.repr_lt <| le_trans ?_ le_self_add).symm
        exact Ordinal.le_mul_left _ (Nat.cast_lt.2 <| Nat.succ_pos _)

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

Goal state before:
pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
⊢ (o₁ ^ o₂).NF

Tactic:
simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, split_eq_scale_split' e₂, mulNat_eq_mul]

Goal state after:
case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
⊢ (match (scale 1 b', k) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
⊢ Majorized (f ^ exp) f exp

Tactic:
by
  simp only [Majorized]
  intro exp' h_exp
  apply (isLittleO_iff_tendsto' _).mpr
  · have : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ (f t) ^ (exp - exp') :=
      (h.eventually_gt_atTop 0).mono (fun _ h ↦ by simp [← Real.rpow_sub h])
    apply Tendsto.congr' this.symm
    conv =>
      arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
    exact (tendsto_rpow_neg_atTop (by linarith)).comp h
  · apply (Tendsto.eventually_gt_atTop h 0).mono
    intro t h1 h2
    absurd h2
    exact (Real.rpow_pos_of_pos h1 _).ne.symm

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

Goal state before:
pp: case cons
hd : ℝ → ℝ
tl : List (ℝ → ℝ)
ih : WellFormedBasis tl → ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ tl, 0 < f x
h : WellFormedBasis (hd :: tl)
⊢ ∀ᶠ (x : ℝ) in atTop, ∀ f ∈ hd :: tl, 0 < f x

Tactic:
simp only [WellFormedBasis, List.pairwise_cons, List.mem_cons, forall_eq_or_imp] at h
    simp only [List.mem_cons, forall_eq_or_imp]
    exact (h.right.left.eventually <| eventually_gt_atTop 0).and (ih (by tauto))

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

Goal state before:
pp: f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Tendsto (fun x ↦ (g ^ b) x / (f ^ a) x) atTop atTop

Tactic:
apply Tendsto.congr' (f₁ := Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f))

Goal state after:
case hl
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f) =ᶠ[atTop] fun x ↦ (g ^ b) x / (f ^ a) x

case h
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Tendsto (Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f)) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

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

Tactic:
by
  simp [head, nil]

Goal state after:
Module: Mathlib.Tactic.ModCases

Goal state before:
pp: case refine_1
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a % n < n

pp: case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]

Tactic:
· exact Nat.mod_lt _ (Nat.le_of_ble_eq_true hn)

Goal state after:
case refine_2
p : Sort ?u.2
a n : ℕ
hn : Nat.ble 1 n = true
H : OnModCases n a 0 p
⊢ a ≡ a % n [MOD n]
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}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (g • interior (V • {x})).Nonempty
⊢ (interior (V • {x})).Nonempty

Tactic:
exact smul_set_nonempty.1 I

Goal state after:
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
⊢ IsInducing (⇑(UniformOnFun.ofFun ?m.83) ∘ Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯))

pp: case 𝔖_covers
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
⊢ ⋃₀ ?m.83 = univ

pp: case 𝔖_compact
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
⊢ ∀ K ∈ ?m.83, IsCompact K

pp: case F_eqcont
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
⊢ ∀ K ∈ ?m.83, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K

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
⊢ Set (Set X)

Tactic:
· exact ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact.isInducing.comp .subtypeVal

Goal state after:
case 𝔖_covers
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
⊢ ⋃₀ {K | IsCompact K} = univ

case 𝔖_compact
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
⊢ ∀ K ∈ {K | IsCompact K}, IsCompact K

case F_eqcont
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
⊢ ∀ K ∈ {K | IsCompact K}, EquicontinuousOn (Subtype.val ∘ ⇑(Equiv.Set.image DFunLike.coe S ⋯)) K
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
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)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
⊢ C = D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1

Tactic:
rw [← union', iUnion_subtype]

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)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
this : IsClosed[inst✝] (A ∩ (D ∪ ⋃ n, ⋃ j, ↑(map (↑n) j) '' closedBall 0 1))
⊢ D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = D ∪ ⋃ x, ⋃ (hx : x < N), ⋃ j, ↑(map (↑⟨x, hx⟩) j) '' closedBall 0 1
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom f) (X.str xs) = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)

Tactic:
change (X.a ≫ f.f) _ = _

Goal state after:
X Y : Compactum
f : X ⟶ Y
xs : Ultrafilter X.A
⊢ (ConcreteCategory.hom (X.a ≫ f.f)) xs = Y.str (Ultrafilter.map (⇑(ConcreteCategory.hom f)) xs)
Module: Mathlib.Topology.Category.Compactum

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

Tactic:
rw [← isOpen_compl_iff]

Goal state after:
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ ↔ ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S
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 : y = x
b : I
left✝ : b ∈ s.sort fun x1 x2 ↦ x1 ≥ x2
⊢ (if ↑x b = true then e (π C fun x ↦ x ∈ s) b else 1 - e (π C fun x ↦ x ∈ s) b) x = 1

Tactic:
split_ifs with hh

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
⊢ (e (π C fun x ↦ x ∈ s) b) x = 1

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 - e (π C fun x ↦ x ∈ s) b) x = 1
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: ⊢ CreatesLimits (forget CompHaus)

Tactic:
let e : forget CompHaus ≅ compactumToCompHaus.inv ⋙ Compactum.forget :=
    (((forget CompHaus).leftUnitor.symm ≪≫
    Functor.isoWhiskerRight compactumToCompHaus.asEquivalence.symm.unitIso (forget CompHaus)) ≪≫
    compactumToCompHaus.inv.associator compactumToCompHaus (forget CompHaus)) ≪≫
    Functor.isoWhiskerLeft _ compactumToCompHausCompForget

Goal state after:
e : forget CompHaus ≅ compactumToCompHaus.inv ⋙ Compactum.forget :=
  (((forget CompHaus).leftUnitor.symm ≪≫
        Functor.isoWhiskerRight compactumToCompHaus.asEquivalence.symm.unitIso (forget CompHaus)) ≪≫
      compactumToCompHaus.inv.associator compactumToCompHaus (forget CompHaus)) ≪≫
    compactumToCompHaus.inv.isoWhiskerLeft compactumToCompHausCompForget
⊢ CreatesLimits (forget CompHaus)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (eval (π C J) l) (Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) = (eval C l) x

Tactic:
rw [Products.eval_eq, Products.eval_eq]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
l : Products I
J : I → Prop
h : ∀ a ∈ ↑l, J a
inst✝ : (j : I) → Decidable (J j)
x : ↑C
⊢ (if ∀ i ∈ ↑l, ↑(Set.MapsTo.restrict (Proj J) C (π C J) ⋯ x) i = true then 1 else 0) =
    if ∀ i ∈ ↑l, ↑x i = true then 1 else 0
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ LinearIndependent ℤ (eval (π C fun x ↦ ord I x < o)) ↔ LinearIndependent ℤ fun (p : ↑(smaller C o)) ↦ ↑p

Tactic:
by
  rw [GoodProducts.linearIndependent_iff_range,
    ← LinearMap.linearIndependent_iff (πs C o)
    (LinearMap.ker_eq_bot_of_injective (injective_πs _ _)), ← smaller_factorization C o]
  exact linearIndependent_equiv _

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

Goal state before:
pp: case refine_3.inl
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 ∈ C
hx₀ : x ∈ C0 C ho
hx₀' : ↑(ProjRestrict C (fun x ↦ ord I x < o) ⟨x, hx⟩) = x
⊢ ((πs C o)
        (LocallyConstant.piecewise' ⋯ ⋯ ⋯ (LocallyConstant.comap { toFun := C₀C, continuous_toFun := h₀ } f)
          (LocallyConstant.comap { toFun := C₁C, continuous_toFun := h₁ } f) ⋯))
      ⟨x, hx⟩ =
    f ⟨x, hx⟩

Tactic:
simp only [C₀C, πs_apply_apply, hx₀', hx₀, LocallyConstant.piecewise'_apply_left,
        LocallyConstant.coe_comap, ContinuousMap.coe_mk, Function.comp_apply]

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
hl : ∀ i ∈ ↑l, ord I i < o
⊢ eval C '' {m | m < l} = ⇑(πs C o) '' eval (π C fun x ↦ ord I x < o) '' {m | m < l}

Tactic:
ext f
  simp only [Set.mem_image, Set.mem_ofPred_eq, exists_exists_and_eq_and]
  apply exists_congr; intro m
  apply and_congr_right; intro hm
  rw [eval_πs C (lt_ord_of_lt hm hl)]

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
⊢ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j = ↑(skeletonLT C n)

Tactic:
← RelCWComplex.iUnion_openCell_eq_skeletonLT,

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝¹ : T2Space X
inst✝ : CWComplex C
n : ℕ∞
⊢ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j = ∅ ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
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}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this✝ : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
this :
  (Linear_CC' C hsC ho) (Products.eval C ↑l) =
    (Linear_CC' C hsC ho) (m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod)
hse :
  { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ), X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ),
      X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ), f := ModuleCat.ofHom (πs C o),
      g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.Exact
⊢ False

Tactic:
rw [ShortComplex.moduleCat_exact_iff_range_eq_ker] at hse

Goal state after:
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
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this✝ : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
this :
  (Linear_CC' C hsC ho) (Products.eval C ↑l) =
    (Linear_CC' C hsC ho) (m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod)
hse :
  (ModuleCat.Hom.hom
        { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
            X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ),
            f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.f).range =
    (ModuleCat.Hom.hom
        { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ),
            X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ),
            f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.g).ker
⊢ False
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst✝] (U i)
hAU : A ∪ B ⊆ ⋃ i, U i
⊢ ∃ t, t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨t₁, ht₁, hA_sub⟩ : ∃ (t₁ : Set ℕ), t₁.Finite ∧ A ⊆ ⋃ k ∈ t₁, U k :=
    hA U hUo (subset_union_left.trans hAU)

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst✝] (U i)
hAU : A ∪ B ⊆ ⋃ i, U i
t₁ : Set ℕ
ht₁ : t₁.Finite
hA_sub : A ⊆ ⋃ k ∈ t₁, U k
⊢ ∃ t, t.Finite ∧ A ∪ B ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Filter

Goal state before:
pp: ι : Sort u_1
α : Type u_2
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
⊢ (𝓝 l).HasBasis p fun i ↦ {l' | s i ∈ l'}

Tactic:
simpa only [Iic_principal] using h.nhds

Goal state after:
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: G G' : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : Group G'
inst✝ : IsTopologicalGroup G'
⊢ hSpace (G × G') = HSpace.prod G G'

Tactic:
simp only [HSpace.prod]

Goal state after:
G G' : Type u
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : TopologicalSpace G'
inst✝¹ : Group G'
inst✝ : IsTopologicalGroup G'
⊢ hSpace (G × G') =
    { hmul := { toFun := fun p ↦ (HSpace.hmul (p.1.1, p.2.1), HSpace.hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ },
      e := (HSpace.e, HSpace.e), hmul_e_e := ⋯,
      eHmul :=
        { toFun := fun p ↦ (HSpace.eHmul (p.1, p.2.1), HSpace.eHmul (p.1, p.2.2)), continuous_toFun := ⋯,
          map_zero_left := ⋯, map_one_left := ⋯, prop' := ⋯ },
      hmulE :=
        { toFun := fun p ↦ (HSpace.hmulE (p.1, p.2.1), HSpace.hmulE (p.1, p.2.2)), continuous_toFun := ⋯,
          map_zero_left := ⋯, map_one_left := ⋯, prop' := ⋯ } }
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mpr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N → y ∈ Cube.boundary (M ⊕ N)

Tactic:
rintro (⟨m, hm⟩ | ⟨n, hn⟩)
    · exact ⟨Sum.inl m, hm⟩
    · exact ⟨Sum.inr n, hn⟩

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.12
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
⊢ ((GenLoop.uncurry x p).comp { toFun := sumArrowHomeomorphProdArrow.toFun, continuous_toFun := ⋯ }) y = x

Tactic:
simp [hy]

Goal state after:
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ¬↑(x✝ i) ≤ 1 / 2
⊢ (↑((Path.extend (toLoop i g)) (2 * ↑(x✝ i) - 1)) fun j ↦ x✝ ↑j) =
    g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))

Tactic:
change g _ = _

Goal state after:
case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ¬↑(x✝ i) ≤ 1 / 2
⊢ g (↑(Cube.insertAt i) (Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑(x✝ i) - 1), fun j ↦ x✝ ↑j)) =
    g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}
⊢ max (⨆ x ∈ s, infEDist x t) (⨆ y ∈ t, infEDist y s) ≤ δ

Tactic:
max_le_iff

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}
⊢ hausdorffEDist s t ≤ δ

Tactic:
rw [hausdorffEDist, max_le_iff]

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : (s, t) ∈ hausdorffEntourage {p | edist p.1 p.2 ≤ δ}
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ