awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y
have pos : ∀ (h : edist x y = 0),
  edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y
Tactic: rcases key x y with h | h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑1 : ℝ≥0∞) * edist x y
have pos₁ : ∀ (h : 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
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ edist x y ≠ 0
have rwa : (↑(nndist x y) : ℝ≥0∞) ≠ 0
Tactic: rwa [edist_nndist, ENNReal.coe_ne_zero]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ edist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
have rw : (↑(nndist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ≥0∞) = (↑r : ℝ≥0∞) * edist x y
Tactic: rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ edist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
have rw₁ : (↑(nndist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ≥0∞) =
  (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)
Tactic: rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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∞)
⊢ edist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
have rw₂ : (↑(r * nndist x y) : ℝ≥0∞) = (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)
Tactic: rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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∞)
⊢ edist.{u_6} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑r : ℝ≥0∞) * edist x y
have rw₃ : (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞) = (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)
Tactic: rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ (↑(nndist.{u_7} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ) = (↑(r * nndist x y) : ℝ)
have rw : dist.{u_7} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = (↑(r * nndist x y) : ℝ)
Tactic: rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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) : ℝ)
⊢ (↑(nndist.{u_7} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ) = (↑(r * nndist x y) : ℝ)
have rw₁ : (↑r : ℝ) * dist x y = (↑(r * nndist x y) : ℝ)
Tactic: rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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) : ℝ)
⊢ (↑(nndist.{u_7} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ) = (↑(r * nndist x y) : ℝ)
have rw₂ : (↑r : ℝ) * dist x y = (↑r : ℝ) * (↑(nndist x y) : ℝ)
Tactic: rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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) : ℝ)
⊢ (↑(nndist.{u_7} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)) : ℝ) = (↑(r * nndist x y) : ℝ)
have rw₃ : (↑r : ℝ) * dist x y = (↑r : ℝ) * dist x y
Tactic: rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
have 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
Tactic: rcases h with ⟨r, hne, h⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
have refine : ∀ (x y : α), edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
Tactic: refine ⟨r, hne, fun x y => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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 : α
⊢ edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
have rw : (↑(nndist (f x) (f y)) : ℝ≥0∞) = (↑r : ℝ≥0∞) * edist x y
Tactic: rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
have rw₁ : (↑(nndist (f x) (f y)) : ℝ≥0∞) = (↑r : ℝ≥0∞) * (↑(nndist x y) : ℝ≥0∞)
Tactic: rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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∞)
⊢ edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
have rw₂ : (↑(nndist (f x) (f y)) : ℝ≥0∞) = (↑(r * nndist x y) : ℝ≥0∞)
Tactic: rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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∞)
⊢ edist (f x) (f y) = (↑r : ℝ≥0∞) * edist x y
have rw₃ : (↑(r * nndist x y) : ℝ≥0∞) = (↑(r * nndist x y) : ℝ≥0∞)
Tactic: rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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 : α
⊢ (↑(nndist (f x) (f y)) : ℝ) = (↑(r * nndist x y) : ℝ)
have rw : dist (f x) (f y) = (↑(r * nndist x y) : ℝ)
Tactic: rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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) : ℝ)
⊢ (↑(nndist (f x) (f y)) : ℝ) = (↑(r * nndist x y) : ℝ)
have rw₁ : (↑r : ℝ) * dist x y = (↑(r * nndist x y) : ℝ)
Tactic: rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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) : ℝ)
⊢ (↑(nndist (f x) (f y)) : ℝ) = (↑(r * nndist x y) : ℝ)
have rw₂ : (↑r : ℝ) * dist x y = (↑r : ℝ) * (↑(nndist x y) : ℝ)
Tactic: rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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) : ℝ)
⊢ (↑(nndist (f x) (f y)) : ℝ) = (↑(r * nndist x y) : ℝ)
have rw₃ : (↑r : ℝ) * dist x y = (↑r : ℝ) * dist x y
Tactic: rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ ratio (Isometry.toDilation f hf) = 1
have pos : ∀ (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞), ratio (Isometry.toDilation f hf) = 1
Tactic: by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ ratio (Isometry.toDilation f hf) = 1
have neg : ∀ (h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (Isometry.toDilation f hf) = 1
Tactic: by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
have neg : ∀ (x y : α) (h₁ : edist x y ≠ 0) (h₂ : edist x y ≠ ∞), ratio (Isometry.toDilation f hf) = 1
Tactic: obtain ⟨x, y, h₁, h₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (hypothesis)
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 : α
⊢ edist x y ≤ (↑(ratio f)⁻¹ : ℝ≥0∞) * edist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β)
have hr : ratio f ≠ 0
Tactic: have hr : ratio f ≠ 0 := ratio_ne_zero f
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1
have pos : ∀ (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞), ratio (F := α →ᵈ α) (Dilation.id α) = 1
Tactic: by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
pos : ∀ (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞), ratio (F := α →ᵈ α) (Dilation.id α) = 1
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1
have neg : ∀ (h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (F := α →ᵈ α) (Dilation.id α) = 1
Tactic: by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1
have 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)
      sorry) =
  1
