awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 β
f : α →+* β
h : Isometry.{u, v} (α := α) (β := β) (⇑f : (a : α) → β)
x : α
⊢ Eq.{v + 1} (α := Completion β)
    (((h.mapRingHom : RingHom.{u, v} (Completion α) (Completion β)) : (a : Completion α) → Completion β)
        (↑x : Completion α) :
      Completion β)
    ((↑((f : (a : α) → β) x) : Completion β) : Completion β)

Tactic:
Completion.mapRingHom_coe h.uniformContinuous.continuous _

Premises used: Isometry.uniformContinuous, UniformContinuous.continuous, UniformSpace.Completion.mapRingHom_coe
-- 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 β
f : α →+* β
h : Isometry.{u, v} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ 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 : 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 : α) → β)
⊢ 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:
exact isClosed_eq (continuous_dist.comp₂ (continuous_map.comp continuous_fst)
        (continuous_map.comp continuous_snd)) (by fun_prop)

Premises used: Continuous.comp₂, continuous_dist, isClosed_eq
-- 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 β
f : α →+* β
h : Isometry.{u, v} (α := α) (β := β) (⇑f : (a : α) → β)
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:
simp only [Completion.dist_eq, mapRingHom_coe, h.dist_eq]

Premises used: UniformSpace.Completion.dist_eq, Isometry.dist_eq, Isometry.mapRingHom_coe
-- 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 β
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}
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 α)
⊢ 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

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]

Premises used: Continuous.comp₂, continuous_dist, UniformSpace.Completion.dist_eq, isClosed_eq, Isometry.dist_eq, Isometry.mapRingHom_coe
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂ ↔ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Congruent
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂)

Tactic:
⟨fun h ↦ fun _ _ _ ↦ h _ _, fun h ↦ fun i₁ i₂ ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
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₂)
⊢ Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) ↦ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
refine ⟨fun h ↦ fun _ _ _ ↦ h _ _, fun h ↦ fun i₁ i₂ ↦ ?_⟩
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂)
neg : ∀ (hi : ¬i₁ = i₂), edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
by_cases hi : i₁ = i₂
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂ : ι
hi : i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
simp [hi]
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
h hi
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂ : ι
hi : ¬i₁ = i₂
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
exact h hi
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
inst : PseudoEMetricSpace P₁
v₁ : ι → P₁
⊢ v₁ ≅ v₁

Tactic:
fun _ _ ↦ rfl

Premises used: Congruent, rfl
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
h : v₁ ≅ v₂
⊢ v₂ ≅ v₁

Tactic:
fun i₁ i₂ ↦ (h i₁ i₂).symm

Premises used: Congruent, Eq.symm
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
⊢ v₁ ≅ v₂ ↔ v₂ ≅ v₁

Tactic:
⟨Congruent.symm, Congruent.symm⟩

Premises used: Congruent.symm, Iff.intro
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
h₁₂ : v₁ ≅ v₂
h₂₃ : v₂ ≅ v₃
⊢ v₁ ≅ v₃

Tactic:
fun i₁ i₂ ↦ (h₁₂ i₁ i₂).trans (h₂₃ i₁ i₂)

Premises used: Congruent, Eq.trans
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
h : v₁ ≅ v₂
f : ι' → ι
⊢ v₁ ∘ f ≅ v₂ ∘ f

Tactic:
fun i₁ i₂ ↦ edist_eq h (f i₁) (f i₂)

Premises used: Congruent, Congruent.edist_eq
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂

Tactic:
⟨fun h i₁ i₂ ↦ ?_, fun h ↦ index_map h f⟩

