mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
          x

Tactic:
·

Goal state after:
case prop'
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : HSpace X
inst✝ : HSpace Y
G : ↑I × X × Y → X × Y := ⋯
hG : Continuous G
⊢ ∀ (t : ↑I),
    ∀ x ∈ {(e, e)},
      { toFun := fun x ↦ { toFun := G, continuous_toFun := hG, map_zero_left := ⋯, map_one_left := ⋯ }.toFun (t, x),
            continuous_toFun := ⋯ }
          x =
        ({ toFun := fun p ↦ (hmul (p.1.1, p.2.1), hmul (p.1.2, p.2.2)), continuous_toFun := ⋯ }.comp
            ((ContinuousMap.id (X × Y)).prodMk (const (X × Y) (e, e))))
          x
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 2 * ↑t

pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 1

Tactic:
·

Goal state after:
case pos
t : ↑I
h✝ : ↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 2 * ↑t
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 1

Tactic:
·

Goal state after:
case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ ↑(Set.projIcc 0 1 qRight._proof_1 (2 * ↑t)) = 1
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t

pp: t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1

Tactic:
·

Goal state after:
case neg
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 1 ≤ 2 * ↑t
Module: Mathlib.Topology.Homotopy.HSpaces

Goal state before:
pp: t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1

Tactic:
·

Goal state after:
t : ↑I
h✝ : ¬↑t ≤ 1 / 2
⊢ 0 < 1
Module: Mathlib.Topology.Homotopy.LocallyContractible

Goal state before:
pp: case refine_1
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),
    (𝓝 x).HasBasis
      (fun x_1 ↦
        match x with
        | (x, y) =>
          match x_1 with
          | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
      fun x ↦
      match x with
      | (Ux, Uy) => Ux ×ˢ Uy

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) (i : Set X × Set Y),
    (match x with
      | (x, y) =>
        match i with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
      ContractibleSpace
        ↑(match i with
          | (Ux, Uy) => Ux ×ˢ Uy)

Tactic:
·

Goal state after:
case refine_1
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),
    (𝓝 x).HasBasis
      (fun x_1 ↦
        match x with
        | (x, y) =>
          match x_1 with
          | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy)
      fun x ↦
      match x with
      | (Ux, Uy) => Ux ×ˢ Uy
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) (i : Set X × Set Y),
    (match x with
      | (x, y) =>
        match i with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
      ContractibleSpace
        ↑(match i with
          | (Ux, Uy) => Ux ×ˢ Uy)

Tactic:
·

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) (i : Set X × Set Y),
    (match x with
      | (x, y) =>
        match i with
        | (Ux, Uy) => (Ux ∈ 𝓝 x ∧ ContractibleSpace ↑Ux) ∧ Uy ∈ 𝓝 y ∧ ContractibleSpace ↑Uy) →
      ContractibleSpace
        ↑(match i with
          | (Ux, Uy) => Ux ×ˢ Uy)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : logSizeRadius t V a c = 1
⊢ a ^ (logSizeRadius t V a c - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(logSizeRadius t V a c) - 1) * c}))

pp: case neg
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬logSizeRadius t V a c = 1
⊢ a ^ (logSizeRadius t V a c - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(logSizeRadius t V a c) - 1) * c}))

Tactic:
·

Goal state after:
case pos
T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : logSizeRadius t V a c = 1
⊢ a ^ (logSizeRadius t V a c - 1) ≤ ↑(#({x ∈ V | edist t x ≤ (↑(logSizeRadius t V a c) - 1) * c}))
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: T : Type u_1
inst✝ : PseudoEMetricSpace T
a c : ℝ≥0∞
V : Finset T
t : T
ha : 1 < a
ht : t ∈ V
h_one : ¬Nat.find ⋯ = 1
this : Nat.find ⋯ - 1 < Nat.find ⋯
h : 1 ≤ Nat.find ⋯ - 1 → a ^ (Nat.find ⋯ - 1) < ↑(#({x ∈ V | edist t x ≤ (↑(Nat.find ⋯) - 1) * c}))
⊢ 1 ≤ Nat.find ⋯ - 1

Tactic:
by lia

Goal state after:
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: case refine_1
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Ioi a)

pp: case refine_2
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Iio a)

Tactic:
·

Goal state after:
case refine_1
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Ioi a)
Module: Mathlib.Topology.Instances.ENNReal.ENatENNReal

Goal state before:
pp: case refine_2
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Iio a)

Tactic:
·

