awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Infsep
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)
neg : ∀ (hs : ¬s.Nontrivial), s.infsep = 0
⊢ s.infsep = if hs : s.Nontrivial then s.offDiag.toFinset.inf' ⋯ (uncurry dist) else 0

Tactic:
split_ifs with hs
-- Module: Mathlib.Topology.MetricSpace.Infsep
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)

Tactic:
eq_of_forall_le_iff fun _ => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
pos : ∀ (x : ℝ), x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (uncurry dist)
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
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)
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
⊢ x ≤ s.infsep ↔ x ≤ s.offDiag.toFinset.inf' ⋯ (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]

Premises used: Finset.le_inf'_iff, and_imp, Set.mem_offDiag, imp_forall_iff, Prod.forall, Set.mem_toFinset, Function.uncurry_apply_pair, Set.Nontrivial.le_infsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : ¬s.Nontrivial
⊢ s.Subsingleton

Tactic:
rw [not_nontrivial_iff] at hs

Premises used: Set.not_nontrivial_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
hs.infsep_zero

Premises used: Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
inst_2 : Fintype (↑s : Type u_1)
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
exact hs.infsep_zero

Premises used: Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
x y z : α
s t : Set α
inst_1 : Fintype (↑s : Type u_1)
hs : s.Nontrivial
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Infsep
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)
rw₁ rw₂ : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
rw [Set.infsep_of_fintype, dif_pos hs]

Premises used: dif_pos, Set.infsep_of_fintype
-- Module: Mathlib.Topology.MetricSpace.Infsep
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)
classical₁ classical₂ : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = s.offDiag.toFinset.inf' ⋯ (uncurry dist)
⊢ s.infsep = s.offDiag.toFinset.inf' ⋯ (uncurry dist)

Tactic:
classical rw [Set.infsep_of_fintype, dif_pos hs]

Premises used: dif_pos, Set.infsep_of_fintype
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
x y z : α
s t : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
⊢ ⋯.toFinset (s := s.offDiag).Nonempty

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Infsep
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)
neg : ∀ (hs : ¬s.Nontrivial), s.infsep = 0
⊢ s.infsep = if hs : s.Nontrivial then ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist) else 0

Tactic:
split_ifs with hs
-- Module: Mathlib.Topology.MetricSpace.Infsep
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)

Tactic:
eq_of_forall_le_iff fun _ => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Nontrivial
pos : ∀ (x : ℝ), x ≤ s.infsep ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
⊢ s.infsep = ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Premises used: eq_of_forall_le_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
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
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)
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
⊢ x ≤ s.infsep ↔ x ≤ ⋯.toFinset (s := s.offDiag).inf' ⋯ (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]

Premises used: Finset.le_inf'_iff, and_imp, Set.Finite.mem_toFinset, Set.mem_offDiag, imp_forall_iff, Prod.forall, Function.uncurry_apply_pair, Set.Nontrivial.le_infsep_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : ¬s.Nontrivial
⊢ s.Subsingleton

Tactic:
rw [not_nontrivial_iff] at hs

Premises used: Set.not_nontrivial_iff
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
hs.infsep_zero

Premises used: Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Decidable s.Nontrivial
hsf : s.Finite
hs : s.Subsingleton
⊢ s.infsep = 0

Tactic:
exact hs.infsep_zero

Premises used: Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
x y z : α
s t : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ ⋯.toFinset (s := s.offDiag).Nonempty

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
simp_rw :
  (if hs : s.Nontrivial then ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist) else 0) =
    ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
⊢ s.infsep = ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)

Tactic:
simp_rw [hsf.infsep, dif_pos hs]

Premises used: Set.Finite.infsep, dif_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
classical :
  (if hs : s.Nontrivial then ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist) else 0) =
    ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)
⊢ s.infsep = ⋯.toFinset (s := s.offDiag).inf' ⋯ (uncurry dist)

Tactic:
classical simp_rw [hsf.infsep, dif_pos hs]

Premises used: dif_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
rw : (↑s : Set α).offDiag.Nonempty ↔ s.offDiag.Nonempty
rw₁ : (↑s.offDiag : Set (α × α)).Nonempty ↔ s.offDiag.Nonempty
rw₂ rw₃ : s.offDiag.Nonempty ↔ s.offDiag.Nonempty
⊢ (↑s : Set α).Nontrivial ↔ s.offDiag.Nonempty