Premises used: Iff.intro, Congruent.index_map, DFunLike.coe
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂
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₂)
⊢ Congruent.{u_2, u_3, u_4} (ι := ι') (v₁ ∘ (⇑f : (a : ι') → ι)) (v₂ ∘ (⇑f : (a : ι') → ι)) ↔ v₁ ≅ v₂

Tactic:
refine ⟨fun h i₁ i₂ ↦ ?_, fun h ↦ index_map h f⟩
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂
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:
simpa [(EquivLike.toEquiv f).right_inv i₁, (EquivLike.toEquiv f).right_inv i₂]
    using edist_eq h ((EquivLike.toEquiv f).symm i₁) ((EquivLike.toEquiv f).symm i₂)

Premises used: Equiv.right_inv, Congruent.edist_eq, Equiv.symm, DFunLike.coe, EquivLike.toEquiv
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : Subsingleton ι
i j : ι
⊢ edist (v₁ i) (v₁ j) = edist (v₂ i) (v₂ j)

Tactic:
simp [Subsingleton.elim i j]

Premises used: Subsingleton.elim
-- Module: Mathlib.Topology.MetricSpace.Congruence
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
h : v₁ ≅ v₂
⊢ f ∘ v₁ ≅ v₂

Tactic:
.trans (fun _ _ ↦ hf _ _) h

Premises used: Congruent.trans
-- Module: Mathlib.Topology.MetricSpace.Congruence
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
h : v₁ ≅ v₂
⊢ v₁ ≅ f ∘ v₂

Tactic:
.trans h (.symm <| fun _ _ ↦ hf _ _)

Premises used: Congruent.symm, Congruent.trans
-- Module: Mathlib.Topology.MetricSpace.Congruence
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
⊢ f ∘ v₁ ≅ v₂ ↔ v₁ ≅ v₂

Tactic:
⟨.trans <| .comp_right hf (.refl _), .comp_left hf⟩

Premises used: Congruent.comp_left, Congruent.refl, Congruent.trans, Iff.intro, Congruent.comp_right
-- Module: Mathlib.Topology.MetricSpace.Congruence
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₂
rw₂ rw₃ : v₁ ≅ v₂ ↔ v₁ ≅ v₂
⊢ v₁ ≅ f ∘ v₂ ↔ v₁ ≅ v₂

Tactic:
rw [congruent_comm, comp_left_iff hf, congruent_comm]

Premises used: congruent_comm, Congruent.comp_left_iff
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
P₄ : Type u_6
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoEMetricSpace P₁
inst_1 : PseudoEMetricSpace P₂
inst_2 : PseudoEMetricSpace P₃
inst_3 : PseudoEMetricSpace P₄
F₁ : Type u_7
F₂ : Type u_8
inst_4 : FunLike F₁ P₁ P₃
inst_5 : DilationClass F₁ P₁ P₃
inst_6 : FunLike F₂ P₂ P₄
inst_7 : DilationClass F₂ P₂ P₄
f₁ : F₁
f₂ : F₂
h : v₁ ≅ v₂
hf : Dilation.ratio f₁ = Dilation.ratio f₂
i j : ι
⊢ edist.{u_5} (α := P₃) (((⇑f₁ : (a : P₁) → P₃) ∘ v₁) i) (((⇑f₁ : (a : P₁) → P₃) ∘ v₁) j) =
    edist.{u_6} (α := P₄) (((⇑f₂ : (a : P₂) → P₄) ∘ v₂) i) (((⇑f₂ : (a : P₂) → P₄) ∘ v₂) j)

Tactic:
simp [hf, h i j]
-- Module: Mathlib.Topology.MetricSpace.Congruence
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 : ι
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)
⊢ edist (v₁ x) (v₁ x_1) = edist (v₂ x) (v₂ x_1) ↔ nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1)

Tactic:
rw [edist_nndist, edist_nndist]

Premises used: edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Congruence
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 : ι
norm_cast norm_cast₁ norm_cast₂ 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)
⊢ (↑(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:
norm_cast
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
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₂)
⊢ Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) ↦ nndist (v₁ i₁) (v₁ i₂) = nndist (v₂ i₁) (v₂ i₂)

Tactic:
simp_rw [congruent_iff_pairwise_edist_eq, edist_nndist]

Premises used: congruent_iff_pairwise_edist_eq, edist_nndist
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ (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:
exact_mod_cast Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.MetricSpace.Congruence
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 : ι
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)) : ℝ)
⊢ nndist (v₁ x) (v₁ x_1) = nndist (v₂ x) (v₂ x_1) ↔ dist (v₁ x) (v₁ x_1) = dist (v₂ x) (v₂ x_1)

Tactic:
rw [dist_nndist, dist_nndist]

Premises used: dist_nndist
-- Module: Mathlib.Topology.MetricSpace.Congruence
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 : ι
norm_cast norm_cast₁ norm_cast₂ 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)
⊢ 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
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
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₂)) : ℝ)
⊢ Congruent v₁ v₂ ↔ Pairwise fun (i₁ i₂ : ι) ↦ dist (v₁ i₁) (v₁ i₂) = dist (v₂ i₁) (v₂ i₂)

Tactic:
simp_rw [congruent_iff_pairwise_nndist_eq, dist_nndist]

Premises used: dist_nndist, congruent_iff_pairwise_nndist_eq
-- Module: Mathlib.Topology.MetricSpace.Congruence
Goal:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst : PseudoMetricSpace P₁
inst_1 : PseudoMetricSpace P₂
⊢ (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:
exact_mod_cast Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
⊢ LipschitzWith K f

Tactic:
hf.2

Premises used: And.right
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
⊢ 0 < 1 - (↑K : ℝ≥0∞)

Tactic:
simp [hf.1]

Premises used: And.left
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
⊢ 1 - (↑K : ℝ≥0∞) ≠ 0

Tactic:
ne_of_gt hf.one_sub_K_pos'

Premises used: ContractingWith.one_sub_K_pos', ne_of_gt
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
K : ℝ≥0
⊢ ¬(↑(1 - K) : ℝ≥0∞) = ∞

Tactic:
ENNReal.coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
K : ℝ≥0
⊢ ¬(↑(1 - K) : ℝ≥0∞) = ∞

Tactic:
exact ENNReal.coe_ne_top

Premises used: ENNReal.coe_ne_top
-- Module: Mathlib.Topology.MetricSpace.Contracting
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)
rw₁ 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)
⊢ 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)

