mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
n✝ : ℕ
J✝ : Finset T✝
inst✝² : DecidableEq T✝
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
t : T
i : ℕ
hiJ : i < #J
hJ : J.Nonempty
hn : 1 ≤ n
ht : t ∈ (logSizeBallSeq J ⋯ a c i).finset
hdist : edist (logSizeBallSeq J ⋯ a c i).point t ≤ ↑(logSizeBallSeq J ⋯ a c i).radius * c
h : ((logSizeBallSeq J ⋯ a c i).point, t) ∈ pairSet J a c
⊢ ↑n * c ≤ ↑n * c

Tactic:
]

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

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
⊢ ∀ (i : ↥J), ⨆ t, edist (f ↑i) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
⊢ ∀ (i : ↥J), ⨆ t, edist (f ↑i) (f ↑↑t) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
⊢ ∀ (i : { t // edist ⟨s, hs⟩ t ≤ c }), edist (f ↑⟨s, hs⟩) (f ↑↑i) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)

Tactic:
]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
⊢ ∀ (i : { t // edist ⟨s, hs⟩ t ≤ c }), edist (f ↑⟨s, hs⟩) (f ↑↑i) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: n : ℕ
⊢ preCantorSet n ⊆ preCantorSet 0

Tactic:
]

Goal state after:
n : ℕ
⊢ preCantorSet n ⊆ preCantorSet 0
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: ⊢ ⋂ n, preCantorSet n = (⋂ i, (fun x ↦ x / 3) '' preCantorSet i) ∪ ⋂ i, (fun x ↦ (2 + x) / 3) '' preCantorSet i

pp: case hf
⊢ Function.Bijective fun x ↦ (2 + x) / 3

pp: case hf
⊢ Function.Bijective fun x ↦ x / 3

Tactic:
]

Goal state after:
⊢ ⋂ n, preCantorSet n = (⋂ i, (fun x ↦ x / 3) '' preCantorSet i) ∪ ⋂ i, (fun x ↦ (2 + x) / 3) '' preCantorSet i

case hf
⊢ Function.Bijective fun x ↦ (2 + x) / 3

case hf
⊢ Function.Bijective fun x ↦ x / 3
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : ∃ a_1, a a_1 ≠ b a_1
⊢ False

Tactic:
]

Goal state after:
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h✝ : ofDigits a = ofDigits b
h : ∃ a_1, a a_1 ≠ b a_1
⊢ False
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_1
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ x = x

pp: case refine_1.a
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N

pp: case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N

Tactic:
]

Goal state after:
case refine_1.a
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N

case refine_1.hx
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i✝ : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
t : ↑I × ↑I
y : { j // j ≠ i✝ } → ↑I
i : { j // j ≠ i✝ }
iH : y i = 0 ∨ y i = 1
⊢ (Cube.insertAt i✝) (t.2, y) ∈ Cube.boundary N
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)
⊢ ∀ (i : ↑S), Continuous[instTopologicalSpaceSubtype, inst✝ ↑i] fun a ↦ ↑a ↑i

Tactic:
]

Goal state after:
ι : 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)
⊢ ∀ (i : ↑S), Continuous[instTopologicalSpaceSubtype, inst✝ ↑i] fun a ↦ ↑a ↑i
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hl : #J ≤ l + 1
⊢ #J - 1 + 1 - 1 + 1 ≤ #J - 1 + 1

Tactic:
]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hl : #J ≤ l + 1
⊢ #J - 1 + 1 - 1 + 1 ≤ #J - 1 + 1
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 :
  (∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm a n1 +
      (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm b n1 + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
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:
]

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
h :
  (∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm a n1 +
      (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ a (i + (n1 + 1))) =
    ∑ x ∈ Finset.range n1, ofDigitsTerm b x + ofDigitsTerm b n1 + (↑3 ^ (n1 + 1))⁻¹ * ofDigits fun i ↦ b (i + (n1 + 1))
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: n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
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
h :
  ((3 ^ n1)⁻¹ * ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹ =
    ((3 ^ n1)⁻¹ * ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * (3⁻¹ * (3 ^ n1)⁻¹)
⊢ (3 ^ n1)⁻¹ * ((ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹) =
    (3 ^ n1)⁻¹ * ((ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * 3⁻¹)

Tactic:
]

Goal state after:
n1 : ℕ
a b : ℕ → Fin 3
ha : ∀ (n : ℕ), a n ≠ 1
hb : ∀ (n : ℕ), b n ≠ 1
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
h :
  ((3 ^ n1)⁻¹ * ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹ =
    ((3 ^ n1)⁻¹ * ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * (3⁻¹ * (3 ^ n1)⁻¹)
⊢ (3 ^ n1)⁻¹ * ((ofDigits fun i ↦ a (1 + n1 + i)) * 3⁻¹) =
    (3 ^ n1)⁻¹ * ((ofDigits fun i ↦ b (1 + n1 + i)) * 3⁻¹ + 2 * 3⁻¹)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed (Prod.snd '' ⇑(Homeomorph.preimageImageRestrict α S s) '' (fun x ↦ ↑x) ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
⊢ IsClosed (Prod.snd '' ⇑(Homeomorph.preimageImageRestrict α S s) '' (fun x ↦ ↑x) ⁻¹' s)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace ↑(Sᶜ.domRestrict '' s)
⊢ IsClosed ((fun x ↦ ↑x) ⁻¹' s)

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
S : Set ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this : CompactSpace ↑(Sᶜ.domRestrict '' s)
⊢ IsClosed ((fun x ↦ ↑x) ⁻¹' s)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ (fun x ↦ x / 3) '' cantorSet ∪ (fun x ↦ (2 + x) / 3) '' cantorSet
⊢ ∃ y ∈ cantorSet, y / 3 = x ∨ (2 + y) / 3 = x

Tactic:
]

Goal state after:
x : ℝ
hx : x ∈ (fun x ↦ x / 3) '' cantorSet ∪ (fun x ↦ (2 + x) / 3) '' cantorSet
⊢ ∃ y ∈ cantorSet, y / 3 = x ∨ (2 + y) / 3 = x
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
S : Set ι
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), CompactSpace (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
this : S.domRestrict = Prod.fst ∘ ⇑(Homeomorph.piEquivPiSubtypeProd (fun x ↦ x ∈ S) α)
⊢ IsClosed (Prod.fst '' ⇑(Homeomorph.piEquivPiSubtypeProd (fun x ↦ x ∈ S) α) '' s)

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
S : Set ι
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), CompactSpace (α i)
s : Set ((a : ι) → α a)
hs : IsClosed s
this : S.domRestrict = Prod.fst ∘ ⇑(Homeomorph.piEquivPiSubtypeProd (fun x ↦ x ∈ S) α)
⊢ IsClosed (Prod.fst '' ⇑(Homeomorph.piEquivPiSubtypeProd (fun x ↦ x ∈ S) α) '' s)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case succ
x : ℝ
n : ℕ
ih : (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n
⊢ 3 *
      ((x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n -
        3 ^ n * ofDigitsTerm (cantorToTernary x).get n) =
    (x - (∑ x_1 ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get x_1 + ofDigitsTerm (cantorToTernary x).get n)) *
      3 ^ (n + 1)

Tactic:
]

Goal state after:
case succ
x : ℝ
n : ℕ
ih : (cantorSequence x).get n = (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n
⊢ 3 *
      ((x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n -
        3 ^ n * ofDigitsTerm (cantorToTernary x).get n) =
    (x - (∑ x_1 ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get x_1 + ofDigitsTerm (cantorToTernary x).get n)) *
      3 ^ (n + 1)
Module: Mathlib.Topology.IsClosedRestrict

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this✝ : IsClosed ({i}.domRestrict '' s)
this : ⇑(Homeomorph.piUnique fun t ↦ α ↑t) ∘ {i}.domRestrict = fun x ↦ x i
⊢ IsClosed ({i}.domRestrict '' s)

Tactic:
]

Goal state after:
ι : Type u_1
α : ι → Type u_2
s : Set ((i : ι) → α i)
inst✝ : (i : ι) → TopologicalSpace (α i)
i : ι
hs_compact : IsCompact s
hs_closed : IsClosed s
this✝ : IsClosed ({i}.domRestrict '' s)
this : ⇑(Homeomorph.piUnique fun t ↦ α ↑t) ∘ {i}.domRestrict = fun x ↦ x i
⊢ IsClosed ({i}.domRestrict '' s)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: 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

Tactic:
]

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 : (x - ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) * 3 ^ n ∈ cantorSet
⊢ x - 3⁻¹ ^ n ≤ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x) i

Tactic:
]

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.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
]

Goal state after:
case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (x_1 : ↑I),
    { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯ }.toFun (1, x_1) =
      (toLoop i q).toContinuousMap x_1

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ?refine_4 }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hl : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ #(logSizeBallSeq J hJ a c #J).finset ≤ #J - #J

Tactic:
]

Goal state after:
T : Type u_1
inst✝² : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝¹ : DecidableEq T
E : Type u_2
inst✝ : PseudoEMetricSpace E
ha : 1 < a
f : T → E
s : T
hs : s ∈ J
t : T
ht : t ∈ J
hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c
hJ : J.Nonempty
P : ℕ → Prop := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset
l : ℕ := Nat.findGreatest P (#J - 1)
hsV : s ∈ (logSizeBallSeq J hJ a c l).finset
htV : t ∈ (logSizeBallSeq J hJ a c l).finset
this :
  ∀ (s : T) (hs : s ∈ J) (t : T) (ht : t ∈ J) (hst : edist ⟨s, hs⟩ ⟨t, ht⟩ ≤ c),
    let P := fun l ↦ s ∈ (logSizeBallSeq J hJ a c l).finset ∧ t ∈ (logSizeBallSeq J hJ a c l).finset;
    let l := Nat.findGreatest P (#J - 1);
    s ∈ (logSizeBallSeq J hJ a c l).finset →
      t ∈ (logSizeBallSeq J hJ a c l).finset →
        s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset →
          edist (f ↑⟨s, hs⟩) (f ↑↑⟨⟨t, ht⟩, hst⟩) ≤ 2 * ⨆ p, edist (f (↑p).1) (f (↑p).2)
h : ¬s ∉ (logSizeBallSeq J hJ a c (l + 1)).finset
hl : #J ≤ l + 1
hlJ : l + 1 = #J
⊢ #(logSizeBallSeq J hJ a c #J).finset ≤ #J - #J
Module: Mathlib.Topology.Instances.CantorSet

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

Tactic:
]

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

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ ?m.15 = x

pp: x : ℝ
hx : x ∈ cantorSet
⊢ HasSum (ofDigitsTerm (cantorToTernary x).get) ?m.15

pp: x : ℝ
hx : x ∈ cantorSet
⊢ ℝ

Tactic:
]

Goal state after:
x : ℝ
hx : x ∈ cantorSet
⊢ HasSum (ofDigitsTerm (cantorToTernary x).get) x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = q ((Cube.insertAt i) (x✝, y✝))

pp: case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

pp: case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1

Tactic:
]

Goal state after:
case refine_4
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((1, x✝).1, (Cube.insertAt i) ((1, x✝).2, y✝)) = q ((Cube.insertAt i) (x✝, y✝))

case refine_3
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
x✝ : ↑I
y✝ : { j // j ≠ i } → ↑I
⊢ H ((0, x✝).1, (Cube.insertAt i) ((0, x✝).2, y✝)) = p ((Cube.insertAt i) (x✝, y✝))

case refine_5
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i : N
p q : ↑(Ω^ N X x)
H : (↑p).HomotopyRel (↑q) (Cube.boundary N)
⊢ ∀ (t x_1 : ↑I),
    x_1 ∈ {0, 1} →
      {
            toFun := fun x_2 ↦
              { toFun := fun t ↦ ⟨(homotopyTo i H) t, ⋯⟩, continuous_toFun := ⋯, map_zero_left := ⋯,
                    map_one_left := ⋯ }.toFun
                (t, x_2),
            continuous_toFun := ⋯ }
          x_1 =
        (toLoop i p).toContinuousMap x_1
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) Filter.atTop (nhds x)

pp: x : ℝ
hx : x ∈ cantorSet
⊢ Summable fun i ↦ ‖ofDigitsTerm (cantorToTernary x).get i‖

Tactic:
]

Goal state after:
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) Filter.atTop (nhds x)

x : ℝ
hx : x ∈ cantorSet
⊢ Summable fun i ↦ ‖ofDigitsTerm (cantorToTernary x).get i‖
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: x : ℝ
hx : x ∈ cantorSet
⊢ Summable fun i ↦ ‖ofDigitsTerm (cantorToTernary x).get i‖

pp: x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) Filter.atTop (nhds x)

Tactic:
· simpa only [norm_of_nonneg ofDigitsTerm_nonneg] using summable_ofDigitsTerm

Goal state after:
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun n ↦ ∑ i ∈ Finset.range n, ofDigitsTerm (cantorToTernary x).get i) Filter.atTop (nhds x)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x_1 ↦ x - 3⁻¹ ^ x_1 - x) Filter.atTop (nhds 0)

Tactic:
]

Goal state after:
case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x_1 ↦ x - 3⁻¹ ^ x_1 - x) Filter.atTop (nhds 0)
Module: Mathlib.Topology.Instances.CantorSet

Goal state before:
pp: case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x ↦ -3⁻¹ ^ x) Filter.atTop (nhds (-0))

Tactic:
]

Goal state after:
case hg
x : ℝ
hx : x ∈ cantorSet
⊢ Filter.Tendsto (fun x ↦ -3⁻¹ ^ x) Filter.atTop (nhds (-0))