awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
Goal:
α : Type u
inst : PseudoMetricSpace α
s : Set (Completion α × Completion α)
r : ℝ
hr : 0 < r
p : ℝ
hp : 0 < 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)
have 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) sorry)) ∧
  (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) sorry))
Tactic: use ⟨min r p, lt_min hr hp⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 (HSMul.hSMul (β := Completion α) c (↑x₁ : Completion α))
      (HSMul.hSMul (β := Completion α) c (↑x₂ : Completion α)) ≤
    dist c 0 * dist (α := Completion α) (↑x₁ : Completion α) (↑x₂ : Completion α)
have ih : dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂
Tactic: rw [← coe_smul, ← coe_smul, Completion.dist_eq, Completion.dist_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 α
⊢ dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂
have hp : IsClosed.{u} (X := Completion α × Completion α)
  {x : Completion α × Completion α | dist (c • x.1) (c • x.2) ≤ dist c 0 * dist x.1 x.2}
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₂
Cleared hypotheses: x₁, x₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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}
⊢ dist (c • x₁) (c • x₂) ≤ dist c 0 * dist x₁ x₂
have 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 α)
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₂
Cleared hypotheses: x₁, x₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 (HSMul.hSMul (β := Completion α) c₁ (↑x : Completion α))
      (HSMul.hSMul (β := Completion α) c₂ (↑x : Completion α)) ≤
    dist c₁ c₂ * dist (α := Completion α) (↑x : Completion α) 0
have ih : dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0
Tactic: rw [← coe_smul, ← coe_smul, Completion.dist_eq, ← coe_zero, Completion.dist_eq]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 α
⊢ dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0
have hp : IsClosed.{u} (X := Completion α) {a : Completion α | dist (c₁ • a) (c₂ • a) ≤ dist c₁ c₂ * dist a 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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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}
⊢ dist (c₁ • x) (c₂ • x) ≤ dist c₁ c₂ * dist x 0
have ih : ∀ (x : α),
  dist (HSMul.hSMul (β := Completion α) c₁ (↑x : Completion α))
      (HSMul.hSMul (β := Completion α) c₂ (↑x : Completion α)) ≤
    dist c₁ c₂ * dist (α := Completion α) (↑x : Completion α) 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
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 β
f : α →+* β
h : Isometry.{u, v} (α := α) (β := β) (⇑f : (a : α) → β)
x y : Completion α
⊢ dist.{v} (α := Completion β)
      (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x :
        Completion β)
      (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β) y :
        Completion β) =
    dist x y
have hp : IsClosed.{u} (X := Completion α × Completion α)
  {x : Completion α × Completion α |
    dist.{v} (α := Completion β)
        (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x.1 :
          Completion β)
        (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x.2 :
          Completion β) =
      dist x.1 x.2}
Tactic: induction x, y using induction_on₂ with
    | hp => exact isClosed_eq (continuous_dist.comp₂ (continuous_map.comp continuous_fst)
        (continuous_map.comp continuous_snd)) (by fun_prop)
    | ih x y => simp only [Completion.dist_eq, mapRingHom_coe, h.dist_eq]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Completion (goal)
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 β
f : α →+* β
h : Isometry.{u, v} (α := α) (β := β) (⇑f : (a : α) → β)
x y : Completion α
hp :
  IsClosed.{u} (X := Completion α × Completion α)
    {x : Completion α × Completion α |
      dist.{v} (α := Completion β)
          (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x.1 :
            Completion β)
          (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x.2 :
            Completion β) =
        dist x.1 x.2}
⊢ dist.{v} (α := Completion β)
      (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β) x :
        Completion β)
      (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β) y :
        Completion β) =
    dist x y
have ih : ∀ (x y : α),
  dist.{v} (α := Completion β)
      (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
          (↑x : Completion α) :
        Completion β)
      (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
          (↑y : Completion α) :
        Completion β) =
    dist (α := Completion α) (↑x : Completion α) (↑y : Completion α)
Tactic: induction x, y using induction_on₂ with
    | hp => exact isClosed_eq (continuous_dist.comp₂ (continuous_map.comp continuous_fst)
        (continuous_map.comp continuous_snd)) (by fun_prop)
    | ih x y => simp only [Completion.dist_eq, mapRingHom_coe, h.dist_eq]
Cleared hypotheses: x, y
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
⊢ Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
have refine : ∀ (h : Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)) (i₁ i₂ : ι),
  edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Tactic: refine ⟨fun h ↦ fun _ _ _ ↦ h _ _, fun h ↦ fun i₁ i₂ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
h : Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
have pos : ∀ (hi : i₁ = i₂), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Tactic: by_cases hi : i₁ = i₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
h : Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
i₁ i₂ : ι
pos : ∀ (hi : i₁ = i₂), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
have neg : ∀ (hi : ¬i₁ = i₂), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Tactic: by_cases hi : i₁ = i₂
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
E : Type u_7
inst_2 : EquivLike E ι' ι
f : E
v₁ : ι → P₁
v₂ : ι → P₂
⊢ Congruent.{u_2, u_3, u_4} (ι := ι') (v₁ ∘ (⇑f : (a : ι') → ι)) (v₂ ∘ (⇑f : (a : ι') → ι)) ↔ v₁ ≅ v₂
have refine : ∀ (h : Congruent.{u_2, u_3, u_4} (ι := ι') (v₁ ∘ (⇑f : (a : ι') → ι)) (v₂ ∘ (⇑f : (a : ι') → ι))) (i₁ i₂ : ι),
  edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Tactic: refine ⟨fun h i₁ i₂ ↦ ?_, fun h ↦ index_map h f⟩
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
f : P₂ → P₃
hf : Isometry f
⊢ v₁ ≅ f ∘ v₂ ↔ v₁ ≅ v₂
have rw : f ∘ v₂ ≅ v₁ ↔ v₁ ≅ v₂
Tactic: rw [congruent_comm, comp_left_iff hf, congruent_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
f : P₂ → P₃
hf : Isometry f
rw : f ∘ v₂ ≅ v₁ ↔ v₁ ≅ v₂
⊢ v₁ ≅ f ∘ v₂ ↔ v₁ ≅ v₂
have rw₁ : v₂ ≅ v₁ ↔ v₁ ≅ v₂
Tactic: rw [congruent_comm, comp_left_iff hf, congruent_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
f : P₂ → P₃
hf : Isometry f
rw : f ∘ v₂ ≅ v₁ ↔ v₁ ≅ v₂
rw₁ : v₂ ≅ v₁ ↔ v₁ ≅ v₂
⊢ v₁ ≅ f ∘ v₂ ↔ v₁ ≅ v₂
have rw₂ : v₁ ≅ v₂ ↔ v₁ ≅ v₂
Tactic: rw [congruent_comm, comp_left_iff hf, congruent_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x x_1 : ι
⊢ edist (v₁ x) (v₁ x_1) = edist (v₂ x) (v₂ x_1) ↔ nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1)
have rw : (↑(nndist (v₁ x) (v₁ x_1)) : ENNReal) = (↑(nndist (v₂ x) (v₂ x_1)) : ENNReal) ↔
  nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1)
Tactic: rw [edist_nndist, edist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x x_1 : ι
⊢ (↑(nndist (v₁ x) (v₁ x_1)) : ENNReal) = (↑(nndist (v₂ x) (v₂ x_1)) : ENNReal) ↔
    nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1)
have norm_cast : nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1) ↔ nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) ↦ nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)
have simp_rw : (Pairwise fun (i₁ i₂ : ι) ↦ (↑(nndist (v₁ i₁) (v₁ i₂)) : ENNReal) = (↑(nndist (v₂ i₁) (v₂ i₂)) : ENNReal)) ↔
  Pairwise fun (i₁ i₂ : ι) ↦ nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)
Tactic: simp_rw [congruent_iff_pairwise_edist_eq, edist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x x_1 : ι
⊢ nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1) ↔ dist (v₁ x) (v₁ x_1) = dist (v₂ x) (v₂ x_1)
have rw : nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1) ↔ (↑(nndist (v₁ x) (v₁ x_1)) : ℝ) = (↑(nndist (v₂ x) (v₂ x_1)) : ℝ)
Tactic: rw [dist_nndist, dist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
x x_1 : ι
⊢ nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1) ↔ (↑(nndist (v₁ x) (v₁ x_1)) : ℝ) = (↑(nndist (v₂ x) (v₂ x_1)) : ℝ)
have norm_cast : nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1) ↔ nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Congruence (goal)
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)
have simp_rw : (Pairwise fun (i₁ i₂ : ι) ↦ nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)) ↔
  Pairwise fun (i₁ i₂ : ι) ↦ (↑(nndist (v₁ i₁) (v₁ i₂)) : ℝ) = (↑(nndist (v₂ i₁) (v₂ i₂)) : ℝ)