Tactic:
rw [edist_comm y, add_right_comm]

Premises used: PseudoEMetricSpace.edist_comm, add_right_comm
-- Module: Mathlib.Topology.MetricSpace.Contracting
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)
rwa₃ : edist x y - (↑K : ℝ≥0∞) * edist x y ≤ edist x (f x) + edist y (f y)
rwa₄ rwa₅ rwa₆ rwa₇ : 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∞))

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]

Premises used: ENNReal.le_div_iff_mul_le, ContractingWith.one_sub_K_ne_zero, ENNReal.sub_mul, tsub_le_iff_right, mul_comm, Or.inl, ContractingWith.one_sub_K_ne_top, one_mul
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
h : edist x y ≠ ∞
hy : IsFixedPt f y
⊢ edist x y ≤ edist x (f x) / (1 - (↑K : ℝ≥0∞))

Tactic:
simpa only [hy.eq, edist_self, add_zero] using hf.edist_inequality h

Premises used: PseudoEMetricSpace.edist_self, ContractingWith.edist_inequality, Function.IsFixedPt.eq, add_zero
-- Module: Mathlib.Topology.MetricSpace.Contracting
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 = ∞

Tactic:
or_iff_not_imp_right.2 fun h ↦ edist_le_zero.1 ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, edist_le_zero, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
refine : ∀ (h : ¬edist x y = ∞), edist x y ≤ 0
⊢ x = y ∨ edist x y = ∞

Tactic:
refine or_iff_not_imp_right.2 fun h ↦ edist_le_zero.1 ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, edist_le_zero, Iff.mp
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
x y : α
hx : IsFixedPt f x
hy : IsFixedPt f y
h : ¬edist x y = ∞
⊢ edist x y ≤ 0

Tactic:
simpa only [hx.eq, edist_self, add_zero, ENNReal.zero_div] using hf.edist_le_of_fixedPoint h hy

Premises used: ContractingWith.edist_le_of_fixedPoint, ENNReal.zero_div, PseudoEMetricSpace.edist_self, Function.IsFixedPt.eq, add_zero
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
hf : ContractingWith K f
s : Set α
hs : MapsTo f s s
⊢ ContractingWith K (MapsTo.restrict f s s hs)

Tactic:
⟨hf.1, fun x y ↦ hf.2 x y⟩

Premises used: And.right, And.left, And.intro, ContractingWith, Subtype.val
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
⊢ ∃ (y : α),
    IsFixedPt f y ∧
      Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 y) ∧
        ∀ (n : ℕ), edist (f^[n] x) y ≤ edist x (f x) * (↑K : ℝ≥0∞) ^ n / (1 - (↑K : ℝ≥0∞))

Tactic:
have : CauchySeq fun n ↦ f^[n] x :=
    cauchySeq_of_edist_le_geometric K (edist x (f x)) (ENNReal.coe_lt_one_iff.2 hf.1) hx
      (hf.toLipschitzWith.edist_iterate_succ_le_geometric x)
  let ⟨y, hy⟩ := cauchySeq_tendsto_of_complete this
  ⟨y, isFixedPt_of_tendsto_iterate hy hf.2.continuous.continuousAt, hy,
    edist_le_of_edist_le_geometric_of_tendsto K (edist x (f x))
      (hf.toLipschitzWith.edist_iterate_succ_le_geometric x) hy⟩

Premises used: Iff.mpr, ENNReal.ofNNReal, isFixedPt_of_tendsto_iterate, edist_le_of_edist_le_geometric_of_tendsto, cauchySeq_tendsto_of_complete, _private.0.ContractingWith.exists_fixedPoint.match_1, Exists, nhds, LipschitzWith.edist_iterate_succ_le_geometric, Nat.iterate, Continuous.continuousAt, Filter.atTop, ContractingWith.toLipschitzWith, LipschitzWith.continuous, And, cauchySeq_of_edist_le_geometric, And.right, And.left, Filter.Tendsto, And.intro, Exists.intro, Function.IsFixedPt, EDist.edist, ENNReal.coe_lt_one_iff
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
⊢ IsFixedPt f (efixedPoint f hf x hx)

Tactic:
(Classical.choose_spec <| hf.exists_fixedPoint x hx).1

Premises used: ContractingWith.efixedPoint, ContractingWith.exists_fixedPoint, Classical.choose_spec, And.left
-- Module: Mathlib.Topology.MetricSpace.Contracting
Goal:
α : Type u_1
inst : EMetricSpace α
K : ℝ≥0
f : α → α
inst_1 : CompleteSpace α
hf : ContractingWith K f
x : α
hx : edist x (f x) ≠ ∞
⊢ Tendsto (fun (n : ℕ) ↦ f^[n] x) atTop (𝓝 (efixedPoint f hf x hx))

Tactic:
(Classical.choose_spec <| hf.exists_fixedPoint x hx).2.1

Premises used: ContractingWith.efixedPoint, ContractingWith.exists_fixedPoint, Classical.choose_spec, And.right, And.left