mathlib-initiative/mathlib-tactics huggingface dataset:
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}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
⊢ Set.range (eval C) = Set.range (Sum.elim (fun l ↦ Products.eval C ↑l) fun l ↦ Products.eval C ↑l)

Tactic:
rw [← sum_equiv_comp_eval_eq_elim C hsC ho, Equiv.toFun_as_coe,
    EquivLike.range_comp (e := sum_equiv C hsC ho)]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ∀
    (j :
      match 0 with
      | 0 => ↑D
      | n.succ => PEmpty.{u_1 + 1}),
    ↑(match 0, j with
          | 0, i => PartialEquiv.single ![] ↑i
          | n.succ, i => PEmpty.elim i) ''
        closedBall 0 1 ⊆
      D

pp: case succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n✝ : ℕ
⊢ ∀
    (j :
      match n✝ + 1 with
      | 0 => ↑D
      | n.succ => PEmpty.{u_1 + 1}),
    ↑(match n✝ + 1, j with
          | 0, i => PartialEquiv.single ![] ↑i
          | n.succ, i => PEmpty.elim i) ''
        closedBall 0 1 ⊆
      D

Tactic:
<;>

Goal state after:
case zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
⊢ ∀
    (j :
      match 0 with
      | 0 => ↑D
      | n.succ => PEmpty.{u_1 + 1}),
    ↑(match 0, j with
          | 0, i => PartialEquiv.single ![] ↑i
          | n.succ, i => PEmpty.elim i) ''
        closedBall 0 1 ⊆
      D

case succ
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
n✝ : ℕ
⊢ ∀
    (j :
      match n✝ + 1 with
      | 0 => ↑D
      | n.succ => PEmpty.{u_1 + 1}),
    ↑(match n✝ + 1, j with
          | 0, i => PartialEquiv.single ![] ↑i
          | n.succ, i => PEmpty.elim i) ''
        closedBall 0 1 ⊆
      D
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 ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
⊢ OnePoint V ≃ₜ ↑(sphere 0 1)

Tactic:
have hv : ‖v‖ = 1 := by simp [v]

Goal state after:
ι : 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 ι
this : Nonempty ι
v : EuclideanSpace ℝ ι := EuclideanSpace.single (Classical.arbitrary ι) 1
hv : ‖v‖ = 1
⊢ OnePoint V ≃ₜ ↑(sphere 0 1)
Module: Mathlib.Topology.Compactness.CompactSystem

