awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Defs (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set α
simp_rw : Dense s ↔ ∀ r > 0, ∀ (x : α), Membership.mem (γ := Set α) (⋃ c ∈ s, ball c r) x
simp_rw₁ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ (i : α) (_ : i ∈ s), x ∈ ball i r
simp_rw₂ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, x ∈ ball i r
simp_rw₃ : Dense s ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
simp_rw₄ :
  (∀ (x : α), x ∈ closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s) ↔
    ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
⊢ Dense s ↔ ∀ r > 0, Eq.{u + 1} (α := Set α) (⋃ c ∈ s, ball c r) univ
have simp_rw₅ : (∀ (x : α), ∀ ε > 0, ∃ b ∈ s, dist x b < ε) ↔ ∀ r > 0, ∀ (x : α), ∃ i ∈ s, dist x i < r
Tactic: simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
    forall_comm (α := α)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
have obtain : ∀ (ε : ℝ) (εpos : 0 < ε) (hε : closedBall x ε ⊆ u), ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
Tactic: obtain ⟨ε, εpos, hε⟩ : ∃ ε, 0 < ε ∧ closedBall x ε ⊆ u := nhds_basis_closedBall.mem_iff.1 hu
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (hypothesis)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
have this : Membership.mem (γ := Filter ℝ) (𝓝 0) (Iic ε)
Tactic: have : Iic ε ∈ 𝓝 (0 : ℝ) := Iic_mem_nhds εpos
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
this : Membership.mem (γ := Filter ℝ) (𝓝 0) (Iic ε)
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
have h : ∀ (a : ℝ),
  Membership.mem (γ := Set ℝ)
    {x_1 : ℝ | x_1 ∈ Iic ε → Membership.mem (γ := Set ℝ) {x_2 : ℝ | (fun (r : ℝ) ↦ closedBall x r ⊆ u) x_2} x_1} a
Tactic: filter_upwards [this] with _ hr using Subset.trans (closedBall_subset_closedBall hr) hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
u : Set α
hu : u ∈ 𝓝 x
ε : ℝ
εpos : 0 < ε
hε : closedBall x ε ⊆ u
this : Membership.mem (γ := Filter ℝ) (𝓝 0) (Iic ε)
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x_1 : ℝ | x_1 ∈ Iic ε → Membership.mem (γ := Set ℝ) {x_2 : ℝ | (fun (r : ℝ) ↦ closedBall x r ⊆ u) x_2} x_1} a
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, closedBall x r ⊆ u
have h₁ : ∀ a ∈ Iic ε, closedBall x a ⊆ u
Tactic: filter_upwards [this] with _ hr using Subset.trans (closedBall_subset_closedBall hr) hε
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)
have rcases : ∀ (s : Set α) (s_compact : IsCompact s) (hs : s ∈ 𝓝 x), ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)
Tactic: rcases exists_compact_mem_nhds x with ⟨s, s_compact, hs⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
s : Set α
s_compact : IsCompact s
hs : s ∈ 𝓝 x
⊢ ∀ᶠ (r : ℝ) in 𝓝 0, IsCompact (closedBall x r)
have h : ∀ (r : ℝ) (hr : closedBall x r ⊆ s), IsCompact (closedBall x r)
Tactic: filter_upwards [eventually_closedBall_subset hs] with r hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (hypothesis)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
inst_1 : WeaklyLocallyCompactSpace α
x : α
⊢ ∃ (r : ℝ), 0 < r ∧ IsCompact (closedBall x r)
have this : ∀ᶠ (r : ℝ) in 𝓝[>] 0, IsCompact (closedBall x r)
Tactic: have : ∀ᶠ r in 𝓝[>] 0, IsCompact (closedBall x r) :=
    eventually_nhdsWithin_of_eventually_nhds (eventually_isCompact_closedBall x)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋂ (r' : ℝ), ⋂ (_ : r' > r), closedBall x r' = closedBall x r