Goal state after:
case refine_2
a : ENNReal
⊢ IsOpen (toENNReal ⁻¹' Set.Iio a)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

pp: case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : ¬(logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J

Tactic:
·

Goal state after:
case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : (logSizeBallSeq J hJ a c i).point ∈ J
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).point ∈ J
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case hab
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset

pp: case hba
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ ¬(logSizeBallSeq J hJ a c i).finset ⊆ (logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
·

Goal state after:
case hab
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c (i + 1)).finset ⊆ (logSizeBallSeq J hJ a c i).finset
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case hba.refine_1
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∈ ↑(logSizeBallSeq J hJ a c i).finset

pp: case hba.refine_2
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∉ ↑(logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
·

Goal state after:
case hba.refine_1
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∈ ↑(logSizeBallSeq J hJ a c i).finset
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case hba.refine_1
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∈ ↑(logSizeBallSeq J hJ a c i).finset

Tactic:
exact point_mem_finset_logSizeBallSeq hJ i h

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

Goal state before:
pp: case hba.refine_2
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∉ ↑(logSizeBallSeq J hJ a c (i + 1)).finset

Tactic:
·

Goal state after:
case hba.refine_2
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ (logSizeBallSeq J hJ a c i).point ∉ ↑(logSizeBallSeq J hJ a c (i + 1)).finset
Module: Mathlib.Topology.Instances.RatLemmas

Goal state before:
pp: case inr
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this : ∀ (s : Set ℚ), IsPreconnected s → ∀ x ∈ s, ∀ y ∈ s, x ≠ y → x < y → False
hlt : ¬x < y
⊢ False

pp: s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
hlt : x < y
⊢ False

Tactic:
·

Goal state after:
case inr
s : Set ℚ
hs : IsPreconnected s
x : ℚ
hx : x ∈ s
y : ℚ
hy : y ∈ s
H : x ≠ y
this : ∀ (s : Set ℚ), IsPreconnected s → ∀ x ∈ s, ∀ y ∈ s, x ≠ y → x < y → False
hlt : ¬x < y
⊢ False
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)

pp: case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : ¬(logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)

Tactic:
·

Goal state after:
case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i : ℕ
ih : #(logSizeBallSeq J hJ a c i).finset ≤ #J - i
h : (logSizeBallSeq J hJ a c i).finset.Nonempty
⊢ #(logSizeBallSeq J hJ a c (i + 1)).finset ≤ #J - (i + 1)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
this :
  ∀ {i j : ℕ},
    i ≠ j → i < j → Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
h : j ≤ i
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

pp: T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)

Tactic:
·

Goal state after:
case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
this :
  ∀ {i j : ℕ},
    i ≠ j → i < j → Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
h : j ≤ i
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ((logSizeBallSeq J hJ a c j).smallBall c)
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case h
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ (logSizeBallSeq J hJ a c j).smallBall c ⊆ ?u

pp: case d
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ Disjoint ((logSizeBallSeq J hJ a c i).smallBall c) ?u

pp: case u
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ Finset T

Tactic:
·

Goal state after:
case h
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i j : ℕ
hij : i ≠ j
h : i < j
⊢ (logSizeBallSeq J hJ a c j).smallBall c ⊆ ?u
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

pp: case inr
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

Tactic:
·

Goal state after:
case inl
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
H : t₀ = 0 ∨ t₀ = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inr
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N

Tactic:
·

Goal state after:
case inr
N : Type u_1
inst✝ : DecidableEq N
i : N
t₀ : ↑I
t : { j // j ≠ i } → ↑I
j : { j // j ≠ i }
H : t j = 0 ∨ t j = 1
⊢ (insertAt i) (t₀, t) ∈ boundary N
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ pairSetSeq J a c i ⊆ J ×ˢ J

pp: case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : ¬J.Nonempty
⊢ pairSetSeq J a c i ⊆ J ×ˢ J

Tactic:
·

Goal state after:
case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ pairSetSeq J a c i ⊆ J ×ˢ J
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos.hs
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ {(logSizeBallSeq J ⋯ a c i).point} ⊆ J

pp: case pos.ht
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ (logSizeBallSeq J ⋯ a c i).ball c ⊆ J

Tactic:
·

Goal state after:
case pos.hs
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
i : ℕ
hi : i ∈ Finset.range #J
hJ : J.Nonempty
⊢ {(logSizeBallSeq J ⋯ a c i).point} ⊆ J
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ ↑(#(pairSetSeq J a c (i + 1))) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius

pp: case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
h : (logSizeBallSeq J hJ a c (i + 1)).finset = ∅
⊢ ↑(#(pairSetSeq J a c (i + 1))) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius

Tactic:
·

Goal state after:
case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
ha : 1 < a
i : ℕ
ih :
  ↑(#(pairSetSeq J a c i)) ≤
    (if (logSizeBallSeq J hJ a c i).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c i).radius
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ ↑(#(pairSetSeq J a c (i + 1))) ≤
    (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) * a ^ (logSizeBallSeq J hJ a c (i + 1)).radius
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ : ℕ
ha : 1 < a
i : ℕ
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c))

pp: case neg
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ : ℕ
ha : 1 < a
i : ℕ
h : (logSizeBallSeq J hJ a c (i + 1)).finset = ∅
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c))

Tactic:
·

Goal state after:
case pos
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
hJ : J.Nonempty
i✝ : ℕ
ha : 1 < a
i : ℕ
h : (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty
⊢ (if (logSizeBallSeq J hJ a c (i + 1)).finset.Nonempty then 1 else 0) *
      a ^ ((logSizeBallSeq J hJ a c (i + 1)).radius - 1) ≤
    ↑(#((logSizeBallSeq J hJ a c (i + 1)).smallBall c))
Module: Mathlib.Topology.EMetricSpace.PairReduction

Goal state before:
pp: case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a → J.Nonempty → ↑(#(pairSet J a c)) ≤ a * ↑(#J)
hJ : ¬J.Nonempty
⊢ ↑(#(pairSet J a c)) ≤ a * ↑(#J)

pp: T✝ : Type u_1
inst✝³ : PseudoEMetricSpace T✝
a✝ c✝ : ℝ≥0∞
J✝ : Finset T✝
inst✝² : DecidableEq T✝
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
hJ : J.Nonempty
⊢ ↑(#(pairSet J a c)) ≤ a * ↑(#J)

Tactic:
·

Goal state after:
case inr
T : Type u_1
inst✝¹ : PseudoEMetricSpace T
a c : ℝ≥0∞
J : Finset T
inst✝ : DecidableEq T
ha : 1 < a
this :
  ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ℝ≥0∞} {J : Finset T} [inst_1 : DecidableEq T],
    1 < a → J.Nonempty → ↑(#(pairSet J a c)) ≤ a * ↑(#J)
hJ : ¬J.Nonempty
⊢ ↑(#(pairSet J a c)) ≤ a * ↑(#J)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mp
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∈ Cube.boundary (M ⊕ N) → y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

pp: case mpr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N → y ∈ Cube.boundary (M ⊕ N)

Tactic:
·

Goal state after:
case mp
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∈ Cube.boundary (M ⊕ N) → y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mp.inl
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
i : M
hi : y (Sum.inl i) = 0 ∨ y (Sum.inl i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

pp: case mp.inr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
i : N
hi : y (Sum.inr i) = 0 ∨ y (Sum.inr i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
·

Goal state after:
case mp.inl
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
i : M
hi : y (Sum.inl i) = 0 ∨ y (Sum.inl i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mp.inr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
i : N
hi : y (Sum.inr i) = 0 ∨ y (Sum.inr i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N

Tactic:
·

Goal state after:
case mp.inr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
i : N
hi : y (Sum.inr i) = 0 ∨ y (Sum.inr i) = 1
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mpr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N → y ∈ Cube.boundary (M ⊕ N)

Tactic:
·

Goal state after:
case mpr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
⊢ y ∘ Sum.inl ∈ Cube.boundary M ∨ y ∘ Sum.inr ∈ Cube.boundary N → y ∈ Cube.boundary (M ⊕ N)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mpr.inl
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
m : M
hm : (y ∘ Sum.inl) m = 0 ∨ (y ∘ Sum.inl) m = 1
⊢ y ∈ Cube.boundary (M ⊕ N)

pp: case mpr.inr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
n : N
hn : (y ∘ Sum.inr) n = 0 ∨ (y ∘ Sum.inr) n = 1
⊢ y ∈ Cube.boundary (M ⊕ N)

Tactic:
·

Goal state after:
case mpr.inl
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
m : M
hm : (y ∘ Sum.inl) m = 0 ∨ (y ∘ Sum.inl) m = 1
⊢ y ∈ Cube.boundary (M ⊕ N)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case mpr.inr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
n : N
hn : (y ∘ Sum.inr) n = 0 ∨ (y ∘ Sum.inr) n = 1
⊢ y ∈ Cube.boundary (M ⊕ N)

Tactic:
·

Goal state after:
case mpr.inr
N : Type u_1
M : Type u_3
y : M ⊕ N → ↑I
n : N
hn : (y ∘ Sum.inr) n = 0 ∨ (y ∘ Sum.inr) n = 1
⊢ y ∈ Cube.boundary (M ⊕ N)
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inl
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hM : y ∘ Sum.inl ∈ Cube.boundary M
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

pp: case inr
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hN : y ∘ Sum.inr ∈ Cube.boundary N
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

Tactic:
·

Goal state after:
case inl
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hM : y ∘ Sum.inl ∈ Cube.boundary M
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x
Module: Mathlib.Topology.Homotopy.HomotopyGroup

Goal state before:
pp: case inr
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hN : y ∘ Sum.inr ∈ Cube.boundary N
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x

Tactic:
·

Goal state after:
case inr
N : Type u_1
X : Type u_2
inst✝ : TopologicalSpace X
M : Type u_3
x : X
p : ↑(Ω^ M (↑(Ω^ N X x)) const)
y : M ⊕ N → ↑I
hy : y ∈ Cube.boundary (M ⊕ N)
hN : y ∘ Sum.inr ∈ Cube.boundary N
⊢ (p (y ∘ Sum.inl)) (y ∘ Sum.inr) = x