Goal state before:
pp: case refine_1
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h3 : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
h4 : ∀ (i : ℕ), C i ∈ S
⊢ (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty

pp: case refine_2
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
h3 : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
s : ∀ (i : ℕ), C i ∈ S
⊢ ⋂ i, C i = ∅ → ∃ n, C n = ∅

Tactic:
<;>

Goal state after:
case refine_1
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 : ∀ (C : ℕ → Set α), Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → ⋂ i, C i = ∅ → ∃ n, C n = ∅
C : ℕ → Set α
h3 : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
h4 : ∀ (i : ℕ), C i ∈ S
⊢ (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty

case refine_2
α : Type u_1
S : Set (Set α)
hpi : IsPiSystem S
h1 :
  ∀ (C : ℕ → Set α),
    Directed (fun x1 x2 ↦ x1 ⊇ x2) C → (∀ (i : ℕ), C i ∈ S) → (∀ (n : ℕ), (C n).Nonempty) → (⋂ i, C i).Nonempty
C : ℕ → Set α
h3 : Directed (fun x1 x2 ↦ x1 ⊇ x2) C
s : ∀ (i : ℕ), C i ∈ S
⊢ ⋂ i, C i = ∅ → ∃ n, C n = ∅
Module: Mathlib.Topology.ContinuousMap.SecondCountableSpace

Goal state before:
pp: case h.refine_1
X : Type u_1
Y : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : SecondCountableTopology X
inst✝¹ : LocallyCompactSpace X
inst✝ : SecondCountableTopology Y
this : ∀ (U : ↑(countableBasis X)), LocallyCompactSpace ↑↑U
K : (U : ↑(countableBasis X)) → CompactExhaustion ↑↑U := fun U ↦ CompactExhaustion.choice ↑↑U
⊢ ∀ K_1 ∈ ⋃ U, range fun n ↦ Subtype.val '' (K U) n, IsCompact K_1

Tactic:
simp only [mem_iUnion, mem_range]
    rintro K ⟨U, n, rfl⟩
    exact ((K U).isCompact _).image continuous_subtype_val

Goal state after:
Module: Mathlib.Topology.Filter

Goal state before:
pp: case hg
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t

pp: case hg'
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (Iic ∘ 𝓟) univ = univ

Tactic:
<;>

Goal state after:
case hg
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t

case hg'
ι : Sort u_1
α : Type u_2
f : ι → Filter α
⊢ (Iic ∘ 𝓟) univ = univ
Module: Mathlib.Topology.Filter

Goal state before:
pp: α : Type u_2
l₁ l₂ : Filter α
⊢ l₁ ⤳ l₂ ↔ l₁ ≤ l₂

Tactic:
simp only [specializes_iff_closure_subset, Filter.closure_singleton, Ici_subset_Ici]

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

Goal state before:
pp: case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
⊢ x ∈ some '' Metric.eball a r → x ∈ Metric.eball (some a) r

pp: case mpr
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
⊢ x ∈ Metric.eball (some a) r → x ∈ some '' Metric.eball a r

Tactic:
<;>

Goal state after:
case mp
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
⊢ x ∈ some '' Metric.eball a r → x ∈ Metric.eball (some a) r

case mpr
α : Type u
t : TopologicalSpace α
m : WeakPseudoEMetricSpace α
a : α
r : ℝ≥0∞
x : Option α
⊢ x ∈ Metric.eball (some a) r → x ∈ some '' Metric.eball a r
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
y : Option α
xy : edist none y = 0
⊢ none = y

pp: case some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
y : Option α
val✝ : α
xy : edist (some val✝) y = 0
⊢ some val✝ = y

Tactic:
<;>

Goal state after:
case none
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
y : Option α
xy : edist none y = 0
⊢ none = y

case some
α✝ : Type u
t✝ : TopologicalSpace α✝
m✝ : WeakPseudoEMetricSpace α✝
α : Type u
t : TopologicalSpace α
inst✝ : TopologicalSpace (Option α)
m : WeakEMetricSpace α
inst : EDist (Option α)
h_edist : inst = toEDist
h : IsOpenEmbedding some
y : Option α
val✝ : α
xy : edist (some val✝) y = 0
⊢ some val✝ = y
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case top
b : ℝ≥0∞
⊢ edist ∞ b = ∞ ↔ ∞ ≠ b ∧ (∞ = ∞ ∨ b = ∞)

pp: case coe
b : ℝ≥0∞
x✝ : ℝ≥0
⊢ edist (↑x✝) b = ∞ ↔ ↑x✝ ≠ b ∧ (↑x✝ = ∞ ∨ b = ∞)

Tactic:
<;>

Goal state after:
case top
b : ℝ≥0∞
⊢ edist ∞ b = ∞ ↔ ∞ ≠ b ∧ (∞ = ∞ ∨ b = ∞)

case coe
b : ℝ≥0∞
x✝ : ℝ≥0
⊢ edist (↑x✝) b = ∞ ↔ ↑x✝ ≠ b ∧ (↑x✝ = ∞ ∨ b = ∞)
Module: Mathlib.Topology.EMetricSpace.Weak

Goal state before:
pp: case top.top
⊢ edist ∞ ∞ = ∞ ↔ ∞ ≠ ∞ ∧ (∞ = ∞ ∨ ∞ = ∞)

pp: case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞ ↔ ∞ ≠ ↑x✝ ∧ (∞ = ∞ ∨ ↑x✝ = ∞)

pp: case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞ ↔ ↑x✝ ≠ ∞ ∧ (↑x✝ = ∞ ∨ ∞ = ∞)

pp: case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ edist ↑x✝¹ ↑x✝ = ∞ ↔ ↑x✝¹ ≠ ↑x✝ ∧ (↑x✝¹ = ∞ ∨ ↑x✝ = ∞)

Tactic:
<;>

Goal state after:
case top.top
⊢ edist ∞ ∞ = ∞ ↔ ∞ ≠ ∞ ∧ (∞ = ∞ ∨ ∞ = ∞)

case top.coe
x✝ : ℝ≥0
⊢ edist ∞ ↑x✝ = ∞ ↔ ∞ ≠ ↑x✝ ∧ (∞ = ∞ ∨ ↑x✝ = ∞)

case coe.top
x✝ : ℝ≥0
⊢ edist ↑x✝ ∞ = ∞ ↔ ↑x✝ ≠ ∞ ∧ (↑x✝ = ∞ ∨ ∞ = ∞)

case coe.coe
x✝¹ x✝ : ℝ≥0
⊢ edist ↑x✝¹ ↑x✝ = ∞ ↔ ↑x✝¹ ≠ ↑x✝ ∧ (↑x✝¹ = ∞ ∨ ↑x✝ = ∞)
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : StronglyLocallyContractibleSpace X
⊢ LocallyContractibleSpace X

Tactic:
intro x U hU
  obtain ⟨V, ⟨hVmem, hVcontractible⟩, hVU⟩ := (contractible_basis x).mem_iff.mp hU
  refine ⟨V, hVU, hVmem, ?_⟩
  -- V is contractible, so the identity on V is nullhomotopic to a constant map
  obtain ⟨v₀, hid⟩ := id_nullhomotopic V
  -- The inclusion V ↪ U is homotopic to the constant map at (inclusion v₀)
  refine ⟨ContinuousMap.inclusion hVU v₀, ?_⟩
  convert! Homotopic.comp (.refl _) hid
  ext
  simp

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

Goal state before:
pp: case inl.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 0
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

pp: case inl.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 1
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

Tactic:
<;>

Goal state after:
case inl.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 0
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x

case inl.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 1
⊢ (↑(p.toContinuousMap (y j)) fun j_1 ↦ y ↑j_1) = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 0
⊢ (↑const fun j_1 ↦ y ↑j_1) = x

pp: case inl.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 1
⊢ (↑const fun j_1 ↦ y ↑j_1) = x

Tactic:
<;>

Goal state after:
case inl.inl
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 0
⊢ (↑const fun j_1 ↦ y ↑j_1) = x

case inl.inr
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
y : N → ↑I
j : N
p : Ω (↑(Ω^ { j_1 // j_1 ≠ j } X x)) const
Hj : y j = 1
⊢ (↑const fun j_1 ↦ y ↑j_1) = x
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case zero.refine_1
⊢ 0 ≤ 1 / 4

pp: case zero.refine_2
⊢ 1 / 4 ≤ 1

pp: case zero.refine_3
⊢ 0 ≤ 3 / 4

pp: case zero.refine_4
⊢ 3 / 4 ≤ 1

Tactic:
<;>

Goal state after:
case zero.refine_1
⊢ 0 ≤ 1 / 4

case zero.refine_2
⊢ 1 / 4 ≤ 1

case zero.refine_3
⊢ 0 ≤ 3 / 4

case zero.refine_4
⊢ 3 / 4 ≤ 1
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case h.«0»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨0, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨0, ⋯⟩) + ofDigits fun i ↦ a (i + 1)

pp: case h.«1»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨1, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨1, ⋯⟩) + ofDigits fun i ↦ a (i + 1)

pp: case h.«2»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨2, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨2, ⋯⟩) + ofDigits fun i ↦ a (i + 1)

Tactic:
<;>

Goal state after:
case h.«0»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨0, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨0, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨0, ⋯⟩) + ofDigits fun i ↦ a (i + 1)

case h.«1»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨1, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨1, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨1, ⋯⟩) + ofDigits fun i ↦ a (i + 1)

case h.«2»
i : ℕ
ih : ∀ {a : ℕ → Fin 3}, (∀ (n : ℕ), a n ≠ 1) → ofDigits a ∈ preCantorSet i
a : ℕ → Fin 3
this : (ofDigits fun i ↦ a (i + 1)) ∈ preCantorSet i
h : (fun i ↦ i) ⟨2, ⋯⟩ ≠ 1
⊢ ((ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨2, ⋯⟩) + ofDigits fun i ↦ a (i + 1)) ∨
    (2 + ofDigits fun i ↦ a (i + 1)) = ↑↑((fun i ↦ i) ⟨2, ⋯⟩) + ofDigits fun i ↦ a (i + 1)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: case fst
ι : 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)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑Sᶜ
⊢ ↑((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p)).1 x✝ = ↑p.1 x✝

pp: case snd
ι : 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)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑S
⊢ ((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p)).2 x✝ = p.2 x✝

Tactic:
<;>

Goal state after:
case fst
ι : 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)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑Sᶜ
⊢ ↑((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p)).1 x✝ = ↑p.1 x✝

case snd
ι : 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)
p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)
x✝ : ↑S
⊢ ((fun x ↦ (⟨Sᶜ.domRestrict ↑x, ⋯⟩, fun i ↦ ↑x ↑i)) ((fun p ↦ ⟨reorderRestrictProd S s p, ⋯⟩) p)).2 x✝ = p.2 x✝
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : ofDigits a = ofDigits b
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False

