mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : 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 ⊥
h : α → E := fun t ↦ if t ≤ b then (IccExtendCM f) t else (IccExtendCM g) t
this : Continuous[inst✝⁴, inst✝] h
⊢ Continuous[instTopologicalSpaceSubtype, inst✝] fun t ↦ h ↑t

Tactic:
by fun_prop

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

Tactic:
apply Submodule.finsuppSum_mem

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
⊢ ∀ (c : { l // Products.isGood (π C fun x ↦ ord I x < o) l }),
    w c ≠ 0 → (πs C o) (w c • eval (π C fun x ↦ ord I x < o) c) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
Module: Mathlib.Topology.ContinuousMap.Interval

Goal state before:
pp: α : 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 ⊥
h : α → E := fun t ↦ if t ≤ b then (IccExtendCM f) t else (IccExtendCM g) t
⊢ Continuous[inst✝⁴, inst✝] ⇑(IccExtendCM f)

Tactic:
by fun_prop

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

Goal state before:
pp: α : 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 ⊥
h : α → E := fun t ↦ if t ≤ b then (IccExtendCM f) t else (IccExtendCM g) t
⊢ Continuous[inst✝⁴, inst✝] ⇑(IccExtendCM g)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Compactness.CountablyCompact

Goal state before:
pp: E : Type u_2
inst✝ : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
x✝¹ : f.NeBot
x✝ : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
⊢ ∀ᶠ (n : ℕ) in atTop, x n ∈ A

Tactic:
simpa using hx.mono_right hle

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

Goal state before:
pp: α : 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) (f x') + dist (g x) (g x') + dist (f x') (g x') ≤ ε₂ + ε₂ + ε₁ / 2

Tactic:
refine le_of_lt (add_lt_add (add_lt_add ?_ ?_) ?_)
      · exact (hU x').2.2 _ hx' _ (hU x').1 hf
      · exact (hU x').2.2 _ hx' _ (hU x').1 hg
      · 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.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
⊢ (m.sum fun i a ↦ a • (List.map (e C) (term I ho :: ↑i)).prod) ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})

Tactic:
apply Submodule.finsuppSum_mem

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
⊢ ∀ (c : Products I),
    m c ≠ 0 → m c • (List.map (e C) (term I ho :: ↑c)).prod ∈ Submodule.span ℤ (Products.eval C '' {m | m < ↑l})
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: 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
h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun x ↦ ord I x < o)))
h : LinearIndependent ℤ (eval (C' C ho))
f : ↑(MaxProducts C ho) → ↑(GoodProducts (C' C ho)) := MaxToGood C hC hsC ho h₁
hf : Function.Injective f
hh : (fun l ↦ Products.eval (C' C ho) (↑l).Tail) = eval (C' C ho) ∘ f
⊢ LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ (eval (C' C ho) ∘ f)

Tactic:
exact h.comp f hf

Goal state after:
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:
exact hf.isCountablyCompact_biUnion hc

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
⊢ ∀ t₁ ∈ range (Iic ∘ 𝓟), ∀ t₂ ∈ range (Iic ∘ 𝓟), ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ range (Iic ∘ 𝓟), x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
by
      rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl
      exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩

Goal state after:
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakPseudoEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
s : Set (Option α)
so : IsOpen[inst✝] s
x : Option α
xs : x ∈ s
this : ∃ ε > 0, Metric.eball x ε ⊆ s
⊢ ∃ ε > 0, Metric.eball x ε ⊆ s

Tactic:
by rwa [← h_edist] at this

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
⊢ Continuous fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2))

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Continuous fun p ↦ 2 * ↑p.1

Tactic:
by fun_prop

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

Goal state before:
pp: ⊢ Continuous fun p ↦ 1 + ↑p.2

Tactic:
by fun_prop

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
θ : ↑I
γ : Path x y
⊢ Continuous fun t ↦ γ (qRight (t, θ))

Tactic:
by fun_prop

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ M X x)
⊢ Continuous fun t m ↦ t (e m)

Tactic:
by fun_prop

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
x✝ : X
M : Type ?u.15
x : X
e : M ≃ N
p : ↑(Ω^ N X x)
⊢ Continuous fun t n ↦ t (e.symm n)

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a →
      ↑(#J) ≤ a ^ n →
        ∀ {s t : T},
          (s, t) ∈ pairSet J a c → ∀ i < #J, (s, t) ∈ pairSetSeq J a c i → J.Nonempty → 1 ≤ n → edist s t ≤ ↑n * c
hn : n < 1
⊢ edist s t ≤ ↑n * c

Tactic:
suffices s = t by simp [this]

Goal state after:
case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
n : ℕ
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ_card : ↑(#J) ≤ a ^ n
s t : T
h : (s, t) ∈ pairSet J a c
i : ℕ
hiJ : i < #J
h' : (s, t) ∈ pairSetSeq J a c i
hJ : J.Nonempty
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {n : ℕ} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a →
      ↑(#J) ≤ a ^ n →
        ∀ {s t : T},
          (s, t) ∈ pairSet J a c → ∀ i < #J, (s, t) ∈ pairSetSeq J a c i → J.Nonempty → 1 ≤ n → edist s t ≤ ↑n * c
hn : n < 1
⊢ s = t
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p : Ω (↑(Ω^ { j // j ≠ i } X x)) const
⊢ Continuous Subtype.val

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ Antitone preCantorSet

Tactic:
refine antitone_nat_of_succ_le fun m ↦ ?_

Goal state after:
m : ℕ
⊢ preCantorSet (m + 1) ⊆ preCantorSet m
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α✝ : ι → Type u_2
s✝ : Set ((i : ι) → α✝ i)
i : ι
S✝ : Set ι
α : ι → Type u_3
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
s : Set ((j : ι) → α j)
⊢ Continuous[instTopologicalSpaceSubtype, Pi.topologicalSpace] fun x ↦ Sᶜ.domRestrict ↑x

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (cantorSequence x).get n ∈ cantorSet
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i ≤ x

Tactic:
cantorSequence_eq_self_sub_sum_cantorToTernary x n

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∈ cantorSet
⊢ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i ≤ x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (cantorSequence x).get n ∈ cantorSet
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i

Tactic:
cantorSequence_eq_self_sub_sum_cantorToTernary x n

Goal state after:
x : ℝ
hx : x ∈ cantorSet
n : ℕ
h_mem : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∈ cantorSet
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i
Module: Mathlib.Topology.List

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
this : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
hv : List.Forall₂ (fun s a ↦ IsOpen[inst✝] s ∧ a ∈ s) v l
⊢ List.Forall₂ (flip fun a s ↦ IsOpen[inst✝] s ∧ a ∈ s) v u

Tactic:
simp only [List.forall₂_and_left, Function.flip_def] at hv ⊢

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
l : List α
s : Set (List α)
u✝ : List (Set α)
hu✝¹ : List.Forall₂ (fun b s ↦ s ∈ 𝓝 b) l u✝
hus : sequence u✝ ⊆ s
v : List (Set α)
hvs : sequence v ⊆ s
this : ∀ᶠ (y : List α) in traverse 𝓝 l, y ∈ sequence v
u : List α
hu✝ : u ∈ sequence v
hu : List.Forall₂ (fun b a ↦ b ∈ id a) u v
hv : (∀ a ∈ v, IsOpen[inst✝] a) ∧ List.Forall₂ Membership.mem v l
⊢ (∀ a ∈ v, IsOpen[inst✝] a) ∧ List.Forall₂ Membership.mem v u
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ Continuous fun x i ↦ bif x i then 2 else 0

Tactic:
by fun_prop

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

Goal state before:
pp: N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : Path.Homotopy (toLoop i p) (toLoop i q)
⊢ Continuous Subtype.val

Tactic:
by fun_prop

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

Goal state before:
pp: case refine_3.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
p q : ↑(Ω^ N X x)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
⊢ (((toLoop j p).toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = ↑p y

pp: case refine_3.inl.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
p q : ↑(Ω^ N X x)
t : ↑I
y : N → ↑I
j : N
jH : y j = 0 ∨ y j = 1
H : Path.Homotopy (toLoop j p) (toLoop j q)
⊢ y j ∈ {0, 1}

Tactic:
exacts [congr_arg p ((Cube.splitAt j).left_inv _), jH]

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

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

Goal state after:
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 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
⊢ a
      (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)))) =
    a
      (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:
congr 1

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 neg
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
⊢ b
      (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))) =
    b
      (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:
congr 1

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 pos
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
⊢ c
      (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)))) =
    c
      (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:
congr 1

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 neg
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
⊢ d
      (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))) =
    d
      (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:
congr 1

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: N✝ : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
x : X
inst✝¹ : DecidableEq N✝
N : Type ?u.15
inst✝ : Unique N
p : ↑(Ω^ N X x)
⊢ Continuous[_, inst✝²] fun t ↦ p fun x ↦ t

Tactic:
by fun_prop

Goal state after:
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✝
N : Type ?u.15
inst✝ : Unique N
p : Ω X x
⊢ Continuous[_, inst✝²] fun c ↦ p (c default)

Tactic:
by fun_prop

Goal state after:
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 ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ

Tactic:
conv at h => enter [2, 2, 1, 1, _]; rw [edist_comm]

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 {x | edist x.2 x.1 ≤ δ} (s, t).1
⊢ ⨆ x ∈ s, infEDist x t ≤ δ ∧ ⨆ y ∈ t, infEDist y s ≤ δ
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
⊢ externalCoveringNumber ε A ≤ 1

Tactic:
rcases eq_empty_or_nonempty A with h_eq_empty | h_nonempty

Goal state after:
case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_eq_empty : A = ∅
⊢ externalCoveringNumber ε A ≤ 1

case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_nonempty : A.Nonempty
⊢ externalCoveringNumber ε A ≤ 1
Module: Mathlib.Topology.MetricSpace.CoveringNumbers

Goal state before:
pp: X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
⊢ coveringNumber ε A ≤ 1

Tactic:
rcases eq_empty_or_nonempty A with h_eq_empty | h_nonempty

Goal state after:
case inl
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_eq_empty : A = ∅
⊢ coveringNumber ε A ≤ 1

case inr
X : Type u_1
inst✝ : PseudoEMetricSpace X
A : Set X
ε : ℝ≥0
hA : ediam A ≤ ↑ε
h_nonempty : A.Nonempty
⊢ coveringNumber ε A ≤ 1