mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Compactification.OnePoint.Sphere

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝⁷ : Fintype ι
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module ℝ V
inst✝⁴ : FiniteDimensional ℝ V
inst✝³ : TopologicalSpace V
inst✝² : IsTopologicalAddGroup V
inst✝¹ : ContinuousSMul ℝ V
inst✝ : T2Space V
h : finrank ℝ V + 1 = Fintype.card ι
⊢ OnePoint V ≃ₜ ↑(sphere 0 1)

Tactic:
by
  classical
  have : Nonempty ι := Fintype.card_pos_iff.mp <| by lia
  let v : EuclideanSpace ℝ ι := .single (Classical.arbitrary ι) 1
  have hv : ‖v‖ = 1 := by simp [v]
  have hv₀ : v ≠ 0 := fun contra ↦ by simp [contra] at hv
  have : Fact (finrank ℝ (EuclideanSpace ℝ ι) = finrank ℝ V + 1) := ⟨by simp [h]⟩
  have hV : finrank ℝ V = finrank ℝ (ℝ ∙ v)ᗮ := (finrank_orthogonal_span_singleton hv₀).symm
  letI e : V ≃ₜ (ℝ ∙ v)ᗮ := (FiniteDimensional.nonempty_continuousLinearEquiv_of_finrank_eq hV).some
  exact e.onePointCongr.trans <| onePointHyperplaneHomeoUnitSphere hv

Goal state after:
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∃ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i ≠ true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 0

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₂ : ∃ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i ≠ true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 0
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ ↑x i ≠ true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 0

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ ↑x i ≠ true
⊢ ((if SwapTrue o (↑x) (term I ho) = true then 1 else 0) - if ↑x (term I ho) = true then 1 else 0) = 0
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ ↑x i ≠ true
⊢ False

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ ↑x i ≠ true
⊢ False
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ SwapTrue o (↑x) i ≠ true
⊢ False

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₁ : ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
i : I
hi : i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩) ∧ SwapTrue o (↑x) i ≠ true
⊢ False
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
h₁ : ∃ i ∈ ↑l.Tail, SwapTrue o (↑x) i ≠ true
⊢ 0 = 1

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
h₁ : ∃ i ∈ ↑l.Tail, SwapTrue o (↑x) i ≠ true
⊢ 0 = 1
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ SwapTrue o (↑x) i ≠ true
⊢ 0 = 1

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ SwapTrue o (↑x) i ≠ true
⊢ 0 = 1
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ SwapTrue o (↑x) i ≠ true
⊢ False

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ SwapTrue o (↑x) i ≠ true
⊢ False
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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ ↑x i ≠ true
⊢ False

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
inst✝ : Inhabited I
l : Products I
hl : ↑l ≠ []
hlh : (↑l).head! = term I ho
hlc : List.IsChain (fun x1 x2 ↦ x1 > x2) (term I ho :: ↑l.Tail)
x : ↑(C' C ho)
hi' : ∀ i ∈ ↑l.Tail, ↑x i = SwapTrue o (↑x) i
H : (∀ i ∈ ↑l.Tail, ↑x i = true) = ∀ i ∈ ↑l.Tail, SwapTrue o (↑x) i = true
h₃ : ∀ i ∈ ↑(Tail ⟨term I ho :: ↑l.Tail, hlc⟩), ↑x i = true
i : I
hi : i ∈ ↑l.Tail ∧ ↑x i ≠ true
⊢ False
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:
· have F_f_g : F (f x') = F (g x') :=
          (congr_arg (fun f : tα → tβ => (f ⟨x', x'tα⟩ : β)) f_eq_g :)
        calc
          dist (f x') (g x') ≤ dist (f x') (F (f x')) + dist (g x') (F (f x')) :=
            dist_triangle_right _ _ _
          _ = dist (f x') (F (f x')) + dist (g x') (F (g x')) := by rw [F_f_g]
          _ < ε₂ + ε₂ := (add_lt_add (hF (f x')).2 (hF (g x')).2)
          _ = ε₁ / 2 := add_halves _

Goal state after:
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
x✝ : α
⊢ f x✝ = (F g) x✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
x✝ : α
⊢ f x✝ = (F g) x✝
Module: Mathlib.Topology.ContinuousMap.Bounded.ArzelaAscoli

Goal state before:
pp: α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf✝ : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
hf : F g ∈ A
x✝ : α
⊢ f x✝ = (F g) x✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x ↦ ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf✝ : f ∈ A
g : α →ᵇ ↑s := codRestrict s f ⋯
hf : F g ∈ A
x✝ : α
⊢ f x✝ = (F g) x✝
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst✝] (U i)
hAU : A ∪ B ⊆ ⋃ i, U i
t₁ : Set ℕ
ht₁ : t₁.Finite
hA_sub : A ⊆ ⋃ k ∈ t₁, U k
t₂ : Set ℕ
ht₂ : t₂.Finite
hB_sub : B ⊆ ⋃ k ∈ t₂, U k
x✝ : E
⊢ x✝ ∈ (⋃ k ∈ t₁, U k) ∪ ⋃ k ∈ t₂, U k ↔ x✝ ∈ ⋃ k ∈ t₁ ∪ t₂, U k

Tactic:
;

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
A B : Set E
hA : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → A ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ A ⊆ ⋃ i ∈ t, U i
hB : ∀ (U : ℕ → Set E), (∀ (i : ℕ), IsOpen[inst✝] (U i)) → B ⊆ ⋃ i, U i → ∃ t, t.Finite ∧ B ⊆ ⋃ i ∈ t, U i
U : ℕ → Set E
hUo : ∀ (i : ℕ), IsOpen[inst✝] (U i)
hAU : A ∪ B ⊆ ⋃ i, U i
t₁ : Set ℕ
ht₁ : t₁.Finite
hA_sub : A ⊆ ⋃ k ∈ t₁, U k
t₂ : Set ℕ
ht₂ : t₂.Finite
hB_sub : B ⊆ ⋃ k ∈ t₂, U k
x✝ : E
⊢ x✝ ∈ (⋃ k ∈ t₁, U k) ∪ ⋃ k ∈ t₂, U k ↔ x✝ ∈ ⋃ k ∈ t₁ ∪ t₂, U k
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃ i ∈ S, i)

Tactic:
;

Goal state after:
E : Type u_2
inst✝ : TopologicalSpace E
S : Set (Set E)
hf : S.Finite
hc : ∀ s ∈ S, IsCountablyCompact s
⊢ IsCountablyCompact (⋃ i ∈ S, i)
Module: Mathlib.Topology.Convenient.Localization

Goal state before:
pp: ι : Type t
X✝ : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X✝ i)
X Y Z : TopCat
⊢ IsIso ((toContinuousGeneratedByCat X✝).map (GeneratedByTopCat.adjCounit.app Z))

Tactic:
;

Goal state after:
ι : Type t
X✝ : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X✝ i)
X Y Z : TopCat
⊢ IsIso ((toContinuousGeneratedByCat X✝).map (GeneratedByTopCat.adjCounit.app Z))
Module: Mathlib.Topology.Convenient.Localization

Goal state before:
pp: ι : Type t
X✝ : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X✝ i)
X Y Z : TopCat
⊢ IsIso (toGeneratedByTopCat.map (GeneratedByTopCat.adjCounit.app Z))

Tactic:
;

Goal state after:
ι : Type t
X✝ : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X✝ i)
X Y Z : TopCat
⊢ IsIso (toGeneratedByTopCat.map (GeneratedByTopCat.adjCounit.app Z))
Module: Mathlib.Topology.Convenient.OpenClosed

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
⊢ IsGeneratedBy X ↑F

Tactic:
let W (a : Σ (i : ι), C(X i, Y)) : TopologicalSpace.Closeds (X a.1) :=
    ⟨a.2 ⁻¹' F, IsClosed.preimage a.2.continuous hF⟩

