mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: p : ℚ
s✝ s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).1ᶜ ∩ (s, o).2).Nonempty

Tactic:
;

Goal state after:
p : ℚ
s✝ s o : Set ℚ
hs : IsCompact (s, o).1
hpo : p ∈ (s, o).2
ho : IsOpen (s, o).2
⊢ ((s, o).1ᶜ ∩ (s, o).2).Nonempty
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False

Tactic:
;

Goal state after:
H : (cocompact ℚ).IsCountablyGenerated
x : ℕ → ℚ
hx : Tendsto x atTop (cocompact ℚ) ∧ Tendsto x atTop (𝓝 0)
⊢ False
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: s : Set ℚ
hsu : s ⊆ univ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y

Tactic:
;

Goal state after:
s : Set ℚ
hsu : s ⊆ univ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
⊢ x = y
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
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊂ (logSizeBallSeq J hJ a c i).finset

Tactic:
apply ssubset_of_subset_not_subset
    · simp [finset_logSizeBallSeq_add_one]
    refine Set.not_subset.mpr ⟨(logSizeBallSeq J hJ a c i).point, ?_, ?_⟩
    · exact point_mem_finset_logSizeBallSeq hJ i h
    · exact point_notMem_finset_logSizeBallSeq_add_one hJ i

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

Goal state before:
pp: case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) i = 0 ∨ (insertAt i) (t₀, t) i = 1

Tactic:
;

Goal state after:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) i = 0 ∨ (insertAt i) (t₀, t) i = 1
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ↑j = 0 ∨ (insertAt i) (t₀, t) ↑j = 1

Tactic:
;

Goal state after:
case h
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ↑j = 0 ∨ (insertAt i) (t₀, t) ↑j = 1
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:
;

Goal state after:
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
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:
;

Goal state after:
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
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✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
| fun i ↦
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c i).radius - ?m.162 i + ?m.162 i)

Tactic:
;

Goal state after:
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
| fun i ↦
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c i).radius - ?m.162 i + ?m.162 i)
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✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
x✝ : ℕ
| (if (logSizeBallSeq J hJ a c x✝).finset.Nonempty then 1 else 0) *
    a ^ ((logSizeBallSeq J hJ a c x✝).radius - ?m.162 x✝ + ?m.162 x✝)

Tactic:
;

Goal state after:
T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
x✝ : ℕ
| (if (logSizeBallSeq J hJ a c x✝).finset.Nonempty then 1 else 0) *
    a ^ ((logSizeBallSeq J hJ a c x✝).radius - ?m.162 x✝ + ?m.162 x✝)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
⊢ Continuous[_, inst✝] (Function.uncurry fun x_1 y ↦ x_1.1 (sumArrowHomeomorphProdArrow.symm (x_1.2, y)))

Tactic:
;

Goal state after:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
⊢ Continuous[_, inst✝] (Function.uncurry fun x_1 y ↦ x_1.1 (sumArrowHomeomorphProdArrow.symm (x_1.2, 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
q : ↑(Ω^ (M ⊕ N) X x)
x✝ : M → ↑I
hm : x✝ ∈ Cube.boundary M
n : N → ↑I
⊢ ((currySum x q) x✝) n = const n

Tactic:
;

Goal state after:
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝¹ : X
M : Type ?u.12
x : X
q : ↑(Ω^ (M ⊕ N) X x)
x✝ : M → ↑I
hm : x✝ ∈ Cube.boundary M
n : N → ↑I
⊢ ((currySum x q) x✝) n = const n
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:
;

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
⊢ (((fun q ↦ ⟨currySum x q, ⋯⟩)
          ((fun p ↦
              ⟨(GenLoop.uncurry x p).comp { toFun := sumArrowHomeomorphProdArrow.toFun, continuous_toFun := ⋯ }, ⋯⟩)
            p))
        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)) const)
y✝¹ : M → ↑I
y✝ : N → ↑I
⊢ ((currySum x ⟨(GenLoop.uncurry x p).comp { toFun := ⇑sumArrowHomeomorphProdArrow, continuous_toFun := ⋯ }, ⋯⟩) y✝¹)
      y✝ =
    (p y✝¹) y✝

Tactic:
;

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:
;

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)
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✝
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
⊢ ⟨((↑p).comp ↑(Cube.insertAt i)).curry 0, ⋯⟩ t = const t

Tactic:
;

Goal state after:
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
⊢ ⟨((↑p).comp ↑(Cube.insertAt i)).curry 0, ⋯⟩ t = const 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
i : N
p : ↑(Ω^ N X x)
t : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) (0, t) i = 0

Tactic:
;

Goal state after:
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
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
⊢ ⟨((↑p).comp ↑(Cube.insertAt i)).curry 1, ⋯⟩ t = const t

Tactic:
;

Goal state after:
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
⊢ ⟨((↑p).comp ↑(Cube.insertAt i)).curry 1, ⋯⟩ t = const 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
i : N
p : ↑(Ω^ N X x)
t : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) (1, t) i = 1

Tactic:
;

Goal state after:
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
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
⊢ ∀ (i : ↥J), ⨆ t, edist (f ↑i) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
;

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
⊢ ∀ (i : ↥J), ⨆ t, edist (f ↑i) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
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
⊢ ∀ (i : { t // edist ⟨s, hs⟩ t ≤ c }), edist (f ↑⟨s, hs⟩) (f ↑↑i) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
;

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
⊢ ∀ (i : { t // edist ⟨s, hs⟩ t ≤ c }), edist (f ↑⟨s, hs⟩) (f ↑↑i) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
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:
;

Goal state after:
ι : 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✝
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 : Ω (↑(Ω^ { j // j ≠ i } X x)) const
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ ({ toFun := fun t ↦ ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.curry t, ⋯⟩,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
        x✝)
      y✝ =
    (p x✝) y✝

Tactic:
;

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ ({ toFun := fun t ↦ ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.curry t, ⋯⟩,
          continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
        x✝)
      y✝ =
    (p x✝) y✝
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)
y✝ : N → ↑I
⊢ (fromLoop i (toLoop i p)) y✝ = p y✝

Tactic:
;

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (fromLoop i (toLoop i p)) y✝ = p y✝
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)
y✝ : N → ↑I
⊢ (Cube.insertAt i) (((Cube.splitAt i) y✝).1, ((Cube.splitAt i) y✝).2) = y✝

Tactic:
;

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (Cube.insertAt i) (((Cube.splitAt i) y✝).1, ((Cube.splitAt i) y✝).2) = y✝
Module: Mathlib.Topology.IsClosedRestrict

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

Tactic:
;

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
S : Set ι
x : ↑(Sᶜ.domRestrict ⁻¹' Sᶜ.domRestrict '' s)
x✝ : ι
⊢ reorderRestrictProd S s (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i) x✝ = ↑x x✝
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:
;

Goal state after:
ι : 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✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1.a
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (t.2 = 0 ∨ t.2 = 1) ∨ y ∈ Cube.boundary { j // j ≠ i✝ }

Tactic:
;

Goal state after:
case refine_1.a
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (t.2 = 0 ∨ t.2 = 1) ∨ y ∈ Cube.boundary { j // j ≠ i✝ }
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1.a
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ y ∈ Cube.boundary { j // j ≠ i✝ }

Tactic:
;

Goal state after:
case refine_1.a
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ y ∈ Cube.boundary { j // j ≠ i✝ }
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (t.2 = 0 ∨ t.2 = 1) ∨ y ∈ Cube.boundary { j // j ≠ i✝ }

Tactic:
;

Goal state after:
case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (t.2 = 0 ∨ t.2 = 1) ∨ y ∈ Cube.boundary { j // j ≠ i✝ }
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ y ∈ Cube.boundary { j // j ≠ i✝ }

Tactic:
;

Goal state after:
case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ y ∈ Cube.boundary { j // j ≠ i✝ }
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
x : ℝ
n : ℕ
ih : (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n
⊢ 3 *
      ((x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n -
        3 ^ n * ofDigitsTerm (cantorToTernary x).get n) =
    (x - (∑ x_1 ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get x_1 + ofDigitsTerm (cantorToTernary x).get n)) *
      3 ^ (n + 1)

Tactic:
;

Goal state after:
case succ
x : ℝ
n : ℕ
ih : (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n
⊢ 3 *
      ((x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n -
        3 ^ n * ofDigitsTerm (cantorToTernary x).get n) =
    (x - (∑ x_1 ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get x_1 + ofDigitsTerm (cantorToTernary x).get n)) *
      3 ^ (n + 1)
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ (Filter.map (fun a b ↦ (a, b).1 :: (a, b).2) (𝓝 a)).seq (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ (Filter.map (fun a b ↦ (a, b).1 :: (a, b).2) (𝓝 a)).seq (𝓝 l) ≤ cons <$> 𝓝 a <*> 𝓝 l
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
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
⊢ edist s t ≤ c

Tactic:
;

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
h' : t ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
⊢ edist s t ≤ c
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) ((t, y).2, y✝) ∈ Cube.boundary N

Tactic:
;

Goal state after:
case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ (Cube.insertAt i) ((t, y).2, y✝) ∈ Cube.boundary N
Module: Mathlib.Topology.List

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
β : Type u_3
f : List α → β
b : Filter β
a : α
l : List α
this : 𝓝 (a :: l) = Filter.map (fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l)
⊢ Tendsto (f ∘ fun p ↦ p.1 :: p.2) (𝓝 a ×ˢ 𝓝 l) b ↔ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) b
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case h
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ ((t, y).2, y✝).1 = 0 ∨ ((t, y).2, y✝).1 = 1

Tactic:
;

Goal state after:
case h
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t y : ↑I
yH : y ∈ {0, 1}
y✝ : { j // j ≠ i } → ↑I
⊢ ((t, y).2, y✝).1 = 0 ∨ ((t, y).2, y✝).1 = 1
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))
a : α
l : List α
⊢ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))

Tactic:
;

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))
a : α
l : List α
⊢ Tendsto (fun p ↦ f (p.1 :: p.2)) (𝓝 a ×ˢ 𝓝 l) (r (a :: l))
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
⊢ ∀ (x : List α), 𝓝 x = pure x

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
⊢ ∀ (x : List α), 𝓝 x = pure x