awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : α →ᵈ β
x : α
⊢ Eq.{u_3 + 1} (α := γ) ((g.comp f : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f : (a : α) → β) x : β) : γ)

Tactic:
rfl

Premises used: 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 : α →ᵈ β
hne : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞
rcases : ∀ (x y : α) (hα : edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (g.comp f) = ratio g * ratio f
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
rcases hne with ⟨x, y, hα⟩
-- 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 : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ (↑(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
-- 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 : α →ᵈ β
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)) : ℝ≥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

Premises used: mul_assoc, Dilation.coe_comp, Function.comp, Dilation.edist_eq, ENNReal.mul_left_inj, And.right, And.left
-- 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 : α →ᵈ β
x y : α
hα : edist x y ≠ 0 ∧ edist x y ≠ ∞
hgf : (↑(ratio (g.comp f)) : ℝ≥0∞) = (↑(ratio g) : ℝ≥0∞) * (↑(ratio f) : ℝ≥0∞)
rwa : (↑(ratio (g.comp f)) : ℝ≥0∞) = (↑(ratio g * ratio f) : ℝ≥0∞)
rwa₁ rwa₂ rwa₃ rwa₄ : (↑(ratio (g.comp f)) : ℝ≥0∞) = (↑(ratio g) : ℝ≥0∞) * (↑(ratio f) : ℝ≥0∞)
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
rwa [← ENNReal.coe_inj, ENNReal.coe_mul]

Premises used: ENNReal.coe_inj, ENNReal.coe_mul
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α →ᵈ β
⊢ f.comp (Dilation.id α) = 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 : α →ᵈ β
⊢ comp (Dilation.id β) f = f

Tactic:
ext fun _ => rfl

Premises used: Dilation.ext, rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ Eq (α := α →ᵈ α) 1 (Dilation.id α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f g : α →ᵈ α
⊢ f * g = f.comp g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ Eq.{u_1 + 1} (α := (a : α) → α) (⇑1 : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f g : α →ᵈ α
⊢ Eq (α := (a : α) → α) (⇑(f * g) : (a : α) → α) (Function.comp (β := α) (⇑f : (a : α) → α) (⇑g : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
⊢ ratio (F := α →ᵈ α) 1 = 1

Tactic:
ratio_id

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

Tactic:
by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f g : α →ᵈ α
h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
simp [ratio_of_trivial, h]

Premises used: Dilation.ratio_of_trivial
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f g : α →ᵈ α
h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
ratio_comp' h

Premises used: Dilation.ratio_comp'
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f g : α →ᵈ α
h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (f * g) = ratio f * ratio g

Tactic:
exact ratio_comp' h

Premises used: Dilation.ratio_comp'
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f : α →ᵈ α
n : ℕ
⊢ ratio (f ^ n) = ratio f ^ n

Tactic:
ratioHom.map_pow _ _

Premises used: Dilation.ratioHom, Dilation.ratio, ite, MonoidHom.map_pow
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g₁ g₂ : β →ᵈ γ
f : α →ᵈ β
hf : Surjective.{u_1 + 1, u_2 + 1} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ g₁.comp f = g₂.comp f ↔ g₁ = g₂

Tactic:
⟨fun h => Dilation.ext <| hf.forall.2 (Dilation.ext_iff.1 h), fun h => h ▸ rfl⟩

Premises used: Iff.mpr, Function.Surjective.forall, Eq.rec, Dilation.ext, Iff.intro, Iff.mp, Dilation.ext_iff, 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₁ f₂ : α →ᵈ β
hg : Injective.{u_2 + 1, u_3 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_3 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₁ : Eq.{u_3 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)

Tactic:
rw [← comp_apply, h, comp_apply]

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

Tactic:
(antilipschitz f).isUniformInducing (lipschitz f).uniformContinuous

Premises used: Dilation.antilipschitz, AntilipschitzWith.isUniformInducing, LipschitzWith.uniformContinuous, Dilation.lipschitz
-- 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
ι : Type u_5
g : ι → α
a : Filter ι
b : α
⊢ Filter.Tendsto g a (𝓝 b) ↔
    Filter.Tendsto.{u_5, u_2} (β := β) ((⇑f : (a : α) → β) ∘ g : ι → β) a (𝓝 ((f : (a : α) → β) b) : Filter β)

Tactic:
(Dilation.isUniformInducing f).isInducing.tendsto_nhds_iff

Premises used: IsUniformInducing.isInducing, Topology.IsInducing.tendsto_nhds_iff, Dilation.isUniformInducing
-- 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
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : α) → β)

Tactic:
(lipschitz f).continuous

Premises used: LipschitzWith.continuous, Dilation.lipschitz
-- 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
s : Set α
⊢ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s) = (↑(ratio f) : ℝ≥0∞) * ediam s

Tactic:
((lipschitz f).ediam_image_le s).antisymm ?_

Premises used: LipschitzWith.ediam_image_le, LE.le.antisymm, Dilation.lipschitz
-- 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
s : Set α
refine : (↑(ratio f) : ℝ≥0∞) * ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)
⊢ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s) = (↑(ratio f) : ℝ≥0∞) * ediam s

Tactic:
refine ((lipschitz f).ediam_image_le s).antisymm ?_

Premises used: LipschitzWith.ediam_image_le, LE.le.antisymm, Dilation.lipschitz
-- 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
s : Set α
h : ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s) / (↑(ratio f) : ℝ≥0∞)
⊢ (↑(ratio f) : ℝ≥0∞) * ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)

