mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
⊢ Seq.destruct ms = some ((exp, coef), tl)

Tactic:
rw [destruct_eq_destruct_map, h]

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
⊢ Option.map
      (fun x ↦
        match x with
        | (exp, coef, tl) => ((exp, coef), tl))
      (some (exp, coef, tl)) =
    some ((exp, coef), tl)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
⊢ (op (opf s)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match h_opf.unfold s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))

Tactic:
have hF := h_opf.destruct_apply_eq_unfold (s := s)

Goal state after:
case h
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
hF :
  (opf s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (h_opf.unfold s.head)
⊢ (op (opf s)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match h_opf.unfold s.head with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.cons.rel
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
exp2 : ℝ
m2 : List ℝ
h2 : (exp2 :: m2).length = (basis_hd :: basis_tl).length
h : exp1 < exp2
⊢ toFun (exp1 :: m1) (basis_hd :: basis_tl) =o[atTop] toFun (exp2 :: m2) (basis_hd :: basis_tl)

Tactic:
| rel h =>

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: a b : ℕ
h : a ≠ 0
this : a ≤ a * a
⊢ b < if a < b then b * b + a else a * a + a + b

Tactic:
have := Nat.le_mul_self b

Goal state after:
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
⊢ b < if a < b then b * b + a else a * a + a + b
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: n : ℕ
h : (Nat.unpair n).1 ≠ 0
⊢ (Nat.unpair n).2 < n

Tactic:
by
  obtain ⟨⟨a, b⟩, rfl⟩ := Nat.pairEquiv.surjective n
  simp only [Nat.pairEquiv_apply, Function.uncurry_apply_pair, Nat.unpair_pair] at *
  unfold Nat.pair
  have := Nat.le_mul_self a
  have := Nat.le_mul_self b
  split <;> lia

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

Goal state before:
pp: ⊢ fastGrowingε₀ 0 = 1

Tactic:
simp [fastGrowingε₀]

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

Goal state before:
pp: case lt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.lt
⊢ Ordering.lt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp only [h] at this

Goal state after:
case lt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.lt
this : Ordering.lt.Compares a b
⊢ Ordering.lt.Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.eq
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp only [h] at this

Goal state after:
case eq
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
this : (a.cmp b).Compares a b
h : a.cmp b = Ordering.gt
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩

Tactic:
simp only [h] at this

Goal state after:
case gt
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.gt
this : Ordering.gt.Compares a b
⊢ Ordering.gt.Compares ⟨a, ha⟩ ⟨b, hb⟩
Module: Mathlib.Tactic.NormNum.IsCoprime

Goal state before:
pp: x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬IsCoprime x y

Tactic:
rw [Int.isCoprime_iff_gcd_eq_one, hd]

Goal state after:
x y : ℤ
d : ℕ
hd : x.gcd y = d
h : d.beq 1 = false
⊢ ¬d = 1
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case 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)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
i : ℕ
h₂ : (x' :: xs)[i]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[i]? = some y

Tactic:
cases i

Goal state after:
case cons.zero
α : 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)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
h₂ : (x' :: xs)[0]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[0]? = some y

case cons.succ
α : 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)
ys : List α
h₀ : (x' :: xs).Nodup
h₁ : (x' :: xs).length = ys.length
n✝ : ℕ
h₂ : (x' :: xs)[n✝ + 1]? = some x
⊢ applyId ((x' :: xs).zip ys) x = y ↔ ys[n✝ + 1]? = some y
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
𝓕₁ : Filter E := 𝓝 0
V_mem : V ∈ 𝓕₁
𝓕₂ : Filter E := 𝓝 0
H : 𝓕₁ = 𝓕₂ ⊓ 𝓟 V
this : V ∈ 𝓕₂
⊢ 𝓕₁ = 𝓕₂

Tactic:
simpa [H]

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

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

Tactic:
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 B : Set X
⊢ derivedSet (A ∪ B) = derivedSet A ∪ derivedSet B

Tactic:
ext x
  simp [derivedSet, ← sup_principal, accPt_sup]

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, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)

Tactic:
have := RelCWComplex.mapsTo n i

Goal state after:
X : Type u_1
t : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
n : ℕ
i : cell C n
this : ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (∅ ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
⊢ ∃ I, MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, ↑(map m j) '' closedBall 0 1)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst✝² : (i : I) → Decidable (J i)
inst✝¹ : (i : I) → Decidable (K i)
inst✝ : (i : I) → Decidable (L i)
hJK : ∀ (i : I), J i → K i
hKL : ∀ (i : I), K i → L i
⊢ ProjRestricts C hJK ∘ ProjRestricts C hKL = ProjRestricts C ⋯

Tactic:
by
  ext x i
  simp only [π, Proj, Function.comp_apply, ProjRestricts_coe]
  simp_all

Goal state after:
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}
⊢ Mono (ModuleCat.ofHom (πs C o))

Tactic:
rw [ModuleCat.mono_iff_injective]
  exact injective_πs _ _

Goal state after:
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
l : Products I
⊢ l ∈ GoodProducts C ↔ l ∈ GoodProducts (π C fun x ↦ ord I x < o) ∪ MaxProducts C ho

Tactic:
simp only [GoodProducts, MaxProducts, Set.mem_union, Set.mem_ofPred_eq]

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
l : Products I
⊢ Products.isGood C l ↔ Products.isGood (π C fun x ↦ ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case h.true
S : Profinite
C : { C // IsClopen C }
⊢ IsOpen ((fun a ↦ decide (a ∈ ↑C)) ⁻¹' {true})

Tactic:
· refine IsClopen.isOpen ?_
      convert! C.2
      ext x
      simp only [Set.mem_preimage, Set.mem_singleton_iff, decide_eq_true_eq]

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

Goal state before:
pp: 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 ∈ A, AccPt a (𝓟 B)

Tactic:
obtain ⟨a, haA, hac⟩ :=
    IsCountablyCompact.seq_clusterPt hA x (Eventually.of_forall (fun n => hBA (f n).2))

Goal state after:
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
⊢ ∃ a ∈ A, AccPt a (𝓟 B)
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
x : X
P : (x : X) → (𝓝 x).Germ Y → Prop
hf : RestrictGermPredicate P A x ↑f
h : ∀ᶠ (z : X) in 𝓝ˢ A, g z = f z
hx : x ∈ A
⊢ ∀ (x : X), (P x ↑f ∧ ∀ᶠ (x : X) in 𝓝 x, g x = f x) → P x ↑g

Tactic:
rintro y ⟨hy, h'y⟩

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

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
x : Option α
r : ℝ≥0∞
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' Metric.eball none r)

Tactic:
apply discreteTopology_iff_forall_isOpen.mp
      rw [ball_infty_of_pos ENNReal.zero_lt_top]
      exact Subsingleton.discreteTopology

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

Goal state before:
pp: case map_one_left
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (x : X × Y), { toFun := G, continuous_toFun := hG }.toFun (1, x) = (ContinuousMap.id (X × Y)) x

pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      {
            toFun := fun x ↦
              { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ?map_one_left }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
          x

Tactic:
· rintro ⟨x, y⟩
      exact Prod.ext (HSpace.hmulE.1.3 x) (HSpace.hmulE.1.3 y)

Goal state after:
case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
          x
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 2 * ↑t

Tactic:
Set.projIcc_of_mem _ ((mul_pos_mem_iff zero_lt_two).2 _)

Goal state after:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑⟨2 * ↑t, ⋯⟩ = 2 * ↑t

t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑t ∈ Set.Icc 0 (1 / 2)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero
⊢ preCantorSet (0 + 1) ⊆ preCantorSet 0

Tactic:
grind [preCantorSet_zero, preCantorSet_succ]

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

Goal state before:
pp: case succ
n✝ : ℕ
a✝ : preCantorSet (n✝ + 1) ⊆ preCantorSet n✝
⊢ preCantorSet (n✝ + 1 + 1) ⊆ preCantorSet (n✝ + 1)

Tactic:
grind [preCantorSet_zero, preCantorSet_succ]

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
x : ↑(Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s)
⊢ reorderRestrictProd S s (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i) = ↑x

Tactic:
by
  ext; simp [reorderRestrictProd]

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 α)
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
hv : (∀ a ∈ v, IsOpen[inst✝] a) ∧ List.Forall₂ Membership.mem v l
⊢ (∀ a ∈ v, IsOpen[inst✝] a) ∧ List.Forall₂ Membership.mem v u

Tactic:
exact ⟨hv.1, hu.flip⟩

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
⊢ Tendsto f (𝓝 (a :: l)) b ↔ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b

Tactic:
have : 𝓝 (a::l) = (𝓝 a ×ˢ 𝓝 l).map fun p : α × List α => p.1::p.2 := by
    simp only [nhds_cons, Filter.prod_eq, (Filter.map_def _ _).symm,
      (Filter.seq_eq_filter_seq _ _).symm]
    simp [-Filter.map_def, Function.comp_def, functor_norm]
  rw [this, Filter.tendsto_map'_iff]; rfl

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α), ContinuousAt length l

Tactic:
simp only [ContinuousAt, nhds_discrete]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
⊢ ∀ (l : List α), Tendsto length (𝓝 l) (pure l.length)
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y : X
⊢ d x y ⊔ d' x y = d y x ⊔ d' y x

Tactic:
by simp [d.symm, d'.symm]

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

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

Tactic:
Set.mem_ofPred

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

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

Tactic:
Set.mem_ofPred

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

Goal state before:
pp: case mpr.refine_3
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
a₁ a₂ : ↑(Ω^ N X x)
H : ((genLoopEquivOfUnique N) a₁).Homotopy ((genLoopEquivOfUnique N) a₂)
y : N → ↑I
⊢ { toFun := fun tx ↦ H (tx.1, tx.2 default), continuous_toFun := ⋯ }.toFun (1, y) = ↑a₂ y

Tactic:
exact (H.apply_one _).trans (congr_arg a₂ (eq_const_of_unique y).symm)

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))
⊢ ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l

Tactic:
obtain ⟨z', z'_mem, hz'⟩ : ∃ z' ∈ s (n + l + 1), edist (z : α) z' < B n / 2 ^ l := by
          refine exists_edist_lt_of_hausdorffEDist_lt (s := s (n + l)) z.2 ?_
          simp only [ENNReal.inv_pow, div_eq_mul_inv]
          rw [← pow_add]
          apply hs <;> simp

Goal state after:
α : 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))
z' : α
z'_mem : z' ∈ s (n + l + 1)
hz' : edist (↑z) z' < B n / 2 ^ l
⊢ ∃ z', edist ↑z ↑z' ≤ B n / 2 ^ l
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (min (⨅ (_ : y ≠ z), edist y z) {z}.einfsep) =
    min (min (edist x y) (edist x z)) (edist y z)

Tactic:
einfsep_singleton,

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
x y z : α
hxy : x ≠ y
hyz : y ≠ z
hxz : x ≠ z
⊢ min (min (⨅ (_ : x ≠ y), edist x y) (⨅ (_ : x ≠ z), edist x z)) (min (⨅ (_ : y ≠ z), edist y z) ∞) =
    min (min (edist x y) (edist x z)) (edist y z)
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝¹ : EMetricSpace α
s : Set α
inst✝ : Finite ↑s
⊢ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
by
  rw [← einfsep_pos]
  exact einfsep_pos_of_finite

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → x✝ ≤ dist x y) ↔ x✝ ≤ ⨅ d, uncurry dist ↑d

Tactic:
le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb,

Goal state after:
case pos
α : Type u_1
inst✝¹ : PseudoMetricSpace α
s : Set α
inst✝ : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x✝ : ℝ
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → x✝ ≤ dist x y) ↔ ∀ i ∈ s.offDiag, x✝ ≤ uncurry dist i
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝² : PseudoMetricSpace α
s : Set α
inst✝¹ : Decidable s.Nontrivial
inst✝ : Fintype ↑s
⊢ s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
by
  split_ifs with hs
  · refine eq_of_forall_le_iff fun _ => ?_
    simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]
  · rw [not_nontrivial_iff] at hs
    exact hs.infsep_zero

Goal state after:
Module: Mathlib.Topology.Order.ScottTopology

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst✝⁴, inst✝²] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
hb : b ∈ upperBounds (f '' t)
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
⊢ False

Tactic:
simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂,
      mem_ofPred] at hb

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder β
inst✝² : TopologicalSpace β
inst✝¹ : IsScott β univ
f : α → β
D : Set (Set α)
inst✝ : IsScott α D
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : Continuous[inst✝⁴, inst✝²] f
t : Set α
h₀ : t ∈ D
d₁ : t.Nonempty
d₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) t
a : α
d₃ : IsLUB t a
b : β
h : ¬f a ≤ b
u : Set β := (Iic b)ᶜ
hu : IsUpperSet (f ⁻¹' u) ∧ DirSupInaccOn D (f ⁻¹' u)
c : α
hcd : c ∈ t
hfcb : c ∈ f ⁻¹' u
hb : ∀ a ∈ t, f a ≤ b
⊢ False
Module: Mathlib.Topology.OmegaCompletePartialOrder

Goal state before:
pp: case left
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (i : ℕ), c i ≤ ωSup c

Tactic:
apply le_ωSup

Goal state after:
Module: Mathlib.Topology.Order.Completion

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace (DedekindCut α)
inst✝ : OrderTopology (DedekindCut α)
c : DedekindCut α
⊢ IsOpen ((fun a ↦ principal a) ⁻¹' Ioi c)

Tactic:
have : IsOpen (⋃ a ∈ c.right, Ioi a) := isOpen_biUnion fun _ _ ↦ isOpen_Ioi
    convert this
    ext
    simp [lt_principal_iff]

Goal state after: