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

Goal state before:
pp: case single_add.hxb
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ (single e x + f) e = x

Tactic:
add_apply,

Goal state after:
case single_add.hxb
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : (∀ (e : Ordinal.{u_1}), f e < b) → coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ (single e x) e + f e = x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b : Ordinal.{u_1}
hb : 1 < b
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ (e : Ordinal.{u_1}), f e < b
⊢ coeff b (eval b f) = f

Tactic:
by
  induction f using Finsupp.induction_on_max with
  | zero => simp
  | single_add e x f hf' hx IH =>
    have IH' (e') : f e' < b := by
      by_cases he' : e' ∈ f.support
      · apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne
      · rw [notMem_support_iff.1 he']
        exact hb.pos
    rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']
    · apply (hf e).trans_eq'
      rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
      exact fun h ↦ (hf' _ h).false
    · exact eval_lt IH' hf'

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

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ = a ↔ ω ^ x = veblen x.invVeblen₁ a

Tactic:
by
  rw [← veblen_inj (o := x.invVeblen₁), veblen_invVeblen₁_invVeblen₂]

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

Goal state before:
pp: p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ ∀ (x : ZFSet.{u}), (∀ y ∈ x, Hereditarily p y → p ∅) → Hereditarily p x → p ∅

Tactic:
intro y

Goal state after:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
⊢ (∀ y_1 ∈ y, Hereditarily p y_1 → p ∅) → Hereditarily p y → p ∅
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ ∀ ⦃y : ZFSet.{u}⦄, (∃ i, y ∈ f i) → y.rank < ⨆ i, (f i).rank

Tactic:
intro y

Goal state after:
case a
α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
y : ZFSet.{u}
⊢ (∃ i, y ∈ f i) → y.rank < ⨆ i, (f i).rank
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
⊢ (o₁ ^ o₂).NF

Tactic:
have h' : o₂ ≠ zero := fun he => h (he ▸ zero_def ▸ rfl)

Goal state after:
case neg
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : ¬o₂ = 0
h' : o₂ ≠ zero
⊢ (o₁ ^ o₂).NF
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case neg.convert_5
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
h' : Seq.cons x s ≠ Seq.cons x t
h_if : ¬some x :: ↑s = some x :: ↑t
⊢ ¬¬(some x :: ↑s) 0 = (some x :: ↑t) 0

Tactic:
simp [Stream'.cons]

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

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

Tactic:
rw [dist_comm]

Goal state after:
α : Type u_1
x : α
s : Stream'.Seq α
⊢ dist (Seq.cons x s) nil = 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case h
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

Tactic:
grind [WellFormedBasis, List.pairwise_cons]

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

Goal state before:
pp: basis : Basis
⊢ Sorted 0

Tactic:
cases basis with
  | nil => constructor
  | cons => apply Sorted.nil

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ e = ↑r

Tactic:
he.out,

Goal state after:
e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ ↑e' = ↑r
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
h₀ : (x' :: xs).Nodup
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
head✝ : α
tail✝ : List α
h₁ : (x' :: xs).length = (head✝ :: tail✝).length
⊢ applyId ((x' :: xs).zip (head✝ :: tail✝)) x = y ↔ (head✝ :: tail✝)[n✝ + 1]? = some y

Tactic:
obtain - | ⟨h₀, h₁⟩ := h₀
        simp only [getElem?_cons_succ, zip_cons_cons, applyId_cons] at h₂ ⊢
        rw [if_neg]
        · apply xs_ih <;> solve_by_elim [Nat.succ.inj]
        · apply h₀; apply List.mem_of_getElem? h₂

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ ∀ (x_1 : α), (x, x_1) ∉ xs.zip ys

Tactic:
intro y

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
y : α
⊢ (x, y) ∉ xs.zip ys
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
⊢ [MapClusterPt x atTop fun x ↦ y ^ x, MapClusterPt x atTop fun x ↦ y ^ x, x ∈ closure[inst✝²] (range fun x ↦ y ^ x),
      x ∈ closure[inst✝²] (range fun x ↦ y ^ x)].TFAE

Tactic:
tfae_have 4 → 1 := by
    refine fun h ↦ closure_minimal ?_ isClosed_setOfPred_clusterPt h
    exact range_subset_iff.2 (mapClusterPt_self_zpow_atTop_pow _)

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
tfae_4_to_1 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → MapClusterPt x atTop fun x ↦ y ^ x
⊢ [MapClusterPt x atTop fun x ↦ y ^ x, MapClusterPt x atTop fun x ↦ y ^ x, x ∈ closure[inst✝²] (range fun x ↦ y ^ x),
      x ∈ closure[inst✝²] (range fun x ↦ y ^ x)].TFAE
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : v x < 1
⊢ ∀ (i : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ), ∃ a, ∀ (b : ℕ), a ≤ b → v.restrict x ^ b < ↑i

Tactic:
intro y

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : v x < 1
y : (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ
⊢ ∃ a, ∀ (b : ℕ), a ≤ b → v.restrict x ^ b < ↑y
Module: Mathlib.Topology.Category.TopCat.Sphere

Goal state before:
pp: n : ℕ
⊢ CompactSpace ↑(𝔻 n)

Tactic:
by
  convert! Homeomorph.compactSpace Homeomorph.ulift.symm
  infer_instance

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

Goal state before:
pp: n : ℕ
⊢ CompactSpace ↑(∂𝔻 n)

Tactic:
by
  convert! Homeomorph.compactSpace Homeomorph.ulift.symm
  infer_instance

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ perfectKernel s = sᵈ[a]

Tactic:
refine le_antisymm (perfectKernel_subset_iteratedDerivedSet s a) ?_

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ sᵈ[a] ⊆ perfectKernel s
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ IsGeneratedBy X PUnit.{v + 1}

Tactic:
iff_le_generatedBy

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
⊢ instTopologicalSpacePUnit ≤ TopologicalSpace.generatedBy X
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
⊢ 1 ≠ 0

Tactic:
by exact one_ne_zero

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
⊢ ∃ a ∈ ↑l, (LocallyConstant.evalMonoidHom x) (e C a) = 0

Tactic:
convert! h with i

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : Products I
x : ↑C
h : ∃ i ∈ ↑l, ↑x i ≠ true
i : I
⊢ (LocallyConstant.evalMonoidHom x) (e C i) = 0 ↔ ↑x i ≠ true
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

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

Tactic:
intro y

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
y : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
⊢ (Linear_CC' C hsC ho) ((πs C o) y) = 0
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
x : ↑C
h' : (∀ i ∈ ↑l, ↑x i = true) ∧ True
⊢ ord I i < o

Tactic:
exact hsC x.val x.prop i (h'.1 i hi)

Goal state after:
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}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant ↑C ℤ
⊢ p ∈ range C ↔ p ∈ ⋃ e, smaller C ↑e

Tactic:
simp only [smaller, range, Set.mem_iUnion, Set.mem_image, Set.mem_range, Subtype.exists]

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
hsC : contained C o
p : LocallyConstant ↑C ℤ
⊢ (∃ a, ∃ (b : Products.isGood C a), eval C ⟨a, b⟩ = p) ↔
    ∃ a,
      ∃ (h : a < o),
        ∃ x,
          (∃ a_1,
              ∃ (h_1 : Products.isGood (π C fun x ↦ ord I x < a) a_1), eval (π C fun x ↦ ord I x < a) ⟨a_1, ⋯⟩ = x) ∧
            (πs C a) x = p
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
⊢ ∀ (y : ConnectedComponents Y), Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))

Tactic:
intro y

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : Finite (ConnectedComponents Y)
hfc : Continuous f
h : ∀ (y : Y), (f ⁻¹' {y}).Finite
y : ConnectedComponents Y
⊢ Finite (ConnectedComponents ↑(f ⁻¹' mk ⁻¹' {y}))
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
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l

Tactic:
← List.cons_head!_tail h,

Goal state after:
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
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ((↑↑q).head! :: (↑↑q).tail) ↑↑l
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
F✝ : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F✝
A : Set E
f : E → F✝
hf : IsInducing f
hs : IsCountablyCompact (f '' A)
F : Filter E
F_ne_bot : F.NeBot
Fc : F.IsCountablyGenerated
F_le : F ≤ 𝓟 A
⊢ ∃ a ∈ A, ClusterPt a F

Tactic:
obtain ⟨_, ⟨x, x_in : x ∈ A, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)

Goal state after:
E : Type u_2
F✝ : Type u_3
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace F✝
A : Set E
f : E → F✝
hf : IsInducing f
hs : IsCountablyCompact (f '' A)
F : Filter E
F_ne_bot : F.NeBot
Fc : F.IsCountablyGenerated
F_le : F ≤ 𝓟 A
x : E
x_in : x ∈ A
hx : ClusterPt (f x) (map f F)
⊢ ∃ a ∈ A, ClusterPt a F
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf✝ : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
hf : F g ∈ A
⊢ F g ∈ comp Subtype.val M '' F ⁻¹' A

Tactic:
exact ⟨g, hf, rfl⟩

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

Goal state before:
pp: case pos
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hAU : A ⊆ ⋃ i, U i
h : Nonempty ι
f : ℕ → ι
hf : A ⊆ ⋃ n, U (f n)
⊢ ∃ t, A ⊆ ⋃ i ∈ t, U i

Tactic:
obtain ⟨t, ht⟩ := isCountablyCompact_iff_countable_open_cover.1 hA (U ∘ f)
      (fun n => hUo (f n)) hf

Goal state after:
case pos
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : IsCountablyCompact A
hl : IsLindelof A
ι : Type u_2
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝] (U i)
hAU : A ⊆ ⋃ i, U i
h : Nonempty ι
f : ℕ → ι
hf : A ⊆ ⋃ n, U (f n)
t : Finset ℕ
ht : A ⊆ ⋃ i ∈ t, (U ∘ f) i
⊢ ∃ t, A ⊆ ⋃ i ∈ t, U i
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f
h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y
x : X
hx : x ∈ A
⊢ ∀ (x : X), (P x ↑f ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x ↑g

Tactic:
intro y

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f g : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f
h : ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, g y = f y
x : X
hx : x ∈ A
y : X
⊢ (P y ↑f ∧ ∀ᶠ (x : X) in 𝓝 y, g x = f x) → P y ↑g
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
⊢ IsGeneratedBy X ↑F

Tactic:
by
  let W (a : Σ (i : ι), C(X i, Y)) : TopologicalSpace.Closeds (X a.1) :=
    ⟨a.2 ⁻¹' F, IsClosed.preimage a.2.continuous hF⟩
  let g (a) : W a → F := F.restrictPreimage a.2
  have hg (a) : Continuous (g a) := a.2.continuous.restrictPreimage
  suffices ∀ (V : Set F), (∀ a, IsClosed ((g a) ⁻¹' V)) → IsClosed V by
    constructor
    rw [continuous_iff_isClosed]
    exact fun _ hV ↦ this _ (fun a ↦ IsClosed.preimage
      ((IsGeneratedBy.equiv_symm_comp_continuous_iff X _).2 (hg a)) hV)
  intro V hV
  obtain ⟨V, hV, rfl⟩ : ∃ (T : Set Y), T ⊆ F ∧ V = Subtype.val ⁻¹' T :=
    ⟨Subtype.val '' V, by simp, by simp⟩
  refine IsClosed.preimage continuous_subtype_val ?_
  rw [IsGeneratedBy.isClosed_iff X]
  intro i f
  convert! (W ⟨i, f⟩).isClosed.isClosedMap_subtype_val _ (hV ⟨i, f⟩)
  aesop

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.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
y : M → ↑I
x✝ : y ∈ Cube.boundary M
m : M
hm : y m = 0 ∨ y m = 1
⊢ ((↑p).comp { toFun := fun t n ↦ t (e.symm n), continuous_toFun := ⋯ }) y = x

Tactic:
by
    simpa using p.2 _ ⟨e m, by simpa using hm⟩

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

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ ∃ y ∈ cantorSet, y / 3 = x ∨ (2 + y) / 3 = x

Tactic:
rw [cantorSet_eq_union_halves] at hx

Goal state after:
x : ℝ
hx : x ∈ (fun x ↦ x / 3) '' cantorSet ∪ (fun x ↦ (2 + x) / 3) '' cantorSet
⊢ ∃ y ∈ cantorSet, y / 3 = x ∨ (2 + y) / 3 = x
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

Goal state after:
y : ℕ → Bool
⊢ (fun x ↦
        match (motive := ↑cantorSet → ℕ → Bool) x with
        | ⟨x, h⟩ => (cantorToBinary x).get)
      ((fun y ↦ ⟨ofDigits fun i ↦ bif y i then 2 else 0, ⋯⟩) y) =
    y
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 := ⋯
l : ℕ := ⋯
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
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hts : edist t s ≤ c
x✝ : ℕ
⊢ P x✝ ↔ t ∈ (logSizeBallSeq J hJ a c x✝).finset ∧ s ∈ (logSizeBallSeq J hJ a c x✝).finset

Tactic:
simp [P, and_comm]

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
ε : ℝ≥0
A : Set X
⊢ packingNumber ε A ≤ A.encard

Tactic:
simp only [packingNumber, iSup_le_iff]
  exact fun _ hC _ ↦ encard_le_encard hC

Goal state after:
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := fun n ↦ 2⁻¹ ^ n
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋂ n, closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (⋃ m, ⋃ (_ : m ≥ n), ↑(s m))
t : Closeds α := { carrier := t0, isClosed' := ⋯ }
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ hausdorffEDist ↑(s (n + l)) ↑(s (n + l + 1)) < 2⁻¹ ^ (n + l)

Tactic:
apply hs

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := ⋯
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋯
t : Closeds α := ⋯
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ n + l ≤ n + l

case a
α : Type u_1
β : Type u_2
inst✝² : EMetricSpace α
inst✝¹ : EMetricSpace β
s✝ : Set α
inst✝ : CompleteSpace α
B : ℕ → ℝ≥0∞ := ⋯
B_pos : ∀ (n : ℕ), 0 < B n
B_ne_top : ∀ (n : ℕ), B n ≠ ∞
s : ℕ → Closeds α
hs : ∀ (N n m : ℕ), N ≤ n → N ≤ m → edist (s n) (s m) < B N
t0 : Set α := ⋯
t : Closeds α := ⋯
n : ℕ
x : α
hx : x ∈ s n
l : ℕ
z : ↥(s (n + l))
⊢ n + l ≤ n + l + 1
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: E : Type u_3
inst✝ : EMetricSpace E
A : Set E
⊢ coveringNumber 0 A = A.encard

Tactic:
refine le_antisymm (coveringNumber_le_encard_self A) ?_
  rw [← externalCoveringNumber_zero]
  exact externalCoveringNumber_le_coveringNumber 0 A

Goal state after:
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
h_nonempty : A.Nonempty
hA : ediam A ≤ ↑ε
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
exact (externalCoveringNumber_le_coveringNumber ε A).trans_eq
      (coveringNumber_eq_one_of_ediam_le h_nonempty hA)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case h
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
i : ι
⊢ ‖↑(f a₀) i‖ ≤ ‖f a₀‖

Tactic:
exact lp.norm_apply_le_norm top_ne_zero (f a₀) i

Goal state after:
Module: Mathlib.Topology.MetricSpace.Kuratowski

Goal state before:
pp: case inr.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ∞
f_ext' : α → ↥(lp (fun x ↦ ℝ) ∞) := fun i ↦ ⟨swap g i, ⋯⟩
⊢ EqOn f f_ext' s

Tactic:
intro a hyp

Goal state after:
case inr.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
ι : Type u_1
f : α → ↥(lp (fun x ↦ ℝ) ∞)
K : ℝ≥0
hfl : ∀ (i : ι), LipschitzOnWith K (fun a ↦ ↑(f a) i) s
g : ι → α → ℝ
hgl : ∀ (i : ι), LipschitzWith K (g i)
hgeq : ∀ (i : ι), EqOn (fun x ↦ ↑(f x) i) (g i) s
a₀ : α
ha₀_in_s : a₀ ∈ s
hf_extb : ∀ (a : α), Memℓp (swap g a) ∞
f_ext' : α → ↥(lp (fun x ↦ ℝ) ∞) := fun i ↦ ⟨swap g i, ⋯⟩
a : α
hyp : a ∈ s
⊢ f a = f_ext' a
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: case right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * maxVar X Y) * dist (x, y) (z, t)

Tactic:
rw [dist_comm]

Goal state after:
case right
X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : ProdSpaceFun X Y
fA : f ∈ candidates X Y
x y z t : X ⊕ Y
⊢ f (z, t) - f (x, y) ≤ ↑(2 * maxVar X Y) * dist (z, t) (x, y)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist s t

Tactic:
rw [dist_comm]

Goal state after:
α : Type u_1
inst✝ : MetricSpace α
x : α
s t : NonemptyCompacts α
⊢ infDist x ↑s ≤ infDist x ↑t + dist t s
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ⨅ C, ⨅ (_ : HolderWith C r (Function.const X c)), ↑C = ⊥

Tactic:
iInf₂_eq_bot

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : HolderWith i r (Function.const X c)), ↑i < b