Tactic: rw [ratio, if_pos h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1
have pos₁ : Eq (α := ℝ≥0) 1 1
Tactic: rw [ratio, if_pos h]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1
have neg : ∀ (x y : α) (hne : edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (F := α →ᵈ α) (Dilation.id α) = 1
Tactic: rcases h with ⟨x, y, hne⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
x y : α
hne : edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (F := α →ᵈ α) (Dilation.id α) = 1
have neg : edist (α := α) ((Dilation.id α : (a : α) → α) x : α) ((Dilation.id α : (a : α) → α) y : α) = (↑1 : ℝ≥0∞) * edist x y
Tactic: refine (ratio_unique hne.1 hne.2 ?_).symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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 : α
⊢ 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
have simp_rw : edist.{u_3} (α := γ) ((g : (a : β) → γ) ((f : (a : α) → β) x : β) : γ)
    ((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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ 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
have simp_rw₁ : (↑(ratio g) : ℝ≥0∞) * ((↑(ratio f) : ℝ≥0∞) * edist x y) = (↑(ratio g * ratio f) : ℝ≥0∞) * edist x y
Tactic: simp_rw [Function.comp, edist_eq, ENNReal.coe_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
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
⊢ 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
have simp_rw₂ : (↑(ratio g) : ℝ≥0∞) * ((↑(ratio f) : ℝ≥0∞) * edist x y) = (↑(ratio g) : ℝ≥0∞) * (↑(ratio f) : ℝ≥0∞) * edist x y
Tactic: simp_rw [Function.comp, edist_eq, ENNReal.coe_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
hne : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (g.comp f) = ratio g * ratio f
have rcases : ∀ (x y : α) (hα : edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (g.comp f) = ratio g * ratio f
Tactic: rcases hne with ⟨x, y, hα⟩
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (g.comp f) = ratio g * ratio f
have hgf : (↑(ratio (g.comp f)) : ℝ≥0∞) * edist x y =
  edist.{u_3} (α := γ) ((g.comp f : (a : α) → γ) x : γ) ((g.comp f : (a : α) → γ) y : γ)
Tactic: have hgf := (edist_eq (g.comp f) x y).symm
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf :
  (↑(ratio (g.comp f)) : ℝ≥0∞) * edist x y =
    edist.{u_3} (α := γ) ((g.comp f : (a : α) → γ) x : γ) ((g.comp f : (a : α) → γ) y : γ)
⊢ ratio (g.comp f) = ratio g * ratio f
have hgf₁ : (↑(ratio (g.comp f)) : ℝ≥0∞) = (↑(ratio g) : ℝ≥0∞) * (↑(ratio f) : ℝ≥0∞)
Tactic: simp_rw [coe_comp, Function.comp, edist_eq, ← mul_assoc, ENNReal.mul_left_inj hα.1 hα.2]
    at hgf
Cleared hypotheses: hgf
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : (↑(ratio (g.comp f)) : ℝ≥0∞) = (↑(ratio g) : ℝ≥0∞) * (↑(ratio f) : ℝ≥0∞)
⊢ ratio (g.comp f) = ratio g * ratio f
have rwa : (↑(ratio (g.comp f)) : ℝ≥0∞) = (↑(ratio g * ratio f) : ℝ≥0∞)
Tactic: rwa [← ENNReal.coe_inj, ENNReal.coe_mul]