mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
l : List α
⊢ 𝓝 l = pure 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 := ⋯
l : ℕ := ⋯
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
hts : edist t s ≤ c
x✝ : ℕ
⊢ P x✝ ↔ t ∈ (logSizeBallSeq J hJ a c x✝).finset ∧ s ∈ (logSizeBallSeq J hJ a c x✝).finset

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 := ⋯
l : ℕ := ⋯
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
hts : edist t s ≤ c
x✝ : ℕ
⊢ P x✝ ↔ t ∈ (logSizeBallSeq J hJ a c x✝).finset ∧ s ∈ (logSizeBallSeq J hJ a c x✝).finset
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ 𝓝 a ×ˢ 𝓝 (a' :: l) = Filter.map (fun p ↦ (p.1, p.2.1 :: p.2.2)) (𝓝 a ×ˢ 𝓝 a' ×ˢ 𝓝 l)

Tactic:
simp only [nhds_cons, Filter.prod_eq, ← Filter.map_def, ← Filter.seq_eq_filter_seq]

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
n : ℕ
a' : α
l : List α
⊢ Prod.mk <$> 𝓝 a <*> (cons <$> 𝓝 a' <*> 𝓝 l) =
    (fun p ↦ (p.1, p.2.1 :: p.2.2)) <$> (Prod.mk <$> 𝓝 a <*> (Prod.mk <$> 𝓝 a' <*> 𝓝 l))
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)) =
    x

Tactic:
;

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 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
⊢ (Prod.map id ⇑(Cube.splitAt i) (t, y)).2.2 ∈ Cube.boundary { j // ¬j = i }

Tactic:
;

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
⊢ (Prod.map id ⇑(Cube.splitAt i) (t, y)).2.2 ∈ Cube.boundary { j // ¬j = i }
Module: Mathlib.Topology.List

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

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
x✝ : α × List α
a : α
l : List α
⊢ Tendsto (fun p ↦ p.2.insertIdx n p.1) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a, l).2.insertIdx n (a, l).1))
Module: Mathlib.Topology.List

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

Tactic:
;

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: α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun p ↦ (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 0))

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
l : List α
⊢ Tendsto (fun p ↦ (p.1 :: p.2).eraseIdx 0) (𝓝 a ×ˢ 𝓝 l) (𝓝 ((a :: l).eraseIdx 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
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (if ↑(x✝ i) ≤ 1 / 2 then f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))
    else g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))) =
    (fromLoop i (Path.trans (toLoop i f) (toLoop i g))) x✝

Tactic:
;

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (if ↑(x✝ i) ≤ 1 / 2 then f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))
    else g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))) =
    (fromLoop i (Path.trans (toLoop i f) (toLoop i g))) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ↑(x✝ i) ≤ 1 / 2
⊢ f (↑(Cube.insertAt i) (Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑(x✝ i)), fun j ↦ x✝ ↑j)) =
    f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))

Tactic:
;

Goal state after:
case pos
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ↑(x✝ i) ≤ 1 / 2
⊢ f (↑(Cube.insertAt i) (Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑(x✝ i)), fun j ↦ x✝ ↑j)) =
    f (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i))))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ¬↑(x✝ i) ≤ 1 / 2
⊢ g (↑(Cube.insertAt i) (Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑(x✝ i) - 1), fun j ↦ x✝ ↑j)) =
    g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))

Tactic:
;

Goal state after:
case neg
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
f g : ↑(Ω^ N X x)
x✝ : N → ↑I
h✝ : ¬↑(x✝ i) ≤ 1 / 2
⊢ g (↑(Cube.insertAt i) (Set.projIcc 0 1 Path.extend._proof_2 (2 * ↑(x✝ i) - 1), fun j ↦ x✝ ↑j)) =
    g (Function.update x✝ i (Set.projIcc 0 1 ⋯ (2 * ↑(x✝ i) - 1)))
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
f : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (f fun j ↦ if j = i then σ (x✝ i) else x✝ j) = (fromLoop i (Path.symm (toLoop i f))) x✝

Tactic:
;

Goal state after:
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
⊢ (f fun j ↦ if j = i then σ (x✝ i) else x✝ j) = (fromLoop i (Path.symm (toLoop i f))) 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
f : ↑(Ω^ N X x)
x✝ : N → ↑I
⊢ (f fun j ↦ if j = i then σ (x✝ i) else x✝ j) =
    f (↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝).1, (↑(Cube.splitAt i) x✝).2))

Tactic:
;

Goal state after:
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
⊢ (f fun j ↦ if j = i then σ (x✝ i) else x✝ j) =
    f (↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝).1, (↑(Cube.splitAt i) x✝).2))
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
⊢ (fun j ↦ if j = i then σ (x✝ i) else x✝ j) = ↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝).1, (↑(Cube.splitAt i) x✝).2)

Tactic:
;

Goal state after:
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
⊢ (fun j ↦ if j = i then σ (x✝ i) else x✝ j) = ↑(Cube.insertAt i) (σ (↑(Cube.splitAt i) x✝).1, (↑(Cube.splitAt i) x✝).2)
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:
;

Goal state after:
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✝
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 j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (transAt i (transAt j a b) (transAt j c d)) y✝ = (transAt j (transAt i a c) (transAt i b d)) y✝

Tactic:
;

Goal state after:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
⊢ (transAt i (transAt j a b) (transAt j c d)) y✝ = (transAt j (transAt i a c) (transAt i b d)) y✝
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
n : ℕ
i : Fin (n + 1)
x✝ : α × Vector α n
a : α
l : Vector α n
⊢ Tendsto (fun p ↦ insertIdx p.1 i p.2) (𝓝 a ×ˢ 𝓝 l) (𝓝 (insertIdx (a, l).1 i (a, l).2))
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
x✝ : α × α
| edist x✝.1 x✝.2 < δ

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h : ⨆ x ∈ s, infEDist x t < δ ∧ ⨆ y ∈ t, infEDist y s < δ
x✝ : α × α
| edist x✝.1 x✝.2 < δ
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))

Tactic:
;

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) x✝

Tactic:
;

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i

Tactic:
;

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
;

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))

Tactic:
;

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) x✝

Tactic:
;

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i)))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i))) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i

Tactic:
;

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
;

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ¬↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))

Tactic:
;

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) x✝

Tactic:
;

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j))) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j)))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) x✝
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i

Tactic:
;

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ x✝ = j → ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i

Tactic:
;

Goal state after:
case pos.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
x✝ : N
h : i ≠ x✝
h✝ : ↑(y✝ x✝) ≤ 1 / 2
⊢ ¬x✝ = i
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))

Tactic:
;

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) x✝

Tactic:
;

Goal state after:
case neg.e_6
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
h : i ≠ j
a b c d : ↑(Ω^ N X x)
y✝ : N → ↑I
h✝¹ : ¬↑(y✝ i) ≤ 1 / 2
h✝ : ¬↑(y✝ j) ≤ 1 / 2
x✝ : N
⊢ Function.update (Function.update y✝ i (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1))) j
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1)) x✝ =
    Function.update (Function.update y✝ j (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ j) - 1))) i
      (Set.projIcc 0 1 transAt._proof_3 (2 * ↑(y✝ i) - 1)) x✝
Module: Mathlib.Topology.MetricSpace.Closeds

Goal state before:
pp: α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {p | edist p.1 p.2 ≤ δ} (s, t).1
x✝ : α × α
| edist x✝.1 x✝.2 ≤ δ

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : PseudoEMetricSpace α
s t : Set α
δ : ℝ≥0∞
h :
  (s, t).1 ⊆ SetRel.preimage {p | edist p.1 p.2 ≤ δ} (s, t).2 ∧ (s, t).2 ⊆ SetRel.image {p | edist p.1 p.2 ≤ δ} (s, t).1
x✝ : α × α
| edist x✝.1 x✝.2 ≤ δ