Goal state after:
ι : Type u_1
X : ι → Type u_2
inst✝³ : (i : ι) → TopologicalSpace (X i)
Y : Type u_3
inst✝² : TopologicalSpace Y
inst✝¹ : ∀ (i : ι) (F : TopologicalSpace.Closeds (X i)), IsGeneratedBy X ↥F
inst✝ : IsGeneratedBy X Y
F : Set Y
hF : IsClosed[inst✝²] F
W : (a : (i : ι) × C(X i, Y)) → TopologicalSpace.Closeds (X a.fst) :=
  fun a ↦ { carrier := ⇑a.snd ⁻¹' F, isClosed' := ⋯ }
⊢ IsGeneratedBy X ↑F
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a✝ : M
⊢ ({ toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((const M 1).prodMk (ContinuousMap.id M))) a✝ =
    (ContinuousMap.id M) a✝

Tactic:
;

Goal state after:
M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a✝ : M
⊢ ({ toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((const M 1).prodMk (ContinuousMap.id M))) a✝ =
    (ContinuousMap.id M) a✝
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a✝ : M
⊢ ({ toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((ContinuousMap.id M).prodMk (const M 1))) a✝ =
    (ContinuousMap.id M) a✝

Tactic:
;

Goal state after:
M : Type u
inst✝² : MulOneClass M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
a✝ : M
⊢ ({ toFun := Function.uncurry Mul.mul, continuous_toFun := ⋯ }.comp ((ContinuousMap.id M).prodMk (const M 1))) a✝ =
    (ContinuousMap.id M) a✝
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: t : ↑I
⊢ Set.projIcc 0 1 qRight._proof_1 (2 * ↑(t, 1).1 / (1 + ↑(t, 1).2)) = Set.projIcc 0 1 ⋯ ↑t

Tactic:
;

Goal state after:
t : ↑I
⊢ Set.projIcc 0 1 qRight._proof_1 (2 * ↑(t, 1).1 / (1 + ↑(t, 1).2)) = Set.projIcc 0 1 ⋯ ↑t
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ γ (qRight (t, 0)) = γ ⟨2 * ↑t, ⋯⟩

pp: case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ γ (qRight (t, 0)) = y

Tactic:
;

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ γ (qRight (t, 0)) = γ ⟨2 * ↑t, ⋯⟩

case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ γ (qRight (t, 0)) = y
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ qRight (t, 0) = 1

Tactic:
;

Goal state after:
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ qRight (t, 0) = 1
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑1

Tactic:
;

Goal state after:
case neg
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ¬↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑1
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ qRight (t, 0) = ⟨2 * ↑t, ⋯⟩

Tactic:
;

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ qRight (t, 0) = ⟨2 * ↑t, ⋯⟩
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑⟨2 * ↑t, ⋯⟩

Tactic:
;

Goal state after:
case pos
X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Path x y
t : ↑I
h : ↑t ≤ 1 / 2
⊢ ↑(qRight (t, 0)) = ↑⟨2 * ↑t, ⋯⟩
Module: Mathlib.Topology.Homotopy.HSpaces

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

Tactic:
;

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

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

Tactic:
;

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

Goal state before:
pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux
hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy
this : ContractibleSpace ↑Ux
⊢ ContractibleSpace
    ↑(match (Ux, Uy) with
      | (Ux, Uy) => Ux ×ˢ Uy)

Tactic:
have : ContractibleSpace Uy := hUy.2

Goal state after:
case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
x✝ y✝ : X
ι : Type u_3
inst✝¹ : StronglyLocallyContractibleSpace X
inst✝ : StronglyLocallyContractibleSpace Y
x : X
y : Y
Ux : Set X
Uy : Set Y
hUx : Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux
hUy : Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy
this✝ : ContractibleSpace ↑Ux
this : ContractibleSpace ↑Uy
⊢ ContractibleSpace
    ↑(match (Ux, Uy) with
      | (Ux, Uy) => Ux ×ˢ Uy)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case a
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i : ℕ
⊢ {x ∈ J | edist (Exists.choose hJ) x ≤ ↑n * c} ⊆ J

Tactic:
;

Goal state after:
case a
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
hn : 1 ≤ n
hJ_card : ↑(#J) ≤ a ^ n
i : ℕ
⊢ {x ∈ J | edist (Exists.choose hJ) x ≤ ↑n * c} ⊆ J