awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε (f '' A) (f '' C')
⊢ IsCover ε A C'

Tactic:
simp only [hf.isCover_image_iff] at hC_cover

Premises used: Isometry.isCover_image_iff
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ ⨅ (_ : IsCover ε A C'), C'.encard ≤ (f '' C').encard

Tactic:
(iInf_le _ hC_cover).trans ?_

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
refine_2 : C'.encard ≤ (f '' C').encard
⊢ ⨅ (_ : IsCover ε A C'), C'.encard ≤ (f '' C').encard

Tactic:
refine (iInf_le _ hC_cover).trans ?_

Premises used: LE.le.trans, iInf_le
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
refine_2 : InjOn f C'
⊢ C'.encard ≤ (f '' C').encard

Tactic:
rw [InjOn.encard_image]

Premises used: Set.InjOn.encard_image
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ InjOn f C'

Tactic:
hf_inj.mono hC'_subset

Premises used: Set.InjOn.mono
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
C' : Set X
hC'_subset : C' ⊆ A
hC_subset : f '' C' ⊆ f '' A
hC_cover : IsCover ε A C'
⊢ InjOn f C'

Tactic:
exact hf_inj.mono hC'_subset

Premises used: Set.InjOn.mono
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
A : Set X
ε : ℝ≥0
f : X → Y
hf : Isometry f
hf_inj : InjOn f A
refine_1 : coveringNumber ε (f '' A) ≤ coveringNumber ε A
refine_2 refine_2₁ : coveringNumber ε A ≤ coveringNumber ε (f '' A)
⊢ coveringNumber ε (f '' A) = coveringNumber ε A

Tactic:
classical
  refine le_antisymm ?_ ?_
  · simp only [coveringNumber, le_iInf_iff]
    intro C hC_subset hC_cover
    refine (iInf_le _ (C.image f)).trans ?_
    simp only [Set.image_subset_iff]
    have : ↑C ⊆ f ⁻¹' f '' A := hC_subset.trans (Set.subset_preimage_image f A)
    refine (iInf_le _ this).trans ?_
    rw [hf.isCover_image_iff]
    refine (iInf_le _ hC_cover).trans ?_
    exact encard_image_le f C
  · simp only [coveringNumber, le_iInf_iff]
    intro C hC_subset hC_cover
    obtain ⟨C', hC'_subset, rfl⟩ : ∃ C', C' ⊆ A ∧ C = C'.image f := by
      have (x : C) : ∃ y ∈ A, f y = x := by simpa using hC_subset x.2
      choose g hg_mem hg using this
      refine ⟨Set.range g, ?_, ?_⟩
      · rwa [Set.range_subset_iff]
      · ext
        simp
        grind
    refine (iInf_le _ C').trans <| (iInf_le _ hC'_subset).trans ?_
    simp only [hf.isCover_image_iff] at hC_cover
    refine (iInf_le _ hC_cover).trans ?_
    rw [InjOn.encard_image]
    exact hf_inj.mono hC'_subset

Premises used: Isometry.isCover_image_iff, le_iInf_iff, Metric.coveringNumber, le_antisymm, Set.InjOn.encard_image, Set.image_subset_iff, rfl
-- Module: Mathlib.Topology.MetricSpace.CoveringNumbers
Goal:
Y : Type u_2
inst : PseudoEMetricSpace Y
ε : ℝ≥0
X : Type u_3
inst_1 : EMetricSpace X
f : X → Y
hf : Isometry f
A : Set X
⊢ coveringNumber ε (f '' A) = coveringNumber ε A

Tactic:
hf.coveringNumber_image' hf.injective.injOn

Premises used: Function.Injective.injOn, Isometry.coveringNumber_image', Isometry.injective
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u_3
m m' : MetricSpace α
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
mk :
  ∀ [toPseudoMetricSpace : PseudoMetricSpace α] (eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y)
    (h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist),
    { toPseudoMetricSpace := toPseudoMetricSpace, eq_of_dist_eq_zero := @eq_of_dist_eq_zero : MetricSpace α } = m'
⊢ m = m'

Tactic:
cases m
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u_3
m' : MetricSpace α
toPseudoMetricSpace : PseudoMetricSpace α
eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
mk :
  ∀ [toPseudoMetricSpace_1 : PseudoMetricSpace α] (eq_of_dist_eq_zero_1 : ∀ {x y : α}, dist x y = 0 → x = y)
    (h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist),
    { toPseudoMetricSpace := toPseudoMetricSpace, eq_of_dist_eq_zero := @eq_of_dist_eq_zero : MetricSpace α } =
      { toPseudoMetricSpace := toPseudoMetricSpace_1, eq_of_dist_eq_zero := @eq_of_dist_eq_zero_1 }
⊢ { toPseudoMetricSpace := toPseudoMetricSpace, eq_of_dist_eq_zero := @eq_of_dist_eq_zero : MetricSpace α } = m'

Tactic:
cases m'
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u_3
toPseudoMetricSpace : PseudoMetricSpace α
eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace_1 : PseudoMetricSpace α
eq_of_dist_eq_zero_1 : ∀ {x y : α}, dist x y = 0 → x = y
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
mk : toPseudoMetricSpace = toPseudoMetricSpace_1
⊢ { toPseudoMetricSpace := toPseudoMetricSpace, eq_of_dist_eq_zero := @eq_of_dist_eq_zero : MetricSpace α } =
    { toPseudoMetricSpace := toPseudoMetricSpace_1, eq_of_dist_eq_zero := @eq_of_dist_eq_zero_1 }

Tactic:
congr
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u_3
toPseudoMetricSpace : PseudoMetricSpace α
eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace_1 : PseudoMetricSpace α
eq_of_dist_eq_zero_1 : ∀ {x y : α}, dist x y = 0 → x = y
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
mk : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
⊢ toPseudoMetricSpace = toPseudoMetricSpace_1

Tactic:
ext1
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u_3
toPseudoMetricSpace : PseudoMetricSpace α
eq_of_dist_eq_zero : ∀ {x y : α}, dist x y = 0 → x = y
toPseudoMetricSpace_1 : PseudoMetricSpace α
eq_of_dist_eq_zero_1 : ∀ {x y : α}, dist x y = 0 → x = y
h : Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist
⊢ Eq.{u_3 + 1} (α := Dist α) PseudoMetricSpace.toDist PseudoMetricSpace.toDist

Tactic:
assumption
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
⊢ dist x y = 0 → x = y

Tactic:
MetricSpace.eq_of_dist_eq_zero

Premises used: MetricSpace.eq_of_dist_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
⊢ dist x y = 0 ↔ x = y

Tactic:
Iff.intro eq_of_dist_eq_zero fun this => this ▸ dist_self _

Premises used: Eq.rec, eq_of_dist_eq_zero, dist_self, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
rw : dist x y = 0 ↔ x = y
rw₁ rw₂ : x = y ↔ x = y
⊢ 0 = dist x y ↔ x = y

Tactic:
rw [eq_comm, dist_eq_zero]

Premises used: eq_comm, dist_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
⊢ dist x y ≠ 0 ↔ x ≠ y

Tactic:
simpa only [not_iff_not] using dist_eq_zero

Premises used: not_iff_not, dist_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
⊢ dist x y ≤ 0 ↔ x = y

Tactic:
simpa [le_antisymm_iff, dist_nonneg] using @dist_eq_zero _ _ x y

Premises used: dist_nonneg, le_antisymm_iff, dist_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
⊢ 0 < dist x y ↔ x ≠ y

Tactic:
simpa only [not_le] using not_congr dist_le_zero

Premises used: not_le, dist_le_zero, not_congr
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
h : ∀ ε > 0, dist x y ≤ ε
⊢ x = y

Tactic:
eq_of_dist_eq_zero (eq_of_le_of_forall_lt_imp_le_of_dense dist_nonneg h)

Premises used: dist_nonneg, eq_of_dist_eq_zero, eq_of_le_of_forall_lt_imp_le_of_dense
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
⊢ nndist x y = 0 → x = y

Tactic:
simp only [NNReal.eq_iff, ← dist_nndist, imp_self, NNReal.coe_zero, dist_eq_zero]

Premises used: NNReal.coe_zero, NNReal.eq_iff, dist_nndist, imp_self, dist_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
⊢ nndist x y = 0 ↔ x = y

Tactic:
simp only [NNReal.eq_iff, ← dist_nndist, NNReal.coe_zero, dist_eq_zero]

Premises used: NNReal.coe_zero, NNReal.eq_iff, dist_nndist, dist_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x y : γ
⊢ 0 = nndist x y ↔ x = y

Tactic:
simp only [NNReal.eq_iff, ← dist_nndist, NNReal.coe_zero, zero_eq_dist]

Premises used: zero_eq_dist, NNReal.coe_zero, NNReal.eq_iff, dist_nndist
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
⊢ closedBall x 0 = {x}

Tactic:
Set.ext fun _ => dist_le_zero

Premises used: Set.ext, dist_le_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
⊢ sphere x 0 = {x}

Tactic:
Set.ext fun _ => dist_eq_zero

Premises used: Set.ext, dist_eq_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
r : ℝ
hr : r ≤ 0
inl : ∀ (hr : r < 0), (closedBall x r).Subsingleton
inr : ∀ (hr : LE.le (α := ℝ) 0 0), (closedBall x 0).Subsingleton
⊢ (closedBall x r).Subsingleton

Tactic:
rcases hr.lt_or_eq with (hr | rfl)

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
r : ℝ
hr_1 : r ≤ 0
hr : r < 0
inl : Set.Subsingleton.{w} (α := γ) ∅
⊢ (closedBall x r).Subsingleton

Tactic:
rw [closedBall_eq_empty.2 hr]

Premises used: Iff.mpr, Metric.closedBall_eq_empty
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
r : ℝ
hr_1 : r ≤ 0
hr : r < 0
⊢ Set.Subsingleton.{w} (α := γ) ∅

Tactic:
subsingleton_empty

Premises used: Set.subsingleton_empty
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
r : ℝ
hr_1 : r ≤ 0
hr : r < 0
⊢ Set.Subsingleton.{w} (α := γ) ∅

Tactic:
exact subsingleton_empty

Premises used: Set.subsingleton_empty
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
hr : LE.le (α := ℝ) 0 0
inr : Set.Subsingleton (α := γ) {x}
⊢ (closedBall x 0).Subsingleton

Tactic:
rw [closedBall_zero]

Premises used: Metric.closedBall_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
hr : LE.le (α := ℝ) 0 0
⊢ Set.Subsingleton (α := γ) {x}

Tactic:
subsingleton_singleton

Premises used: Set.subsingleton_singleton
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
hr : LE.le (α := ℝ) 0 0
⊢ Set.Subsingleton (α := γ) {x}

Tactic:
exact subsingleton_singleton

Premises used: Set.subsingleton_singleton
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type w
inst : MetricSpace γ
x : γ
r : ℝ
hr : r ≤ 0
⊢ (sphere x r).Subsingleton

Tactic:
(subsingleton_closedBall x hr).anti sphere_subset_closedBall

Premises used: Set.Subsingleton.anti, Metric.sphere_subset_closedBall, Metric.subsingleton_closedBall
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
h : ∀ (x x_1 : γ), dist x x_1 = dist x x_1
⊢ m.replaceUniformity H = m

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type u_3
U : UniformSpace γ
m : MetricSpace γ
H : 𝓤 γ = 𝓤 γ
x x_1 : γ
⊢ dist x x_1 = dist x x_1

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = UniformSpace.toTopologicalSpace
h : ∀ (x x_1 : γ), dist x x_1 = dist x x_1
⊢ m.replaceTopology H = m

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
γ : Type u_3
U : TopologicalSpace γ
m : MetricSpace γ
H : U = UniformSpace.toTopologicalSpace
x x_1 : γ
⊢ dist x x_1 = dist x x_1

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u_3
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
h : ∀ (x x_1 : α), dist x x_1 = dist x x_1
⊢ m.replaceBornology H = m

Tactic:
ext
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u_3
m : MetricSpace α
B : Bornology α
H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s
x x_1 : α
⊢ dist x x_1 = dist x x_1

Tactic:
rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
x x_1 x_2 : Empty
rw rw₁ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) 0 0

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
x x_1 x_2 : PUnit.{u + 1}
rw rw₁ : LE.le (α := ℝ) 0 0
⊢ 0 ≤ HAdd.hAdd (α := ℝ) 0 0

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
α : Type u
β : Type v
X : Type u_1
ι : Type u_2
inst : PseudoMetricSpace α
γ : Type w
inst_1 : MetricSpace γ
⊢ 𝓤 PUnit.{u + 1} = ⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : PUnit.{u + 1} × PUnit.{u + 1} | 0 < ε}

Tactic:
simp +contextual [principal_univ, eq_top_of_neBot (𝓤 PUnit)]

Premises used: uniformity, Filter.principal_univ, PUnit, Filter.eq_top_of_neBot
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
X : Type u_1
inst : Dist X
a b : X
⊢ dist (α := Additive X) ((ofMul : (a : X) → Additive X) a : Additive X)
      ((ofMul : (a : X) → Additive X) b : Additive X) =
    dist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
X : Type u_1
inst : Dist X
a b : X
⊢ dist (α := Multiplicative X) ((ofAdd : (a : X) → Multiplicative X) a : Multiplicative X)
      ((ofAdd : (a : X) → Multiplicative X) b : Multiplicative X) =
    dist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
X : Type u_1
inst : Dist X
a b : Additive X
⊢ dist (α := X) ((toMul : (a : Additive X) → X) a : X) ((toMul : (a : Additive X) → X) b : X) = dist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
X : Type u_1
inst : Dist X
a b : Multiplicative X
⊢ dist (α := X) ((toAdd : (a : Multiplicative X) → X) a : X) ((toAdd : (a : Multiplicative X) → X) b : X) = dist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
X : Type u_1
inst : Dist X
a b : X
⊢ dist (α := Xᵒᵈ) ((toDual : (a : X) → Xᵒᵈ) a : Xᵒᵈ) ((toDual : (a : X) → Xᵒᵈ) b : Xᵒᵈ) = dist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Defs
Goal:
X : Type u_1
inst : Dist X
a b : Xᵒᵈ
⊢ dist (α := X) ((ofDual : (a : Xᵒᵈ) → X) a : X) ((ofDual : (a : Xᵒᵈ) → X) b : X) = dist a b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : α →ᵈ β
h : f.toFun = g.toFun
mk :
  ∀ (toFun : α → β) (edist_eq' : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (toFun x) (toFun y) = (↑r : ℝ≥0∞) * edist x y)
    (h : { toFun := toFun, edist_eq' := edist_eq' : α →ᵈ β }.toFun = g.toFun),
    { toFun := toFun, edist_eq' := edist_eq' : α →ᵈ β } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
g : α →ᵈ β
toFun : α → β
edist_eq' : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (toFun x) (toFun y) = (↑r : ℝ≥0∞) * edist x y
h : { toFun := toFun, edist_eq' := edist_eq' : α →ᵈ β }.toFun = g.toFun
mk :
  ∀ (toFun_1 : α → β)
    (edist_eq'_1 : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (toFun_1 x) (toFun_1 y) = (↑r : ℝ≥0∞) * edist x y)
    (h :
      { toFun := toFun, edist_eq' := edist_eq' : α →ᵈ β }.toFun =
        { toFun := toFun_1, edist_eq' := edist_eq'_1 : α →ᵈ β }.toFun),
    { toFun := toFun, edist_eq' := edist_eq' : α →ᵈ β } = { toFun := toFun_1, edist_eq' := edist_eq'_1 }
⊢ { toFun := toFun, edist_eq' := edist_eq' : α →ᵈ β } = g

Tactic:
cases g
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
toFun : α → β
edist_eq' : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (toFun x) (toFun y) = (↑r : ℝ≥0∞) * edist x y
toFun_1 : α → β
edist_eq'_1 : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (toFun_1 x) (toFun_1 y) = (↑r : ℝ≥0∞) * edist x y
h :
  { toFun := toFun, edist_eq' := edist_eq' : α →ᵈ β }.toFun =
    { toFun := toFun_1, edist_eq' := edist_eq'_1 : α →ᵈ β }.toFun
⊢ { toFun := toFun, edist_eq' := edist_eq' : α →ᵈ β } = { toFun := toFun_1, edist_eq' := edist_eq'_1 }

Tactic:
congr
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α →ᵈ β
⊢ f.toFun = (⇑f : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
⊢ (⇑{ toFun := f, edist_eq' := h : α →ᵈ β } : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : α →ᵈ β
h : f = g
x : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)

Tactic:
DFunLike.congr_fun h x

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α →ᵈ β
x y : α
h : x = y
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
DFunLike.congr_arg f h

Premises used: DFunLike.congr_arg
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f g : α →ᵈ β
h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α →ᵈ β
h :
  ∃ (r : ℝ≥0),
    r ≠ 0 ∧
      ∀ (x y : α), edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
⊢ { toFun := (⇑f : (a : α) → β), edist_eq' := h : α →ᵈ β } = f

Tactic:
ext fun _ => rfl

Premises used: Dilation.ext, rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α →ᵈ β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ratio f = 1

Tactic:
if_pos h

Premises used: if_pos, Dilation.ratio
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : Subsingleton α
inst_4 : DilationClass F α β
f : F
x y : α
⊢ edist x y = 0 ∨ edist x y = ∞

Tactic:
simp [Subsingleton.elim x y]

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
pos : (∀ (x y : α), edist x y = 0 ∨ edist x y = ∞) → Ne (α := ℝ≥0) 1 0
neg :
  (¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞) →
    Exists.choose (p := fun (r : ℝ≥0) ↦
        r ≠ 0 ∧
          ∀ (x y : α),
            edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y)
        ⋯ ≠
      0
⊢ (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞ then 1
    else
      Exists.choose (p := fun (r : ℝ≥0) ↦
        r ≠ 0 ∧
          ∀ (x y : α),
            edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y)
        ⋯) ≠
    0

Tactic:
split_ifs
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ Ne (α := ℝ≥0) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ Ne (α := ℝ≥0) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ Exists.choose (p := fun (r : ℝ≥0) ↦
      r ≠ 0 ∧
        ∀ (x y : α), edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y)
      ⋯ ≠
    0

Tactic:
(DilationClass.edist_eq' f).choose_spec.1

Premises used: Exists.choose_spec, DilationClass.edist_eq', And.left
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
h : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ Exists.choose (p := fun (r : ℝ≥0) ↦
      r ≠ 0 ∧
        ∀ (x y : α), edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y)
      ⋯ ≠
    0

Tactic:
exact (DilationClass.edist_eq' f).choose_spec.1

Premises used: Exists.choose_spec, DilationClass.edist_eq', And.left
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
⊢ 0 < ratio f

Tactic:
(ratio_ne_zero f).bot_lt

Premises used: Dilation.ratio_ne_zero, Ne.bot_lt