awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x y : α
pos :
  ∀ (key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞),
    edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y
neg :
  ∀ (key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞),
    edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) 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∞) *
        edist x y
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) =
    (↑(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∞) *
      edist x y

Tactic:
split_ifs with key
-- 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
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
pos :
  ∀ (r : ℝ≥0) (hne : r ≠ 0)
    (hr :
      ∀ (x y : α), edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y),
    edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y

Tactic:
rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩

Premises used: DilationClass.edist_eq'
-- 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
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
r : ℝ≥0
hne : r ≠ 0
hr : ∀ (x y : α), edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y

Tactic:
replace hr := hr x y
-- 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
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
r : ℝ≥0
hne : r ≠ 0
hr : edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
pos :
  ∀ (h : edist x y = 0),
    edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y
pos₁ :
  ∀ (h : edist x y = ∞),
    edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y

Tactic:
rcases key x y with h | h
-- 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
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
r : ℝ≥0
hne : r ≠ 0
hr : edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
h : edist x y = 0
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y

Tactic:
simp only [hr, h, mul_zero]

Premises used: MulZeroClass.mul_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
x y : α
key : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
r : ℝ≥0
hne : r ≠ 0
hr : edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
h : edist x y = ∞
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y

Tactic:
simp [hr, h, hne]
-- 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
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) 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∞) *
      edist x y

Tactic:
(DilationClass.edist_eq' f).choose_spec.2 x y

Premises used: Exists.choose_spec, DilationClass.edist_eq', And.right
-- 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
x y : α
key : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) 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∞) *
      edist x y

Tactic:
exact (DilationClass.edist_eq' f).choose_spec.2 x y

Premises used: Exists.choose_spec, DilationClass.edist_eq', And.right
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_5
β : Type u_6
F : Type u_7
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x y : α
⊢ nndist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = ratio f * nndist x y

Tactic:
simp only [← ENNReal.coe_inj, ← edist_nndist, ENNReal.coe_mul, edist_eq]

Premises used: ENNReal.coe_inj, Dilation.edist_eq, ENNReal.coe_mul, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_5
β : Type u_6
F : Type u_7
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x y : α
⊢ dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑(ratio f) : ℝ) * dist x y

Tactic:
simp only [dist_nndist, nndist_eq, NNReal.coe_mul]

Premises used: Dilation.nndist_eq, dist_nndist, NNReal.coe_mul
-- 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
x y : α
r : ℝ≥0
h₀ : edist x y ≠ 0
htop : edist x y ≠ ∞
hr : edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
⊢ r = ratio f

Tactic:
simpa only [hr, ENNReal.mul_left_inj h₀ htop, ENNReal.coe_inj] using edist_eq f x y

Premises used: ENNReal.coe_inj, Dilation.edist_eq, ENNReal.mul_left_inj
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_5
β : Type u_6
F : Type u_7
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = r * nndist x y
rwa : (↑(nndist x y) : ℝ≥0∞) ≠ 0
rwa₁ rwa₂ rwa₃ rwa₄ : nndist x y ≠ 0
⊢ edist x y ≠ 0

Tactic:
rwa [edist_nndist, ENNReal.coe_ne_zero]

Premises used: ENNReal.coe_ne_zero, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_5
β : Type u_6
F : Type u_7
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : nndist x y ≠ 0
hr : nndist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = r * nndist x y
rw : (↑(nndist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ≥0∞) = (↑r : ℝ≥0∞) * edist x y
rw₁ :
  (↑(nndist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ≥0∞) =
    (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)
rw₂ : (↑(r * nndist x y) : ℝ≥0∞) = (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)
rw₃ rw₄ : (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞) = (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)
⊢ edist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y

Tactic:
rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]

Premises used: ENNReal.coe_mul, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_6
β : Type u_7
F : Type u_5
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x y : α
r : ℝ≥0
hxy : dist x y ≠ 0
hr : dist.{u_7} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ) * dist x y
rw : dist.{u_7} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑(r * nndist x y) : ℝ)
rw₁ : (↑r : ℝ) * dist x y = (↑(r * nndist x y) : ℝ)
rw₂ : (↑r : ℝ) * dist x y = (↑r : ℝ) * (↑(nndist x y) : ℝ)
rw₃ rw₄ : (↑r : ℝ) * dist x y = (↑r : ℝ) * dist x y
⊢ (↑(nndist.{u_7} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ) = (↑(r * nndist x y) : ℝ)

Tactic:
rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]

