mathlib-initiative/mathlib-tactics huggingface dataset:
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₁.repr * ↑(succ n✝) + a₁.repr = ω ^ e₁.repr * ↑(n✝ + 1 + ↑n₂) + a₁.repr - (ω ^ e₁.repr * ↑↑n₂ + a₂.repr)

Tactic:
add_comm,

Goal state after:
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₁.repr * ↑(succ n✝) + a₁.repr = ω ^ e₁.repr * ↑(↑n₂ + (n✝ + 1)) + a₁.repr - (ω ^ e₁.repr * ↑↑n₂ + a₂.repr)
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case inr.inr
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
y z w : ↥x
hyz : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y z
hzw : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) z w
hwy : Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) w y
⊢ Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) y w

Tactic:
· cases mem_wf.asymmetric₃ _ _ _ hyz hzw hwy

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

Goal state before:
pp: case refine_1
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy : y ∈ insert x x
⊢ y ⊆ insert x x

pp: case refine_2
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw : w ∈ insert x x
⊢ y ∈ w

Tactic:
· obtain rfl | hy := mem_insert_iff.1 hy
    on_goal 2 => apply (h.subset_of_mem hy).trans
    all_goals simp_all [subset_def]

Goal state after:
case refine_2
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw : w ∈ insert x x
⊢ y ∈ w
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet

Tactic:
rw [toPSet, PSet.mem_def]

Goal state after:
o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ (∃ b, x.Equiv ((PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet).Func b)) ↔ ∃ a < o, x.Equiv a.toPSet
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ x✝¹.toZFSet ⊂ x✝.toZFSet

Tactic:
rw [ssubset_iff_subset_not_subset]

Goal state after:
x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ x✝¹.toZFSet ⊆ x✝.toZFSet ∧ ¬x✝.toZFSet ⊆ x✝¹.toZFSet
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_2
x : ZFSet.{u}
⊢ x ∈ Set.range toZFSet → x.IsOrdinal

Tactic:
rintro ⟨a, rfl⟩

Goal state after:
case refine_2
a : Ordinal.{u}
⊢ a.toZFSet.IsOrdinal
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (match k, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
| succ m =>

Goal state after:
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 * ω)

Tactic:
le_succ b,

Goal state after:
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 * succ b) ≤ ω ^ (e.repr * ω)

case hc
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
⊢ 0 < ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist (Seq.cons x s) nil = 1

Tactic:
apply dist_eq_one_of_head
  simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
⊢ ∃ f, Function.IsFixedPt F f

Tactic:
have hF : ContractingWith 2⁻¹ F := by
    constructor
    · norm_num
    · exact h

Goal state after:
α : Type u_1
β : Type u_2
F : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α
h : LipschitzWith 2⁻¹ F
hF : ContractingWith 2⁻¹ F
⊢ ∃ f, Function.IsFixedPt F f
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis (left ++ f :: right)

Tactic:
have : WellFormedBasis (f :: right) := cons (h.of_sublist (by simp)) hf_tendsto
    (compare_right_aux (h.of_sublist (by simp)) hf_comp_right)

Goal state after:
left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
this : WellFormedBasis (f :: right)
⊢ WellFormedBasis (left ++ f :: right)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: hd : ℝ → ℝ
tl : Basis
h : WellFormedBasis (hd :: tl)
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
WellFormedBasis,

Goal state after:
hd : ℝ → ℝ
tl : Basis
h : List.Pairwise (fun x y ↦ (Real.log ∘ y) =o[atTop] (Real.log ∘ x)) (hd :: tl) ∧ ∀ f ∈ hd :: tl, Tendsto f atTop atTop
f : ℝ → ℝ
hf : f ∈ tl
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case succ
basis_hd : ℝ → ℝ
basis_tl : Basis
r : ℝ
m : ℕ
⊢ (Multiseries.monomialRpow basis_hd basis_tl (m + 1) r).Sorted

Tactic:
| succ m =>

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

Goal state before:
pp: case cons.succ
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
m : Fin basis_tl.length
⊢ (mk (Multiseries.monomialRpow basis_hd basis_tl (↑m.succ) r) ((basis_hd :: basis_tl)[↑m.succ] ^ r)).Approximates

Tactic:
| succ m =>

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

Goal state before:
pp: m1 m2 : UnitMonomial
h : List.length m1 = List.length m2
⊢ List.length (m1.mul m2) = List.length m1

Tactic:
by
  simp [mul, h]

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

Goal state before:
pp: m1 m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m1 = List.length m2
x : ℝ
⊢ (∀ f ∈ basis, 0 < f x) → (m1.mul m2).toFun basis x = (m1.toFun basis * m2.toFun basis) x

Tactic:
h_pos

