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

Goal state before:
pp: H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x
A : Class.{u}
⊢ ∀ y ∈ A, Acc (fun x1 x2 ↦ x1 ∈ x2) y

Tactic:
rintro B ⟨x, rfl, _⟩

Goal state after:
H : ∀ (x : ZFSet.{u}), Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x
A : Class.{u}
x : ZFSet.{u}
right✝ : A x
⊢ Acc (fun x1 x2 ↦ x1 ∈ x2) ↑x
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mp
x y : Class.{u}
⊢ y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z

pp: case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x

Tactic:
· rintro ⟨w, rfl, z, hzx, hwz⟩
    exact ⟨z, hzx, coe_mem.2 hwz⟩

Goal state after:
case mpr
x y : Class.{u}
⊢ (∃ z ∈ x, y ∈ z) → y ∈ ⋃₀ x
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ x.rank ≤ o

Tactic:
rank_le_iff

Goal state after:
o : Ordinal.{u_1}
x : ZFSet.{u_1}
⊢ x ⊆ V_ o ↔ ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg.refine_1
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ ω * a'.repr + ↑m' < ω * ω ^ (e.repr - 1)

Tactic:
rw [← this, ← IH₂]

Goal state after:
case neg.refine_1
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : ¬e = 0
a' : ONote
m' : ℕ
h' : a.split' = (a', m')
this✝¹ : e.NF
this✝ : a.NF
IH₁ : a'.NF
IH₂ : a.repr = ω * a'.repr + ↑m'
this : ω ^ e.repr = ω * ω ^ (e.repr - 1)
⊢ a.repr < ω ^ e.repr
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
this : a0.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

Tactic:
rcases k with - | k