Premises used: coe_nndist, NNReal.coe_mul
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α_1
inst_1 : PseudoEMetricSpace β_1
inst_2 : FunLike F α_1 β_1
α : Type u_5
β : Type u_6
inst_3 : PseudoMetricSpace α
inst_4 : PseudoMetricSpace β
f : α → β
h : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
rcases :
  ∀ (r : ℝ≥0) (hne : r ≠ 0) (h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y),
    ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y

Tactic:
rcases h with ⟨r, hne, h⟩
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α_1
inst_1 : PseudoEMetricSpace β_1
inst_2 : FunLike F α_1 β_1
α : Type u_5
β : Type u_6
inst_3 : PseudoMetricSpace α
inst_4 : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y

Tactic:
⟨r, hne, fun x y => ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α_1
inst_1 : PseudoEMetricSpace β_1
inst_2 : FunLike F α_1 β_1
α : Type u_5
β : Type u_6
inst_3 : PseudoMetricSpace α
inst_4 : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
refine : ∀ (x y : α), edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y

Tactic:
refine ⟨r, hne, fun x y => ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α_1
inst_1 : PseudoEMetricSpace β_1
inst_2 : FunLike F α_1 β_1
α : Type u_5
β : Type u_6
inst_3 : PseudoMetricSpace α
inst_4 : PseudoMetricSpace β
f : α → β
r : ℝ≥0
hne : r ≠ 0
h : ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
x y : α
rw : (↑(nndist (f x) (f y)) : ℝ≥0∞) = (↑r : ℝ≥0∞) * edist x y
rw₁ : (↑(nndist (f x) (f y)) : ℝ≥0∞) = (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)
rw₂ : (↑(nndist (f x) (f y)) : ℝ≥0∞) = (↑(r * nndist x y) : ℝ≥0∞)
rw₃ rw₄ : (↑(r * nndist x y) : ℝ≥0∞) = (↑(r * nndist x y) : ℝ≥0∞)
⊢ edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y

Tactic:
rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]

Premises used: ENNReal.coe_mul, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_5
β : Type u_6
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
h : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y
⊢ (⇑(mkOfNNDistEq f h) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_5
β : Type u_6
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵈ β
h :
  ∃ (r : ℝ≥0),
    r ≠ 0 ∧ ∀ (x y : α), nndist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = r * nndist x y
⊢ mkOfNNDistEq (⇑f : (a : α) → β) h = f

Tactic:
ext fun _ => rfl

Premises used: Dilation.ext, rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α_1
inst_1 : PseudoEMetricSpace β_1
inst_2 : FunLike F α_1 β_1
α : Type u_5
β : Type u_6
inst_3 : PseudoMetricSpace α
inst_4 : PseudoMetricSpace β
f : α → β
h : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = (↑r : ℝ) * dist x y
r : ℝ≥0
hr : r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = (↑r : ℝ) * dist x y
x y : α
rw : dist (f x) (f y) = (↑(r * nndist x y) : ℝ)
rw₁ : (↑r : ℝ) * dist x y = (↑(r * nndist x y) : ℝ)
rw₂ : (↑r : ℝ) * dist x y = (↑r : ℝ) * (↑(nndist x y) : ℝ)
rw₃ rw₄ : (↑r : ℝ) * dist x y = (↑r : ℝ) * dist x y
⊢ (↑(nndist (f x) (f y)) : ℝ) = (↑(r * nndist x y) : ℝ)

Tactic:
rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]