Goal state after:
m1 m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length m1 = List.length m2
x : ℝ
h_pos : ∀ f ∈ basis, 0 < f x
⊢ (m1.mul m2).toFun basis x = (m1.toFun basis * m2.toFun basis) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case h₁
basis : Basis
t1 t2 : Monomial
h_basis : WellFormedBasis basis
h1 : List.length t1.unit = List.length basis
h2 : List.length t2.unit = List.length basis
h_coef2 : t2.coef ≠ 0
h_lt : t1.unit < t2.unit
⊢ (fun x ↦ t1.coef) =O[atTop] fun x ↦ t2.coef

Tactic:
simp at h_coef2
    simp
    grind

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
⊢ (S.decode n).encode = n

Tactic:
induction n using Nat.strongRecOn with | _ n ih =>
    unfold S.decode
    dsimp only
    split
    next h =>
      unfold S.encode
      rw [← h, Nat.pair_unpair]
    next h =>
      unfold S.encode
      rw [ih, ih, Nat.sub_add_cancel, Nat.pair_unpair]
      · rwa [Nat.one_le_iff_ne_zero]
      · exact nat_unpair_lt_2 h
      · obtain _ | n' := n
        · exact False.elim (h (by simp))
        · have := Nat.unpair_lt (by lia : 1 ≤ n' + 1)
          lia

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

Goal state before:
pp: a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym (a % ↑b) b = jacobiSym (↑ab') b

Tactic:
hb',

Goal state after:
a : ℤ
b ab' : ℕ
ab r b' : ℤ
hb' : ↑b = b'
hab : a % b' = ab
h : ↑ab' = ab
hr : jacobiSymNat ab' b = r
⊢ jacobiSym (a % b') b = jacobiSym (↑ab') b
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 0 = ∅

Tactic:
simp only [Iio_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 1 = {0}

Tactic:
simp only [Iio_ofNat]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 2 = {0, 1}

Tactic:
simp only [Iio_ofNat]

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

Goal state before:
pp: case inr.mp
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f)) → Tendsto F ℱ (𝓝 f)

Tactic:
intro H

Goal state after:
case inr.mp
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
⊢ Tendsto F ℱ (𝓝 f)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
⊢ Tendsto F ℱ (𝓝 f) → Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
intro H

Goal state after:
case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : ContinuousMul G
⊢ Function.Injective toFiniteIndexNormalSubgroup

Tactic:
intro H

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : ContinuousMul G
H : OpenNormalSubgroup G
⊢ ∀ ⦃a₂ : OpenNormalSubgroup G⦄, H.toFiniteIndexNormalSubgroup = a₂.toFiniteIndexNormalSubgroup → H = a₂
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case h₀
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ (map Sigma.fst (List.toFinmap' (xs₀.zip xs₁))).Nodup

Tactic:
hperm.nodup_iff

Goal state after:
case h₀
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))
hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
⊢ (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: case e'_3
𝕜 : 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
hB_inj : Function.Injective ⇑B
⊢ inst = TopologicalSpace.induced (DFunLike.coe ∘ ⇑B) Pi.topologicalSpace

Tactic:
exact hB.eq_induced

Goal state after:
Module: Mathlib.Topology.DerivedSet

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

Tactic:
eq_comm

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ U = derivedSet U ↔ U = derivedSet U
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s P : Set X
hP : Perfect P
hPs : P ⊆ s
⊢ P ⊆ perfectKernel s

Tactic:
by
  refine Set.subset_iInter fun i => ?_
  simpa [iteratedDerivedSet_constant_iff_preperfect.mp hP.acc i] using
    iteratedDerivedSet_mono hPs i

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
inst✝ : WellFoundedLT I
x : ↑(π C fun x ↦ x ∈ s)
l : List I := s.sort fun x1 x2 ↦ x1 ≥ x2
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
⊢ (e (π C fun x ↦ x ∈ s) a * 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:
rw [hmap]
      exact finsuppSum_mem_span_eval _ _ ha hc

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
⊢ WellFoundedLT (Products I)

Tactic:
by
  have : (· < · : Products I → _ → _) = (fun l m ↦ List.Lex (· < ·) l.val m.val) := by
    ext; exact lt_iff_lex_lt _ _
  rw [WellFoundedLT, this]
  dsimp [Products]
  rw [(by rfl : (· > · : I → _) = flip (· < ·))]
  infer_instance

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}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
⊢ eval C l ∈ Submodule.span ℤ (eval C '' {m | m < l})

Tactic:
suffices eval C l = 0 by simp [this]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
l : Products I
o : Ordinal.{u}
h : isGood C l
hsC : contained C o
i : I
hi : i ∈ ↑l
h' : ¬ord I i < o
⊢ eval C l = 0
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
l : ℕ
i : cell C l
hi : i ∈ {x | ↑l < n}
⊢ closedCell l ↑⟨i, hi⟩ ⊆ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
apply subset_iUnion₂_of_subset l hi

Goal state after:
X : Type u_1
t : TopologicalSpace X
C✝ D✝ : Set X
inst✝¹ : T2Space X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
l : ℕ
i : cell C l
hi : i ∈ {x | ↑l < n}
⊢ closedCell l ↑⟨i, hi⟩ ⊆ ⋃ j, closedCell l j
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:
← Nat.cast_add,

Goal state after:
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✝
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ s_1 ∈ L '' ↑s, MapsTo (⇑f) s_1 (⋃₀ t)

Tactic:
forall_mem_image

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
S : Set (Set X)
T : Set (Set Y)
hS₁ : ∀ K ∈ S, IsCompact K
hT : IsTopologicalBasis T
hS₂ : ∀ (f : C(X, Y)) (x : X), ∀ V ∈ T, f x ∈ V → ∃ K ∈ S, K ∈ 𝓝 x ∧ MapsTo (⇑f) K V
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Y
hU : IsOpen[inst✝] U
hfKU : MapsTo (⇑f) K U
t : Set (Set Y)
htT : t ⊆ T
htf : t.Finite
hTU : ∀ V ∈ t, V ⊆ U
hKT : K ⊆ ⇑f ⁻¹' ⋃₀ t
L : X → Set X
hLS : ∀ x ∈ K, L x ∈ S
hLmem : ∀ x ∈ K, L x ∈ 𝓝 x
hLt : ∀ x ∈ K, MapsTo (⇑f) (L x) (⋃₀ t)
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hs : K ⊆ ⋃ x ∈ s, L x
⊢ ∀ ⦃x : X⦄, x ∈ ↑s → MapsTo (⇑f) (L x) (⋃₀ t)
Module: Mathlib.Topology.ContinuousMap.T0Sierpinski

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsInducing ⇑(productOfMemOpens X)

Tactic:
convert! inducing_iInf_to_pi fun (u : Opens X) (x : X) => x ∈ u
  apply eq_induced_by_maps_to_sierpinski

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

Goal state before:
pp: θ : ↑I
⊢ 1 + ↑θ ≤ 2

Tactic:
add_comm,

Goal state after:
θ : ↑I
⊢ ↑θ + 1 ≤ 2
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: ⊢ ¬(cocompact ℚ).IsCountablyGenerated

Tactic:
intro H

Goal state after:
H : (cocompact ℚ).IsCountablyGenerated
⊢ False
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ cantorStep x ∈ cantorSet

Tactic:
by
  simp only [cantorStep]
  obtain ⟨y, hy, rfl | rfl⟩ : ∃ y ∈ cantorSet, y / 3 = x ∨ (2 + y) / 3 = x := by
    rw [cantorSet_eq_union_halves] at hx
    grind
  all_goals
    grind [cantorSet_subset_unitInterval]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_1.cons
α : Type u_1
inst✝ : TopologicalSpace α
as : List α
a : α
l : List α
ih : pure l ≤ traverse 𝓝 l
⊢ pure (a :: l) ≤ traverse 𝓝 (a :: l)

Tactic:
| cons a l ih =>

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
⊢ List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) u v

Tactic:
refine List.Forall₂.flip ?_

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hv : List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) l v
hvs : sequence v ⊆ s
this : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
⊢ List.Forall₂ (flip fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) v u
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ Function.RightInverse (fun y ↦ ⟨ofDigits fun i ↦ bif y i then 2 else 0, ⋯⟩) fun x ↦
    match (motive := ↑cantorSet → ℕ → Bool) x with
    | ⟨x, h⟩ => (cantorToBinary x).get

