awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t1
t2 : Set (Completion α × Completion α)
ht2 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t2
ht :
  t1 ×ˢ t2 ⊆
    preimage (β := (Completion α × Completion α) × Completion α × Completion α)
      (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
mpr : t1 ⊆ s
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s

Tactic:
refine mem_of_superset ht1 ?_

Premises used: Filter.mem_of_superset
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t1
t2 : Set (Completion α × Completion α)
ht2 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t2
ht :
  t1 ×ˢ t2 ⊆
    preimage (β := (Completion α × Completion α) × Completion α × Completion α)
      (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
a b : Completion α
hab : (a, b) ∈ t1
⊢ ((a, b), a, a) ∈ t1 ×ˢ t2

Tactic:
have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this_1 : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t1
t2 : Set (Completion α × Completion α)
ht2 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t2
ht :
  t1 ×ˢ t2 ⊆
    preimage (β := (Completion α × Completion α) × Completion α × Completion α)
      (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
⊢ |dist a b| < ε

Tactic:
simpa [r, Completion.dist_self, Real.dist_eq, Completion.dist_comm] using ht this

Premises used: Real.dist_eq, UniformSpace.Completion.dist_comm, UniformSpace.Completion.dist_self
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this_1 : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t1
t2 : Set (Completion α × Completion α)
ht2 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t2
ht :
  t1 ×ˢ t2 ⊆
    preimage (β := (Completion α × Completion α) × Completion α × Completion α)
      (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
a b : Completion α
hab : (a, b) ∈ t1
this : ((a, b), a, a) ∈ t1 ×ˢ t2
⊢ dist a b < ε

Tactic:
exact lt_of_le_of_lt (le_abs_self _)
        (by simpa [r, Completion.dist_self, Real.dist_eq, Completion.dist_comm] using ht this)

Premises used: lt_of_le_of_lt, le_abs_self
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t1
t2 : Set (Completion α × Completion α)
ht2 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t2
ht :
  t1 ×ˢ t2 ⊆
    preimage (β := (Completion α × Completion α) × Completion α × Completion α)
      (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
⊢ ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε

Tactic:
have A : ∀ a b : Completion α, (a, b) ∈ t1 → dist a b < ε := by
      intro a b hab
      have : ((a, b), (a, a)) ∈ t1 ×ˢ t2 := ⟨hab, refl_mem_uniformity ht2⟩
      exact lt_of_le_of_lt (le_abs_self _)
        (by simpa [r, Completion.dist_self, Real.dist_eq, Completion.dist_comm] using ht this)
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
ε : ℝ
εpos : ε > 0
hε : ∀ {a b : Completion α}, dist a b < ε → (a, b) ∈ s
r : Set (ℝ × ℝ) := {p : ℝ × ℝ | dist p.1 p.2 < ε}
this : r ∈ 𝓤 ℝ
t1 : Set (Completion α × Completion α)
ht1 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t1
t2 : Set (Completion α × Completion α)
ht2 : Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) t2
ht :
  t1 ×ˢ t2 ⊆
    preimage (β := (Completion α × Completion α) × Completion α × Completion α)
      (fun (p : (Completion α × Completion α) × Completion α × Completion α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2))
      {x : (Completion α × Completion α) × Completion α × Completion α | (dist x.1.1 x.1.2, dist x.2.1 x.2.2) ∈ r}
A : ∀ (a b : Completion α), (a, b) ∈ t1 → dist a b < ε
⊢ t1 ⊆ s

Tactic:
grind
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
h :
  ∀ (s : Set (Completion α × Completion α)),
    Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
      Membership.mem (γ := Filter (Completion α × Completion α))
        (⨅ (ε : { ε : ℝ // 0 < ε }), 𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)}) s
⊢ Eq.{u + 1} (α := Filter (Completion α × Completion α)) (𝓤 (Completion α))
    (⨅ (ε : { ε : ℝ // 0 < ε }), 𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)})

Tactic:
ext s
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
h :
  Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    ∃ (i : { ε : ℝ // 0 < ε }),
      Membership.mem (γ := Filter (Completion α × Completion α))
        (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑i : ℝ)}) s
h₁ :
  Directed (fun (x1 x2 : Filter (Completion α × Completion α)) ↦ x1 ≥ x2) fun (ε : { ε : ℝ // 0 < ε }) ↦
    𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)}
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    Membership.mem (γ := Filter (Completion α × Completion α))
      (⨅ (ε : { ε : ℝ // 0 < ε }), 𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)}) s

Tactic:
rw [mem_iInf_of_directed]

Premises used: Filter.mem_iInf_of_directed
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
⊢ Membership.mem (γ := Filter (Completion α × Completion α)) (𝓤 (Completion α)) s ↔
    ∃ (i : { ε : ℝ // 0 < ε }),
      Membership.mem (γ := Filter (Completion α × Completion α))
        (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑i : ℝ)}) s

Tactic:
simp [Completion.mem_uniformity_dist, subset_def]

Premises used: UniformSpace.Completion.mem_uniformity_dist, Set.subset_def
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
h :
  (fun (x1 x2 : Filter (Completion α × Completion α)) ↦ x1 ≥ x2)
      ((fun (ε : { ε : ℝ // 0 < ε }) ↦
          (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
        (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) r hr))
      ((fun (ε : { ε : ℝ // 0 < ε }) ↦
          (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
        (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) (min r p) ⋯)) ∧
    (fun (x1 x2 : Filter (Completion α × Completion α)) ↦ x1 ≥ x2)
      ((fun (ε : { ε : ℝ // 0 < ε }) ↦
          (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
        (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) p hp))
      ((fun (ε : { ε : ℝ // 0 < ε }) ↦
          (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
        (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) (min r p) ⋯))
⊢ ∃ (z : { ε : ℝ // 0 < ε }),
    (fun (x1 x2 : Filter (Completion α × Completion α)) ↦ x1 ≥ x2)
        ((fun (ε : { ε : ℝ // 0 < ε }) ↦
            (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
          (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) r hr))
        ((fun (ε : { ε : ℝ // 0 < ε }) ↦
            (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
          z) ∧
      (fun (x1 x2 : Filter (Completion α × Completion α)) ↦ x1 ≥ x2)
        ((fun (ε : { ε : ℝ // 0 < ε }) ↦
            (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
          (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) p hp))
        ((fun (ε : { ε : ℝ // 0 < ε }) ↦
            (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
          z)

Tactic:
use ⟨min r p, lt_min hr hp⟩
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < p
⊢ (fun (x1 x2 : Filter (Completion α × Completion α)) ↦ x1 ≥ x2)
      ((fun (ε : { ε : ℝ // 0 < ε }) ↦
          (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
        (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) r hr))
      ((fun (ε : { ε : ℝ // 0 < ε }) ↦
          (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
        (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) (min r p) ⋯)) ∧
    (fun (x1 x2 : Filter (Completion α × Completion α)) ↦ x1 ≥ x2)
      ((fun (ε : { ε : ℝ // 0 < ε }) ↦
          (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
        (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) p hp))
      ((fun (ε : { ε : ℝ // 0 < ε }) ↦
          (𝓟 {p : Completion α × Completion α | dist p.1 p.2 < (↑ε : ℝ)} : Filter (Completion α × Completion α)))
        (Subtype.mk (p := fun (ε : ℝ) ↦ 0 < ε) (min r p) ⋯))

Tactic:
simp +contextual
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ Eq.{u + 1} (α := Filter (Completion α × Completion α)) (𝓤 (Completion α))
    (⨅ (ε : ℝ), ⨅ (_ : ε > 0), 𝓟 {p : Completion α × Completion α | dist p.1 p.2 < ε})

Tactic:
simpa [iInf_subtype] using @Completion.uniformity_dist' α _

Premises used: iInf_subtype, UniformSpace.Completion.uniformity_dist'
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
⊢ Isometry.{u, u} (α := α) (β := Completion α) coe'

Tactic:
Isometry.of_dist_eq Completion.dist_eq

Premises used: UniformSpace.Completion.dist_eq, Isometry.of_dist_eq
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
inst : PseudoMetricSpace α
x y : α
⊢ edist (α := Completion α) (↑x : Completion α) (↑y : Completion α) = edist x y

Tactic:
coe_isometry x y

Premises used: UniformSpace.Completion.coe_isometry
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c : M
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α) ↦ dist (c • x.1) (c • x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c : M
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α) ↦ dist c 0 * dist x.1 x.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c : M
⊢ IsClosed.{u} (X := Completion α × Completion α)
    {x : Completion α × Completion α | dist (c • x.1) (c • x.2) ≤ dist c 0 * dist x.1 x.2}

Tactic:
exact isClosed_le (by fun_prop) (by fun_prop)

Premises used: isClosed_le
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c : M
x₁ x₂ : α
ih : dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂
⊢ dist (HSMul.hSMul (β := Completion α) c (↑x₁ : Completion α))
      (HSMul.hSMul (β := Completion α) c (↑x₂ : Completion α)) ≤
    dist c 0 * dist (α := Completion α) (↑x₁ : Completion α) (↑x₂ : Completion α)

Tactic:
rw [← coe_smul, ← coe_smul, Completion.dist_eq, Completion.dist_eq]

Premises used: UniformSpace.Completion.dist_eq, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c : M
x₁ x₂ : α
⊢ dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂

Tactic:
dist_smul_pair c x₁ x₂

Premises used: dist_smul_pair
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c : M
x₁ x₂ : α
⊢ dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂

Tactic:
exact dist_smul_pair c x₁ x₂

Premises used: dist_smul_pair
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c : M
x₁ x₂ : Completion α
hp :
  IsClosed.{u} (X := Completion α × Completion α)
    {x : Completion α × Completion α | dist (c • x.1) (c • x.2) ≤ dist c 0 * dist x.1 x.2}
ih :
  ∀ (x₁ x₂ : α),
    dist (HSMul.hSMul (β := Completion α) c (↑x₁ : Completion α))
        (HSMul.hSMul (β := Completion α) c (↑x₂ : Completion α)) ≤
      dist c 0 * dist (α := Completion α) (↑x₁ : Completion α) (↑x₂ : Completion α)
⊢ dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂

Tactic:
induction x₁, x₂ using induction_on₂ with
    | hp => exact isClosed_le (by fun_prop) (by fun_prop)
    | ih x₁ x₂ =>
      rw [← coe_smul, ← coe_smul, Completion.dist_eq, Completion.dist_eq]
      exact dist_smul_pair c x₁ x₂

Premises used: UniformSpace.Completion.dist_eq, isClosed_le, UniformSpace.Completion.coe_smul, dist_smul_pair
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c₁ c₂ : M
⊢ Continuous (Y := ℝ) fun (a : Completion α) ↦ dist (c₁ • a) (c₂ • a)

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c₁ c₂ : M
⊢ Continuous (Y := ℝ) fun (a : Completion α) ↦ dist c₁ c₂ * dist a 0

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c₁ c₂ : M
⊢ IsClosed.{u} (X := Completion α) {a : Completion α | dist (c₁ • a) (c₂ • a) ≤ dist c₁ c₂ * dist a 0}

Tactic:
exact isClosed_le (by fun_prop) (by fun_prop)

Premises used: isClosed_le
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c₁ c₂ : M
x : α
ih : dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0
⊢ dist (HSMul.hSMul (β := Completion α) c₁ (↑x : Completion α))
      (HSMul.hSMul (β := Completion α) c₂ (↑x : Completion α)) ≤
    dist c₁ c₂ * dist (α := Completion α) (↑x : Completion α) 0

Tactic:
rw [← coe_smul, ← coe_smul, Completion.dist_eq, ← coe_zero, Completion.dist_eq]

Premises used: UniformSpace.Completion.dist_eq, UniformSpace.Completion.coe_zero, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c₁ c₂ : M
x : α
⊢ dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0

Tactic:
dist_pair_smul c₁ c₂ x

Premises used: dist_pair_smul
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c₁ c₂ : M
x : α
⊢ dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0

Tactic:
exact dist_pair_smul c₁ c₂ x

Premises used: dist_pair_smul
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
M : Type u_1
inst_1 : Zero M
inst_2 : Zero α
inst_3 : SMul M α
inst_4 : PseudoMetricSpace M
inst_5 : IsBoundedSMul M α
c₁ c₂ : M
x : Completion α
hp : IsClosed.{u} (X := Completion α) {a : Completion α | dist (c₁ • a) (c₂ • a) ≤ dist c₁ c₂ * dist a 0}
ih :
  ∀ (x : α),
    dist (HSMul.hSMul (β := Completion α) c₁ (↑x : Completion α))
        (HSMul.hSMul (β := Completion α) c₂ (↑x : Completion α)) ≤
      dist c₁ c₂ * dist (α := Completion α) (↑x : Completion α) 0
⊢ dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0

Tactic:
induction x using induction_on with
    | hp => exact isClosed_le (by fun_prop) (by fun_prop)
    | ih x =>
      rw [← coe_smul, ← coe_smul, Completion.dist_eq, ← coe_zero, Completion.dist_eq]
      exact dist_pair_smul c₁ c₂ x

Premises used: dist_pair_smul, UniformSpace.Completion.dist_eq, isClosed_le, UniformSpace.Completion.coe_zero, UniformSpace.Completion.coe_smul
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : MetricSpace β
inst_2 : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α) ↦
    dist (Completion.extension f x.1) (Completion.extension f x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : MetricSpace β
inst_2 : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α) ↦ (↑K : ℝ) * dist x.1 x.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : MetricSpace β
inst_2 : CompleteSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
x y : Completion α
⊢ ∀ (a b : α),
    dist (Completion.extension f (↑a : Completion α)) (Completion.extension f (↑b : Completion α)) ≤
      (↑K : ℝ) * dist (α := Completion α) (↑a : Completion α) (↑b : Completion α)

Tactic:
simpa only [extension_coe h.uniformContinuous, Completion.dist_eq] using h.dist_le_mul

Premises used: LipschitzWith.dist_le_mul, UniformSpace.Completion.extension_coe, UniformSpace.Completion.dist_eq, LipschitzWith.uniformContinuous
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
K : ℝ≥0
h : LipschitzWith K f
⊢ LipschitzWith (α := Completion α) (β := Completion β) K (Completion.map f)

Tactic:
one_mul K ▸ (coe_isometry.lipschitz.comp h).completion_extension

Premises used: LipschitzWith.completion_extension, Eq.rec, UniformSpace.Completion.coe_isometry, Isometry.lipschitz, LipschitzWith.comp, one_mul
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : CompleteSpace β
inst_3 : T0Space β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α) ↦
    dist (Completion.extension f x.1) (Completion.extension f x.2)

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : CompleteSpace β
inst_3 : T0Space β
f : α → β
h : Isometry f
x y : Completion α
⊢ Continuous (Y := ℝ) fun (x : Completion α × Completion α) ↦ dist x.1 x.2

Tactic:
fun_prop
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
inst_2 : CompleteSpace β
inst_3 : T0Space β
f : α → β
h : Isometry f
x y : Completion α
x_1 x_2 : α
⊢ dist (Completion.extension f (↑x_1 : Completion α)) (Completion.extension f (↑x_2 : Completion α)) =
    dist (α := Completion α) (↑x_1 : Completion α) (↑x_2 : Completion α)

Tactic:
simp only [extension_coe h.uniformContinuous, Completion.dist_eq, h.dist_eq]

Premises used: Isometry.uniformContinuous, UniformSpace.Completion.extension_coe, UniformSpace.Completion.dist_eq, Isometry.dist_eq
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : PseudoMetricSpace β
f : α → β
h : Isometry f
⊢ Isometry (α := Completion α) (β := Completion β) (Completion.map f)

Tactic:
(coe_isometry.comp h).completion_extension

Premises used: Isometry.comp, UniformSpace.Completion.map, UniformSpace.Completion.coe', UniformSpace.Completion.coe_isometry, Isometry.completion_extension, Quotient, SeparationQuotient, SeparationQuotient.mk, AbstractCompletion.map, UniformSpace.Completion
-- Module: Mathlib.Topology.MetricSpace.Completion
Goal:
α : Type u
β : Type v
inst : PseudoMetricSpace α
inst_1 : Ring α
inst_2 : IsTopologicalRing α
inst_3 : IsUniformAddGroup α
inst_4 : Ring β
inst_5 : PseudoMetricSpace β
inst_6 : IsUniformAddGroup β
inst_7 : IsTopologicalRing β
inst_8 : CompleteSpace β
inst_9 : T0Space β
f : α →+* β
h : Isometry.{u, v} (α := α) (β := β) (⇑f : (a : α) → β)
x : α
⊢ Eq.{v + 1} (α := β) ((h.extensionHom : (a : Completion α) → β) (↑x : Completion α) : β) ((f : (a : α) → β) x : β)

Tactic:
Completion.extensionHom_coe f h.continuous _

Premises used: UniformSpace.Completion.extensionHom_coe, Isometry.continuous