awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ≥0
⊢ (∀ (i : β) ⦃x : (x : β) → X x⦄,
      x ∈ s →
        ∀ ⦃x_1 : (x : β) → X x⦄,
          x_1 ∈ s → (↑(nndist (Function.eval (β := X) i x) (Function.eval (β := X) i x_1)) : ℝ) ≤ (↑C : ℝ)) ↔
    ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ (↑C : ℝ)

Tactic:
⟨fun H x hx y hy ↦ NNReal.coe_le_coe.2 <| Finset.sup_le fun b _ ↦ H b hx hy,
    fun H b x hx y hy ↦ NNReal.coe_le_coe.2 ?_⟩

Premises used: Iff.mpr, Finset.sup_le, Iff.intro, NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ≥0
refine :
  ∀ (H : ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ (↑C : ℝ)) (b : β) (x : (x : β) → X x)
    (hx : x ∈ s) (y : (x : β) → X x) (hy : y ∈ s), nndist (Function.eval (β := X) b x) (Function.eval (β := X) b y) ≤ C
⊢ (∀ (i : β) ⦃x : (x : β) → X x⦄,
      x ∈ s →
        ∀ ⦃x_1 : (x : β) → X x⦄,
          x_1 ∈ s → (↑(nndist (Function.eval (β := X) i x) (Function.eval (β := X) i x_1)) : ℝ) ≤ (↑C : ℝ)) ↔
    ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ (↑C : ℝ)

Tactic:
refine ⟨fun H x hx y hy ↦ NNReal.coe_le_coe.2 <| Finset.sup_le fun b _ ↦ H b hx hy,
    fun H b x hx y hy ↦ NNReal.coe_le_coe.2 ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
X : β → Type u_3
inst_1 : Fintype β
inst_2 : (b : β) → PseudoMetricSpace (X b)
i : PseudoMetricSpace ((b : β) → X b) :=
  PseudoEMetricSpace.toPseudoMetricSpaceOfDist
    (fun (f g : (b : β) → X b) ↦ (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)) ⋯ ⋯
s : Set ((b : β) → X b)
C : ℝ≥0
H : ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ (↑C : ℝ)
b : β
x : (x : β) → X x
hx : x ∈ s
y : (x : β) → X x
hy : y ∈ s
⊢ nndist (Function.eval (β := X) b x) (Function.eval (β := X) b y) ≤ C

Tactic:
simpa only using Finset.sup_le_iff.1 (NNReal.coe_le_coe.1 <| H hx hy) b (Finset.mem_univ b)

Premises used: Finset.mem_univ, Iff.mp, Finset.sup_le_iff, NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
⊢ nndist f g = sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)

Tactic:
rfl

Premises used: Multiset.foldr, Finset.fold, NNReal, Finset.sup, NNReal.toReal, rfl, Multiset.fold
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
⊢ dist f g = (↑(sup Finset.univ fun (b : β) ↦ nndist (f b) (g b)) : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
⊢ nndist f g ≤ r ↔ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
simp [nndist_pi_def]

Premises used: nndist_pi_def
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
⊢ nndist f g < r ↔ ∀ (b : β), nndist (f b) (g b) < r

Tactic:
simp [nndist_pi_def, Finset.sup_lt_iff hr]

Premises used: Finset.sup_lt_iff, nndist_pi_def
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
rw :
  ((∃ (x : β), ¬nndist (f x) (g x) < r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r
⊢ nndist f g = r ↔ (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
rw [eq_iff_le_not_lt, nndist_pi_lt_iff hr, nndist_pi_le_iff, not_forall, and_comm]

Premises used: nndist_pi_le_iff, and_comm, eq_iff_le_not_lt, nndist_pi_lt_iff, Classical.not_forall
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
simp_rw :
  (∀ (b : β), nndist (f b) (g b) ≤ r) →
    ((∃ (x : β), r ≤ nndist (f x) (g x)) ↔ ∃ (i : β), nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i))
⊢ ((∃ (x : β), ¬nndist (f x) (g x) < r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r

Tactic:
simp_rw [not_lt, and_congr_left_iff, le_antisymm_iff]

Premises used: not_lt, le_antisymm_iff, and_congr_left_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
⊢ (∃ (x : β), r ≤ nndist (f x) (g x)) ↔ ∃ (i : β), nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i)

Tactic:
exists_congr fun b => ?_

Premises used: exists_congr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
refine : ∀ (b : β), r ≤ nndist (f b) (g b) ↔ nndist (f b) (g b) ≤ r ∧ r ≤ nndist (f b) (g b)
⊢ (∃ (x : β), r ≤ nndist (f x) (g x)) ↔ ∃ (i : β), nndist (f i) (g i) ≤ r ∧ r ≤ nndist (f i) (g i)

Tactic:
refine exists_congr fun b => ?_

Premises used: exists_congr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < r
h : ∀ (b : β), nndist (f b) (g b) ≤ r
b : β
⊢ r ≤ nndist (f b) (g b) ↔ nndist (f b) (g b) ≤ r ∧ r ≤ nndist (f b) (g b)

Tactic:
apply (and_iff_right <| h _).symm

Premises used: and_iff_right, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 < r
⊢ 0 ≤ r

Tactic:
hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 < r
lift : ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)), dist f g < (↑r : ℝ) ↔ ∀ (b : β), dist (f b) (g b) < (↑r : ℝ)
⊢ dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r

Tactic:
lift r to ℝ≥0 using hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < (↑r : ℝ)
⊢ dist f g < (↑r : ℝ) ↔ ∀ (b : β), dist (f b) (g b) < (↑r : ℝ)

Tactic:
nndist_pi_lt_iff hr

Premises used: nndist_pi_lt_iff, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < (↑r : ℝ)
⊢ dist f g < (↑r : ℝ) ↔ ∀ (b : β), dist (f b) (g b) < (↑r : ℝ)

Tactic:
exact nndist_pi_lt_iff hr

Premises used: nndist_pi_lt_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ 0 ≤ r

Tactic:
hr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 ≤ r
lift : ∀ (r : ℝ≥0), dist f g ≤ (↑r : ℝ) ↔ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
lift r to ℝ≥0 using hr
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
⊢ dist f g ≤ (↑r : ℝ) ↔ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)

Tactic:
nndist_pi_le_iff

Premises used: nndist_pi_le_iff, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
⊢ dist f g ≤ (↑r : ℝ) ↔ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)