Tactic:
apply ENNReal.mul_le_of_le_div'

Premises used: ENNReal.mul_le_of_le_div'
-- 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
s : Set α
h : ediam s ≤ (↑(ratio f)⁻¹ : ℝ≥0∞) * ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)
h₁ : ratio f ≠ 0
⊢ ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s) / (↑(ratio f) : ℝ≥0∞)

Tactic:
rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]

Premises used: ENNReal.coe_inv, div_eq_mul_inv, mul_comm
-- 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
s : Set α
⊢ ediam s ≤ (↑(ratio f)⁻¹ : ℝ≥0∞) * ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)

Tactic:
(antilipschitz f).le_mul_ediam_image s

Premises used: Dilation.antilipschitz, AntilipschitzWith.le_mul_ediam_image
-- 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
s : Set α
⊢ ratio f ≠ 0

Tactic:
ratio_ne_zero f

Premises used: Dilation.ratio_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
s : Set α
⊢ ediam s ≤ (↑(ratio f)⁻¹ : ℝ≥0∞) * ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)

Tactic:
exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]

Premises used: Dilation.antilipschitz, Dilation.ratio_ne_zero, AntilipschitzWith.le_mul_ediam_image
-- 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
rw :
  ediam.{u_2} (X := β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) univ) =
    (↑(ratio f) : ℝ≥0∞) * ediam.{u_1} (X := α) univ
⊢ ediam.{u_2} (X := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) =
    (↑(ratio f) : ℝ≥0∞) * ediam.{u_1} (X := α) univ

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- 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
⊢ ediam.{u_2} (X := β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) univ) =
    (↑(ratio f) : ℝ≥0∞) * ediam.{u_1} (X := α) univ

Tactic:
ediam_image f univ

Premises used: Set.univ, Dilation.ediam_image
-- 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
⊢ ediam.{u_2} (X := β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) univ) =
    (↑(ratio f) : ℝ≥0∞) * ediam.{u_1} (X := α) univ

Tactic:
exact ediam_image f univ

Premises used: Set.univ, Dilation.ediam_image
-- 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 : α
r : ℝ≥0∞
y : α
hy : edist y x < r
rw : (↑(ratio f) : ℝ≥0∞) * edist y x < (↑(ratio f) : ℝ≥0∞) * r
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (eball ((f : (a : α) → β) x) ((↑(ratio f) : ℝ≥0∞) * r) : Set β)
    ((f : (a : α) → β) y : β)

Tactic:
rw [Metric.mem_eball, edist_eq f y x]

Premises used: Dilation.edist_eq, Metric.mem_eball
-- 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 : α
r : ℝ≥0∞
y : α
hy : edist y x < r
h0 : (↑(ratio f) : ℝ≥0∞) ≠ 0
hinf : (↑(ratio f) : ℝ≥0∞) ≠ ∞
⊢ (↑(ratio f) : ℝ≥0∞) * edist y x < (↑(ratio f) : ℝ≥0∞) * r

