awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : IsometryClass F α β
f : F
x y : α
⊢ nndist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = nndist x y

Tactic:
(IsometryClass.isometry f).nndist_eq x y

Premises used: Isometry.nndist_eq, IsometryClass.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : IsometryClass F α β
f : F
s : Set α
⊢ Metric.diam.{v} (α := β) ((⇑f : (a : α) → β) '' s) = Metric.diam s

Tactic:
(IsometryClass.isometry f).diam_image s

Premises used: Isometry.diam_image, IsometryClass.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : IsometryClass F α β
f : F
⊢ Metric.diam.{v} (α := β) (range.{v, u + 1} (ι := α) (⇑f : (a : α) → β)) = Metric.diam.{u} (α := α) univ

Tactic:
(IsometryClass.isometry f).diam_range

Premises used: Isometry.diam_range, IsometryClass.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
e₁ e₂ : α ≃ᵢ β
⊢ e₁.toEquiv = e₂.toEquiv ↔ e₁ = e₂

Tactic:
toEquiv_injective.eq_iff

Premises used: Function.Injective.eq_iff, IsometryEquiv.toEquiv_injective
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
a : α
⊢ Eq.{v + 1} (α := β) ((h : (a : α) → β) a : β) ((h.toEquiv : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq (α := (a : α) → β) (⇑h.toEquiv : (a : α) → β) (⇑h : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
e : α ≃ β
h : Isometry e.toFun
⊢ Eq (α := (a : α) → β) (⇑{ toEquiv := e, isometry_toFun := h : α ≃ᵢ β } : (a : α) → β) (⇑e : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Isometry.{u, v} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
h.isometry_toFun

Premises used: IsometryEquiv.isometry_toFun
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Bijective.{u + 1, v + 1} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
h.toEquiv.bijective

Premises used: Equiv.bijective, IsometryEquiv.toEquiv
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Injective.{u + 1, v + 1} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
h.toEquiv.injective

Premises used: IsometryEquiv.toEquiv, Equiv.injective
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Surjective.{u + 1, v + 1} (α := α) (β := β) (⇑h : (a : α) → β)

Tactic:
h.toEquiv.surjective

Premises used: IsometryEquiv.toEquiv, Equiv.surjective
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x y : α
⊢ edist.{v} (α := β) ((h : (a : α) → β) x : β) ((h : (a : α) → β) y : β) = edist x y

Tactic:
h.isometry.edist_eq x y

Premises used: Isometry.edist_eq, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u_3
β : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x y : α
⊢ dist.{u_4} (α := β) ((h : (a : α) → β) x : β) ((h : (a : α) → β) y : β) = dist x y

Tactic:
h.isometry.dist_eq x y

Premises used: Isometry.dist_eq, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u_3
β : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x y : α
⊢ nndist.{u_4} (α := β) ((h : (a : α) → β) x : β) ((h : (a : α) → β) y : β) = nndist x y

Tactic:
h.isometry.nndist_eq x y

Premises used: Isometry.nndist_eq, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑h : (a : α) → β)

Tactic:
h.isometry.continuous

Premises used: Isometry.continuous, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set α
⊢ Metric.ediam.{v} (X := β) ((⇑h : (a : α) → β) '' s) = Metric.ediam s

Tactic:
h.isometry.ediam_image s

Premises used: Isometry.ediam_image, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h₁ h₂ : α ≃ᵢ β
H : ∀ (x : α), Eq.{v + 1} (α := β) ((h₁ : (a : α) → β) x : β) ((h₂ : (a : α) → β) x : β)
⊢ h₁ = h₂

Tactic:
DFunLike.ext _ _ H

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
h₁ : α ≃ᵢ β
h₂ : β ≃ᵢ γ
x : α
⊢ Eq.{w + 1} (α := γ) ((h₁.trans h₂ : (a : α) → γ) x : γ) ((h₂ : (a : β) → γ) ((h₁ : (a : α) → β) x : β) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq (α := (a : β) → α) (⇑h.symm : (a : β) → α) (⇑h.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ h.symm.symm = h

Tactic:
rfl

Premises used: IsometryEquiv.symm, Equiv.symm, rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
⊢ Bijective (α := α ≃ᵢ β) IsometryEquiv.symm

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

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, IsometryEquiv.symm_symm, And.intro, Exists.intro
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
y : β
⊢ (h : (a : α) → β) ((h.symm : (a : β) → α) y : α) = y

Tactic:
h.toEquiv.apply_symm_apply y

Premises used: Equiv.apply_symm_apply, IsometryEquiv.toEquiv
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
⊢ (h.symm : (a : β) → α) ((h : (a : α) → β) x : β) = x

Tactic:
h.toEquiv.symm_apply_apply x

Premises used: Equiv.symm_apply_apply, IsometryEquiv.toEquiv
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
y : β
⊢ (h.symm : (a : β) → α) y = x ↔ y = (h : (a : α) → β) x

Tactic:
h.toEquiv.symm_apply_eq

Premises used: IsometryEquiv.toEquiv, Equiv.symm_apply_eq
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
y : β
⊢ x = (h.symm : (a : β) → α) y ↔ (h : (a : α) → β) x = y

Tactic:
h.toEquiv.eq_symm_apply

Premises used: IsometryEquiv.toEquiv, Equiv.eq_symm_apply
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq.{u + 1} (α := α → α) (comp.{u + 1, v + 1, u + 1} (β := β) (⇑h.symm : (a : β) → α) (⇑h : (a : α) → β)) id

Tactic:
funext h.left_inv

Premises used: IsometryEquiv.toEquiv, funext, Equiv.left_inv
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq.{v + 1} (α := β → β) (comp.{v + 1, u + 1, v + 1} (β := α) (⇑h : (a : α) → β) (⇑h.symm : (a : β) → α)) id

Tactic:
funext h.right_inv

Premises used: Equiv.right_inv, IsometryEquiv.toEquiv, funext
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq.{v + 1} (α := Set β) (range.{v, u + 1} (ι := α) (⇑h : (a : α) → β)) univ

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq (α := (s : Set β) → Set α) (image (⇑h.symm : (a : β) → α)) (preimage (⇑h : (a : α) → β))

Tactic:
image_eq_preimage_of_inverse h.symm.toEquiv.left_inv h.symm.toEquiv.right_inv

Premises used: Equiv.right_inv, IsometryEquiv.toEquiv, IsometryEquiv.symm, Set.image_eq_preimage_of_inverse, Equiv.left_inv
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq (α := (s : Set α) → Set β) (preimage (⇑h.symm : (a : β) → α)) (image (⇑h : (a : α) → β))

Tactic:
(image_eq_preimage_of_inverse h.toEquiv.left_inv h.toEquiv.right_inv).symm

Premises used: Equiv.right_inv, IsometryEquiv.toEquiv, Set.image_eq_preimage_of_inverse, Eq.symm, Equiv.left_inv
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
h₁ : α ≃ᵢ β
h₂ : β ≃ᵢ γ
x : γ
⊢ Eq.{u + 1} (α := α) (((h₁.trans h₂).symm : (a : γ) → α) x : α)
    ((h₁.symm : (a : β) → α) ((h₂.symm : (a : γ) → β) x : β) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
rw : Metric.ediam.{u} (X := α) univ = Metric.ediam.{v} (X := β) (range.{v, u + 1} (ι := α) (⇑h : (a : α) → β))
rw₁ rw₂ : Metric.ediam.{u} (X := α) univ = Metric.ediam.{u} (X := α) univ
⊢ Metric.ediam.{u} (X := α) univ = Metric.ediam.{v} (X := β) univ

Tactic:
rw [← h.range_eq_univ, h.isometry.ediam_range]

Premises used: Isometry.ediam_range, IsometryEquiv.range_eq_univ, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set β
rw : Metric.ediam.{u} (X := α) ((⇑h.symm : (a : β) → α) '' s) = Metric.ediam s
rw₁ rw₂ : Metric.ediam s = Metric.ediam s
⊢ Metric.ediam.{u} (X := α) ((⇑h : (a : α) → β) ⁻¹' s) = Metric.ediam s

Tactic:
rw [← image_symm, ediam_image]

Premises used: IsometryEquiv.ediam_image, IsometryEquiv.image_symm
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
rw :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.eball x r)
    (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
      (Metric.eball ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
rw₁ rw₂ : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.eball x r) ((⇑h : (a : α) → β) ⁻¹' Metric.eball x r)
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.eball x r : Set α)
    (Metric.eball ((h.symm : (a : β) → α) x) r : Set α)

Tactic:
rw [← h.isometry.preimage_eball (h.symm x) r, h.apply_symm_apply]

Premises used: IsometryEquiv.apply_symm_apply, IsometryEquiv.symm, DFunLike.coe, Isometry.preimage_eball, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
rw :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedEBall x r)
    (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
      (Metric.closedEBall ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
rw₁ rw₂ :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedEBall x r)
    ((⇑h : (a : α) → β) ⁻¹' Metric.closedEBall x r)
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedEBall x r : Set α)
    (Metric.closedEBall ((h.symm : (a : β) → α) x) r : Set α)

Tactic:
rw [← h.isometry.preimage_closedEBall (h.symm x) r, h.apply_symm_apply]

Premises used: IsometryEquiv.apply_symm_apply, Isometry.preimage_closedEBall, IsometryEquiv.symm, DFunLike.coe, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
rw :
  Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.eball x r : Set β)
    (Metric.eball ((h : (a : α) → β) x) r : Set β)
rw₁ :
  Eq.{v + 1} (α := Set β) (Metric.eball ((h.symm.symm : (a : α) → β) x) r : Set β)
    (Metric.eball ((h : (a : α) → β) x) r : Set β)
rw₂ rw₃ :
  Eq.{v + 1} (α := Set β) (Metric.eball ((h : (a : α) → β) x) r : Set β) (Metric.eball ((h : (a : α) → β) x) r : Set β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.eball x r : Set β)
    (Metric.eball ((h : (a : α) → β) x) r : Set β)

Tactic:
rw [← h.preimage_symm, h.symm.preimage_eball, symm_symm]

Premises used: IsometryEquiv.symm, IsometryEquiv.symm_symm, IsometryEquiv.preimage_symm, IsometryEquiv.preimage_eball
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
rw :
  Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.closedEBall x r : Set β)
    (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
rw₁ :
  Eq.{v + 1} (α := Set β) (Metric.closedEBall ((h.symm.symm : (a : α) → β) x) r : Set β)
    (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
rw₂ rw₃ :
  Eq.{v + 1} (α := Set β) (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
    (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.closedEBall x r : Set β)
    (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)

Tactic:
rw [← h.preimage_symm, h.symm.preimage_closedEBall, symm_symm]

Premises used: IsometryEquiv.preimage_closedEBall, IsometryEquiv.symm, IsometryEquiv.symm_symm, IsometryEquiv.preimage_symm
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq (α := (a : α) → β) (⇑h.toHomeomorph : (a : α) → β) (⇑h : (a : α) → β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Eq (α := (a : β) → α) (⇑h.toHomeomorph.symm : (a : β) → α) (⇑h.symm : (a : β) → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
γ : Type u_3
inst_2 : TopologicalSpace γ
h : α ≃ᵢ β
f : γ → α
s : Set γ
⊢ ContinuousOn.{u_3, v} (Y := β) ((⇑h : (a : α) → β) ∘ f) s ↔ ContinuousOn f s

Tactic:
h.toHomeomorph.comp_continuousOn_iff _ _

Premises used: Homeomorph.comp_continuousOn_iff, IsometryEquiv.toHomeomorph
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
γ : Type u_3
inst_2 : TopologicalSpace γ
h : α ≃ᵢ β
f : γ → α
⊢ Continuous[inst_2, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] ((⇑h : (a : α) → β) ∘ f) ↔
    Continuous[inst_2, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
h.toHomeomorph.comp_continuous_iff

Premises used: Homeomorph.comp_continuous_iff, IsometryEquiv.toHomeomorph
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
γ : Type u_3
inst_2 : TopologicalSpace γ
h : α ≃ᵢ β
f : β → γ
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, inst_2] (f ∘ (⇑h : (a : α) → β)) ↔
    Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, inst_2] f

Tactic:
h.toHomeomorph.comp_continuous_iff'

Premises used: Homeomorph.comp_continuous_iff', IsometryEquiv.toHomeomorph
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ Eq.{u + 1} (α := (a : α) → α) (⇑1 : (a : α) → α) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
e₁ e₂ : α ≃ᵢ α
⊢ Eq (α := (a : α) → α) (⇑(e₁ * e₂) : (a : α) → α) (comp (β := α) (⇑e₁ : (a : α) → α) (⇑e₂ : (a : α) → α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
e₁ e₂ : α ≃ᵢ α
x : α
⊢ Eq (α := α) ((e₁ * e₂ : (a : α) → α) x : α) ((e₁ : (a : α) → α) ((e₂ : (a : α) → α) x : α) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
e : α ≃ᵢ α
x : α
⊢ (e⁻¹ : (a : α) → α) ((e : (a : α) → α) x : α) = x

Tactic:
e.symm_apply_apply x

Premises used: IsometryEquiv.symm_apply_apply
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
e : α ≃ᵢ α
x : α
⊢ (e : (a : α) → α) ((e⁻¹ : (a : α) → α) x : α) = x

Tactic:
e.apply_symm_apply x

Premises used: IsometryEquiv.apply_symm_apply
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
e : α ≃ᵢ β
⊢ CompleteSpace α ↔ CompleteSpace β

Tactic:
simp only [completeSpace_iff_isComplete_univ, ← e.range_eq_univ, ← image_univ,
    isComplete_image_iff e.isometry.isUniformInducing]

Premises used: IsometryEquiv.range_eq_univ, Set.image_univ, completeSpace_iff_isComplete_univ, Isometry.isUniformInducing, isComplete_image_iff, IsometryEquiv.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : CompleteSpace β
e : α ≃ᵢ β
⊢ CompleteSpace α

Tactic:
e.completeSpace_iff.2 ‹_›

Premises used: Iff.mpr, IsometryEquiv.completeSpace_iff
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
ι' : Type u_3
inst_3 : Fintype ι
inst_4 : Fintype ι'
Y : ι → Type u_4
inst_5 : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
simp_rw :
  Eq (α := ℝ≥0∞) (⨆ (b : ι'), edist ((Equiv.piCongrLeft' Y e).toFun x1 b) ((Equiv.piCongrLeft' Y e).toFun x2 b))
    (⨆ (b : ι), edist (x1 b) (x2 b))
⊢ edist ((Equiv.piCongrLeft' Y e).toFun x1) ((Equiv.piCongrLeft' Y e).toFun x2) = edist x1 x2

Tactic:
simp_rw [edist_pi_def, Finset.sup_univ_eq_iSup]

Premises used: edist_pi_def, Finset.sup_univ_eq_iSup
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
ι' : Type u_3
inst_3 : Fintype ι
inst_4 : Fintype ι'
Y : ι → Type u_4
inst_5 : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ Eq (α := ℝ≥0∞) (⨆ (b : ι'), edist ((Equiv.piCongrLeft' Y e).toFun x1 b) ((Equiv.piCongrLeft' Y e).toFun x2 b))
    (⨆ (b : ι), edist (x1 b) (x2 b))

Tactic:
(Equiv.iSup_comp (g := fun b ↦ edist (x1 b) (x2 b)) e.symm)

Premises used: Equiv.iSup_comp, Equiv.symm
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
ι' : Type u_3
inst_3 : Fintype ι
inst_4 : Fintype ι'
Y : ι → Type u_4
inst_5 : (j : ι) → PseudoEMetricSpace (Y j)
e : ι ≃ ι'
x1 x2 : (i : ι) → Y i
⊢ Eq (α := ℝ≥0∞) (⨆ (b : ι'), edist ((Equiv.piCongrLeft' Y e).toFun x1 b) ((Equiv.piCongrLeft' Y e).toFun x2 b))
    (⨆ (b : ι), edist (x1 b) (x2 b))

Tactic:
exact (Equiv.iSup_comp (g := fun b ↦ edist (x1 b) (x2 b)) e.symm)

Premises used: Equiv.iSup_comp, Equiv.symm
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : Fintype α
inst_4 : Fintype β
x x_1 : α ⊕ β → γ
⊢ edist ((Equiv.sumArrowEquivProdArrow α β γ).toFun x) ((Equiv.sumArrowEquivProdArrow α β γ).toFun x_1) = edist x x_1

Tactic:
simp [Prod.edist_eq, edist_pi_def, Finset.sup_univ_eq_iSup, iSup_sum]

Premises used: Prod.edist_eq, edist_pi_def, Finset.sup_univ_eq_iSup, iSup_sum
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
γ : Type w
inst : PseudoEMetricSpace γ
α : Type u_3
β : Type u_4
inst_1 : Fintype α
inst_2 : Fintype β
⊢ Eq (α := (α ⊕ β → γ) ≃ₜ (α → γ) × (β → γ)) (IsometryEquiv.toHomeomorph sumArrowIsometryEquivProdArrow)
    Homeomorph.sumArrowHomeomorphProdArrow

Tactic:
rfl

Premises used: setOf, Homeomorph.sumArrowHomeomorphProdArrow, IsometryEquiv.toHomeomorph, rfl, Equiv.sumArrowEquivProdArrow
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
m n : ℕ
x x2 : Fin m → α
y y2 : Fin n → α
⊢ edist (Fin.append x y) (Fin.append x2 y2) = max (edist x x2) (edist y y2)

Tactic:
simp [edist_pi_def, Finset.sup_univ_eq_iSup, ← Equiv.iSup_comp (e := finSumFinEquiv),
    iSup_sum]

Premises used: Equiv.iSup_comp, finSumFinEquiv, edist_pi_def, Finset.sup_univ_eq_iSup, iSup_sum
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
m n : ℕ
x x_1 : (Fin m → α) × (Fin n → α)
simp_rw : edist (Fin.append x.1 x.2) (Fin.append x_1.1 x_1.2) = edist x x_1
simp_rw₁ : max (edist x.1 x_1.1) (edist x.2 x_1.2) = edist x x_1
⊢ edist (Equiv.toFun (Fin.appendEquiv m n) x) (Equiv.toFun (Fin.appendEquiv m n) x_1) = edist x x_1

Tactic:
simp_rw [Fin.appendEquiv, Fin.edist_append_eq_max_edist, Prod.edist_eq]

Premises used: Prod.edist_eq, Fin.appendEquiv, Fin.edist_append_eq_max_edist
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
m n : ℕ
⊢ Eq.{u + 1} (α := (Fin m → α) × (Fin n → α) ≃ₜ (Fin (m + n) → α)) (IsometryEquiv.toHomeomorph (Fin.appendIsometry m n))
    (Fin.appendHomeomorph m n)

Tactic:
rfl

Premises used: Fin.appendHomeomorph, Fin.appendEquiv, setOf, IsometryEquiv.toHomeomorph, rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
ι : Type u_2
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
inst_3 : Unique ι
inst_4 : Fintype ι
x hx : ι → α
⊢ edist ((Equiv.funUnique ι α).toFun x) ((Equiv.funUnique ι α).toFun hx) = edist x hx

Tactic:
simp [edist_pi_def, Finset.univ_unique, Finset.sup_singleton]

Premises used: Finset.sup_singleton, Finset.univ_unique, edist_pi_def
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
ι : Type u_2
α_1 : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α_1
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
α : Fin 2 → Type u_3
inst_3 : (i : Fin 2) → PseudoEMetricSpace (α i)
x hx : (i : Fin 2) → α i
⊢ edist ((piFinTwoEquiv α).toFun x) ((piFinTwoEquiv α).toFun hx) = edist x hx

Tactic:
simp [edist_pi_def, Fin.univ_succ, Prod.edist_eq]

Premises used: Prod.edist_eq, Fin.univ_succ, edist_pi_def
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set α
⊢ Metric.diam.{v} (α := β) ((⇑h : (a : α) → β) '' s) = Metric.diam s

Tactic:
h.isometry.diam_image s

Premises used: Isometry.diam_image, IsometryEquiv.isometry