Goal state after:
case oadd.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0)
⊢ (match (scale 1 b', 0) 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

case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
⊢ (match (scale 1 b', k + 1) 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.SetTheory.Ordinal.Notation

Goal state before:
pp: case inl
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)

pp: case inr
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)

Tactic:
· grw [le_succ b, succ_eq_add_one, add_mul_succ _ (one_add_of_omega0_le h)]
    · gcongr
      · exact omega0_pos
      · exact succ_le_iff.2 <| by gcongr; exact isSuccLimit_omega0.succ_lt l
    · exact omega0_pos

Goal state after:
case inr
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ IsClosed {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}

Tactic:
isClosed_iff_clusterPt

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
⊢ ∀ (a : Stream' (Option α)),
    ClusterPt a (Filter.principal {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}) →
      a ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case inr.inr
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : (Real.log ∘ f) =o[atTop] (Real.log ∘ basis_end)
hg : g = basis_end
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
· grind

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

Goal state before:
pp: case right
left right : Basis
h_left : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) left ∧ ∀ f ∈ left, Tendsto f atTop atTop
h_right : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) right ∧ ∀ f ∈ right, Tendsto f atTop atTop
h : ∀ f ∈ left, ∀ g ∈ right, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ ∀ f ∈ left ++ right, Tendsto f atTop atTop

Tactic:
· grind

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

Goal state before:
pp: case nil
⊢ zero.Approximates

Tactic:
simp [zero]

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

Goal state before:
pp: case oadd
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
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
⊢ (match (scale 1 b', k) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr

Tactic:
rcases k with - | k

Goal state after:
case oadd.zero
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
e₂ : o₂.split' = (b', 0)
r₂ : o₂.repr = ω * b'.repr + ↑0
⊢ (match (scale 1 b', 0) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr

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)
⊢ (match (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: α : Sort u_1
hα : Nonempty α
o : Ordinal.{u_2}
f : α → Ordinal.{u_2}
H : ∀ ⦃a : Ordinal.{u_2}⦄, a < o → ∃ i, a < f i
b a : Ordinal.{u_2}
h : a < b + o
⊢ ∃ i, a < b + f i

Tactic:
by
  rcases lt_or_ge a b with h | h'
  · obtain ⟨i⟩ := id hα
    exact ⟨i, h.trans_le le_self_add⟩
  · rw [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left] at h
    refine (H h).imp fun i H => ?_
    rwa [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left]

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

Goal state before:
pp: case x
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.Approximates ∨ ∃ (h_basis : basis_hd :: basis_tl = basis_hd :: basis_tl), motive (h_basis ▸ ms)

Tactic:
· grind

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

Goal state before:
pp: b m n : ℕ
hb : 1 < b
h₁ : b ^ m < n
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1

Tactic:
← Nat.lt_clog_iff_pow_lt hb

Goal state after:
b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : n.ble (b ^ (m + 1)) = true
⊢ Nat.clog b n = m + 1
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 ↑a = 1

Tactic:
simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 1
hb : b % 2 = 0
hc : b / 2 = c
hr : jacobiSymNat a c = r
⊢ legendreSym 2 ↑1 = 1
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : 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
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ TopologicalSpace.induced ((fun x1 x2 ↦ (B x1) x2) ∘ ⇑e.symm) Pi.topologicalSpace =
    TopologicalSpace.induced (fun x1 x2 ↦ (B' x1) x2) Pi.topologicalSpace

Tactic:
← hBB',

Goal state after:
𝕜 : 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
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ TopologicalSpace.induced ((fun x1 x2 ↦ (B x1) x2) ∘ ⇑e.symm) Pi.topologicalSpace =
    TopologicalSpace.induced (fun x1 x2 ↦ ((((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B) x1) x2)
      Pi.topologicalSpace
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₂
o : ↑V := ⟨0, ⋯⟩
⊢ map Subtype.val (𝓝 o) = map Subtype.val (𝓝 o)

Tactic:
H

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
V_mem : V ∈ 𝓝 0
H : TopologicalSpace.induced Subtype.val t₁ = TopologicalSpace.induced Subtype.val t₂
o : ↑V := ⟨0, ⋯⟩
⊢ map Subtype.val (𝓝 o) = map Subtype.val (𝓝 o)
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✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
H : (∏ p, p.asIdeal) ^ n = ⊥
this✝ : Finite (R ⧸ ∏ i, i.asIdeal)
this : Finite (R ⧸ (∏ p, p.asIdeal) ^ n)
⊢ Finite R

Tactic:
H

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
H : (∏ p, p.asIdeal) ^ n = ⊥
this✝ : Finite (R ⧸ ∏ i, i.asIdeal)
this : Finite (R ⧸ ⊥)
⊢ Finite R
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: case iUnion
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : ℕ → Set α
a✝ : Pairwise (Function.onFun Disjoint f)
hf✝ : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∃ u, IsOpen[inst✝²] u ∧ f i =ᶠ[residual α] u
⊢ ∃ u, IsOpen[inst✝²] u ∧ ⋃ i, f i =ᶠ[residual α] u

Tactic:
choose u uo su using ihf
    exact ⟨⋃ i, u i, isOpen_iUnion uo, .countable_iUnion su⟩

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
⊢ e ∈ univ ↔ ∃ x y, cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y

Tactic:
by
    simp only [mem_univ, true_iff]
    exact exists_cellFrontier_one_eq e

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
⊢ IsClosed[inst✝] A

Tactic:
isClosed_iff_clusterPt

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
⊢ ∀ (a : X), ClusterPt a (𝓟 A) → a ∈ A
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: case limit
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
a : Ordinal.{u}
ha : Order.IsSuccLimit a
ih : ∀ o' < a, IsClosed sᵈ[o']
⊢ IsClosed sᵈ[a]

Tactic:
| limit a ha ih =>

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
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:
exact congrFun h ⟨i, hi⟩

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✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ↑(map n j) '' closure (ball 0 1) ⊆ closure[t] (openCell n j)

Tactic:
apply ContinuousOn.image_closure

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
n : ℕ
j : cell C n
⊢ ContinuousOn (↑(map n j)) (closure (ball 0 1))
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}
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 : ¬ord I i = o
h : ¬ord I i < o
⊢ false = x i

Tactic:
simp only [not_lt] at h
    have h' : o < ord I i := lt_of_le_of_ne h (Ne.symm hi)
    specialize hsC x hx.1 i
    rw [← not_imp_not] at hsC
    simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC
    exact (hsC h').symm

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
⊢ ∃ I, cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, openCell m j

Tactic:
by
  simpa using RelCWComplex.cellFrontier_subset_finite_openCell n i

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : IsCompactSystem S
⊢ IsCompactSystem (insert ∅ S)

Tactic:
by
  intro s h' hd
  by_cases! g : ∃ n, s n = ∅
  · use g.choose
    rw [← subset_empty_iff] at hd ⊢
    exact (dissipate_subset le_rfl).trans g.choose_spec.le
  · exact h s (fun i ↦ (mem_of_mem_insert_of_ne (h' i) (g i).ne_empty)) hd

Goal state after:
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
⊢ dissipate C n ⊆ ∅

Tactic:
dissipate

Goal state after:
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (⋂ k, ⋂ (_ : k < n), C k).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
hi : ∀ (i : ℕ), C i ∈ S
h' : ∀ (n : ℕ), dissipate C n ≠ ∅
n : ℕ
g : ⋂ k, ⋂ (_ : k < n), C k ⊆ ∅
⊢ ⋂ y, ⋂ (_ : y ≤ n), C y ⊆ ∅
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ (⋂ i, C i).Nonempty

Tactic:
rw [← iInter_dissipate]

Goal state after:
α : Type u_2
inst✝ : TopologicalSpace α
C : ℕ → Set α
hC_cc : ∀ (i : ℕ), C i ∈ {s | IsCompact s ∧ IsClosed s}
h_nonempty : ∀ (n : ℕ), (dissipate C n).Nonempty
⊢ (⋂ x, dissipate C x).Nonempty
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: case refine_2
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hBA : B ⊆ A
hB : B.Infinite
f : ℕ ↪ ↑B := Set.Infinite.natEmbedding B hB
x : ℕ → E := Subtype.val ∘ ⇑f
hx_inj : Function.Injective x
a : E
haA : a ∈ A
hac : MapClusterPt a atTop x
⊢ map x atTop ≤ 𝓟 B

Tactic:
exact tendsto_principal.mpr <| Eventually.of_forall fun n => (f n).2

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
⊢ (logSizeBallSeq J hJ a c i).point ∉ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
by
  simp [finset_logSizeBallSeq_add_one, logSizeBallStruct.smallBall]

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ (M ⊕ N) X x)
y : M ⊕ N → ↑I
⊢ ((currySum x p) (y ∘ Sum.inl)) (y ∘ Sum.inr) = p y

Tactic:
by
  simp [currySum, sumArrowHomeomorphProdArrow, Equiv.sumArrowEquivProdArrow]

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ ⋂ n, preCantorSet n = ((fun x ↦ x / 3) '' ⋂ n, preCantorSet n) ∪ (fun x ↦ (2 + x) / 3) '' ⋂ n, preCantorSet n

Tactic:
Set.image_iInter,

Goal state after:
⊢ ⋂ n, preCantorSet n = (⋂ i, (fun x ↦ x / 3) '' preCantorSet i) ∪ (fun x ↦ (2 + x) / 3) '' ⋂ n, preCantorSet n

case hf
⊢ Function.Bijective fun x ↦ x / 3
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: case mpr
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
inst✝ : (i : ι) → TopologicalSpace (α i)
x : (i : ↑S) → α ↑i
⊢ (∃ x_1 ∈ s, S.domRestrict x_1 = x) →
    ∃ a,
      (∃ x ∈ s, Sᶜ.domRestrict x = a) ∧
        ∃ a_1 ∈ s, ((∃ x ∈ s, Sᶜ.domRestrict x = Sᶜ.domRestrict a_1) ∧ Sᶜ.domRestrict a_1 = a) ∧ (fun i ↦ a_1 ↑i) = x

Tactic:
rintro ⟨z, hz_mem, hzx⟩
    exact ⟨Sᶜ.domRestrict z, mem_image_of_mem Sᶜ.domRestrict hz_mem, z, hz_mem,
      ⟨⟨⟨z, hz_mem, rfl⟩, rfl⟩, hzx⟩⟩

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hl : #J ≤ l + 1
⊢ False

Tactic:
have hlJ : l + 1 = #J := by
          refine Nat.le_antisymm_iff.mpr ⟨?_, hl⟩
          dsimp [l]
          grw [← Nat.sub_add_cancel <| Order.one_le_iff_pos.mpr (Finset.card_pos.mpr hJ),
            Nat.findGreatest_le]
          rfl

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hl : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ False
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed (S.domRestrict '' s)

Tactic:
rw [← Topology.image_snd_preimageImageRestrict]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed (Prod.snd '' ⇑(Homeomorph.preimageImageRestrict α S s) '' (fun x ↦ ↑x) ⁻¹' s)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i

Tactic:
by
  have h_mem := cantorSequence_mem_cantorSet hx n
  rw [cantorSequence_eq_self_sub_sum_cantorToTernary x n] at h_mem
  apply cantorSet_subset_unitInterval at h_mem
  simp only [Set.mem_Icc] at h_mem
  rw [← mul_le_mul_iff_left₀ (show 0 < (3 : ℝ) ^ n by positivity), sub_mul, inv_pow,
    inv_mul_cancel₀ (by simp)]
  linarith!

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case hb
y : ℕ → Bool
x : ℝ := ⋯
this : ofDigits (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = ofDigits fun i ↦ bif y i then 2 else 0
⊢ ∀ (n : ℕ), (bif y n then 2 else 0) ≠ 1

pp: y : ℕ → Bool
x : ℝ := ofDigits fun i ↦ bif y i then 2 else 0
this : (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = fun i ↦ bif y i then 2 else 0
⊢ (cantorToBinary x).get = y

Tactic:
· grind

Goal state after:
y : ℕ → Bool
x : ℝ := ofDigits fun i ↦ bif y i then 2 else 0
this : (cantorToTernary (ofDigits fun i ↦ bif y i then 2 else 0)).get = fun i ↦ bif y i then 2 else 0
⊢ (cantorToBinary x).get = y
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: E : Type u_3
inst✝ : EMetricSpace E
A C : Set E
hC₁ : A ⊆ C
⊢ A.encard ≤ C.encard

Tactic:
exact encard_le_encard hC₁

Goal state after: