text:
/-
Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sébastien Gouëzel

! This file was ported from Lean 3 source module topology.metric_space.gromov_hausdorff
! leanprover-community/mathlib commit 0c1f285a9f6e608ae2bdffa3f993eafb01eba829
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.SetTheory.Cardinal.Basic
import Mathbin.Topology.MetricSpace.Closeds
import Mathbin.Topology.MetricSpace.Completion
import Mathbin.Topology.MetricSpace.GromovHausdorffRealized
import Mathbin.Topology.MetricSpace.Kuratowski

/-!
# Gromov-Hausdorff distance

This file defines the Gromov-Hausdorff distance on the space of nonempty compact metric spaces
up to isometry.

We introduce the space of all nonempty compact metric spaces, up to isometry,
called `GH_space`, and endow it with a metric space structure. The distance,
known as the Gromov-Hausdorff distance, is defined as follows: given two
nonempty compact spaces `X` and `Y`, their distance is the minimum Hausdorff distance
between all possible isometric embeddings of `X` and `Y` in all metric spaces.
To define properly the Gromov-Hausdorff space, we consider the non-empty
compact subsets of `ℓ^∞(ℝ)` up to isometry, which is a well-defined type,
and define the distance as the infimum of the Hausdorff distance over all
embeddings in `ℓ^∞(ℝ)`. We prove that this coincides with the previous description,
as all separable metric spaces embed isometrically into `ℓ^∞(ℝ)`, through an
embedding called the Kuratowski embedding.
To prove that we have a distance, we should show that if spaces can be coupled
to be arbitrarily close, then they are isometric. More generally, the Gromov-Hausdorff
distance is realized, i.e., there is a coupling for which the Hausdorff distance
is exactly the Gromov-Hausdorff distance. This follows from a compactness
argument, essentially following from Arzela-Ascoli.

## Main results

We prove the most important properties of the Gromov-Hausdorff space: it is a polish space,
i.e., it is complete and second countable. We also prove the Gromov compactness criterion.

-/

noncomputable section

open Classical Topology ENNReal

-- mathport name: exprℓ_infty_ℝ
local notation "ℓ_infty_ℝ" => lp (fun n : ℕ => ℝ) ∞

universe u v w

open Classical Set Function TopologicalSpace Filter Metric Quotient

open BoundedContinuousFunction Nat Int kuratowskiEmbedding

open Sum (inl inr)

attribute [local instance] metric_space_sum

namespace GromovHausdorff

section GHSpace

/- In this section, we define the Gromov-Hausdorff space, denoted `GH_space` as the quotient
of nonempty compact subsets of `ℓ^∞(ℝ)` by identifying isometric sets.
Using the Kuratwoski embedding, we get a canonical map `to_GH_space` mapping any nonempty
compact type to `GH_space`. -/
/-- Equivalence relation identifying two nonempty compact sets which are isometric -/
private def isometry_rel : NonemptyCompacts ℓ_infty_ℝ → NonemptyCompacts ℓ_infty_ℝ → Prop :=
  fun x y => Nonempty (x ≃ᵢ y)
#align Gromov_Hausdorff.isometry_rel Gromov_Hausdorff.isometry_rel

/-- This is indeed an equivalence relation -/
private theorem is_equivalence_isometry_rel : Equivalence IsometryRel :=
  ⟨fun x => ⟨IsometryEquiv.refl _⟩, fun x y ⟨e⟩ => ⟨e.symm⟩, fun x y z ⟨e⟩ ⟨f⟩ => ⟨e.trans f⟩⟩
#align Gromov_Hausdorff.is_equivalence_isometry_rel Gromov_Hausdorff.is_equivalence_isometry_rel

/-- setoid instance identifying two isometric nonempty compact subspaces of ℓ^∞(ℝ) -/
instance IsometryRel.setoid : Setoid (NonemptyCompacts ℓ_infty_ℝ) :=
  Setoid.mk IsometryRel is_equivalence_isometryRel
#align Gromov_Hausdorff.isometry_rel.setoid GromovHausdorff.IsometryRel.setoid

/-- The Gromov-Hausdorff space -/
def GHSpace : Type :=
  Quotient IsometryRel.setoid
#align Gromov_Hausdorff.GH_space GromovHausdorff.GHSpace

/-- Map any nonempty compact type to `GH_space` -/
def toGHSpace (X : Type u) [MetricSpace X] [CompactSpace X] [Nonempty X] : GHSpace :=
  ⟦NonemptyCompacts.kuratowskiEmbedding X⟧
#align Gromov_Hausdorff.to_GH_space GromovHausdorff.toGHSpace

instance : Inhabited GHSpace :=
  ⟨Quot.mk _ ⟨⟨{0}, isCompact_singleton⟩, singleton_nonempty _⟩⟩

/-- A metric space representative of any abstract point in `GH_space` -/
@[nolint has_nonempty_instance]
def GHSpace.Rep (p : GHSpace) : Type :=
  (Quotient.out p : NonemptyCompacts ℓ_infty_ℝ)
#align Gromov_Hausdorff.GH_space.rep GromovHausdorff.GHSpace.Rep

theorem eq_toGHSpace_iff {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X]
    {p : NonemptyCompacts ℓ_infty_ℝ} :
    ⟦p⟧ = toGHSpace X ↔ ∃ Ψ : X → ℓ_infty_ℝ, Isometry Ψ ∧ range Ψ = p :=
  by
  simp only [to_GH_space, Quotient.eq']
  refine' ⟨fun h => _, _⟩
  · rcases Setoid.symm h with ⟨e⟩
    have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.trans e
    use fun x => f x, isometry_subtype_coe.comp f.isometry
    rw [range_comp, f.range_eq_univ, Set.image_univ, Subtype.range_coe]
    rfl
  · rintro ⟨Ψ, ⟨isomΨ, rangeΨ⟩⟩
    have f :=
      ((kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm.trans
          isomΨ.isometry_equiv_on_range).symm
    have E :
      (range Ψ ≃ᵢ NonemptyCompacts.kuratowskiEmbedding X) = (p ≃ᵢ range (kuratowskiEmbedding X)) :=
      by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]
      rw [rangeΨ] <;> rfl
    exact ⟨cast E f⟩
#align Gromov_Hausdorff.eq_to_GH_space_iff GromovHausdorff.eq_toGHSpace_iff

theorem eq_toGHSpace {p : NonemptyCompacts ℓ_infty_ℝ} : ⟦p⟧ = toGHSpace p :=
  eq_toGHSpace_iff.2 ⟨fun x => x, isometry_subtype_coe, Subtype.range_coe⟩
#align Gromov_Hausdorff.eq_to_GH_space GromovHausdorff.eq_toGHSpace

section

attribute [local reducible] GH_space.rep

instance repGHSpaceMetricSpace {p : GHSpace} : MetricSpace p.rep := by infer_instance
#align Gromov_Hausdorff.rep_GH_space_metric_space GromovHausdorff.repGHSpaceMetricSpace

instance rep_gHSpace_compactSpace {p : GHSpace} : CompactSpace p.rep := by infer_instance
#align Gromov_Hausdorff.rep_GH_space_compact_space GromovHausdorff.rep_gHSpace_compactSpace

instance rep_gHSpace_nonempty {p : GHSpace} : Nonempty p.rep := by infer_instance
#align Gromov_Hausdorff.rep_GH_space_nonempty GromovHausdorff.rep_gHSpace_nonempty

end

theorem GHSpace.toGHSpace_rep (p : GHSpace) : toGHSpace p.rep = p :=
  by
  change to_GH_space (Quot.out p : nonempty_compacts ℓ_infty_ℝ) = p
  rw [← eq_to_GH_space]
  exact Quot.out_eq p
#align Gromov_Hausdorff.GH_space.to_GH_space_rep GromovHausdorff.GHSpace.toGHSpace_rep

/-- Two nonempty compact spaces have the same image in `GH_space` if and only if they are
isometric. -/
theorem toGHSpace_eq_toGHSpace_iff_isometryEquiv {X : Type u} [MetricSpace X] [CompactSpace X]
    [Nonempty X] {Y : Type v} [MetricSpace Y] [CompactSpace Y] [Nonempty Y] :
    toGHSpace X = toGHSpace Y ↔ Nonempty (X ≃ᵢ Y) :=
  ⟨by
    simp only [to_GH_space, Quotient.eq']
    rintro ⟨e⟩
    have I :
      (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) =
        (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) :=
      by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]
      rfl
    have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange
    have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange.symm
    exact ⟨f.trans <| (cast I e).trans g⟩, by
    rintro ⟨e⟩
    simp only [to_GH_space, Quotient.eq']
    have f := (kuratowskiEmbedding.isometry X).isometryEquivOnRange.symm
    have g := (kuratowskiEmbedding.isometry Y).isometryEquivOnRange
    have I :
      (range (kuratowskiEmbedding X) ≃ᵢ range (kuratowskiEmbedding Y)) =
        (NonemptyCompacts.kuratowskiEmbedding X ≃ᵢ NonemptyCompacts.kuratowskiEmbedding Y) :=
      by
      dsimp only [NonemptyCompacts.kuratowskiEmbedding]
      rfl
    exact ⟨cast I ((f.trans e).trans g)⟩⟩
#align Gromov_Hausdorff.to_GH_space_eq_to_GH_space_iff_isometry_equiv GromovHausdorff.toGHSpace_eq_toGHSpace_iff_isometryEquiv

/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
/-- Distance on `GH_space`: the distance between two nonempty compact spaces is the infimum
Hausdorff distance between isometric copies of the two spaces in a metric space. For the definition,
we only consider embeddings in `ℓ^∞(ℝ)`, but we will prove below that it works for all spaces. -/
instance : Dist GHSpace
    where dist x y :=
    infₛ <|
      (fun p : NonemptyCompacts ℓ_infty_ℝ × NonemptyCompacts ℓ_infty_ℝ =>
          hausdorffDist (p.1 : Set ℓ_infty_ℝ) p.2) ''
        { a | ⟦a⟧ = x } ×ˢ { b | ⟦b⟧ = y }

/-- The Gromov-Hausdorff distance between two nonempty compact metric spaces, equal by definition to
the distance of the equivalence classes of these spaces in the Gromov-Hausdorff space. -/
def gHDist (X : Type u) (Y : Type v) [MetricSpace X] [Nonempty X] [CompactSpace X] [MetricSpace Y]
    [Nonempty Y] [CompactSpace Y] : ℝ :=
  dist (toGHSpace X) (toGHSpace Y)
#align Gromov_Hausdorff.GH_dist GromovHausdorff.gHDist

theorem dist_gHDist (p q : GHSpace) : dist p q = gHDist p.rep q.rep := by
  rw [GH_dist, p.to_GH_space_rep, q.to_GH_space_rep]
#align Gromov_Hausdorff.dist_GH_dist GromovHausdorff.dist_gHDist

/-- The Gromov-Hausdorff distance between two spaces is bounded by the Hausdorff distance
of isometric copies of the spaces, in any metric space. -/
theorem gHDist_le_hausdorffDist {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X]
    {Y : Type v} [MetricSpace Y] [CompactSpace Y] [Nonempty Y] {γ : Type w} [MetricSpace γ]
    {Φ : X → γ} {Ψ : Y → γ} (ha : Isometry Φ) (hb : Isometry Ψ) :
    gHDist X Y ≤ hausdorffDist (range Φ) (range Ψ) :=
  by
  /- For the proof, we want to embed `γ` in `ℓ^∞(ℝ)`, to say that the Hausdorff distance is realized
    in `ℓ^∞(ℝ)` and therefore bounded below by the Gromov-Hausdorff-distance. However, `γ` is not
    separable in general. We restrict to the union of the images of `X` and `Y` in `γ`, which is
    separable and therefore embeddable in `ℓ^∞(ℝ)`. -/
  rcases exists_mem_of_nonempty X with ⟨xX, _⟩
  let s : Set γ := range Φ ∪ range Ψ
  let Φ' : X → Subtype s := fun y => ⟨Φ y, mem_union_left _ (mem_range_self _)⟩
  let Ψ' : Y → Subtype s := fun y => ⟨Ψ y, mem_union_right _ (mem_range_self _)⟩
  have IΦ' : Isometry Φ' := fun x y => ha x y
  have IΨ' : Isometry Ψ' := fun x y => hb x y
  have : IsCompact s := (isCompact_range ha.continuous).union (isCompact_range hb.continuous)
  letI : MetricSpace (Subtype s) := by infer_instance
  haveI : CompactSpace (Subtype s) := ⟨isCompact_iff_isCompact_univ.1 ‹IsCompact s›⟩
  haveI : Nonempty (Subtype s) := ⟨Φ' xX⟩
  have ΦΦ' : Φ = Subtype.val ∘ Φ' := by
    funext
    rfl
  have ΨΨ' : Ψ = Subtype.val ∘ Ψ' := by
    funext
    rfl
  have : Hausdorff_dist (range Φ) (range Ψ) = Hausdorff_dist (range Φ') (range Ψ') :=
    by
    rw [ΦΦ', ΨΨ', range_comp, range_comp]
    exact Hausdorff_dist_image isometry_subtype_coe
  rw [this]
  -- Embed `s` in `ℓ^∞(ℝ)` through its Kuratowski embedding
  let F := kuratowskiEmbedding (Subtype s)
  have : Hausdorff_dist (F '' range Φ') (F '' range Ψ') = Hausdorff_dist (range Φ') (range Ψ') :=
    Hausdorff_dist_image (kuratowskiEmbedding.isometry _)
  rw [← this]
  -- Let `A` and `B` be the images of `X` and `Y` under this embedding. They are in `ℓ^∞(ℝ)`, and
  -- their Hausdorff distance is the same as in the original space.
  let A : nonempty_compacts ℓ_infty_ℝ :=
    ⟨⟨F '' range Φ',
        (isCompact_range IΦ'.continuous).image (kuratowskiEmbedding.isometry _).Continuous⟩,
      (range_nonempty _).image _⟩
  let B : nonempty_compacts ℓ_infty_ℝ :=
    ⟨⟨F '' range Ψ',
        (isCompact_range IΨ'.continuous).image (kuratowskiEmbedding.isometry _).Continuous⟩,
      (range_nonempty _).image _⟩
  have AX : ⟦A⟧ = to_GH_space X := by
    rw [eq_to_GH_space_iff]
    exact ⟨fun x => F (Φ' x), (kuratowskiEmbedding.isometry _).comp IΦ', range_comp _ _⟩
  have BY : ⟦B⟧ = to_GH_space Y := by
    rw [eq_to_GH_space_iff]
    exact ⟨fun x => F (Ψ' x), (kuratowskiEmbedding.isometry _).comp IΨ', range_comp _ _⟩
  refine' cinfₛ_le ⟨0, _⟩ _
  · simp only [lowerBounds, mem_image, mem_prod, mem_set_of_eq, Prod.exists, and_imp,
      forall_exists_index]
    intro t _ _ _ _ ht
    rw [← ht]
    exact Hausdorff_dist_nonneg
  apply (mem_image _ _ _).2
  exists (⟨A, B⟩ : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ)
  simp [AX, BY]
#align Gromov_Hausdorff.GH_dist_le_Hausdorff_dist GromovHausdorff.gHDist_le_hausdorffDist

/-- The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance,
essentially by design. -/
theorem hausdorffDist_optimal {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X]
    {Y : Type v} [MetricSpace Y] [CompactSpace Y] [Nonempty Y] :
    hausdorffDist (range (optimalGHInjl X Y)) (range (optimalGHInjr X Y)) = gHDist X Y :=
  by
  inhabit X
  inhabit Y
  /- we only need to check the inequality `≤`, as the other one follows from the previous lemma.
       As the Gromov-Hausdorff distance is an infimum, we need to check that the Hausdorff distance
       in the optimal coupling is smaller than the Hausdorff distance of any coupling.
       First, we check this for couplings which already have small Hausdorff distance: in this
       case, the induced "distance" on `X ⊕ Y` belongs to the candidates family introduced in the
       definition of the optimal coupling, and the conclusion follows from the optimality
       of the optimal coupling within this family.
    -/
  have A :
    ∀ p q : nonempty_compacts ℓ_infty_ℝ,
      ⟦p⟧ = to_GH_space X →
        ⟦q⟧ = to_GH_space Y →
          Hausdorff_dist (p : Set ℓ_infty_ℝ) q < diam (univ : Set X) + 1 + diam (univ : Set Y) →
            Hausdorff_dist (range (optimal_GH_injl X Y)) (range (optimal_GH_injr X Y)) ≤
              Hausdorff_dist (p : Set ℓ_infty_ℝ) q :=
    by
    intro p q hp hq bound
    rcases eq_to_GH_space_iff.1 hp with ⟨Φ, ⟨Φisom, Φrange⟩⟩
    rcases eq_to_GH_space_iff.1 hq with ⟨Ψ, ⟨Ψisom, Ψrange⟩⟩
    have I : diam (range Φ ∪ range Ψ) ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) :=
      by
      rcases exists_mem_of_nonempty X with ⟨xX, _⟩
      have : ∃ y ∈ range Ψ, dist (Φ xX) y < diam (univ : Set X) + 1 + diam (univ : Set Y) :=
        by
        rw [Ψrange]
        have : Φ xX ∈ ↑p := Φrange.subst (mem_range_self _)
        exact
          exists_dist_lt_of_Hausdorff_dist_lt this bound
            (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty
              p.is_compact.bounded q.is_compact.bounded)
      rcases this with ⟨y, hy, dy⟩
      rcases mem_range.1 hy with ⟨z, hzy⟩
      rw [← hzy] at dy
      have DΦ : diam (range Φ) = diam (univ : Set X) := Φisom.diam_range
      have DΨ : diam (range Ψ) = diam (univ : Set Y) := Ψisom.diam_range
      calc
        diam (range Φ ∪ range Ψ) ≤ diam (range Φ) + dist (Φ xX) (Ψ z) + diam (range Ψ) :=
          diam_union (mem_range_self _) (mem_range_self _)
        _ ≤
            diam (univ : Set X) + (diam (univ : Set X) + 1 + diam (univ : Set Y)) +
              diam (univ : Set Y) :=
          by
          rw [DΦ, DΨ]
          apply add_le_add (add_le_add le_rfl (le_of_lt dy)) le_rfl
        _ = 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := by ring

    let f : Sum X Y → ℓ_infty_ℝ := fun x =>
      match x with
      | inl y => Φ y
      | inr z => Ψ z
    let F : Sum X Y × Sum X Y → ℝ := fun p => dist (f p.1) (f p.2)
    -- check that the induced "distance" is a candidate
    have Fgood : F ∈ candidates X Y :=
      by
      simp only [candidates, forall_const, and_true_iff, add_comm, eq_self_iff_true, dist_eq_zero,
        and_self_iff, Set.mem_setOf_eq]
      repeat' constructor
      ·
        exact fun x y =>
          calc
            F (inl x, inl y) = dist (Φ x) (Φ y) := rfl
            _ = dist x y := Φisom.dist_eq x y

      ·
        exact fun x y =>
          calc
            F (inr x, inr y) = dist (Ψ x) (Ψ y) := rfl
            _ = dist x y := Ψisom.dist_eq x y

      · exact fun x y => dist_comm _ _
      · exact fun x y z => dist_triangle _ _ _
      ·
        exact fun x y =>
          calc
            F (x, y) ≤ diam (range Φ ∪ range Ψ) :=
              by
              have A : ∀ z : Sum X Y, f z ∈ range Φ ∪ range Ψ :=
                by
                intro z
                cases z
                · apply mem_union_left
                  apply mem_range_self
                · apply mem_union_right
                  apply mem_range_self
              refine' dist_le_diam_of_mem _ (A _) (A _)
              rw [Φrange, Ψrange]
              exact (p ⊔ q).IsCompact.Bounded
            _ ≤ 2 * diam (univ : Set X) + 1 + 2 * diam (univ : Set Y) := I

    let Fb := candidates_b_of_candidates F Fgood
    have : Hausdorff_dist (range (optimal_GH_injl X Y)) (range (optimal_GH_injr X Y)) ≤ HD Fb :=
      Hausdorff_dist_optimal_le_HD _ _ (candidates_b_of_candidates_mem F Fgood)
    refine' le_trans this (le_of_forall_le_of_dense fun r hr => _)
    have I1 : ∀ x : X, (⨅ y, Fb (inl x, inr y)) ≤ r :=
      by
      intro x
      have : f (inl x) ∈ ↑p := Φrange.subst (mem_range_self _)
      rcases exists_dist_lt_of_Hausdorff_dist_lt this hr
          (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty p.is_compact.bounded
            q.is_compact.bounded) with
        ⟨z, zq, hz⟩
      have : z ∈ range Ψ := by rwa [← Ψrange] at zq
      rcases mem_range.1 this with ⟨y, hy⟩
      calc
        (⨅ y, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) :=
          cinfᵢ_le (by simpa only [add_zero] using HD_below_aux1 0) y
        _ = dist (Φ x) (Ψ y) := rfl
        _ = dist (f (inl x)) z := by rw [hy]
        _ ≤ r := le_of_lt hz

    have I2 : ∀ y : Y, (⨅ x, Fb (inl x, inr y)) ≤ r :=
      by
      intro y
      have : f (inr y) ∈ ↑q := Ψrange.subst (mem_range_self _)
      rcases exists_dist_lt_of_Hausdorff_dist_lt' this hr
          (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.nonempty q.nonempty p.is_compact.bounded
            q.is_compact.bounded) with
        ⟨z, zq, hz⟩
      have : z ∈ range Φ := by rwa [← Φrange] at zq
      rcases mem_range.1 this with ⟨x, hx⟩
      calc
        (⨅ x, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) :=
          cinfᵢ_le (by simpa only [add_zero] using HD_below_aux2 0) x
        _ = dist (Φ x) (Ψ y) := rfl
        _ = dist z (f (inr y)) := by rw [hx]
        _ ≤ r := le_of_lt hz

    simp only [HD, csupᵢ_le I1, csupᵢ_le I2, max_le_iff, and_self_iff]
  /- Get the same inequality for any coupling. If the coupling is quite good, the desired
    inequality has been proved above. If it is bad, then the inequality is obvious. -/
  have B :
    ∀ p q : nonempty_compacts ℓ_infty_ℝ,
      ⟦p⟧ = to_GH_space X →
        ⟦q⟧ = to_GH_space Y →
          Hausdorff_dist (range (optimal_GH_injl X Y)) (range (optimal_GH_injr X Y)) ≤
            Hausdorff_dist (p : Set ℓ_infty_ℝ) q :=
    by
    intro p q hp hq
    by_cases h :
      Hausdorff_dist (p : Set ℓ_infty_ℝ) q < diam (univ : Set X) + 1 + diam (univ : Set Y)
    · exact A p q hp hq h
    ·
      calc
        Hausdorff_dist (range (optimal_GH_injl X Y)) (range (optimal_GH_injr X Y)) ≤
            HD (candidates_b_dist X Y) :=
          Hausdorff_dist_optimal_le_HD _ _ candidates_b_dist_mem_candidates_b
        _ ≤ diam (univ : Set X) + 1 + diam (univ : Set Y) := HD_candidates_b_dist_le
        _ ≤ Hausdorff_dist (p : Set ℓ_infty_ℝ) q := not_lt.1 h

  refine' le_antisymm _ _
  · apply le_cinfₛ
    · refine' (Set.Nonempty.prod _ _).image _ <;> exact ⟨_, rfl⟩
    · rintro b ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩
      exact B p q hp hq
  · exact GH_dist_le_Hausdorff_dist (isometry_optimal_GH_injl X Y) (isometry_optimal_GH_injr X Y)
#align Gromov_Hausdorff.Hausdorff_dist_optimal GromovHausdorff.hausdorffDist_optimal

/-- The Gromov-Hausdorff distance can also be realized by a coupling in `ℓ^∞(ℝ)`, by embedding
the optimal coupling through its Kuratowski embedding. -/
theorem gHDist_eq_hausdorffDist (X : Type u) [MetricSpace X] [CompactSpace X] [Nonempty X]
    (Y : Type v) [MetricSpace Y] [CompactSpace Y] [Nonempty Y] :
    ∃ Φ : X → ℓ_infty_ℝ,
      ∃ Ψ : Y → ℓ_infty_ℝ,
        Isometry Φ ∧ Isometry Ψ ∧ gHDist X Y = hausdorffDist (range Φ) (range Ψ) :=
  by
  let F := kuratowskiEmbedding (optimal_GH_coupling X Y)
  let Φ := F ∘ optimal_GH_injl X Y
  let Ψ := F ∘ optimal_GH_injr X Y
  refine' ⟨Φ, Ψ, _, _, _⟩
  · exact (kuratowskiEmbedding.isometry _).comp (isometry_optimal_GH_injl X Y)
  · exact (kuratowskiEmbedding.isometry _).comp (isometry_optimal_GH_injr X Y)
  · rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimal_GH_injr X Y),
      image_univ, ← Hausdorff_dist_optimal]
    exact (Hausdorff_dist_image (kuratowskiEmbedding.isometry _)).symm
#align Gromov_Hausdorff.GH_dist_eq_Hausdorff_dist GromovHausdorff.gHDist_eq_hausdorffDist

/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/
/-- The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space. -/
instance : MetricSpace GHSpace where
  dist := dist
  dist_self x := by
    rcases exists_rep x with ⟨y, hy⟩
    refine' le_antisymm _ _
    · apply cinfₛ_le
      ·
        exact
          ⟨0, by
            rintro b ⟨⟨u, v⟩, ⟨hu, hv⟩, rfl⟩
            exact Hausdorff_dist_nonneg⟩
      · simp only [mem_image, mem_prod, mem_set_of_eq, Prod.exists]
        exists y, y
        simpa only [and_self_iff, Hausdorff_dist_self_zero, eq_self_iff_true, and_true_iff]
    · apply le_cinfₛ
      · exact (nonempty.prod ⟨y, hy⟩ ⟨y, hy⟩).image _
      · rintro b ⟨⟨u, v⟩, ⟨hu, hv⟩, rfl⟩
        exact Hausdorff_dist_nonneg
  dist_comm x y :=
    by
    have A :
      (fun p : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ =>
            Hausdorff_dist (p.1 : Set ℓ_infty_ℝ) p.2) ''
          { a | ⟦a⟧ = x } ×ˢ { b | ⟦b⟧ = y } =
        (fun p : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ =>
              Hausdorff_dist (p.1 : Set ℓ_infty_ℝ) p.2) ∘
            Prod.swap ''
          { a | ⟦a⟧ = x } ×ˢ { b | ⟦b⟧ = y } :=
      by
      congr
      funext
      simp only [comp_app, Prod.fst_swap, Prod.snd_swap]
      rw [Hausdorff_dist_comm]
    simp only [dist, A, image_comp, image_swap_prod]
  eq_of_dist_eq_zero x y hxy :=
    by
    /- To show that two spaces at zero distance are isometric, we argue that the distance
        is realized by some coupling. In this coupling, the two spaces are at zero Hausdorff distance,
        i.e., they coincide. Therefore, the original spaces are isometric. -/
    rcases GH_dist_eq_Hausdorff_dist x.rep y.rep with ⟨Φ, Ψ, Φisom, Ψisom, DΦΨ⟩
    rw [← dist_GH_dist, hxy] at DΦΨ
    have : range Φ = range Ψ :=
      by
      have hΦ : IsCompact (range Φ) := isCompact_range Φisom.continuous
      have hΨ : IsCompact (range Ψ) := isCompact_range Ψisom.continuous
      apply (IsClosed.hausdorffDist_zero_iff_eq _ _ _).1 DΦΨ.symm
      · exact hΦ.is_closed
      · exact hΨ.is_closed
      ·
        exact
          Hausdorff_edist_ne_top_of_nonempty_of_bounded (range_nonempty _) (range_nonempty _)
            hΦ.bounded hΨ.bounded
    have T : (range Ψ ≃ᵢ y.rep) = (range Φ ≃ᵢ y.rep) := by rw [this]
    have eΨ := cast T Ψisom.isometry_equiv_on_range.symm
    have e := Φisom.isometry_equiv_on_range.trans eΨ
    rw [← x.to_GH_space_rep, ← y.to_GH_space_rep, to_GH_space_eq_to_GH_space_iff_isometry_equiv]
    exact ⟨e⟩
  dist_triangle x y z :=
    by
    /- To show the triangular inequality between `X`, `Y` and `Z`, realize an optimal coupling
        between `X` and `Y` in a space `γ1`, and an optimal coupling between `Y` and `Z` in a space
        `γ2`. Then, glue these metric spaces along `Y`. We get a new space `γ` in which `X` and `Y` are
        optimally coupled, as well as `Y` and `Z`. Apply the triangle inequality for the Hausdorff
        distance in `γ` to conclude. -/
    let X := x.rep
    let Y := y.rep
    let Z := z.rep
    let γ1 := optimal_GH_coupling X Y
    let γ2 := optimal_GH_coupling Y Z
    let Φ : Y → γ1 := optimal_GH_injr X Y
    have hΦ : Isometry Φ := isometry_optimal_GH_injr X Y
    let Ψ : Y → γ2 := optimal_GH_injl Y Z
    have hΨ : Isometry Ψ := isometry_optimal_GH_injl Y Z
    let γ := glue_space hΦ hΨ
    have Comm : to_glue_l hΦ hΨ ∘ optimal_GH_injr X Y = to_glue_r hΦ hΨ ∘ optimal_GH_injl Y Z :=
      to_glue_commute hΦ hΨ
    calc
      dist x z = dist (to_GH_space X) (to_GH_space Z) := by
        rw [x.to_GH_space_rep, z.to_GH_space_rep]
      _ ≤
          Hausdorff_dist (range (to_glue_l hΦ hΨ ∘ optimal_GH_injl X Y))
            (range (to_glue_r hΦ hΨ ∘ optimal_GH_injr Y Z)) :=
        (GH_dist_le_Hausdorff_dist ((to_glue_l_isometry hΦ hΨ).comp (isometry_optimal_GH_injl X Y))
          ((to_glue_r_isometry hΦ hΨ).comp (isometry_optimal_GH_injr Y Z)))
      _ ≤
          Hausdorff_dist (range (to_glue_l hΦ hΨ ∘ optimal_GH_injl X Y))
              (range (to_glue_l hΦ hΨ ∘ optimal_GH_injr X Y)) +
            Hausdorff_dist (range (to_glue_l hΦ hΨ ∘ optimal_GH_injr X Y))
              (range (to_glue_r hΦ hΨ ∘ optimal_GH_injr Y Z)) :=
        by
        refine'
          Hausdorff_dist_triangle
            (Hausdorff_edist_ne_top_of_nonempty_of_bounded (range_nonempty _) (range_nonempty _) _
              _)
        ·
          exact
            (isCompact_range
                (Isometry.continuous
                  ((to_glue_l_isometry hΦ hΨ).comp (isometry_optimal_GH_injl X Y)))).Bounded
        ·
          exact
            (isCompact_range
                (Isometry.continuous
                  ((to_glue_l_isometry hΦ hΨ).comp (isometry_optimal_GH_injr X Y)))).Bounded
      _ =
          Hausdorff_dist (to_glue_l hΦ hΨ '' range (optimal_GH_injl X Y))
              (to_glue_l hΦ hΨ '' range (optimal_GH_injr X Y)) +
            Hausdorff_dist (to_glue_r hΦ hΨ '' range (optimal_GH_injl Y Z))
              (to_glue_r hΦ hΨ '' range (optimal_GH_injr Y Z)) :=
        by simp only [← range_comp, Comm, eq_self_iff_true, add_right_inj]
      _ =
          Hausdorff_dist (range (optimal_GH_injl X Y)) (range (optimal_GH_injr X Y)) +
            Hausdorff_dist (range (optimal_GH_injl Y Z)) (range (optimal_GH_injr Y Z)) :=
        by
        rw [Hausdorff_dist_image (to_glue_l_isometry hΦ hΨ),
          Hausdorff_dist_image (to_glue_r_isometry hΦ hΨ)]
      _ = dist (to_GH_space X) (to_GH_space Y) + dist (to_GH_space Y) (to_GH_space Z) := by
        rw [Hausdorff_dist_optimal, Hausdorff_dist_optimal, GH_dist, GH_dist]
      _ = dist x y + dist y z := by rw [x.to_GH_space_rep, y.to_GH_space_rep, z.to_GH_space_rep]

end GHSpace

--section
end GromovHausdorff

/-- In particular, nonempty compacts of a metric space map to `GH_space`. We register this
in the topological_space namespace to take advantage of the notation `p.to_GH_space`. -/
def TopologicalSpace.NonemptyCompacts.toGHSpace {X : Type u} [MetricSpace X]
    (p : NonemptyCompacts X) : GromovHausdorff.GHSpace :=
  GromovHausdorff.toGHSpace p
#align topological_space.nonempty_compacts.to_GH_space TopologicalSpace.NonemptyCompacts.toGHSpace

open TopologicalSpace

namespace GromovHausdorff

section NonemptyCompacts

variable {X : Type u} [MetricSpace X]

theorem GH_dist_le_nonemptyCompacts_dist (p q : NonemptyCompacts X) :
    dist p.toGHSpace q.toGHSpace ≤ dist p q :=
  by
  have ha : Isometry (coe : p → X) := isometry_subtype_coe
  have hb : Isometry (coe : q → X) := isometry_subtype_coe
  have A : dist p q = Hausdorff_dist (p : Set X) q := rfl
  have I : ↑p = range (coe : p → X) := subtype.range_coe_subtype.symm
  have J : ↑q = range (coe : q → X) := subtype.range_coe_subtype.symm
  rw [A, I, J]
  exact GH_dist_le_Hausdorff_dist ha hb
#align Gromov_Hausdorff.GH_dist_le_nonempty_compacts_dist GromovHausdorff.GH_dist_le_nonemptyCompacts_dist

theorem toGHSpace_lipschitz :
    LipschitzWith 1 (NonemptyCompacts.toGHSpace : NonemptyCompacts X → GHSpace) :=
  LipschitzWith.mk_one GH_dist_le_nonemptyCompacts_dist
#align Gromov_Hausdorff.to_GH_space_lipschitz GromovHausdorff.toGHSpace_lipschitz

theorem toGHSpace_continuous :
    Continuous (NonemptyCompacts.toGHSpace : NonemptyCompacts X → GHSpace) :=
  toGHSpace_lipschitz.Continuous
#align Gromov_Hausdorff.to_GH_space_continuous GromovHausdorff.toGHSpace_continuous

end NonemptyCompacts

section

/- In this section, we show that if two metric spaces are isometric up to `ε₂`, then their
Gromov-Hausdorff distance is bounded by `ε₂ / 2`. More generally, if there are subsets which are
`ε₁`-dense and `ε₃`-dense in two spaces, and isometric up to `ε₂`, then the Gromov-Hausdorff
distance between the spaces is bounded by `ε₁ + ε₂/2 + ε₃`. For this, we construct a suitable
coupling between the two spaces, by gluing them (approximately) along the two matching subsets. -/
variable {X : Type u} [MetricSpace X] [CompactSpace X] [Nonempty X] {Y : Type v} [MetricSpace Y]
  [CompactSpace Y] [Nonempty Y]

-- we want to ignore these instances in the following theorem
attribute [local instance] Sum.topologicalSpace Sum.uniformSpace

/-- If there are subsets which are `ε₁`-dense and `ε₃`-dense in two spaces, and
isometric up to `ε₂`, then the Gromov-Hausdorff distance between the spaces is bounded by
`ε₁ + ε₂/2 + ε₃`. -/
theorem gHDist_le_of_approx_subsets {s : Set X} (Φ : s → Y) {ε₁ ε₂ ε₃ : ℝ}
    (hs : ∀ x : X, ∃ y ∈ s, dist x y ≤ ε₁) (hs' : ∀ x : Y, ∃ y : s, dist x (Φ y) ≤ ε₃)
    (H : ∀ x y : s, |dist x y - dist (Φ x) (Φ y)| ≤ ε₂) : gHDist X Y ≤ ε₁ + ε₂ / 2 + ε₃ :=
  by
  refine' le_of_forall_pos_le_add fun δ δ0 => _
  rcases exists_mem_of_nonempty X with ⟨xX, _⟩
  rcases hs xX with ⟨xs, hxs, Dxs⟩
  have sne : s.nonempty := ⟨xs, hxs⟩
  letI : Nonempty s := sne.to_subtype
  have : 0 ≤ ε₂ := le_trans (abs_nonneg _) (H ⟨xs, hxs⟩ ⟨xs, hxs⟩)
  have : ∀ p q : s, |dist p q - dist (Φ p) (Φ q)| ≤ 2 * (ε₂ / 2 + δ) := fun p q =>
    calc
      |dist p q - dist (Φ p) (Φ q)| ≤ ε₂ := H p q
      _ ≤ 2 * (ε₂ / 2 + δ) := by linarith

  -- glue `X` and `Y` along the almost matching subsets
  letI : MetricSpace (Sum X Y) :=
    glue_metric_approx (fun x : s => (x : X)) (fun x => Φ x) (ε₂ / 2 + δ) (by linarith) this
  let Fl := @Sum.inl X Y
  let Fr := @Sum.inr X Y
  have Il : Isometry Fl := Isometry.of_dist_eq fun x y => rfl
  have Ir : Isometry Fr := Isometry.of_dist_eq fun x y => rfl
  /- The proof goes as follows : the `GH_dist` is bounded by the Hausdorff distance of the images
    in the coupling, which is bounded (using the triangular inequality) by the sum of the Hausdorff
    distances of `X` and `s` (in the coupling or, equivalently in the original space), of `s` and
    `Φ s`, and of `Φ s` and `Y` (in the coupling or, equivalently, in the original space). The first
    term is bounded by `ε₁`, by `ε₁`-density. The third one is bounded by `ε₃`. And the middle one is
    bounded by `ε₂/2` as in the coupling the points `x` and `Φ x` are at distance `ε₂/2` by
    construction of the coupling (in fact `ε₂/2 + δ` where `δ` is an arbitrarily small positive
    constant where positivity is used to ensure that the coupling is really a metric space and not a
    premetric space on `X ⊕ Y`). -/
  have : GH_dist X Y ≤ Hausdorff_dist (range Fl) (range Fr) := GH_dist_le_Hausdorff_dist Il Ir
  have :
    Hausdorff_dist (range Fl) (range Fr) ≤
      Hausdorff_dist (range Fl) (Fl '' s) + Hausdorff_dist (Fl '' s) (range Fr) :=
    haveI B : bounded (range Fl) := (isCompact_range Il.continuous).Bounded
    Hausdorff_dist_triangle
      (Hausdorff_edist_ne_top_of_nonempty_of_bounded (range_nonempty _) (sne.image _) B
        (B.mono (image_subset_range _ _)))
  have :
    Hausdorff_dist (Fl '' s) (range Fr) ≤
      Hausdorff_dist (Fl '' s) (Fr '' range Φ) + Hausdorff_dist (Fr '' range Φ) (range Fr) :=
    haveI B : bounded (range Fr) := (isCompact_range Ir.continuous).Bounded
    Hausdorff_dist_triangle'
      (Hausdorff_edist_ne_top_of_nonempty_of_bounded ((range_nonempty _).image _) (range_nonempty _)
        (bounded.mono (image_subset_range _ _) B) B)
  have : Hausdorff_dist (range Fl) (Fl '' s) ≤ ε₁ :=
    by
    rw [← image_univ, Hausdorff_dist_image Il]
    have : 0 ≤ ε₁ := le_trans dist_nonneg Dxs
    refine'
      Hausdorff_dist_le_of_mem_dist this (fun x hx => hs x) fun x hx =>
        ⟨x, mem_univ _, by simpa only [dist_self] ⟩
  have : Hausdorff_dist (Fl '' s) (Fr '' range Φ) ≤ ε₂ / 2 + δ :=
    by
    refine' Hausdorff_dist_le_of_mem_dist (by linarith) _ _
    · intro x' hx'
      rcases(Set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩
      rw [← xx']
      use Fr (Φ ⟨x, x_in_s⟩), mem_image_of_mem Fr (mem_range_self _)
      exact le_of_eq (glue_dist_glued_points (fun x : s => (x : X)) Φ (ε₂ / 2 + δ) ⟨x, x_in_s⟩)
    · intro x' hx'
      rcases(Set.mem_image _ _ _).1 hx' with ⟨y, ⟨y_in_s', yx'⟩⟩
      rcases mem_range.1 y_in_s' with ⟨x, xy⟩
      use Fl x, mem_image_of_mem _ x.2
      rw [← yx', ← xy, dist_comm]
      exact le_of_eq (glue_dist_glued_points (@Subtype.val X s) Φ (ε₂ / 2 + δ) x)
  have : Hausdorff_dist (Fr '' range Φ) (range Fr) ≤ ε₃ :=
    by
    rw [← @image_univ _ _ Fr, Hausdorff_dist_image Ir]
    rcases exists_mem_of_nonempty Y with ⟨xY, _⟩
    rcases hs' xY with ⟨xs', Dxs'⟩
    have : 0 ≤ ε₃ := le_trans dist_nonneg Dxs'
    refine'
      Hausdorff_dist_le_of_mem_dist this (fun x hx => ⟨x, mem_univ _, by simpa only [dist_self] ⟩)
        fun x _ => _
    rcases hs' x with ⟨y, Dy⟩
    exact ⟨Φ y, mem_range_self _, Dy⟩
  linarith
#align Gromov_Hausdorff.GH_dist_le_of_approx_subsets GromovHausdorff.gHDist_le_of_approx_subsets

end

--section
/-- The Gromov-Hausdorff space is second countable. -/
instance : SecondCountableTopology GHSpace :=
  by
  refine' second_countable_of_countable_discretization fun δ δpos => _
  let ε := 2 / 5 * δ
  have εpos : 0 < ε := mul_pos (by norm_num) δpos
  have : ∀ p : GH_space, ∃ s : Set p.rep, s.Finite ∧ univ ⊆ ⋃ x ∈ s, ball x ε := fun p => by
    simpa only [subset_univ, exists_true_left] using
      finite_cover_balls_of_compact isCompact_univ εpos
  -- for each `p`, `s p` is a finite `ε`-dense subset of `p` (or rather the metric space
  -- `p.rep` representing `p`)
  choose s hs using this
  have : ∀ p : GH_space, ∀ t : Set p.rep, t.Finite → ∃ n : ℕ, ∃ e : Equiv t (Fin n), True :=
    by
    intro p t ht
    letI : Fintype t := finite.fintype ht
    exact ⟨Fintype.card t, Fintype.equivFin t, trivial⟩
  choose N e hne using this
  -- cardinality of the nice finite subset `s p` of `p.rep`, called `N p`
  let N := fun p : GH_space => N p (s p) (hs p).1
  -- equiv from `s p`, a nice finite subset of `p.rep`, to `fin (N p)`, called `E p`
  let E := fun p : GH_space => e p (s p) (hs p).1
  -- A function `F` associating to `p : GH_space` the data of all distances between points
  -- in the `ε`-dense set `s p`.
  let F : GH_space → Σn : ℕ, Fin n → Fin n → ℤ := fun p =>
    ⟨N p, fun a b => ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋⟩
  refine' ⟨Σn, Fin n → Fin n → ℤ, by infer_instance, F, fun p q hpq => _⟩
  /- As the target space of F is countable, it suffices to show that two points
    `p` and `q` with `F p = F q` are at distance `≤ δ`.
    For this, we construct a map `Φ` from `s p ⊆ p.rep` (representing `p`)
    to `q.rep` (representing `q`) which is almost an isometry on `s p`, and
    with image `s q`. For this, we compose the identification of `s p` with `fin (N p)`
    and the inverse of the identification of `s q` with `fin (N q)`. Together with
    the fact that `N p = N q`, this constructs `Ψ` between `s p` and `s q`, and then
    composing with the canonical inclusion we get `Φ`. -/
  have Npq : N p = N q := (Sigma.mk.inj_iff.1 hpq).1
  let Ψ : s p → s q := fun x => (E q).symm (Fin.cast Npq ((E p) x))
  let Φ : s p → q.rep := fun x => Ψ x
  -- Use the almost isometry `Φ` to show that `p.rep` and `q.rep`
  -- are within controlled Gromov-Hausdorff distance.
  have main : GH_dist p.rep q.rep ≤ ε + ε / 2 + ε :=
    by
    refine' GH_dist_le_of_approx_subsets Φ _ _ _
    show ∀ x : p.rep, ∃ (y : p.rep)(H : y ∈ s p), dist x y ≤ ε
    · -- by construction, `s p` is `ε`-dense
      intro x
      have : x ∈ ⋃ y ∈ s p, ball y ε := (hs p).2 (mem_univ _)
      rcases mem_Union₂.1 this with ⟨y, ys, hy⟩
      exact ⟨y, ys, le_of_lt hy⟩
    show ∀ x : q.rep, ∃ z : s p, dist x (Φ z) ≤ ε
    · -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
      intro x
      have : x ∈ ⋃ y ∈ s q, ball y ε := (hs q).2 (mem_univ _)
      rcases mem_Union₂.1 this with ⟨y, ys, hy⟩
      let i : ℕ := E q ⟨y, ys⟩
      let hi := ((E q) ⟨y, ys⟩).is_lt
      have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]
      have hiq : i < N q := hi
      have hip : i < N p := by rwa [Npq.symm] at hiq
      let z := (E p).symm ⟨i, hip⟩
      use z
      have C1 : (E p) z = ⟨i, hip⟩ := (E p).apply_symm_apply ⟨i, hip⟩
      have C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl
      have C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩ :=
        by
        rw [ihi_eq]
        exact (E q).symm_apply_apply ⟨y, ys⟩
      have : Φ z = y := by
        simp only [Φ, Ψ]
        rw [C1, C2, C3]
        rfl
      rw [this]
      exact le_of_lt hy
    show ∀ x y : s p, |dist x y - dist (Φ x) (Φ y)| ≤ ε
    · /- the distance between `x` and `y` is encoded in `F p`, and the distance between
            `Φ x` and `Φ y` (two points of `s q`) is encoded in `F q`, all this up to `ε`.
            As `F p = F q`, the distances are almost equal. -/
      intro x y
      have : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y) := rfl
      rw [this]
      -- introduce `i`, that codes both `x` and `Φ x` in `fin (N p) = fin (N q)`
      let i : ℕ := E p x
      have hip : i < N p := ((E p) x).2
      have hiq : i < N q := by rwa [Npq] at hip
      have i' : i = (E q) (Ψ x) := by simp only [Equiv.apply_symm_apply, Fin.coe_cast]
      -- introduce `j`, that codes both `y` and `Φ y` in `fin (N p) = fin (N q)`
      let j : ℕ := E p y
      have hjp : j < N p := ((E p) y).2
      have hjq : j < N q := by rwa [Npq] at hjp
      have j' : j = ((E q) (Ψ y)).1 := by
        simp only [Equiv.apply_symm_apply, [anonymous], Fin.coe_cast]
      -- Express `dist x y` in terms of `F p`
      have : (F p).2 ((E p) x) ((E p) y) = floor (ε⁻¹ * dist x y) := by
        simp only [F, (E p).symm_apply_apply]
      have Ap : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = floor (ε⁻¹ * dist x y) :=
        by
        rw [← this]
        congr <;> apply Fin.ext_iff.2 <;> rfl
      -- Express `dist (Φ x) (Φ y)` in terms of `F q`
      have : (F q).2 ((E q) (Ψ x)) ((E q) (Ψ y)) = floor (ε⁻¹ * dist (Ψ x) (Ψ y)) := by
        simp only [F, (E q).symm_apply_apply]
      have Aq : (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ = floor (ε⁻¹ * dist (Ψ x) (Ψ y)) :=
        by
        rw [← this]
        congr <;> apply Fin.ext_iff.2 <;> [exact i', exact j']
      -- use the equality between `F p` and `F q` to deduce that the distances have equal
      -- integer parts
      have : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ :=
        by
        -- we want to `subst hpq` where `hpq : F p = F q`, except that `subst` only works
        -- with a constant, so replace `F q` (and everything that depends on it) by a constant `f`
        -- then `subst`
        revert hiq hjq
        change N q with (F q).1
        generalize F q = f at hpq⊢
        subst hpq
        intros
        rfl
      rw [Ap, Aq] at this
      -- deduce that the distances coincide up to `ε`, by a straightforward computation
      -- that should be automated
      have I :=
        calc
          |ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))| :=
            (abs_mul _ _).symm
          _ = |ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)| :=
            by
            congr
            ring
          _ ≤ 1 := le_of_lt (abs_sub_lt_one_of_floor_eq_floor this)

      calc
        |dist x y - dist (Ψ x) (Ψ y)| = ε * ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| := by
          rw [mul_inv_cancel (ne_of_gt εpos), one_mul]
        _ = ε * (|ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)|) := by
          rw [abs_of_nonneg (le_of_lt (inv_pos.2 εpos)), mul_assoc]
        _ ≤ ε * 1 := (mul_le_mul_of_nonneg_left I (le_of_lt εpos))
        _ = ε := mul_one _

  calc
    dist p q = GH_dist p.rep q.rep := dist_GH_dist p q
    _ ≤ ε + ε / 2 + ε := main
    _ = δ := by
      simp only [ε]
      ring

/-- Compactness criterion: a closed set of compact metric spaces is compact if the spaces have
a uniformly bounded diameter, and for all `ε` the number of balls of radius `ε` required
to cover the spaces is uniformly bounded. This is an equivalence, but we only prove the
interesting direction that these conditions imply compactness. -/
theorem totallyBounded {t : Set GHSpace} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ}
    (ulim : Tendsto u atTop (𝓝 0)) (hdiam : ∀ p ∈ t, diam (univ : Set (GHSpace.Rep p)) ≤ C)
    (hcov :
      ∀ p ∈ t,
        ∀ n : ℕ, ∃ s : Set (GHSpace.Rep p), Cardinal.mk s ≤ K n ∧ univ ⊆ ⋃ x ∈ s, ball x (u n)) :
    TotallyBounded t :=
  by
  /- Let `δ>0`, and `ε = δ/5`. For each `p`, we construct a finite subset `s p` of `p`, which
    is `ε`-dense and has cardinality at most `K n`. Encoding the mutual distances of points in `s p`,
    up to `ε`, we will get a map `F` associating to `p` finitely many data, and making it possible to
    reconstruct `p` up to `ε`. This is enough to prove total boundedness. -/
  refine' Metric.totallyBounded_of_finite_discretization fun δ δpos => _
  let ε := 1 / 5 * δ
  have εpos : 0 < ε := mul_pos (by norm_num) δpos
  -- choose `n` for which `u n < ε`
  rcases Metric.tendsto_atTop.1 ulim ε εpos with ⟨n, hn⟩
  have u_le_ε : u n ≤ ε := by
    have := hn n le_rfl
    simp only [Real.dist_eq, add_zero, sub_eq_add_neg, neg_zero] at this
    exact le_of_lt (lt_of_le_of_lt (le_abs_self _) this)
  -- construct a finite subset `s p` of `p` which is `ε`-dense and has cardinal `≤ K n`
  have :
    ∀ p : GH_space,
      ∃ s : Set p.rep, ∃ N ≤ K n, ∃ E : Equiv s (Fin N), p ∈ t → univ ⊆ ⋃ x ∈ s, ball x (u n) :=
    by
    intro p
    by_cases hp : p ∉ t
    · have : Nonempty (Equiv (∅ : Set p.rep) (Fin 0)) :=
        by
        rw [← Fintype.card_eq]
        simp only [empty_card', Fintype.card_fin]
      use ∅, 0, bot_le, choice this
    · rcases hcov _ (Set.not_not_mem.1 hp) n with ⟨s, ⟨scard, scover⟩⟩
      rcases Cardinal.lt_aleph0.1 (lt_of_le_of_lt scard (Cardinal.nat_lt_aleph0 _)) with ⟨N, hN⟩
      rw [hN, Cardinal.natCast_le] at scard
      have : Cardinal.mk s = Cardinal.mk (Fin N) := by rw [hN, Cardinal.mk_fin]
      cases' Quotient.exact this with E
      use s, N, scard, E
      simp only [scover, imp_true_iff]
  choose s N hN E hs using this
  -- Define a function `F` taking values in a finite type and associating to `p` enough data
  -- to reconstruct it up to `ε`, namely the (discretized) distances between elements of `s p`.
  let M := ⌊ε⁻¹ * max C 0⌋₊
  let F : GH_space → Σk : Fin (K n).succ, Fin k → Fin k → Fin M.succ := fun p =>
    ⟨⟨N p, lt_of_le_of_lt (hN p) (Nat.lt_succ_self _)⟩, fun a b =>
      ⟨min M ⌊ε⁻¹ * dist ((E p).symm a) ((E p).symm b)⌋₊,
        (min_le_left _ _).trans_lt (Nat.lt_succ_self _)⟩⟩
  refine' ⟨_, _, fun p => F p, _⟩
  infer_instance
  -- It remains to show that if `F p = F q`, then `p` and `q` are `ε`-close
  rintro ⟨p, pt⟩ ⟨q, qt⟩ hpq
  have Npq : N p = N q := Fin.ext_iff.1 (Sigma.mk.inj_iff.1 hpq).1
  let Ψ : s p → s q := fun x => (E q).symm (Fin.cast Npq ((E p) x))
  let Φ : s p → q.rep := fun x => Ψ x
  have main : GH_dist p.rep q.rep ≤ ε + ε / 2 + ε :=
    by
    -- to prove the main inequality, argue that `s p` is `ε`-dense in `p`, and `s q` is `ε`-dense
    -- in `q`, and `s p` and `s q` are almost isometric. Then closeness follows
    -- from `GH_dist_le_of_approx_subsets`
    refine' GH_dist_le_of_approx_subsets Φ _ _ _
    show ∀ x : p.rep, ∃ (y : p.rep)(H : y ∈ s p), dist x y ≤ ε
    · -- by construction, `s p` is `ε`-dense
      intro x
      have : x ∈ ⋃ y ∈ s p, ball y (u n) := (hs p pt) (mem_univ _)
      rcases mem_Union₂.1 this with ⟨y, ys, hy⟩
      exact ⟨y, ys, le_trans (le_of_lt hy) u_le_ε⟩
    show ∀ x : q.rep, ∃ z : s p, dist x (Φ z) ≤ ε
    · -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
      intro x
      have : x ∈ ⋃ y ∈ s q, ball y (u n) := (hs q qt) (mem_univ _)
      rcases mem_Union₂.1 this with ⟨y, ys, hy⟩
      let i : ℕ := E q ⟨y, ys⟩
      let hi := ((E q) ⟨y, ys⟩).2
      have ihi_eq : (⟨i, hi⟩ : Fin (N q)) = (E q) ⟨y, ys⟩ := by rw [Fin.ext_iff, Fin.val_mk]
      have hiq : i < N q := hi
      have hip : i < N p := by rwa [Npq.symm] at hiq
      let z := (E p).symm ⟨i, hip⟩
      use z
      have C1 : (E p) z = ⟨i, hip⟩ := (E p).apply_symm_apply ⟨i, hip⟩
      have C2 : Fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl
      have C3 : (E q).symm ⟨i, hi⟩ = ⟨y, ys⟩ :=
        by
        rw [ihi_eq]
        exact (E q).symm_apply_apply ⟨y, ys⟩
      have : Φ z = y := by
        simp only [Φ, Ψ]
        rw [C1, C2, C3]
        rfl
      rw [this]
      exact le_trans (le_of_lt hy) u_le_ε
    show ∀ x y : s p, |dist x y - dist (Φ x) (Φ y)| ≤ ε
    · /- the distance between `x` and `y` is encoded in `F p`, and the distance between
            `Φ x` and `Φ y` (two points of `s q`) is encoded in `F q`, all this up to `ε`.
            As `F p = F q`, the distances are almost equal. -/
      intro x y
      have : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y) := rfl
      rw [this]
      -- introduce `i`, that codes both `x` and `Φ x` in `fin (N p) = fin (N q)`
      let i : ℕ := E p x
      have hip : i < N p := ((E p) x).2
      have hiq : i < N q := by rwa [Npq] at hip
      have i' : i = (E q) (Ψ x) := by simp only [Equiv.apply_symm_apply, Fin.coe_cast]
      -- introduce `j`, that codes both `y` and `Φ y` in `fin (N p) = fin (N q)`
      let j : ℕ := E p y
      have hjp : j < N p := ((E p) y).2
      have hjq : j < N q := by rwa [Npq] at hjp
      have j' : j = (E q) (Ψ y) := by simp only [Equiv.apply_symm_apply, Fin.coe_cast]
      -- Express `dist x y` in terms of `F p`
      have Ap : ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ⌊ε⁻¹ * dist x y⌋₊ :=
        calc
          ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ((F p).2 ((E p) x) ((E p) y)).1 := by
            congr <;> apply Fin.ext_iff.2 <;> rfl
          _ = min M ⌊ε⁻¹ * dist x y⌋₊ := by simp only [F, (E p).symm_apply_apply]
          _ = ⌊ε⁻¹ * dist x y⌋₊ := by
            refine' min_eq_right (Nat.floor_mono _)
            refine' mul_le_mul_of_nonneg_left (le_trans _ (le_max_left _ _)) (inv_pos.2 εpos).le
            change dist (x : p.rep) y ≤ C
            refine'
              le_trans (dist_le_diam_of_mem is_compact_univ.bounded (mem_univ _) (mem_univ _)) _
            exact hdiam p pt

      -- Express `dist (Φ x) (Φ y)` in terms of `F q`
      have Aq : ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ :=
        calc
          ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = ((F q).2 ((E q) (Ψ x)) ((E q) (Ψ y))).1 := by
            congr <;> apply Fin.ext_iff.2 <;> [exact i', exact j']
          _ = min M ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ := by simp only [F, (E q).symm_apply_apply]
          _ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋₊ :=
            by
            refine' min_eq_right (Nat.floor_mono _)
            refine' mul_le_mul_of_nonneg_left (le_trans _ (le_max_left _ _)) (inv_pos.2 εpos).le
            change dist (Ψ x : q.rep) (Ψ y) ≤ C
            refine'
              le_trans (dist_le_diam_of_mem is_compact_univ.bounded (mem_univ _) (mem_univ _)) _
            exact hdiam q qt

      -- use the equality between `F p` and `F q` to deduce that the distances have equal
      -- integer parts
      have : ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 :=
        by
        -- we want to `subst hpq` where `hpq : F p = F q`, except that `subst` only works
        -- with a constant, so replace `F q` (and everything that depends on it) by a constant `f`
        -- then `subst`
        revert hiq hjq
        change N q with (F q).1
        generalize F q = f at hpq⊢
        subst hpq
        intros
        rfl
      have : ⌊ε⁻¹ * dist x y⌋ = ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋ :=
        by
        rw [Ap, Aq] at this
        have D : 0 ≤ ⌊ε⁻¹ * dist x y⌋ :=
          floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos.2 εpos)) dist_nonneg)
        have D' : 0 ≤ ⌊ε⁻¹ * dist (Ψ x) (Ψ y)⌋ :=
          floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos.2 εpos)) dist_nonneg)
        rw [← Int.toNat_of_nonneg D, ← Int.toNat_of_nonneg D', Int.floor_toNat, Int.floor_toNat,
          this]
      -- deduce that the distances coincide up to `ε`, by a straightforward computation
      -- that should be automated
      have I :=
        calc
          |ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)| = |ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))| :=
            (abs_mul _ _).symm
          _ = |ε⁻¹ * dist x y - ε⁻¹ * dist (Ψ x) (Ψ y)| :=
            by
            congr
            ring
          _ ≤ 1 := le_of_lt (abs_sub_lt_one_of_floor_eq_floor this)

      calc
        |dist x y - dist (Ψ x) (Ψ y)| = ε * ε⁻¹ * |dist x y - dist (Ψ x) (Ψ y)| := by
          rw [mul_inv_cancel (ne_of_gt εpos), one_mul]
        _ = ε * (|ε⁻¹| * |dist x y - dist (Ψ x) (Ψ y)|) := by
          rw [abs_of_nonneg (le_of_lt (inv_pos.2 εpos)), mul_assoc]
        _ ≤ ε * 1 := (mul_le_mul_of_nonneg_left I (le_of_lt εpos))
        _ = ε := mul_one _

  calc
    dist p q = GH_dist p.rep q.rep := dist_GH_dist p q
    _ ≤ ε + ε / 2 + ε := main
    _ = δ / 2 := by
      simp only [ε, one_div]
      ring
    _ < δ := half_lt_self δpos

#align Gromov_Hausdorff.totally_bounded GromovHausdorff.totallyBounded

section Complete

/- We will show that a sequence `u n` of compact metric spaces satisfying
`dist (u n) (u (n+1)) < 1/2^n` converges, which implies completeness of the Gromov-Hausdorff space.
We need to exhibit the limiting compact metric space. For this, start from
a sequence `X n` of representatives of `u n`, and glue in an optimal way `X n` to `X (n+1)`
for all `n`, in a common metric space. Formally, this is done as follows.
Start from `Y 0 = X 0`. Then, glue `X 0` to `X 1` in an optimal way, yielding a space
`Y 1` (with an embedding of `X 1`). Then, consider an optimal gluing of `X 1` and `X 2`, and
glue it to `Y 1` along their common subspace `X 1`. This gives a new space `Y 2`, with an
embedding of `X 2`. Go on, to obtain a sequence of spaces `Y n`. Let `Z0` be the inductive
limit of the `Y n`, and finally let `Z` be the completion of `Z0`.
The images `X2 n` of `X n` in `Z` are at Hausdorff distance `< 1/2^n` by construction, hence they
form a Cauchy sequence for the Hausdorff distance. By completeness (of `Z`, and therefore of its
set of nonempty compact subsets), they converge to a limit `L`. This is the nonempty
compact metric space we are looking for.  -/
variable (X : ℕ → Type) [∀ n, MetricSpace (X n)] [∀ n, CompactSpace (X n)] [∀ n, Nonempty (X n)]

/-- Auxiliary structure used to glue metric spaces below, recording an isometric embedding
of a type `A` in another metric space. -/
structure AuxGluingStruct (A : Type) [MetricSpace A] : Type 1 where
  Space : Type
  metric : MetricSpace space
  embed : A → space
  isom : Isometry embed
#align Gromov_Hausdorff.aux_gluing_struct GromovHausdorff.AuxGluingStruct

attribute [local instance] aux_gluing_struct.metric

instance (A : Type) [MetricSpace A] : Inhabited (AuxGluingStruct A) :=
  ⟨{  Space := A
      metric := by infer_instance
      embed := id
      isom := fun x y => rfl }⟩

/-- Auxiliary sequence of metric spaces, containing copies of `X 0`, ..., `X n`, where each
`X i` is glued to `X (i+1)` in an optimal way. The space at step `n+1` is obtained from the space
at step `n` by adding `X (n+1)`, glued in an optimal way to the `X n` already sitting there. -/
def auxGluing (n : ℕ) : AuxGluingStruct (X n) :=
  Nat.recOn n default fun n Y =>
    { Space := GlueSpace Y.isom (isometry_optimalGHInjl (X n) (X (n + 1)))
      metric := by infer_instance
      embed :=
        toGlueR Y.isom (isometry_optimalGHInjl (X n) (X (n + 1))) ∘ optimalGHInjr (X n) (X (n + 1))
      isom := (toGlueR_isometry _ _).comp (isometry_optimalGHInjr (X n) (X (n + 1))) }
#align Gromov_Hausdorff.aux_gluing GromovHausdorff.auxGluing

/-- The Gromov-Hausdorff space is complete. -/
instance : CompleteSpace GHSpace :=
  by
  have : ∀ n : ℕ, 0 < ((1 : ℝ) / 2) ^ n := by
    apply pow_pos
    norm_num
  -- start from a sequence of nonempty compact metric spaces within distance `1/2^n` of each other
  refine'
    Metric.complete_of_convergent_controlled_sequences (fun n => (1 / 2) ^ n) this fun u hu => _
  -- `X n` is a representative of `u n`
  let X n := (u n).rep
  -- glue them together successively in an optimal way, getting a sequence of metric spaces `Y n`
  let Y := aux_gluing X
  -- this equality is true by definition but Lean unfolds some defs in the wrong order
  have E :
    ∀ n : ℕ,
      glue_space (Y n).isom (isometry_optimal_GH_injl (X n) (X (n + 1))) = (Y (n + 1)).Space :=
    fun n => by
    dsimp only [Y, aux_gluing]
    rfl
  let c n := cast (E n)
  have ic : ∀ n, Isometry (c n) := fun n x y =>
    by
    dsimp only [Y, aux_gluing]
    exact rfl
  -- there is a canonical embedding of `Y n` in `Y (n+1)`, by construction
  let f : ∀ n, (Y n).Space → (Y (n + 1)).Space := fun n =>
    c n ∘ to_glue_l (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ))
  have I : ∀ n, Isometry (f n) := fun n => (ic n).comp (to_glue_l_isometry _ _)
  -- consider the inductive limit `Z0` of the `Y n`, and then its completion `Z`
  let Z0 := Metric.InductiveLimit I
  let Z := UniformSpace.Completion Z0
  let Φ := to_inductive_limit I
  let coeZ := (coe : Z0 → Z)
  -- let `X2 n` be the image of `X n` in the space `Z`
  let X2 n := range (coeZ ∘ Φ n ∘ (Y n).embed)
  have isom : ∀ n, Isometry (coeZ ∘ Φ n ∘ (Y n).embed) :=
    by
    intro n
    refine' uniform_space.completion.coe_isometry.comp _
    exact (to_inductive_limit_isometry _ _).comp (Y n).isom
  -- The Hausdorff distance of `X2 n` and `X2 (n+1)` is by construction the distance between
  -- `u n` and `u (n+1)`, therefore bounded by `1/2^n`
  have D2 : ∀ n, Hausdorff_dist (X2 n) (X2 n.succ) < (1 / 2) ^ n :=
    by
    intro n
    have X2n :
      X2 n =
        range
          ((coeZ ∘
              Φ n.succ ∘ c n ∘ to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ))) ∘
            optimal_GH_injl (X n) (X n.succ)) :=
      by
      change
        X2 n =
          range
            (coeZ ∘
              Φ n.succ ∘
                c n ∘
                  to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ)) ∘
                    optimal_GH_injl (X n) (X n.succ))
      simp only [X2, Φ]
      rw [← to_inductive_limit_commute I]
      simp only [f]
      rw [← to_glue_commute]
    rw [range_comp] at X2n
    have X2nsucc :
      X2 n.succ =
        range
          ((coeZ ∘
              Φ n.succ ∘ c n ∘ to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ))) ∘
            optimal_GH_injr (X n) (X n.succ)) :=
      by rfl
    rw [range_comp] at X2nsucc
    rw [X2n, X2nsucc, Hausdorff_dist_image, Hausdorff_dist_optimal, ← dist_GH_dist]
    · exact hu n n n.succ (le_refl n) (le_succ n)
    · apply uniform_space.completion.coe_isometry.comp _
      exact (to_inductive_limit_isometry _ _).comp ((ic n).comp (to_glue_r_isometry _ _))
  -- consider `X2 n` as a member `X3 n` of the type of nonempty compact subsets of `Z`, which
  -- is a metric space
  let X3 : ℕ → nonempty_compacts Z := fun n =>
    ⟨⟨X2 n, isCompact_range (isom n).Continuous⟩, range_nonempty _⟩
  -- `X3 n` is a Cauchy sequence by construction, as the successive distances are
  -- bounded by `(1/2)^n`
  have : CauchySeq X3 :=
    by
    refine' cauchySeq_of_le_geometric (1 / 2) 1 (by norm_num) fun n => _
    rw [one_mul]
    exact le_of_lt (D2 n)
  -- therefore, it converges to a limit `L`
  rcases cauchySeq_tendsto_of_complete this with ⟨L, hL⟩
  -- the images of `X3 n` in the Gromov-Hausdorff space converge to the image of `L`
  have M : tendsto (fun n => (X3 n).toGHSpace) at_top (𝓝 L.to_GH_space) :=
    tendsto.comp (to_GH_space_continuous.tendsto _) hL
  -- By construction, the image of `X3 n` in the Gromov-Hausdorff space is `u n`.
  have : ∀ n, (X3 n).toGHSpace = u n := by
    intro n
    rw [nonempty_compacts.to_GH_space, ← (u n).toGHSpace_rep,
      to_GH_space_eq_to_GH_space_iff_isometry_equiv]
    constructor
    convert(isom n).isometryEquivOnRange.symm
  -- Finally, we have proved the convergence of `u n`
  exact ⟨L.to_GH_space, by simpa only [this] using M⟩

end Complete

--section
end GromovHausdorff

--namespace

author: leanprover-community


text:
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura

! This file was ported from Lean 3 source module data.nat.gcd.big_operators
! leanprover-community/mathlib commit 327c3c0d9232d80e250dc8f65e7835b82b266ea5
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Data.Nat.Gcd.Basic
import Mathbin.Algebra.BigOperators.Basic

/-! # Lemmas about coprimality with big products.

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.

These lemmas are kept separate from `data.nat.gcd.basic` in order to minimize imports.
-/

namespace Nat

open BigOperators

#print Nat.coprime_prod_left /-
/-- See `is_coprime.prod_left` for the corresponding lemma about `is_coprime` -/
theorem coprime_prod_left {ι : Type _} {x : ℕ} {s : ι → ℕ} {t : Finset ι} :
    (∀ i : ι, i ∈ t → coprime (s i) x) → coprime (∏ i : ι in t, s i) x :=
  Finset.prod_induction s (fun y => y.coprime x) (fun a b => coprime.mul) (by simp)
#align nat.coprime_prod_left Nat.coprime_prod_left
-/

#print Nat.coprime_prod_right /-
/-- See `is_coprime.prod_right` for the corresponding lemma about `is_coprime` -/
theorem coprime_prod_right {ι : Type _} {x : ℕ} {s : ι → ℕ} {t : Finset ι} :
    (∀ i : ι, i ∈ t → coprime x (s i)) → coprime x (∏ i : ι in t, s i) :=
  Finset.prod_induction s (fun y => x.coprime y) (fun a b => coprime.mul_right) (by simp)
#align nat.coprime_prod_right Nat.coprime_prod_right
-/

end Nat


text:
import data.rat
import data.set.basic
import order.bounds

open classical
/-import order.bounds
import data.rat

class linear_order (α : Type)

is a structure (in fact a class) which looks like this:

There's a function
le : α → α → Prop

with notation ≤ ( type with \le )

There is also lt : α → α → Prop with notation <
satisfying a < b ↔ (a ≤ b ∧ ¬ b ≤ a)

Axioms:

(le_refl : ∀ a : α, a ≤ a)
(le_trans : ∀ a b c : α, a ≤ b → b ≤ c → a ≤ c)
(le_antisymm : ∀ a b : α, a ≤ b → b ≤ a → a = b)
(le_total : ∀ a b : α, a ≤ b ∨ b ≤ a)

And here are some definitions from order.bounds, valid
for α a total order:

def upper_bounds (s : set α) : set α := { x | ∀a ∈ s, a ≤ x }
def lower_bounds (s : set α) : set α := { x | ∀a ∈ s, x ≤ a }
def is_least (s : set α) (a : α) : Prop := a ∈ s ∧ a ∈ lower_bounds s
def is_greatest (s : set α) (a : α) : Prop := a ∈ s ∧ a ∈ upper_bounds s
def is_lub (s : set α) : α → Prop := is_least (upper_bounds s)
def is_glb (s : set α) : α → Prop := is_greatest (lower_bounds s)
-/

structure Dedekind_real :=
(carrier : set ℚ)
(nonemp : ∃ a, a ∈ carrier)
(nonrat : ∃ a, a ∉ carrier)
(down : ∀ p ∈ carrier, ∀ q, q ≤ p → q ∈ carrier)
(nomax : ∀ p ∈ carrier, ∃ q, q ∈ carrier ∧ p ≤ q ∧ p ≠ q)

notation `ℝ` := Dedekind_real

instance : has_coe ℝ (set ℚ) := ⟨λ r, r.carrier⟩

namespace Dedekind_real

protected def le (α β : ℝ) : Prop := (α : set ℚ) ⊆ β
protected def lt (α β : ℝ) : Prop := (α : set ℚ) ⊂ β

-- notation typeclass
instance : has_le ℝ := ⟨Dedekind_real.le⟩
instance : has_lt ℝ := ⟨Dedekind_real.lt⟩

def union_of_ne_b_r_set (S : set ℝ) (hne : ∃ s, s ∈ S) (hb : ∃ (b : ℝ), ∀ (s ∈ S), s ≤ b) : ℝ :=
⟨{x : ℚ | ∃ (s : ℝ), s ∈ S ∧ x ∈ (s : ℝ).carrier},
exists.elim hne (λ s hs, exists.elim s.nonemp (λ q hq, ⟨q, ⟨s, hs, hq⟩ ⟩ ) ),
exists.elim hb (λ b h, exists.elim b.nonrat (λ q hnq, ⟨q, (λ h0, hnq
(exists.elim h0 (λ s H, ( (h s) H.left ) H.right ) ) ) ⟩ )),
(λ p hp q hqp, exists.elim hp (λ s H, ⟨s, H.left, s.down p H.right q hqp⟩ ) ),
(λ p hp, exists.elim hp (λ s H, exists.elim (s.nomax p H.right) (λ r H0, ⟨r, ⟨s, H.left, H0.left ⟩,
H0.right.left, H0.right.right ⟩ ) ) ) ⟩

def arthm_mean (a b : ℚ) : ℚ := (a + b)/2

end Dedekind_real

open Dedekind_real

lemma bounded_by_non_elements : ∀ (α : ℝ) (x : ℚ),
x ∉ α.carrier ↔ (∀ (q ∈ α.carrier), q < x) := λ α x,
⟨(λ h q hq, classical.by_contradiction (λ hn, h (α.down q hq x (le_of_not_lt hn)))),
(λ h hx, (λ (h0 : x < x), not_lt_of_le (le_refl x) h0) (h x hx))⟩

lemma real_intro : ∀ {a b : ℝ}, a.carrier = b.carrier → a = b
| ⟨a, _, _, _, _⟩ ⟨b, _, _, _, _⟩ rfl := rfl

lemma le_intro : ∀ {a b : ℝ}, a.carrier ⊆ b.carrier → a ≤ b := λ a b h x hb, h hb

theorem eq_reals (a b : ℝ) : a = b ↔ a.carrier = b.carrier := ⟨λ hab, by rw hab,
real_intro⟩

theorem arthm_mean_bounded_q : ∀ (a b : ℚ), a < b → (a < arthm_mean a b ∧ arthm_mean a b < b) := λ a b hab,
⟨by calc a = a/2*2 : eq.symm (@div_mul_cancel _ _ a 2 (dec_trivial) )
... = a/2 + a/2 : mul_two (a/2)
... < a/2 + b/2 : (λ (h1 : (0 : ℚ) < 2), add_lt_add_left
( (div_lt_div_right h1).2 hab) (a/2) ) dec_trivial
... = (a + b)/2 : eq.symm (add_div a b 2),
by calc (a + b)/2 = a/2 + b/2 : add_div a b 2
... < b/2 + b/2 : (λ (h1 : (0 : ℚ) < 2), add_lt_add_right
( (div_lt_div_right h1).2 hab) (b/2) ) dec_trivial
... = b/2*2 : eq.symm (mul_two (b/2) )
... = b : (@div_mul_cancel _ _ b 2 (dec_trivial) ) ⟩

namespace Dedekind_real

def lt_rat_r (p : ℚ) : ℝ := ⟨{q | q < p}, ⟨p-1, trans_rel_left rat.has_lt.lt (lt_add_one (p-1) )
(sub_add_cancel p 1) ⟩, ⟨p+1, (λ h, (not_lt_of_lt (lt_add_one p) ) h) ⟩, (λ q hq r hrq, lt_of_le_of_lt hrq hq),
(λ q hq, ⟨ (q+p)/2, (arthm_mean_bounded_q q p hq).right, le_of_lt ( (arthm_mean_bounded_q q p hq).left),
ne_of_lt ( (arthm_mean_bounded_q q p hq).left) ⟩ ) ⟩

protected def add (α β : ℝ) : ℝ := ⟨{x | ∃ (a b : ℚ), a ∈ α.carrier ∧ b ∈ β.carrier ∧ x = a + b},
(exists.elim α.nonemp (λ a haα, exists.elim β.nonemp (λ b hbβ, ⟨a + b, ⟨a, b, haα, hbβ, rfl ⟩ ⟩ ) ) ), --nonemp
exists.elim α.nonrat (exists.elim β.nonrat (λ b hbβ a haα, ⟨a+b, not_exists.2 (λ a0,
not_exists.2 (λ b0 h, absurd (eq.symm h.right.right) (ne_of_lt (add_lt_add_of_lt_of_le
( ( bounded_by_non_elements α a ).1 haα a0 h.left )
( le_of_lt ( ( bounded_by_non_elements β b ).1 hbβ b0 h.right.left ) ) ) ) ) ) ⟩ ) ), --nonrat
(λ p padd q hqp, exists.elim padd (λ a hb, exists.elim hb (λ b h, ⟨ q-b, b,
(α.down a h.left (q-b) (trans_rel_left rat.le (add_le_add_right (trans_rel_left rat.le hqp h.right.right)
(-b) ) (add_sub_cancel a b) ) ),
h.right.left, eq.symm (sub_add_cancel q b) ⟩ ) ) ), --down
(λ p padd, exists.elim padd (λ a H, exists.elim H (λ b h, exists.elim (α.nomax a h.left)
(λ c hc, ⟨c + b, ⟨c, b, hc.left, h.right.left, rfl⟩, (trans_rel_right rat.le h.right.right
(add_le_add_right hc.right.left b) ), (λ hn, hc.right.right ( (add_right_inj b).1
(eq.trans (eq.symm h.right.right) hn) ) ) ⟩ ) ) ) ) ⟩ --nomax

protected def zero : ℝ := lt_rat_r 0

/-
protected def neg (α : ℝ) : ℝ := ⟨{p : ℚ | ∀ (q : ℚ), q ∈ α.carrier → p < -q},
exists.elim α.nonrat (λ r hr, ⟨-r, (λ q hq, neg_lt_neg_iff.2 ( (bounded_by_non_elements α r).1 hr q hq) ) ⟩ ),
(classical.by_contradiction (λ h, exists.elim α.nonemp (λ q0 hq0, (not_lt_of_lt (lt_add_one (-q0) ) )
(classical.not_exists_not.1 h (-q0 + 1) q0 hq0 ) ) ) ), _, _⟩
-/
instance : has_add ℝ := ⟨Dedekind_real.add⟩
instance : has_zero ℝ := ⟨Dedekind_real.zero⟩

end Dedekind_real

variables (a b : ℝ)
variable (h : ¬∃ (x : ℚ), x ∈ a.carrier ∧ x ∉ b.carrier)
variable (x : ℚ)
variable (hxa : x ∈ (↑a : set ℚ))

--#check (not_exists.1 h x : ¬(x ∈ ↑a ∧ x ∉ ↑b))

--⊢ ¬(x ∈ ↑a ∧ x ∉ ↑b)

lemma le_total_r : ∀ a b : ℝ, a ≤ b ∨ b ≤ a := λ a b, (em (∃ x, x ∈ a.carrier ∧ x ∉ b.carrier)).elim
(λ h, exists.elim h (λ x H, or.inr (λ y hyb, (a.down x H.left y
(le_of_lt ( (bounded_by_non_elements b x).1 H.right y hyb) ) ) ) ) )
(λ h, or.inl (λ x hxa, classical.not_not.1 (not_and.1 ((@not_exists ℚ _).1 h x) hxa) ) )

instance linear_order_r : linear_order ℝ := ⟨Dedekind_real.le, Dedekind_real.lt, (λ a x h, h),
(λ a b c hab hbc x hxa, hbc (hab hxa) ), ((λ a b, ⟨(λ hab, ⟨hab.left,(λ hba, hab.right (antisymm hab.left hba))⟩),
(λ h, ⟨h.left,(λ hab, h.right (((@set.subset.antisymm_iff _ ↑a ↑b).1) hab).right)⟩)⟩)), λ a b hab hba,
(eq_reals a b).2 ((set.ext_iff a.carrier b.carrier).2 (λ x, ⟨(λ hxa, hab hxa),(λ hxb, hba hxb)⟩)), le_total_r⟩

lemma union_is_bound (S : set ℝ) (hne : ∃ s, s ∈ S) (hb : ∃ (b : ℝ), ∀ (s ∈ S), s ≤ b) :
(union_of_ne_b_r_set S hne hb) ∈ upper_bounds S := λ s hs x hxs, ⟨s, hs, hxs⟩

theorem has_lub_property (S : set ℝ) (hne : ∃ s, s ∈ S) (hb : ∃ (b : ℝ), ∀ (s ∈ S), s ≤ b) :
(∃ (b : ℝ), is_lub S b) := ⟨union_of_ne_b_r_set S hne hb, ⟨(λ s hs x hxs, ⟨s, hs, hxs⟩),
(λ s hs x hx, exists.elim hx (λ sx hsx, hs sx hsx.left hsx.right ) ) ⟩ ⟩

theorem add_assoc_r (a b c : ℝ) : a + b + c = a + (b + c) := real_intro (set.ext (λ x,
⟨ (λ hx, exists.elim hx (λ ab hc, exists.elim hc (λ c hab, exists.elim hab.left (λ a hb, exists.elim hb
(λ b h, ⟨a, b+c, h.left, ⟨b, c, h.right.left, hab.right.left, rfl⟩, eq.trans hab.right.right (eq.trans
( (add_right_inj c).2 h.right.right) (add_assoc a b c) ) ⟩ ) ) ) ) ), -- left inclusion
(λ hx, exists.elim hx (λ a hbc, exists.elim hbc (λ bc hbc, exists.elim hbc.right.left (λ b hc, exists.elim hc
(λ c h, ⟨ a + b, c, ⟨a, b, hbc.left, h.left, rfl⟩ , h.right.left, eq.trans hbc.right.right (eq.trans
( (add_left_inj a).2 h.right.right) (eq.symm (add_assoc a b c) ) ) ⟩ ) ) ) ) ) ⟩ ) ) --right inclusion

theorem add_comm_r (a b : ℝ) : a + b = b + a := real_intro (set.ext (λ x,
⟨λ hx, exists.elim hx (λ a hb, exists.elim hb (λ b h, ⟨b, a, h.right.left, h.left,
eq.trans h.right.right (add_comm a b) ⟩ ) ),
λ hx, exists.elim hx (λ b ha, exists.elim ha (λ a h, ⟨a, b, h.right.left, h.left,
eq.trans h.right.right (add_comm b a)⟩  ) ) ⟩ ) )