Tactic:
gcongr
-- 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 : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ (↑(ratio f) : ℝ≥0∞) ≠ 0

Tactic:
simp [ratio_ne_zero, *]

Premises used: Dilation.ratio_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
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ (↑(ratio f) : ℝ≥0∞) ≠ ∞

Tactic:
simp [ratio_ne_zero, *]

Premises used: Dilation.ratio_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
x : α
r' : ℝ≥0∞
y : α
hy : y ∈ closedEBall x r'
bc : edist y x ≤ r'
⊢ (↑(ratio f) : ℝ≥0∞) * edist y x ≤ (↑(ratio f) : ℝ≥0∞) * r'

Tactic:
gcongr
-- 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 : α
r' : ℝ≥0∞
y : α
hy : y ∈ closedEBall x r'
⊢ edist y x ≤ r'

Tactic:
hy

Premises used: Set.Mem, setOf, Metric.closedEBall
-- 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 : α
r' : ℝ≥0∞
y : α
hy : y ∈ closedEBall x r'
⊢ edist y x ≤ r'

Tactic:
exact hy
-- 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
γ : Type u_5
inst_4 : TopologicalSpace γ
g : γ → α
s : Set γ
⊢ ContinuousOn.{u_5, u_2} (Y := β) ((⇑f : (a : α) → β) ∘ g) s ↔ ContinuousOn g s

Tactic:
(Dilation.isUniformInducing f).isInducing.continuousOn_iff.symm

Premises used: IsUniformInducing.isInducing, Dilation.isUniformInducing, Topology.IsInducing.continuousOn_iff, Iff.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
γ : Type u_5
inst_4 : TopologicalSpace γ
g : γ → α
⊢ Continuous[inst_4, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑f : (a : α) → β) ∘ g) ↔
    Continuous[inst_4, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] g

Tactic:
(Dilation.isUniformInducing f).isInducing.continuous_iff.symm

Premises used: Topology.IsInducing.continuous_iff, IsUniformInducing.isInducing, Dilation.isUniformInducing, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : EMetricSpace α
inst_1 : FunLike F α β
inst_2 : PseudoEMetricSpace β
inst_3 : DilationClass F α β
f : F
⊢ IsUniformEmbedding.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
(antilipschitz f).isUniformEmbedding (lipschitz f).uniformContinuous

Premises used: Dilation.antilipschitz, AntilipschitzWith.isUniformEmbedding, LipschitzWith.uniformContinuous, Dilation.lipschitz
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : EMetricSpace α
inst_1 : FunLike F α β
inst_2 : PseudoEMetricSpace β
inst_3 : DilationClass F α β
f : F
⊢ IsEmbedding.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
(Dilation.isUniformEmbedding f).isEmbedding

Premises used: Dilation.isUniformEmbedding, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : EMetricSpace α
inst_1 : FunLike F α β
inst_2 : CompleteSpace α
inst_3 : EMetricSpace β
inst_4 : DilationClass F α β
f : F
⊢ IsClosedEmbedding.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β)

Tactic:
(antilipschitz f).isClosedEmbedding (lipschitz f).uniformContinuous

Premises used: Dilation.antilipschitz, AntilipschitzWith.isClosedEmbedding, LipschitzWith.uniformContinuous, Dilation.lipschitz
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MetricSpace α
inst_1 : Nontrivial α
inst_2 : PseudoEMetricSpace β
inst_3 : PseudoEMetricSpace γ
g : β →ᵈ γ
f : α →ᵈ β
⊢ ratio (g.comp f) = ratio g * ratio f

Tactic:
ratio_comp' <|
    let ⟨x, y, hne⟩ := exists_pair_ne α; ⟨x, y, mt edist_eq_zero.1 hne, edist_ne_top _ _⟩

Premises used: Exists, mt, _private.0.Dilation.ratio_comp.match_1, Ne, And, edist_ne_top, And.intro, Exists.intro, Iff.mp, Dilation.ratio_comp', EDist.edist, Top.top, OfNat.ofNat, edist_eq_zero, exists_pair_ne
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
s : Set α
⊢ diam.{u_2} (α := β) ((⇑f : (a : α) → β) '' s) = (↑(ratio f) : ℝ) * diam s

Tactic:
simp [diam, ediam_image, ENNReal.toReal_mul]

Premises used: ENNReal.toReal_mul, Metric.diam, Dilation.ediam_image
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
rw :
  diam.{u_2} (α := β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) univ) = (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ
rw₁ rw₂ : (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ = (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ
⊢ diam.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) = (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ

Tactic:
rw [← image_univ, diam_image]

Premises used: Set.image_univ, Dilation.diam_image
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
ha : 0 < (↑(ratio f) : ℝ)
hbc : dist y x < r'
⊢ (↑(ratio f) : ℝ) * dist y x < (↑(ratio f) : ℝ) * r'

Tactic:
gcongr
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ 0 < (↑(ratio f) : ℝ)

Tactic:
ratio_pos _

Premises used: Dilation.ratio_pos, NNReal.toReal
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ dist y x < r'

Tactic:
hy

Premises used: Set.Mem, Metric.ball
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ 0 < (↑(ratio f) : ℝ)

Tactic:
exacts [ratio_pos _, hy]

Premises used: Dilation.ratio_pos
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ
⊢ MapsTo.{u_1, u_2} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (sphere x r')
    (sphere ((f : (a : α) → β) x) ((↑(ratio f) : ℝ) * r') : Set β)

Tactic:
fun y hy => Metric.mem_sphere.mp hy ▸ dist_eq f y x

Premises used: Eq.rec, Metric.mem_sphere, Set.MapsTo, Iff.mp, Dilation.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ
⊢ MapsTo.{u_1, u_2} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (closedBall x r')
    (closedBall ((f : (a : α) → β) x) ((↑(ratio f) : ℝ) * r') : Set β)

Tactic:
fun y hy => (dist_eq f y x).trans_le <| mul_le_mul_of_nonneg_left hy (NNReal.coe_nonneg _)

Premises used: Set.Mem, setOf, Eq.trans_le, Dilation.ratio, Set.MapsTo, NNReal.coe_nonneg, Dilation.dist_eq, Metric.closedBall, mul_le_mul_of_nonneg_left
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
⊢ Filter.Tendsto (⇑f : (a : α) → β) (cobounded α) (cobounded β)

Tactic:
(Dilation.antilipschitz f).tendsto_cobounded

Premises used: AntilipschitzWith.tendsto_cobounded, Dilation.antilipschitz
-- Module: Mathlib.Topology.MetricSpace.Dilation
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
⊢ Filter.comap (⇑f : (a : α) → β) (cobounded β) = cobounded α

Tactic:
le_antisymm (lipschitz f).comap_cobounded_le (tendsto_cobounded f).le_comap

Premises used: Filter.Tendsto.le_comap, LipschitzWith.comap_cobounded_le, le_antisymm, Dilation.tendsto_cobounded, Dilation.lipschitz
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
F : Type u_1
X : Type u_2
Y : Type u_3
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : EquivLike F X Y
inst_3 : DilationEquivClass F X Y
⊢ DilationClass F X Y

Tactic:
{ (inferInstance : FunLike F X Y), ‹DilationEquivClass F X Y› with }

Premises used: DilationClass.mk, inferInstance, DilationEquivClass.edist_eq'
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : PseudoEMetricSpace Z
toEquiv : X ≃ Y
edist_eq' : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv.toFun x) (toEquiv.toFun y) = (↑r : ℝ≥0∞) * edist x y
toEquiv_1 : X ≃ Y
edist_eq'_1 : ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv_1.toFun x) (toEquiv_1.toFun y) = (↑r : ℝ≥0∞) * edist x y
h :
  Eq (α := X → Y) (⇑{ toEquiv := toEquiv, edist_eq' := edist_eq' : X ≃ᵈ Y }.toEquiv : (a : X) → Y)
    (⇑{ toEquiv := toEquiv_1, edist_eq' := edist_eq'_1 : X ≃ᵈ Y }.toEquiv : (a : X) → Y)
e_toEquiv : toEquiv = toEquiv_1
⊢ { toEquiv := toEquiv, edist_eq' := edist_eq' : X ≃ᵈ Y } = { toEquiv := toEquiv_1, edist_eq' := edist_eq'_1 }

Tactic:
congr