Tactic:
rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]

Premises used: Set.offDiag_nonempty, Finset.coe_nonempty, Finset.coe_offDiag
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
⊢ (↑s : Set α).Nontrivial ↔ s.offDiag.Nonempty

Tactic:
have H : (s : Set α).Nontrivial ↔ s.offDiag.Nonempty := by
    rw [← Set.offDiag_nonempty, ← Finset.coe_offDiag, Finset.coe_nonempty]
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
H : (↑s : Set α).Nontrivial ↔ s.offDiag.Nonempty
pos : ∀ (hs : s.offDiag.Nonempty), (↑s : Set α).infsep = s.offDiag.inf' hs (uncurry dist)
neg : ∀ (hs : ¬s.offDiag.Nonempty), (↑s : Set α).infsep = 0
⊢ (↑s : Set α).infsep = if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0

Tactic:
split_ifs with hs
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
H : (↑s : Set α).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
pos : (↑s : Set α).offDiag.toFinset.inf' ⋯ (uncurry dist) = s.offDiag.inf' hs (uncurry dist)
pos₁ : ((↑s.offDiag : Set (α × α)).toFinset.inf' ⋯ fun (x : α × α) ↦ uncurry dist x) = s.offDiag.inf' hs (uncurry dist)
⊢ (↑s : Set α).infsep = s.offDiag.inf' hs (uncurry dist)

Tactic:
simp_rw [(H.mpr hs).infsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

Premises used: Iff.mpr, Finset.toFinset_coe, Set.Nontrivial.infsep_of_fintype, Finset.coe_offDiag
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
H : (↑s : Set α).Nontrivial ↔ s.offDiag.Nonempty
hs : s.offDiag.Nonempty
pos : (↑s : Set α).offDiag.toFinset.inf' ⋯ (uncurry dist) = s.offDiag.inf' hs (uncurry dist)
pos₁ : ((↑s.offDiag : Set (α × α)).toFinset.inf' ⋯ fun (x : α × α) ↦ uncurry dist x) = s.offDiag.inf' hs (uncurry dist)
⊢ (↑s : Set α).infsep = s.offDiag.inf' hs (uncurry dist)

Tactic:
classical simp_rw [(H.mpr hs).infsep_of_fintype, ← Finset.coe_offDiag, Finset.toFinset_coe]

Premises used: Iff.mpr, Finset.toFinset_coe, Set.Nontrivial.infsep_of_fintype, Finset.coe_offDiag
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
H : (↑s : Set α).Nontrivial ↔ s.offDiag.Nonempty
hs : ¬s.offDiag.Nonempty
⊢ (↑s : Set α).infsep = 0

Tactic:
(not_nontrivial_iff.mp (H.mp.mt hs)).infsep_zero

Premises used: Function.mt, Set.not_nontrivial_iff, Iff.mp, Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
H : (↑s : Set α).Nontrivial ↔ s.offDiag.Nonempty
hs : ¬s.offDiag.Nonempty
⊢ (↑s : Set α).infsep = 0

Tactic:
exact (not_nontrivial_iff.mp (H.mp.mt hs)).infsep_zero

Premises used: Function.mt, Set.not_nontrivial_iff, Iff.mp, Set.Subsingleton.infsep_zero
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
hs : s.offDiag.Nonempty
rw : (if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0) = s.offDiag.inf' hs (uncurry dist)
rw₁ rw₂ : s.offDiag.inf' hs (uncurry dist) = s.offDiag.inf' hs (uncurry dist)
⊢ (↑s : Set α).infsep = s.offDiag.inf' hs (uncurry dist)

Tactic:
rw [Finset.coe_infsep, dif_pos hs]

Premises used: dif_pos, Finset.coe_infsep
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
hs : s.offDiag = ∅
⊢ ¬s.offDiag.Nonempty

Tactic:
rw [← Finset.not_nonempty_iff_eq_empty] at hs

Premises used: Finset.not_nonempty_iff_eq_empty
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Finset α
hs : ¬s.offDiag.Nonempty
rw : Eq (α := ℝ) (if hs : s.offDiag.Nonempty then s.offDiag.inf' hs (uncurry dist) else 0) 0
rw₁ rw₂ : Eq (α := ℝ) 0 0
⊢ (↑s : Set α).infsep = 0

Tactic:
rw [Finset.coe_infsep, dif_neg hs]

Premises used: Finset.coe_infsep, dif_neg
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
intro : ∀ (val : Fintype (↑s : Type u_1)), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y

Tactic:
cases nonempty_fintype s

Premises used: Set.Elem, nonempty_fintype
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
intro : ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y

Tactic:
simp_rw [hs.infsep_of_fintype]

Premises used: Set.Nontrivial.infsep_of_fintype
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
⊢ s.offDiag.toFinset.Nonempty

Tactic:
simpa
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
intro :
  ∀ (w : α × α) (hxy : w ∈ s.offDiag.toFinset) (hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w),
    ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y

Tactic:
rcases Finset.exists_mem_eq_inf' (s := s.offDiag.toFinset) (by simpa) (uncurry dist) with
      ⟨w, hxy, hed⟩

Premises used: Dist.dist, Function.uncurry, Finset.exists_mem_eq_inf'
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
w : α × α
hxy : w ∈ s.offDiag.toFinset
hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w
⊢ w ∈ s.offDiag

Tactic:
simp_rw [mem_toFinset] at hxy

Premises used: Set.mem_toFinset
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
w : α × α
hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w
hxy : w ∈ s.offDiag
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y

Tactic:
⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

Premises used: Prod.fst, And.right, And.left, And.intro, Exists.intro, Prod.snd
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
val : Fintype (↑s : Type u_1)
w : α × α
hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w
hxy : w ∈ s.offDiag
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y

Tactic:
exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
hs : s.Nontrivial
intro : ∀ (val : Fintype (↑s : Type u_1)), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y
intro₁ :
  ∀ (val : Fintype (↑s : Type u_1)), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y
intro₂ :
  ∀ (val : Fintype (↑s : Type u_1)) (w : α × α) (hxy : w ∈ s.offDiag.toFinset)
    (hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w),
    ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y
intro₃ :
  ∀ (val : Fintype (↑s : Type u_1)) (w : α × α) (hed : s.offDiag.toFinset.inf' ⋯ (uncurry dist) = uncurry dist w)
    (hxy : w ∈ s.offDiag), ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.offDiag.toFinset.inf' ⋯ (uncurry dist) = dist x y
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y

Tactic:
classical
    cases nonempty_fintype s
    simp_rw [hs.infsep_of_fintype]
    rcases Finset.exists_mem_eq_inf' (s := s.offDiag.toFinset) (by simpa) (uncurry dist) with
      ⟨w, hxy, hed⟩
    simp_rw [mem_toFinset] at hxy
    exact ⟨w.fst, hxy.1, w.snd, hxy.2.1, hxy.2.2, hed⟩

Premises used: Set.Elem, nonempty_fintype, Set.mem_toFinset
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : PseudoMetricSpace α
s : Set α
hsf : s.Finite
hs : s.Nontrivial
⊢ ∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.infsep = dist x y

Tactic:
letI := hsf.fintype
  hs.infsep_exists_of_finite

Premises used: Set.Nontrivial.infsep_exists_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
rw : s.einfsep = 0 → s.Subsingleton
⊢ s.infsep = 0 ↔ s.Subsingleton

Tactic:
rw [infsep_zero, einfsep_eq_top_iff, or_iff_right_iff_imp]

Premises used: Set.einfsep_eq_top_iff, Set.infsep_zero, or_iff_right_iff_imp
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ s.einfsep = 0 → s.Subsingleton

Tactic:
fun H => (einfsep_pos_of_finite.ne' H).elim

Premises used: False.elim, LT.lt.ne', Set.einfsep_pos_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ s.einfsep = 0 → s.Subsingleton

Tactic:
exact fun H => (einfsep_pos_of_finite.ne' H).elim

Premises used: False.elim, LT.lt.ne', Set.einfsep_pos_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
rw : s.Nontrivial → 0 < s.einfsep
⊢ 0 < s.infsep ↔ s.Nontrivial

Tactic:
rw [infsep_pos, einfsep_lt_top_iff, and_iff_right_iff_imp]

Premises used: Set.einfsep_lt_top_iff, and_iff_right_iff_imp, Set.infsep_pos
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ s.Nontrivial → 0 < s.einfsep

Tactic:
fun _ => einfsep_pos_of_finite

Premises used: Set.einfsep_pos_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Set α
inst_1 : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ s.Nontrivial → 0 < s.einfsep

Tactic:
exact fun _ => einfsep_pos_of_finite

Premises used: Set.einfsep_pos_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Set α
hs : s.Finite
⊢ s.infsep = 0 ↔ s.Subsingleton

Tactic:
letI := hs.fintype
  infsep_zero_iff_subsingleton_of_finite

Premises used: Set.infsep_zero_iff_subsingleton_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Set α
hs : s.Finite
⊢ 0 < s.infsep ↔ s.Nontrivial

Tactic:
letI := hs.fintype
  infsep_pos_iff_nontrivial_of_finite

Premises used: Set.infsep_pos_iff_nontrivial_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Finset α
⊢ (↑s : Set α).infsep = 0 ↔ (↑s : Set α).Subsingleton

Tactic:
infsep_zero_iff_subsingleton_of_finite

Premises used: Set.infsep_zero_iff_subsingleton_of_finite
-- Module: Mathlib.Topology.MetricSpace.Infsep
Goal:
α : Type u_1
inst : MetricSpace α
s : Finset α
⊢ 0 < (↑s : Set α).infsep ↔ (↑s : Set α).Nontrivial

Tactic:
infsep_pos_iff_nontrivial_of_finite

Premises used: Set.infsep_pos_iff_nontrivial_of_finite
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
inst : PseudoEMetricSpace X
inst_1 : SMul M X
inst_2 : IsIsometricSMul M X
⊢ ContinuousConstSMul M X

Tactic:
⟨fun c => (isometry_smul X c).continuous⟩

Premises used: ContinuousConstSMul.mk, Isometry.continuous, IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
inst : PseudoEMetricSpace X
inst_1 : SMul M X
inst_2 : SMul.{u, w} Mᵐᵒᵖ X
inst_3 : IsCentralScalar M X
inst_4 : IsIsometricSMul M X
c : Mᵐᵒᵖ
x y : X
⊢ edist.{w} (α := X) ((fun (x : X) ↦ c • x) x) ((fun (x : X) ↦ c • x) y) = edist x y

Tactic:
simpa only [← op_smul_eq_smul] using isometry_smul X c.unop x y

Premises used: IsIsometricSMul.isometry_smul, MulOpposite.unop, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
X : Type w
inst : PseudoEMetricSpace X
inst_1 : SMul M X
inst_2 : IsIsometricSMul M X
c : M
x y : X
⊢ edist (c • x) (c • y) = edist x y

Tactic:
isometry_smul X c x y

Premises used: IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
X : Type w
inst : PseudoEMetricSpace X
inst_1 : SMul M X
inst_2 : IsIsometricSMul M X
c : M
s : Set X
⊢ Metric.ediam (c • s) = Metric.ediam s

Tactic:
(isometry_smul _ _).ediam_image s

Premises used: Isometry.ediam_image, IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : Mul M
inst_1 : PseudoEMetricSpace M
inst_2 : IsIsometricSMul M M
a : M
⊢ Isometry (β := M) fun (x : M) ↦ a * x

Tactic:
isometry_smul M a

Premises used: IsIsometricSMul.isometry_smul
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : Mul M
inst_1 : PseudoEMetricSpace M
inst_2 : IsIsometricSMul M M
a b c : M
⊢ edist (a * b) (a * c) = edist b c

Tactic:
isometry_mul_left a b c

Premises used: isometry_mul_left
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : Mul M
inst_1 : PseudoEMetricSpace M
inst_2 : IsIsometricSMul Mᵐᵒᵖ M
a : M
⊢ Isometry (β := M) fun (x : M) ↦ x * a

Tactic:
isometry_smul M (MulOpposite.op a)

Premises used: IsIsometricSMul.isometry_smul, MulOpposite.unop, MulOpposite.op
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : Mul M
inst_1 : PseudoEMetricSpace M
inst_2 : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ edist (a * c) (b * c) = edist a b

Tactic:
isometry_mul_right c a b

Premises used: isometry_mul_right
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
inst : DivInvMonoid M
inst_1 : PseudoEMetricSpace M
inst_2 : IsIsometricSMul Mᵐᵒᵖ M
a b c : M
⊢ edist (a / c) (b / c) = edist a b

Tactic:
simp only [div_eq_mul_inv, edist_mul_right]

Premises used: edist_mul_right, div_eq_mul_inv