awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
p q : ℝ × ℝ
⊢ dist (p.1 + p.2) (q.1 + q.2) ≤ (↑2 : ℝ) * dist p q
have simp : |p.1 - q.1 + (p.2 - q.2)| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|
Tactic: simp only [Real.dist_eq, Prod.dist_eq, NNReal.coe_ofNat,
      add_sub_add_comm, two_mul]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Monoid β
inst_3 : LipschitzMul β
p q : ℝ × ℝ
⊢ |p.1 - q.1 + (p.2 - q.2)| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|
have refine : |p.1 - q.1| + |p.2 - q.2| ≤ max |p.1 - q.1| |p.2 - q.2| + max |p.1 - q.1| |p.2 - q.2|
Tactic: refine le_trans (abs_add_le (p.1 - q.1) (p.2 - q.2)) ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
⊢ UniformContinuousOn (β := β) (Function.uncurry fun (x1 : α) (x2 : β) ↦ x1 • x2) s
have rcases : ∀ (C : ℝ) (hC₀ : 0 < C) (hC : s ⊆ Metric.ball 0 C),
  UniformContinuousOn (β := β) (Function.uncurry fun (x1 : α) (x2 : β) ↦ x1 • x2) s
Tactic: rcases hs.subset_ball_lt 0 0 with ⟨C, hC₀, hC⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
⊢ UniformContinuousOn (β := β) (Function.uncurry fun (x1 : α) (x2 : β) ↦ x1 • x2) s
have rw : ∀ ε > 0,
  ∃ δ > 0,
    ∀ x ∈ s,
      ∀ y ∈ s,
        dist x y ≤ δ →
          dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) x)
              (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) y) ≤
            ε
Tactic: rw [Metric.uniformContinuousOn_iff_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0,
    ∀ x ∈ s,
      ∀ y ∈ s,
        dist x y ≤ δ →
          dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) x)
              (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) y) ≤
            ε
have refine : ∀ (x x : α × β) (a : α) (b : β) (hab : (a, b) ∈ s) (x : α) (y : β) (hxy : (x, y) ∈ s)
  (h : dist (a, b) (x, y) ≤ ε / (2 * C)),
  dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
      (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
    ε
Tactic: refine ⟨ε / (2 * C), by positivity, fun ⟨a, b⟩ hab ⟨x, y⟩ hxy h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : (a, b) ∈ s
x : α
y : β
hxy : (x, y) ∈ s
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
      (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
    ε
have grw : ∀ (hab : dist (a, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C) (x : α) (y : β)
  (hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C) (h : dist (a, b) (x, y) ≤ ε / (2 * C)),
  dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
      (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
    ε
Tactic: grw [hC, Metric.mem_ball, Prod.dist_eq, max_lt_iff] at hab hxy
Cleared hypotheses: hab, x, y, hxy, h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist (a, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C
x : α
y : β
hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C
h : dist (a, b) (x, y) ≤ ε / (2 * C)
⊢ dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
      (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
    ε
have h₁ : dist (a, b).1 (x, y).1 ≤ ε / (2 * C) ∧ dist (a, b).2 (x, y).2 ≤ ε / (2 * C)
Tactic: rw [Prod.dist_eq, max_le_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist (a, b).1 0.1 < C ∧ dist (a, b).2 0.2 < C
x : α
y : β
hxy : dist (x, y).1 0.1 < C ∧ dist (x, y).2 0.2 < C
h : dist (a, b).1 (x, y).1 ≤ ε / (2 * C) ∧ dist (a, b).2 (x, y).2 ≤ ε / (2 * C)
⊢ dist (α := β) (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (a, b))
      (Function.uncurry (fun (x1 : α) (x2 : β) ↦ x1 • x2) (x, y)) ≤
    ε
have dsimp : dist (a • b) (x • y) ≤ ε
Tactic: dsimp at hab hxy h ⊢
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ dist (a • b) (x • y) ≤ ε
have grw : C * (ε / (2 * C)) + ε / (2 * C) * C ≤ ε
Tactic: grw [dist_triangle _ (a • y), dist_pair_smul, dist_smul_pair, hab.1, hxy.2, h.2, h.1]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
s : Set (α × β)
hs : IsBounded s
C : ℝ
hC₀ : 0 < C
hC : s ⊆ Metric.ball 0 C
ε : ℝ
hε : ε > 0
x_1 x_2 : α × β
a : α
b : β
hab : dist a 0 < C ∧ dist b 0 < C
x : α
y : β
hxy : dist x 0 < C ∧ dist y 0 < C
h : dist a x ≤ ε / (2 * C) ∧ dist b y ≤ ε / (2 * C)
⊢ C * (ε / (2 * C)) + ε / (2 * C) * C ≤ ε
have field_simp : HAdd.hAdd (α := ℝ) 1 1 ≤ 2
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : α × β) ↦ p.1 • p.2
have rw : ∀ (x : α × β), ContinuousAt (Y := β) (fun (p : α × β) ↦ p.1 • p.2) x
Tactic: rw [continuous_iff_continuousAt]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Algebra (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : Zero α
inst_3 : Zero β
inst_4 : SMul α β
inst_5 : IsBoundedSMul α β
x : α × β
⊢ ContinuousAt (Y := β) (fun (p : α × β) ↦ p.1 • p.2) x
have refine : Metric.ball 0 (dist x 0 + 1) ∈ 𝓝 x
Tactic: refine Metric.isBounded_ball (x := 0) (r := dist x 0 + 1) |>.uniformContinuousOn_smul
      |>.continuousOn |>.continuousAt ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
have simp : (∀ (x y : α), (↑(nndist x y) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist (f x) (f y)) : ℝ≥0∞)) ↔
  ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
Tactic: simp only [AntilipschitzWith, edist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), (↑(nndist x y) : ℝ≥0∞) ≤ (↑K : ℝ≥0∞) * (↑(nndist (f x) (f y)) : ℝ≥0∞)) ↔
    ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
have norm_cast : (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ AntilipschitzWith K f ↔ ∀ (x y : α), dist x y ≤ (↑K : ℝ) * dist (f x) (f y)
have simp : (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔
  ∀ (x y : α), (↑(nndist x y) : ℝ) ≤ (↑K : ℝ) * (↑(nndist (f x) (f y)) : ℝ)
Tactic: simp only [antilipschitzWith_iff_le_mul_nndist, dist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔
    ∀ (x y : α), (↑(nndist x y) : ℝ) ≤ (↑K : ℝ) * (↑(nndist (f x) (f y)) : ℝ)
have norm_cast : (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) ↔ ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x y : α
⊢ (↑K : ℝ≥0∞)⁻¹ * edist x y ≤ edist (f x) (f y)
have rw : edist x y / (↑K : ℝ≥0∞) ≤ edist (f x) (f y)
Tactic: rw [mul_comm, ← div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
⊢ edist x y ≤ (↑K : ℝ≥0∞) * ediam s
have grw : (↑K : ℝ≥0∞) * edist (f x) (f y) ≤ (↑K : ℝ≥0∞) * ediam s
Tactic: grw [hf x y, edist_le_ediam_of_mem (mem_preimage.1 hx) hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
s : Set β
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
grw : (↑K : ℝ≥0∞) * edist (f x) (f y) ≤ (↑K : ℝ≥0∞) * ediam s
⊢ edist x y ≤ (↑K : ℝ≥0∞) * ediam s
have grw₁ : (↑K : ℝ≥0∞) * ediam s ≤ (↑K : ℝ≥0∞) * ediam s
Tactic: grw [hf x y, edist_le_ediam_of_mem (mem_preimage.1 hx) hy]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
inst_2 : PseudoEMetricSpace γ
Kg : ℝ≥0
g : β → γ
hg : AntilipschitzWith Kg g
Kf : ℝ≥0
f : α → β
hf : AntilipschitzWith Kf f
x y : α
⊢ (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist (g (f x)) (g (f y))) = (↑(Kf * Kg) : ℝ≥0∞) * edist ((g ∘ f) x) ((g ∘ f) y)
have rw : (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist (g (f x)) (g (f y))) =
  (↑Kf : ℝ≥0∞) * ((↑Kg : ℝ≥0∞) * edist ((g ∘ f) x) ((g ∘ f) y))
Tactic: rw [ENNReal.coe_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
⊢ edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y
have this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist (f (g x)) (f (g y))
Tactic: have := hf (g x) (g y)
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist (f (g x)) (f (g y))
⊢ edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y
have rwa : ∀ (this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x (f (g y))), edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y
Tactic: rwa [hg x, hg y] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
g : β → α
hg : Function.RightInverse g f
x y : β
this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist (f (g x)) (f (g y))
rwa : ∀ (this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x (f (g y))), edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y
⊢ edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y
have rwa₁ : ∀ (this : edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y), edist (g x) (g y) ≤ (↑K : ℝ≥0∞) * edist x y
Tactic: rwa [hg x, hg y] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
⊢ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
have refine : ∀ (ε : ℝ≥0∞) (h₀ : 0 < ε),
  ∃ (i : ℝ≥0∞), 0 < i ∧ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < i} ⊆ {p : α × α | edist p.1 p.2 < ε}
Tactic: refine ((uniformity_basis_edist.comap _).le_basis_iff uniformity_basis_edist).2 fun ε h₀ => ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ ∃ (i : ℝ≥0∞), 0 < i ∧ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < i} ⊆ {p : α × α | edist p.1 p.2 < ε}
have refine : Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε} ⊆ {p : α × α | edist p.1 p.2 < ε}
Tactic: refine ⟨(↑K)⁻¹ * ε, ENNReal.mul_pos (ENNReal.inv_ne_zero.2 ENNReal.coe_ne_top) h₀.ne', ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
⊢ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε} ⊆ {p : α × α | edist p.1 p.2 < ε}
have refine : ∀ (x : α × α) (hx : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε}),
  (↑K : ℝ≥0∞) * edist (f x.1) (f x.2) < ε
Tactic: refine fun x hx => (hf x.1 x.2).trans_lt ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < (↑K : ℝ≥0∞)⁻¹ * ε}
⊢ (↑K : ℝ≥0∞) * edist (f x.1) (f x.2) < ε
have hx₁ : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < ε / (↑K : ℝ≥0∞)}
Tactic: rw [mul_comm, ← div_eq_mul_inv] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
ε : ℝ≥0∞
h₀ : 0 < ε
x : α × α
hx : x ∈ Prod.map f f ⁻¹' {p : β × β | edist p.1 p.2 < ε / (↑K : ℝ≥0∞)}
⊢ (↑K : ℝ≥0∞) * edist (f x.1) (f x.2) < ε
have rw : edist (f x.1) (f x.2) * (↑K : ℝ≥0∞) < ε
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (𝓝 (f x)) ≤ 𝓝 x
have simp : comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (𝓤 α)
Tactic: simp only [nhds_eq_comap_uniformity]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
hf : AntilipschitzWith K f
x : α
⊢ comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (𝓤 α)
have grw : comap f (comap (Prod.mk (f x)) (𝓤 β)) ≤ comap (Prod.mk x) (comap (Prod.map f f) (𝓤 β))
Tactic: grw [← hf.comap_uniformity_le]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
⊢ 0 < K
have by_contra! : ∀ (h₀ : K ≤ 0), False
Tactic: by_contra! h₀
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K ≤ 0
⊢ K = 0
have rwa : ∀ (h₀ : K = 0), K = 0
Tactic: rwa [le_zero_iff] at h₀
Cleared hypotheses: h₀
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K ≤ 0
⊢ False
have hf₁ : AntilipschitzWith 0 f
Tactic: obtain rfl : K = 0 := by rwa [le_zero_iff] at h₀
Cleared hypotheses: K, hf, h₀
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
β : Type u_2
inst : PseudoEMetricSpace β
K : ℝ≥0
α : Type u_4
inst_1 : EMetricSpace α
inst_2 : Nontrivial α
f : α → β
hf : AntilipschitzWith K f
h₀ : K ≤ 0
hf₁ : AntilipschitzWith 0 f
⊢ False
have h₁ : LE.le (α := ℝ≥0) 0 0
Tactic: obtain rfl : K = 0 := by rwa [le_zero_iff] at h₀
Cleared hypotheses: K, hf, h₀
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
⊢ ProperSpace β
have refine : ∀ (x₀ : β) (r : ℝ), IsCompact (closedBall x₀ r)
Tactic: refine ⟨fun x₀ r => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
⊢ IsCompact (closedBall x₀ r)
have A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
Tactic: have A : IsClosed K := isClosed_closedBall.preimage f_cont
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
⊢ IsCompact (closedBall x₀ r)
have B : Bornology.IsBounded K
Tactic: have B : IsBounded K := hK.isBounded_preimage isBounded_closedBall
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
⊢ IsCompact (closedBall x₀ r)
have this : IsCompact K
Tactic: have : IsCompact K := isCompact_iff_isClosed_bounded.2 ⟨A, B⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
β : Type u_2
inst : PseudoMetricSpace β
α : Type u_4
inst_1 : MetricSpace α
K_1 : ℝ≥0
f : α → β
inst_2 : ProperSpace α
hK : AntilipschitzWith K_1 f
f_cont :
  Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hf : Function.Surjective f
x₀ : β
r : ℝ
K : Set α := f ⁻¹' closedBall x₀ r
A : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] K
B : Bornology.IsBounded K
this : IsCompact K
⊢ IsCompact (closedBall x₀ r)
have h : closedBall x₀ r = f '' K
Tactic: convert! this.image f_cont
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : Bornology.IsBounded (image2 f s t)
⊢ Bornology.IsBounded s ∨ Bornology.IsBounded t
have contrapose! : ∀ (hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t), ¬Bornology.IsBounded (image2 f s t)
Tactic: contrapose! hst
Cleared hypotheses: hst
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
⊢ ¬Bornology.IsBounded (image2 f s t)
have obtain : ∀ (b : β) (hb : b ∈ t), ¬Bornology.IsBounded (image2 f s t)
Tactic: obtain ⟨b, hb⟩ : t.Nonempty := nonempty_of_not_isBounded hst.2
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded (image2 f s {b})
⊢ False
have apply : Bornology.IsBounded s
Tactic: apply hst.1
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded (image2 f s {b})
⊢ Bornology.IsBounded s
have h₁ : Bornology.IsBounded.{u_3} (α := γ) ((fun (a : α) ↦ f a b) '' s)
Tactic: rw [Set.image2_singleton_right] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Antilipschitz (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : PseudoMetricSpace γ
f : α → β → γ
K₁ : ℝ≥0
hf : ∀ (b : β), AntilipschitzWith.{u_1, u_3} (β := γ) K₁ fun (a : α) ↦ f a b
s : Set α
t : Set β
hst : ¬Bornology.IsBounded s ∧ ¬Bornology.IsBounded t
b : β
hb : b ∈ t
h : Bornology.IsBounded.{u_3} (α := γ) ((fun (a : α) ↦ f a b) '' s)
⊢ Bornology.IsBounded s
have h₁ : Bornology.IsBounded.{u_1} (α := α) (preimage.{u_1, u_3} (β := γ) (fun (a : α) ↦ f a b) ((fun (a : α) ↦ f a b) '' s))
Tactic: replace h := (hf b).isBounded_preimage h
Cleared hypotheses: h