mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
⊢ X.str F ∈ cl A

Tactic:
let ι : fsu → ssu := fun x ↦ ↑x

Goal state after:
X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : F ∈ basic (cl A)
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
⊢ X.str F ∈ cl A
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
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
U : Set (WithGeneratedByTopology X Z)
hU : IsOpen U
⊢ IsOpen[inst✝² i] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f ⁻¹' U)

Tactic:
rw [WithGeneratedByTopology.isOpen_iff] at hU

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
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
i : ι
f : C(X i, Y)
U : Set (WithGeneratedByTopology X Z)
hU : ∀ ⦃i : ι⦄ (f : C(X i, Z)), IsOpen[inst✝² i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ IsOpen[inst✝² i] ((⇑WithGeneratedByTopology.equiv.symm ∘ g) ∘ ⇑f ⁻¹' U)
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
i : ι
U : Set (WithGeneratedByTopology X (X i))
hU : IsOpen U
⊢ IsOpen[inst✝¹ i] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)

Tactic:
rw [WithGeneratedByTopology.isOpen_iff] at hU

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
i : ι
U : Set (WithGeneratedByTopology X (X i))
hU : ∀ ⦃i_1 : ι⦄ (f : C(X i_1, X i)), IsOpen[inst✝¹ i_1] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
⊢ IsOpen[inst✝¹ i] (⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
⊢ ↑F ≤ 𝓝 x → X.str F = x

Tactic:
let ι : fsu → ssu := fun x ↦ ↑x

Goal state after:
X : Compactum
F : Ultrafilter X.A
x : X.A
fsu : Type u_1 := Finset (Set (Ultrafilter X.A))
ssu : Type u_1 := Set (Set (Ultrafilter X.A))
ι : fsu → ssu := fun x ↦ ↑x
⊢ ↑F ≤ 𝓝 x → X.str F = x
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝ : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
a b : ↑C
h : ∀ (J : Finset ι), (π_app C fun x ↦ x ∈ J) a = (π_app C fun x ↦ x ∈ J) b
⊢ a = b

Tactic:
ext i
  specialize h ({i} : Finset ι)
  rw [Subtype.ext_iff] at h
  simp only [π_app, ContinuousMap.precomp, ContinuousMap.coe_mk] at h
  exact congr_fun h ⟨i, Finset.mem_singleton.mpr rfl⟩

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
n : ℕ
i : cell C n
⊢ sphere 0 1 ∪ ball 0 1 = closedBall 0 1

Tactic:
exact sphere_union_ball

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

Goal state before:
pp: case nil
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
⊢ List.IsChain (fun x1 x2 ↦ x1 > x2) [] →
    (List.map (fun i ↦ if ↑x i = true then e (π C fun x ↦ x ∈ s) i else 1 - e (π C fun x ↦ x ∈ s) i) []).prod ∈
      Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ []})

Tactic:
| nil =>

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]

Goal state after:
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
⊢ (c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * b • Products.eval (π C fun x ↦ x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg
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
⊢ (c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) +
      -1 • (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]

Goal state after:
case neg
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
⊢ ((c.sum fun i a ↦ a • Products.eval (π C fun x ↦ x ∈ s) i) +
      -1 • c.sum fun a_1 b ↦ e (π C fun x ↦ x ∈ s) a * b • Products.eval (π C fun x ↦ x ∈ s) a_1) ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Span

Goal state before:
pp: case neg.h₁.nil
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
c : Products I →₀ ℤ
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
m : Products I
hm : c m ≠ 0
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) [a]
hc : ↑c.support ⊆ {m | ↑m ≤ []}
hmas : ↑m ≤ []
⊢ [] ≤ [a]

Tactic:
| nil =>

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

Goal state before:
pp: case hi.inl
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h1 : IsClosed[t] (A ∩ openCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

pp: case hi.inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h2 : IsClosed[t] (A ∩ closedCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)

Tactic:
· rw [← cellFrontier_union_openCell_eq_closedCell, inter_union_distrib_left]
      exact (isClosed_inter_cellFrontier_succ_of_le_isClosed_inter_closedCell hn j hDA).union h1

Goal state after:
case hi.inr
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
hAC : A ⊆ C
hDA : IsClosed[t] (A ∩ D)
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
h2 : IsClosed[t] (A ∩ closedCell n.succ j)
⊢ IsClosed[t] (A ∩ closedCell (n + 1) j)
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : List I
hl : List.IsChain (fun x1 x2 ↦ x1 > x2) l
hll : Products.isGood {fun x ↦ false} ⟨l, hl⟩
⊢ ↑↑⟨⟨l, hl⟩, hll⟩ = ↑↑⟨Products.nil, ⋯⟩

Tactic:
apply (List.lex_nil_or_eq_nil l (r := (· < ·))).resolve_left

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
l : List I
hl : List.IsChain (fun x1 x2 ↦ x1 > x2) l
hll : Products.isGood {fun x ↦ false} ⟨l, hl⟩
⊢ ¬List.Lex (fun x1 x2 ↦ x1 < x2) [] 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
⊢ ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o ∧
    isGood (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l

Tactic:
have hslt : Finset.sup l.val.toFinset (fun a ↦ Order.succ (ord I a)) < o := by
    simp only [Finset.sup_lt_iff ho.bot_lt, List.mem_toFinset]
    exact fun b hb ↦ ho.succ_lt (prop_of_isGood C (ord I · < o) h b hb)

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
⊢ ((↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) < o ∧
    isGood (π C fun x ↦ ord I x < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)) l
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
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})
i : I
hi : i ∈ ↑l
⊢ ord I i < (↑l).toFinset.sup fun a ↦ Order.succ (ord I a)

Tactic:
simp only [Finset.lt_sup_iff, List.mem_toFinset, Order.lt_succ_iff]

Goal state after:
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})
i : I
hi : i ∈ ↑l
⊢ ∃ b ∈ ↑l, ord I i ≤ ord I b
Module: Mathlib.Topology.Category.Profinite.Projective

Goal state before:
pp: case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ (⇑(TopCat.Hom.hom g.hom) ∘ h) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure

Tactic:
rw [comp_assoc, ultrafilter_extend_extends, ← comp_assoc, this, id_comp]

Goal state after:
case h
X : Type u
Y Z : Profinite
f : of (Ultrafilter X) ⟶ Z
g : Y ⟶ Z
hg : Surjective ⇑(ConcreteCategory.hom g)
g' : (fun X ↦ ↑X.toTop) Z → (fun X ↦ ↑X.toTop) Y
hg' : RightInverse g' ⇑(ConcreteCategory.hom g)
t : X → ↑Y.toTop := g' ∘ ⇑(ConcreteCategory.hom f) ∘ pure
h : Ultrafilter X → ↑Y.toTop := Ultrafilter.extend t
hh : Continuous h
this : ⇑(ConcreteCategory.hom g.hom) ∘ g' = id
⊢ ⇑(ConcreteCategory.hom f) ∘ pure = ⇑(TopCat.Hom.hom f.hom) ∘ pure
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n : ℕ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
⊢ (match 0, i with
      | 0, i => PartialEquiv.single ![] ↑i
      | n.succ, i => PEmpty.elim i).source =
    ball 0 1

Tactic:
by simp [ball, Matrix.empty_eq, eq_univ_iff_forall]

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

Goal state before:
pp: case neg
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := Nat.find h₀
s' : ℕ → Set α := fun i ↦ if s i ∈ S then s i else s n
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
⊢ (⋂ i, s i).Nonempty

Tactic:
apply h₂ ▸ h s' h₁

Goal state after:
case neg
α : Type u_1
S : Set (Set α)
h : ∀ (C : ℕ → Set α), (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (dissipate C n).Nonempty) → (⋂ i, C i).Nonempty
h✝ : Nonempty α
s : ℕ → Set α
h' : ∀ (i : ℕ), s i ∈ insert Set.univ S
hd : ∀ (n : ℕ), (dissipate s n).Nonempty
h₀ : ∃ n, s n ∈ S
n : ℕ := ⋯
s' : ℕ → Set α := ⋯
h₁ : ∀ (i : ℕ), s' i ∈ S
h₂ : ⋂ i, s i = ⋂ i, s' i
⊢ ∀ (n : ℕ), (dissipate s' n).Nonempty
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h1 : ∀ (i : ℕ), C i ∈ insert ∅ S
h2 : ⋂ n, ⋂ m, ⋂ (_ : m ≤ n), C m = ∅
this : (∀ (n : ℕ), dissipate C n ∈ S ∨ dissipate C n = ∅) ∧ ⋂ n, dissipate C n = ∅
⊢ ∃ n, dissipate C n = ∅

Tactic:
by
    by_cases! f : ∀ n, dissipate C n ∈ S
    · exact h (dissipate C) directed_dissipate f this.2
    · obtain ⟨n, hn⟩ := f
      exact ⟨n, by simpa [hn] using this.1 n⟩

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

Goal state before:
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 := ⋯ }.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
            ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
          x