Tactic:
exact nndist_pi_le_iff

Premises used: nndist_pi_le_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ
hr : 0 < r
lift :
  ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)),
    dist f g = (↑r : ℝ) ↔ (∃ (i : β), dist (f i) (g i) = (↑r : ℝ)) ∧ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)
⊢ dist f g = r ↔ (∃ (i : β), dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
lift r to ℝ≥0 using hr.le

Premises used: LT.lt.le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
r : ℝ≥0
hr : 0 < (↑r : ℝ)
simp_rw :
  (↑(nndist f g) : ℝ) = (↑r : ℝ) ↔
    (∃ (i : β), (↑(nndist (f i) (g i)) : ℝ) = (↑r : ℝ)) ∧ ∀ (b : β), (↑(nndist (f b) (g b)) : ℝ) ≤ (↑r : ℝ)
simp_rw₁ : nndist f g = r ↔ (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), (↑(nndist (f b) (g b)) : ℝ) ≤ (↑r : ℝ)
simp_rw₂ :
  ((∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r) ↔
    (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), (↑(nndist (f b) (g b)) : ℝ) ≤ (↑r : ℝ)
⊢ dist f g = (↑r : ℝ) ↔ (∃ (i : β), dist (f i) (g i) = (↑r : ℝ)) ∧ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)

Tactic:
simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]

Premises used: coe_nndist, NNReal.coe_le_coe, NNReal.coe_inj, nndist_pi_eq_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
inst_2 : Nonempty β
f g : (b : β) → X b
r : ℝ
pos : ∀ (hr : 0 ≤ r), dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
neg : ∀ (hr : ¬0 ≤ r), dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
by_cases hr : 0 ≤ r
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
inst_2 : Nonempty β
f g : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
dist_pi_le_iff hr

Premises used: dist_pi_le_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
inst_2 : Nonempty β
f g : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
exact dist_pi_le_iff hr

Premises used: dist_pi_le_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
inst_2 : Nonempty β
f g : (b : β) → X b
r : ℝ
hr : ¬0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
iff_of_false (fun h => hr <| dist_nonneg.trans h) fun h =>
      hr <| dist_nonneg.trans <| h <| Classical.arbitrary _

Premises used: dist_nonneg, iff_of_false, Classical.arbitrary, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
inst_2 : Nonempty β
f g : (b : β) → X b
r : ℝ
hr : ¬0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
exact iff_of_false (fun h => hr <| dist_nonneg.trans h) fun h =>
      hr <| dist_nonneg.trans <| h <| Classical.arbitrary _

Premises used: dist_nonneg, iff_of_false, LE.le.trans
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : Fintype β
a b : α
⊢ (dist (α := β → α) (fun (x : β) ↦ a) fun (x : β) ↦ b) ≤ dist a b

Tactic:
(dist_pi_le_iff dist_nonneg).2 fun _ => le_rfl

