mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨x, val⟩ ∈ map Prod.toSigma (xs.zip ys)
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ val ∈ ys

pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : val ∈ dlookup x (map Prod.toSigma (xs.zip ys))
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ (map Prod.toSigma (xs.zip ys)).NodupKeys

Tactic:
]

Goal state after:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : ⟨x, val⟩ ∈ map Prod.toSigma (xs.zip ys)
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ val ∈ ys

case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : val ∈ dlookup x (map Prod.toSigma (xs.zip ys))
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ (map Prod.toSigma (xs.zip ys)).NodupKeys
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : val ∈ dlookup x (map Prod.toSigma (xs.zip ys))
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ xs.Nodup

Tactic:
]

Goal state after:
case neg.cons.cons
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : val ∈ dlookup x (map Prod.toSigma (xs.zip ys))
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
⊢ xs.Nodup
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : ∀ i_1 ∈ A, (i, j) ∈ {ij | (F ij.1 i_1, F ij.2 i_1) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : ∀ i_1 ∈ A, (i, j) ∈ {ij | (F ij.1 i_1, F ij.2 i_1) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ none.getD x = x

pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ none.getD x = x

α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap (⇑UniformFun.ofFun ∘ F) (UniformFun.uniformSpace X α) = inst✝¹ ↔
    UniformSpace.comap F (UniformFun.uniformSpace X α) = inst✝¹

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap (⇑UniformFun.ofFun ∘ F) (UniformFun.uniformSpace X α) = inst✝¹ ↔
    UniformSpace.comap F (UniformFun.uniformSpace X α) = inst✝¹
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = TopologicalSpace.induced (⇑UniformFun.ofFun ∘ F) (UniformFun.topologicalSpace X α) ↔
    inst✝¹ = TopologicalSpace.induced F Pi.topologicalSpace

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = TopologicalSpace.induced (⇑UniformFun.ofFun ∘ F) (UniformFun.topologicalSpace X α) ↔
    inst✝¹ = TopologicalSpace.induced F Pi.topologicalSpace
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : ∃ i, xs[i]? = some x
hy : ∃ i, xs[i]? = some y
⊢ x = y

Tactic:
]

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : ∃ i, xs[i]? = some x
hy : ∃ i, xs[i]? = some y
⊢ x = y
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ inst✝¹ = (UniformSpace.comap F (Pi.uniformSpace fun i ↦ α)).toTopologicalSpace ↔
    inst✝¹ = (UniformSpace.comap F (Pi.uniformSpace fun i ↦ α)).toTopologicalSpace

Tactic:
]

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

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ some x = some y

Tactic:
]

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ some x = some y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = xs[j]?

Tactic:
]

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[i]? = xs[j]?
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = some (List.applyId (xs.zip ys) y)

Tactic:
]

Goal state after:
case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ys[j]? = some (List.applyId (xs.zip ys) y)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous Subtype.val
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
⊢ Equicontinuous (id ∘ Subtype.val)

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous Subtype.val
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
⊢ Equicontinuous (id ∘ Subtype.val)
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos.e_a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ List.applyId (zip ?m.157 ys) ?pos.e_a.x✝ = List.applyId (xs.zip ys) y

pp: case pos.e_a.h₀
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ Nodup ?m.157

pp: case pos.e_a.h₁
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ length ?m.157 = ys.length

pp: case pos.e_a.x
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ α

pp: case pos.e_a.h₂
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ ?m.157[j]? = some ?pos.e_a.x✝

pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ List α

Tactic:
]

Goal state after:
case pos.e_a.h₀
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs.Nodup

case pos.e_a.h₁
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs.length = ys.length

case pos.e_a.h₂
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ xs[j]? = some y
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
⊢ map F ℱ ≤ 𝓝 ↑⟨f, f_mem⟩

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
⊢ map F ℱ ≤ 𝓝 ↑⟨f, f_mem⟩
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
H' : Tendsto (⇑UniformFun.ofFun) (map F ℱ) (𝓝 ((⇑UniformFun.ofFun ∘ Subtype.val) ⟨f, f_mem⟩))
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
]

Goal state after:
case inr.mpr
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
H' : Tendsto (⇑UniformFun.ofFun) (map F ℱ) (𝓝 ((⇑UniformFun.ofFun ∘ Subtype.val) ⟨f, f_mem⟩))
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ i < xs.length

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ i < xs.length
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : ∃ (h : i < xs.length), xs[i] = x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ i < xs.length

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
i : ℕ
h : ys[i]? = some (List.applyId (xs.zip ys) y)
hx : ∃ (h : i < xs.length), xs[i] = x
j : ℕ
hy : xs[j]? = some y
h₂ : xs.length = ys.length
⊢ i < xs.length
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) x ∈ ys
hy : List.applyId (xs.zip ys) y ∉ ys
⊢ x = y

Tactic:
]

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) x ∈ ys
hy : List.applyId (xs.zip ys) y ∉ ys
⊢ x = y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) y ∈ ys
hy : List.applyId (xs.zip ys) y ∉ ys
⊢ x = y

Tactic:
]

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) y ∈ ys
hy : List.applyId (xs.zip ys) y ∉ ys
⊢ x = y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) x ∉ ys
hy : List.applyId (xs.zip ys) y ∈ ys
⊢ x = y

Tactic:
]

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) x ∉ ys
hy : List.applyId (xs.zip ys) y ∈ ys
⊢ x = y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) y ∉ ys
hy : List.applyId (xs.zip ys) y ∈ ys
⊢ x = y

Tactic:
]

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : List.applyId (xs.zip ys) y ∉ ys
hy : List.applyId (xs.zip ys) y ∈ ys
⊢ x = y
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : x = y
hx : x ∉ xs
hy : y ∉ xs
⊢ x = y

pp: case neg.a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ y ∉ xs

pp: case neg.a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ x ∉ xs

Tactic:
]

Goal state after:
case neg
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : x = y
hx : x ∉ xs
hy : y ∉ xs
⊢ x = y

case neg.a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ y ∉ xs

case neg.a
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
hx : x ∉ xs
hy : y ∉ xs
⊢ x ∉ xs
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) = inst✝ ↔
    UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst✝

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) = inst✝ ↔
    UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst✝
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs).zip (map Sigma.snd xs))
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
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous Subtype.val
hS4 : S4 = DFunLike.coe '' S1
⊢ Equicontinuous Subtype.val

Tactic:
]

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
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous Subtype.val
hS4 : S4 = DFunLike.coe '' S1
⊢ Equicontinuous Subtype.val
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁)))
    (hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup),
    Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply

Tactic:
]

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst (List.toFinmap' (xs₀.zip xs₁)) ~ map Sigma.snd (List.toFinmap' (xs₀.zip xs₁)))
    (hnodup : (map Sigma.snd (List.toFinmap' (xs₀.zip xs₁))).Nodup),
    Injective (mapToSelf (List.toFinmap' (xs₀.zip xs₁)) hperm hnodup).apply
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsUniformInducing (⇑φ.symm ∘ F) ↔ IsUniformInducing F

Tactic:
]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ IsUniformInducing (⇑φ.symm ∘ F) ↔ IsUniformInducing F