Tactic:
ofDigits_eq_sum_add_ofDigits a (n1 + 1),

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h : (∑ i ∈ Finset.range (n1 + 1), ofDigitsTerm a i + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) = ofDigits b
h1 : ∀ n < n1, a n = b n
h3 : a n1 = 0
h4 : b n1 = 2
this : ∑ x ∈ Finset.range n1, ofDigitsTerm a x = ∑ x ∈ Finset.range n1, ofDigitsTerm b x
⊢ False
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case pos
x : ℝ
n : ℕ
h✝ : 0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3
⊢ 3 * (Stream'.iterate cantorStep x).get n =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (↑↑0 * (↑3 ^ (n + 1))⁻¹))

pp: case neg
x : ℝ
n : ℕ
h✝ : ¬(0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3)
⊢ 3 * (Stream'.iterate cantorStep x).get n - 2 =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (↑↑2 * (↑3 ^ (n + 1))⁻¹))

Tactic:
<;>

Goal state after:
case pos
x : ℝ
n : ℕ
h✝ : 0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3
⊢ 3 * (Stream'.iterate cantorStep x).get n =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (↑↑0 * (↑3 ^ (n + 1))⁻¹))

case neg
x : ℝ
n : ℕ
h✝ : ¬(0 ≤ (Stream'.iterate cantorStep x).get n ∧ (Stream'.iterate cantorStep x).get n ≤ 1 / 3)
⊢ 3 * (Stream'.iterate cantorStep x).get n - 2 =
    3 * ((Stream'.iterate cantorStep x).get n - 3 ^ n * (↑↑2 * (↑3 ^ (n + 1))⁻¹))
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap (Prod.map f id)

pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ∧ IsClosedMap (Prod.map f id) → IsProperMap f

Tactic:
<;>

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ IsClosedMap (Prod.map f id)

case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Continuous f ∧ IsClosedMap (Prod.map f id) → IsProperMap f
Module: Mathlib.Topology.List

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
⊢ 𝓝 [] = pure []

pp: case cons
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
head✝ : α
tail✝ : List α
tail_ih✝ : 𝓝 tail✝ = pure tail✝
⊢ 𝓝 (head✝ :: tail✝) = pure (head✝ :: tail✝)

Tactic:
<;>

Goal state after:
case nil
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
⊢ 𝓝 [] = pure []

case cons
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology α
head✝ : α
tail✝ : List α
tail_ih✝ : 𝓝 tail✝ = pure tail✝
⊢ 𝓝 (head✝ :: tail✝) = pure (head✝ :: tail✝)
Module: Mathlib.Topology.Maps.Proper.UniversallyClosed

Goal state before:
pp: case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

pp: case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)) → IsProperMap f

Tactic:
<;>

Goal state after:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f → Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)) → IsProperMap f
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case refine_1
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d x y + d y z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z

pp: case refine_2
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d' x y + d' y z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z

Tactic:
<;>

Goal state after:
case refine_1
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d x y + d y z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z

case refine_2
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d' x y + d' y z ≤ d x y ⊔ d' x y + d y z ⊔ d' y z
Module: Mathlib.Topology.MetricSpace.BundledFun

Goal state before:
pp: case refine_1.h₁
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d x y ≤ d x y ⊔ d' x y

pp: case h₂
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d y z ≤ d y z ⊔ d' y z

pp: case refine_2.h₁
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d' x y ≤ d x y ⊔ d' x y

pp: case h₂
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d' y z ≤ d y z ⊔ d' y z

Tactic:
<;>

Goal state after:
case refine_1.h₁
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d x y ≤ d x y ⊔ d' x y

case h₂
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d y z ≤ d y z ⊔ d' y z

case refine_2.h₁
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d' x y ≤ d x y ⊔ d' x y

case h₂
X : Type u_1
R : Type u_2
inst✝³ : AddZeroClass R
inst✝² : SemilatticeSup R
inst✝¹ : AddLeftMono R
inst✝ : AddRightMono R
d d' : PseudoMetric X R
x y z : X
⊢ d' y z ≤ d y z ⊔ d' y z
Module: Mathlib.Topology.List

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

Tactic:
ContinuousAt,

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

Goal state before:
pp: case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (f i) x z ≤ (f i) x y → ∃ b ∈ s, (f i) x z ≤ (f b) x y

pp: case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (f i) x z ≤ (f i) y z → ∃ b ∈ s, (f i) x z ≤ (f b) y z

Tactic:
<;>

Goal state after:
case inr.refine_1
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (f i) x z ≤ (f i) x y → ∃ b ∈ s, (f i) x z ≤ (f b) x y

case inr.refine_2
X : Type u_1
R : Type u_2
Y : Type u_3
inst✝³ : AddCommMonoid R
inst✝² : LinearOrder R
inst✝¹ : AddLeftStrictMono R
inst✝ : IsOrderedAddMonoid R
f : Y → PseudoMetric X R
s : Finset Y
h✝ : ∀ d ∈ s, (f d).IsUltra
x y z : X
hs : s.Nonempty
i : Y
hi : i ∈ s
h : (f i) x z ≤ (f i) x y ∨ (f i) x z ≤ (f i) y z
⊢ (f i) x z ≤ (f i) y z → ∃ b ∈ s, (f i) x z ≤ (f b) y z