awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ toEquiv = toEquiv_1

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- 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)
⊢ toEquiv = toEquiv_1

Tactic:
exact DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ Eq (α := (a : X) → Y) (⇑e.toEquiv : (a : X) → Y) (⇑e : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e e' : X ≃ᵈ Y
h : ∀ (x : X), Eq.{u_2 + 1} (α := Y) ((e : (a : X) → Y) x : Y) ((e' : (a : X) → Y) x : Y)
⊢ e = e'

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- 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
e : X ≃ᵈ Y
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : Y), edist (e.symm.toFun x) (e.symm.toFun y) = (↑r : ℝ≥0∞) * edist x y

Tactic:
⟨(ratio e)⁻¹, inv_ne_zero <| ratio_ne_zero e, e.surjective.forall₂.2 fun x y ↦ ?_⟩

Premises used: Iff.mpr, DilationEquiv.toEquiv, Dilation.ratio, Inv.inv, And.intro, Exists.intro, inv_ne_zero, Dilation.ratio_ne_zero, Equiv.surjective, Function.Surjective.forall₂
-- 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
e : X ≃ᵈ Y
refine :
  ∀ (x y : X),
    edist (e.symm.toFun ((e.toEquiv : (a : X) → Y) x)) (e.symm.toFun ((e.toEquiv : (a : X) → Y) y)) =
      (↑(ratio e)⁻¹ : ℝ≥0∞) * edist.{u_2} (α := Y) ((e.toEquiv : (a : X) → Y) x : Y) ((e.toEquiv : (a : X) → Y) y : Y)
⊢ ∃ (r : ℝ≥0), r ≠ 0 ∧ ∀ (x y : Y), edist (e.symm.toFun x) (e.symm.toFun y) = (↑r : ℝ≥0∞) * edist x y

Tactic:
refine ⟨(ratio e)⁻¹, inv_ne_zero <| ratio_ne_zero e, e.surjective.forall₂.2 fun x y ↦ ?_⟩
-- 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
e : X ≃ᵈ Y
x y : X
simp_rw : edist x y = (↑(ratio e)⁻¹ : ℝ≥0∞) * ((↑(ratio e) : ℝ≥0∞) * edist x y)
⊢ edist (e.symm.toFun ((e.toEquiv : (a : X) → Y) x)) (e.symm.toFun ((e.toEquiv : (a : X) → Y) y)) =
    (↑(ratio e)⁻¹ : ℝ≥0∞) * edist.{u_2} (α := Y) ((e.toEquiv : (a : X) → Y) x : Y) ((e.toEquiv : (a : X) → Y) y : Y)

Tactic:
simp_rw [Equiv.toFun_as_coe, Equiv.symm_apply_apply, coe_toEquiv, edist_eq]

Premises used: Equiv.symm_apply_apply, Equiv.toFun_as_coe, DilationEquiv.coe_toEquiv, Dilation.edist_eq
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: Equiv.symm, DilationEquiv.symm, rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
⊢ Bijective (α := X ≃ᵈ Y) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, DilationEquiv.symm_symm
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
x : Y
⊢ (e : (a : X) → Y) ((e.symm : (a : Y) → X) x : X) = x

Tactic:
e.right_inv x

Premises used: Equiv.right_inv, DilationEquiv.toEquiv
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
x : X
⊢ (e.symm : (a : Y) → X) ((e : (a : X) → Y) x : Y) = x

Tactic:
e.left_inv x

Premises used: DilationEquiv.toEquiv, Equiv.left_inv
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ ratio e.toDilation = ratio e

Tactic:
rfl

Premises used: Dilation.ratio, rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X_1 : Type u_1
Y : Type u_2
Z : Type u_3
inst : PseudoEMetricSpace X_1
inst_1 : PseudoEMetricSpace Y
inst_2 : PseudoEMetricSpace Z
X : Type u_4
inst_3 : PseudoEMetricSpace X
x x_1 : X
⊢ edist ((Equiv.refl X).toFun x) ((Equiv.refl X).toFun x_1) = (↑1 : ℝ≥0∞) * edist x x_1

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
⊢ Eq (α := X ≃ᵈ X) (symm (refl X)) (refl X)

Tactic:
rfl

Premises used: DilationEquiv.refl, Equiv.symm, DilationEquiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
⊢ ratio (F := X ≃ᵈ X) (refl X) = 1

Tactic:
Dilation.ratio_id

Premises used: Dilation.ratio_id, Dilation.ratio, Dilation.id, DilationEquiv.refl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ trans (refl X) e = e

Tactic:
rfl

Premises used: DilationEquiv.trans, Equiv.trans, rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ e.trans (refl Y) = e

Tactic:
rfl

Premises used: DilationEquiv.trans, Equiv.trans, rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ e.symm.trans e = refl Y

Tactic:
DilationEquiv.ext e.apply_symm_apply

Premises used: DilationEquiv.apply_symm_apply, DilationEquiv.ext
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ e.trans e.symm = refl X

Tactic:
DilationEquiv.ext e.symm_apply_apply

Premises used: DilationEquiv.symm_apply_apply, DilationEquiv.ext
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := X) (β := Y) (⇑e : (a : X) → Y)

Tactic:
e.1.surjective

Premises used: DilationEquiv.toEquiv, Equiv.surjective
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ Bijective.{u_1 + 1, u_2 + 1} (α := X) (β := Y) (⇑e : (a : X) → Y)

Tactic:
e.1.bijective

Premises used: Equiv.bijective, DilationEquiv.toEquiv
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ Injective.{u_1 + 1, u_2 + 1} (α := X) (β := Y) (⇑e : (a : X) → Y)

Tactic:
e.1.injective

Premises used: DilationEquiv.toEquiv, Equiv.injective
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
pos : ∀ (hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞), ratio (e.trans e') = ratio e * ratio e'
neg : ∀ (hX : ∃ (x : X) (y : X), edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (e.trans e') = ratio e * ratio e'
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
by_cases! hX : ∀ x y : X, edist x y = 0 ∨ edist x y = ∞
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
⊢ edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = 0 ∨
    edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = ∞

Tactic:
(hX x y).imp (fun h ↦ ?_) fun h ↦ ?_

Premises used: Or.imp
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
refine_1 : ∀ (h : edist x y = 0), edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = 0
refine_2 : ∀ (h : edist x y = ∞), edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = ∞
⊢ edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = 0 ∨
    edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = ∞

Tactic:
refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_

Premises used: Or.imp
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = 0
⊢ edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = 0

Tactic:
simp [*, Dilation.ratio_ne_zero]

Premises used: Dilation.ratio_ne_zero
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
x y : X
h : edist x y = ∞
⊢ edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = ∞

Tactic:
simp [*, Dilation.ratio_ne_zero]

Premises used: Dilation.ratio_ne_zero
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
⊢ ∀ (x y : Y), edist x y = 0 ∨ edist x y = ∞

Tactic:
have hY : ∀ x y : Y, edist x y = 0 ∨ edist x y = ∞ := e.surjective.forall₂.2 fun x y ↦ by
      refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_ <;> simp [*, Dilation.ratio_ne_zero]
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞
hY : ∀ (x y : Y), edist x y = 0 ∨ edist x y = ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
simp [Dilation.ratio_of_trivial, *]

Premises used: Dilation.ratio_of_trivial
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∃ (x : X) (y : X), edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
(Dilation.ratio_comp' (g := e'.toDilation) (f := e.toDilation) hX).trans (mul_comm _ _)

Premises used: Dilation.comp, DilationEquiv.trans, Dilation.ratio, mul_comm, Dilation.ratio_comp', Eq.trans
-- 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
e : X ≃ᵈ Y
e' : Y ≃ᵈ Z
hX : ∃ (x : X) (y : X), edist x y ≠ 0 ∧ edist x y ≠ ∞
⊢ ratio (e.trans e') = ratio e * ratio e'

Tactic:
exact (Dilation.ratio_comp' (g := e'.toDilation) (f := e.toDilation) hX).trans (mul_comm _ _)

Premises used: mul_comm, Dilation.ratio_comp', Eq.trans
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
rw : ratio (e.symm.trans e) = 1
rw₁ : ratio (F := Y ≃ᵈ Y) (refl Y) = 1
rw₂ rw₃ : Eq (α := ℝ≥0) 1 1
⊢ ratio e.symm * ratio e = 1

Tactic:
rw [← ratio_trans, symm_trans_self, ratio_refl]

Premises used: DilationEquiv.ratio_trans, DilationEquiv.ratio_refl, DilationEquiv.symm_trans_self
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e e' : X ≃ᵈ X
⊢ e * e' = e'.trans e

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
⊢ Eq (α := X ≃ᵈ X) 1 (refl X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e : X ≃ᵈ X
⊢ e⁻¹ = e.symm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e e' : X ≃ᵈ X
⊢ Eq (α := (a : X) → X) (⇑(e * e') : (a : X) → X) (comp (β := X) (⇑e : (a : X) → X) (⇑e' : (a : X) → X))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e : X ≃ᵈ X
⊢ Eq (α := (a : X) → X) (⇑e⁻¹ : (a : X) → X) (⇑e.symm : (a : X) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e : X ≃ᵈ X
⊢ ratio e⁻¹ = (ratio e)⁻¹

Tactic:
ratio_symm e

Premises used: DilationEquiv.ratio_symm
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ ratio (e ^ n) = ratio e ^ n

Tactic:
ratioHom.map_pow _ _

Premises used: DilationEquiv.ratioHom, Dilation.ratio, ite, MonoidHom.map_pow
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℤ
⊢ ratio (e ^ n) = ratio e ^ n

Tactic:
ratioHom.map_zpow _ _

Premises used: DilationEquiv.ratioHom, Dilation.ratio, MonoidHom.map_zpow, ite
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
rw :
  Eq (α := (a : X) → X) (⇑((toPerm : (a : X ≃ᵈ X) → Equiv.Perm X) e : Equiv.Perm X) : (a : X) → X)^[n]
    (⇑e : (a : X) → X)^[n]
⊢ Eq (α := (a : X) → X) (⇑(e ^ n) : (a : X) → X) (⇑e : (a : X) → X)^[n]

Tactic:
rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow]

Premises used: DilationEquiv.toPerm_apply, DilationEquiv.coe_toEquiv, map_pow, Equiv.Perm.coe_pow
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ Eq (α := (a : X) → X) (⇑((toPerm : (a : X ≃ᵈ X) → Equiv.Perm X) e : Equiv.Perm X) : (a : X) → X)^[n]
    (⇑e : (a : X) → X)^[n]

Tactic:
rfl
-- 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
e : X ≃ᵢ Y
⊢ ∀ (x y : X), edist (e.toFun x) (e.toFun y) = (↑1 : ℝ≥0∞) * edist x y

Tactic:
simpa using e.isometry

Premises used: IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵢ Y
x : X
⊢ Eq.{u_2 + 1} (α := Y) ((e.toDilationEquiv : (a : X) → Y) x : Y) ((e : (a : X) → Y) x : Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ e.symm.toDilationEquiv = e.toDilationEquiv.symm

Tactic:
rfl

Premises used: IsometryEquiv.toDilationEquiv, Equiv.symm, DilationEquiv.symm, rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ Eq (α := (a : X) → Y) (⇑e.toDilationEquiv : (a : X) → Y) (⇑e : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ Eq (α := (a : Y) → X) (⇑e.toDilationEquiv.symm : (a : Y) → X) (⇑e.symm : (a : Y) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ e.toDilationEquiv.toDilation = Isometry.toDilation (⇑e : (a : X) → Y) ⋯

Tactic:
rfl

Premises used: Isometry.toDilation, rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵢ Y
rw : ratio e.toDilationEquiv.toDilation = 1
rw₁ : ratio (Isometry.toDilation (⇑e : (a : X) → Y) ⋯) = 1
rw₂ rw₃ : Eq (α := ℝ≥0) 1 1
⊢ ratio e.toDilationEquiv = 1

Tactic:
rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]

Premises used: Isometry.toDilation_ratio, DilationEquiv.ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ e.symm.toHomeomorph = e.toHomeomorph.symm

Tactic:
rfl

Premises used: DilationEquiv.toHomeomorph, Homeomorph.symm, Equiv.symm, rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ Eq (α := (a : X) → Y) (⇑e.toHomeomorph : (a : X) → Y) (⇑e : (a : X) → Y)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ Eq (α := (a : Y) → X) (⇑e.toHomeomorph.symm : (a : Y) → X) (⇑e.symm : (a : Y) → X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.DilationEquiv
Goal:
X : Type u_1
Y : Type u_2
F : Type u_3
inst : PseudoMetricSpace X
inst_1 : PseudoMetricSpace Y
inst_2 : EquivLike F X Y
inst_3 : DilationEquivClass F X Y
e : F
rw : map.{u_1, u_2} (α := X) (⇑e : (a : X) → Y) (comap (⇑e : (a : X) → Y) (cobounded Y)) = cobounded Y
rw₁ rw₂ : cobounded Y = cobounded Y
⊢ map (⇑e : (a : X) → Y) (cobounded X) = cobounded Y

Tactic:
rw [← Dilation.comap_cobounded e, map_comap_of_surjective (EquivLike.surjective e)]

Premises used: Filter.map_comap_of_surjective, Dilation.comap_cobounded, EquivLike.surjective
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

Tactic:
uniformity_basis_dist.equicontinuousAt_iff_right

Premises used: Set.Mem, Filter.HasBasis.equicontinuousAt_iff_right, Metric.uniformity_basis_dist
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
F : ι → β → α
x₀ : β
⊢ EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x : β), dist x x₀ < δ → ∀ (i : ι), dist (F i x₀) (F i x) < ε

Tactic:
nhds_basis_ball.equicontinuousAt_iff uniformity_basis_dist

Premises used: Set.Mem, Metric.uniformity_basis_dist, Metric.ball, Filter.HasBasis.equicontinuousAt_iff, Metric.nhds_basis_ball
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
rw :
  (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) ↔
    ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
⊢ EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε

Tactic:
rw [equicontinuousAt_iff_pair]

Premises used: equicontinuousAt_iff_pair
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
mp :
  (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) →
    ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
mpr :
  (∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε) →
    ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ (∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U) ↔
    ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε

Tactic:
constructor
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
ε : ℝ
hε : ε > 0
⊢ ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε

Tactic:
H _ (dist_mem_uniformity hε)

Premises used: Set.Mem, Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
ε : ℝ
hε : ε > 0
⊢ ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε

Tactic:
exact H _ (dist_mem_uniformity hε)

Premises used: Metric.dist_mem_uniformity
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
mpr :
  ∀ (ε : ℝ) (hε : ε > 0) (hεU : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ U),
    ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩

Premises used: Metric.mem_uniformity_dist, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ U
⊢ ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
Exists.imp (fun V => And.imp_right fun h => ?_) (H _ hε)

Premises used: Exists.imp, And.imp_right
-- Module: Mathlib.Topology.MetricSpace.Equicontinuity
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
H : ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
U : Set (α × α)
hU : U ∈ 𝓤 α
ε : ℝ
hε : ε > 0
hεU : ∀ ⦃a b : α⦄, dist a b < ε → (a, b) ∈ U
mpr :
  ∀ (V : Set β) (h : ∀ x ∈ V, ∀ x' ∈ V, ∀ (i : ι), dist (F i x) (F i x') < ε),
    ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
⊢ ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U

Tactic:
refine Exists.imp (fun V => And.imp_right fun h => ?_) (H _ hε)

Premises used: Exists.imp, And.imp_right