Tactic:
intro y
    simp only [Fin.isValue]
    set x := @ofDigits 3 (fun i ↦ cond (y i) 2 0)
    have := ofDigits_cantorToTernary (ofDigits_bool_to_fin_three_mem_cantorSet y)
    apply ofDigits_zero_two_sequence_unique at this
    rotate_left
    · exact fun n ↦ cantorToTernary_ne_one
    · grind
    ext n
    apply congrFun (a := n) at this
    grind [cantorToTernary, Stream'.get_map]

Goal state after:
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap (Prod.map f id)

Tactic:
intro H

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ∧ IsClosedMap (Prod.map f id) → IsProperMap f

Tactic:
intro H

Goal state after:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ IsClosedMap (Prod.map f id)
⊢ IsProperMap f
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

Tactic:
intro H

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)) → IsProperMap f

Tactic:
intro H

Goal state after:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ IsProperMap f
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (f i) x z ≤ (f i) x y → ∃ b ∈ s, (f i) x z ≤ (f b) x y

Tactic:
intro H

Goal state after:
case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) x y
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) x y
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (f i) x z ≤ (f i) y z → ∃ b ∈ s, (f i) x z ≤ (f b) y z

Tactic:
intro H

Goal state after:
case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
H : (f i) x z ≤ (f i) y z
⊢ ∃ b ∈ s, (f i) x z ≤ (f b) y z
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A C : Set X
ε : ℝ≥0
h_subset : C ⊆ A
h_sep : IsSeparated (↑ε) C
h : packingNumber ε A ≠ ⊤
⊢ C.encard ≤ packingNumber ε A

Tactic:
exact le_iSup_of_le C <| le_iSup_of_le h_subset <| le_iSup_of_le h_sep (by simp)

Goal state after: