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

Goal state before:
pp: case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
h_firstIsPos : FirstNonzeroIsPos (exps_hd :: exps_tl)
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
simp only [FirstNonzeroIsPos.cons_iff] at h_firstIsPos

Goal state after:
case cons.cons
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h_firstIsPos : 0 < exps_hd ∨ exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.right.cons.right
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
tl_tl : Multiseries basis_hd basis_tl
h_coef : ∀ x ∈ (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq, x.2.Sorted
h_Pairwise✝ :
  Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons tl_exp tl_coef tl_tl)) 0).seq
h_all : ∀ x ∈ Multiseries.cons tl_exp tl_coef tl_tl, (exp, coef) > x
h_Pairwise : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (Multiseries.cons tl_exp tl_coef tl_tl)
⊢ (Multiseries.cons tl_exp tl_coef tl_tl).Sorted

Tactic:
exact Sorted.seq _ (fun x hx ↦ h_coef _ (by simp_all)) h_Pairwise

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

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

Tactic:
← Nat.clog_le_iff_le_pow hb

Goal state after:
b m n : ℕ
hb : 1 < b
h₁ : m < Nat.clog b n
h₂ : Nat.clog b n ≤ m + 1
⊢ Nat.clog b n = m + 1
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
⊢ ∃ m, n = m ^ q

Tactic:
let f := n.factorization.mapRange (· / q) <| by simp

Goal state after:
case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
⊢ ∃ m, n = m ^ q
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
⊢ jacobiSymNat a b = r

Tactic:
have ha' : legendreSym 2 a = 1 := by
    simp only [legendreSym.mod 2 a, Int.ofNat_mod_ofNat, ha]
    decide
  rcases eq_or_ne c 0 with (rfl | hc')
  · rw [← hr, Nat.eq_zero_of_dvd_of_div_eq_zero (Nat.dvd_of_mod_eq_zero hb) hc]
  · have : NeZero c := ⟨hc'⟩
    -- for `jacobiSym.mul_right`
    rwa [← Nat.mod_add_div b 2, hb, hc, Nat.zero_add, jacobiSymNat, jacobiSym.mul_right,
      ← jacobiSym.legendreSym.to_jacobiSym, ha', one_mul]

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -b = a' * b

Tactic:
← pa,

Goal state after:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -b = ↑a * b
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -(a * b) = na' * b

Tactic:
← pa,

Goal state after:
α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -(a * b) = ↑na * b
Module: Mathlib.Topology.Category.TopCat.Sphere

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

Tactic:
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:
convert! Homeomorph.compactSpace Homeomorph.ulift.symm
  infer_instance

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
a✝¹ : ⟨n, i⟩ ∈ univ
m : ℕ
j : ↑(E.I m)
a✝ : ⟨m, j⟩ ∈ univ
hne : ⟨n, i⟩ ≠ ⟨m, j⟩
⊢ Function.onFun Disjoint (fun ni ↦ ↑(map ni.fst ↑ni.snd) '' ball 0 1) ⟨n, i⟩ ⟨m, j⟩

Tactic:
refine @pairwiseDisjoint' _ _ C D _ ⟨n, i⟩ trivial ⟨m, j⟩ trivial ?_

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
n : ℕ
i : ↑(E.I n)
a✝¹ : ⟨n, i⟩ ∈ univ
m : ℕ
j : ↑(E.I m)
a✝ : ⟨m, j⟩ ∈ univ
hne : ⟨n, i⟩ ≠ ⟨m, j⟩
⊢ ⟨n, ↑i⟩ ≠ ⟨m, ↑j⟩
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
A : Set X
asubc : A ⊆ C
h : (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D)
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → IsEmpty (cell b)
⊢ IsClosed[inst✝] (A ∩ D ∪ ⋃ i, ⋃ i_1, A ∩ ↑(map (↑i) i_1) '' closedBall 0 1)

Tactic:
exact h.2.union (isClosed_iUnion_of_finite (fun n ↦ isClosed_iUnion_of_finite (h.1 n.1)))

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
e : cell C 1
⊢ cellFrontier 1 e = ↑(map 1 e) '' {-1, 1}

Tactic:
cellFrontier

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
⊢ ↑(map 1 e) '' sphere 0 1 = ↑(map 1 e) '' {-1, 1}
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ x ∈ s)))

Tactic:
span_iff_products

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
s : Finset I
inst✝ : WellFoundedLT I
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval (π C fun x ↦ x ∈ s)))
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) ℤ
x : ↑(C' C ho)
i : I
h₁ : ord I i < o
⊢ ord I i = o → true = ↑x i

Tactic:
h₂

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) ℤ
x : ↑(C' C ho)
i : I
h₁ : ord I i < o
h₂ : ord I i = o
⊢ true = ↑x i
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (eval C))

Tactic:
span_iff_products

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
hC : IsClosed C
⊢ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
⊢ eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o) '' {m | m < l})

Tactic:
have hlt : ∀ i ∈ l.val, ord I i < Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) := by
    intro i hi
    simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]
    exact ⟨i, hi, le_rfl⟩

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o) '' {m | m < l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ eval (π C fun x ↦ ord I x < o) l ∈ Submodule.span ℤ (eval (π C fun x ↦ ord I x < o) '' {m | m < l})

Tactic:
eval_πs_image' C (le_of_lt hslt) hlt,

Goal state after:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
l : Products I
h : isGood (π C fun x ↦ ord I x < o) l
hslt : ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o
he :
  eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l ∈
    Submodule.span ℤ (eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
hlt : ∀ i ∈ ↑l, ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)
⊢ eval (π C fun x ↦ ord I x < o) l ∈
    Submodule.span ℤ
      (⇑(πs' C ⋯) '' eval (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) '' {m | m < l})
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 : ℕ∞
⊢ ∀ (n_1 : ℕ) (i : ↑{x | ↑n_1 < n}), closedCell n_1 ↑i ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

Tactic:
intro l ⟨i, 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⟩ ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j
Module: Mathlib.Topology.Category.UniformSpace

Goal state before:
pp: X : UniformSpaceCat
Y : CpltSepUniformSpace
f : X ⟶ (forget₂ CpltSepUniformSpace UniformSpaceCat).obj Y
⊢ (fun f ↦ X.completionHom ≫ f.hom) ((fun f ↦ extensionHom f) f) = f

Tactic:
by
            ext x
            rcases f with ⟨⟨_, _⟩⟩
            exact @Completion.extension_coe _ _ _ _ _ (CpltSepUniformSpace.t0Space _)
              ‹_› _

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

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

Tactic:
rcases isEmpty_or_nonempty α with hα | _
  · simp
  rw [IsCompactSystem.iff_nonempty_iInter] at h ⊢
  intro s h' hd
  by_cases! h₀ : ∀ n, s n ∉ S
  · simp_all
  classical
  let n := Nat.find h₀
  let s' := fun i ↦ if s i ∈ S then s i else s n
  have h₁ : ∀ i, s' i ∈ S := by grind
  have h₂ : ⋂ i, s i = ⋂ i, s' i := by ext; simp; grind
  apply h₂ ▸ h s' h₁
  by_contra! ⟨j, hj⟩
  have h₃ (v : ℕ) (hv : n ≤ v) : dissipate s v = dissipate s' v := by ext; simp; grind
  have h₇ : dissipate s' (max j n) = ∅ := by
    rw [← subset_empty_iff] at hj ⊢
    exact (antitone_dissipate (Nat.le_max_left j n)).trans hj
  specialize h₃ (max j n) (Nat.le_max_right j n)
  specialize hd (max j n)
  simp [h₃, h₇] at hd

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

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
⊢ IsCompactSystem S ↔
    ∀ (C : ℕ → Set α),
      Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty

Tactic:
isCompactSystem_iff_of_directed hpi

Goal state after:
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
⊢ (∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅) ↔
    ∀ (C : ℕ → Set α),
      Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty
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
l : ↑(MaxProducts C ho)
q : Products I
hq : q < (↑l).Tail
this : Inhabited I
a : I
ha : a ∈ ↑q
hM : ¬↑(↑l).Tail = []
⊢ (↑(↑l).Tail).head! < term I ho

Tactic:
have := l.val.prop
    rw [max_eq_o_cons_tail C hsC ho l, List.isChain_iff_pairwise] at this
    exact List.rel_of_pairwise_cons this (List.head!_mem_self hM)

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

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

Tactic:
exact ⟨t₁ ∪ t₂, ht₁.union ht₂, h ▸ union_subset_union hA_sub hB_sub⟩

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ {refl x},
      { toFun := fun x_2 ↦ (fun p ↦ delayReflLeft p.1 p.2) (t, x_2), continuous_toFun := ⋯ } x_1 =
        ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
            ((const (Path x x) (refl x)).prodMk (ContinuousMap.id (Path x x))))
          x_1

Tactic:
rintro t _ rfl; exact refl_trans_refl.symm

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x✝ y x : X
⊢ ∀ (t : ↑I),
    ∀ x_1 ∈ {refl x},
      { toFun := fun x_2 ↦ (fun p ↦ delayReflRight p.1 p.2) (t, x_2), continuous_toFun := ⋯ } x_1 =
        ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (Path x x)).prodMk (const (Path x x) (refl x))))
          x_1

Tactic:
rintro t _ rfl; exact refl_trans_refl.symm

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

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
⊢ ∃ V, ∃ (hVU : V ⊆ U), V ∈ 𝓝 x ∧ (ContinuousMap.inclusion hVU).Nullhomotopic

Tactic:
obtain ⟨V, ⟨hVmem, hVcontractible⟩, hVU⟩ := (contractible_basis x).mem_iff.mp hU

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : StronglyLocallyContractibleSpace X
x : X
U : Set X
hU : U ∈ 𝓝 x
V : Set X
hVU : id V ⊆ U
hVmem : V ∈ 𝓝 x
hVcontractible : ContractibleSpace ↑V
⊢ ∃ V, ∃ (hVU : V ⊆ U), V ∈ 𝓝 x ∧ (ContinuousMap.inclusion hVU).Nullhomotopic
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
hlJ : l + 1 = #J
h_emp : (logSizeBallSeq J hJ a c (l + 1)).finset = ∅
⊢ s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset

Tactic:
simp [h_emp]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p ↦ (p.1 :: p.2).length) (𝓝 a ×ˢ 𝓝 l) (pure (a :: l).length)

Tactic:
dsimp only [List.length]

Goal state after:
case refine_2
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
a : α
ih : Tendsto length (𝓝 l) (pure l.length)
⊢ Tendsto (fun p ↦ p.2.length + 1) (𝓝 a ×ˢ 𝓝 l) (pure (l.length + 1))
Module: Mathlib.Topology.List

Goal state before:
pp: case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)

Tactic:
tendsto_cons_iff,

Goal state after:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto (fun p ↦ (p.1 :: p.2).prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x :: l).prod)
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y ↑t + (edist x y + hausdorffEDist ↑t ↑s) = infEDist y ↑t + (edist x y + hausdorffEDist ↑s ↑t)

Tactic:
hausdorffEDist_comm

Goal state after:
α : Type u_1
inst✝ : EMetricSpace α
x : α
s : Closeds α
y : α
t : Closeds α
⊢ infEDist y ↑t + (edist x y + hausdorffEDist ↑s ↑t) = infEDist y ↑t + (edist x y + hausdorffEDist ↑s ↑t)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦symmAt i p⟧

Tactic:
symmAt_indep (Classical.arbitrary N) p,

Goal state after:
N : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N
inst✝ : Nonempty N
i : N
p : ↑(Ω^ N X x)
⊢ (⟦p⟧)⁻¹ = ⟦symmAt (Classical.arbitrary N) p⟧
Module: Mathlib.Topology.MetricSpace.GromovHausdorffRealized

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
⊢ 2 * 0 + 1 + 2 * 0 ≤ 2 * diam univ + 1 + 2 * diam univ

Tactic:
gcongr <;> positivity

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
inst✝¹ : DecidableEq N
inst✝ : Nontrivial N
h : ∃ y, y ≠ Classical.arbitrary N := exists_ne (Classical.arbitrary N)
⊢ ∀ (a b c d : HomotopyGroup N X x), Mul.mul (a * b) (c * d) = Mul.mul a c * Mul.mul b d

Tactic:
rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ⟨d⟩
      apply congr_arg Quotient.mk'
      simp only [fromLoop_trans_toLoop, transAt_distrib <| Classical.choose_spec h, coe_toEquiv,
        loopHomeo_apply, coe_symm_toEquiv, loopHomeo_symm_apply]

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

Goal state before:
pp: case h
α : 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' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
⊢ Tendsto s atTop (𝓝 t)

Tactic:
have I2 : ∀ n, ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n := by
    /- For the (much easier) reverse inequality, we start from a point `x ∈ t0` and we want
            to find a point `y ∈ s n` which is close to `x`.
            `x` belongs to `t0`, the intersection of the closures. In particular, it is well
            approximated by a point `z` in `⋃m≥n, s m`, say in `s m`. Since `s m` and
            `s n` are close, this point is itself well approximated by a point `y` in `s n`,
            as required. -/
    intro n x xt0
    have : x ∈ closure (⋃ m ≥ n, s m : Set α) := by apply mem_iInter.1 xt0 n
    obtain ⟨z : α, hz, Dxz : edist x z < B n⟩ := EMetric.mem_closure_iff.1 this (B n) (B_pos n)
    simp only [exists_prop, Set.mem_iUnion] at hz
    obtain ⟨m : ℕ, m_ge_n : m ≥ n, hm : z ∈ (s m : Set α)⟩ := hz
    have : hausdorffEDist (s m : Set α) (s n) < B n := hs n m n m_ge_n (le_refl n)
    obtain ⟨y : α, hy : y ∈ (s n : Set α), Dzy : edist z y < B n⟩ :=
      exists_edist_lt_of_hausdorffEDist_lt hm this
    exact
      ⟨y, hy,
        calc
          edist x y ≤ edist x z + edist z y := edist_triangle _ _ _
          _ ≤ B n + B n := by gcongr
          _ = 2 * B n := (two_mul _).symm
          ⟩

Goal state after:
case h
α : 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' := ⋯ }
I1 : ∀ (n : ℕ), ∀ x ∈ s n, ∃ y ∈ t0, edist x y ≤ 2 * B n
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
⊢ Tendsto s atTop (𝓝 t)
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
⊢ ∀ (b : ℝ≥0∞), ⊥ < b → ∃ i, ∃ (_ : HolderWith i r (Function.const X c)), ↑i < b

Tactic:
exact fun C' hC' => ⟨0, .const, hC'⟩

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

Goal state before:
pp: case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y

Tactic:
mem_toFinset

Goal state after:
case intro
α : Type u_1
inst✝¹ : EDist α
s : Set α
inst✝ : Finite ↑s
hs : s.Nontrivial
val✝ : Fintype ↑s
w : α × α
hed : s.offDiag.toFinset.inf (uncurry edist) = uncurry edist w
hxy : w ∈ s.offDiag
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf (uncurry edist) = edist x y