have h : ∀ (x_1 : α), Membership.mem (γ := Set α) (⋂ (r' : ℝ), ⋂ (_ : r' > r), closedBall x r') x_1 ↔ x_1 ∈ closedBall x r
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋂ (r' : ℝ), ⋂ (_ : r' > r), ball x r' = closedBall x r
have h : ∀ (x_1 : α), Membership.mem (γ := Set α) (⋂ (r' : ℝ), ⋂ (_ : r' > r), ball x r') x_1 ↔ x_1 ∈ closedBall x r
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r' = ball x r
have h : ∀ (x_1 : α), Membership.mem (γ := Set α) (⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r') x_1 ↔ x_1 ∈ ball x r
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
x_1 : α
⊢ Membership.mem (γ := Set α) (⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r') x_1 ↔ x_1 ∈ ball x r
have h : x_1 ∉ ⋃ (r' : ℝ), ⋃ (_ : r' < r), ball x r' ↔ x_1 ∉ ball x r
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
⊢ ⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r' = ball x r
have h : ∀ (x_1 : α), Membership.mem (γ := Set α) (⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r') x_1 ↔ x_1 ∈ ball x r
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (goal)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
x : α
r : ℝ
x_1 : α
⊢ Membership.mem (γ := Set α) (⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r') x_1 ↔ x_1 ∈ ball x r
have h : x_1 ∉ ⋃ (r' : ℝ), ⋃ (_ : r' < r), closedBall x r' ↔ x_1 ∉ ball x r
Tactic: rw [← not_iff_not]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Lemmas (hypothesis)
Goal:
α : Type u_2
inst : PseudoMetricSpace α
s : Set α
c : Set (Set α)
hs : IsCompact s
hc₁ : ∀ t ∈ c, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
hc₂ : s ⊆ ⋃₀ c
⊢ ∃ δ > 0, ∀ x ∈ s, ∃ t ∈ c, ball x δ ⊆ t
have hc₃ : s ⊆ ⋃ (i : (↑c : Type u_2)), (↑i : Set α)
Tactic: rw [sUnion_eq_iUnion] at hc₂
Cleared hypotheses: hc₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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)) : ℝ)) ⋯ ⋯
⊢ PseudoMetricSpace ((b : β) → X b)
have refine : ∀ (s : Set ((b : β) → X b)), Bornology.IsBounded s ↔ Bornology.IsBounded s
Tactic: refine i.replaceBornology fun s => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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)
⊢ Bornology.IsBounded s ↔ Bornology.IsBounded s
have simp : (∀ᶠ (x : ℝ) in atTop,
    ∀ (i : β) ⦃x_1 : (x : β) → X x⦄,
      x_1 ∈ s →
        ∀ ⦃x_2 : (x : β) → X x⦄,
          x_2 ∈ s → (↑(nndist (Function.eval (β := X) i x_1) (Function.eval (β := X) i x_2)) : ℝ) ≤ x) ↔
  ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ C
Tactic: simp only [isBounded_iff_eventually, ← forall_isBounded_image_eval_iff,
    forall_mem_image, ← Filter.eventually_all, @dist_nndist (X _)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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)
⊢ (∀ᶠ (x : ℝ) in atTop,
      ∀ (i : β) ⦃x_1 : (x : β) → X x⦄,
        x_1 ∈ s →
          ∀ ⦃x_2 : (x : β) → X x⦄,
            x_2 ∈ s → (↑(nndist (Function.eval (β := X) i x_1) (Function.eval (β := X) i x_2)) : ℝ) ≤ x) ↔
    ∀ᶠ (C : ℝ) in atTop, ∀ ⦃x : (b : β) → X b⦄, x ∈ s → ∀ ⦃y : (b : β) → X b⦄, y ∈ s → dist x y ≤ C
have refine : ∀ (C : ℝ) (hC : 0 ≤ 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 eventually_congr ((eventually_ge_atTop 0).mono fun C hC ↦ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 : ℝ
hC : 0 ≤ 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
have lift : ∀ (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: lift C to ℝ≥0 using hC
Cleared hypotheses: C, hC
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 : ℝ)
have 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
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 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 ↔ (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), nndist (f b) (g b) ≤ r
have 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
Tactic: rw [eq_iff_le_not_lt, nndist_pi_lt_iff hr, nndist_pi_le_iff, not_forall, and_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
⊢ ((∃ (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
have 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))
Tactic: simp_rw [not_lt, and_congr_left_iff, le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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)
have refine : ∀ (b : β), r ≤ nndist (f b) (g b) ↔ nndist (f b) (g b) ≤ r ∧ r ≤ nndist (f b) (g b)
Tactic: refine exists_congr fun b => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
⊢ dist f g < r ↔ ∀ (b : β), dist (f b) (g b) < r
have lift : ∀ (r : ℝ≥0) (hr : 0 < (↑r : ℝ)), dist f g < (↑r : ℝ) ↔ ∀ (b : β), dist (f b) (g b) < (↑r : ℝ)
Tactic: lift r to ℝ≥0 using hr.le
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
have lift : ∀ (r : ℝ≥0), dist f g ≤ (↑r : ℝ) ↔ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
⊢ dist f g = r ↔ (∃ (i : β), dist (f i) (g i) = r) ∧ ∀ (b : β), dist (f b) (g b) ≤ r
have lift : ∀ (r : ℝ≥0) (hr : 0 < (↑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
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 : ℝ) ↔ (∃ (i : β), dist (f i) (g i) = (↑r : ℝ)) ∧ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)
have simp_rw : (↑(nndist f g) : ℝ) = (↑r : ℝ) ↔
  (∃ (i : β), (↑(nndist (f i) (g i)) : ℝ) = (↑r : ℝ)) ∧ ∀ (b : β), (↑(nndist (f b) (g b)) : ℝ) ≤ (↑r : ℝ)
Tactic: simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 : ℝ)
⊢ dist f g = (↑r : ℝ) ↔ (∃ (i : β), dist (f i) (g i) = (↑r : ℝ)) ∧ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)
have simp_rw₁ : nndist f g = r ↔ (∃ (i : β), nndist (f i) (g i) = r) ∧ ∀ (b : β), (↑(nndist (f b) (g b)) : ℝ) ≤ (↑r : ℝ)
Tactic: simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 : ℝ)
⊢ dist f g = (↑r : ℝ) ↔ (∃ (i : β), dist (f i) (g i) = (↑r : ℝ)) ∧ ∀ (b : β), dist (f b) (g b) ≤ (↑r : ℝ)
have 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 : ℝ)
Tactic: simp_rw [← coe_nndist, NNReal.coe_inj, nndist_pi_eq_iff hr, NNReal.coe_le_coe]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 : ℝ
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
have pos : ∀ (hr : 0 ≤ r), dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
Tactic: by_cases hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
have neg : ∀ (hr : ¬0 ≤ r), dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r
Tactic: by_cases hr : 0 ≤ r
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
f g : (b : β) → X b
b : β
⊢ nndist (f b) (g b) ≤ nndist f g
have rw : edist (f b) (g b) ≤ edist f g
Tactic: rw [← ENNReal.coe_le_coe, ← edist_nndist, ← edist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 < r
⊢ ball x r = Set.pi (α := X) Set.univ fun (b : β) ↦ ball (x b) r
have 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
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
Goal:
β : Type u_2
X : β → Type u_3
inst : Fintype β
inst_1 : (b : β) → PseudoMetricSpace (X b)
x : (b : β) → X b
r : ℝ
hr : 0 ≤ r
⊢ closedBall x r = Set.pi (α := X) Set.univ fun (b : β) ↦ closedBall (x b) r
have 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
Tactic: ext p
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 β
⊢ sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r
have inl : ∀ (hr : r < 0), sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r
Tactic: obtain hr | rfl | hr := lt_trichotomy r 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
⊢ sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r
have inr : ∀ (h : LT.lt (α := ℝ) 0 0 ∨ Nonempty β),
  sphere x 0 = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0) ∩ closedBall x 0
Tactic: obtain hr | rfl | hr := lt_trichotomy r 0
Cleared hypotheses: r, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
⊢ sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r
have inr₁ : ∀ (hr : 0 < 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 β
⊢ sphere x 0 = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0) ∩ closedBall x 0
have inr : sphere x 0 ⊆ ⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0
Tactic: rw [closedBall_eq_sphere_of_nonpos le_rfl, eq_comm, Set.inter_eq_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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 β := ⋯
⊢ sphere x 0 ⊆ ⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0
have inr : ∀ (inhabited_h : Inhabited β), sphere x 0 ⊆ ⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) 0
Tactic: inhabit β
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
have inr : sphere x 0 ⊆ Set.preimage (β := X default) (Function.eval (β := X) default) (sphere (x default) 0)
Tactic: refine subset_iUnion_of_subset default ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (hypothesis)
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
⊢ x ∈ Set.preimage (β := X default) (Function.eval (β := X) default) (sphere (x_1 default) 0)
have hx₁ : dist x x_1 ≤ 0
Tactic: replace hx := hx.le
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (hypothesis)
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
⊢ x ∈ Set.preimage (β := X default) (Function.eval (β := X) default) (sphere (x_1 default) 0)
have hx₁ : ∀ (b : β), dist (x b) (x_1 b) ≤ 0
Tactic: rw [dist_pi_le_iff le_rfl] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
⊢ sphere x r = (⋃ (i : β), Function.eval (β := X) i ⁻¹' sphere (x i) r) ∩ closedBall x r
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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)
have refine_1 : ∀ (k : β),
  nndist.{u_4} (α := Y) (Pi.single (M := fun (a : β) ↦ Y) i a k : Y) (Pi.single (M := fun (j : β) ↦ Y) j b k : Y) ≤
    max (nndist a 0) (nndist b 0)
Tactic: refine le_antisymm (nndist_pi_le_iff.2 fun k ↦ ?_) (max_le ?_ ?_)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Pseudo.Pi (goal)
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
refine_1 :
  ∀ (k : β),
    nndist.{u_4} (α := Y) (Pi.single (M := fun (a : β) ↦ Y) i a k : Y) (Pi.single (M := fun (j : β) ↦ Y) j b k : Y) ≤
      max (nndist a 0) (nndist b 0)
⊢ 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)
have refine_2 : nndist a 0 ≤ nndist (α := (j : β) → Y) (Pi.single (M := fun (a : β) ↦ Y) i a) (Pi.single (M := fun (j : β) ↦ Y) j b)
Tactic: refine le_antisymm (nndist_pi_le_iff.2 fun k ↦ ?_) (max_le ?_ ?_)