Tactic: simp_rw [congruent_iff_pairwise_nndist_eq, dist_nndist]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
⊢ edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist y (f y) + edist (f x) (f y)
have rw : edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist (f y) y + edist (f x) (f y)
Tactic: rw [edist_comm y, add_right_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
rw : edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist (f y) y + edist (f x) (f y)
⊢ edist x (f x) + edist (f x) (f y) + edist (f y) y = edist x (f x) + edist y (f y) + edist (f x) (f y)
have rw₁ : edist x (f x) + edist (f y) y + edist (f x) (f y) = edist x (f x) + edist (f y) y + edist (f x) (f y)
Tactic: rw [edist_comm y, add_right_comm]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
this : edist x y ≤ edist x (f x) + edist y (f y) + (↑K : ℝ≥0∞) * edist x y
⊢ edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - (↑K : ℝ≥0∞))
have rwa : edist x y * (1 - (↑K : ℝ≥0∞)) ≤ edist x (f x) + edist y (f y)
Tactic: rwa [ENNReal.le_div_iff_mul_le (Or.inl hf.one_sub_K_ne_zero) (Or.inl one_sub_K_ne_top),
      mul_comm, ENNReal.sub_mul fun _ _ ↦ h, one_mul, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
this : edist x y ≤ edist x (f x) + edist y (f y) + (↑K : ℝ≥0∞) * edist x y
rwa : edist x y * (1 - (↑K : ℝ≥0∞)) ≤ edist x (f x) + edist y (f y)
⊢ edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - (↑K : ℝ≥0∞))
have rwa₁ : (1 - (↑K : ℝ≥0∞)) * edist x y ≤ edist x (f x) + edist y (f y)
Tactic: rwa [ENNReal.le_div_iff_mul_le (Or.inl hf.one_sub_K_ne_zero) (Or.inl one_sub_K_ne_top),
      mul_comm, ENNReal.sub_mul fun _ _ ↦ h, one_mul, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
this : edist x y ≤ edist x (f x) + edist y (f y) + (↑K : ℝ≥0∞) * edist x y
rwa : edist x y * (1 - (↑K : ℝ≥0∞)) ≤ edist x (f x) + edist y (f y)
rwa₁ : (1 - (↑K : ℝ≥0∞)) * edist x y ≤ edist x (f x) + edist y (f y)
⊢ edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - (↑K : ℝ≥0∞))
have rwa₂ : 1 * edist x y - (↑K : ℝ≥0∞) * edist x y ≤ edist x (f x) + edist y (f y)
Tactic: rwa [ENNReal.le_div_iff_mul_le (Or.inl hf.one_sub_K_ne_zero) (Or.inl one_sub_K_ne_top),
      mul_comm, ENNReal.sub_mul fun _ _ ↦ h, one_mul, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
this : edist x y ≤ edist x (f x) + edist y (f y) + (↑K : ℝ≥0∞) * edist x y
rwa : edist x y * (1 - (↑K : ℝ≥0∞)) ≤ edist x (f x) + edist y (f y)
rwa₁ : (1 - (↑K : ℝ≥0∞)) * edist x y ≤ edist x (f x) + edist y (f y)
rwa₂ : 1 * edist x y - (↑K : ℝ≥0∞) * edist x y ≤ edist x (f x) + edist y (f y)
⊢ edist x y ≤ (edist x (f x) + edist y (f y)) / (1 - (↑K : ℝ≥0∞))
have rwa₃ : edist x y - (↑K : ℝ≥0∞) * edist x y ≤ edist x (f x) + edist y (f y)
Tactic: rwa [ENNReal.le_div_iff_mul_le (Or.inl hf.one_sub_K_ne_zero) (Or.inl one_sub_K_ne_top),
      mul_comm, ENNReal.sub_mul fun _ _ ↦ h, one_mul, tsub_le_iff_right]
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
⊢ x = y ∨ edist x y = ∞
have refine : ∀ (h : ¬edist x y = ∞), edist x y ≤ 0
Tactic: refine or_iff_not_imp_right.2 fun h ↦ edist_le_zero.1 ?_
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
⊢ edist x (efixedPoint f hf x hx) ≤ edist x (f x) / (1 - (↑K : ℝ≥0∞))
have h : edist x (f x) = edist x (f x) * HPow.hPow (β := ℕ) (↑K : ℝ≥0∞) 0
Tactic: convert! hf.apriori_edist_iterate_efixedPoint_le hx 0
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
⊢ efixedPoint f hf x hx = efixedPoint f hf y hy
have refine_1 : IsFixedPt f (efixedPoint f hf x hx)
Tactic: refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
refine_1 : IsFixedPt f (efixedPoint f hf x hx)
⊢ efixedPoint f hf x hx = efixedPoint f hf y hy
have refine_2 : IsFixedPt f (efixedPoint f hf y hy)
Tactic: refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
refine_1 : IsFixedPt f (efixedPoint f hf x hx)
refine_2 : IsFixedPt f (efixedPoint f hf y hy)
⊢ efixedPoint f hf x hx = efixedPoint f hf y hy
have refine_3 : ∀ (h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞),
  edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ∞
Tactic: refine (hf.eq_or_edist_eq_top_of_fixedPoints ?_ ?_).elim id fun h' ↦ False.elim (ne_of_lt ?_ h')
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) < ∞
have refine_3 : (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) (efixedPoint f hf y hy)
Tactic: change Metric.edistLtTopSetoid _ _
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
⊢ (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) (efixedPoint f hf y hy)
have trans : (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) x
Tactic: trans x
-- Lean 4 proof step from Mathlib.Topology.MetricSpace.Contracting (goal)
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
y : α
hy : edist y (f y) ≠ ∞
h : edist x y ≠ ∞
h' : edist (efixedPoint f hf x hx) (efixedPoint f hf y hy) = ∞
trans : (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) x
⊢ (Metric.edistLtTopSetoid : α → α → Prop) (efixedPoint f hf x hx) (efixedPoint f hf y hy)
have trans₁ : (Metric.edistLtTopSetoid : α → α → Prop) x (efixedPoint f hf y hy)
Tactic: trans x