awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
inst_4 : Add M
inst_5 : PseudoEMetricSpace M
inst_6 : IsIsometricVAdd M M
⊢ IsIsometricSMul.{u, u} (Multiplicative M) (Multiplicative M)

Tactic:
⟨fun c x y => edist_vadd_left c.toAdd x.toAdd y.toAdd⟩

Premises used: edist_vadd_left, Multiplicative.toAdd, IsIsometricSMul.mk, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.IsometricSMul
Goal:
M : Type u
G : Type v
X : Type w
Y : Type u_1
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
inst_2 : SMul M X
inst_3 : IsIsometricSMul M X
inst_4 : Add M
inst_5 : PseudoEMetricSpace M
inst_6 : IsIsometricVAdd Mᵃᵒᵖ M
⊢ IsIsometricSMul.{u, u} (Multiplicative M)ᵐᵒᵖ (Multiplicative M)

Tactic:
⟨fun c x y => edist_vadd_left (AddOpposite.op c.unop.toAdd) x.toAdd y.toAdd⟩

Premises used: edist_vadd_left, MulOpposite.unop, Multiplicative.toAdd, IsIsometricSMul.mk, DFunLike.coe, AddOpposite.op
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), nndist (f x) (f y) = nndist x y

Tactic:
simp only [Isometry, edist_nndist, ENNReal.coe_inj]

Premises used: ENNReal.coe_inj, edist_nndist, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
⊢ Isometry f ↔ ∀ (x y : α), dist (f x) (f y) = dist x y

Tactic:
simp only [isometry_iff_nndist_eq, ← coe_nndist, NNReal.coe_inj]

Premises used: coe_nndist, isometry_iff_nndist_eq, NNReal.coe_inj
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x y : α
⊢ edist (f x) (f y) = edist x y

Tactic:
hf x y
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
⊢ LipschitzWith 1 f

Tactic:
LipschitzWith.of_edist_le fun x y => (h x y).le

Premises used: LipschitzWith.of_edist_le, Eq.le
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
x y : α
⊢ edist x y ≤ (↑1 : ℝ≥0∞) * edist (f x) (f y)

Tactic:
simp only [h x y, ENNReal.coe_one, one_mul, le_refl]

Premises used: le_refl, ENNReal.coe_one, one_mul
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
inst_2 : Subsingleton α
x y : α
rw : edist (f y) (f y) = edist y y
⊢ edist (f x) (f y) = edist x y

Tactic:
rw [Subsingleton.elim x y]

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
inst_2 : Subsingleton α
x y : α
⊢ edist (f y) (f y) = edist y y

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
⊢ Isometry.{u, u} (α := α) id

Tactic:
fun _ _ => rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
δ : Type u_3
inst_3 : PseudoEMetricSpace δ
f : α → β
g : γ → δ
hf : Isometry f
hg : Isometry g
x y : α × γ
⊢ edist (Prod.map f g x) (Prod.map f g y) = edist x y

Tactic:
simp only [Prod.edist_eq, Prod.map_fst, hf.edist_eq, Prod.map_snd, hg.edist_eq]

Premises used: Prod.edist_eq, Prod.map_snd, Isometry.edist_eq, Prod.map_fst
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
ι : Type u_5
inst : Fintype ι
α : ι → Type u_3
β : ι → Type u_4
inst_1 : (i : ι) → PseudoEMetricSpace (α i)
inst_2 : (i : ι) → PseudoEMetricSpace (β i)
f : (i : ι) → α i → β i
hf : ∀ (i : ι), Isometry (f i)
x y : (i : ι) → α i
⊢ edist (Pi.map (α := α) (β := β) f x) (Pi.map (α := α) (β := β) f y) = edist x y

Tactic:
simp only [edist_pi_def, (hf _).edist_eq, Pi.map_apply]

Premises used: Isometry.edist_eq, edist_pi_def, Pi.map_apply
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → PseudoEMetricSpace (E i)
inst_3 : (i : ι) → Zero (E i)
i : ι
x y : E i
rw : (Finset.sup Finset.univ fun (b : ι) ↦ edist (Pi.single (M := E) i x b) (Pi.single (M := E) i y b)) = edist x y
⊢ edist (Pi.single (M := E) i x) (Pi.single (M := E) i y) = edist x y

Tactic:
rw [edist_pi_def]

Premises used: edist_pi_def
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → PseudoEMetricSpace (E i)
inst_3 : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ edist x y ≤ edist (Pi.single (M := E) i x i) (Pi.single (M := E) i y i)

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → PseudoEMetricSpace (E i)
inst_3 : (i : ι) → Zero (E i)
i : ι
x y : E i
refine :
  ∀ (j : ι),
    Membership.mem (γ := Finset ι) Finset.univ j →
      edist (Pi.single (M := E) i x j) (Pi.single (M := E) i y j) ≤ edist x y
⊢ (Finset.sup Finset.univ fun (b : ι) ↦ edist (Pi.single (M := E) i x b) (Pi.single (M := E) i y b)) = edist x y

Tactic:
refine le_antisymm (Finset.sup_le fun j ↦ ?_) (Finset.le_sup_of_le (Finset.mem_univ i) (by simp))

Premises used: Finset.mem_univ, Finset.sup_le, le_antisymm, Finset.le_sup_of_le
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → PseudoEMetricSpace (E i)
inst_3 : (i : ι) → Zero (E i)
i : ι
x y : E i
j : ι
inl :
  Membership.mem (γ := Finset ι) Finset.univ i → edist (Pi.single (M := E) i x i) (Pi.single (M := E) i y i) ≤ edist x y
inr :
  ∀ (h : i ≠ j),
    Membership.mem (γ := Finset ι) Finset.univ j →
      edist (Pi.single (M := E) i x j) (Pi.single (M := E) i y j) ≤ edist x y
⊢ Membership.mem (γ := Finset ι) Finset.univ j → edist (Pi.single (M := E) i x j) (Pi.single (M := E) i y j) ≤ edist x y

Tactic:
obtain rfl | h := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → PseudoEMetricSpace (E i)
inst_3 : (i : ι) → Zero (E i)
i : ι
x y : E i
⊢ Membership.mem (γ := Finset ι) Finset.univ i → edist (Pi.single (M := E) i x i) (Pi.single (M := E) i y i) ≤ edist x y

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
ι : Type u_2
inst : Fintype ι
inst_1 : DecidableEq ι
E : ι → Type u_3
inst_2 : (i : ι) → PseudoEMetricSpace (E i)
inst_3 : (i : ι) → Zero (E i)
i : ι
x y : E i
j : ι
h : i ≠ j
⊢ Membership.mem (γ := Finset ι) Finset.univ j → edist (Pi.single (M := E) i x j) (Pi.single (M := E) i y j) ≤ edist x y

Tactic:
simp [h]
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : AddZeroClass α
inst_3 : AddZeroClass β
x y : α
⊢ max (edist.{u} (α := α) ((AddMonoidHom.inl α β : (a : α) → α × β) x).1 ((AddMonoidHom.inl α β : (a : α) → α × β) y).1)
      (edist.{v} (α := β) ((AddMonoidHom.inl α β : (a : α) → α × β) x).2
        ((AddMonoidHom.inl α β : (a : α) → α × β) y).2) =
    edist x y

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : AddZeroClass α
inst_3 : AddZeroClass β
x y : β
⊢ max (edist.{u} (α := α) ((AddMonoidHom.inr α β : (a : β) → α × β) x).1 ((AddMonoidHom.inr α β : (a : β) → α × β) y).1)
      (edist.{v} (α := β) ((AddMonoidHom.inr α β : (a : β) → α × β) x).2
        ((AddMonoidHom.inr α β : (a : β) → α × β) y).2) =
    edist x y

Tactic:
simp
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
γ : Type w
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β → γ
f : α → β
hg : Isometry g
hf : Isometry f
⊢ Isometry (g ∘ f)

Tactic:
fun _ _ => (hg _ _).trans (hf _ _)

Premises used: Eq.trans, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ UniformContinuous f

Tactic:
hf.lipschitz.uniformContinuous

Premises used: LipschitzWith.uniformContinuous, Isometry.lipschitz
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ IsUniformInducing f

Tactic:
hf.antilipschitz.isUniformInducing hf.uniformContinuous

Premises used: Isometry.uniformContinuous, AntilipschitzWith.isUniformInducing, Isometry.antilipschitz
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
ι : Type u_3
f : α → β
g : ι → α
a : Filter ι
b : α
hf : Isometry f
⊢ Filter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto (f ∘ g) a (𝓝 (f b))

Tactic:
hf.isUniformInducing.isInducing.tendsto_nhds_iff

Premises used: IsUniformInducing.isInducing, Topology.IsInducing.tendsto_nhds_iff, Isometry.isUniformInducing
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    f

Tactic:
hf.lipschitz.continuous

Premises used: LipschitzWith.continuous, Isometry.lipschitz
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
rw : edist (f (g x)) (f (g y)) = edist x y
rw₁ : edist x (f (g y)) = edist x y
rw₂ rw₃ : edist x y = edist x y
⊢ edist (g x) (g y) = edist x y

Tactic:
rw [← h, hg _, hg _]
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
h₁ : ∀ (y : α), y ∈ f ⁻¹' Metric.closedEBall (f x) r ↔ y ∈ Metric.closedEBall x r
⊢ f ⁻¹' Metric.closedEBall (f x) r = Metric.closedEBall x r

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
y : α
⊢ y ∈ f ⁻¹' Metric.closedEBall (f x) r ↔ y ∈ Metric.closedEBall x r

Tactic:
simp [h.edist_eq]

Premises used: Isometry.edist_eq
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
h₁ : ∀ (y : α), y ∈ f ⁻¹' Metric.eball (f x) r ↔ y ∈ Metric.eball x r
⊢ f ⁻¹' Metric.eball (f x) r = Metric.eball x r

Tactic:
ext y
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
y : α
⊢ y ∈ f ⁻¹' Metric.eball (f x) r ↔ y ∈ Metric.eball x r

Tactic:
simp [h.edist_eq]

Premises used: Isometry.edist_eq
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
s : Set α
d : ℝ≥0∞
⊢ Metric.ediam (f '' s) ≤ d ↔ Metric.ediam s ≤ d

Tactic:
simp only [Metric.ediam_le_iff, forall_mem_image, hf.edist_eq]

Premises used: Isometry.edist_eq, Metric.ediam_le_iff, Set.forall_mem_image
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
rw : Metric.ediam (f '' univ) = Metric.ediam.{u} (X := α) univ
⊢ Metric.ediam (range f) = Metric.ediam.{u} (X := α) univ

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.ediam (f '' univ) = Metric.ediam.{u} (X := α) univ

Tactic:
hf.ediam_image univ

Premises used: Set.univ, Isometry.ediam_image
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.ediam (f '' univ) = Metric.ediam.{u} (X := α) univ

Tactic:
exact hf.ediam_image univ

Premises used: Set.univ, Isometry.ediam_image
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x : α
r : ℝ≥0∞
⊢ MapsTo f (Metric.eball x r) (Metric.eball (f x) r)

Tactic:
(hf.preimage_eball x r).ge

Premises used: Eq.ge, Set.Mem, setOf, Metric.eball, Set.Subset, Set.preimage, Set.MapsTo, Isometry.preimage_eball
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
x : α
r : ℝ≥0∞
⊢ MapsTo f (Metric.closedEBall x r) (Metric.closedEBall (f x) r)

Tactic:
(hf.preimage_closedEBall x r).ge

Premises used: Eq.ge, Isometry.preimage_closedEBall, Set.Mem, setOf, Set.Subset, Set.preimage, Set.MapsTo, Metric.closedEBall
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
inst : PseudoEMetricSpace α
s : Set α
⊢ Isometry.{u, u} (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))

Tactic:
fun _ _ => rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
⊢ Isometry NNReal.toReal

Tactic:
fun _ _ ↦ rfl

Premises used: NNReal.toReal, rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
γ : Type u_3
inst_2 : TopologicalSpace γ
hf : Isometry f
g : γ → α
s : Set γ
⊢ ContinuousOn (f ∘ g) s ↔ ContinuousOn g s

Tactic:
hf.isUniformInducing.isInducing.continuousOn_iff.symm

Premises used: IsUniformInducing.isInducing, Isometry.isUniformInducing, Topology.IsInducing.continuousOn_iff, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
γ : Type u_3
inst_2 : TopologicalSpace γ
hf : Isometry f
g : γ → α
⊢ Continuous[inst_2, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (f ∘ g) ↔
    Continuous[inst_2, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] g

Tactic:
hf.isUniformInducing.isInducing.continuous_iff.symm

Premises used: Topology.IsInducing.continuous_iff, IsUniformInducing.isInducing, Isometry.isUniformInducing, Iff.symm
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : EMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
⊢ Injective f

Tactic:
h.antilipschitz.injective

Premises used: AntilipschitzWith.injective, Isometry.antilipschitz
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : EMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ IsUniformEmbedding f

Tactic:
hf.antilipschitz.isUniformEmbedding hf.lipschitz.uniformContinuous

Premises used: AntilipschitzWith.isUniformEmbedding, LipschitzWith.uniformContinuous, Isometry.lipschitz, Isometry.antilipschitz
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : EMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ IsEmbedding f

Tactic:
hf.isUniformEmbedding.isEmbedding

Premises used: Isometry.isUniformEmbedding, IsUniformEmbedding.isEmbedding
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
γ : Type w
inst : EMetricSpace α
inst_1 : CompleteSpace α
inst_2 : EMetricSpace γ
f : α → γ
hf : Isometry f
⊢ IsClosedEmbedding f

Tactic:
hf.antilipschitz.isClosedEmbedding hf.lipschitz.uniformContinuous

Premises used: AntilipschitzWith.isClosedEmbedding, LipschitzWith.uniformContinuous, Isometry.lipschitz, Isometry.antilipschitz
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
rw : (Metric.ediam (f '' s)).toReal = Metric.diam s
rw₁ : (Metric.ediam (f '' s)).toReal = (Metric.ediam s).toReal
rw₂ rw₃ : (Metric.ediam s).toReal = (Metric.ediam s).toReal
⊢ Metric.diam (f '' s) = Metric.diam s

Tactic:
rw [Metric.diam, Metric.diam, hf.ediam_image]

Premises used: Isometry.ediam_image, Metric.diam
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
rw : Metric.diam (f '' univ) = Metric.diam.{u} (α := α) univ
⊢ Metric.diam (range f) = Metric.diam.{u} (α := α) univ

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (f '' univ) = Metric.diam.{u} (α := α) univ

Tactic:
hf.diam_image univ

Premises used: Set.univ, Isometry.diam_image
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (f '' univ) = Metric.diam.{u} (α := α) univ

Tactic:
exact hf.diam_image univ

Premises used: Set.univ, Isometry.diam_image
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
p : ℝ → Prop
⊢ f ⁻¹' {y : β | p (dist y (f x))} = {y : α | p (dist y x)}

Tactic:
simp [hf.dist_eq]

Premises used: Isometry.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
r : ℝ
⊢ f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r

Tactic:
hf.preimage_setOf_dist x (· ≤ r)

Premises used: LE.le, Isometry.preimage_setOf_dist, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
r : ℝ
⊢ f ⁻¹' Metric.ball (f x) r = Metric.ball x r

Tactic:
hf.preimage_setOf_dist x (· < r)

Premises used: Metric.ball, Isometry.preimage_setOf_dist, LT.lt
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
r : ℝ
⊢ f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r

Tactic:
hf.preimage_setOf_dist x (· = r)

Premises used: Isometry.preimage_setOf_dist, Eq, Metric.sphere
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
r : ℝ
⊢ MapsTo f (Metric.ball x r) (Metric.ball (f x) r)

Tactic:
(hf.preimage_ball x r).ge

Premises used: Isometry.preimage_ball, Eq.ge, Set.Mem, setOf, Metric.ball, Set.Subset, Set.preimage, Set.MapsTo
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
r : ℝ
⊢ MapsTo f (Metric.sphere x r) (Metric.sphere (f x) r)

Tactic:
(hf.preimage_sphere x r).ge

Premises used: Eq.ge, Set.Mem, setOf, Isometry.preimage_sphere, Set.Subset, Set.preimage, Set.MapsTo, Metric.sphere
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
x : α
r : ℝ
⊢ MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) r)

