awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
⊢ s.infsep = if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0
have pos : ∀ (hs : s.Nontrivial), s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
pos : ∀ (hs : s.Nontrivial), s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
⊢ s.infsep = if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0
have neg : ∀ (hs : ¬s.Nontrivial), s.infsep = 0
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ BddBelow (uncurry dist '' s.offDiag)
have refine : ∀ (d : ℝ) (h : d ∈ uncurry dist '' s.offDiag), 0 ≤ d
Tactic: refine ⟨0, fun d h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : d ∈ uncurry dist '' s.offDiag
⊢ 0 ≤ d
have h₁ : ∃ (a : α) (b : α), (a, b) ∈ s.offDiag ∧ dist a b = d
Tactic: simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
d : ℝ
h : ∃ (a : α) (b : α), (a, b) ∈ s.offDiag ∧ dist a b = d
⊢ 0 ≤ d
have rcases : ∀ (w w_1 : α), (w, w_1) ∈ s.offDiag → 0 ≤ dist w w_1
Tactic: rcases h with ⟨_, _, _, rfl⟩
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have hb : BddBelow (uncurry dist '' s.offDiag)
Tactic: have hb : BddBelow (uncurry dist '' s.offDiag) := by
      refine ⟨0, fun d h => ?_⟩
      simp_rw [mem_image, Prod.exists, uncurry_apply_pair] at h
      rcases h with ⟨_, _, _, rfl⟩
      exact dist_nonneg
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have pos : ∀ (x : ℝ), x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
Tactic: refine eq_of_forall_le_iff fun _ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x : ℝ
⊢ x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
Tactic: simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
⊢ x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have pos₁ : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
Tactic: simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
pos₁ : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
⊢ x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have pos₂ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
Tactic: simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
pos₁ : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
pos₂ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
⊢ x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have pos₃ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
  ∀ (i : α × α), i.1 ∈ s ∧ i.2 ∈ s ∧ i.1 ≠ i.2 → x ≤ uncurry dist i
Tactic: simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
pos₁ : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
pos₂ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
pos₃ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (i : α × α), i.1 ∈ s ∧ i.2 ∈ s ∧ i.1 ≠ i.2 → x ≤ uncurry dist i
⊢ x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have pos₄ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
  ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ uncurry dist (a, b)
