awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f g : α →ᵈ α
⊢ ratio (f * g) = ratio f * ratio g
have pos : ∀ (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞), ratio (f * g) = ratio f * ratio g
Tactic: by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
inst : PseudoEMetricSpace α
f g : α →ᵈ α
pos : ∀ (h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ∞), ratio (f * g) = ratio f * ratio g
⊢ ratio (f * g) = ratio f * ratio g
have neg : ∀ (h : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (f * g) = ratio f * ratio g
Tactic: by_cases! h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective.{u_2 + 1, u_3 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw : Eq.{u_3 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective.{u_2 + 1, u_3 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_3 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw₁ : Eq.{u_3 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
g : β →ᵈ γ
f₁ f₂ : α →ᵈ β
hg : Injective.{u_2 + 1, u_3 + 1} (α := β) (β := γ) (⇑g : (a : β) → γ)
h : g.comp f₁ = g.comp f₂
x : α
rw : Eq.{u_3 + 1} (α := γ) ((g.comp f₁ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
rw₁ : Eq.{u_3 + 1} (α := γ) ((g.comp f₂ : (a : α) → γ) x : γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
⊢ Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) ((f₁ : (a : α) → β) x : β) : γ)
    ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
have rw₂ : Eq.{u_3 + 1} (α := γ) ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
  ((g : (a : β) → γ) ((f₂ : (a : α) → β) x : β) : γ)
Tactic: rw [← comp_apply, h, comp_apply]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
s : Set α
⊢ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s) = (↑(ratio f) : ℝ≥0∞) * ediam s
have refine : (↑(ratio f) : ℝ≥0∞) * ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)
Tactic: refine ((lipschitz f).ediam_image_le s).antisymm ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
s : Set α
⊢ (↑(ratio f) : ℝ≥0∞) * ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)
have h : ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s) / (↑(ratio f) : ℝ≥0∞)
Tactic: apply ENNReal.mul_le_of_le_div'
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
s : Set α
⊢ ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s) / (↑(ratio f) : ℝ≥0∞)
have h : ediam s ≤ (↑(ratio f)⁻¹ : ℝ≥0∞) * ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)
Tactic: rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
s : Set α
h : ediam s ≤ (↑(ratio f)⁻¹ : ℝ≥0∞) * ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s)
⊢ ediam s ≤ ediam.{u_2} (X := β) ((⇑f : (a : α) → β) '' s) / (↑(ratio f) : ℝ≥0∞)
have h₁ : ratio f ≠ 0
Tactic: rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
⊢ ediam.{u_2} (X := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) =
    (↑(ratio f) : ℝ≥0∞) * ediam.{u_1} (X := α) univ
have rw : ediam.{u_2} (X := β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) univ) =
  (↑(ratio f) : ℝ≥0∞) * ediam.{u_1} (X := α) univ
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (eball ((f : (a : α) → β) x) ((↑(ratio f) : ℝ≥0∞) * r) : Set β)
    ((f : (a : α) → β) y : β)
have rw : (↑(ratio f) : ℝ≥0∞) * edist y x < (↑(ratio f) : ℝ≥0∞) * r
Tactic: rw [Metric.mem_eball, edist_eq f y x]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
⊢ (↑(ratio f) : ℝ≥0∞) * edist y x < (↑(ratio f) : ℝ≥0∞) * r
have h0 : (↑(ratio f) : ℝ≥0∞) ≠ 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r : ℝ≥0∞
y : α
hy : edist y x < r
h0 : (↑(ratio f) : ℝ≥0∞) ≠ 0
⊢ (↑(ratio f) : ℝ≥0∞) * edist y x < (↑(ratio f) : ℝ≥0∞) * r
have hinf : (↑(ratio f) : ℝ≥0∞) ≠ ∞
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ≥0∞
y : α
hy : y ∈ closedEBall x r'
⊢ (↑(ratio f) : ℝ≥0∞) * edist y x ≤ (↑(ratio f) : ℝ≥0∞) * r'
have bc : edist y x ≤ r'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
⊢ diam.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) = (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ
have rw : diam.{u_2} (α := β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) univ) = (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ
Tactic: rw [← image_univ, diam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
rw :
  diam.{u_2} (α := β) (image.{u_1, u_2} (α := α) (⇑f : (a : α) → β) univ) = (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ
⊢ diam.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑f : (a : α) → β)) = (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ
have rw₁ : (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ = (↑(ratio f) : ℝ) * diam.{u_1} (α := α) univ
Tactic: rw [← image_univ, diam_image]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
⊢ (↑(ratio f) : ℝ) * dist y x < (↑(ratio f) : ℝ) * r'
have ha : 0 < (↑(ratio f) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Dilation (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_4
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : FunLike F α β
inst_3 : DilationClass F α β
f : F
x : α
r' : ℝ
y : α
hy : y ∈ ball x r'
ha : 0 < (↑(ratio f) : ℝ)
⊢ (↑(ratio f) : ℝ) * dist y x < (↑(ratio f) : ℝ) * r'
have hbc : dist y x < r'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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, edist_eq' := edist_eq' : X ≃ᵈ Y } = { toEquiv := toEquiv_1, edist_eq' := edist_eq'_1 }
have e_toEquiv : toEquiv = toEquiv_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
have 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)
Tactic: refine ⟨(ratio e)⁻¹, inv_ne_zero <| ratio_ne_zero e, e.surjective.forall₂.2 fun x y ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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.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)
have simp_rw : edist x y = (↑(ratio e)⁻¹ : ℝ≥0∞) * ((↑(ratio e) : ℝ≥0∞) * edist x y)
Tactic: simp_rw [Equiv.toFun_as_coe, Equiv.symm_apply_apply, coe_toEquiv, edist_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
⊢ ratio (e.trans e') = ratio e * ratio e'
have pos : ∀ (hX : ∀ (x y : X), edist x y = 0 ∨ edist x y = ∞), ratio (e.trans e') = ratio e * ratio e'
Tactic: by_cases! hX : ∀ x y : X, edist x y = 0 ∨ edist x y = ∞
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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'
⊢ ratio (e.trans e') = ratio e * ratio e'
have neg : ∀ (hX : ∃ (x : X) (y : X), edist x y ≠ 0 ∧ edist x y ≠ ∞), ratio (e.trans e') = ratio e * ratio e'
Tactic: by_cases! hX : ∀ x y : X, edist x y = 0 ∨ edist x y = ∞
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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) = ∞
have refine_1 : ∀ (h : edist x y = 0), edist.{u_2} (α := Y) ((e : (a : X) → Y) x : Y) ((e : (a : X) → Y) y : Y) = 0
Tactic: refine (hX x y).imp (fun h ↦ ?_) fun h ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
⊢ 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) = ∞
have refine_2 : ∀ (h : edist x y = ∞), 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 ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (hypothesis)
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 = ∞
⊢ ratio (e.trans e') = ratio e * ratio e'
have hY : ∀ (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]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵈ Y
⊢ ratio e.symm * ratio e = 1
have rw : ratio (e.symm.trans e) = 1
Tactic: rw [← ratio_trans, symm_trans_self, ratio_refl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
⊢ ratio e.symm * ratio e = 1
have rw₁ : ratio (F := Y ≃ᵈ Y) (refl Y) = 1
Tactic: rw [← ratio_trans, symm_trans_self, ratio_refl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
⊢ ratio e.symm * ratio e = 1
have rw₂ : Eq (α := ℝ≥0) 1 1
Tactic: rw [← ratio_trans, symm_trans_self, ratio_refl]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
Goal:
X : Type u_1
inst : PseudoEMetricSpace X
e : X ≃ᵈ X
n : ℕ
⊢ Eq (α := (a : X) → X) (⇑(e ^ n) : (a : X) → X) (⇑e : (a : X) → X)^[n]
have 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]
Tactic: rw [← coe_toEquiv, ← toPerm_apply, map_pow, Equiv.Perm.coe_pow]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
Goal:
X : Type u_1
Y : Type u_2
inst : PseudoEMetricSpace X
inst_1 : PseudoEMetricSpace Y
e : X ≃ᵢ Y
⊢ ratio e.toDilationEquiv = 1
have rw : ratio e.toDilationEquiv.toDilation = 1
Tactic: rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
⊢ ratio e.toDilationEquiv = 1
have rw₁ : ratio (Isometry.toDilation (⇑e : (a : X) → Y) sorry) = 1
Tactic: rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
⊢ ratio e.toDilationEquiv = 1
have rw₂ : Eq (α := ℝ≥0) 1 1
Tactic: rw [← ratio_toDilation, IsometryEquiv.toDilationEquiv_toDilation, Isometry.toDilation_ratio]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
⊢ map (⇑e : (a : X) → Y) (cobounded X) = cobounded Y
have rw : map.{u_1, u_2} (α := X) (⇑e : (a : X) → Y) (comap (⇑e : (a : X) → Y) (cobounded Y)) = cobounded Y
Tactic: rw [← Dilation.comap_cobounded e, map_comap_of_surjective (EquivLike.surjective e)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.DilationEquiv (goal)
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
⊢ map (⇑e : (a : X) → Y) (cobounded X) = cobounded Y
have rw₁ : cobounded Y = cobounded Y
Tactic: rw [← Dilation.comap_cobounded e, map_comap_of_surjective (EquivLike.surjective e)]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ 𝓝 x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
have 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') < ε
Tactic: rw [equicontinuousAt_iff_pair]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
F : ι → β → α
x₀ : β
⊢ (∀ 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') < ε
have 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') < ε
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
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') < ε
⊢ (∀ 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') < ε
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
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 ∈ 𝓤 α
⊢ ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ (i : ι), (F i x, F i y) ∈ U
have 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
Tactic: rcases mem_uniformity_dist.mp hU with ⟨ε, hε, hεU⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
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
have 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
Tactic: refine Exists.imp (fun V => And.imp_right fun h => ?_) (H _ hε)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ EquicontinuousAt F x₀
have rw : ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
Tactic: rw [Metric.equicontinuousAt_iff_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
have h : ∀ (a : β),
  Membership.mem (γ := Set β)
    {x : β |
      x ∈ b ⁻¹' Set.Iio ε →
        Membership.mem (γ := Set β)
          {x : β |
            Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x) x} x →
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ (i : ι), dist (F i x₀) (F i x) < ε) x} x}
          x}
    a
Tactic: filter_upwards [b_lim (Iio_mem_nhds ε0), H] using fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
h :
  ∀ (a : β),
    Membership.mem (γ := Set β)
      {x : β |
        x ∈ b ⁻¹' Set.Iio ε →
          Membership.mem (γ := Set β)
            {x : β |
              Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x) x} x →
                Membership.mem (γ := Set β) {x : β | (fun (x : β) ↦ ∀ (i : ι), dist (F i x₀) (F i x) < ε) x} x}
            x}
      a
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
have h₁ : ∀ a ∈ b ⁻¹' Set.Iio ε, (∀ (i : ι), dist (F i x₀) (F i a) ≤ b a) → ∀ (i : ι), dist (F i x₀) (F i a) < ε
Tactic: filter_upwards [b_lim (Iio_mem_nhds ε0), H] using fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
⊢ UniformEquicontinuous F
have rw : ∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
Tactic: rw [Metric.uniformEquicontinuous_iff]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Equicontinuity (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
ι : Type u_4
inst_1 : PseudoMetricSpace β
b : ℝ → ℝ
b_lim : Tendsto b (𝓝 0) (𝓝 0)
F : ι → β → α
H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)
ε : ℝ
ε0 : ε > 0
⊢ ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
have rcases : ∀ (δ : ℝ) (δ0 : δ > 0) (hδ : ∀ ⦃x : ℝ⦄, dist x 0 < δ → dist (b x) 0 < ε),
  ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
Tactic: rcases tendsto_nhds_nhds.1 b_lim ε ε0 with ⟨δ, δ0, hδ⟩