Tactic:
rintro t ⟨x, y⟩ h

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 := fun p ↦ (eHmul (p.1, p.2.1), eHmul (p.1, p.2.2))
hG : Continuous G
t : ↑I
x : X
y : Y
h : (x, y) ∈ {(e, e)}
⊢ { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
        continuous_toFun := ⋯ }
      (x, y) =
    ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
        ((const (X × Y) (e, e)).prodMk (ContinuousMap.id (X × Y))))
      (x, y)
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
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 := ⋯ }.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 t ⟨x, y⟩ h

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 := fun p ↦ (hmulE (p.1, p.2.1), hmulE (p.1, p.2.2))
hG : Continuous G
t : ↑I
x : X
y : Y
h : (x, y) ∈ {(e, e)}
⊢ { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
        continuous_toFun := ⋯ }
      (x, y) =
    ({ 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, y)
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1

Tactic:
· exact zero_lt_one

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ γ (qRight (1, θ)) = y

Tactic:
by
    rw [qRight_one_left, γ.target]

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

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

Tactic:
rw [← Finset.card_eq_zero, ← Nat.le_zero, ← Nat.sub_self #J, hlJ]

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

Goal state before:
pp: case refine_1.nil
α : Type u_1
inst✝ : TopologicalSpace α
as : List α
⊢ pure [] ≤ traverse 𝓝 []

Tactic:
| nil =>

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
⊢ List.cons <$> pure a <*> pure l ≤ List.cons <$> 𝓝 a <*> traverse 𝓝 l

Tactic:
exact Filter.seq_mono (Filter.map_mono <| pure_le_nhds a) ih

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: case nil
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
u : List (Set α)
s : Set (List α)
hus : sequence [] ⊆ s
⊢ ∃ v, List.Forall₂ (fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) [] v ∧ sequence v ⊆ s

Tactic:
| nil =>

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
⊢ Tendsto f (𝓝 []) (r [])

Tactic:
nhds_nil

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
r : List α → Filter β
h_nil : Tendsto f (pure []) (r [])
h_cons : ∀ (l : List α) (a : α), Tendsto f (𝓝 l) (r l) → Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
⊢ Tendsto f (pure []) (r [])
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝² : AddCommMonoid R
inst✝¹ : LinearOrder R
inst✝ : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
H : d x y < 0
⊢ False

Tactic:
have : d x x < 0 := by
    calc d x x ≤ d x y + d y x := d.triangle' x y x
      _ < 0 + 0 := by refine add_lt_add H (d.symm x y ▸ H)
      _ = 0 := by simp

Goal state after:
X : Type u_1
R : Type u_2
inst✝² : AddCommMonoid R
inst✝¹ : LinearOrder R
inst✝ : AddLeftStrictMono R
d : PseudoMetric X R
x y : X
H : d x y < 0
this : d x x < 0
⊢ False
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x✝ : ℕ
⊢ Tendsto (fun x ↦ x.eraseIdx x✝) (𝓝 []) (𝓝 ([].eraseIdx x✝))

Tactic:
nhds_nil

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
x✝ : ℕ
⊢ Tendsto (fun x ↦ x.eraseIdx x✝) (pure []) (𝓝 ([].eraseIdx x✝))
Module: Mathlib.Topology.List

Goal state before:
pp: case nil
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
⊢ Tendsto prod (𝓝 []) (𝓝 [].prod)

Tactic:
| nil =>

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

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

Tactic:
by
      gcongr; apply infEDist_le_infEDist_add_edist

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < externalCoveringNumber ε A ↔ ¬A.Nonempty

Tactic:
simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < coveringNumber ε A ↔ ¬A.Nonempty

Tactic:
simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
⊢ ¬0 < packingNumber ε A ↔ ¬A.Nonempty

Tactic:
simp [not_nonempty_iff_eq_empty]

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

Goal state before:
pp: Y : Type u_2
inst✝¹ : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst✝ : PseudoMetricSpace X
hX : BoundedSpace X
f : X → Y
s : ℝ≥0
hf : MemHolder r f
hs : s ≤ r
⊢ MemHolder s f

Tactic:
obtain ⟨C, hf⟩ := hf

Goal state after:
Y : Type u_2
inst✝¹ : PseudoEMetricSpace Y
r : ℝ≥0
X : Type u_3
inst✝ : PseudoMetricSpace X
hX : BoundedSpace X
f : X → Y
s : ℝ≥0
hs : s ≤ r
C : ℝ≥0
hf : HolderWith C r f
⊢ MemHolder s f
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: α : Type u_1
inst✝ : EDist α
s : Set α
⊢ 0 < s.einfsep ↔ ∃ C > 0, ∀ x ∈ s, ∀ y ∈ s, x ≠ y → C ≤ edist x y

Tactic:
rw [pos_iff_ne_zero, Ne, einfsep_zero]
  simp only [not_forall, not_exists, not_lt, exists_prop, not_and]

Goal state after: