mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
⊢ MapsTo (⇑(F i)) K₁ U → MapsTo (⇑(G i)) K₂ U → (F i) ⊤ = (G i) ⊥ → MapsTo (⇑((F i).concat (G i))) K U

Tactic:
hf

Goal state after:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
ι : Type u_3
p : Filter ι
F : ι → C(↑(Icc a b), E)
G : ι → C(↑(Icc b c), E)
hfg : ∀ᶠ (i : ι) in p, (F i) ⊤ = (G i) ⊥
hfg' : f ⊤ = g ⊥
hf✝ :
  ∀ (K : Set ↑(Icc a b)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑f) K U → ∀ᶠ (a_4 : ι) in p, MapsTo (⇑(F a_4)) K U
hg :
  ∀ (K : Set ↑(Icc b c)),
    IsCompact K → ∀ (U : Set E), IsOpen[inst✝] U → MapsTo (⇑g) K U → ∀ᶠ (a : ι) in p, MapsTo (⇑(G a)) K U
K : Set ↑(Icc a c)
hK : IsCompact K
U : Set E
hU : IsOpen[inst✝] U
hfgU : MapsTo (⇑(f.concat g)) K U
h : b ∈ Icc a c
K₁ : Set ↑(Icc a b) := ⇑projIccCM '' Subtype.val '' (K ∩ Iic ⟨b, h⟩)
K₂ : Set ↑(Icc b c) := ⇑projIccCM '' Subtype.val '' (K ∩ Ici ⟨b, h⟩)
hK₁ : IsCompact K₁
hK₂ : IsCompact K₂
hfU : MapsTo (⇑f) K₁ U
hgU : MapsTo (⇑g) K₂ U
i : ι
hf : MapsTo (⇑(F i)) K₁ U
⊢ MapsTo (⇑(G i)) K₂ U → (F i) ⊤ = (G i) ⊥ → MapsTo (⇑((F i).concat (G i))) K U
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : T1Space E
A : Set E
h : ∀ B ⊆ A, B.Infinite → ∃ a ∈ A, AccPt a (𝓟 B)
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in cofinite, x n ∈ A
hfin : (range x).Finite
⊢ ∀ᶠ (x_1 : ℕ) in cofinite, x x_1 ∈ A → x x_1 ∈ range x ∩ A

Tactic:
simp

Goal state after:
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)
⊢ ∀ ⦃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)

Tactic:
intro j

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)
j : ι
⊢ ∀ (f : C(X j, X i₁ × X i₂)),
    Continuous[inst✝⁴ j, inst✝¹]
      ((fun x ↦
          match x with
          | (x₁, x₂) => g (f₂ x₂, f₁ x₁)) ∘
        ⇑f)
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ (Iic ∘ 𝓟) (s ∩ t) = Iic (𝓟 s) ∩ Iic (𝓟 t)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
β : Type u_3
la : Filter α
lb : Filter β
f : α → Filter β
⊢ Tendsto f la (𝓝 lb) ↔ ∀ s ∈ lb, ∀ᶠ (a : α) in la, s ∈ f a

Tactic:
simp only [nhds_eq', tendsto_lift', mem_ofPred_eq]

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: case hg
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: case hg'
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (Iic ∘ 𝓟) univ = univ

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist (some val✝) none = edist none (some val✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none (some val✝) = edist (some val✝) none

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
⊢ edist none none = edist none none

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist none (some val✝) ≤ edist none (some val✝¹) + edist (some val✝¹) (some val✝)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Germ

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f✝ g : X → Y
A✝ : Set X
x✝ : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
f f' : X → Y
hff' : f =ᶠ[𝓝 x] f'
⊢ (∀ᶠ (y : X) in 𝓝 x, P y ↑f) → ∀ᶠ (y : X) in 𝓝 x, P y ↑f'

Tactic:
hf

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f✝ g : X → Y
A✝ : Set X
x✝ : X
P : (x : X) → (𝓝 x).Germ Y → Prop
A : Set X
x : X
φ : (𝓝 x).Germ Y
f f' : X → Y
hff' : f =ᶠ[𝓝 x] f'
hf : ∀ᶠ (y : X) in 𝓝 x, P y ↑f
⊢ ∀ᶠ (y : X) in 𝓝 x, P y ↑f'
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist (some val✝¹) (some val✝) ≤ edist (some val✝¹) none + edist none (some val✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none (some val✝) ≤ edist none none + edist none (some val✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝¹ val✝ : α
⊢ edist (some val✝¹) none ≤ edist (some val✝¹) (some val✝) + edist (some val✝) none

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist none none ≤ edist none (some val✝) + edist (some val✝) none

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
val✝ : α
⊢ edist (some val✝) none ≤ edist (some val✝) none + edist none none

Tactic:
simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
m : WeakPseudoEMetricSpace α
⊢ edist none none ≤ edist none none + edist none none

Tactic:
simp

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

Goal state before:
pp: α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
r : ℝ≥0∞
hr : 0 < r
x : Option α
val✝ : α
⊢ some val✝ ∈ Metric.eball none r → some val✝ = none

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ Subtype.val '' V ⊆ U

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (U : TopologicalSpace.Opens (X i)), IsGeneratedBy X ↥U
inst✝ : IsGeneratedBy X Y
U : Set Y
hU : IsOpen[inst✝²] U
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Opens (X a.fst) := fun a ↦ { carrier := ⇑a.snd ⁻¹' U, is_open' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑U := fun a ↦ U.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑U
hV : ∀ (a : (i : ι) × C(X i, Y)), IsOpen[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ V = Subtype.val ⁻¹' Subtype.val '' V

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ Subtype.val '' V ⊆ F

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
g : (a : (i : ι) × C(X i, Y)) → ↥(W a) → ↑F := fun a ↦ F.restrictPreimage ⇑a.snd
hg : ∀ (a : (i : ι) × C(X i, Y)), Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (g a)
V : Set ↑F
hV : ∀ (a : (i : ι) × C(X i, Y)), IsClosed[instTopologicalSpaceSubtype] (g a ⁻¹' V)
⊢ V = Subtype.val ⁻¹' Subtype.val '' V

Tactic:
simp

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

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

Tactic:
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
⊢ { toFun := fun x_1 ↦ (fun p ↦ delayReflRight p.1 p.2) (t, x_1), continuous_toFun := ⋯ } (refl x) =
    ({ toFun := fun ρ ↦ ρ.1.trans ρ.2, continuous_toFun := ⋯ }.comp
        ((ContinuousMap.id (Path x x)).prodMk (const (Path x x) (refl x))))
      (refl x)

Tactic:
exact refl_trans_refl.symm

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

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find ⋯ = 1
⊢ Nat.find ⋯ - 1 < Nat.find ⋯

Tactic:
simp

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

Goal state before:
pp: case e'_5
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₀ : ↑V
hid : (ContinuousMap.id ↑V).Homotopic (ContinuousMap.const (↑V) v₀)
a✝ : ↑V
⊢ ↑((ContinuousMap.inclusion hVU) a✝) = ↑(((ContinuousMap.inclusion hVU).comp (ContinuousMap.id ↑V)) a✝)

Tactic:
simp

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
t : M → ↑I
⊢ ((fun p ↦ ⟨(↑p).comp { toFun := fun t n ↦ t (e.symm n), continuous_toFun := ⋯ }, ⋯⟩)
        ((fun p ↦ ⟨(↑p).comp { toFun := fun t m ↦ t (e m), continuous_toFun := ⋯ }, ⋯⟩) p))
      t =
    p t

Tactic:
simp

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
t : N → ↑I
⊢ ((fun p ↦ ⟨(↑p).comp { toFun := fun t m ↦ t (e m), continuous_toFun := ⋯ }, ⋯⟩)
        ((fun p ↦ ⟨(↑p).comp { toFun := fun t n ↦ t (e.symm n), continuous_toFun := ⋯ }, ⋯⟩) p))
      t =
    p t

Tactic:
simp

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.12
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y✝¹ : M → ↑I
y✝ : N → ↑I
⊢ (((fun q ↦ ⟨currySum x q, ⋯⟩)
          ((fun p ↦
              ⟨(GenLoop.uncurry x p).comp { toFun := sumArrowHomeomorphProdArrow.toFun, continuous_toFun := ⋯ }, ⋯⟩)
            p))
        y✝¹)
      y✝ =
    (p y✝¹) y✝

Tactic:
simp

Goal state after:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.12
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y✝¹ : M → ↑I
y✝ : N → ↑I
⊢ ((currySum x ⟨(GenLoop.uncurry x p).comp { toFun := ⇑sumArrowHomeomorphProdArrow, continuous_toFun := ⋯ }, ⋯⟩) y✝¹)
      y✝ =
    (p y✝¹) y✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.12
x : X
p : ↑(Ω^ (M ⊕ N) X x)
y✝ : M ⊕ N → ↑I
⊢ ((fun p ↦ ⟨(GenLoop.uncurry x p).comp { toFun := sumArrowHomeomorphProdArrow.toFun, continuous_toFun := ⋯ }, ⋯⟩)
        ((fun q ↦ ⟨currySum x q, ⋯⟩) p))
      y✝ =
    p y✝

Tactic:
simp

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
i : N
p : ↑(Ω^ N X x)
t : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) (0, t) i = 0

Tactic:
simp

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
i : N
p : ↑(Ω^ N X x)
t : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) (1, t) i = 1

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ 0 ≤ n

Tactic:
simp

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

Goal state before:
pp: ⊢ 3⁻¹ ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑Sᶜ
⊢ Sᶜ.domRestrict (reorderRestrictProd S s p) x✝ = ↑p.1 x✝

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ 1 / 3 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

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

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: case fst
ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑Sᶜ
⊢ ↑((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p)).1 x✝ = ↑p.1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: case snd
ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑S
⊢ ((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p)).2 x✝ = p.2 x✝

Tactic:
simp

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

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
⊢ (cantorSequence x).get n ∈ cantorSet

Tactic:
by
  induction n with
  | zero => simpa [cantorSequence]
  | succ n ih => exact cantorStep_mem_cantorSet ih

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

Goal state before:
pp: x : ℝ
n : ℕ
⊢ (cantorToTernary x).get n ≠ 1

Tactic:
by
  grind [cantorToTernary, Stream'.get_map]

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

Goal state before:
pp: case pos
x : ℝ
n : ℕ
h✝ : 0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3
⊢ 3 * (Stream'.iterate cantorStep x).get n =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (↑↑0 * (↑3 ^ (n + 1))⁻¹))

Tactic:
simp

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

Goal state before:
pp: case neg
x : ℝ
n : ℕ
h✝ : ¬(0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3)
⊢ 3 * (Stream'.iterate cantorStep x).get n - 2 =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (↑↑2 * (↑3 ^ (n + 1))⁻¹))

Tactic:
simp

Goal state after:
case neg
x : ℝ
n : ℕ
h✝ : ¬(0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3)
⊢ 3 * (Stream'.iterate cantorStep x).get n - 2 =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (2 * (3 ^ (n + 1))⁻¹))
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem :
  0 ≤ (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∧
    (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ≤ 1
⊢ 3 ^ n ≠ 0

Tactic:
simp

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

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ 0 = -0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
l : List α
⊢ 𝓝 l = pure l

Tactic:
induction l <;> simp [*, nhds_cons]

Goal state after:
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
⊢ Tendsto (fun p ↦ p.2.insertIdx (n + 1) p.1) (𝓝 a ×ˢ 𝓝 []) (𝓝 ([].insertIdx (n + 1) a))

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝¹ : AddZeroClass R
inst✝ : Preorder R
x✝² x✝¹ x✝ : X
⊢ 0 x✝² x✝ ≤ 0 x✝² x✝¹ + 0 x✝¹ x✝

Tactic:
simp

Goal state after:
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✝ : X
⊢ d x✝ x✝ ⊔ d' x✝ x✝ = 0

Tactic:
simp

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

Goal state before:
pp: case refine_1.h₁
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 z : X
⊢ d x y ≤ d x y ⊔ d' x y

Tactic:
simp

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

Goal state before:
pp: case h₂
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 z : X
⊢ d y z ≤ d y z ⊔ d' y z

Tactic:
simp

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

Goal state before:
pp: case refine_2.h₁
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 z : X
⊢ d' x y ≤ d x y ⊔ d' x y

Tactic:
simp

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

Goal state before:
pp: case h₂
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 z : X
⊢ d' y z ≤ d y z ⊔ d' y z

Tactic:
simp

Goal state after:
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
⊢ 0 + 0 = 0

Tactic:
simp

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

Goal state before:
pp: case singleton
X : Type u_1
R : Type u_2
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
Y : Type u_3
f : Y → PseudoMetric X R
s : Finset Y
x y : X
i : Y
⊢ ({i}.sup f) x y = {i}.sup' ⋯ fun i ↦ (f i) x y

Tactic:
simp

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

Goal state before:
pp: X : Type u_1
R : Type u_2
inst✝¹ : AddZeroClass R
inst✝ : SemilatticeSup R
⊢ ∀ (x y z : X), ⊥ x z ≤ ⊥ x y ⊔ ⊥ y z

Tactic:
simp

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

Goal state before:
pp: case inl
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
x y z : X
h : ∀ d ∈ ∅, (f d).IsUltra
⊢ (∅.sup f) x z ≤ max ((∅.sup f) x y) ((∅.sup f) y z)

Tactic:
simp

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

Goal state before:
pp: case e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f : ↑(Ω^ N X x)
x✝¹ : N → ↑I
x✝ : N
⊢ (if x✝ = i then σ (x✝¹ i) else x✝¹ x✝) =
    ↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝¹).1, (↑(Cube.splitAt i) x✝¹).2) x✝

Tactic:
simp

Goal state after: