mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_den : ℕ
hx_isNNRat : IsNNRat x x_num x_den
hy_isNNRat : IsNNRat y y_num y_den
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hd1 : k_den ^ y_den < x_den
hd2 : x_den < (k_den + 1) ^ y_den
⊢ Irrational (x ^ y)

Tactic:
by
  rcases hx_isNNRat with ⟨hx_inv, hx_eq⟩
  apply Irrational.of_inv
  rw [← Real.inv_rpow (by simp only [hx_eq, invOf_eq_inv]; positivity)]
  apply irrational_rpow_rat_rat_of_num (x_num := x_den) (x_den := x_num) _ hy_isNNRat
    (Nat.coprime_comm.mp hx_coprime) hy_coprime hd1 hd2
  refine ⟨invertibleOfNonzero (fun _ ↦ ?_), by simp [hx_eq]⟩
  simp_all

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : fst = x
⊢ Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) (⟨fst, snd⟩ :: m)) =
    List.dlookup x (⟨fst, snd⟩ :: m)

Tactic:
simp [heq]

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

Goal state before:
pp: case neg.a
α : Type u
β : Type v
inst✝ : DecidableEq α
y : β
x : α
m : List ((_ : α) × β)
ih : Option.map Sigma.snd (List.find? (fun x_1 ↦ decide (x_1.fst = x)) m) = List.dlookup x m
fst : α
snd : β
heq : ¬fst = x
⊢ ⟨fst, snd⟩.fst ≠ x

Tactic:
simp [heq]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
have hU3 : ∀ n, U (n + 1) ⊆ U n :=
    fun n x hx ↦ hU2 n (mul_one x ▸ Set.mul_mem_mul hx (mem_of_mem_nhds (hU1 (n + 1))))

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
⊢ LocallyCompactSpace (X →ₜ* Y)
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: case zero
X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
f : X →* Y
hf : Set.MapsTo (⇑f) (U 0) (V 0)
⊢ Set.MapsTo (⇑f) (U 0) (V 0)

Tactic:
exact hf

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
⊢ ∀ ⦃X Y : OpenNormalSubgroup ↑P.toProfinite.toTop⦄ (f_1 : X ⟶ Y),
    ((Functor.const (OpenNormalSubgroup ↑P.toProfinite.toTop)).obj (limitCone (diagram G)).pt).map f_1 ≫
        (limitCone (diagram G)).π.app (preimage f Y) ≫ ofFiniteGrpHom (quotientMap f Y) =
      ((limitCone (diagram G)).π.app (preimage f X) ≫ ofFiniteGrpHom (quotientMap f X)) ≫ P.diagram.map f_1

Tactic:
intro X

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ ∀ ⦃Y : OpenNormalSubgroup ↑P.toProfinite.toTop⦄ (f_1 : X ⟶ Y),
    ((Functor.const (OpenNormalSubgroup ↑P.toProfinite.toTop)).obj (limitCone (diagram G)).pt).map f_1 ≫
        (limitCone (diagram G)).π.app (preimage f Y) ≫ ofFiniteGrpHom (quotientMap f Y) =
      ((limitCone (diagram G)).π.app (preimage f X) ≫ ofFiniteGrpHom (quotientMap f X)) ≫ P.diagram.map f_1
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 ↦ x_1 • x) = (fun x_1 ↦ x_1 • g • x) ∘ fun x ↦ x * g⁻¹
⊢ (fun g ↦ g • x) '' U ∈ 𝓝 (g • x)

Tactic:
rw [this, image_comp, ← smul_singleton]

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
g : G
U : Set G
hU : U ∈ 𝓝 g
this : (fun x_1 ↦ x_1 • x) = (fun x_1 ↦ x_1 • g • x) ∘ fun x ↦ x * g⁻¹
⊢ (fun x ↦ x * g⁻¹) '' U • {g • x} ∈ 𝓝 (g • x)
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
x✝ : A
a✝ : x✝ ∈ Set.univ
⊢ π / 2 ≤ π

Tactic:
linarith [pi_pos]

Goal state after:
Module: Mathlib.Topology.Algebra.PontryaginDual

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
x✝ : A
a✝ : x✝ ∈ Set.univ
⊢ π / 2 ≤ π

Tactic:
by linarith [pi_pos]

Goal state after:
Module: Mathlib.Topology.Category.Locale

Goal state before:
pp: X✝ Y✝ : CompHaus
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (compHausToTop ⋙ topToLocale).map a₁✝ = (compHausToTop ⋙ topToLocale).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
dsimp at h

Goal state after:
X✝ Y✝ : CompHaus
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : topToLocale.map (compHausToTop.map a₁✝) = topToLocale.map (compHausToTop.map a₂✝)
⊢ a₁✝ = a₂✝
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, cellFrontier n i ⊆ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ I m, closedCell m j

Tactic:
by
  rcases RelCWComplex.mapsTo n i with ⟨I, hI⟩
  use I
  rw [mapsTo_iff_image_subset, empty_union] at hI
  exact hI

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
D C : Set X
inst✝ : RelCWComplex C D
⊢ Injective fun x ↦ ↑(map 0 x) ![]

Tactic:
by
  rintro x z h
  by_contra hne
  exact not_disjoint_iff.mpr ⟨map 0 x ![], by simp [openCell_zero_eq_singleton, h]⟩
    <| disjoint_openCell_of_ne (by grind : (⟨0, x⟩ : Σ n, cell C n) ≠ ⟨0, z⟩)

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

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
a b : ↑(π C J)
h : ↑((iso_map C J) a) = ↑((iso_map C J) b)
i : I
hi : ¬J i
⊢ ↑a i = ↑b i

Tactic:
rcases a with ⟨_, c, hc, rfl⟩

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
b : ↑(π C J)
i : I
hi : ¬J i
c : I → Bool
hc : c ∈ C
h : ↑((iso_map C J) ⟨Proj J c, ⋯⟩) = ↑((iso_map C J) b)
⊢ ↑⟨Proj J c, ⋯⟩ i = ↑b i
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)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
⊢ ∀ ⦃X Y : (Finset I)ᵒᵖ⦄ (f : X ⟶ Y),
    ((Functor.const (Finset I)ᵒᵖ).obj (of ↑C)).map f ≫
        ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop Y, continuous_toFun := ⋯ } =
      ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
        (spanFunctor hC).map f

Tactic:
intro X

Goal state after:
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)
inst✝ : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
X : (Finset I)ᵒᵖ
⊢ ∀ ⦃Y : (Finset I)ᵒᵖ⦄ (f : X ⟶ Y),
    ((Functor.const (Finset I)ᵒᵖ).obj (of ↑C)).map f ≫
        ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop Y, continuous_toFun := ⋯ } =
      ConcreteCategory.ofHom { toFun := ProjRestrict C fun x ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
        (spanFunctor hC).map f
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:
exact (List.nil_lt_cons a []).le

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

Goal state before:
pp: I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndependent ℤ (eval C)

Tactic:
linearIndependent_iff_union_smaller C ho hsC,

Goal state after:
I : Type u
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : Order.IsSuccLimit o
h : ∀ o' < o, P I o'
hho : o ≤ Ordinal.type fun x1 x2 ↦ x1 < x2
C : Set (I → Bool)
hC : IsClosed C
hsC : contained C o
⊢ LinearIndependent ℤ fun (p : ↑(⋃ e, smaller C ↑e)) ↦ ↑p
Module: Mathlib.Topology.Category.Profinite.Nobeling.Induction

Goal state before:
pp: case hf
S : Profinite
a b : ↑S.toTop
h : ι S a = ι S b
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true

Tactic:
dsimp +unfoldPartialApp [ι] at h

Goal state after:
case hf
S : Profinite
a b : ↑S.toTop
h : (fun C ↦ decide (a ∈ ↑C)) = fun C ↦ decide (b ∈ ↑C)
hn : ¬a = b
C : Set ↑S.toTop
hC : IsClopen C
hh : a ∈ C ∧ b ∈ Cᶜ
⊢ decide (b ∈ C) = true
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ x ∈ ⋃ m, ⋃ (_ : ↑m < ↑n + 1), ⋃ j, closedCell m j

Tactic:
simp_rw [mem_iUnion, exists_prop]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
n : ℕ
j : cell C n
x : X
xmem : x ∈ closedCell n j
⊢ ∃ i, ↑i < ↑n + 1 ∧ ∃ i_1, x ∈ closedCell i i_1
Module: Mathlib.Topology.Connected.CardComponents

Goal state before:
pp: case inl.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Finite (ConnectedComponents X)
val✝ : Fintype (ConnectedComponents X)
⊢ ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard

Tactic:
simp only [ENat.card_eq_coe_fintype_card]

Goal state after:
case inl.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
hf₁ : IsOpenMap f
hf₂ : IsClosedMap f
inst✝ : ConnectedSpace Y
y : Y
h :
  ∀ {n : ℕ} (U : Fin n → Set X),
    (∀ (i : Fin n), IsClopen (U i)) →
      (∀ (i : Fin n), (U i).Nonempty) → Pairwise (Disjoint on U) → ⋃ i, U i = Set.univ → ↑n ≤ (f ⁻¹' {y}).encard
hy : Finite (ConnectedComponents X)
val✝ : Fintype (ConnectedComponents X)
⊢ ↑(Fintype.card (ConnectedComponents X)) ≤ (f ⁻¹' {y}).encard
Module: Mathlib.Topology.Convenient.HomSpace

Goal state before:
pp: case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦
    match x with
    | (x₁, x₂) => g (f₂ x₂, f₁ x₁)

Tactic:
rw [IsGeneratedBy.continuous_iff X]

Goal state after:
case refine_1
ι : Type t
X : ι → Type u
inst✝⁴ : (i : ι) → TopologicalSpace (X i)
Y : Type v
inst✝³ : TopologicalSpace Y
Z : Type v'
inst✝² : TopologicalSpace Z
T : Type v''
inst✝¹ : TopologicalSpace T
inst✝ : ∀ (i j : ι), IsGeneratedBy X (X i × X j)
g : Y × Z → T
h : ContinuousGeneratedBy X g
i₁ : ι
f₁ : C(X i₁, Z)
i₂ : ι
f₂ : C(X i₂, Y)
⊢ ∀ ⦃i : ι⦄ (f : C(X i, X i₁ × X i₂)),
    Continuous[inst✝⁴ i, inst✝¹]
      ((fun x ↦
          match x with
          | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
        ⇑f)
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
⊢ (∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ᶠ (x : X) in 𝓝ˢ A, P x ↑f

Tactic:
rw [eventually_nhdsSet_iff_forall]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
A : Set X
P : (x : X) → (𝓝 x).Germ Y → Prop
⊢ (∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ x ∈ A, ∀ᶠ (y : X) in 𝓝 x, P y ↑f
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
      replace h := Prod.mk_inj.mp h
      exact Prod.ext (HSpace.hmulE.2 t x h.1) (HSpace.hmulE.2 t y h.2)

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
⊢ delayReflLeft 0 γ = (refl x).trans γ

Tactic:
simp only [delayReflLeft, delayReflRight_zero, trans_symm, refl_symm, Path.symm_symm]

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

Goal state before:
pp: n : ℕ
⊢ preCantorSet n ⊆ Set.Icc 0 1

Tactic:
rw [← preCantorSet_zero]

Goal state after:
n : ℕ
⊢ preCantorSet n ⊆ preCantorSet 0
Module: Mathlib.Topology.List

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

Tactic:
by
  rw [nhds_cons, Tendsto, Filter.map_prod]; exact le_rfl

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

Goal state before:
pp: case refine_3.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
h : j ≠ i
⊢ Function.uncurry (fun x_1 y ↦ Function.uncurry (fun x_2 y ↦ (H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (t, y)) =
    ↑p y

Tactic:
rw [p.2 _ ⟨j, jH⟩]

Goal state after:
case refine_3.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
h : j ≠ i
⊢ Function.uncurry (fun x_1 y ↦ Function.uncurry (fun x_2 y ↦ (H (x_1, x_2)) y) y)
      (Prod.map id ⇑(Cube.splitAt i) (t, y)) =
    x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 0
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

Tactic:
apply (congr_arg p iH).trans

Goal state after:
case inl.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 0
⊢ p 0 = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inr.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 1
⊢ { toFun := fun c ↦ p (c default), continuous_toFun := ⋯ } y = x

Tactic:
apply (congr_arg p iH).trans

Goal state after:
case inr.refl
N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
y : N → ↑I
iH : y default = 1
⊢ p 1 = x
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 ↑s ↑t) ≤ infEDist y ↑t + (edist (x, s) (y, t) + edist (x, s) (y, t))

Tactic:
by
      gcongr <;> apply_rules [le_max_left, le_max_right]

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

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

Tactic:
exact (coveringNumber_eq_one_of_ediam_le h_nonempty hA).le

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
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty { s // s ⊆ A ∧ IsCover ε A s }
C : { s // s ⊆ A ∧ IsCover ε A s }
hC : (↑C).encard = ⨅ x, (↑x).encard
⊢ (↑C).Finite

pp: case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty { s // s ⊆ A ∧ IsCover ε A s }
C : { s // s ⊆ A ∧ IsCover ε A s }
hC : (↑C).encard = ⨅ x, (↑x).encard
⊢ (↑C).encard = coveringNumber ε A

Tactic:
· refine Set.encard_lt_top_iff.mp ?_
    simp only [hC, iInf_lt_top, encard_lt_top_iff, Subtype.exists, exists_prop]
    exact ⟨C', ⟨hC'_subset, hC'_cover⟩, hC'_fin⟩

Goal state after:
case refine_2
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
C' : Set X
hC'_subset : C' ⊆ A
hC'_cover : IsCover ε A C'
hC'_fin : C'.Finite
this : Nonempty { s // s ⊆ A ∧ IsCover ε A s }
C : { s // s ⊆ A ∧ IsCover ε A s }
hC : (↑C).encard = ⨅ x, (↑x).encard
⊢ (↑C).encard = coveringNumber ε A
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
I2 : ∀ (n : ℕ), ∀ x ∈ t0, ∃ y ∈ s n, edist x y ≤ 2 * B n
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun n ↦ 2 * B n) atTop (𝓝 0)
⊢ ∃ N, ∀ n ≥ N, edist (s n) t < ε

Tactic:
obtain ⟨N, hN⟩ : ∃ N, ∀ b ≥ N, ε > 2 * B b :=
    ((tendsto_order.1 this).2 ε εpos).exists_forall_of_atTop

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
main : ∀ (n : ℕ), edist (s n) t ≤ 2 * B n
ε : ℝ≥0∞
εpos : ε > 0
this : Tendsto (fun n ↦ 2 * B n) atTop (𝓝 0)
N : ℕ
hN : ∀ b ≥ N, ε > 2 * B b
⊢ ∃ N, ∀ n ≥ N, edist (s n) t < ε
Module: Mathlib.Topology.MetricSpace.Infsep

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝ : PseudoEMetricSpace α
s : Set α
y : α
hy : y ∈ s
z : α
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : z ≠ y), edist z y ≤ edist y z ∨ s.einfsep ≤ edist y z

pp: case inr.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z

Tactic:
· rw [edist_comm]
    exact Or.inl (iInf_le_of_le _ (iInf₂_le hy hyz.symm))

Goal state after:
case inr.inr
α : Type u_1
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
y : α
hy : y ∈ s
z : α
hz : z ∈ s
hyz : y ≠ z
⊢ ⨅ y ∈ s, ⨅ (_ : x ≠ y), edist x y ≤ edist y z ∨ s.einfsep ≤ edist y z
Module: Mathlib.Topology.MetricSpace.HolderNorm

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
inst✝⁴ : MetricSpace X
inst✝³ : NormedAddCommGroup Y
r : ℝ≥0
f : X → Y
α : Type u_3
inst✝² : NormedRing α
inst✝¹ : Module α Y
inst✝ : NormSMulClass α Y
c : α
hc : ¬‖c‖₊ = 0
hf : MemHolder r f
⊢ eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f

Tactic:
refine le_antisymm ((hf.holderWith.smul c).eHolderNorm_le.trans ?_) <| mul_le_of_le_div' ?_
    · rw [coe_mul, hf.coe_nnHolderNorm_eq_eHolderNorm, mul_comm]
    · rw [← (hf.holderWith.smul c).memHolder.coe_nnHolderNorm_eq_eHolderNorm, ← coe_div hc]
      refine HolderWith.eHolderNorm_le fun x₁ x₂ => ?_
      rw [coe_div hc, ← ENNReal.mul_div_right_comm,
        ENNReal.le_div_iff_mul_le (Or.inl <| coe_ne_zero.2 hc) <| Or.inl coe_ne_top,
        mul_comm, ← smul_eq_mul, ← ENNReal.smul_def, ← edist_smul₀, ← Pi.smul_apply,
        ← Pi.smul_apply]
      exact hf.smul.holderWith x₁ x₂

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

Goal state before:
pp: p : GHSpace
⊢ ⟦Quot.out p⟧ = p

Tactic:
exact Quot.out_eq p

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
a b : α
⊢ a ⤳ b ↔ b ≤ a

Tactic:
by
  simp only [specializes_iff_closure_subset, closure_singleton, Iic_subset_Iic]

Goal state after: