awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
inst : Group G
inst_1 : PseudoEMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ≥0∞
⊢ (fun (x : G) ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b / a) r
have rw : (fun (x : G) ↦ x * a) ⁻¹' closedEBall b r = closedEBall (b * a⁻¹) r
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun (x : X) ↦ c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r
have rw : c⁻¹ • ball x r = ball (c⁻¹ • x) r
Tactic: rw [preimage_smul, smul_ball]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
rw : c⁻¹ • ball x r = ball (c⁻¹ • x) r
⊢ (fun (x : X) ↦ c • x) ⁻¹' ball x r = ball (c⁻¹ • x) r
have rw₁ : ball (c⁻¹ • x) r = ball (c⁻¹ • x) r
Tactic: rw [preimage_smul, smul_ball]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun (x : X) ↦ c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r
have rw : c⁻¹ • closedBall x r = closedBall (c⁻¹ • x) r
Tactic: rw [preimage_smul, smul_closedBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
rw : c⁻¹ • closedBall x r = closedBall (c⁻¹ • x) r
⊢ (fun (x : X) ↦ c • x) ⁻¹' closedBall x r = closedBall (c⁻¹ • x) r
have rw₁ : closedBall (c⁻¹ • x) r = closedBall (c⁻¹ • x) r
Tactic: rw [preimage_smul, smul_closedBall]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
⊢ (fun (x : X) ↦ c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r
have rw : c⁻¹ • sphere x r = sphere (c⁻¹ • x) r
Tactic: rw [preimage_smul, smul_sphere]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
X : Type w
inst : PseudoMetricSpace X
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : IsIsometricSMul G X
c : G
x : X
r : ℝ
rw : c⁻¹ • sphere x r = sphere (c⁻¹ • x) r
⊢ (fun (x : X) ↦ c • x) ⁻¹' sphere x r = sphere (c⁻¹ • x) r
have rw₁ : sphere (c⁻¹ • x) r = sphere (c⁻¹ • x) r
Tactic: rw [preimage_smul, smul_sphere]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun (x : G) ↦ x * a) ⁻¹' ball b r = ball (b / a) r
have rw : (fun (x : G) ↦ x * a) ⁻¹' ball b r = ball (b * a⁻¹) r
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.IsometricSMul (goal)
Goal:
G : Type v
inst : Group G
inst_1 : PseudoMetricSpace G
inst_2 : IsIsometricSMul Gᵐᵒᵖ G
a b : G
r : ℝ
⊢ (fun (x : G) ↦ x * a) ⁻¹' closedBall b r = closedBall (b / a) r
have rw : (fun (x : G) ↦ x * a) ⁻¹' closedBall b r = closedBall (b * a⁻¹) r
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
inst_2 : Subsingleton α
x y : α
⊢ edist (f x) (f y) = edist x y
have rw : edist (f y) (f y) = edist y y
Tactic: rw [Subsingleton.elim x y]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 (Pi.single (M := E) i x) (Pi.single (M := E) i y) = edist x y
have 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
Tactic: rw [edist_pi_def]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ (Finset.sup Finset.univ fun (b : ι) ↦ edist (Pi.single (M := E) i x b) (Pi.single (M := E) i y b)) = edist x y
have 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
Tactic: refine le_antisymm (Finset.sup_le fun j ↦ ?_) (Finset.le_sup_of_le (Finset.mem_univ i) (by simp))
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 : ι
⊢ Membership.mem (γ := Finset ι) Finset.univ j → edist (Pi.single (M := E) i x j) (Pi.single (M := E) i y j) ≤ edist x y
have 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
Tactic: obtain rfl | h := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ Membership.mem (γ := Finset ι) Finset.univ j → edist (Pi.single (M := E) i x j) (Pi.single (M := E) i y j) ≤ edist x y
have 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
Tactic: obtain rfl | h := eq_or_ne i j
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
g : β → α
h : Isometry f
hg : RightInverse g f
x y : β
⊢ edist (g x) (g y) = edist x y
have rw : edist (f (g x)) (f (g y)) = edist x y
Tactic: rw [← h, hg _, hg _]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ edist (g x) (g y) = edist x y
have rw₁ : edist x (f (g y)) = edist x y
Tactic: rw [← h, hg _, hg _]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ edist (g x) (g y) = edist x y
have rw₂ : edist x y = edist x y
Tactic: rw [← h, hg _, hg _]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' Metric.closedEBall (f x) r = Metric.closedEBall x r
have h₁ : ∀ (y : α), y ∈ f ⁻¹' Metric.closedEBall (f x) r ↔ y ∈ Metric.closedEBall x r
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
h : Isometry f
x : α
r : ℝ≥0∞
⊢ f ⁻¹' Metric.eball (f x) r = Metric.eball x r
have h₁ : ∀ (y : α), y ∈ f ⁻¹' Metric.eball (f x) r ↔ y ∈ Metric.eball x r
Tactic: ext y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.ediam (range f) = Metric.ediam.{u} (X := α) univ
have rw : Metric.ediam (f '' univ) = Metric.ediam.{u} (X := α) univ
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
s : Set α
⊢ Metric.diam (f '' s) = Metric.diam s
have rw : (Metric.ediam (f '' s)).toReal = Metric.diam s
Tactic: rw [Metric.diam, Metric.diam, hf.ediam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ Metric.diam (f '' s) = Metric.diam s
have rw₁ : (Metric.ediam (f '' s)).toReal = (Metric.ediam s).toReal
Tactic: rw [Metric.diam, Metric.diam, hf.ediam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ Metric.diam (f '' s) = Metric.diam s
have rw₂ : (Metric.ediam s).toReal = (Metric.ediam s).toReal
Tactic: rw [Metric.diam, Metric.diam, hf.ediam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
hf : Isometry f
⊢ Metric.diam (range f) = Metric.diam.{u} (α := α) univ
have rw : Metric.diam (f '' univ) = Metric.diam.{u} (α := α) univ
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ Metric.ediam.{u} (X := α) univ = Metric.ediam.{v} (X := β) univ
have rw : Metric.ediam.{u} (X := α) univ = Metric.ediam.{v} (X := β) (range.{v, u + 1} (ι := α) (⇑h : (a : α) → β))
Tactic: rw [← h.range_eq_univ, h.isometry.ediam_range]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 : α) → β))
⊢ Metric.ediam.{u} (X := α) univ = Metric.ediam.{v} (X := β) univ
have rw₁ : Metric.ediam.{u} (X := α) univ = Metric.ediam.{u} (X := α) univ
Tactic: rw [← h.range_eq_univ, h.isometry.ediam_range]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.ediam.{u} (X := α) ((⇑h : (a : α) → β) ⁻¹' s) = Metric.ediam s
have rw : Metric.ediam.{u} (X := α) ((⇑h.symm : (a : β) → α) '' s) = Metric.ediam s
Tactic: rw [← image_symm, ediam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ Metric.ediam.{u} (X := α) ((⇑h : (a : α) → β) ⁻¹' s) = Metric.ediam s
have rw₁ : Metric.ediam s = Metric.ediam s
Tactic: rw [← image_symm, ediam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.eball x r : Set α)
    (Metric.eball ((h.symm : (a : β) → α) x) r : Set α)
have 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 β))
Tactic: rw [← h.isometry.preimage_eball (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 β))
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.eball x r : Set α)
    (Metric.eball ((h.symm : (a : β) → α) x) r : Set α)
have rw₁ : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.eball x r) ((⇑h : (a : α) → β) ⁻¹' Metric.eball x r)
Tactic: rw [← h.isometry.preimage_eball (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ≥0∞
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedEBall x r : Set α)
    (Metric.closedEBall ((h.symm : (a : β) → α) x) r : Set α)
have 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 β))
Tactic: rw [← h.isometry.preimage_closedEBall (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 β))
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedEBall x r : Set α)
    (Metric.closedEBall ((h.symm : (a : β) → α) x) r : Set α)
have rw₁ : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedEBall x r) ((⇑h : (a : α) → β) ⁻¹' Metric.closedEBall x r)
Tactic: rw [← h.isometry.preimage_closedEBall (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.eball x r : Set β)
    (Metric.eball ((h : (a : α) → β) x) r : Set β)
have rw : Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.eball x r : Set β)
  (Metric.eball ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_eball, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.eball x r : Set β)
    (Metric.eball ((h : (a : α) → β) x) r : Set β)
have rw₁ : Eq.{v + 1} (α := Set β) (Metric.eball ((h.symm.symm : (a : α) → β) x) r : Set β)
  (Metric.eball ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_eball, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.eball x r : Set β)
    (Metric.eball ((h : (a : α) → β) x) r : Set β)
have rw₂ : Eq.{v + 1} (α := Set β) (Metric.eball ((h : (a : α) → β) x) r : Set β) (Metric.eball ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_eball, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
h : α ≃ᵢ β
x : α
r : ℝ≥0∞
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.closedEBall x r : Set β)
    (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
have rw : Eq.{v + 1} (α := Set β) ((⇑h.symm : (a : β) → α) ⁻¹' Metric.closedEBall x r : Set β)
  (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_closedEBall, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.closedEBall x r : Set β)
    (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
have rw₁ : Eq.{v + 1} (α := Set β) (Metric.closedEBall ((h.symm.symm : (a : α) → β) x) r : Set β)
  (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_closedEBall, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 β)
⊢ Eq.{v + 1} (α := Set β) ((⇑h : (a : α) → β) '' Metric.closedEBall x r : Set β)
    (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
have rw₂ : Eq.{v + 1} (α := Set β) (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
  (Metric.closedEBall ((h : (a : α) → β) x) r : Set β)
Tactic: rw [← h.preimage_symm, h.symm.preimage_closedEBall, symm_symm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ edist ((Equiv.piCongrLeft' Y e).toFun x1) ((Equiv.piCongrLeft' Y e).toFun x2) = edist x1 x2
have 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))
Tactic: simp_rw [edist_pi_def, Finset.sup_univ_eq_iSup]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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 → α)
⊢ edist (Equiv.toFun (Fin.appendEquiv m n) x) (Equiv.toFun (Fin.appendEquiv m n) x_1) = edist x x_1
have simp_rw : edist (Fin.append x.1 x.2) (Fin.append x_1.1 x_1.2) = edist x x_1
Tactic: simp_rw [Fin.appendEquiv, Fin.edist_append_eq_max_edist, Prod.edist_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
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
⊢ edist (Equiv.toFun (Fin.appendEquiv m n) x) (Equiv.toFun (Fin.appendEquiv m n) x_1) = edist x x_1
have simp_rw₁ : max (edist x.1 x_1.1) (edist x.2 x_1.2) = edist x x_1
Tactic: simp_rw [Fin.appendEquiv, Fin.edist_append_eq_max_edist, Prod.edist_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
⊢ Metric.diam.{u} (α := α) ((⇑h : (a : α) → β) ⁻¹' s) = Metric.diam s
have rw : Metric.diam.{u} (α := α) ((⇑h.symm : (a : β) → α) '' s) = Metric.diam s
Tactic: rw [← image_symm, diam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
s : Set β
rw : Metric.diam.{u} (α := α) ((⇑h.symm : (a : β) → α) '' s) = Metric.diam s
⊢ Metric.diam.{u} (α := α) ((⇑h : (a : α) → β) ⁻¹' s) = Metric.diam s
have rw₁ : Metric.diam s = Metric.diam s
Tactic: rw [← image_symm, diam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r : Set α)
    (Metric.ball ((h.symm : (a : β) → α) x) r : Set α)
have rw : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r)
  (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
    (Metric.ball ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
Tactic: rw [← h.isometry.preimage_ball (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
rw :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r)
    (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
      (Metric.ball ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r : Set α)
    (Metric.ball ((h.symm : (a : β) → α) x) r : Set α)
have rw₁ : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r) ((⇑h : (a : α) → β) ⁻¹' Metric.ball x r)
Tactic: rw [← h.isometry.preimage_ball (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r : Set α)
    (Metric.sphere ((h.symm : (a : β) → α) x) r : Set α)
have rw : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r)
  (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
    (Metric.sphere ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
Tactic: rw [← h.isometry.preimage_sphere (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
rw :
  Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r)
    (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
      (Metric.sphere ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r : Set α)
    (Metric.sphere ((h.symm : (a : β) → α) x) r : Set α)
have rw₁ : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r) ((⇑h : (a : α) → β) ⁻¹' Metric.sphere x r)
Tactic: rw [← h.isometry.preimage_sphere (h.symm x) r, h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Isometry (goal)
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r : Set α)
    (Metric.closedBall ((h.symm : (a : β) → α) x) r : Set α)
have rw : Eq.{u + 1} (α := Set α) ((⇑h : (a : α) → β) ⁻¹' Metric.closedBall x r)
  (preimage.{u, v} (β := β) ((⇑h : (a : α) → β) : (a : α) → β)
    (Metric.closedBall ((h : (a : α) → β) ((h.symm : (a : β) → α) x : α)) r : Set β))
Tactic: rw [← h.isometry.preimage_closedBall (h.symm x) r, h.apply_symm_apply]