theorem zero_add_r (α : ℝ) : α + 0 = α := real_intro (set.ext (λ x, ⟨ (λ hx, exists.elim hx (λ a h0,
exists.elim h0 (λ b h, α.down a h.left x (le_of_lt (by calc x = a + b : h.right.right
... < a + 0 : add_lt_add_of_le_of_lt (le_refl a) h.right.left
... = a : add_zero a) ) ) ) ), (λ hx, exists.elim (α.nomax x hx) (λ a h, ⟨a, x-a, h.left,
sub_lt_zero.2 (lt_of_le_of_ne h.right.left h.right.right), eq.symm (add_sub_cancel'_right a x) ⟩ ) ) ⟩ ) )

theorem add_zero_r (α : ℝ) : 0 + α = α := eq.trans (add_comm_r 0 α) (zero_add_r α)

author: ImperialCollegeLondon


text:
/-
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.category_theory.limits.shapes.equalizers
import Mathlib.PostPort

universes v u l u₂

namespace Mathlib

/-!
# Split coequalizers

We define what it means for a triple of morphisms `f g : X ⟶ Y`, `π : Y ⟶ Z` to be a split
coequalizer: there is a section `s` of `π` and a section `t` of `g`, which additionally satisfy
`t ≫ f = π ≫ s`.

In addition, we show that every split coequalizer is a coequalizer
(`category_theory.is_split_coequalizer.is_coequalizer`) and absolute
(`category_theory.is_split_coequalizer.map`)

A pair `f g : X ⟶ Y` has a split coequalizer if there is a `Z` and `π : Y ⟶ Z` making `f,g,π` a
split coequalizer.
A pair `f g : X ⟶ Y` has a `G`-split coequalizer if `G f, G g` has a split coequalizer.

These definitions and constructions are useful in particular for the monadicity theorems.

## TODO

Dualise to split equalizers.
-/

namespace category_theory

/--
A split coequalizer diagram consists of morphisms

      f   π
    X ⇉ Y → Z
      g

satisfying `f ≫ π = g ≫ π` together with morphisms

      t   s
    X ← Y ← Z

satisfying `s ≫ π = 𝟙 Z`, `t ≫ g = 𝟙 Y` and `t ≫ f = π ≫ s`.

The name "coequalizer" is appropriate, since any split coequalizer is a coequalizer, see
`category_theory.is_split_coequalizer.is_coequalizer`.
Split coequalizers are also absolute, since a functor preserves all the structure above.
-/
structure is_split_coequalizer {C : Type u} [category C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) {Z : C} (π : Y ⟶ Z)
where
  right_section : Z ⟶ Y
  left_section : Y ⟶ X
  condition : f ≫ π = g ≫ π
  right_section_π : right_section ≫ π = 𝟙
  left_section_bottom : left_section ≫ g = 𝟙
  left_section_top : left_section ≫ f = π ≫ right_section

protected instance is_split_coequalizer.inhabited {C : Type u} [category C] {X : C} : Inhabited (is_split_coequalizer 𝟙 𝟙 𝟙) :=
  { default := is_split_coequalizer.mk 𝟙 𝟙 sorry sorry sorry sorry }

theorem is_split_coequalizer.condition_assoc {C : Type u} [category C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (c : is_split_coequalizer f g π) {X' : C} (f' : Z ⟶ X') : f ≫ π ≫ f' = g ≫ π ≫ f' := sorry

@[simp] theorem is_split_coequalizer.right_section_π_assoc {C : Type u} [category C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (c : is_split_coequalizer f g π) {X' : C} (f' : Z ⟶ X') : is_split_coequalizer.right_section c ≫ π ≫ f' = f' := sorry

/-- Split coequalizers are absolute: they are preserved by any functor. -/
@[simp] theorem is_split_coequalizer.map_left_section {C : Type u} [category C] {D : Type u₂} [category D] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} (q : is_split_coequalizer f g π) (F : C ⥤ D) : is_split_coequalizer.left_section (is_split_coequalizer.map q F) = functor.map F (is_split_coequalizer.left_section q) :=
  Eq.refl (is_split_coequalizer.left_section (is_split_coequalizer.map q F))

/-- A split coequalizer clearly induces a cofork. -/
@[simp] theorem is_split_coequalizer.as_cofork_X {C : Type u} [category C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} {Z : C} {h : Y ⟶ Z} (t : is_split_coequalizer f g h) : limits.cocone.X (is_split_coequalizer.as_cofork t) = Z :=
  Eq.refl Z

/--
The cofork induced by a split coequalizer is a coequalizer, justifying the name. In some cases it
is more convenient to show a given cofork is a coequalizer by showing it is split.
-/
def is_split_coequalizer.is_coequalizer {C : Type u} [category C] {X : C} {Y : C} {f : X ⟶ Y} {g : X ⟶ Y} {Z : C} {h : Y ⟶ Z} (t : is_split_coequalizer f g h) : limits.is_colimit (is_split_coequalizer.as_cofork t) :=
  limits.cofork.is_colimit.mk' (is_split_coequalizer.as_cofork t)
    fun (s : limits.cofork f g) => { val := is_split_coequalizer.right_section t ≫ limits.cofork.π s, property := sorry }

/--
The pair `f,g` is a split pair if there is a `h : Y ⟶ Z` so that `f, g, h` forms a split coequalizer
in `C`.
-/
class has_split_coequalizer {C : Type u} [category C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y)
where
  splittable : Exists fun {Z : C} => ∃ (h : Y ⟶ Z), Nonempty (is_split_coequalizer f g h)

/--
The pair `f,g` is a `G`-split pair if there is a `h : G Y ⟶ Z` so that `G f, G g, h` forms a split
coequalizer in `D`.
-/
def functor.is_split_pair {C : Type u} [category C] {D : Type u₂} [category D] (G : C ⥤ D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) :=
  has_split_coequalizer (functor.map G f) (functor.map G g)

/-- Get the coequalizer object from the typeclass `is_split_pair`. -/
def has_split_coequalizer.coequalizer_of_split {C : Type u} [category C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [has_split_coequalizer f g] : C :=
  Exists.some (has_split_coequalizer.splittable f g)

/-- Get the coequalizer morphism from the typeclass `is_split_pair`. -/
def has_split_coequalizer.coequalizer_π {C : Type u} [category C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [has_split_coequalizer f g] : Y ⟶ has_split_coequalizer.coequalizer_of_split f g :=
  Exists.some sorry

/-- The coequalizer morphism `coequalizer_ι` gives a split coequalizer on `f,g`. -/
def has_split_coequalizer.is_split_coequalizer {C : Type u} [category C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [has_split_coequalizer f g] : is_split_coequalizer f g (has_split_coequalizer.coequalizer_π f g) :=
  Classical.choice sorry

/-- If `f, g` is split, then `G f, G g` is split. -/
protected instance map_is_split_pair {C : Type u} [category C] {D : Type u₂} [category D] (G : C ⥤ D) {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [has_split_coequalizer f g] : has_split_coequalizer (functor.map G f) (functor.map G g) :=
  has_split_coequalizer.mk
    (Exists.intro (functor.obj G (has_split_coequalizer.coequalizer_of_split f g))
      (Exists.intro (functor.map G (has_split_coequalizer.coequalizer_π f g))
        (Nonempty.intro (is_split_coequalizer.map (has_split_coequalizer.is_split_coequalizer f g) G))))

namespace limits

/-- If a pair has a split coequalizer, it has a coequalizer. -/
protected instance has_coequalizer_of_has_split_coequalizer {C : Type u} [category C] {X : C} {Y : C} (f : X ⟶ Y) (g : X ⟶ Y) [has_split_coequalizer f g] : has_coequalizer f g :=
  has_colimit.mk
    (colimit_cocone.mk (is_split_coequalizer.as_cofork (has_split_coequalizer.is_split_coequalizer f g))
      (is_split_coequalizer.is_coequalizer (has_split_coequalizer.is_split_coequalizer f g)))

author: AurelienSaue


text:
/-
Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Robert Y. Lewis, Sébastien Gouëzel
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.analysis.normed_space.basic
import Mathlib.PostPort

universes v u

namespace Mathlib

/-!
# Completeness in terms of `cauchy` filters vs `is_cau_seq` sequences

In this file we apply `metric.complete_of_cauchy_seq_tendsto` to prove that a `normed_ring`
is complete in terms of `cauchy` filter if and only if it is complete in terms
of `cau_seq` Cauchy sequences.
-/

theorem cau_seq.tendsto_limit {β : Type v} [normed_ring β] [hn : is_absolute_value norm] (f : cau_seq β norm) [cau_seq.is_complete β norm] : filter.tendsto (⇑f) filter.at_top (nhds (cau_seq.lim f)) := sorry

/-
 This section shows that if we have a uniform space generated by an absolute value, topological
 completeness and Cauchy sequence completeness coincide. The problem is that there isn't
 a good notion of "uniform space generated by an absolute value", so right now this is
 specific to norm. Furthermore, norm only instantiates is_absolute_value on normed_field.
 This needs to be fixed, since it prevents showing that ℤ_[hp] is complete
-/

protected instance normed_field.is_absolute_value {β : Type v} [normed_field β] : is_absolute_value norm :=
  is_absolute_value.mk norm_nonneg (fun (_x : β) => norm_eq_zero) norm_add_le normed_field.norm_mul

theorem cauchy_seq.is_cau_seq {β : Type v} [normed_field β] {f : ℕ → β} (hf : cauchy_seq f) : is_cau_seq norm f := sorry

theorem cau_seq.cauchy_seq {β : Type v} [normed_field β] (f : cau_seq β norm) : cauchy_seq ⇑f := sorry

/-- In a normed field, `cau_seq` coincides with the usual notion of Cauchy sequences. -/
theorem cau_seq_iff_cauchy_seq {α : Type u} [normed_field α] {u : ℕ → α} : is_cau_seq norm u ↔ cauchy_seq u :=
  { mp := fun (h : is_cau_seq norm u) => cau_seq.cauchy_seq { val := u, property := h },
    mpr := fun (h : cauchy_seq u) => cauchy_seq.is_cau_seq h }

/-- A complete normed field is complete as a metric space, as Cauchy sequences converge by
assumption and this suffices to characterize completeness. -/
protected instance complete_space_of_cau_seq_complete {β : Type v} [normed_field β] [cau_seq.is_complete β norm] : complete_space β := sorry


text:
/-
Copyright (c) 2021 OpenAI. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kunhao Zheng, Stanislas Polu, David Renshaw, OpenAI GPT-f
-/
import mathzoo.imports.miniF2F

open_locale nat rat real big_operators topological_space

theorem aime_1983_p9
  (x : ℝ)
  (h₀ : 0 < x ∧ x < real.pi) :
  12 ≤ ((9 * (x^2 * (real.sin x)^2)) + 4) / (x * real.sin x) :=
begin
  let y := x * real.sin x,
  rw ← mul_pow,
  change 12 ≤ (9 * y^2 + 4) / y,
  refine (le_div_iff _).mpr _,
  apply mul_pos h₀.1,
  apply real.sin_pos_of_pos_of_lt_pi h₀.1 h₀.2,
  suffices : 0 ≤ (3 * y - 2)^2, nlinarith,
  exact pow_two_nonneg (3 * y - 2),
end

repo: mathzoo


text:
import Lean
syntax (name := test) "test%" ident : command

open Lean.Elab
open Lean.Elab.Command

@[command_elab test] def elabTest : CommandElab := fun stx => do
  let id ← resolveGlobalConstNoOverloadWithInfo stx[1]
  liftTermElabM do
    IO.println (repr (← Lean.Meta.Match.getEquationsFor id))
  return ()

def f (x : List Nat) : Nat :=
  match x with
  | [] => 1
  | [a] => 2
  | _ => 3

test% f.match_1
#check @f.match_1
#check @f.match_1.splitter

theorem ex (x : List Nat) : f x > 0 := by
  simp [f]
  split <;> decide

test% Lean.RBNode.balance1.match_1
#check @Lean.RBNode.balance1.match_1.splitter

author: leanprover


text:
import algebra.ring

namespace my_ring

variables {R : Type*} [ring R]
variables a b c : R

#check zero_add
#check add_zero c
#check add_comm c a
#check add_assoc a
#check add_right_neg c
#check add_left_neg

-- BEGIN
theorem neg_eq_of_add_eq_zero {a b : R} (h : a + b = 0) : -a = b :=
begin
  rw ← add_zero b,
  rw ← add_right_neg a,
  rw ← add_assoc b,
  rw add_comm b a,
  rw h,
  rw zero_add,
end

theorem eq_neg_of_add_eq_zero {a b : R} (h : a + b = 0) : a = -b :=
begin
 rw ← add_zero a,
 rw ← add_right_neg b,
 rw ← add_assoc a,
 sorry,
end

theorem neg_zero : (-0 : R) = 0 :=
begin
  apply neg_eq_of_add_eq_zero,
  rw add_zero,
end

theorem neg_neg (a : R) : -(-a) = a :=
begin
  apply neg_eq_of_add_eq_zero,
  sorry,
end

-- END

#check @neg_eq_of_add_eq_zero
#check neg_zero
#check neg_neg

end my_ring

author: xhkittyyan


text:
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Simon Hudon, Scott Morrison
-/
import tactic.equiv_rw

/-!
## The `transport` tactic

`transport` attempts to move an `s : S α` expression across an equivalence `e : α ≃ β` to solve
a goal of the form `S β`, by building the new object field by field, taking each field of `s`
and rewriting it along `e` using the `equiv_rw` tactic.

We try to ensure good definitional properties, so that, for example, when we transport a `monoid α`
to a `monoid β`, the new multiplication is definitionally `λ x y, e (e.symm a * e.symm b)`.
-/

namespace tactic
open tactic.interactive

mk_simp_attribute transport_simps
"The simpset `transport_simps` is used by the tactic `transport`
to simplify certain expressions involving application of equivalences,
and trivial `eq.rec` or `ep.mpr` conversions.
It's probably best not to adjust it without understanding the algorithm used by `transport`."

attribute [transport_simps]
  eq_rec_constant
  eq_mp_eq_cast
  cast_eq
  equiv.to_fun_as_coe
  equiv.arrow_congr'_apply
  equiv.symm_apply_apply
  -- we use `apply_eq_iff_eq_symm_apply` rather than `apply_eq_iff_eq`,
  -- as many axioms have a constant on the right-hand-side
  equiv.apply_eq_iff_eq_symm_apply

/--
Given `s : S α` for some structure `S` depending on a type `α`,
and an equivalence `e : α ≃ β`,
try to produce an `S β`,
by transporting data and axioms across `e` using `equiv_rw`.
-/
-- At present we don't actually use `s`; it's inferred in the `mk_app` call.
@[nolint unused_arguments]
meta def transport (s e : expr) : tactic unit :=
do
  (_, α, β) ← infer_type e >>= relation_lhs_rhs <|>
    fail format!"second argument to `transport` was not an equivalence-type relation",
  -- We explode the goal into individual fields using `refine_struct`.
  -- Later we'll want to also consider falling back to `fconstructor`,
  -- but for now this suffices.
  seq' `[refine_struct { .. }]
  -- We now deal with each field sequentially.
  -- Since we may pass goals through to the user if the heuristics here fail,
  -- we wrap everything in `propagate_tags`.
  (propagate_tags (try (do
    -- Look up the name of the current field being processed
    f ← get_current_field,
    -- Note the value in the original structure.
    -- (This `mk_mapp` call with second argument inferred only works for typeclasses!)
    mk_mapp f [α, none] >>= note f none,
    -- We now run different algorithms,
    -- depending on whether we're transporting data or a proposition.
    b ← target >>= is_prop,
    -- In order to achieve good definitional properties,
    -- we use `simp_result` to intercept the synthesized term and simplify it,
    -- in particular simplifying along `eq_rec_constant`.
    if ¬ b then simp_result (do
      -- For data fields, simply rewrite them using `equiv_rw`.
      equiv_rw_hyp f e,
      get_local f >>= exact)
    else try (do
      -- The goal probably has messy expressions produced by `equiv_rw` acting on early data fields,
      -- so we clean up a little.
      try unfold_projs_target,
      `[simp only with transport_simps],
      -- If the field is an equation in `β`, try to use injectivity of the equivalence
      -- to turn it into an equation in `α`.
      -- (If the left hand side of the equation involved an operation we've already transported,
      -- this step has already been achieved by the `transport_simps`, so we `try` this step.)
      try $ under_binders $ to_expr ``((%%e).symm.injective) >>= apply,
      -- Finally, rewrite the original field value using the equivalence `e`, and try to close
      -- the goal using
      equiv_rw_hyp f e,
      get_local f >>= exact))))

namespace interactive
setup_tactic_parser

/--
Given a goal `⊢ S β` for some type class `S`, and an equivalence `e : α ≃ β`.
`transport using e` will look for a hypothesis `s : S α`,
and attempt to close the goal by transporting `s` across the equivalence `e`.

```lean
example {α : Type} [ring α] {β : Type} (e : α ≃ β) : ring β :=
by transport using e.
```

You can specify the object to transport using `transport s using e`.

`transport` works by attempting to copy each of the operations and axiom fields of `s`,
rewriting them using `equiv_rw e` and defining a new structure using these rewritten fields.

If it fails to fill in all the new fields, `transport` will produce new subgoals.
It's probably best to think about which missing `simp` lemmas would have allowed `transport`
to finish, rather than solving these goals by hand.
(This may require looking at the implementation of `tranport` to understand its algorithm;
there are several examples of "transport-by-hand" at the end of `test/equiv_rw.lean`,
which `transport` is an abstraction of.)
-/
meta def transport (s : parse texpr?) (e : parse $ (tk "using" *> texpr)) : itactic :=
do
  s ← match s with
  | some s := to_expr s
  | none := (do
      t ← target,
      let n := t.get_app_fn.const_name,
      ctx ← local_context,
      ctx.any_of (λ e, (do t ← infer_type e, guard (t.get_app_fn.const_name = n), return e))) <|>
        fail "`transport` could not find an appropriate source object. Try `transport s using e`."
  end,
  e ← to_expr e,
  tactic.transport s e

add_tactic_doc
{ name        := "transport",
  category    := doc_category.tactic,
  decl_names  := [`tactic.interactive.transport],
  tags        := ["rewriting", "equiv", "transport"] }

end interactive

end tactic

repo: mathlib


text:
import MyNat.Definition
import MyNat.Inequality -- le_iff_exists_add
import Mathlib.Tactic.Use -- use tactic
import AdditionWorld.Level4 -- add_comm
namespace MyNat
open MyNat
/-!

# Inequality world.

## Level 3: `le_succ_of_le`

We have seen how the `use` tactic makes progress on goals of the form `⊢ ∃ c, ...`.
But what do we do when we have a *hypothesis* of the form `h : ∃ c, ...`?
The hypothesis claims that there exists some natural number `c` with some
property. How are we going to get to that natural number `c`? It turns out
that the `cases` tactic can be used (just like it was used to extract
information from `∧` and `∨` and `↔` hypotheses). Let me talk you through
the proof of `a ≤ b ⟹ a ≤ succ b`.

The goal is an implication so we clearly want to start with

`intro h`

After this, if you *want*, you can do something like

`rw [le_iff_exists_add] at h ⊢ `

(get the sideways T with `\|-` or `\goal` then space). This `rw` changes the `≤` into
its `∃` form in `h` and the goal -- but if you are happy with just
*imagining* the `∃` whenever you read a `≤` then you don't need to do this line.

Our hypothesis `h` is now `∃ (c : MyNat), b = a + c` (or `a ≤ b` if you
elected not to do the definitional rewriting) so

`cases h with | _ c hc => ..`

gives you the natural number `c` and the hypothesis `hc : b = a + c`.
Now use `use` wisely and you're home.

## Lemma : le_succ
For all naturals `a`, `b`, if `a ≤ b` then `a ≤ succ b`.
-/
theorem le_succ (a b : MyNat) : a ≤ b → a ≤ (succ b) := by
  intro h
  cases h with
  | _ c hc => -- a = 0, b = 0
    rw [hc]
    use c + 1

/-!

You can use `succ c` or `c + 1` or `1 + c`. Those numbers are all
equal, right? Try these variations and see what happens.

Now what about if you do `use 1 + c`? Can you work out
what is going on? Does it help if I tell you that the *definition*
of `1` is `succ 0`?

Next up [Level 4](./Level4.lean.md)
-/


text:
/-
Copyright (c) 2018 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Johannes Hölzl
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.data.multiset.nodup
import Mathlib.PostPort

universes u_1 u_2

namespace Mathlib

/-!
# The cartesian product of multisets
-/

namespace multiset

/-- Given `δ : α → Type*`, `pi.empty δ` is the trivial dependent function out of the empty
multiset. -/
def pi.empty {α : Type u_1} (δ : α → Type u_2) (a : α) (H : a ∈ 0) : δ a :=
  sorry

/-- Given `δ : α → Type*`, a multiset `m` and a term `a`, as well as a term `b : δ a` and a
function `f` such that `f a' : δ a'` for all `a'` in `m`, `pi.cons m a b f` is a function `g` such
that `g a'' : δ a''` for all `a''` in `a ::ₘ m`. -/
def pi.cons {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} (m : multiset α) (a : α) (b : δ a) (f : (a : α) → a ∈ m → δ a) (a' : α) (H : a' ∈ a ::ₘ m) : δ a' :=
  dite (a' = a) (fun (h : a' = a) => Eq._oldrec b (Eq.symm h)) fun (h : ¬a' = a) => f a' sorry

theorem pi.cons_same {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} {m : multiset α} {a : α} {b : δ a} {f : (a : α) → a ∈ m → δ a} (h : a ∈ a ::ₘ m) : pi.cons m a b f a h = b :=
  dif_pos rfl

theorem pi.cons_ne {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} {m : multiset α} {a : α} {a' : α} {b : δ a} {f : (a : α) → a ∈ m → δ a} (h' : a' ∈ a ::ₘ m) (h : a' ≠ a) : pi.cons m a b f a' h' = f a' (or.resolve_left (iff.mp mem_cons h') h) :=
  dif_neg h

theorem pi.cons_swap {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} {a : α} {a' : α} {b : δ a} {b' : δ a'} {m : multiset α} {f : (a : α) → a ∈ m → δ a} (h : a ≠ a') : pi.cons (a' ::ₘ m) a b (pi.cons m a' b' f) == pi.cons (a ::ₘ m) a' b' (pi.cons m a b f) := sorry

/-- `pi m t` constructs the Cartesian product over `t` indexed by `m`. -/
def pi {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} (m : multiset α) (t : (a : α) → multiset (δ a)) : multiset ((a : α) → a ∈ m → δ a) :=
  multiset.rec_on m (singleton sorry)
    (fun (a : α) (m : multiset α) (p : multiset ((a : α) → a ∈ m → δ a)) => bind (t a) fun (b : δ a) => map sorry p) sorry

@[simp] theorem pi_zero {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} (t : (a : α) → multiset (δ a)) : pi 0 t = pi.empty δ ::ₘ 0 :=
  rfl

@[simp] theorem pi_cons {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} (m : multiset α) (t : (a : α) → multiset (δ a)) (a : α) : pi (a ::ₘ m) t = bind (t a) fun (b : δ a) => map (pi.cons m a b) (pi m t) :=
  rec_on_cons a m

theorem pi_cons_injective {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} {a : α} {b : δ a} {s : multiset α} (hs : ¬a ∈ s) : function.injective (pi.cons s a b) := sorry

theorem card_pi {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} (m : multiset α) (t : (a : α) → multiset (δ a)) : coe_fn card (pi m t) = prod (map (fun (a : α) => coe_fn card (t a)) m) := sorry

theorem nodup_pi {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} {s : multiset α} {t : (a : α) → multiset (δ a)} : nodup s → (∀ (a : α), a ∈ s → nodup (t a)) → nodup (pi s t) := sorry

theorem mem_pi {α : Type u_1} [DecidableEq α] {δ : α → Type u_2} (m : multiset α) (t : (a : α) → multiset (δ a)) (f : (a : α) → a ∈ m → δ a) : f ∈ pi m t ↔ ∀ (a : α) (h : a ∈ m), f a h ∈ t a := sorry


text:
import algebra.field
import tactic

-- ad-hoc definitions for quadratic and cubic polynomials

@[ext]
structure monic_quad_poly (K : Type*) [comm_ring K] :=
mk :: (a b : K)

namespace monic_quad_poly

def eval_at {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K) : K
:= x^2 + f.a*x + f.b

def eval_dx_at {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K) : K
:= 2*x + f.a

def is_root {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K)
:= f.eval_at x = 0

def is_multiple_root {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K)
:= f.eval_at x = 0 ∧ f.eval_dx_at x = 0

lemma vieta_key_b {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K)
(h : f.is_root x)
: f.b = x*(-f.a-x) :=
sub_eq_zero.1 begin
  unfold is_root at h,
  transitivity f.b - x*(-f.a-x) - f.eval_at x, {
    rw h, ring,
  },
  unfold eval_at,
  ring,
end

lemma vieta_key {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K)
(h : f.is_root x) (z : K)
: f.eval_at z = (z - x) * (z + f.a + x) :=
sub_eq_zero.1 begin
  unfold eval_at,
  rw vieta_key_b f x h,
  ring,
end

lemma vieta {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K)
(h : f.is_root x) : f.is_root (-f.a-x) :=
begin
  unfold is_root,
  rw vieta_key f x h,
  ring,
end

lemma vieta_iff {K : Type*} [integral_domain K] (f : monic_quad_poly K) (x : K)
(h : f.is_root x) (z : K)
: f.is_root z ↔ z = x ∨ z = -f.a-x :=
begin
  unfold is_root,
  rw vieta_key f x h z,
  split, {
    intro h1,
    simp at h1,
    cases h1 with h1 h1, {
      left, exact sub_eq_zero.1 h1,
    },
    right,
    transitivity z - (z + f.a + x), {
      rw h1, ring,
    },
    rw ← sub_eq_zero, ring,
  },
  intro h1,
  cases h1 with h1 h1,
  { rw h1, ring, },
  rw h1, ring,
end

lemma vieta_2_iff {K : Type*} [integral_domain K] (f : monic_quad_poly K) (x : K)
(h : f.is_multiple_root x) (z : K)
: f.is_root z ↔ z = x :=
begin
  unfold is_multiple_root at h,
  cases h with h1 h2,
  replace h2 : x = -f.a-x := by {
    transitivity x - f.eval_dx_at x, {
      rw h2, ring,
    },
    unfold eval_dx_at,
    ring,
  },
  have key := vieta_iff f x h1 z,
  rw [← h2, or_self] at key,
  exact key,
end

def has_multiple_root {K : Type*} [comm_ring K] (f : monic_quad_poly K)
:= ∃ x : K, f.is_multiple_root x

def disc {K : Type*} [comm_ring K] (f : monic_quad_poly K) : K
:= f.a^2 - 4*f.b

lemma disc_scale {K : Type*} [comm_ring K] (f : monic_quad_poly K) (d : K)
: disc ⟨ f.a*d, f.b*d^2 ⟩ = disc f * d^2 :=
begin
  simp only [disc],
  ring,
end

lemma disc' {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K)
: f.disc = (f.eval_dx_at x) ^ 2 - 4 * f.eval_at x :=
begin
  simp only [eval_at, eval_dx_at, disc],
  ring,
end

lemma disc_eq_prod_of_roots {K : Type*} [comm_ring K] (f : monic_quad_poly K) (x : K)
(h : f.is_root x)
: f.disc = (f.a + 2*x)^2 :=
sub_eq_zero.1 begin
  unfold disc,
  rw [vieta_key_b f x h],
  ring,
end

lemma has_multiple_root_implies_disc_zero
{K : Type*} [comm_ring K] (f : monic_quad_poly K):
f.has_multiple_root → f.disc = 0 :=
begin
  simp only [has_multiple_root, is_multiple_root],
  rintro ⟨ x, h1, h2 ⟩,
  rw [disc' f x, h1, h2],
  ring,
end

lemma is_multiple_root'
{K : Type*} [comm_ring K] (f : monic_quad_poly K)
(x : K) (h : f.is_root x)
: x = -f.a-x ↔ f.is_multiple_root x :=
begin
  unfold is_root at h,
  unfold is_multiple_root,
  transitivity f.eval_dx_at x = 0, {
    split, {
      intro h1,
      unfold eval_dx_at,
      transitivity x - (-f.a-x),
      { rw ← sub_eq_zero, ring, },
      rw ← h1, ring,
    },
    intro h1,
    transitivity x - f.eval_dx_at x,
    { rw h1, ring, },
    unfold eval_dx_at, ring,
  },
  simp [h],
end

lemma has_multiple_root_iff_disc_zero'
{K : Type*} [integral_domain K] (f : monic_quad_poly K)
(x : K) (h : f.is_root x)
: x = -f.a-x ↔ f.disc = 0 :=
begin
  unfold is_root at h,
  rw is_multiple_root' f x h,
  split, {
    intro h1,
    exact f.has_multiple_root_implies_disc_zero ⟨ x, h1 ⟩,
  },
  intro h1,
  rw [disc' f x, h] at h1,
  simp at h1,
  exact ⟨ h, h1 ⟩,
end

end monic_quad_poly

@[ext]
structure monic_cubic_poly (K : Type*) [comm_ring K] :=
mk :: (a b c : K)

namespace monic_cubic_poly

def eval_at {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x : K) : K
:= x^3 + f.a*x^2 + f.b*x + f.c

def eval_dx_at {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x : K) : K
:= 3*x^2 + 2*f.a*x + f.b

def is_root {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x : K)
:= f.eval_at x = 0

def is_multiple_root {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x : K)
:= f.eval_at x = 0 ∧ f.eval_dx_at x = 0

lemma eval_at_sub {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x y : K)
: f.eval_at x - f.eval_at y = (x^2+x*y+y^2 + f.a*(x+y) + f.b) * (x - y) :=
begin
  unfold eval_at,
  ring,
end

lemma eval_at_sub_2 {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x y : K)
: y * f.eval_at x - x * f.eval_at y = (x*y*(f.a+x+y) - f.c) * (x - y) :=
begin
  unfold eval_at,
  ring,
end

lemma vieta_key_b {K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
: f.b = -x^2-x*y-y^2 - f.a*(x+y) :=
begin
  unfold is_root at hx hy,
  have key := eval_at_sub f x y,
  simp [hx, hy, sub_ne_zero.2 hneq] at key,
  transitivity f.b - (x^2+x*y+y^2 + f.a*(x+y) + f.b),
  { rw key, ring, },
  rw ← sub_eq_zero, ring,
end

lemma vieta_key_c {K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
: f.c = x*y*(f.a+x+y) :=
begin
  unfold is_root at hx hy,
  have key := eval_at_sub_2 f x y,
  simp [hx, hy, sub_ne_zero.2 hneq] at key,
  exact (sub_eq_zero.1 key).symm,
end

lemma vieta_key {K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
(z : K)
: f.eval_at z = (z - x) * (z - y) * (z + f.a + x + y) :=
begin
  unfold eval_at,
  rw [vieta_key_b f x y hx hy hneq, vieta_key_c f x y hx hy hneq],
  ring,
end

lemma vieta {K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
: f.is_root (-f.a-x-y) :=
begin
  unfold is_root,
  rw vieta_key f x y hx hy hneq,
  ring,
end

lemma vieta_2_key {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x : K)
(h : f.is_multiple_root x) (z : K)
: f.eval_at z = (z - x)^2 * (z + f.a + 2*x) :=
sub_eq_zero.1 begin
  transitivity f.eval_at x + f.eval_dx_at x * (z-x), {
    rw ← sub_eq_zero, unfold eval_at eval_dx_at, ring,
  },
  rw [h.1, h.2],
  ring,
end

lemma vieta_2 {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x : K)
(h : f.is_multiple_root x)
: f.is_root (-f.a-2*x) :=
begin
  unfold is_root,
  rw vieta_2_key f x h,
  ring,
end

lemma vieta_iff {K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
(z : K)
: f.is_root z ↔ z = x ∨ z = y ∨ z = -f.a-x-y :=
begin
  unfold is_root,
  rw vieta_key f x y hx hy hneq,
  split, {
    intro h1,
    simp at h1,
    rcases h1 with ⟨ h1 | h1 ⟩ | h1, {
      left, exact sub_eq_zero.1 h1,
    }, {
      right, left, exact sub_eq_zero.1 h1,
    },
    right, right,
    transitivity z - (z + f.a + x + y), {
      rw h1, ring,
    },
    rw ← sub_eq_zero, ring,
  },
  intro h1,
  rcases h1 with h1 | h1 | h1,
  { rw h1, ring, },
  { rw h1, ring, },
  rw h1, ring,
end

lemma vieta_2_iff {K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x : K)
(h : f.is_multiple_root x)
(z : K)
: f.is_root z ↔ z = x ∨ z = -f.a-2*x :=
begin
  unfold is_root,
  rw vieta_2_key f x h,
  split, {
    intro h1,
    simp at h1,
    cases h1 with h1 h1, {
      left, exact sub_eq_zero.1 h1,
    },
    right,
    transitivity z - (z + f.a + 2*x), {
      rw h1, ring,
    },
    rw ← sub_eq_zero, ring,
  },
  intro h1,
  cases h1 with h1 h1,
  { rw h1, ring, },
  rw h1, ring,
end

def has_multiple_root {K : Type*} [comm_ring K] (f : monic_cubic_poly K)
:= ∃ x : K, f.is_multiple_root x

def disc {K : Type*} [comm_ring K] (f : monic_cubic_poly K) : K
:= -4*f.a^3*f.c + f.a^2*f.b^2 - 4*f.b^3 - 27*f.c^2 + 18*f.a*f.b*f.c

lemma disc_scale {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (d : K)
: disc ⟨ f.a*d, f.b*d^2, f.c*d^3 ⟩ = disc f * d^6 :=
begin
  simp only [disc],
  ring,
end

lemma disc' {K : Type*} [comm_ring K] (f : monic_cubic_poly K) (x : K)
: f.disc = f.eval_at x * (-3*(2*f.a^2 - 6*f.b)*x + (-4*f.a^3 + 15*f.a*f.b - 27*f.c))
+ f.eval_dx_at x * ((2*f.a^2 - 6*f.b)*x^2 + (2*f.a^3 - 7*f.a*f.b + 9*f.c)*x + (f.a^2*f.b - 4*f.b^2 + 3*f.a*f.c)) :=
begin
  simp only [eval_at, eval_dx_at, disc],
  ring,
end

lemma disc_eq_prod_of_roots {K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
: f.disc = (x - y)^2 * (f.a + 2*x + y)^2 * (f.a + x + 2*y)^2 :=
sub_eq_zero.1 begin
  unfold disc,
  rw [vieta_key_b f x y hx hy hneq, vieta_key_c f x y hx hy hneq],
  ring,
end

lemma has_multiple_root_implies_disc_zero
{K : Type*} [comm_ring K] (f : monic_cubic_poly K):
f.has_multiple_root → f.disc = 0 :=
begin
  simp only [has_multiple_root, is_multiple_root],
  rintro ⟨ x, h1, h2 ⟩,
  rw [disc' f x, h1, h2],
  ring,
end

lemma eval_dx_at'
{K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
: f.eval_dx_at x = (f.a + 2*x + y) * (x - y) :=
begin
  unfold eval_dx_at,
  rw [vieta_key_b f x y hx hy hneq],
  ring,
end

lemma is_multiple_root'
{K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
: x = -f.a-x-y ↔ f.is_multiple_root x :=
begin
  transitivity y = -f.a-2*x, {
    split, {
      intro h,
      transitivity y - f.a - x - y - (-f.a-x-y),
      { rw ← sub_eq_zero, ring, },
      rw ← h, ring,
    },
    intro h,
    rw h,
    ring,
  },
  transitivity f.eval_dx_at x = 0, {
    rw eval_dx_at' f x y hx hy hneq,
    split, {
      intro h,
      rw h,
      ring,
    },
    intro h,
    simp [sub_ne_zero.2 hneq] at h,
    transitivity y - (f.a + 2*x + y),
    { rw h, ring, },
    rw ← sub_eq_zero, ring,
  },
  unfold is_root at hx,
  unfold is_multiple_root,
  simp [hx],
end

lemma has_multiple_root_iff_disc_zero'
{K : Type*} [integral_domain K] (f : monic_cubic_poly K) (x y : K)
(hx : f.is_root x)
(hy : f.is_root y)
(hneq : x ≠ y)
: x = -f.a-x-y ∨ y = -f.a-x-y ↔ f.disc = 0 :=
begin
  split, {
    intro h1,
    cases h1 with h1 h1, {
      rw is_multiple_root' f x y hx hy hneq at h1,
      exact has_multiple_root_implies_disc_zero f ⟨ x, h1 ⟩,
    },
    replace h1 := calc y = -f.a-x-y : h1
    ... = -f.a-y-x : by ring,
    rw is_multiple_root' f y x hy hx hneq.symm at h1,
    exact has_multiple_root_implies_disc_zero f ⟨ y, h1 ⟩,
  },
  intro h1,
  rw disc_eq_prod_of_roots f x y hx hy hneq at h1,
  simp [sub_ne_zero.2 hneq] at h1,
  cases h1 with h1 h1, {
    left,
    transitivity x - (f.a + 2*x + y),
    { rw h1, ring, },
    rw ← sub_eq_zero, ring,
  },
  right,
  transitivity y - (f.a + x + 2*y),
  { rw h1, ring, },
  rw ← sub_eq_zero, ring,
end

end monic_cubic_poly

author: acmepjz

repo: my-lean-test

save_path: github-repos/lean/acmepjz-my-lean-test