Tactic:
(hf.preimage_closedBall x r).ge

Premises used: Eq.ge, Set.Mem, setOf, Isometry.preimage_closedBall, Set.Subset, Set.preimage, Set.MapsTo, Metric.closedBall
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u_3
β : Type u_4
inst : UniformSpace α
inst_1 : MetricSpace β
f : α → β
h : IsUniformEmbedding f
⊢ Isometry f

Tactic:
let _ := h.comapMetricSpace f
  Isometry.of_dist_eq fun _ _ => rfl

Premises used: Isometry.of_dist_eq, IsUniformEmbedding.comapMetricSpace, rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u_3
β : Type u_4
inst : TopologicalSpace α
inst_1 : PseudoMetricSpace β
f : α → β
h : IsEmbedding f
⊢ Isometry f

Tactic:
let _ := h.comapPseudoMetricSpace
  Isometry.of_dist_eq fun _ _ => rfl

Premises used: Isometry.of_dist_eq, Topology.IsInducing.comapPseudoMetricSpace, Topology.IsEmbedding.toIsInducing, rfl
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
f : α → β
m : PseudoEMetricSpace β
⊢ Isometry f

Tactic:
fun _ _ ↦ rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
f : α → β
m : PseudoMetricSpace β
⊢ Isometry f

Tactic:
fun _ _ ↦ rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
m : EMetricSpace β
⊢ Isometry f

Tactic:
fun _ _ ↦ rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
α : Type u
β : Type v
f : α → β
hf : Injective f
m : MetricSpace β
⊢ Isometry f

Tactic:
fun _ _ ↦ rfl

Premises used: rfl, Isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : IsometryClass F α β
f : F
x y : α
⊢ edist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = edist x y

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

Premises used: Isometry.edist_eq, IsometryClass.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : IsometryClass F α β
f : F
⊢ Continuous[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace, PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (⇑f : (a : α) → β)

Tactic:
(IsometryClass.isometry f).continuous

Premises used: Isometry.continuous, IsometryClass.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : IsometryClass F α β
f : F
⊢ LipschitzWith.{u, v} (α := α) (β := β) 1 (⇑f : (a : α) → β)

Tactic:
(IsometryClass.isometry f).lipschitz

Premises used: Isometry.lipschitz, IsometryClass.isometry
-- Module: Mathlib.Topology.MetricSpace.Isometry
Goal:
F : Type u_1
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : IsometryClass F α β
f : F
⊢ AntilipschitzWith.{u, v} (α := α) (β := β) 1 (⇑f : (a : α) → β)

Tactic:
(IsometryClass.isometry f).antilipschitz

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

Tactic:
(IsometryClass.isometry f).ediam_image s

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

Tactic:
(IsometryClass.isometry f).ediam_range

Premises used: Isometry.ediam_range, 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
x y : α
⊢ dist.{v} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) = dist x y

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

Premises used: Isometry.dist_eq, IsometryClass.isometry