Premises used: Iff.mpr, le_rfl, dist_nonneg, dist_pi_le_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : Fintype β
a b : α
⊢ (nndist (α := β → α) (fun (x : β) ↦ a) fun (x : β) ↦ b) ≤ nndist a b

Tactic:
nndist_pi_le_iff.2 fun _ => le_rfl

Premises used: Iff.mpr, nndist_pi_le_iff, le_rfl
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : Fintype β
inst_2 : Nonempty β
a b : α
⊢ (dist (α := β → α) (fun (x : β) ↦ a) fun (x : β) ↦ b) = dist a b

Tactic:
simpa only [dist_edist] using congr_arg ENNReal.toReal (edist_pi_const a b)

Premises used: congr_arg, ENNReal.toReal, edist_pi_const, dist_edist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : Fintype β
inst_2 : Nonempty β
a b : α
⊢ (nndist (α := β → α) (fun (x : β) ↦ a) fun (x : β) ↦ b) = nndist a b

Tactic:
NNReal.eq <| dist_pi_const a b

Premises used: NNReal.eq, dist_pi_const
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
rw : edist (f b) (g b) ≤ edist f g
⊢ nndist (f b) (g b) ≤ nndist f g

Tactic:
rw [← ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]

Premises used: ENNReal.coe_le_coe, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ edist (f b) (g b) ≤ edist f g

Tactic:
edist_le_pi_edist f g b

Premises used: edist_le_pi_edist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ edist (f b) (g b) ≤ edist f g

Tactic:
exact edist_le_pi_edist f g b

Premises used: edist_le_pi_edist
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ dist (f b) (g b) ≤ dist f g

Tactic:
simp only [dist_nndist, NNReal.coe_le_coe, nndist_le_pi_nndist f g b]

Premises used: nndist_le_pi_nndist, dist_nndist, NNReal.coe_le_coe
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 < r
h :
  ∀ (p : (b : β) → X b),
    p ∈ ball x r ↔ Membership.mem (γ := Set ((b : β) → X b)) (Set.pi (α := X) Set.univ fun (b : β) ↦ ball (x b) r) p
⊢ ball x r = Set.pi (α := X) Set.univ fun (b : β) ↦ ball (x b) r

Tactic:
ext p
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 < r
p : (b : β) → X b
⊢ p ∈ ball x r ↔ Membership.mem (γ := Set ((b : β) → X b)) (Set.pi (α := X) Set.univ fun (b : β) ↦ ball (x b) r) p

Tactic:
simp [dist_pi_lt_iff hr]

Premises used: dist_pi_lt_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
inst_2 : Nonempty β
x : (b : β) → X b
r : ℝ
hr : r ≤ 0
⊢ ball x r = Set.pi (α := X) Set.univ fun (b : β) ↦ ball (x b) r

Tactic:
simp [ball_eq_empty.2 hr]

Premises used: Iff.mpr, Metric.ball_eq_empty
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
h :
  ∀ (p : (b : β) → X b),
    p ∈ closedBall x r ↔
      Membership.mem (γ := Set ((b : β) → X b)) (Set.pi (α := X) Set.univ fun (b : β) ↦ closedBall (x b) r) p
⊢ closedBall x r = Set.pi (α := X) Set.univ fun (b : β) ↦ closedBall (x b) r

Tactic:
ext p
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
p : (b : β) → X b
⊢ p ∈ closedBall x r ↔
    Membership.mem (γ := Set ((b : β) → X b)) (Set.pi (α := X) Set.univ fun (b : β) ↦ closedBall (x b) r) p

Tactic:
simp [dist_pi_le_iff hr]

Premises used: dist_pi_le_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
inst_2 : Nonempty β
x : (b : β) → X b
r : ℝ
hr : r < 0
⊢ closedBall x r = Set.pi (α := X) Set.univ fun (b : β) ↦ closedBall (x b) r

Tactic:
simp [closedBall_eq_empty.2 hr]

Premises used: Iff.mpr, Metric.closedBall_eq_empty
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
inl : ∀ (hr : r < 0), sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r
inr :
  ∀ (h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β),
    sphere x 0 = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0) ∩ closedBall x 0
inr₁ : ∀ (hr : 0 < r), sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r
⊢ sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
obtain hr | rfl | hr := lt_trichotomy r 0

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : r < 0
⊢ sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
simp [hr]
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β
inr : sphere x 0 ⊆ ⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0
⊢ sphere x 0 = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0) ∩ closedBall x 0

Tactic:
rw [closedBall_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right]

Premises used: le_rfl, Set.inter_eq_right, eq_comm, Metric.closedBall_eq_sphere_of_nonpos
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β
this : Nonempty β := ⋯
inr : ∀ (inhabited_h : Inhabited β), sphere x 0 ⊆ ⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0
⊢ sphere x 0 ⊆ ⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0

Tactic:
inhabit β
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β
this : Nonempty β := ⋯
inhabited_h : Inhabited β
⊢ sphere x 0 ⊆ ⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0

Tactic:
subset_iUnion_of_subset default ?_

Premises used: Inhabited.default, Set.subset_iUnion_of_subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β
this : Nonempty β := ⋯
inhabited_h : Inhabited β
inr : sphere x 0 ⊆ Set.preimage (β := X default) (Function.eval (β := X) default) (sphere (x default) 0)
⊢ sphere x 0 ⊆ ⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0

Tactic:
refine subset_iUnion_of_subset default ?_

Premises used: Inhabited.default, Set.subset_iUnion_of_subset
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x_1 : (b : β) → X b
h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β
this : Nonempty β := ⋯
inhabited_h : Inhabited β
x : (x : β) → X x
hx : x ∈ sphere x_1 0
⊢ dist x x_1 ≤ 0

Tactic:
replace hx := hx.le
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x_1 : (b : β) → X b
h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β
this : Nonempty β := ⋯
inhabited_h : Inhabited β
x : (x : β) → X x
hx : dist x x_1 ≤ 0
⊢ ∀ (b : β), dist (x b) (x_1 b) ≤ 0

Tactic:
rw [dist_pi_le_iff le_rfl] at hx

Premises used: le_rfl, dist_pi_le_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x_1 : (b : β) → X b
h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β
this : Nonempty β := ⋯
inhabited_h : Inhabited β
x : (x : β) → X x
hx : ∀ (b : β), dist (x b) (x_1 b) ≤ 0
⊢ x ∈ Set.preimage (β := X default) (Function.eval (β := X) default) (sphere (x_1 default) 0)

Tactic:
le_antisymm (hx default) dist_nonneg

Premises used: Inhabited.default, Set.Mem, setOf, dist_nonneg, le_antisymm, Set.preimage, Metric.sphere
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x_1 : (b : β) → X b
h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β
this : Nonempty β := ⋯
inhabited_h : Inhabited β
x : (x : β) → X x
hx : ∀ (b : β), dist (x b) (x_1 b) ≤ 0
⊢ x ∈ Set.preimage (β := X default) (Function.eval (β := X) default) (sphere (x_1 default) 0)

Tactic:
exact le_antisymm (hx default) dist_nonneg

Premises used: Inhabited.default, dist_nonneg, le_antisymm
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
inr :
  ∀ (x_1 : (b : β) → X b),
    x_1 ∈ sphere x r ↔ x_1 ∈ (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r
⊢ sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
h : 0 < r ∨ Nonempty β
hr : 0 < r
x_1 : (b : β) → X b
⊢ x_1 ∈ sphere x r ↔ x_1 ∈ (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r

Tactic:
simp [dist_pi_eq_iff hr, dist_pi_le_iff hr.le]

Premises used: LT.lt.le, dist_pi_le_iff, dist_pi_eq_iff
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
n : ℕ
α : Fin (n + 1) → Type u_4
inst : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (i.succAbove j)
c : ℝ≥0
⊢ nndist (i.insertNth (α := α) x f) (i.insertNth (α := α) y g) ≤ c ↔ max (nndist x y) (nndist f g) ≤ c

Tactic:
simp [nndist_pi_le_iff, i.forall_iff_succAbove]

Premises used: nndist_pi_le_iff, Fin.forall_iff_succAbove
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
n : ℕ
α : Fin (n + 1) → Type u_4
inst : (i : Fin (n + 1)) → PseudoMetricSpace (α i)
i : Fin (n + 1)
x y : α i
f g : (j : Fin n) → α (i.succAbove j)
⊢ dist (i.insertNth (α := α) x f) (i.insertNth (α := α) y g) = max (dist x y) (dist f g)

Tactic:
simp only [dist_nndist, Fin.nndist_insertNth_insertNth, NNReal.coe_max]

Premises used: Fin.nndist_insertNth_insertNth, dist_nndist, NNReal.coe_max
-- Module: Mathlib.Topology.MetricSpace.Pseudo.Pi
Goal:
β : Type u_2
inst : Fintype β
Y : Type u_4
inst_1 : PseudoMetricSpace Y
inst_2 : Zero Y
inst_3 : DecidableEq β
i j : β
a b : Y
h : i ≠ j
⊢ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b) =
    max (nndist a 0) (nndist b 0)

Tactic:
le_antisymm (nndist_pi_le_iff.2 fun k ↦ ?_) (max_le ?_ ?_)

Premises used: Iff.mpr, nndist_pi_le_iff, le_antisymm, max_le