Premises used: coe_nndist, And.right, NNReal.coe_mul
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_5
β : Type u_6
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
h : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = (↑r : ℝ) * dist x y
⊢ (⇑(mkOfDistEq f h) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_5
β : Type u_6
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α →ᵈ β
h :
  ∃ (r : ℝ≥0),
    r ≠ 0 ∧ ∀ (x y : α), dist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ) * dist x y
⊢ mkOfDistEq (⇑f : (a : α) → β) h = f

Tactic:
ext fun _ => rfl

Premises used: Dilation.ext, 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 β
inst_2 : PseudoEMetricSpace γ
inst_3 : FunLike F α β
inst_4 : DilationClass F α β
f_1 : F
f : α → β
hf : Isometry f
⊢ ∀ (x y : α), edist (f x) (f y) = (↑1 : ℝ≥0∞) * edist x y

Tactic:
simpa using hf
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
pos : ∀ (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞), ratio (Isometry.toDilation f hf) = 1
neg : ∀ (h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (Isometry.toDilation f hf) = 1
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
ratio_of_trivial hf.toDilation h

Premises used: Isometry.toDilation, Dilation.ratio_of_trivial
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
exact ratio_of_trivial hf.toDilation h

Premises used: Isometry.toDilation, Dilation.ratio_of_trivial
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞
neg : ∀ (x y : α) (h₁ : edist x y ≠ 0) (h₂ : edist x y ≠ ∞), ratio (Isometry.toDilation f hf) = 1
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
obtain ⟨x, y, h₁, h₂⟩ := h
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
h₁ : edist x y ≠ 0
h₂ : edist x y ≠ ∞
⊢ edist.{u_2} (α := β) ((Isometry.toDilation f hf : (a : α) → β) x : β)
      ((Isometry.toDilation f hf : (a : α) → β) y : β) =
    (↑1 : ℝ≥0∞) * edist x y

Tactic:
simp [hf x y]
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
h₁ : edist x y ≠ 0
h₂ : edist x y ≠ ∞
⊢ ratio (Isometry.toDilation f hf) = 1

Tactic:
exact ratio_unique h₁ h₂ (by simp [hf x y]) |>.symm

Premises used: Dilation.ratio_unique, Eq.symm
-- 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
⊢ LipschitzWith.{u_1, u_2} (α := α) (β := β) (ratio f) (⇑f : (a : α) → β)

Tactic:
fun x y => (edist_eq f x y).le

Premises used: LipschitzWith, Dilation.edist_eq, Eq.le
-- 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
x y : α
⊢ ratio f ≠ 0

Tactic:
have hr : ratio f ≠ 0 := ratio_ne_zero f
-- 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
x y : α
hr : ratio f ≠ 0
⊢ edist x y ≤ (↑(ratio f)⁻¹ : ℝ≥0∞) * edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
mod_cast
    (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge

Premises used: Iff.mpr, Eq.ge, HMul.hMul, ENNReal.coe_inv._simp_1, congrArg, ENNReal.mul_le_iff_le_inv, cast, Dilation.edist_eq, LE.le, ENNReal.coe_ne_zero, Iff.mp, congrFun', EDist.edist, DFunLike.coe, ENNReal.coe_ne_top
-- 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
x y : α
hr : ratio f ≠ 0
⊢ edist x y ≤ (↑(ratio f)⁻¹ : ℝ≥0∞) * edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)

Tactic:
exact mod_cast
    (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge

Premises used: Iff.mpr, Eq.ge, ENNReal.mul_le_iff_le_inv, Dilation.edist_eq, ENNReal.coe_ne_zero, Iff.mp, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace β
α : Type u_5
inst_1 : EMetricSpace α
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
⊢ Injective.{u_5 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
(antilipschitz f).injective

Premises used: Dilation.antilipschitz, AntilipschitzWith.injective
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α_1
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : FunLike F α_1 β
inst_4 : DilationClass F α_1 β
f : F
α : Type u_5
inst_5 : PseudoEMetricSpace α
x y : α
⊢ edist (id x) (id y) = (↑1 : ℝ≥0∞) * edist x y

Tactic:
simp only [id, ENNReal.coe_one, one_mul]

Premises used: id, ENNReal.coe_one, one_mul
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ Eq (α := (a : α) → α) (⇑(Dilation.id α) : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pos : ∀ (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞), ratio (F := α →ᵈ α) (Dilation.id α) = 1
neg : ∀ (h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (F := α →ᵈ α) (Dilation.id α) = 1
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1

Tactic:
by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
pos :
  (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞ then 1
    else
      Exists.choose (p := fun (r : ℝ≥0) ↦
        r ≠ 0 ∧
          ∀ (x y : α),
            edist (α := α) ((Dilation.id α : (a : α) → α) x : α) ((Dilation.id α : (a : α) → α) y : α) =
              (↑r : ℝ≥0∞) * edist x y)
        ⋯) =
    1
pos₁ pos₂ : Eq (α := ℝ≥0) 1 1
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1

Tactic:
rw [ratio, if_pos h]

Premises used: if_pos, Dilation.ratio
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞
neg : ∀ (x y : α) (hne : edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (F := α →ᵈ α) (Dilation.id α) = 1
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1

Tactic:
rcases h with ⟨x, y, hne⟩
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1

Tactic:
(ratio_unique hne.1 hne.2 ?_).symm

Premises used: Dilation.ratio_unique, And.right, And.left, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ∞
neg :
  edist (α := α) ((Dilation.id α : (a : α) → α) x : α) ((Dilation.id α : (a : α) → α) y : α) = (↑1 : ℝ≥0∞) * edist x y
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1

Tactic:
refine (ratio_unique hne.1 hne.2 ?_).symm

Premises used: Dilation.ratio_unique, And.right, And.left, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ edist (α := α) ((Dilation.id α : (a : α) → α) x : α) ((Dilation.id α : (a : α) → α) y : α) = (↑1 : ℝ≥0∞) * edist x y

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : FunLike F α β
inst_4 : DilationClass F α β
f_1 : F
g : β →ᵈ γ
f : α →ᵈ β
x y : α
simp_rw :
  edist.{u_3} (α := γ) ((g : (a : β) → γ) ((f : (a : α) → β) x : β) : γ)
      ((g : (a : β) → γ) ((f : (a : α) → β) y : β) : γ) =
    (↑(ratio g * ratio f) : ℝ≥0∞) * edist x y
simp_rw₁ : (↑(ratio g) : ℝ≥0∞) * ((↑(ratio f) : ℝ≥0∞) * edist x y) = (↑(ratio g * ratio f) : ℝ≥0∞) * edist x y
simp_rw₂ :
  (↑(ratio g) : ℝ≥0∞) * ((↑(ratio f) : ℝ≥0∞) * edist x y) = (↑(ratio g) : ℝ≥0∞) * (↑(ratio f) : ℝ≥0∞) * edist x y
⊢ edist.{u_3} (α := γ) (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β) x)
      (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β) y) =
    (↑(ratio g * ratio f) : ℝ≥0∞) * edist x y

Tactic:
simp_rw [Function.comp, edist_eq, ENNReal.coe_mul, mul_assoc]

Premises used: mul_assoc, Function.comp, Dilation.edist_eq, ENNReal.coe_mul
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
δ : Type u_5
inst_3 : PseudoEMetricSpace δ
f : α →ᵈ β
g : β →ᵈ γ
h : γ →ᵈ δ
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
rfl

Premises used: Dilation.comp, rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
⊢ Eq (α := (a : α) → γ) (⇑(g.comp f) : (a : α) → γ)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := β) (⇑g : (a : β) → γ) (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: rfl