mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l

pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l

Tactic:
·

Goal state after:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l

Tactic:
·

Goal state after:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
q : ↑(GoodProducts (π C fun x ↦ ord I x < o))
l : ↑(MaxProducts C ho)
this : Inhabited I
h : ¬↑↑q = []
⊢ List.Lex (fun x1 x2 ↦ x1 < x2) ↑↑q ↑↑l

Tactic:
rw [← List.cons_head!_tail h, max_eq_o_cons_tail C hsC ho l]
    apply List.Lex.rel
    rw [← Ordinal.typein_lt_typein (· < ·)]
    simp only [term, Ordinal.typein_enum]
    exact Products.prop_of_isGood C _ q.prop q.val.val.head! (List.head!_mem_self h)

Goal state after:
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖

pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
·

Goal state after:
case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∈ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∉ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

Tactic:
·

Goal state after:
case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∈ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∉ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖

Tactic:
·

Goal state after:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : (tsupport ⇑f).Nonempty
x : α
left✝ : x ∈ tsupport ⇑f
hmax : IsMaxOn (fun x ↦ ‖f x‖) (tsupport ⇑f) x
y : α
hy : y ∉ tsupport ⇑f
⊢ ‖f y‖ ≤ ‖f x‖
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖

Tactic:
·

Goal state after:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
hs : ¬(tsupport ⇑f).Nonempty
⊢ ∃ x, ‖f x‖ = ‖f‖
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
·

Goal state after:
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : IsEmpty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
·

Goal state after:
case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : IsEmpty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M

Tactic:
·

Goal state after:
case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
M0 : 0 < M
he : Nonempty α
⊢ (∀ (x : α), ‖f x‖ < M) → ‖f‖ < M
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
·

Goal state after:
case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
·

Goal state after:
case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
c : Nonempty α
f : α →ᵇ γ
h : f ∈ C_cb(α, γ)
M : ℝ
hM : M ≤ 0
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : tsupport g = ∅
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C

pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
·

Goal state after:
case inl
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : tsupport g = ∅
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C

Tactic:
·

Goal state after:
case inr
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
⊢ ∃ C, ∀ (x y : α), dist (g x) (g y) ≤ C
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left✝ : z ∈ tsupport g
hmax : IsMaxOn (fun x ↦ ‖g x‖) (tsupport g) z
x : α
hx : x ∈ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖

pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left✝ : z ∈ tsupport g
hmax : IsMaxOn (fun x ↦ ‖g x‖) (tsupport g) z
x : α
hx : x ∉ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖

Tactic:
·

Goal state after:
case pos
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left✝ : z ∈ tsupport g
hmax : IsMaxOn (fun x ↦ ‖g x‖) (tsupport g) z
x : α
hx : x ∈ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖
Module: Mathlib.Topology.ContinuousMap.BoundedCompactlySupported

Goal state before:
pp: case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left✝ : z ∈ tsupport g
hmax : IsMaxOn (fun x ↦ ‖g x‖) (tsupport g) z
x : α
hx : x ∉ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖

Tactic:
·

Goal state after:
case neg
α : Type u_1
γ : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : NonUnitalNormedRing γ
g : α → γ
hg₁ : Continuous g
hg₂ : HasCompactSupport g
hs : (tsupport g).Nonempty
z : α
left✝ : z ∈ tsupport g
hmax : IsMaxOn (fun x ↦ ‖g x‖) (tsupport g) z
x : α
hx : x ∉ tsupport g
⊢ ‖g x‖ ≤ ‖g z‖
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (g x) (g x') < ε₂

pp: case refine_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (f x') (g x') < ε₁ / 2

Tactic:
·

Goal state after:
case refine_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (g x) (g x') < ε₂
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
⊢ (w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

pp: case h₂
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
⊢ (m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
·

Goal state after:
case h₁
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hC : IsClosed C
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
l : ↑(MaxProducts C ho)
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
this : Inhabited I
m : Products I →₀ ℤ
hmmem : m ∈ Finsupp.supported ℤ ℤ {m | m < (↑l).Tail}
hmsum : (m.sum fun i a ↦ a • Products.eval (C' C ho) i) = (Linear_CC' C hsC ho) (Products.eval C ↑l)
hse : (πs C o).range = (Linear_CC' C hsC ho).ker
n : LocallyConstant ↑(π C fun x ↦ ord I x < o) ℤ
w : { l // Products.isGood (π C fun x ↦ ord I x < o) l } →₀ ℤ
hn :
  ((w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) +
      m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) =
    Products.eval C ↑l
hc : (w.sum fun i a ↦ a • eval (π C fun x ↦ ord I x < o) i) = n
⊢ (w.sum fun a b ↦ (πs C o) (b • eval (π C fun x ↦ ord I x < o) a)) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: case refine_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (f x') (g x') < ε₁ / 2

Tactic:
·

Goal state after:
case refine_3
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : CompactSpace β
A : Set (α →ᵇ β)
closed : IsClosed A
H : ∀ (x₀ : α), ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ↑A), dist (↑i x) (↑i x') < ε
ε : ℝ
ε0 : ε > 0
ε₁ : ℝ
ε₁0 : 0 < ε₁
εε₁ : ε₁ < ε
ε₂ : ℝ := ε₁ / 2 / 2
ε₂0 : ε₂ > 0
U : α → Set α
hU : ∀ (x : α), x ∈ U x ∧ IsOpen (U x) ∧ ∀ y ∈ U x, ∀ z ∈ U x, ∀ {f : α →ᵇ β}, f ∈ A → dist (f y) (f z) < ε₂
tα : Set α
left✝¹ : tα ⊆ univ
hfin✝ : tα.Finite
htα : univ ⊆ ⋃ x ∈ tα, U x
val✝¹ : Fintype ↑tα
tβ : Set β
left✝ : tβ ⊆ univ
hfin : tβ.Finite
htβ : univ ⊆ ⋃ y ∈ tβ, ball y ε₂
val✝ : Fintype ↑tβ
F : β → β
hF : ∀ (y : β), F y ∈ tβ ∧ dist y (F y) < ε₂
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ β
hg : g ∈ A
f_eq_g : (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨f, hf⟩ = (fun f a ↦ ⟨F (↑f ↑a), ⋯⟩) ⟨g, hg⟩
x x' : α
x'tα : x' ∈ tα
hx' : x ∈ U x'
⊢ dist (f x') (g x') < ε₁ / 2
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case pos
α : 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)
hb : f ⊤ = g ⊥
⊢ C(↑(Icc a c), E)

pp: case neg
α : 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)
hb : ¬f ⊤ = g ⊥
⊢ C(↑(Icc a c), E)

Tactic:
·

Goal state after:
case pos
α : 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)
hb : f ⊤ = g ⊥
⊢ C(↑(Icc a c), E)
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case neg
α : 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)
hb : ¬f ⊤ = g ⊥
⊢ C(↑(Icc a c), E)

Tactic:
·

Goal state after:
case neg
α : 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)
hb : ¬f ⊤ = g ⊥
⊢ C(↑(Icc a c), E)
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a c : α
E : Type u_2
inst✝² : TopologicalSpace E
x : α
inst✝¹ : Fact (a ≤ x)
inst✝ : Fact (x ≤ c)
f : C(↑(Icc a x), E)
g : C(↑(Icc x c), E)
hb : f ⊤ = g ⊥
hx : x ∈ Icc x c
⊢ ((f.concat g).comp IccInclusionRight) ⟨x, hx⟩ = g ⟨x, hx⟩

pp: case inr
α : 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)
hb : f ⊤ = g ⊥
x : α
hx : x ∈ Icc b c
hxb : x ≠ b
⊢ ((f.concat g).comp IccInclusionRight) ⟨x, hx⟩ = g ⟨x, hx⟩

Tactic:
·

Goal state after:
case inl
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a c : α
E : Type u_2
inst✝² : TopologicalSpace E
x : α
inst✝¹ : Fact (a ≤ x)
inst✝ : Fact (x ≤ c)
f : C(↑(Icc a x), E)
g : C(↑(Icc x c), E)
hb : f ⊤ = g ⊥
hx : x ∈ Icc x c
⊢ ((f.concat g).comp IccInclusionRight) ⟨x, hx⟩ = g ⟨x, hx⟩
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: case inr
α : 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)
hb : f ⊤ = g ⊥
x : α
hx : x ∈ Icc b c
hxb : x ≠ b
⊢ ((f.concat g).comp IccInclusionRight) ⟨x, hx⟩ = g ⟨x, hx⟩

Tactic:
·

Goal state after:
case inr
α : 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)
hb : f ⊤ = g ⊥
x : α
hx : x ∈ Icc b c
hxb : x ≠ b
⊢ ((f.concat g).comp IccInclusionRight) ⟨x, hx⟩ = g ⟨x, hx⟩
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun x1 x2 ↦ x1 ≥ x2) fun i ↦ 𝓟 (A \ U i)
this : (⨅ i, 𝓟 (A \ U i)).NeBot
hle : ⨅ i, 𝓟 (A \ U i) ≤ 𝓟 A
⊢ False

Tactic:
rcases hA hle with ⟨a, ha, hac⟩

Goal state after:
ι : Type u_1
E : Type u_2
inst✝² : TopologicalSpace E
A : Set E
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hA : IsCountablyCompact A
U : ι → Set E
hUo : ∀ (i : ι), IsOpen[inst✝²] (U i)
hAU : A ⊆ ⋃ i, U i
hdU : Directed (fun x1 x2 ↦ x1 ⊆ x2) U
h : ∀ (i : ι), ¬A ⊆ U i
hdir : Directed (fun x1 x2 ↦ x1 ≥ x2) fun i ↦ 𝓟 (A \ U i)
this : (⨅ i, 𝓟 (A \ U i)).NeBot
hle : ⨅ i, 𝓟 (A \ U i) ≤ 𝓟 A
a : E
ha : a ∈ A
hac : ClusterPt a (⨅ i, 𝓟 (A \ U i))
⊢ False
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
hac : ∀ a ∈ A, ¬MapClusterPt a atTop x
⊢ False

Tactic:
let V : ℕ → Set E := fun n => (closure (x '' Ici n))ᶜ

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
h : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, A ⊆ ⋃ i ∈ t, U i
x : ℕ → E
hx : ∀ᶠ (n : ℕ) in atTop, x n ∈ A
hac : ∀ a ∈ A, ¬MapClusterPt a atTop x
V : ℕ → Set E := fun n ↦ (closure[inst✝] (x '' Ici n))ᶜ
⊢ False