Tactic: simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hs : s.Nontrivial
hb : BddBelow (uncurry dist '' s.offDiag)
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
pos₁ : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
pos₂ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ i ∈ s.offDiag, x ≤ uncurry dist i
pos₃ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (i : α × α), i.1 ∈ s ∧ i.2 ∈ s ∧ i.1 ≠ i.2 → x ≤ uncurry dist i
pos₄ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ uncurry dist (a, b)
⊢ x ≤ s.infsep ↔ x ≤ ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have pos₅ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ dist a b
Tactic: simp_rw [hs.le_infsep_iff, le_ciInf_set_iff (offDiag_nonempty.mpr hs) hb, imp_forall_iff,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have rw : Eq (α := ℝ) (if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0)
  (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
Tactic: rw [Set.infsep_eq_iInf, if_pos hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
rw :
  Eq (α := ℝ) (if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0)
    (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have rw₁ : Eq (α := ℝ) (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
  (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
Tactic: rw [Set.infsep_eq_iInf, if_pos hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have classical : Eq (α := ℝ) (if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0)
  (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
Tactic: classical rw [Set.infsep_eq_iInf, if_pos hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
classical :
  Eq (α := ℝ) (if s.Nontrivial then ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α) else 0)
    (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
⊢ s.infsep = ⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α)
have classical₁ : Eq (α := ℝ) (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
  (⨅ (d : (↑s.offDiag : Type u_1)), uncurry dist (↑d : α × α))
Tactic: classical rw [Set.infsep_eq_iInf, if_pos hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
⊢ s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0
have pos : ∀ (hs : s.Nontrivial), s.infsep = s.offDiag.toFinset.inf' sorry (uncurry dist)
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
pos : ∀ (hs : s.Nontrivial), s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
⊢ s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0
have neg : ∀ (hs : ¬s.Nontrivial), s.infsep = 0
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have pos : ∀ (x : ℝ), x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' sorry (uncurry dist)
Tactic: refine eq_of_forall_le_iff fun _ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
x : ℝ
⊢ x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ s.offDiag.toFinset.inf' sorry (uncurry dist)
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
⊢ x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have pos₁ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ x ≤ s.offDiag.toFinset.inf' sorry (uncurry dist)
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
⊢ x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have pos₂ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag.toFinset, x ≤ uncurry dist b
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₂ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag.toFinset, x ≤ uncurry dist b
⊢ x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have pos₃ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag, x ≤ uncurry dist b
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₂ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag.toFinset, x ≤ uncurry dist b
pos₃ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag, x ≤ uncurry dist b
⊢ x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have pos₄ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
  ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x ≤ uncurry dist b
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₂ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag.toFinset, x ≤ uncurry dist b
pos₃ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag, x ≤ uncurry dist b
pos₄ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x ≤ uncurry dist b
⊢ x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have pos₅ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
  ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ uncurry dist (a, b)
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
pos₂ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag.toFinset, x ≤ uncurry dist b
pos₃ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag, x ≤ uncurry dist b
pos₄ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (b : α × α), b.1 ∈ s ∧ b.2 ∈ s ∧ b.1 ≠ b.2 → x ≤ uncurry dist b
pos₅ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ uncurry dist (a, b)
⊢ x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have pos₆ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ (a b : α), a ∈ s ∧ b ∈ s ∧ a ≠ b → x ≤ dist a b
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, mem_toFinset, mem_offDiag,
      Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (hypothesis)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : ¬s.Nontrivial
⊢ s.infsep = 0
have hs₁ : s.Subsingleton
Tactic: rw [not_nontrivial_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have rw : (if hs : s.Nontrivial then s.offDiag.toFinset.inf' sorry (uncurry dist) else 0) = s.offDiag.toFinset.inf' sorry (uncurry dist)
Tactic: rw [Set.infsep_of_fintype, dif_pos hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
rw :
  (if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0) = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have rw₁ : s.offDiag.toFinset.inf' sorry (uncurry dist) = s.offDiag.toFinset.inf' sorry (uncurry dist)
Tactic: rw [Set.infsep_of_fintype, dif_pos hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have classical : (if hs : s.Nontrivial then s.offDiag.toFinset.inf' sorry (uncurry dist) else 0) = s.offDiag.toFinset.inf' sorry (uncurry dist)
Tactic: classical rw [Set.infsep_of_fintype, dif_pos hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
classical :
  (if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0) = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
have classical₁ : s.offDiag.toFinset.inf' sorry (uncurry dist) = s.offDiag.toFinset.inf' sorry (uncurry dist)
Tactic: classical rw [Set.infsep_of_fintype, dif_pos hs]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
⊢ s.infsep = if hs : s.Nontrivial then ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist) else 0
have pos : ∀ (hs : s.Nontrivial), s.infsep = sorry.toFinset (s := s.offDiag).inf' sorry (uncurry dist)
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
pos : ∀ (hs : s.Nontrivial), s.infsep = ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
⊢ s.infsep = if hs : s.Nontrivial then ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist) else 0
have neg : ∀ (hs : ¬s.Nontrivial), s.infsep = 0
Tactic: split_ifs with hs
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ s.infsep = ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
have pos : ∀ (x : ℝ), x ≤ s.infsep ↔ x ≤ sorry.toFinset (s := s.offDiag).inf' sorry (uncurry dist)
Tactic: refine eq_of_forall_le_iff fun _ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x : ℝ
⊢ x ≤ s.infsep ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
have pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ sorry.toFinset (s := s.offDiag).inf' sorry (uncurry dist)
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
⊢ x ≤ s.infsep ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
have pos₁ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
  x ≤ sorry.toFinset (s := s.offDiag).inf' sorry (uncurry dist)
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
pos₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
⊢ x ≤ s.infsep ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
have pos₂ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
  ∀ b ∈ sorry.toFinset (s := s.offDiag), x ≤ uncurry dist b
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Infsep (goal)
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
x : ℝ
pos : (∀ x_1 ∈ s, ∀ y ∈ s, x_1 ≠ y → x ≤ dist x_1 y) ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
pos₁ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
pos₂ :
  (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔
    ∀ b ∈ ⋯.toFinset (s := s.offDiag), x ≤ uncurry dist b
⊢ x ≤ s.infsep ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
have pos₃ : (∀ (x_1 x_2 : α), x_1 ∈ s → x_2 ∈ s → x_1 ≠ x_2 → x ≤ dist x_1 x_2) ↔ ∀ b ∈ s.offDiag, x ≤ uncurry dist b
Tactic: simp_rw [hs.le_infsep_iff, imp_forall_iff, Finset.le_inf'_iff, Finite.mem_toFinset,
      mem_offDiag, Prod.forall, uncurry_apply_pair, and_imp]