Theory pAdic_Product

(*  Title:       Computational p-Adics: Product of All p-Adic Fields
    Author:      Jeremy Sylvestre <jeremy.sylvestre at ualberta.ca>, 2025
    Maintainer:  Jeremy Sylvestre <jeremy.sylvestre at ualberta.ca>
*)


theory pAdic_Product

imports
  FLS_Prime_Equiv_Depth
  "HOL-Computational_Algebra.Fraction_Field"
  "HOL-Analysis.Elementary_Metric_Spaces"

begin


section ‹p-Adic fields as equivalence classes of sequences of formal Laurent series›


subsection ‹Preliminaries›

lemma inj_on_vimage_image_eq:
  "(f -` (f ` B)) ∩ A = B" if "inj_on f A" and "B ⊆ A"
  using that unfolding inj_on_def by fast


subsection ‹The type definition as a quotient›

quotient_type (overloaded) 'a p_adic_prod
  = "'a::nontrivial_factorial_idom fls_pseq" / globally_p_equal
  by (simp, rule p_equality_depth_fls_pseq.globally_p_equal_equivp)

lemmas  rep_p_adic_prod_inverse              = Quotient3_abs_rep[OF Quotient3_p_adic_prod]
  and   p_adic_prod_lift_globally_p_equal    = Quotient3_rel_abs[OF Quotient3_p_adic_prod]
  and   globally_p_equal_fls_pseq_equals_rsp = equals_rsp[OF Quotient3_p_adic_prod]
  and   p_adic_prod_eq_iff
    = Quotient3_rel_rep[OF Quotient3_p_adic_prod, symmetric]
  and   globally_p_equal_fls_pseq_rep_p_adic_prod_refl
    = Quotient3_rep_reflp[OF Quotient3_p_adic_prod]
  and globally_p_equal_fls_pseq_rep_abs_p_adic_prod
    = rep_abs_rsp[OF Quotient3_p_adic_prod] rep_abs_rsp_left[OF Quotient3_p_adic_prod]

lemma p_adic_prod_globally_p_equal_self:
  "(rep_p_adic_prod (abs_p_adic_prod r)) ≃∀p r"
  using Quotient3_rep_abs[OF Quotient3_p_adic_prod]
        p_equality_depth_fls_pseq.globally_p_equal_refl
  by    auto

lemma rep_p_adic_prod_p_equal_self: "rep_p_adic_prod (abs_p_adic_prod r) ≃⇩p r"
  for p :: "'a::nontrivial_factorial_idom prime" and r :: "'a fls_pseq"
  using p_adic_prod_globally_p_equal_self p_equality_depth_fls_pseq.globally_p_equalD by auto

lemma rep_p_adic_prod_set_inverse: "abs_p_adic_prod ` (rep_p_adic_prod ` A) = A"
proof
  show "abs_p_adic_prod ` rep_p_adic_prod ` A ⊆ A"
  proof
    fix x assume "x ∈ abs_p_adic_prod ` rep_p_adic_prod ` A"
    from this obtain a where "a ∈ A" "x = abs_p_adic_prod (rep_p_adic_prod a)" by fast
    thus "x ∈ A" using rep_p_adic_prod_inverse by metis
  qed
  show "A ⊆ abs_p_adic_prod ` rep_p_adic_prod ` A"
  proof
    fix a assume "a ∈ A"
    thus "a ∈ abs_p_adic_prod ` rep_p_adic_prod ` A"
      using rep_p_adic_prod_inverse[of a] by force
  qed
qed

lemma p_adic_prod_cases [case_names abs_p_adic_prod, cases type: p_adic_prod]:
  C if "⋀X. x = abs_p_adic_prod X ⟹ C"
  by (metis that rep_p_adic_prod_inverse)

lemmas  two_p_adic_prod_cases   = p_adic_prod_cases[case_product p_adic_prod_cases]
  and   three_p_adic_prod_cases =
    p_adic_prod_cases[case_product p_adic_prod_cases[case_product p_adic_prod_cases]]

lemma p_adic_prod_reduced_cases [case_names abs_p_adic_prod]:
  fixes x :: "'a::nontrivial_euclidean_ring_cancel p_adic_prod"
  obtains X where "x = abs_p_adic_prod X" and "∀p. (X p) pmod p = X p"
proof (cases x)
  case (abs_p_adic_prod X)
  define Y where "Y ≡ (λp. (X p) pmod p)"
  with abs_p_adic_prod have "x = abs_p_adic_prod Y"
    using fls_pseq_globally_reduced p_adic_prod_lift_globally_p_equal by blast
  moreover from Y_def have "∀p. (Y p) pmod p = Y p" by fastforce
  ultimately show ?thesis using that by blast
qed

lemma p_adic_prod_unique_rep:
  "∃!X. x = abs_p_adic_prod X ∧ (∀p. (X p) pmod p = X p)"
  for x :: "'a::nontrivial_euclidean_ring_cancel p_adic_prod"
proof (intro ex_ex1I, safe)
  obtain X where "x = abs_p_adic_prod X ∧ (∀p. (X p) pmod p = X p)"
    using p_adic_prod_reduced_cases by meson
  thus "∃X. x = abs_p_adic_prod X ∧ (∀p. X p pmod p = X p)" by fast
next
  fix X X' :: "'a fls_pseq"
  assume  "∀p. X  p pmod p = X  p"
    and   "∀p. X' p pmod p = X' p"
    and   "abs_p_adic_prod X = abs_p_adic_prod X'"
  thus "X = X'" using p_adic_prod.abs_eq_iff[of X X'] fls_pmod_cong by fastforce
qed

abbreviation
  "reduced_rep_p_adic_prod x ≡
    (THE X. x = abs_p_adic_prod X ∧ (∀p. (X p) pmod p = X p))"

lemma reduced_rep_p_adic_prod_is_rep:
  "x = abs_p_adic_prod (reduced_rep_p_adic_prod x)"
  for x :: "'a::nontrivial_euclidean_ring_cancel p_adic_prod"
  using theI'[OF p_adic_prod_unique_rep] by fast

lemma reduced_rep_p_adic_prod_is_reduced:
  "(reduced_rep_p_adic_prod x p) pmod p = reduced_rep_p_adic_prod x p"
  for p :: "'a::nontrivial_euclidean_ring_cancel prime" and X :: "'a p_adic_prod"
  using theI'[OF p_adic_prod_unique_rep] by fast

lemma abs_p_adic_prod_inverse:
  "reduced_rep_p_adic_prod (abs_p_adic_prod X) = X" if "∀p. (X p) pmod p = X p"
  for X :: "'a::nontrivial_euclidean_ring_cancel fls_pseq"
  by (intro the1_equality p_adic_prod_unique_rep, simp add: that)

lemma p_adic_prod_seq_cases [case_names abs_p_adic_prod]:
  C if "⋀F. X = (λn. abs_p_adic_prod (F n)) ⟹ C"
proof-
  define F where "F ≡ λn. rep_p_adic_prod (X n)"
  hence "X = (λn. abs_p_adic_prod (F n))"
    using rep_p_adic_prod_inverse by metis
  with that show C by auto
qed

lemma p_adic_prod_seq_reduced_cases [case_names abs_p_adic_prod]:
  fixes X :: "nat ⇒ 'a::nontrivial_euclidean_ring_cancel p_adic_prod"
  obtains F
    where "X = (λn. abs_p_adic_prod (F n))"
    and   "∀(n::nat) (p::'a prime). (F n p) pmod p = F n p"
proof-
  define F where "F ≡ λn. reduced_rep_p_adic_prod (X n)"
  from F_def have "X = (λn. abs_p_adic_prod (F n))"
    using reduced_rep_p_adic_prod_is_rep by blast
  moreover from F_def have "∀(n::nat) (p::'a prime). (F n p) pmod p = F n p"
    using reduced_rep_p_adic_prod_is_reduced by blast
  ultimately show thesis using that by simp
qed


subsection ‹Algebraic instantiations›

text ‹The product of p-adic fields form a ring.›

instantiation p_adic_prod :: (nontrivial_factorial_idom) comm_ring_1
begin

lift_definition zero_p_adic_prod :: "'a p_adic_prod" is "0::'a fls_pseq" .

lift_definition one_p_adic_prod :: "'a p_adic_prod" is "1::'a fls_pseq" .

lift_definition plus_p_adic_prod ::
  "'a p_adic_prod ⇒ 'a p_adic_prod ⇒ 'a p_adic_prod"
  is "λX Y. X + Y"
  using p_equality_depth_fls_pseq.globally_p_equal_add by force

lift_definition uminus_p_adic_prod :: "'a p_adic_prod ⇒ 'a p_adic_prod"
  is "λX. - X"
using p_equality_depth_fls_pseq.globally_p_equal_uminus by auto

lift_definition minus_p_adic_prod ::
  "'a p_adic_prod ⇒ 'a p_adic_prod ⇒ 'a p_adic_prod"
  is "λX Y. X - Y"
  using p_equality_depth_fls_pseq.globally_p_equal_minus by force

lift_definition times_p_adic_prod ::
  "'a p_adic_prod ⇒ 'a p_adic_prod ⇒ 'a p_adic_prod"
  is "λX Y. X * Y"
  using p_equality_depth_fls_pseq.globally_p_equal_mult by fastforce

instance
proof
  fix a b c :: "'a p_adic_prod"
  show "a + b + c = a + (b + c)" by transfer (simp add: add.assoc)
  show "a + b = b + a" by transfer (simp add: add.commute)
  show "1 * a = a" by transfer simp
  show "0 + a = a" by transfer simp
  show "- a + a = 0" by transfer simp
  show "a - b = a + - b" by transfer simp
  show "a * b * c = a * (b * c)" by transfer (simp add: mult.assoc)
  show "(a + b) * c = a * c + b * c" by transfer (simp add: distrib_right)
  show "a * b = b * a" by transfer (simp add: mult.commute)
  have "¬ (0::'a fls_pseq) ≃∀p (1::'a fls_pseq)"
    using p_equality_depth_fls_pseq.globally_p_equalD p_equal_fls_sym fls_1_not_p_equal_0
    by    fastforce
  thus "(0::'a p_adic_prod) ≠ (1::'a p_adic_prod)" by transfer simp
qed

end (* instantiation p_adic_prod :: comm_ring_1 *)

lemma pow_p_adic_prod_abs_eq:
  "(abs_p_adic_prod X) ^ n = abs_p_adic_prod (X ^ n)"
  for X :: "'a::nontrivial_factorial_idom fls_pseq"
proof (induct n)
  case 0
  have "(abs_p_adic_prod X) ^ 0 = (1 :: 'a p_adic_prod)" by auto
  moreover have "abs_p_adic_prod (X ^ 0) = (1 :: 'a p_adic_prod)"
    using one_p_adic_prod.abs_eq by simp
  ultimately show ?case by presburger
next
  case (Suc n) thus "(abs_p_adic_prod X) ^ Suc n = abs_p_adic_prod (X ^ Suc n)"
    using times_p_adic_prod.abs_eq by auto
qed

text ‹We can create inverses at the nonzero places.›

instantiation p_adic_prod ::
  (nontrivial_factorial_unique_euclidean_bezout) "{divide_trivial, inverse}"
begin

lift_definition divide_p_adic_prod ::
  "'a p_adic_prod ⇒ 'a p_adic_prod ⇒ 'a p_adic_prod"
  is "λX Y. X * (Y¯∀p)"
proof-
  fix X X' Y Y' :: "'a fls_pseq"
  assume "X ≃∀p X'" and "Y ≃∀p Y'"
  thus
    "X * (Y¯∀p) ≃∀p
      X' * (Y'¯∀p)"
    using globally_pinverse_cong[of Y Y'] p_equality_depth_fls_pseq.globally_p_equal_mult[of X X']
    by    fastforce
qed

lift_definition inverse_p_adic_prod :: "'a p_adic_prod ⇒ 'a p_adic_prod"
  is global_pinverse_fls_pseq
  by (rule globally_pinverse_cong)

instance
proof
  show "⋀a::'a p_adic_prod. a div 0 = 0" by transfer (simp flip: zero_fun_def)
  show "⋀a::'a p_adic_prod. a div 1 = a" by transfer (simp flip: one_fun_def)
  show "⋀a::'a p_adic_prod. 0 div a = 0" by transfer (simp flip: zero_fun_def)
qed

end


subsection ‹Equivalence and depth relative to a prime›

overloading
  p_equal_p_adic_prod ≡
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒ 'a p_adic_prod ⇒
      'a p_adic_prod ⇒ bool"
  p_restrict_p_adic_prod ≡
    "p_restrict :: 'a p_adic_prod ⇒
      ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
  p_depth_p_adic_prod ≡ "p_depth :: 'a prime ⇒ 'a p_adic_prod ⇒ int"
  global_unfrmzr_pows_p_adic_prod ≡
    "global_unfrmzr_pows :: ('a prime ⇒ int) ⇒ 'a p_adic_prod"
begin

lift_definition p_equal_p_adic_prod ::
  "'a::nontrivial_factorial_idom prime ⇒
    'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
  is p_equal
  by (
    simp only: globally_p_equal_fls_pseq_def,
    rule p_equality_depth_fls_pseq.globally_p_equal_transfer_equals_rsp, simp_all
  )

lift_definition p_restrict_p_adic_prod ::
  "'a::nontrivial_factorial_idom p_adic_prod ⇒
    ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
  is "λX P p. if P p then X p else 0"
  using p_equality_depth_fls_pseq.globally_p_equalD by fastforce

lift_definition p_depth_p_adic_prod ::
  "'a::nontrivial_factorial_idom prime ⇒ 'a p_adic_prod ⇒ int"
  is p_depth
  by (
    simp only: globally_p_equal_fls_pseq_def,
    rule p_equality_depth_fls_pseq.globally_p_equal_p_depth
  )

lift_definition global_unfrmzr_pows_p_adic_prod ::
  "('a::nontrivial_factorial_idom prime ⇒ int) ⇒ 'a p_adic_prod"
  is global_unfrmzr_pows .

end  (* overloading *)

lemma p_equal_p_adic_prod_abs_eq0: "(abs_p_adic_prod X ≃⇩p 0) = (X ≃⇩p 0)"
  for   p :: "'a::nontrivial_factorial_idom prime" and X :: "'a fls_pseq"
  using p_equal_p_adic_prod.abs_eq[of p X "0::'a fls_pseq"]
  by    (simp add: zero_p_adic_prod.abs_eq)

lemma p_equal_p_adic_prod_abs_eq1: "(abs_p_adic_prod X ≃⇩p 1) = (X ≃⇩p 1)"
  for   p :: "'a::nontrivial_factorial_idom prime" and X :: "'a fls_pseq"
  using p_equal_p_adic_prod.abs_eq[of p X "1::'a fls_pseq"]
  by    (simp add: one_p_adic_prod.abs_eq)

global_interpretation p_equality_p_adic_prod:
  p_equality_no_zero_divisors_1
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
proof

  fix p :: "'a prime"

  define E :: "'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    where "E ≡ p_equal p"

  show "equivp E"
    unfolding E_def p_equal_p_adic_prod_def
  proof-
    define  F :: "'a fls_pseq ⇒ 'a fls_pseq ⇒ bool"
      and   G :: "'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
      where "F ≡ p_equal p"
      and
        "G ≡
          map_fun id (map_fun rep_p_adic_prod (map_fun rep_p_adic_prod id)) p_equal p"
    hence "G = (λx y. F (rep_p_adic_prod x) (rep_p_adic_prod y))" by force
    with F_def show "equivp G" using equivp_transfer p_equality_depth_fls_pseq.equivp by fast
  qed

  show  "∃x::'a p_adic_prod. x ¬≃⇩p 0"
    by (transfer, rule p_equality_depth_fls_pseq.nontrivial)

  fix x y :: "'a p_adic_prod"
  show  "(x ≃⇩p y) = (x - y ≃⇩p 0)"
  and   "y ≃⇩p 0 ⟹ x * y ≃⇩p 0"
    by (
      transfer, rule p_equality_depth_fls_pseq.conv_0,
      transfer, rule p_equality_depth_fls_pseq.mult_0_right
    )

  assume "x ¬≃⇩p 0" and "y ¬≃⇩p 0"
  thus "x * y ¬≃⇩p 0"
    using p_depth_fls.no_zero_divisors[of p]
    by    (cases x, cases y)
          (auto simp add: p_equal_p_adic_prod_abs_eq0 times_p_adic_prod.abs_eq)

qed

overloading
  globally_p_equal_p_adic_prod ≡
    "globally_p_equal ::
      'a::nontrivial_factorial_idom p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
begin

definition globally_p_equal_p_adic_prod ::
  "'a::nontrivial_factorial_idom p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
  where globally_p_equal_p_adic_prod_def[simp]:
    "globally_p_equal_p_adic_prod = p_equality_p_adic_prod.globally_p_equal"

end  (* overloading *)

global_interpretation global_p_depth_p_adic_prod:
  global_p_equal_depth_no_zero_divisors_w_inj_index_consts
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    "p_restrict ::
      'a p_adic_prod ⇒ ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
    "p_depth :: 'a prime ⇒ 'a p_adic_prod ⇒ int"
    "λf. abs_p_adic_prod (λp. fls_const (f p))"
    Rep_prime
proof (unfold_locales, fold globally_p_equal_p_adic_prod_def)

  fix p :: "'a prime"

  fix x y :: "'a p_adic_prod"

  show "x ≃∀p y ⟹ x = y" by (simp, transfer, simp)

  fix P :: "'a prime ⇒ bool"
  show "P p ⟹ x prestrict P ≃⇩p x" by transfer simp
  show "¬ P p ⟹ x prestrict P ≃⇩p 0" by transfer simp

  show "((0::'a p_adic_prod)°⇧p) = 0" by transfer simp
  show "x ≃⇩p y ⟹ (x°⇧p) = (y°⇧p)"
    by (transfer, rule p_equality_depth_fls_pseq.depth_equiv, simp)
  show   "(- x°⇧p) = (x°⇧p)"
    by (transfer, rule p_equality_depth_fls_pseq.depth_uminus)
  show
    "x ¬≃⇩p 0 ⟹ (x°⇧p) < (y°⇧p)
      ⟹ (x + y°⇧p) = (x°⇧p)"
    by (transfer, rule p_equality_depth_fls_pseq.depth_pre_nonarch(1), simp, simp)
  show
    "⟦
      x ¬≃⇩p 0; x + y ¬≃⇩p 0;
      (x°⇧p) = (y°⇧p)
    ⟧ ⟹ (x°⇧p) ≤ ((x + y)°⇧p)"
    using p_equality_depth_fls_pseq.depth_pre_nonarch(2)[of p] by (transfer, simp add: mult.commute)
  show
    "x * y ¬≃⇩p 0 ⟹
      (x * y°⇧p) = (x°⇧p) + (y°⇧p)"
    by (transfer, rule p_equality_depth_fls_pseq.depth_mult_additive, simp)

  define F :: "('a prime ⇒ 'a) ⇒ 'a p_adic_prod"
    where "F ≡ λf. abs_p_adic_prod (λp. fls_const (f p))"

  show "F 1 = 1" by (simp add: F_def one_p_adic_prod.abs_eq flip: one_fun_def)

  fix f g :: "'a prime ⇒ 'a"
  show  "F (f - g) = F f - F g"
    and "F (f * g) = F f * F g"
    and "(F f ≃⇩p 0) = (f p = 0)"
    and "((F f)°⇧p) = int (pmultiplicity p (f p))"
    by  (simp_all
      add:  F_def fls_minus_const fun_diff_def minus_p_adic_prod.abs_eq times_p_adic_prod.abs_eq
            times_fun_def p_equal_p_adic_prod_abs_eq0 p_equal_fls_const_0_iff p_depth_const_def
            p_depth_p_adic_prod.abs_eq
      flip: p_depth_const
    )

qed (
  metis Rep_prime_inject injI, rule Rep_prime_n0, rule Rep_prime_not_unit,
  rule multiplicity_distinct_primes
)

lemma p_depth_p_adic_prod_diff_abs_eq:
  "((abs_p_adic_prod X - abs_p_adic_prod Y)°⇧p) = ((X - Y)°⇧p)"
  for p :: "'a::nontrivial_factorial_idom prime" and X Y :: "'a fls_pseq"
  using minus_p_adic_prod.abs_eq p_depth_p_adic_prod.abs_eq by metis

lemma p_depth_p_adic_prod_diff_abs_eq':
  "((abs_p_adic_prod X - abs_p_adic_prod Y)°⇧p) = ((X p - Y p)°⇧p)"
  for p :: "'a::nontrivial_factorial_idom prime" and X Y :: "'a fls_pseq"
  using p_depth_p_adic_prod_diff_abs_eq by auto

overloading
  p_depth_set_p_adic_prod ≡
    "p_depth_set ::
      'a::nontrivial_factorial_idom prime ⇒ int ⇒ 'a p_adic_prod set"
  global_depth_set_p_adic_prod ≡
    "global_depth_set :: int ⇒ 'a p_adic_prod set"
begin

definition p_depth_set_p_adic_prod ::
  "'a::nontrivial_factorial_idom prime ⇒ int ⇒ 'a p_adic_prod set"
  where p_depth_set_p_adic_prod_def[simp]:
    "p_depth_set_p_adic_prod = global_p_depth_p_adic_prod.p_depth_set"

definition global_depth_set_p_adic_prod ::
  "int ⇒ 'a::nontrivial_factorial_idom p_adic_prod set"
  where global_depth_set_p_adic_prod_def[simp]:
    "global_depth_set_p_adic_prod = global_p_depth_p_adic_prod.global_depth_set"

end

lemma p_depth_set_p_adic_prod_eq_projection:
  "((𝒫@⇩p⇧n) :: 'a p_adic_prod set) =
    abs_p_adic_prod ` (𝒫@⇩p⇧n)"
  for p :: "'a::nontrivial_factorial_idom prime"
proof safe
  fix x :: "'a p_adic_prod"
  assume x: "x ∈ 𝒫@⇩p⇧n"
  show "x ∈ abs_p_adic_prod ` 𝒫@⇩p⇧n"
  proof (cases x)
    case (abs_p_adic_prod X)
    with x have "X ∈ 𝒫@⇩p⇧n"
      using p_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.p_depth_setD
            p_equal_p_adic_prod_abs_eq0 p_depth_p_adic_prod.abs_eq
            p_equality_depth_fls_pseq.p_depth_setI p_depth_set_fls_pseq_def
      by    metis
    with abs_p_adic_prod show "x ∈ abs_p_adic_prod ` 𝒫@⇩p⇧n" by fast
  qed
qed (
  metis p_equality_depth_fls_pseq.p_depth_setD p_depth_set_fls_pseq_def p_equal_p_adic_prod_abs_eq0
        p_depth_p_adic_prod.abs_eq p_depth_set_p_adic_prod_def
        global_p_depth_p_adic_prod.p_depth_setI
)

lemma global_depth_set_p_adic_prod_eq_projection:
  "((𝒫∀p⇧n) :: 'a p_adic_prod set) =
    abs_p_adic_prod ` (𝒫∀p⇧n)"
  for p :: "'a::nontrivial_factorial_idom prime"
proof safe
  fix x :: "'a p_adic_prod"
  assume x: "x ∈ 𝒫∀p⇧n"
  show "x ∈ abs_p_adic_prod ` 𝒫∀p⇧n"
  proof (cases x)
    case (abs_p_adic_prod X)
    with x have "X ∈ 𝒫∀p⇧n"
      using global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.global_depth_setD
            p_equal_p_adic_prod_abs_eq0 p_depth_p_adic_prod.abs_eq
            p_equality_depth_fls_pseq.global_depth_setI global_depth_set_fls_pseq_def
      by    metis
    with abs_p_adic_prod show "x ∈ abs_p_adic_prod ` 𝒫∀p⇧n"
      by fast
  qed
qed (
  metis p_equality_depth_fls_pseq.global_depth_setD global_depth_set_fls_pseq_def
        p_equal_p_adic_prod_abs_eq0 p_depth_p_adic_prod.abs_eq global_depth_set_p_adic_prod_def
        global_p_depth_p_adic_prod.global_depth_setI
)

context
  fixes x :: "'a::nontrivial_factorial_idom p_adic_prod"
begin

lemma p_adic_prod_p_restrict_depth:
  "(x prestrict P)°⇧p = (if P p then x°⇧p else 0)"
  for P :: "'a prime ⇒ bool"
  by (transfer, simp)

lemma p_adic_prod_global_depth_setI:
  "x ∈ 𝒫∀p⇧n"
  if  "⋀p::'a prime. x ¬≃⇩p 0 ⟹ (x°⇧p) ≥ n"
  using that global_p_depth_p_adic_prod.global_depth_setI global_depth_set_p_adic_prod_def by auto

lemma p_adic_prod_global_depth_setI':
  "x ∈ 𝒫∀p⇧n"
  if  "⋀p::'a prime. (x°⇧p) ≥ n"
  using that global_p_depth_p_adic_prod.global_depth_setI' global_depth_set_p_adic_prod_def by auto

lemma p_adic_prod_global_depth_set_p_restrictI:
  "p_restrict x P ∈ 𝒫∀p⇧n"
  if "⋀p::'a prime. P p ⟹ x ∈ 𝒫@⇩p⇧n"
  using that global_p_depth_p_adic_prod.global_depth_set_p_restrictI
        global_depth_set_p_adic_prod_def
  by    auto

lemma p_adic_prod_p_depth_setI:
  "x ∈ 𝒫@⇩p⇧n"
  if "x ¬≃⇩p 0 ⟶ (x°⇧p) ≥ n"
  for p :: "'a prime"
  using that global_p_depth_p_adic_prod.p_depth_setI p_depth_set_p_adic_prod_def by auto

end (* context nontrivial_factorial_idom *)

context
  fixes p :: "'a::nontrivial_euclidean_ring_cancel prime"
begin

lemma p_adic_prod_diff_depth_gt_equiv_trans:
  "((x - z)°⇧p) > n"
  if  xy: "x ≃⇩p y"
  and yz: "y ¬≃⇩p z" "((y - z)°⇧p) > n"
  for x y z :: "'a p_adic_prod"
proof (cases x y z  rule: three_p_adic_prod_cases)
  case (abs_p_adic_prod_abs_p_adic_prod_abs_p_adic_prod X Y Z)
  from xy abs_p_adic_prod_abs_p_adic_prod_abs_p_adic_prod(1,2)
    have XY: "X ≃⇩p Y" using p_equal_p_adic_prod.abs_eq by auto
  moreover from yz(1) abs_p_adic_prod_abs_p_adic_prod_abs_p_adic_prod(2,3)
    have YZ: "Y ¬≃⇩p Z" using p_equal_p_adic_prod.abs_eq by auto
  moreover from yz(2) abs_p_adic_prod_abs_p_adic_prod_abs_p_adic_prod(2,3)
    have "((Y p - Z p)°⇧p) > n" using p_depth_p_adic_prod_diff_abs_eq' by metis
  ultimately have "∀k≤n. ((X p) pmod p) $$ k = ((Z p) pmod p) $$ k"
    using fls_pmod_eq_pmod_iff[of "X p" p "Y p"] fls_pmod_diff_cancel_iff by fastforce
  moreover have "(X p) ¬≃⇩p (Z p)" using XY YZ p_equality_fls.trans_right by auto
  ultimately show "n < ((x - z)°⇧p)"
    using abs_p_adic_prod_abs_p_adic_prod_abs_p_adic_prod(1,3) fls_pmod_diff_cancel_iff
          p_depth_p_adic_prod_diff_abs_eq'
    by    metis
qed

lemma p_adic_prod_diff_depth_gt0_equiv_trans:
  "((x - z)°⇧p) > n"
  if "n ≥ 0" and "x ≃⇩p y" and "((y - z)°⇧p) > n"
  for x y z :: "'a p_adic_prod"
  using that p_equality_p_adic_prod.conv_0 p_adic_prod_diff_depth_gt_equiv_trans
        global_p_depth_p_adic_prod.depth_equiv_0[of p "y - z"]
  by    fastforce

lemma p_adic_prod_diff_depth_gt_trans:
  "((x - z)°⇧p) > n"
  if  xy: "x ¬≃⇩p y" "((x - y)°⇧p) > n"
  and yz: "y ¬≃⇩p z" "((y - z)°⇧p) > n"
  and xz: "x ¬≃⇩p z"
  for x y z :: "'a p_adic_prod"
proof (cases x y z rule: three_p_adic_prod_cases)
  case (abs_p_adic_prod_abs_p_adic_prod_abs_p_adic_prod X Y Z)
  moreover from this xy(2) yz(2)
    have  "((X p - Y p)°⇧p) > n"
    and   "((Y p - Z p)°⇧p) > n"
    using p_depth_p_adic_prod_diff_abs_eq'
    by    (metis, metis)
  ultimately have "∀k≤n. ((X p) pmod p) $$ k = ((Z p) pmod p) $$ k"
    using xy(1) yz(1) by (simp add: p_equal_p_adic_prod.abs_eq fls_pmod_diff_cancel_iff)
  with xz abs_p_adic_prod_abs_p_adic_prod_abs_p_adic_prod(1,3)
    show  "n < ((x - z)°⇧p)"
    using p_equal_p_adic_prod.abs_eq[of p X Z] fls_pmod_diff_cancel_iff[of p "X p" "Z p"]
          p_depth_p_adic_prod_diff_abs_eq[of p X Z]
    by    simp
qed

lemma p_adic_prod_diff_depth_gt0_trans:
  "((x - z)°⇧p) > n"
  if  "n ≥ 0"
  and "((x - y)°⇧p) > n"
  and "((y - z)°⇧p) > n"
  and "x ¬≃⇩p z"
  for x y z :: "'a p_adic_prod"
  using that p_adic_prod_diff_depth_gt_trans
        p_equality_p_adic_prod.conv_0[of p x y] p_equality_p_adic_prod.conv_0[of p y z]
        global_p_depth_p_adic_prod.depth_equiv_0[of p "x - y"]
        global_p_depth_p_adic_prod.depth_equiv_0[of p "y - z"]
  by    auto

end (* context nontrivial_euclidean_ring_cancel *)

lemma p_adic_prod_diff_cancel_lead_coeff:
  "((inverse x - inverse y)°⇧p) > -n"
  if  x : "x ¬≃⇩p 0" "x°⇧p = n"
  and y : "y ¬≃⇩p 0" "y°⇧p = n"
  and xy: "x ¬≃⇩p y" "((x - y)°⇧p) > n"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
  and x y :: "'a p_adic_prod"
proof (cases x y rule: two_p_adic_prod_cases)
  case (abs_p_adic_prod_abs_p_adic_prod X Y)
  with x(1) y(1) xy(1)
    have  "X ¬≃⇩p 0"
    and   "Y ¬≃⇩p 0"
    and   "X ¬≃⇩p Y"
    using p_equal_p_adic_prod_abs_eq0 p_equal_p_adic_prod.abs_eq
    by    (fast, fast, fast)
  moreover from abs_p_adic_prod_abs_p_adic_prod x(2) y(2) xy(2)
    have  "X°⇧p = n"
    and   "Y°⇧p = n"
    and   "((X - Y)°⇧p) > n"
    using p_depth_p_adic_prod.abs_eq
    by    (metis, metis, metis minus_p_adic_prod.abs_eq)
  moreover from abs_p_adic_prod_abs_p_adic_prod have
    "((inverse x - inverse y)°⇧p) =
      ((
        (X¯∀p) -
        (Y¯∀p)
      )°⇧p)"
    using inverse_p_adic_prod.abs_eq[of X] inverse_p_adic_prod.abs_eq[of Y]
          p_depth_p_adic_prod_diff_abs_eq[of
            p "X¯∀p" "Y¯∀p"
          ]
    by    argo
  ultimately show ?thesis using global_pinverse_diff_cancel_lead_coeff by auto
qed

lemma global_unfrmzr_pows_p_adic_prod0:
  "(𝔭 (0 :: 'a::nontrivial_factorial_idom prime ⇒ int) :: 'a p_adic_prod) = 1"
  by (
    transfer,
    metis p_equality_depth_fls_pseq.globally_p_equal_refl globally_p_equal_fls_pseq_def
          global_unfrmzr_pows0_fls_pseq
  )

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma global_unfrmzr_pows_p_adic_prod_nequiv0:
  "(𝔭 f :: 'a p_adic_prod) ¬≃⇩p 0" for f :: "'a prime ⇒ int"
  by (transfer, rule global_unfrmzr_pows_fls_pseq_nequiv0)

lemma global_unfrmzr_pows_p_adic_prod:
  "(𝔭 f :: 'a p_adic_prod)°⇧p = f p" for f :: "'a prime ⇒ int"
  by (transfer, rule global_unfrmzr_pows_fls_pseq)

lemma global_unfrmzr_pows_p_adic_prod_depth_set:
  fixes   f :: "'a prime ⇒ int"
  defines "n ≡ f p"
  shows   "(𝔭 f :: 'a p_adic_prod) ∈ 𝒫@⇩p⇧n"
  using p_adic_prod_p_depth_setI[of p] n_def global_unfrmzr_pows_p_adic_prod[of f] by force

lemma global_unfrmzr_pows_p_adic_prod_pequiv_iff:
  "((𝔭 f :: 'a p_adic_prod) ≃⇩p (𝔭 g)) = (f p = g p)"
  for f g :: "'a prime ⇒ int"
  by (transfer, rule global_unfrmzr_pows_fls_pseq_pequiv_iff)

end (* context nontrivial_factorial_idom *)

lemma global_unfrmzr_pows_p_adic_prod_global_depth_set:
  "(𝔭 f :: 'a p_adic_prod) ∈ 𝒫∀p⇧n"
  if "∀p. f p ≥ n" for f :: "'a::nontrivial_factorial_idom prime ⇒ int"
  by (
    metis that global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.global_depth_setI
          global_unfrmzr_pows_p_adic_prod
  )

lemma global_unfrmzr_pows_p_adic_prod_global_depth_set_0:
  "(𝔭 (int ∘ f) :: 'a p_adic_prod) ∈ 𝒪∀p"
  for f :: "'a::nontrivial_factorial_idom prime ⇒ nat"
  using global_unfrmzr_pows_p_adic_prod_global_depth_set[of 0 "int ∘ f"] by simp

lemma global_unfrmzr_pows_prod_p_adic_prod:
  "(𝔭 f :: 'a p_adic_prod) * (𝔭 g) = 𝔭 (f + g)"
  for f g :: "'a::nontrivial_factorial_idom prime ⇒ int"
  by (
    transfer, simp, standard,
    simp only: global_unfrmzr_pows_prod_fls_pseq p_equality_fls.refl flip: times_fun_apply
  )

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma global_unfrmzr_pows_p_adic_prod_nzero:
  "(𝔭 f :: 'a p_adic_prod) ¬≃⇩p 0" for f :: "'a prime ⇒ int"
  by (transfer, rule global_unfrmzr_pows_fls_pseq_nzero)

lemma prod_w_global_unfrmzr_pows_p_adic_prod:
  "x ¬≃⇩p 0 ⟹
    (x * 𝔭 f)°⇧p = (x°⇧p) + f p"
  for f :: "'a prime ⇒ int" and x :: "'a p_adic_prod"
  by (transfer, rule prod_w_global_unfrmzr_pows_fls_pseq, simp)

lemma p_adic_prod_normalize_depth:
  "(x * 𝔭 (λp::'a prime. -(x°⇧p)))°⇧p = 0"
  for x :: "'a p_adic_prod"
  by (transfer, rule normalize_depth_fls_pseq)

end (* context nontrivial_factorial_idom *)

lemma p_adic_prod_normalized_depth_product_equiv:
  "(x * 𝔭 (λp::'a prime. -(x°⇧p))) *
    (y * 𝔭 (λp::'a prime. -(y°⇧p))) =
      ((x * y) * 𝔭 (λp::'a prime. -((x * y)°⇧p)))"
  for x y :: "'a::nontrivial_factorial_idom p_adic_prod"
proof transfer
  fix X Y :: "'a fls_pseq"
  define d :: "'a fls_pseq ⇒ 'a prime ⇒ int"
    where "d ≡ λX p. - (X°⇧p)"
  thus
    "(X * 𝔭 (d X)) * (Y * 𝔭 (d Y)) ≃∀p
      (X * Y * 𝔭 (d (X * Y)))"
    using times_fun_apply p_equal_fls_pseq_def normalized_depth_fls_pseq_product_equiv by fastforce
qed

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma trivial_global_unfrmzr_pows_p_adic_prod:
  "f p = 0 ⟹ (𝔭 f :: 'a p_adic_prod) ≃⇩p 1"
  for f :: "'a prime ⇒ int"
  by (transfer, rule trivial_global_unfrmzr_pows_fls_pseq, simp)

lemma prod_w_trivial_global_unfrmzr_pows_p_adic_prod:
  "f p = 0 ⟹ x * 𝔭 f ≃⇩p x"
  for f :: "'a prime ⇒ int" and x :: "'a p_adic_prod"
  by (transfer, rule prod_w_trivial_global_unfrmzr_pows_fls_pseq, simp)

end (* context nontrivial_factorial_idom *)

lemma global_unfrmzr_pows_p_adic_prod_pow:
  "(𝔭 f :: 'a p_adic_prod) ^ n = (𝔭 (λp. int n * f p))"
  for f :: "'a::nontrivial_factorial_idom prime ⇒ int"
  by (
    transfer,
    metis globally_p_equal_fls_pseq_def p_equality_depth_fls_pseq.globally_p_equal_refl
          pow_global_unfrmzr_pows_fls_pseq
  )
lemma global_unfrmzr_pows_p_adic_prod_inv:
  "(𝔭 (-f) :: 'a p_adic_prod) * (𝔭 f) = 1"
  for f :: "'a::nontrivial_factorial_idom prime ⇒ int"
  by (
    transfer,
    metis globally_p_equal_fls_pseq_def p_equality_depth_fls_pseq.globally_p_equal_refl
          global_unfrmzr_pows_fls_pseq_inv
  )

lemma global_unfrmzr_pows_p_adic_prod_inverse:
  "inverse (𝔭 f :: 'a p_adic_prod) = 𝔭 (-f)"
  for f :: "'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒ int"
proof (transfer)
  fix f :: "'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒ int"
  have "((𝔭 f)¯∀p) = (𝔭 (- f) :: 'a fls_pseq)"
    using global_unfrmzr_pows_fls_pseq_def[of f] global_unfrmzr_pows_fls_pseq_def[of "-f"]
          fls_pinv_X_intpow
    by    auto
  thus
    "((𝔭 f)¯∀p) ≃∀p
      (𝔭 (- f) :: 'a fls_pseq)"
    by auto
qed

lemma global_unfrmzr_pows_p_adic_prod_decomp:
  "x = (
    (x * 𝔭 (λp::'a prime. -(x°⇧p))) *
    𝔭 (λp::'a prime. x°⇧p)
  )"
  for p :: "'a::nontrivial_factorial_idom prime" and x :: "'a p_adic_prod"
  by (
    transfer,
    metis global_unfrmzr_pows_fls_pseq_decomp p_equality_depth_fls_pseq.globally_p_equal_refl
          globally_p_equal_fls_pseq_def
  )

lemma p_adic_prod_normalize_depthE:
  fixes   x :: "'a::nontrivial_factorial_idom p_adic_prod"
  obtains x_0
  where   "∀p::'a prime. x_0°⇧p = 0"
  and     "x = x_0 * 𝔭 (λp::'a prime. x°⇧p)"
  using   p_adic_prod_normalize_depth global_unfrmzr_pows_p_adic_prod_decomp
  by      blast

global_interpretation p_adic_prod_div_inv:
  global_p_equal_depth_div_inv
    "p_equal :: 'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    "p_depth :: 'a prime ⇒ 'a p_adic_prod ⇒ int"
    "p_restrict ::
      'a p_adic_prod ⇒ ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
proof
  fix p :: "'a prime" and x y :: "'a p_adic_prod"
  show "x / y = x * inverse y" by transfer simp
  show "inverse (inverse x) = x" by transfer (rule global_pinverse_pinverse_fls_pseq)
  show "inverse (x * y) = inverse x * inverse y" by transfer (rule global_pinverse_mult_fls_pseq)
  show "(inverse x ≃⇩p 0) = (x ≃⇩p 0)"
    by transfer (simp add: fls_pinv_equiv0_iff)
  show "x ¬≃⇩p 0 ⟹ x / x ≃⇩p 1"
    by transfer (simp add: pinverse_fls_mult_equiv1')
qed


subsection ‹Embeddings of the base ring, @{typ nat}, @{typ int}, and @{typ rat}›

subsubsection ‹Embedding of the base ring›

abbreviation "p_adic_prod_consts ≡ global_p_depth_p_adic_prod.consts"
abbreviation "p_adic_prod_const ≡ global_p_depth_p_adic_prod.const"

lemma p_depth_p_adic_prod_consts:
  "(p_adic_prod_consts f)°⇧p = ((f p)°⇧p)"
  for p :: "'a::nontrivial_factorial_idom prime" and f :: "'a prime ⇒ 'a"
  by (simp add: p_depth_p_adic_prod.abs_eq flip: p_depth_const_def)

lemmas p_depth_p_adic_prod_const = p_depth_p_adic_prod_consts[of _ "λp. _"]

lemma p_adic_prod_global_unfrmzr:
  "(𝔭 (1 :: 'a::nontrivial_factorial_idom prime ⇒ int) :: 'a p_adic_prod) =
    p_adic_prod_consts Rep_prime"
proof (rule global_p_depth_p_adic_prod.global_imp_eq, standard)
  fix p :: "'a prime"
  define 𝔭1_fls_pseq :: "'a fls_pseq" and 𝔭1_pre :: "'a p_adic_prod"
    where "𝔭1_fls_pseq ≡ 𝔭 (1 :: 'a prime ⇒ int)"
    and   "𝔭1_pre ≡ 𝔭 (1 :: 'a prime ⇒ int)"
  have
    "(abs_p_adic_prod 𝔭1_fls_pseq) ≃⇩p
      (abs_p_adic_prod (λp::'a prime. fls_const (Rep_prime p)))"
    unfolding 𝔭1_fls_pseq_def p_equal_p_adic_prod.abs_eq
    by        (rule global_unfrmzr_fls_pseq)
  thus "𝔭1_pre ≃⇩p (p_adic_prod_consts Rep_prime)"
    unfolding 𝔭1_fls_pseq_def 𝔭1_pre_def global_unfrmzr_pows_p_adic_prod_def by simp
qed


subsubsection ‹Embedding of the field of fractions of the base ring›

global_interpretation p_adic_prod_embeds:
  global_p_equal_div_inv_w_inj_idom_consts
    "p_equal :: 'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    "p_restrict ::
      'a p_adic_prod ⇒ ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
    "λf. abs_p_adic_prod (λp. fls_const (f p))"
  ..

global_interpretation p_adic_prod_depth_embeds:
  global_p_equal_depth_div_inv_w_inj_index_consts
    "p_equal :: 'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    "p_depth :: 'a prime ⇒ 'a p_adic_prod ⇒ int"
    "p_restrict ::
      'a p_adic_prod ⇒ ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
    "λf. abs_p_adic_prod (λp. fls_const (f p))"
    Rep_prime
  ..

abbreviation "p_adic_prod_shift_p_depth ≡ p_adic_prod_depth_embeds.shift_p_depth"
abbreviation "p_adic_prod_of_fract      ≡ p_adic_prod_embeds.const_of_fract"

lemma p_adic_prod_of_fract_depth:
  "(p_adic_prod_of_fract (Fraction_Field.Fract a b) :: 'a p_adic_prod)°⇧p =
    (a°⇧p) - (b°⇧p)"
  if  "a ≠ 0" and "b ≠ 0"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
  and a b :: 'a
  using that global_p_depth_p_adic_prod.p_equal_func_of_const_0
        p_adic_prod_div_inv.divide_equiv_0_iff p_adic_prod_embeds.const_of_fract_Fract
        p_adic_prod_div_inv.divide_depth p_depth_p_adic_prod_const
  by    metis

text ‹Product of all p-adic embeddings of the field of fractions of the base ring.›
abbreviation p_adic_Fracts_prod ::
  "'a::nontrivial_factorial_unique_euclidean_bezout p_adic_prod set"
  ("𝒬∀p")
  where "𝒬∀p ≡ p_adic_prod_embeds.range_const_of_fract"

subsubsection ‹Characteristic zero embeddings›

class nontrivial_factorial_idom_char_0 = nontrivial_factorial_idom + semiring_char_0
begin
subclass ring_char_0 ..
end

instance int :: nontrivial_factorial_idom_char_0 ..

class nontrivial_factorial_unique_euclidean_bezout_char_0 =
  nontrivial_factorial_unique_euclidean_bezout + nontrivial_factorial_idom_char_0

instance int :: nontrivial_factorial_unique_euclidean_bezout_char_0 ..

instance p_adic_prod :: (nontrivial_factorial_idom_char_0) ring_char_0
  by (
    standard, standard,
    metis global_p_depth_p_adic_prod.const_of_nat global_p_depth_p_adic_prod.const_eq_iff
          of_nat_eq_iff
  )

global_interpretation p_adic_prod_consts_char_0:
  global_p_equality_w_inj_consts_char_0
    "p_equal :: 'a::nontrivial_factorial_idom_char_0 prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    "p_restrict ::
      'a p_adic_prod ⇒ ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
    "λf. abs_p_adic_prod (λp. fls_const (f p))"
  ..

global_interpretation p_adic_prod_div_inv_consts_char_0:
  global_p_equal_div_inv_w_inj_consts_char_0
    "p_equal :: 'a::nontrivial_factorial_unique_euclidean_bezout_char_0 prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    "p_restrict ::
      'a p_adic_prod ⇒ ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
    "λf. abs_p_adic_prod (λp. fls_const (f p))"
 ..

lemma p_adic_prod_of_nat_depth:
  "(of_nat n :: 'a p_adic_prod)°⇧p = ((of_nat n :: 'a)°⇧p)"
  for p :: "'a::nontrivial_factorial_idom prime"
  by (metis global_p_depth_p_adic_prod.const_of_nat p_depth_p_adic_prod_const)

lemma p_adic_prod_of_int_depth:
  "(of_int z :: 'a p_adic_prod)°⇧p = ((of_int z :: 'a)°⇧p)"
  for p :: "'a::nontrivial_factorial_idom prime"
  by (metis global_p_depth_p_adic_prod.const_of_int p_depth_p_adic_prod_const)

abbreviation "p_adic_prod_of_rat ≡ p_adic_prod_div_inv_consts_char_0.const_of_rat"

lemma p_adic_prod_of_rat_depth:
  "(p_adic_prod_of_rat (Rat.Fract a b) :: 'a p_adic_prod)°⇧p =
    ((of_int a :: 'a)°⇧p) - ((of_int b :: 'a)°⇧p)"
  if  "a ≠ 0" and "b ≠ 0"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout_char_0 prime"
  and a b :: int
  using that p_adic_prod_consts_char_0.const_of_int_p_equal_0_iff
        p_adic_prod_div_inv.divide_equiv_0_iff p_adic_prod_div_inv_consts_char_0.const_of_rat_rat
        p_adic_prod_div_inv.divide_depth p_adic_prod_of_int_depth
  by    metis


subsection ‹Topologies on products of p-adic fields›

subsubsection ‹By local place›

text ‹Completeness›

abbreviation "p_adic_prod_p_open_nbhd ≡ global_p_depth_p_adic_prod.p_open_nbhd"
abbreviation "p_adic_prod_p_open_nbhds ≡ global_p_depth_p_adic_prod.p_open_nbhds"
abbreviation
  "p_adic_prod_p_limseq_condition ≡ global_p_depth_p_adic_prod.p_limseq_condition"
abbreviation
  "p_adic_prod_p_cauchy_condition ≡ global_p_depth_p_adic_prod.p_cauchy_condition"
abbreviation "p_adic_prod_p_limseq ≡ global_p_depth_p_adic_prod.p_limseq"
abbreviation "p_adic_prod_p_cauchy ≡ global_p_depth_p_adic_prod.p_cauchy"
abbreviation
  "p_adic_prod_p_open_nbhds_limseq ≡ global_p_depth_p_adic_prod.p_open_nbhds_LIMSEQ"
abbreviation
  "p_adic_prod_local_p_open_nbhds ≡ global_p_depth_p_adic_prod.local_p_open_nbhds"

lemma abs_p_adic_prod_seq_cases [case_names abs_p_adic_prod]:
  C if "⋀F. X = (λn. abs_p_adic_prod (F n)) ⟹ C"
proof-
  have "X = (λn. abs_p_adic_prod (rep_p_adic_prod (X n)))"
    using rep_p_adic_prod_inverse by metis
  with that show C by fast
qed

lemma abs_p_adic_prod_p_limseq_condition:
  "p_adic_prod_p_limseq_condition p (λn. abs_p_adic_prod (F n)) (abs_p_adic_prod X) n K =
    fls_p_limseq_condition p (λn. F n p) (X p) n K"
  unfolding global_p_depth_p_adic_prod.p_limseq_condition_def p_depth_fls.p_limseq_condition_def
  by (auto simp add: p_equal_p_adic_prod.abs_eq p_depth_p_adic_prod_diff_abs_eq)

lemma abs_p_adic_prod_p_limseq:
  "p_adic_prod_p_limseq p (λn. abs_p_adic_prod (F n)) (abs_p_adic_prod X) =
    fls_p_limseq p (λn. F n p) (X p)"
  using abs_p_adic_prod_p_limseq_condition by fast

lemma abs_p_adic_prod_p_cauchy_condition:
  "p_adic_prod_p_cauchy_condition p (λn. abs_p_adic_prod (F n)) n K =
    fls_p_cauchy_condition p (λn. F n p) n K"
  unfolding global_p_depth_p_adic_prod.p_cauchy_condition_def p_depth_fls.p_cauchy_condition_def
  by (auto simp add: p_equal_p_adic_prod.abs_eq p_depth_p_adic_prod_diff_abs_eq)

lemma abs_p_adic_prod_p_cauchy:
  "p_adic_prod_p_cauchy p (λn. abs_p_adic_prod (F n)) = fls_p_cauchy p (λn. F n p) "
  using abs_p_adic_prod_p_cauchy_condition by blast

lemma p_adic_prod_p_restrict_cauchy_lim:
  "p_adic_prod_p_limseq q
    (λn. p_restrict (X n) ((=) p))
    (abs_p_adic_prod (λq.
      if q = p then fls_p_cauchy_lim p (λn. rep_p_adic_prod (X n) p) else 0
    ))"
  if "p_adic_prod_p_cauchy p X"
proof (cases X rule: abs_p_adic_prod_seq_cases)
  case (abs_p_adic_prod F)
  define limval where
    "limval ≡
      abs_p_adic_prod (λq.
        if q = p then fls_p_cauchy_lim p (λn. rep_p_adic_prod (X n) p) else 0
      )"
  show "p_adic_prod_p_limseq q (λn. X n prestrict (=) p) limval"
  proof (cases "p = q")
    case True
    with that abs_p_adic_prod have F: "fls_p_cauchy q (λn. F n q)"
      using abs_p_adic_prod_p_cauchy by blast
    have "fls_p_limseq q (λn. F n q) (fls_p_cauchy_lim q (λn. F n q))"
      using F fls_p_cauchy_limseq by blast
    moreover have
      "fls_p_cauchy_lim q (λn. rep_p_adic_prod (abs_p_adic_prod (F n)) q) =
        fls_p_cauchy_lim q (λn. F n q)"
      by (
        intro fls_p_cauchy_lim_unique F, clarify,
        use abs_p_adic_prod p_adic_prod_globally_p_equal_self globally_p_equal_fls_pseq_def
        in  auto
      )
    ultimately have "p_adic_prod_p_limseq q X limval"
      using True limval_def abs_p_adic_prod abs_p_adic_prod_p_limseq by force
    moreover from True have "∀n. (p_restrict (X n) ((=) p)) ≃⇩q (X n)"
      using global_p_depth_p_adic_prod.p_restrict_equiv by blast
    ultimately show ?thesis
      using global_p_depth_p_adic_prod.p_limseq_p_cong[of 0 q _ X limval limval] by auto
  next
    case False
    with abs_p_adic_prod limval_def show ?thesis
      using global_p_depth_p_adic_prod.p_restrict_equiv0[of "(=) p" q]
            p_equal_p_adic_prod_abs_eq0[of q]
            global_p_depth_p_adic_prod.p_limseq_p_cong[of
              0 q "λn. (X n) prestrict (=) p" 0 limval
            ]
            global_p_depth_p_adic_prod.p_limseq_0_iff[of q limval]
      by    fastforce
  qed
qed


global_interpretation p_complete_p_adic_prod:
  p_complete_global_p_equal_depth
    "p_equal :: 'a::nontrivial_euclidean_ring_cancel prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    "p_restrict ::
      'a p_adic_prod ⇒ ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
    "p_depth :: 'a prime ⇒ 'a p_adic_prod ⇒ int"
proof
  fix p :: "'a prime" and X :: "nat ⇒ 'a p_adic_prod"
  define res_X :: "nat ⇒ 'a p_adic_prod" and limval :: "'a p_adic_prod"
    where "res_X ≡ λn. p_restrict (X n) ((=) p)"
    and
      "limval ≡
        abs_p_adic_prod (λq.
          if q = p then fls_p_cauchy_lim p (λn. rep_p_adic_prod (X n) p) else 0
        )"
  moreover assume "p_adic_prod_p_cauchy p X"
  ultimately have "∀q. p_adic_prod_p_limseq q res_X limval"
    using p_adic_prod_p_restrict_cauchy_lim by blast
  hence "p_adic_prod_p_open_nbhds_limseq res_X limval"
    using global_p_depth_p_adic_prod.globally_limseq_iff_locally_limseq by fast
  thus "global_p_depth_p_adic_prod.p_open_nbhds_convergent res_X"
    using global_p_depth_p_adic_prod.t2_p_open_nbhds.convergent_def by auto
qed

global_interpretation p_complete_p_adic_prod_div_inv:
  p_complete_global_p_equal_depth_div_inv
    "p_equal :: 'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒
      'a p_adic_prod ⇒ 'a p_adic_prod ⇒ bool"
    "p_depth :: 'a prime ⇒ 'a p_adic_prod ⇒ int"
    "p_restrict ::
      'a p_adic_prod ⇒ ('a prime ⇒ bool) ⇒ 'a p_adic_prod"
  ..

lemmas p_adic_prod_hensel = p_complete_p_adic_prod_div_inv.hensel


subsubsection ‹By bounded global depth›

text ‹The metric›
instantiation p_adic_prod :: (nontrivial_factorial_idom) metric_space
begin

definition "dist = global_p_depth_p_adic_prod.bdd_global_dist"
declare dist_p_adic_prod_def [simp]

definition "uniformity = global_p_depth_p_adic_prod.bdd_global_uniformity"
declare uniformity_p_adic_prod_def [simp]

definition open_p_adic_prod :: "'a p_adic_prod set ⇒ bool"
  where
    "open_p_adic_prod U = (∀x∈U.
      eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity
    )"

instance
  by (
    standard,
    simp_all add: global_p_depth_p_adic_prod.bdd_global_uniformity_def open_p_adic_prod_def
                  global_p_depth_p_adic_prod.metric_space_by_bdd_depth.dist_triangle2
  )

end (* instantiation p_adic_prod metric_space *)

abbreviation "p_adic_prod_global_depth ≡ global_p_depth_p_adic_prod.bdd_global_depth"

lemma bdd_global_depth_p_adic_prod_abs_eq:
  "p_adic_prod_global_depth (abs_p_adic_prod X) = fls_pseq_bdd_global_depth X"
proof (cases "X ≃∀p 0")
  case True
  hence "abs_p_adic_prod X = 0"
    using p_adic_prod_lift_globally_p_equal zero_p_adic_prod.abs_eq by metis
  with True show ?thesis by force
next
  case False
  hence "abs_p_adic_prod X ≠ 0"
    using p_adic_prod.abs_eq_iff zero_p_adic_prod.abs_eq by metis
  hence "¬ abs_p_adic_prod X ≃∀p 0"
    using global_p_depth_p_adic_prod.global_eq_iff by auto
  hence
    "p_adic_prod_global_depth (abs_p_adic_prod X) =
      (INF p∈{p::'a prime. abs_p_adic_prod X ¬≃⇩p 0}.
        nat (((abs_p_adic_prod X)°⇧p) + 1))"
    using global_p_depth_p_adic_prod.bdd_global_depthD_as_image[of "abs_p_adic_prod X"]
    by    fastforce
  also have
    "… = (INF p∈{p::'a prime. X ¬≃⇩p 0}.
      nat (((abs_p_adic_prod X)°⇧p) + 1))"
    using p_equal_p_adic_prod.abs_eq zero_p_adic_prod.abs_eq by metis
  finally show ?thesis
    using False p_depth_p_adic_prod.abs_eq[of _ X]
          p_equality_depth_fls_pseq.bdd_global_depthD_as_image
    by    force
qed

lemma dist_p_adic_prod_abs_eq:
  "dist (abs_p_adic_prod X) (abs_p_adic_prod Y) = fls_pseq_bdd_global_dist X Y"
proof (cases "X ≃∀p Y")
  case True
  hence "abs_p_adic_prod X = abs_p_adic_prod Y" using p_adic_prod_lift_globally_p_equal by metis
  with True show ?thesis by fastforce
next
  case False
  from False have "abs_p_adic_prod X ≠ abs_p_adic_prod Y"
    using p_adic_prod.abs_eq_iff by metis
  hence "¬ abs_p_adic_prod X ≃∀p abs_p_adic_prod Y"
    using global_p_depth_p_adic_prod.global_eq_iff by auto
  hence
    "dist (abs_p_adic_prod X) (abs_p_adic_prod Y) =
      inverse (2 ^ p_adic_prod_global_depth (abs_p_adic_prod X - abs_p_adic_prod Y))"
    using global_p_depth_p_adic_prod.bdd_global_distD by auto
  also have "… = inverse (2 ^ p_adic_prod_global_depth (abs_p_adic_prod (X - Y)))"
    using minus_p_adic_prod.abs_eq by metis
  finally show ?thesis
    using False bdd_global_depth_p_adic_prod_abs_eq p_equality_depth_fls_pseq.bdd_global_distD
    by    fastforce
qed

lemma p_adic_prod_metric_is_finer:
  "generate_topology p_adic_prod_p_open_nbhds U ⟹ open U"
proof (induct U rule: generate_topology.induct)
  case (Basis U) show "open U"
  proof (intro Elementary_Metric_Spaces.openI)
    fix u assume "u ∈ U"
    moreover from Basis obtain p n x where "U = p_adic_prod_p_open_nbhd p n x"
      by fast
    ultimately have U: "U = p_adic_prod_p_open_nbhd p n u"
      using global_p_depth_p_adic_prod.p_open_nbhd_circle_multicentre by fast
    have "ball u (inverse (2 ^ nat n)) ⊆ U"
      unfolding U global_p_depth_p_adic_prod.p_open_nbhd_eq_circle ball_def
      using     global_p_depth_p_adic_prod.bdd_global_dist_sym[of u]
                global_p_depth_p_adic_prod.bdd_global_dist_less_pow2_iff[of _ u "nat n"]
      by        auto
    thus "∃e>0. ball u e ⊆ U" by force
  qed
qed (simp, fast, fast)

lemma p_adic_prod_metric_is_finer_than_purely_local:
  "generate_topology (p_adic_prod_local_p_open_nbhds p) U ⟹
    open U"
  for p :: "'a::nontrivial_factorial_idom prime"
  and U :: "'a p_adic_prod set"
  using global_p_depth_p_adic_prod.local_p_open_nbhds_are_coarser p_adic_prod_metric_is_finer
  by    blast

lemma p_adic_prod_limseq_abs_eq:
  "(λn. abs_p_adic_prod (X n)) ⇢ abs_p_adic_prod x
    ⟷
    (∀e>0. ∀F n in sequentially. fls_pseq_bdd_global_dist (X n) x < e)"
proof-
  have
    "∀n. dist (abs_p_adic_prod (X n)) (abs_p_adic_prod x) =
      fls_pseq_bdd_global_dist (X n) x"
    using dist_p_adic_prod_abs_eq[of "X _" x] by blast
  thus ?thesis
    using tendsto_iff[of "λn. abs_p_adic_prod (X n)" "abs_p_adic_prod x"] by presburger
qed

lemma p_adic_prod_bdd_metric_LIMSEQ:
  "X ⇢ x = global_p_depth_p_adic_prod.metric_space_by_bdd_depth.LIMSEQ X x"
  for X :: "nat ⇒ 'a::nontrivial_factorial_idom p_adic_prod" and x :: "'a p_adic_prod"
  unfolding tendsto_iff global_p_depth_p_adic_prod.metric_space_by_bdd_depth.tendsto_iff
            dist_p_adic_prod_def
  by        fast

lemma p_adic_prod_global_depth_set_lim_closed:
  "x ∈ 𝒫∀p⇧n"
  if  lim  : "X ⇢ x"
  and depth: "∀F k in sequentially. X k ∈ 𝒫∀p⇧n"
  for X :: "nat ⇒ 'a::nontrivial_factorial_unique_euclidean_bezout p_adic_prod"
  and x :: "'a p_adic_prod"
  using that p_adic_prod_bdd_metric_LIMSEQ p_adic_prod_depth_embeds.global_depth_set_LIMSEQ_closed
  by    fastforce

lemma p_adic_prod_metric_ball_multicentre:
  "ball y e = ball x e" if "y ∈ ball x e"
  for x y :: "'a::nontrivial_factorial_idom p_adic_prod"
  using     that global_p_depth_p_adic_prod.bdd_global_dist_ball_multicentre
  unfolding ball_def dist_p_adic_prod_def
  by        blast

lemma p_adic_prod_metric_ball_at_0:
  "ball (0::'a::nontrivial_factorial_idom p_adic_prod) (inverse (2 ^ n)) = global_depth_set (int n)"
  using     global_p_depth_p_adic_prod.bdd_global_dist_ball_at_0
  unfolding ball_def dist_p_adic_prod_def global_depth_set_p_adic_prod_def
  by        auto

lemma p_adic_prod_metric_ball_UNIV:
  "ball x e = UNIV" if "e > 1"
  for x :: "'a::nontrivial_factorial_idom p_adic_prod"
  using     that global_p_depth_p_adic_prod.bdd_global_dist_ball_UNIV
  unfolding ball_def dist_p_adic_prod_def
  by        blast

lemma p_adic_prod_metric_ball_at_0_normalize:
  "ball (0::'a::nontrivial_factorial_idom p_adic_prod) e =
    global_depth_set ⌊log 2 (inverse e)⌋"
  if "e > 0" and "e ≤ 1"
  using     that global_p_depth_p_adic_prod.bdd_global_dist_ball_at_0_normalize
  unfolding ball_def dist_p_adic_prod_def global_depth_set_p_adic_prod_def
  by        blast

lemma p_adic_prod_metric_ball_translate:
  "ball x e = x +o ball 0 e" for x :: "'a::nontrivial_factorial_idom p_adic_prod"
  using     global_p_depth_p_adic_prod.bdd_global_dist_ball_translate
  unfolding ball_def dist_p_adic_prod_def
  by        blast

lemma p_adic_prod_left_translate_metric_continuous:
  "continuous_on UNIV ((+) x)" for x :: "'a::nontrivial_factorial_idom p_adic_prod"
proof
  fix e :: real and z :: "'a p_adic_prod"
  assume e: "e > 0"
  moreover have "∀y. dist y z < e ⟶ dist (x + y) (x + z) ≤ e"
    using global_p_depth_p_adic_prod.bdd_global_dist_left_translate_continuous[of
            _ _ e x
          ]
    unfolding dist_p_adic_prod_def
    by        fastforce
  ultimately show
    "∃d>0. ∀x'∈UNIV.
      dist x' z < d ⟶ dist (x + x') (x + z) ≤ e"
    by auto
qed

lemma p_adic_prod_right_translate_metric_continuous:
  "continuous_on UNIV (λz. z + x)" for x :: "'a::nontrivial_factorial_idom p_adic_prod"
proof-
  have "(λz. z + x) = (+) x" by (auto simp add: add.commute)
  thus ?thesis using p_adic_prod_left_translate_metric_continuous by metis
qed

lemma p_adic_prod_left_bdd_mult_bdd_metric_continuous:
  "continuous_on UNIV ((*) x)"
  if bdd:
    "∀p::'a prime. x ¬≃⇩p 0 ⟶
      (x°⇧p) ≥ n"
  for x :: "'a::nontrivial_factorial_idom p_adic_prod"
proof
  fix e :: real and z :: "'a p_adic_prod"
  assume e: "e > 0"
  moreover define d where "d ≡ min (e * 2 powi (n - 1)) 1"
  ultimately have "∀y. dist y z < d ⟶ dist (x * y) (x * z) ≤ e"
    using bdd global_p_depth_p_adic_prod.bdd_global_dist_bdd_mult_continuous by fastforce
  moreover from e d_def have "d > 0" by auto
  ultimately show
    "∃d>0. ∀y∈UNIV. dist y z < d ⟶ dist (x * y) (x * z) ≤ e"
    by blast
qed

lemma p_adic_prod_bdd_metric_limseq_bdd_mult:
  "(λk. w * X k) ⇢ (w * x)"
  if bdd:
    "∀p::'a prime. w ¬≃⇩p 0 ⟶
      (w°⇧p) ≥ n"
  and seq: "X ⇢ x"
  for w x :: "'a::nontrivial_factorial_idom p_adic_prod" and X :: "nat ⇒ 'a p_adic_prod"
  using bdd seq p_adic_prod_left_bdd_mult_bdd_metric_continuous continuous_on_tendsto_compose
  by    fastforce

lemma p_adic_prod_nonpos_global_depth_set_open:
  "ball x 1 ⊆ (𝒫∀p⇧n)"
  if "n ≤ 0" and "x ∈ (𝒫∀p⇧n)"
  for x :: "'a::nontrivial_factorial_idom p_adic_prod"
proof-
  have "ball x 1 = x +o ball 0 1" using p_adic_prod_metric_ball_translate by blast
  also have "… = x +o (𝒪∀p)"
    using p_adic_prod_metric_ball_at_0[of 0] by auto
  finally show ?thesis
    using that global_p_depth_p_adic_prod.global_depth_set_elt_set_plus_closed[of n 0] by auto
qed

lemma p_adic_prod_global_depth_set_open:
  "open ((𝒫∀p⇧n) :: 'a::nontrivial_factorial_idom p_adic_prod set)"
proof (cases "n ≥ 0")
  case True
  hence "(𝒫∀p⇧n) = ball (0::'a p_adic_prod) (inverse (2 ^ nat n))"
    using p_adic_prod_metric_ball_at_0 by fastforce
  thus ?thesis by simp
next
  case False thus ?thesis
    using p_adic_prod_nonpos_global_depth_set_open[of n]
          Elementary_Metric_Spaces.openI[of
            "(𝒫∀p⇧n) :: 'a p_adic_prod set"
          ]
    by    force
qed

lemma p_adic_prod_ball_abs_eq:
  "abs_p_adic_prod ` {Y. fls_pseq_bdd_global_dist X Y < e} =
    ball (abs_p_adic_prod X) e"
  for x :: "'a::nontrivial_factorial_idom p_adic_prod"
proof-
  define B B'
    where "B ≡  {Y. fls_pseq_bdd_global_dist X Y < e}"
    and   "B' ≡ ball (abs_p_adic_prod X) e"
  moreover have "⋀y. y ∈ B' ⟹ y ∈ abs_p_adic_prod ` B"
  proof-
    fix y assume y: "y ∈ B'"
    show "y ∈ abs_p_adic_prod ` B"
    proof (cases y)
      case (abs_p_adic_prod Y)
      moreover from this B'_def y have "fls_pseq_bdd_global_dist X Y < e"
        using mem_ball dist_p_adic_prod_abs_eq by metis
      ultimately show ?thesis using B_def by blast
    qed
  qed
  ultimately show "abs_p_adic_prod ` B = B'"
    using dist_p_adic_prod_abs_eq[of X] by fastforce
qed

text ‹Completeness›

abbreviation "p_adic_prod_globally_cauchy ≡ global_p_depth_p_adic_prod.globally_cauchy"
abbreviation
  "p_adic_prod_global_cauchy_condition  ≡ global_p_depth_p_adic_prod.global_cauchy_condition"

lemma p_adic_prod_global_cauchy_condition_abs_eq:
  "p_adic_prod_global_cauchy_condition (λn. abs_p_adic_prod (X n)) =
    fls_pseq_global_cauchy_condition X"
  unfolding global_p_depth_p_adic_prod.global_cauchy_condition_def
            p_equality_depth_fls_pseq.global_cauchy_condition_def
  by        (
              standard, standard,
              metis p_equal_p_adic_prod.abs_eq p_depth_p_adic_prod_diff_abs_eq
            )

lemma p_adic_prod_globally_cauchy_abs_eq:
  "p_adic_prod_globally_cauchy (λn. abs_p_adic_prod (X n)) = fls_pseq_globally_cauchy X"
  using p_adic_prod_global_cauchy_condition_abs_eq by metis

lemma p_adic_prod_globally_cauchy_vs_bdd_metric_Cauchy:
  "p_adic_prod_globally_cauchy X = Cauchy X"
  for X :: "nat ⇒ 'a::nontrivial_factorial_idom p_adic_prod"
  using     global_p_depth_p_adic_prod.globally_cauchy_vs_bdd_metric_Cauchy
  unfolding global_p_depth_p_adic_prod.metric_space_by_bdd_depth.Cauchy_def Cauchy_def
  by        auto

abbreviation
  "p_adic_prod_cauchy_lim X ≡
    abs_p_adic_prod (λp.
      fls_condition_lim p
        (λn. reduced_rep_p_adic_prod (X n) p)
        (p_adic_prod_global_cauchy_condition X)
    )"

lemma p_adic_prod_bdd_metric_complete':
  "X ⇢ p_adic_prod_cauchy_lim X" if "Cauchy X"
proof (cases X rule: p_adic_prod_seq_reduced_cases)
  case (abs_p_adic_prod F) with that show ?thesis
    using p_adic_prod_globally_cauchy_vs_bdd_metric_Cauchy[of "λn. abs_p_adic_prod (F n)"]
          p_adic_prod_globally_cauchy_abs_eq fls_pseq_cauchy_condition_lim
          p_adic_prod_global_cauchy_condition_abs_eq[of F] abs_p_adic_prod_inverse[of "F _"]
          p_adic_prod_limseq_abs_eq[of F]
    by    fastforce
qed

lemma p_adic_prod_bdd_metric_complete:
  "complete (UNIV :: 'a::nontrivial_euclidean_ring_cancel p_adic_prod set)"
  using p_adic_prod_bdd_metric_complete' completeI by blast


subsection ‹Hiding implementation details›

lifting_update p_adic_prod.lifting
lifting_forget p_adic_prod.lifting


subsection ‹The subring of adelic integers›

subsubsection ‹Type definition as a subtype of adeles›

typedef (overloaded) 'a adelic_int =
  "𝒪∀p :: 'a::nontrivial_factorial_idom p_adic_prod set"
  using global_p_depth_p_adic_prod.global_depth_set_0 by auto

lemma Abs_adelic_int_inverse':
  "Rep_adelic_int (Abs_adelic_int x) = x" if "x ∈ 𝒪∀p"
  using that Abs_adelic_int_inverse by fast

lemma Abs_adelic_int_cases [case_names Abs_adelic_int, cases type: adelic_int]:
  P if
    "⋀x. z = Abs_adelic_int x ⟹
      x ∈ 𝒪∀p ⟹ P"
proof-
  define x where "x ≡ Rep_adelic_int z"
  hence "z = Abs_adelic_int x" using Rep_adelic_int_inverse by metis
  moreover from x_def have "x ∈ 𝒪∀p" using Rep_adelic_int by blast
  ultimately show P using that by fast
qed

lemmas  two_Abs_adelic_int_cases   = Abs_adelic_int_cases[case_product Abs_adelic_int_cases]
  and   three_Abs_adelic_int_cases =
    Abs_adelic_int_cases[case_product Abs_adelic_int_cases[case_product Abs_adelic_int_cases]]

lemma adelic_int_seq_cases [case_names Abs_adelic_int]:
  fixes X :: "nat ⇒ 'a::nontrivial_factorial_idom adelic_int"
  obtains F :: "nat ⇒ 'a p_adic_prod"
    where "X = (λn. Abs_adelic_int (F n))"
    and   "range F ⊆ 𝒪∀p"
proof-
  define F where "F ≡ λn. Rep_adelic_int (X n)"
  hence "X = (λn. Abs_adelic_int (F n))"
    using Rep_adelic_int_inverse by metis
  moreover from F_def have "range F ⊆ 𝒪∀p"
    using Rep_adelic_int by blast
  ultimately show thesis using that by presburger
qed

subsubsection ‹Algebraic instantiaions›

instantiation adelic_int :: (nontrivial_factorial_idom) comm_ring_1
begin

definition "0 = Abs_adelic_int 0"

lemma zero_adelic_int_rep_eq: "Rep_adelic_int 0 = 0"
  using global_p_depth_p_adic_prod.global_depth_set_0[of 0] Abs_adelic_int_inverse
  by    (simp add: zero_adelic_int_def)

definition "1 ≡ Abs_adelic_int 1"

lemma one_adelic_int_rep_eq: "Rep_adelic_int 1 = 1"
  using global_p_depth_p_adic_prod.global_depth_set_1 Abs_adelic_int_inverse
  by    (simp add: one_adelic_int_def)

definition "x + y = Abs_adelic_int (Rep_adelic_int x + Rep_adelic_int y)"

lemma plus_adelic_int_rep_eq: "Rep_adelic_int (a + b) = Rep_adelic_int a + Rep_adelic_int b"
  using     Rep_adelic_int global_p_depth_p_adic_prod.global_depth_set_add Abs_adelic_int_inverse
  unfolding plus_adelic_int_def
  by        fastforce

lemma plus_adelic_int_abs_eq:
  "x ∈ 𝒪∀p ⟹
    y ∈ 𝒪∀p ⟹
    Abs_adelic_int x + Abs_adelic_int y = Abs_adelic_int (x + y)"
  using     Abs_adelic_int_inverse[of x] Abs_adelic_int_inverse[of y]
  unfolding plus_adelic_int_def
  by        simp

definition "-x = Abs_adelic_int (- Rep_adelic_int x)"

lemma uminus_adelic_int_rep_eq: "Rep_adelic_int (- x) = - Rep_adelic_int x"
  using     Rep_adelic_int global_p_depth_p_adic_prod.global_depth_set_uminus
            Abs_adelic_int_inverse
  unfolding uminus_adelic_int_def
  by        auto

lemma uminus_adelic_int_abs_eq:
  "x ∈ 𝒪∀p ⟹ - Abs_adelic_int x = Abs_adelic_int (- x)"
  using Abs_adelic_int_inverse[of x] unfolding uminus_adelic_int_def by simp

definition minus_adelic_int ::
  "'a adelic_int ⇒ 'a adelic_int ⇒ 'a adelic_int"
  where "minus_adelic_int ≡ (λx y. x + - y)"

lemma minus_adelic_int_rep_eq: "Rep_adelic_int (x - y) = Rep_adelic_int x - Rep_adelic_int y"
  using plus_adelic_int_rep_eq uminus_adelic_int_rep_eq by (simp add: minus_adelic_int_def)

lemma minus_adelic_int_abs_eq:
  "x ∈ 𝒪∀p ⟹
    y ∈ 𝒪∀p ⟹
    Abs_adelic_int x - Abs_adelic_int y = Abs_adelic_int (x - y)"
  using global_p_depth_p_adic_prod.global_depth_set_uminus[of y]
  by    (simp add:
          minus_adelic_int_def uminus_adelic_int_abs_eq
          plus_adelic_int_abs_eq
        )

definition "x * y = Abs_adelic_int (Rep_adelic_int x * Rep_adelic_int y)"

lemma times_adelic_int_rep_eq: "Rep_adelic_int (x * y) = Rep_adelic_int x * Rep_adelic_int y"
  using     Rep_adelic_int global_p_depth_p_adic_prod.global_depth_set_times Abs_adelic_int_inverse
  unfolding times_adelic_int_def
  by        force

lemma times_adelic_int_abs_eq:
  "x ∈ 𝒪∀p ⟹
    y ∈ 𝒪∀p ⟹
    Abs_adelic_int x * Abs_adelic_int y = Abs_adelic_int (x * y)"
  using     Abs_adelic_int_inverse[of x] Abs_adelic_int_inverse[of y]
  unfolding times_adelic_int_def
  by        simp

instance
proof

  fix a b c :: "'a adelic_int"

  show "a + b = b + a" by (cases a, cases b) (simp add: plus_adelic_int_abs_eq add.commute)
  show "0 + a = a"
    using     global_p_depth_p_adic_prod.global_depth_set_0 plus_adelic_int_abs_eq[of 0]
    unfolding zero_adelic_int_def
    by        (cases a) auto
  show "1 * a = a"
    using global_p_depth_p_adic_prod.global_depth_set_1 times_adelic_int_abs_eq[of 1]
    by    (cases a) (simp add: one_adelic_int_def)
  show "- a + a = 0"
    using     global_p_depth_p_adic_prod.global_depth_set_uminus uminus_adelic_int_abs_eq
              plus_adelic_int_abs_eq
    unfolding zero_adelic_int_def
   by         (cases a) fastforce
  show "a - b = a + - b" by (simp add: minus_adelic_int_def)
  show "a * b = b * a" by (cases a, cases b) (simp add: times_adelic_int_abs_eq mult.commute)

  show "a + b + c = a + (b + c)"
  proof (cases a b c rule: three_Abs_adelic_int_cases)
    case (Abs_adelic_int_Abs_adelic_int_Abs_adelic_int x y z) thus ?thesis
      using global_p_depth_p_adic_prod.global_depth_set_add[of x]
            global_p_depth_p_adic_prod.global_depth_set_add[of y]
      by    (simp add: plus_adelic_int_abs_eq add.assoc)
  qed

  show "a * b * c = a * (b * c)"
  proof (cases a b c rule: three_Abs_adelic_int_cases)
    case (Abs_adelic_int_Abs_adelic_int_Abs_adelic_int x y z) thus "a * b * c = a * (b * c)"
      using global_p_depth_p_adic_prod.global_depth_set_times[of 0 x]
            global_p_depth_p_adic_prod.global_depth_set_times[of 0 y]
      by    (simp add: times_adelic_int_abs_eq mult.assoc)
  qed

  show "(a + b) * c = a * c + b * c"
  proof (cases a b c rule: three_Abs_adelic_int_cases)
    case (Abs_adelic_int_Abs_adelic_int_Abs_adelic_int x y z) thus "(a + b) * c = a * c + b * c"
      using global_p_depth_p_adic_prod.global_depth_set_add[of x]
            global_p_depth_p_adic_prod.global_depth_set_times[of 0 x]
            global_p_depth_p_adic_prod.global_depth_set_times[of 0 y]
      by    (simp add: plus_adelic_int_abs_eq times_adelic_int_abs_eq distrib_right)
  qed

  show "(0::'a adelic_int) ≠ 1"
    using     Abs_adelic_int_inject[of "0::'a p_adic_prod" 1]
              global_p_depth_p_adic_prod.global_depth_set_0
              global_p_depth_p_adic_prod.global_depth_set_1
    unfolding zero_adelic_int_def one_adelic_int_def
    by        auto

qed

end (* instantiation adelic_int :: comm_ring *)

lemma pow_adelic_int_rep_eq: "Rep_adelic_int (x ^ n) = (Rep_adelic_int x) ^ n"
  by (induct n, simp_all add: one_adelic_int_rep_eq times_adelic_int_rep_eq)

lemma pow_adelic_int_abs_eq:
  "(Abs_adelic_int x) ^ n = Abs_adelic_int (x ^ n)" if "x ∈ 𝒪∀p"
  using that global_p_depth_p_adic_prod.global_depth_set_0_pow times_adelic_int_abs_eq
  by    (induct n, simp add: one_adelic_int_def, fastforce)


subsubsection ‹Equivalence and depth relative to a prime›

overloading
  p_equal_adelic_int ≡
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒
      'a adelic_int ⇒ 'a adelic_int ⇒ bool"
  p_restrict_adelic_int ≡
    "p_restrict :: 'a adelic_int ⇒
      ('a prime ⇒ bool) ⇒ 'a adelic_int"
  p_depth_adelic_int ≡
    "p_depth :: 'a::nontrivial_factorial_idom prime ⇒ 'a adelic_int ⇒ int"
  global_unfrmzr_pows_adelic_int ≡
    "global_unfrmzr_pows :: ('a prime ⇒ nat) ⇒ 'a adelic_int"
begin

definition p_equal_adelic_int ::
  "'a::nontrivial_factorial_idom prime ⇒
    'a adelic_int ⇒ 'a adelic_int ⇒ bool"
  where "p_equal_adelic_int p x y ≡ (Rep_adelic_int x) ≃⇩p (Rep_adelic_int y)"

definition p_restrict_adelic_int ::
  "'a::nontrivial_factorial_idom adelic_int ⇒
    ('a prime ⇒ bool) ⇒ 'a adelic_int"
  where
    "p_restrict_adelic_int x P ≡ Abs_adelic_int ((Rep_adelic_int x) prestrict P)"

definition p_depth_adelic_int ::
  "'a::nontrivial_factorial_idom prime ⇒ 'a adelic_int ⇒ int"
  where "p_depth_adelic_int p x ≡ ((Rep_adelic_int x)°⇧p)"

definition global_unfrmzr_pows_adelic_int ::
  "('a::nontrivial_factorial_idom prime ⇒ nat) ⇒ 'a adelic_int"
  where
    "global_unfrmzr_pows_adelic_int f ≡ Abs_adelic_int (global_unfrmzr_pows (int ∘ f))"

end  (* overloading *)

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma p_equal_adelic_int_abs_eq:
  "(Abs_adelic_int x) ≃⇩p (Abs_adelic_int y) ⟷
    x ≃⇩p y"
  if  "x ∈ 𝒪∀p"
  and "y ∈ 𝒪∀p"
  for x y :: "'a p_adic_prod"
  using that
  by    (simp add: p_equal_adelic_int_def Abs_adelic_int_inverse)

lemma p_equal_adelic_int_abs_eq0:
  "(Abs_adelic_int x) ≃⇩p 0 ⟷ x ≃⇩p 0"
  if "x ∈ 𝒪∀p" for x :: "'a p_adic_prod"
  using     that p_equal_adelic_int_abs_eq global_p_depth_p_adic_prod.global_depth_set_0
  unfolding zero_adelic_int_def
  by        auto

lemma p_equal_adelic_int_rep_eq0:
  "(Rep_adelic_int x) ≃⇩p 0 ⟷ x ≃⇩p 0"
  for x :: "'a adelic_int"
  using p_equal_adelic_int_def zero_adelic_int_rep_eq by metis

lemma p_equal_adelic_int_abs_eq1:
  "(Abs_adelic_int x) ≃⇩p 1 ⟷ x ≃⇩p 1"
  if "x ∈ 𝒪∀p" for x :: "'a p_adic_prod"
  using     that p_equal_adelic_int_abs_eq global_p_depth_p_adic_prod.global_depth_set_1
  unfolding one_adelic_int_def
  by        auto

lemma p_depth_adelic_int_abs_eq:
  "(Abs_adelic_int x)°⇧p = (x°⇧p)"
  if "x ∈ 𝒪∀p" for x :: "'a p_adic_prod"
  using that by (simp add: p_depth_adelic_int_def Abs_adelic_int_inverse)

lemma adelic_int_depth: "(x°⇧p) ≥ 0" for x :: "'a adelic_int"
  using global_p_depth_p_adic_prod.nonpos_global_depth_setD p_depth_adelic_int_abs_eq
  by    (cases x) auto

end (* context nontrivial_factorial_idom *)

lemma p_restrict_adelic_int_rep_eq:
  "Rep_adelic_int (x prestrict P) = (Rep_adelic_int x) prestrict P"
  for x :: "'a::nontrivial_factorial_idom adelic_int"
  and P :: "'a prime ⇒ bool"
  using     Rep_adelic_int global_p_depth_p_adic_prod.global_depth_set_p_restrict
            Abs_adelic_int_inverse
  unfolding p_restrict_adelic_int_def
  by        fastforce

lemma p_restrict_adelic_int_abs_eq:
  "(Abs_adelic_int x) prestrict P = Abs_adelic_int (x prestrict P)"
  if "x ∈ 𝒪∀p"
  for x :: "'a::nontrivial_factorial_idom p_adic_prod" and P :: "'a prime ⇒ bool"
  using that Abs_adelic_int_inverse' p_restrict_adelic_int_def by metis

lemma global_unfrmzr_pows_adelic_int_rep_eq:
  "Rep_adelic_int (𝔭 f :: 'a adelic_int) = 𝔭 (int ∘ f)"
  for f :: "'a::nontrivial_factorial_idom prime ⇒ nat"
  using global_unfrmzr_pows_p_adic_prod_global_depth_set_0 Abs_adelic_int_inverse'
        global_unfrmzr_pows_adelic_int_def
  by    metis

global_interpretation p_equality_adelic_int:
  p_equality_no_zero_divisors_1
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒
      'a adelic_int ⇒ 'a adelic_int ⇒ bool"
proof

  fix p :: "'a prime"

  show "equivp (p_equal p :: 'a adelic_int ⇒ 'a adelic_int ⇒ bool)"
    using equivp_transfer p_equality_p_adic_prod.equivp unfolding p_equal_adelic_int_def by fast

  fix x y :: "'a adelic_int"

  show "(x ≃⇩p y) = (x - y ≃⇩p 0)"
    using p_equality_p_adic_prod.conv_0
    by    (simp add: p_equal_adelic_int_def minus_adelic_int_rep_eq zero_adelic_int_rep_eq)

  show "y ≃⇩p 0 ⟹ x * y ≃⇩p 0"
    using p_equality_p_adic_prod.mult_0_right
    by    (simp add: p_equal_adelic_int_def times_adelic_int_rep_eq zero_adelic_int_rep_eq)

  have "(1::'a adelic_int) ¬≃⇩p 0"
    unfolding p_equal_adelic_int_def
    by        (metis
                zero_adelic_int_rep_eq one_adelic_int_rep_eq
                p_equality_p_adic_prod.one_p_nequal_zero
              )
  thus "∃x::'a adelic_int. x ¬≃⇩p 0" by blast

  assume "x ¬≃⇩p 0" and "y ¬≃⇩p 0"
  thus "x * y ¬≃⇩p 0"
    using p_equality_p_adic_prod.no_zero_divisors
    by    (simp add: p_equal_adelic_int_def times_adelic_int_rep_eq zero_adelic_int_rep_eq)

qed

overloading
  globally_p_equal_adelic_int ≡
    "globally_p_equal ::
      'a::nontrivial_factorial_idom adelic_int ⇒ 'a adelic_int ⇒ bool"
begin

definition globally_p_equal_adelic_int ::
  "'a::nontrivial_factorial_idom adelic_int ⇒ 'a adelic_int ⇒ bool"
  where globally_p_equal_adelic_int_def[simp]:
    "globally_p_equal_adelic_int = p_equality_adelic_int.globally_p_equal"

end  (* overloading *)

global_interpretation global_p_depth_adelic_int:
  global_p_equal_depth_no_zero_divisors_w_inj_index_consts
    "p_equal :: 'a::nontrivial_factorial_idom prime ⇒
      'a adelic_int ⇒ 'a adelic_int ⇒ bool"
    "p_restrict ::
      'a adelic_int ⇒ ('a prime ⇒ bool) ⇒ 'a adelic_int"
    "p_depth :: 'a prime ⇒ 'a adelic_int ⇒ int"
    "λf. Abs_adelic_int (p_adic_prod_consts f)"
    Rep_prime
proof (unfold_locales, fold globally_p_equal_adelic_int_def)

  fix p :: "'a prime"

  fix x y :: "'a adelic_int"

  show "x ≃∀p y ⟹ x = y"
    by (
      cases x, cases y,
      use p_equal_adelic_int_abs_eq global_p_depth_p_adic_prod.global_imp_eq in fastforce
    )

  fix P :: "'a prime ⇒ bool"
  show  "P p ⟹ x prestrict P ≃⇩p x"
    by (
      cases x,
      metis global_depth_set_p_adic_prod_def p_restrict_adelic_int_abs_eq p_equal_adelic_int_abs_eq
            global_p_depth_p_adic_prod.global_depth_set_p_restrict
            global_p_depth_p_adic_prod.p_restrict_equiv
    )
  show "¬ P p ⟹ x prestrict P ≃⇩p 0"
    by (
      cases x,
      metis global_depth_set_p_adic_prod_def p_restrict_adelic_int_abs_eq p_equal_adelic_int_abs_eq0
            global_p_depth_p_adic_prod.global_depth_set_p_restrict
            global_p_depth_p_adic_prod.p_restrict_equiv0
    )

  show "((0::'a adelic_int)°⇧p) = 0"
    using global_p_depth_p_adic_prod.depth_of_0
    by    (simp add: p_depth_adelic_int_def zero_adelic_int_rep_eq)

  show "x ≃⇩p y ⟹ (x°⇧p) = (y°⇧p)"
    using global_p_depth_p_adic_prod.depth_equiv
    by    (simp add: p_equal_adelic_int_def p_depth_adelic_int_def)

  show "(- x°⇧p) = (x°⇧p)"
    using global_p_depth_p_adic_prod.depth_uminus
    by    (simp add: p_depth_adelic_int_def uminus_adelic_int_rep_eq)

  show
    "x ¬≃⇩p 0 ⟹
      (x°⇧p) < (y°⇧p) ⟹
      ((x + y)°⇧p) = (x°⇧p)"
    using global_p_depth_p_adic_prod.depth_pre_nonarch(1)
    by    (
            simp add: p_equal_adelic_int_def p_depth_adelic_int_def zero_adelic_int_rep_eq
                      plus_adelic_int_rep_eq
          )

  show
    "⟦
      x ¬≃⇩p 0;
      (x + y) ¬≃⇩p 0;
      (x°⇧p) = (y°⇧p)
    ⟧ ⟹ (x + y°⇧p) ≥ (x°⇧p)"
    using global_p_depth_p_adic_prod.depth_pre_nonarch(2)
    by    (
            fastforce
            simp add: p_equal_adelic_int_def p_depth_adelic_int_def zero_adelic_int_rep_eq
                      plus_adelic_int_rep_eq
          )

  show
    "(x * y) ¬≃⇩p 0 ⟹
       (x * y°⇧p) = (x°⇧p) + (y°⇧p)"
    using global_p_depth_p_adic_prod.depth_mult_additive
    by    (
            simp add: p_equal_adelic_int_def p_depth_adelic_int_def zero_adelic_int_rep_eq
                      times_adelic_int_rep_eq
          )

  show "Abs_adelic_int (p_adic_prod_consts 1) = 1"
    by (metis global_p_depth_p_adic_prod.consts_1 one_adelic_int_def)

  fix f g :: "'a prime ⇒ 'a"

  show
    "Abs_adelic_int (p_adic_prod_consts (f - g)) =
      Abs_adelic_int (p_adic_prod_consts f) - Abs_adelic_int (p_adic_prod_consts g)"
    by (
      metis global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.consts_diff
            global_p_depth_p_adic_prod.global_depth_set_consts minus_adelic_int_abs_eq
    )

  show
    "Abs_adelic_int (p_adic_prod_consts (f * g)) =
      Abs_adelic_int (p_adic_prod_consts f) * Abs_adelic_int (p_adic_prod_consts g)"
    by (
      metis global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.consts_mult
            global_p_depth_p_adic_prod.global_depth_set_consts times_adelic_int_abs_eq
    )

  show "(Abs_adelic_int (p_adic_prod_consts f) ≃⇩p 0) = (f p = 0)"
    by (
      metis global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.global_depth_set_consts
            p_equal_adelic_int_abs_eq0 global_p_depth_p_adic_prod.p_equal_func_of_consts_0
    )

  show "(Abs_adelic_int (p_adic_prod_consts f)°⇧p) = int (pmultiplicity p (f p))"
    by (
      metis global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.global_depth_set_consts
            p_depth_adelic_int_abs_eq global_p_depth_p_adic_prod.p_depth_func_of_consts
    )

qed
(
  metis Rep_prime_inject injI, rule Rep_prime_n0, rule Rep_prime_not_unit,
  rule multiplicity_distinct_primes
)

lemma p_depth_adelic_int_diff_abs_eq:
  "((Abs_adelic_int x - Abs_adelic_int y)°⇧p) = ((x - y)°⇧p)"
  if "x ∈ 𝒪∀p" and "y ∈ 𝒪∀p"
  for p :: "'a::nontrivial_factorial_idom prime" and x y :: "'a p_adic_prod"
  using that global_depth_set_p_adic_prod_def minus_adelic_int_abs_eq p_depth_adelic_int_abs_eq
        global_p_depth_p_adic_prod.global_depth_set_minus
  by    metis

lemma p_depth_adelic_int_diff_abs_eq':
  "((Abs_adelic_int (abs_p_adic_prod X) - Abs_adelic_int (abs_p_adic_prod Y))°⇧p) =
    ((X - Y)°⇧p)"
  if X: "X ∈ 𝒪∀p" and Y: "Y ∈ 𝒪∀p"
  for p :: "'a::nontrivial_factorial_idom prime" and X Y :: "'a fls_pseq"
proof-
  have "abs_p_adic_prod X ∈ 𝒪∀p"
    by (
      simp, intro global_p_depth_p_adic_prod.global_depth_setI,
      metis X p_equal_p_adic_prod_abs_eq0 p_equality_depth_fls_pseq.global_depth_setD
            global_depth_set_fls_pseq_def p_depth_p_adic_prod.abs_eq
    )
  moreover have "abs_p_adic_prod Y ∈ 𝒪∀p"
    by (
      simp, intro global_p_depth_p_adic_prod.global_depth_setI,
      metis Y p_equal_p_adic_prod_abs_eq0 p_equality_depth_fls_pseq.global_depth_setD
            global_depth_set_fls_pseq_def p_depth_p_adic_prod.abs_eq
    )
  ultimately show ?thesis by (metis p_depth_adelic_int_diff_abs_eq p_depth_p_adic_prod_diff_abs_eq)
qed

context
  fixes p :: "'a::nontrivial_euclidean_ring_cancel prime"
begin

lemma adelic_int_diff_depth_gt_equiv_trans:
  "((a - c)°⇧p) > n"
  if  "a ≃⇩p b" and "b ¬≃⇩p c" and "((b - c)°⇧p) > n"
  for a b c :: "'a adelic_int"
  by (
    cases a, cases b, cases c,
    metis that p_depth_adelic_int_diff_abs_eq p_equal_adelic_int_abs_eq
          p_adic_prod_diff_depth_gt_equiv_trans
  )

lemma adelic_int_diff_depth_gt0_equiv_trans:
  "((a - c)°⇧p) > n"
  if "n ≥ 0" and "a ≃⇩p b" and "((b - c)°⇧p) > n"
  for a b c :: "'a adelic_int"
  using that p_equality_adelic_int.conv_0 adelic_int_diff_depth_gt_equiv_trans
        global_p_depth_adelic_int.depth_equiv_0[of p "b - c"]
  by    fastforce

lemma adelic_int_diff_depth_gt_trans:
  "((a - c)°⇧p) > n"
  if  "a ¬≃⇩p b" and "((a - b)°⇧p) > n"
  and "b ¬≃⇩p c" and "((b - c)°⇧p) > n"
  and "a ¬≃⇩p c"
  for a b c :: "'a adelic_int"
  by (
    cases a, cases b, cases c,
    metis that p_depth_adelic_int_diff_abs_eq p_equal_adelic_int_abs_eq
          p_adic_prod_diff_depth_gt_trans
  )

lemma adelic_int_diff_depth_gt0_trans:
  "((a - c)°⇧p) > n"
  if  "n ≥ 0"
  and "((a - b)°⇧p) > n"
  and "((b - c)°⇧p) > n"
  and "a ¬≃⇩p c"
  for a b c :: "'a adelic_int"
  using that adelic_int_diff_depth_gt_trans
        p_equality_adelic_int.conv_0[of p a b] p_equality_adelic_int.conv_0[of p b c]
        global_p_depth_adelic_int.depth_equiv_0[of p "a - b"]
        global_p_depth_adelic_int.depth_equiv_0[of p "b - c"]
  by    auto

lemma adelic_int_prestrict_zero_depth:
  "1 ≤ ((x prestrict (λp::'a prime. (x°⇧p) = 0) - x)°⇧p)"
  if "x prestrict (λp::'a prime. (x°⇧p) = 0) ¬≃⇩p x"
  for x :: "'a adelic_int"
  using that adelic_int_depth[of p x] global_p_depth_adelic_int.depth_equiv[of p]
        global_p_depth_adelic_int.p_restrict_equiv[of "λp. (x°⇧p) = 0"]
        global_p_depth_adelic_int.p_restrict_equiv0[of "λp. (x°⇧p) = 0" p x]
        p_equality_adelic_int.minus_right[of p _ _ x] global_p_depth_adelic_int.depth_uminus[of p x]
  by    force

end (* context nontrivial_euclidean_ring_cancel *)

lemma adelic_int_normalize_depth:
  "(x * 𝔭 (λp::'a prime. -(x°⇧p))) ∈ 𝒪∀p"
  for x :: "'a::nontrivial_factorial_idom p_adic_prod"
  using p_adic_prod_normalize_depth[of _ x] by (fastforce intro: p_adic_prod_global_depth_setI')

lemma global_unfrmzr_pows0_adelic_int:
  "(𝔭 (0 :: 'a::nontrivial_factorial_idom prime ⇒ nat) :: 'a adelic_int) = 1"
proof-
  have "int ∘ (0 :: 'a prime ⇒ nat) = (0 :: 'a prime ⇒ int)" by auto
  thus ?thesis
    using     global_unfrmzr_pows_p_adic_prod0
    unfolding global_unfrmzr_pows_adelic_int_def one_adelic_int_def
    by        metis
qed

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma global_unfrmzr_pows_adelic_int:
  "(𝔭 f :: 'a adelic_int)°⇧p = int (f p)" for f :: "'a prime ⇒ nat"
  using     global_unfrmzr_pows_p_adic_prod_global_depth_set_0 p_depth_adelic_int_abs_eq[of _ p]
            global_unfrmzr_pows_p_adic_prod[of p]
  unfolding global_unfrmzr_pows_adelic_int_def
  by        fastforce

lemma global_unfrmzr_pows_adelic_int_pequiv_iff:
  "((𝔭 f :: 'a adelic_int) ≃⇩p (𝔭 g)) = (f p = g p)"
  for f g :: "'a prime ⇒ nat"
proof-
  have "((int ∘ f) p = (int ∘ g) p) = (f p = g p)" by fastforce
  thus ?thesis
    using     global_unfrmzr_pows_p_adic_prod_global_depth_set_0 p_equal_adelic_int_abs_eq
              global_unfrmzr_pows_p_adic_prod_pequiv_iff
    unfolding global_unfrmzr_pows_adelic_int_def
    by        blast
qed

end (* context nontrivial_factorial_idom *)

lemma global_unfrmzr_pows_prod_adelic_int:
  "(𝔭 f :: 'a adelic_int) * (𝔭 g) = 𝔭 (f + g)"
  for f g :: "'a::nontrivial_factorial_idom prime ⇒ nat"
proof-
  have "(int ∘ f) + (int ∘ g) = int ∘ (f + g)" by fastforce
  thus ?thesis
    using     global_unfrmzr_pows_p_adic_prod_global_depth_set_0 times_adelic_int_abs_eq
              global_unfrmzr_pows_prod_p_adic_prod
    unfolding global_unfrmzr_pows_adelic_int_def
    by        metis
qed

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma global_unfrmzr_pows_adelic_int_nzero:
  "(𝔭 f :: 'a adelic_int) ¬≃⇩p 0" for f :: "'a prime ⇒ nat"
  using     global_unfrmzr_pows_p_adic_prod_global_depth_set_0 p_equal_adelic_int_abs_eq0
            global_unfrmzr_pows_p_adic_prod_nzero
  unfolding global_unfrmzr_pows_adelic_int_def
  by        blast

lemma prod_w_global_unfrmzr_pows_adelic_int:
  "(x * 𝔭 f)°⇧p = (x°⇧p) + int (f p)"
  if  "x ¬≃⇩p 0" for f :: "'a prime ⇒ nat" and x :: "'a adelic_int"
proof (cases x)
  case (Abs_adelic_int a)
  moreover have "(λx. int (f x)) = int ∘ f" by auto
  moreover from that Abs_adelic_int have "a ¬≃⇩p 0"
    using p_equal_adelic_int_abs_eq0[of a p] by blast
  ultimately have
    "((x * 𝔭 f)°⇧p) =
      (a°⇧p) + int (f p)"
    using     that times_adelic_int_abs_eq global_unfrmzr_pows_p_adic_prod_global_depth_set_0
              p_depth_adelic_int_abs_eq global_depth_set_p_adic_prod_def
              global_p_depth_p_adic_prod.global_depth_set_times[of 0 _ "𝔭 (int ∘ f)"]
              prod_w_global_unfrmzr_pows_p_adic_prod[of p a f]
    unfolding global_unfrmzr_pows_adelic_int_def
    by        fastforce
  with Abs_adelic_int show ?thesis using p_depth_adelic_int_abs_eq by fastforce
qed

lemma trivial_global_unfrmzr_pows_adelic_int:
  "(𝔭 f :: 'a adelic_int) ≃⇩p 1" if "f p = 0" for f :: "'a prime ⇒ nat"
  using     that p_equal_adelic_int_abs_eq1 global_unfrmzr_pows_p_adic_prod_global_depth_set_0
            trivial_global_unfrmzr_pows_p_adic_prod[of _ p]
  unfolding global_unfrmzr_pows_adelic_int_def
  by        force

lemma prod_w_trivial_global_unfrmzr_pows_adelic_int:
  "x * 𝔭 f ≃⇩p x" if "f p = 0"
  for f :: "'a prime ⇒ nat" and x :: "'a adelic_int"
  using that p_equality_adelic_int.mult_one_right trivial_global_unfrmzr_pows_adelic_int by blast

end (* context nontrivial_factorial_idom *)

lemma pow_global_unfrmzr_pows_adelic_int:
  "(𝔭 f :: 'a adelic_int) ^ n = (𝔭 ((λp. n) * f))"
  for f :: "'a::nontrivial_factorial_idom prime ⇒ nat"
proof-
  have "(λp. int n * (int ∘ f) p) = int ∘ ((λp. n) * f)" by auto
  thus ?thesis
    using     global_unfrmzr_pows_p_adic_prod_global_depth_set_0 pow_adelic_int_abs_eq
              global_unfrmzr_pows_p_adic_prod_pow
    unfolding global_unfrmzr_pows_adelic_int_def
    by        metis
qed

abbreviation "adelic_int_consts ≡ global_p_depth_adelic_int.consts"
abbreviation "adelic_int_const  ≡ global_p_depth_adelic_int.const"

lemma adelic_int_p_depth_consts:
  "(adelic_int_consts f)°⇧p = ((f p)°⇧p)"
  for p :: "'a::nontrivial_factorial_idom prime" and f :: "'a prime ⇒ 'a"
  using global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.global_depth_set_consts
        p_depth_adelic_int_abs_eq p_depth_p_adic_prod_consts
  by    metis

lemmas adelic_int_p_depth_const = adelic_int_p_depth_consts[of _ "λp. _"]

lemma adelic_int_global_unfrmzr:
  "(𝔭 (1 :: 'a::nontrivial_factorial_idom prime ⇒ nat) :: 'a adelic_int)
    = adelic_int_consts Rep_prime"
proof-
  define natfun_1 :: "'a prime ⇒ nat" and intfun_1 :: "'a prime ⇒ int"
    where "natfun_1 ≡ 1" and "intfun_1 ≡ 1"
  moreover from this have "int ∘ natfun_1 = intfun_1" by auto
  ultimately show ?thesis
    using p_adic_prod_global_unfrmzr unfolding global_unfrmzr_pows_adelic_int_def by metis
qed

lemma adelic_int_normalize_depthE:
  fixes   x :: "'a::nontrivial_factorial_idom adelic_int"
  obtains x_0
  where   "∀p::'a prime. x_0°⇧p = 0"
  and     "x = x_0 * 𝔭 (λp::'a prime. nat (x°⇧p))"
proof (cases x)
  define f :: "'a prime ⇒ nat"
    where "f ≡ λp::'a prime. nat (x°⇧p)"
  case (Abs_adelic_int a)
  obtain a_0 where a_0:
    "∀p::'a prime. a_0°⇧p = 0"
    "a = a_0 * 𝔭 (λp::'a prime. (a°⇧p))"
    by (elim p_adic_prod_normalize_depthE)
  from a_0(1) have a_0_int: "a_0 ∈ 𝒪∀p"
    using p_adic_prod_global_depth_setI'[of 0 a_0] by auto
  moreover from f_def Abs_adelic_int
    have  "(λp::'a prime. (a°⇧p)) = int ∘ f"
    using p_depth_adelic_int_abs_eq adelic_int_depth
    by    fastforce
  ultimately have "x = Abs_adelic_int a_0 * 𝔭 f"
    using f_def Abs_adelic_int(1) a_0(2) times_adelic_int_abs_eq
          global_unfrmzr_pows_p_adic_prod_global_depth_set[of 0 "int ∘ f"]
          global_unfrmzr_pows_adelic_int_def[of f]
    by    fastforce
  moreover from a_0(1) have "∀p::'a prime. (Abs_adelic_int (a_0))°⇧p = 0"
    using a_0_int p_depth_adelic_int_abs_eq by metis
  ultimately show thesis using that f_def by presburger
qed


subsubsection ‹Inverses›

text ‹We can create inverses at depth-zero places.›

instantiation adelic_int ::
  (nontrivial_factorial_unique_euclidean_bezout) "{divide_trivial, inverse}"
begin

definition inverse_adelic_int ::
  "'a adelic_int ⇒ 'a adelic_int"
  where
    "inverse_adelic_int x =
      Abs_adelic_int (
        (inverse (Rep_adelic_int x)) prestrict (λp::'a prime. x°⇧p = 0)
      )"

definition divide_adelic_int ::
  "'a adelic_int ⇒ 'a adelic_int ⇒ 'a adelic_int"
  where divide_adelic_int_def[simp]: "divide_adelic_int x y = x * inverse y"

instance
proof
  fix x :: "'a adelic_int"
  have "(λp::'a prime. (0::'a adelic_int)°⇧p = 0) = (λp. True)"
    using global_p_depth_adelic_int.depth_of_0 by fast
  hence "x div 0 = x * Abs_adelic_int (0 prestrict (λp::'a prime. True))"
    using     inverse_adelic_int_def[of 0]
    unfolding zero_adelic_int_rep_eq p_adic_prod_div_inv.inverse_0
    by        simp
  thus "x div 0 = 0"
    by (metis global_p_depth_p_adic_prod.p_restrict_true mult_zero_right zero_adelic_int_def)
  have "(λp::'a prime. (1::'a adelic_int)°⇧p = 0) = (λp. True)"
    using global_p_depth_adelic_int.p_depth_1 by fast
  hence "x div 1 = x * Abs_adelic_int (1 prestrict (λp::'a prime. True))"
    using     inverse_adelic_int_def[of 1]
    unfolding one_adelic_int_rep_eq p_adic_prod_div_inv.inverse_1
    by        simp
  thus "x div 1 = x"
    by (metis global_p_depth_p_adic_prod.p_restrict_true mult_1_right one_adelic_int_def)
qed simp

end

lemma inverse_adelic_int_abs_eq:
  "inverse (Abs_adelic_int x) =
    Abs_adelic_int (inverse x prestrict (λp::'a prime. x°⇧p = 0))"
  if  "x ∈ 𝒪∀p"
  for x :: "'a::nontrivial_factorial_unique_euclidean_bezout p_adic_prod"
  using     that Abs_adelic_int_inverse[of x] p_depth_adelic_int_abs_eq[of x]
  unfolding inverse_adelic_int_def
  by        auto

lemma divide_adelic_int_abs_eq:
  "Abs_adelic_int x / Abs_adelic_int y =
      Abs_adelic_int ((x / y) prestrict (λp::'a prime. y°⇧p = 0))"
  if "x ∈ 𝒪∀p" and "y ∈ 𝒪∀p"
  for x y :: "'a::nontrivial_factorial_unique_euclidean_bezout p_adic_prod"
  using that divide_adelic_int_def inverse_adelic_int_abs_eq global_depth_set_p_adic_prod_def
        p_adic_prod_div_inv.global_depth_set_inverse times_adelic_int_abs_eq
        global_p_depth_p_adic_prod.times_p_restrict p_adic_prod_div_inv.divide_inverse
  by    metis

lemma p_depth_adelic_int_inverse_diff_abs_eq:
  "((inverse (Abs_adelic_int x) - inverse (Abs_adelic_int y))°⇧p) =
    ((inverse x - inverse y)°⇧p)"
  if  "x ∈ 𝒪∀p" "x°⇧p = 0"
  and "y ∈ 𝒪∀p" "y°⇧p = 0"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime" and x y :: "'a p_adic_prod"
  using that inverse_adelic_int_abs_eq p_adic_prod_div_inv.global_depth_set_inverse
        p_depth_adelic_int_diff_abs_eq[of
          "inverse x prestrict (λp::'a prime. (x°⇧p) = 0)"
        ]
        global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.depth_diff_equiv[of p]
        global_p_depth_p_adic_prod.p_restrict_equiv[of _ p]
  by    fastforce

context
  fixes x :: "'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
begin

lemma inverse_adelic_int_rep_eq:
  "Rep_adelic_int (inverse x) =
    (inverse (Rep_adelic_int x)) prestrict (λp::'a prime. x°⇧p = 0)"
  using     Rep_adelic_int p_adic_prod_div_inv.global_depth_set_inverse Abs_adelic_int_inverse
  unfolding inverse_adelic_int_def
  by        (auto simp add: p_depth_adelic_int_def)

lemma adelic_int_inverse_equiv0_iff:
  "inverse x ≃⇩p 0 ⟷
    (x ≃⇩p 0 ∨ (x°⇧p) ≠ 0)"
  for p :: "'a prime"
proof (cases x)
  case (Abs_adelic_int a)
  thus ?thesis
    using inverse_adelic_int_abs_eq[of a] p_adic_prod_div_inv.global_depth_set_inverse[of a]
          p_equal_adelic_int_abs_eq0[of _ p]
          global_p_depth_p_adic_prod.p_restrict_equiv0[of _ p "inverse a"]
          global_p_depth_p_adic_prod.p_restrict_equiv[of _ p "inverse a"]
          p_equality_p_adic_prod.trans0_iff[of p _ "inverse a"]
          p_adic_prod_div_inv.inverse_equiv0_iff[of p] p_depth_adelic_int_abs_eq[of a]
    by    auto
qed

lemma adelic_int_inverse_equiv0_iff':
  "inverse x ≃⇩p 0 ⟷
    (x ≃⇩p 0 ∨ (x°⇧p) ≥ 1)"
  for p :: "'a prime"
  using adelic_int_inverse_equiv0_iff adelic_int_depth[of p x] by force

end (* context nontrivial_factorial_unique_euclidean_bezout *)

lemma adelic_int_inverse_eq0_iff:
  "inverse x = 0 ⟷
    (∀p::'a prime. x°⇧p = 0 ⟶ x ≃⇩p 0)"
  for x :: "'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
proof (standard, clarify)
  fix p :: "'a prime" assume "inverse x = 0" "x°⇧p = 0" thus "x ≃⇩p 0"
    using adelic_int_inverse_equiv0_iff by fastforce
next
  assume x: "∀p::'a prime. x°⇧p = 0 ⟶ x ≃⇩p 0"
  show "inverse x = 0"
  proof (intro global_p_depth_adelic_int.global_imp_eq, standard)
    fix p :: "'a prime"
    from x show "inverse x ≃⇩p 0"
      using adelic_int_depth[of p x] adelic_int_inverse_equiv0_iff
      by    (cases "x°⇧p = 0", fast, fastforce)
  qed
qed

lemma divide_adelic_int_rep_eq:
  "Rep_adelic_int (x / y) =
    (Rep_adelic_int x / Rep_adelic_int y) prestrict (λp::'a prime. y°⇧p = 0)"
  for x y :: "'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
  using divide_adelic_int_def times_adelic_int_rep_eq inverse_adelic_int_rep_eq
        global_p_depth_p_adic_prod.times_p_restrict p_adic_prod_div_inv.divide_inverse
  by    metis

lemma adelic_int_divide_by_pequiv0:
  "x / y ≃⇩p 0" if "y ≃⇩p 0"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime" and x y :: "'a adelic_int"
  using that divide_adelic_int_def adelic_int_inverse_equiv0_iff p_equality_adelic_int.mult_0_right
  by    metis

lemma adelic_int_divide_by_pos_depth:
  "x / y ≃⇩p 0" if "(y°⇧p) > 0"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime" and x y :: "'a adelic_int"
  using that adelic_int_inverse_equiv0_iff p_equality_adelic_int.mult_0_right[of p] by force

lemma adelic_int_inverse0[simp]:
  "inverse (0::'a::nontrivial_factorial_unique_euclidean_bezout adelic_int) = 0"
  using adelic_int_inverse_eq0_iff by force

lemma adelic_int_inverse1[simp]:
  "inverse (1::'a::nontrivial_factorial_unique_euclidean_bezout adelic_int) = 1"
proof-
  have "(λp::'a prime. (1::'a p_adic_prod)°⇧p = 0) = (λp. True)"
    by simp
  thus ?thesis
    using global_depth_set_p_adic_prod_def one_adelic_int_def inverse_adelic_int_abs_eq
          global_p_depth_p_adic_prod.global_depth_set_1 p_adic_prod_div_inv.inverse_1
          global_p_depth_p_adic_prod.p_restrict_true
    by    metis
qed

lemma adelic_int_inverse_mult:
  "inverse (x * y) = inverse x * inverse y"
  for x y :: "'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
proof (
  intro global_p_depth_adelic_int.global_imp_eq, standard, cases x y rule: two_Abs_adelic_int_cases
)
  case (Abs_adelic_int_Abs_adelic_int a b)
  fix p :: "'a prime"
  define P :: "'a p_adic_prod ⇒ 'a prime ⇒ bool"
    where "P ≡ (λz p. z°⇧p = 0)"
  define iab iab' ia ib
    where "iab  ≡ inverse (a * b) prestrict (P (a * b))"
    and   "iab' ≡ inverse (a * b) prestrict (λp. P a p ∧ P b p)"
    and   "ia   ≡ inverse a prestrict (P a)"
    and   "ib   ≡ inverse b prestrict (P b)"
  from P_def Abs_adelic_int_Abs_adelic_int(2,4) have
    "P (a * b) p ⟹ inverse (a *b) ¬≃⇩p 0 ⟹
      P a p ∧ P b p"
    using p_adic_prod_div_inv.inverse_equiv0_iff global_p_depth_p_adic_prod.depth_mult_additive
          global_p_depth_p_adic_prod.nonpos_global_depth_setD[of 0 a p]
          global_p_depth_p_adic_prod.nonpos_global_depth_setD[of 0 b p]
          global_depth_set_p_adic_prod_def
    by    force
  moreover from P_def have
    "¬ P (a * b) p ⟹ P a p ⟹ P b p ⟹
      inverse (a * b) ≃⇩p 0"
    using global_p_depth_p_adic_prod.depth_mult_additive p_adic_prod_div_inv.inverse_equiv0_iff
    by    force
  ultimately have "iab ≃⇩p iab'"
    using     global_p_depth_p_adic_prod.p_restrict_p_equal_p_restrictI[of _ p]
    unfolding iab_def iab'_def
    by        force
  moreover from iab'_def ia_def ib_def have "iab' ≃⇩p ia * ib"
    using global_p_depth_p_adic_prod.p_restrict_times_equiv[of p _ "P a" _ "P b"]
          p_adic_prod_div_inv.inverse_mult p_equality_p_adic_prod.sym by metis
  ultimately have "iab ≃⇩p ia * ib" using p_equality_p_adic_prod.trans by metis
  with Abs_adelic_int_Abs_adelic_int P_def iab_def ia_def ib_def show
    "inverse (x * y) ≃⇩p
      (inverse x * inverse y)"
    using global_depth_set_p_adic_prod_def p_adic_prod_div_inv.global_depth_set_inverse
          global_p_depth_p_adic_prod.global_depth_set_times times_adelic_int_abs_eq
          p_equal_adelic_int_abs_eq[of
            "inverse (a * b) prestrict (P (a * b))"
            "(inverse a prestrict (P a)) * (inverse b prestrict (P b))"
          ]
          inverse_adelic_int_abs_eq[of a] inverse_adelic_int_abs_eq[of b]
          inverse_adelic_int_abs_eq[of "a * b"]
    by    fastforce
qed

lemma adelic_int_inverse_pcong:
  "(inverse x) ≃⇩p (inverse y)" if "x ≃⇩p y"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime" and x y :: "'a adelic_int"
proof (cases x y rule: two_Abs_adelic_int_cases)
  case (Abs_adelic_int_Abs_adelic_int a b)
  with that have "a ≃⇩p b" using p_equal_adelic_int_abs_eq by blast
  moreover define d :: "'a p_adic_prod ⇒ 'a prime ⇒ bool"
    where "d ≡ λz p. z°⇧p = 0"
  ultimately have "(inverse a prestrict (d a)) ≃⇩p (inverse b prestrict (d b))"
    by (
      auto
        intro   : global_p_depth_p_adic_prod.p_restrict_p_equal_p_restrictI
        simp add: p_adic_prod_div_inv.inverse_pcong global_p_depth_p_adic_prod.depth_equiv
    )
  with Abs_adelic_int_Abs_adelic_int d_def show ?thesis
    using inverse_adelic_int_abs_eq[of a] inverse_adelic_int_abs_eq[of b] p_equal_adelic_int_abs_eq
          p_adic_prod_div_inv.global_depth_set_inverse[of a]
          p_adic_prod_div_inv.global_depth_set_inverse[of b]
    by    auto
qed

context
  fixes x :: "'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
begin

lemma adelic_int_inverse_uminus: "inverse (-x) = - inverse x"
proof (cases x)
  case (Abs_adelic_int a) thus ?thesis
    using global_depth_set_p_adic_prod_def global_p_depth_p_adic_prod.global_depth_set_uminus[of a]
          uminus_adelic_int_abs_eq[of a] p_adic_prod_div_inv.inverse_uminus[of a]
          uminus_adelic_int_abs_eq[of "inverse a prestrict _"]
          p_adic_prod_div_inv.global_depth_set_inverse[of a]
          inverse_adelic_int_abs_eq[of "-a"] inverse_adelic_int_abs_eq[of a]
          global_p_depth_p_adic_prod.p_restrict_uminus[of "inverse a"]
          global_p_depth_p_adic_prod.depth_uminus[of _ a]
    by    fastforce
qed

lemma adelic_int_inverse_inverse:
  "inverse (inverse x) = x prestrict (λp::'a prime. x°⇧p = 0)"
proof (cases x)
  case (Abs_adelic_int a)
  moreover define P where "P ≡ (λp::'a prime. a°⇧p = 0)"
  moreover from this
    have  "(λp::'a prime. P p ∧ (inverse a prestrict P)°⇧p = 0) = P"
    using global_p_depth_p_adic_prod.p_restrict_depth[of P]
          p_adic_prod_div_inv.inverse_depth[of _ a]
    by    auto
  ultimately show ?thesis
    using inverse_adelic_int_abs_eq p_adic_prod_div_inv.global_depth_set_inverse[of a]
          p_adic_prod_div_inv.inverse_inverse[of a]
          inverse_adelic_int_abs_eq[of "inverse a prestrict P"] p_depth_adelic_int_abs_eq
          p_adic_prod_div_inv.inverse_p_restrict[of "inverse a" P] p_restrict_adelic_int_abs_eq
          global_p_depth_p_adic_prod.p_restrict_restrict[of a P]
    by    fastforce
qed

lemma adelic_int_inverse_pow: "inverse (x ^ n) = (inverse x) ^ n"
  by (induct n, simp_all add: adelic_int_inverse_mult)

lemma adelic_int_divide_self':
  "x / x ≃⇩p 1" if "x ¬≃⇩p 0" and "x°⇧p = 0"
  for p :: "'a prime"
proof (cases x)
  case (Abs_adelic_int a)
  define P :: "'a prime ⇒ bool"
    where "P ≡ (λp. (a°⇧p) = 0)"
  moreover from that Abs_adelic_int have "a ¬≃⇩p 0" "a°⇧p = 0"
    using that p_equal_adelic_int_abs_eq0 p_depth_adelic_int_abs_eq by (blast, fastforce)
  ultimately
    have  "Abs_adelic_int (a / a prestrict P) ≃⇩p (Abs_adelic_int 1)"
    using Abs_adelic_int(2) global_p_depth_p_adic_prod.p_restrict_equiv[of P p]
          p_adic_prod_div_inv.divide_right_equiv[of p _ a]
          p_adic_prod_div_inv.divide_self_equiv[of p] p_equality_p_adic_prod.trans[of p _ "a / a" 1]
          p_adic_prod_div_inv.divide_p_restrict_right[of a a]
          p_adic_prod_div_inv.global_depth_set_divide[of a 0]
          p_equal_adelic_int_abs_eq global_p_depth_p_adic_prod.global_depth_set_1
    by    fastforce
  with Abs_adelic_int P_def show ?thesis using divide_adelic_int_abs_eq one_adelic_int_def by metis
qed

lemma adelic_int_global_divide_self:
  "x / x = 1"
  if    "∀p::'a prime. x ¬≃⇩p 0"
  and   "∀p::'a prime. x°⇧p = 0"
  using that global_p_depth_adelic_int.global_imp_eq adelic_int_divide_self' by fastforce

lemma adelic_int_divide_self:
  "x / x =
    1 prestrict (λp::'a prime. x ¬≃⇩p 0 ∧ x°⇧p = 0)"
proof (intro global_p_depth_adelic_int.global_imp_eq, standard)
  define P :: "'a prime ⇒ bool"
    where "P ≡ (λp. x ¬≃⇩p 0 ∧ x°⇧p = 0)"
  fix p :: "'a prime" show "x / x ≃⇩p 1 prestrict P"
  proof (cases "P p")
    case True with P_def show ?thesis
      using p_equality_adelic_int.trans_left adelic_int_divide_self'[of p]
            global_p_depth_adelic_int.p_restrict_equiv[of _ p]
      by    force
  next
    case False
    moreover from this P_def have "x / x ≃⇩p 0"
      using divide_adelic_int_def adelic_int_inverse_equiv0_iff
            p_equality_adelic_int.mult_0_right
      by    metis
    ultimately show ?thesis
      using global_p_depth_adelic_int.p_restrict_equiv0 p_equality_adelic_int.trans_left by metis
  qed
qed

lemma adelic_int_p_restrict_inverse:
  "(inverse x) prestrict P = inverse (x prestrict P)" for P :: "'a prime ⇒ bool"
proof (cases x)
  case (Abs_adelic_int a)
  moreover have
    "(λp::'a prime. a°⇧p = 0 ∧ P p) =
      (λp::'a prime. P p ∧ (a prestrict P)°⇧p = 0)"
    using global_p_depth_p_adic_prod.p_restrict_equiv global_p_depth_p_adic_prod.depth_equiv
    by    metis
  ultimately show ?thesis
    using inverse_adelic_int_abs_eq[of a] inverse_adelic_int_abs_eq[of "a prestrict P"]
          p_adic_prod_div_inv.global_depth_set_inverse[of a] p_restrict_adelic_int_abs_eq[of _ P]
          p_adic_prod_div_inv.inverse_p_restrict[of a]
          global_p_depth_p_adic_prod.p_restrict_restrict[of "inverse a"]
          global_p_depth_p_adic_prod.global_depth_set_p_restrict[of a 0 P]
    by    force
qed

lemma adelic_int_inverse_depth: "(inverse x)°⇧p = 0" for p :: "'a prime"
proof (cases x)
  case (Abs_adelic_int X)
  hence
    "(inverse x)°⇧p =
      ((inverse X prestrict (λp::'a prime. X°⇧p = 0))°⇧p)"
    using inverse_adelic_int_abs_eq p_adic_prod_div_inv.global_depth_set_inverse
          p_depth_adelic_int_abs_eq
    by    fastforce
  thus ?thesis
    using global_p_depth_p_adic_prod.p_restrict_equiv[of _ p "inverse X"]
          global_p_depth_p_adic_prod.depth_equiv[of p _ "inverse X"]
          p_adic_prod_div_inv.inverse_depth[of p X] global_p_depth_p_adic_prod.depth_equiv_0[of p]
          global_p_depth_p_adic_prod.p_restrict_equiv0[of _ p "inverse X"]
    by    (cases "X°⇧p = 0", presburger, presburger)
qed

end (* context nontrivial_factorial_unique_euclidean_bezout *)

lemma adelic_int_consts_divide_self:
  "(adelic_int_consts f) / (adelic_int_consts f) =
    1 prestrict (λp::'a prime. f p ≠ 0 ∧ (f p)°⇧p = 0)"
  for f :: "'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒ 'a"
  using adelic_int_divide_self[of "adelic_int_consts f"] adelic_int_p_depth_consts[of _ f]
        global_p_depth_adelic_int.p_equal_func_of_consts_0[of _ f]
  by    presburger

lemma adelic_int_const_divide_self:
  "(adelic_int_const c) / (adelic_int_const c) =
    1 prestrict (λp::'a prime. c°⇧p = 0)"
  if "c ≠ 0" for c :: "'a::nontrivial_factorial_unique_euclidean_bezout"
  using that by (simp del: divide_adelic_int_def add: adelic_int_consts_divide_self)

lemma adelic_int_consts_divide_self':
  "(adelic_int_consts f) / (adelic_int_consts f) ≃⇩p 1"
  if "f p ≠ 0" and "(f p)°⇧p = 0"
  for f :: "'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒ 'a"
  using that adelic_int_consts_divide_self[of f] global_p_depth_adelic_int.p_restrict_equiv[of _ p]
  by    presburger

lemma adelic_int_divide_depth:
  "(x / y)°⇧p = (x°⇧p)" if "x / y ¬≃⇩p 0"
  for x y :: "'a::nontrivial_factorial_unique_euclidean_bezout adelic_int" and p :: "'a prime"
proof (cases x y rule: two_Abs_adelic_int_cases)
  case (Abs_adelic_int_Abs_adelic_int a b)
  from that Abs_adelic_int_Abs_adelic_int(3,4) have db: "b°⇧p = 0"
    using p_depth_adelic_int_abs_eq adelic_int_depth[of p y] adelic_int_divide_by_pos_depth[of p y]
    by    fastforce
  moreover have "a / b ¬≃⇩p 0"
  proof
    assume "a / b ≃⇩p 0" with that Abs_adelic_int_Abs_adelic_int db show False
      using global_p_depth_p_adic_prod.p_restrict_equiv[of _ p "a / b"]
            p_equality_p_adic_prod.trans[of p _ "a / b" 0]
            p_adic_prod_div_inv.global_depth_set_divide[of a 0 b]
            p_equal_adelic_int_abs_eq0 divide_adelic_int_abs_eq[of a b]
      by    force
  qed
  ultimately show "(x / y)°⇧p = (x°⇧p)"
    using Abs_adelic_int_Abs_adelic_int divide_adelic_int_abs_eq
          p_adic_prod_div_inv.global_depth_set_divide[of _ 0] p_depth_adelic_int_abs_eq[of _ p]
          p_adic_prod_div_inv.divide_depth[of p a b]
          global_p_depth_p_adic_prod.depth_equiv[of p _ "a / b"]
          global_p_depth_p_adic_prod.p_restrict_equiv[of _ p "a / b"]
    by    fastforce
qed

lemma global_unfrmzr_pows_adelic_int_inverse:
  "inverse (𝔭 f :: 'a adelic_int) = 1 prestrict (λp::'a prime. f p = 0)"
  for f :: "'a::nontrivial_factorial_unique_euclidean_bezout prime ⇒ nat"
proof (intro global_p_depth_adelic_int.global_imp_eq, standard)
  fix p :: "'a prime"
  define P :: "'a prime ⇒ bool" where "P ≡ (λp. f p = 0)"
  define  𝔭nif :: "'a p_adic_prod" and 𝔭f   :: "'a adelic_int"
    where "𝔭nif ≡ 𝔭 (- (int ∘ f))" and "𝔭f   ≡ 𝔭 f"
  from P_def 𝔭nif_def 𝔭f_def have "inverse 𝔭f = Abs_adelic_int (𝔭nif prestrict P)"
    using     global_unfrmzr_pows_p_adic_prod_global_depth_set_0[of f]
              inverse_adelic_int_abs_eq[of "𝔭 (int ∘ f)"]
              global_unfrmzr_pows_p_adic_prod[of _ "int ∘ f"]
              global_unfrmzr_pows_p_adic_prod_inverse[of "int ∘ f"]
    unfolding global_unfrmzr_pows_adelic_int_def
    by        fastforce
  moreover from P_def 𝔭nif_def have "𝔭nif prestrict P ≃⇩p 1 prestrict P"
    using global_p_depth_p_adic_prod.p_restrict_p_equal_p_restrict_by_sameI[of P p]
          trivial_global_unfrmzr_pows_p_adic_prod[of _ p]
    by    force
  moreover have "𝔭nif prestrict P ∈ 𝒪∀p"
  proof (intro p_adic_prod_global_depth_set_p_restrictI)
    fix p :: "'a prime" assume "P p"
    moreover from 𝔭nif_def have "𝔭nif ∈ p_depth_set p (- (int ∘ f) p)"
      using global_unfrmzr_pows_p_adic_prod_depth_set[of "- (int ∘ f)"] by simp
    ultimately show "𝔭nif ∈ 𝒪@⇩p" using P_def by fastforce
  qed
  ultimately show "(inverse 𝔭f) ≃⇩p (1 prestrict P)"
    using one_adelic_int_def global_p_depth_p_adic_prod.global_depth_set_1
          p_equal_adelic_int_abs_eq p_restrict_adelic_int_abs_eq global_depth_set_p_adic_prod_def
          global_p_depth_p_adic_prod.global_depth_set_p_restrict
    by    metis
qed

lemma adelic_int_diff_cancel_lead_coeff:
  "((inverse x - inverse y)°⇧p) > 0"
  if  x : "x ¬≃⇩p 0" "x°⇧p = 0"
  and y : "y ¬≃⇩p 0" "y°⇧p = 0"
  and xy: "x ¬≃⇩p y" "((x - y)°⇧p) > 0"
  for p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
  and x y :: "'a adelic_int"
proof (cases x y rule: two_Abs_adelic_int_cases)
  define P :: "'a p_adic_prod ⇒ 'a prime ⇒ bool"
    where "P ≡ λa p. a°⇧p = 0"
  case (Abs_adelic_int_Abs_adelic_int a b)
  moreover from this x(1) y(1) xy(1)
    have  "a ¬≃⇩p 0"
    and   "b ¬≃⇩p 0"
    and   "a ¬≃⇩p b"
    using p_equal_adelic_int_abs_eq0 p_equal_adelic_int_abs_eq
    by    (fast, fast, fast)
  moreover from Abs_adelic_int_Abs_adelic_int x(2) y(2) xy(2)
    have  "a°⇧p = 0"
    and   "b°⇧p = 0"
    and   "((a - b)°⇧p) > 0"
    by (
      metis p_depth_adelic_int_abs_eq, metis p_depth_adelic_int_abs_eq,
      metis p_depth_adelic_int_diff_abs_eq
    )
  ultimately show ?thesis
    using p_depth_adelic_int_inverse_diff_abs_eq p_adic_prod_diff_cancel_lead_coeff by fastforce
qed


subsubsection ‹The ideal of primes›

overloading
  p_depth_set_adelic_int ≡
    "p_depth_set ::
      'a::nontrivial_factorial_idom prime ⇒ int ⇒ 'a adelic_int set"
  global_depth_set_adelic_int ≡
    "global_depth_set :: int ⇒ 'a adelic_int set"
begin

definition p_depth_set_adelic_int ::
  "'a::nontrivial_factorial_idom prime ⇒ int ⇒ 'a adelic_int set"
  where p_depth_set_adelic_int_def[simp]:
    "p_depth_set_adelic_int = global_p_depth_adelic_int.p_depth_set"

definition global_depth_set_adelic_int ::
  "int ⇒ 'a::nontrivial_factorial_idom adelic_int set"
  where global_depth_set_adelic_int_def[simp]:
    "global_depth_set_adelic_int = global_p_depth_adelic_int.global_depth_set"

end

context
  fixes x :: "'a::nontrivial_factorial_idom adelic_int"
begin

lemma adelic_int_global_depth_setI:
  "x ∈ 𝒫∀p⇧n"
  if  "⋀p::'a prime. x ¬≃⇩p 0 ⟹ (x°⇧p) ≥ n"
  using that global_p_depth_adelic_int.global_depth_setI by auto

lemma adelic_int_global_depth_setI':
  "x ∈ 𝒫∀p⇧n"
  if  "⋀p::'a prime. (x°⇧p) ≥ n"
  using that global_p_depth_adelic_int.global_depth_setI' by auto

lemma adelic_int_global_depth_set_p_restrictI:
  "p_restrict x P ∈ 𝒫∀p⇧n"
  if "⋀p::'a prime. P p ⟹ x ∈ 𝒫@⇩p⇧n"
  using that global_p_depth_adelic_int.global_depth_set_p_restrictI by auto

end (* context nontrivial_factorial_idom *)

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
begin

lemma adelic_int_p_depth_setI:
  "x ∈ 𝒫@⇩p⇧n"
  if "x ¬≃⇩p 0 ⟶ (x°⇧p) ≥ n"
  for x :: "'a adelic_int"
  using that global_p_depth_adelic_int.p_depth_setI by auto

lemma nonpos_p_depth_set_adelic_int:
  "(𝒫@⇩p⇧n) = (UNIV :: 'a::nontrivial_factorial_idom adelic_int set)"
  if "n ≤ 0"
proof safe
  fix x :: "'a adelic_int" show "x ∈ (𝒫@⇩p⇧n)"
  proof (intro adelic_int_p_depth_setI, clarify)
    from that show "n ≤ (x°⇧p)"
      using adelic_int_depth[of p x] by fastforce
  qed
qed simp

lemma p_depth_set_adelic_int_eq_projection:
  "((𝒫@⇩p⇧n) :: 'a::nontrivial_factorial_idom adelic_int set) =
    Abs_adelic_int ` ((𝒫@⇩p⇧n) ∩ 𝒪∀p)"
proof safe
  fix x :: "'a adelic_int" assume "x ∈ 𝒫@⇩p⇧n"
  thus
    "x ∈
      Abs_adelic_int ` ((𝒫@⇩p⇧n) ∩ 𝒪∀p)"
    using p_equal_adelic_int_abs_eq0 global_p_depth_adelic_int.p_depth_setD
          p_depth_adelic_int_abs_eq p_adic_prod_p_depth_setI
    by    (cases x) fastforce
next
  fix a :: "'a p_adic_prod"
  assume "a ∈ 𝒫@⇩p⇧n" "a ∈ 𝒪∀p"
  thus "Abs_adelic_int a ∈ 𝒫@⇩p⇧n"
    using p_equal_adelic_int_abs_eq0 global_p_depth_p_adic_prod.p_depth_setD
          p_depth_adelic_int_abs_eq
    by    (fastforce intro: adelic_int_p_depth_setI)
qed

lemma lift_p_depth_set_adelic_int:
  "Rep_adelic_int `
    ((𝒫@⇩p⇧n) :: 'a::nontrivial_factorial_idom adelic_int set)
    = (𝒫@⇩p⇧n) ∩ 𝒪∀p"
proof-
  have
    "Rep_adelic_int ` Abs_adelic_int `
      ((𝒫@⇩p⇧n) ∩ 𝒪∀p)
      = (𝒫@⇩p⇧n) ∩ 𝒪∀p"
    using Abs_adelic_int_inverse by force
  thus ?thesis using p_depth_set_adelic_int_eq_projection by metis
qed

end (* context nontrivial_factorial_idom *)

lemma nonpos_global_depth_set_adelic_int:
  "(𝒫∀p⇧n) = (UNIV :: 'a::nontrivial_factorial_idom adelic_int set)"
  if "n ≤ 0"
  using that nonpos_p_depth_set_adelic_int global_p_depth_adelic_int.global_depth_set by fastforce

lemma nonneg_global_depth_set_adelic_int_eq_projection:
  "((𝒫∀p⇧n)  :: 'a::nontrivial_factorial_idom adelic_int set) =
    Abs_adelic_int ` 𝒫∀p⇧n"
  if n: "n ≥ 0"
proof safe
  fix x :: "'a adelic_int" assume x: "x ∈ 𝒫∀p⇧n"
  show "x ∈ Abs_adelic_int ` 𝒫∀p⇧n"
  proof (cases x)
    case (Abs_adelic_int a)
    moreover from this x have "a ∈ 𝒫∀p⇧n"
      using p_equal_adelic_int_abs_eq0 global_p_depth_adelic_int.global_depth_setD
            p_depth_adelic_int_abs_eq
      by    (fastforce intro: p_adic_prod_global_depth_setI)
    ultimately show ?thesis by fast
  qed
next
  fix a :: "'a p_adic_prod" assume "a ∈ 𝒫∀p⇧n"
  moreover from this n have "a ∈ 𝒪∀p"
    using global_p_depth_p_adic_prod.global_depth_set_antimono by auto
  ultimately show "Abs_adelic_int a ∈ 𝒫∀p⇧n"
    using n p_equal_adelic_int_abs_eq0 global_p_depth_p_adic_prod.global_depth_setD
          p_depth_adelic_int_abs_eq
    by    (fastforce intro: adelic_int_global_depth_setI)
qed

lemma lift_nonneg_global_depth_set_adelic_int:
  "Rep_adelic_int `
    ((𝒫∀p⇧n)  :: 'a::nontrivial_factorial_idom adelic_int set)
    = 𝒫∀p⇧n"
  if n: "n ≥ 0"
proof-
  from n have
    "Rep_adelic_int ` Abs_adelic_int `
      (𝒫∀p⇧n)
      = 𝒫∀p⇧n"
    using global_p_depth_p_adic_prod.global_depth_set_antimono Abs_adelic_int_inverse by force
  with n show ?thesis using nonneg_global_depth_set_adelic_int_eq_projection by metis
qed

subsubsection ‹Topology p-open neighbourhoods›

text ‹General properties of p-open sets›

abbreviation "adelic_int_p_open_nbhd         ≡ global_p_depth_adelic_int.p_open_nbhd"
abbreviation "adelic_int_p_open_nbhds        ≡ global_p_depth_adelic_int.p_open_nbhds"
abbreviation "adelic_int_local_p_open_nbhds  ≡ global_p_depth_adelic_int.local_p_open_nbhds"

lemma adelic_int_nonpos_p_open_nbhd:
  "adelic_int_p_open_nbhd p n x = UNIV" if "n ≤ 0"
  for p :: "'a::nontrivial_factorial_idom prime"
proof-
  from that have "adelic_int_p_open_nbhd p n x = adelic_int_p_open_nbhd p n 0"
    using global_p_depth_adelic_int.p_open_nbhd_eq_circle[of 0 p n]
          adelic_int_depth[of p x]
          global_p_depth_adelic_int.p_open_nbhd_circle_multicentre[of x 0 p n]
    by    simp
  moreover have "adelic_int_p_open_nbhd p n 0 = UNIV"
  proof safe
    fix y :: "'a adelic_int" from that show "y ∈ adelic_int_p_open_nbhd p n 0"
      using global_p_depth_adelic_int.p_open_nbhd_eq_circle[of 0 p n] adelic_int_depth[of p y]
      by    auto
  qed simp
  ultimately show ?thesis by presburger
qed

lemma adelic_int_p_open_nbhd_bound:
  "adelic_int_p_open_nbhd p n x = adelic_int_p_open_nbhd p (int (nat n)) x"
  using adelic_int_nonpos_p_open_nbhd[of n x p] adelic_int_nonpos_p_open_nbhd[of 0 x p] by simp

lemma adelic_int_p_open_nbhd_abs_eq:
  "adelic_int_p_open_nbhd p n (Abs_adelic_int x) =
    Abs_adelic_int ` (p_adic_prod_p_open_nbhd p n x ∩ 𝒪∀p)"
  if "x ∈ 𝒪∀p"
  for p :: "'a::nontrivial_factorial_idom prime"
proof safe
  fix y assume y: "y ∈ adelic_int_p_open_nbhd p n (Abs_adelic_int x)"
  show
    "y ∈ Abs_adelic_int ` (p_adic_prod_p_open_nbhd p n x ∩ 𝒪∀p)"
  proof (cases y)
    case (Abs_adelic_int z)
    with that y have "z ∈ p_adic_prod_p_open_nbhd p n x"
      using global_p_depth_adelic_int.p_open_nbhd_eq_circle p_equal_adelic_int_abs_eq[of z x p]
            p_depth_adelic_int_diff_abs_eq[of z x p]
            global_p_depth_p_adic_prod.p_open_nbhd_eq_circle
      by    fastforce
    with Abs_adelic_int show ?thesis by blast
  qed
next
  fix z assume z: "z ∈ p_adic_prod_p_open_nbhd p n x" "z ∈ 𝒪∀p"
  with that show "Abs_adelic_int z ∈ adelic_int_p_open_nbhd p n (Abs_adelic_int x)"
    using global_p_depth_adelic_int.p_open_nbhd_eq_circle p_equal_adelic_int_abs_eq[of z x p]
          p_depth_adelic_int_diff_abs_eq[of z x p] global_p_depth_p_adic_prod.p_open_nbhd_eq_circle
    by    fastforce
qed

lemma adelic_int_p_open_nbhd_rep_eq:
  "Rep_adelic_int ` adelic_int_p_open_nbhd p n x =
    p_adic_prod_p_open_nbhd p n (Rep_adelic_int x) ∩ 𝒪∀p"
  for p :: "'a::nontrivial_factorial_idom prime"
proof (cases x)
  case (Abs_adelic_int z)
  hence
    "Rep_adelic_int ` adelic_int_p_open_nbhd p n x =
      Rep_adelic_int ` Abs_adelic_int `
        (p_adic_prod_p_open_nbhd p n z ∩ 𝒪∀p)"
    using adelic_int_p_open_nbhd_abs_eq by metis
  also have "… = p_adic_prod_p_open_nbhd p n z ∩ 𝒪∀p"
    using Abs_adelic_int_inverse by force
  finally show ?thesis using Abs_adelic_int Abs_adelic_int_inverse by force
qed

lemma adelic_int_local_depth_ring_lift_cover:
  fixes n :: int
  and   p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
  and   𝒜 :: "'a adelic_int set set"
  defines
    "(𝒜' :: 'a p_adic_prod set set) ≡
      (λA.
        (λx. x prestrict ((=) p)) ` Rep_adelic_int ` A +
        range (λx. x prestrict ((≠) p))
      ) ` 𝒜"
  assumes nonneg: "n ≥ 0"
    and   cover:
    "(λx. x prestrict ((=) p)) ` (𝒫∀p⇧n) ⊆
      ⋃ 𝒜"
  shows
    "(λx. x prestrict ((=) p)) ` (𝒫∀p⇧n) ⊆
      ⋃ 𝒜'"
proof clarify
  fix x :: "'a p_adic_prod"
  assume x: "x ∈ (𝒫∀p⇧n)"
  with nonneg have x_O: "x ∈ 𝒪∀p"
    using global_p_depth_p_adic_prod.global_depth_set_antimono by auto
  from x nonneg have res_x_P: "x prestrict ((=) p) ∈ (𝒫∀p⇧n)"
    using global_p_depth_p_adic_prod.global_depth_set_closed_under_p_restrict_image
    by    fastforce
  with nonneg have res_x_O: "x prestrict ((=) p) ∈ 𝒪∀p"
    using global_p_depth_p_adic_prod.global_depth_set_antimono by auto
  from nonneg
    have  "Abs_adelic_int (x prestrict ((=) p)) ∈ (𝒫∀p⇧n)"
    using res_x_P nonneg_global_depth_set_adelic_int_eq_projection
    by    fast
  moreover have
    "Abs_adelic_int (x prestrict ((=) p)) =
      (Abs_adelic_int (x prestrict ((=) p))) prestrict ((=) p)"
    using res_x_O p_restrict_adelic_int_abs_eq by fastforce
  ultimately obtain A where A: "A ∈ 𝒜" "Abs_adelic_int (x prestrict ((=) p)) ∈ A"
    using cover by blast
  from A(2) have "x prestrict ((=) p) ∈ Rep_adelic_int ` A"
    using res_x_O Abs_adelic_int_inverse by force
  moreover have "x prestrict ((=) p) = (x prestrict ((=) p)) prestrict ((=) p)"
    using global_p_depth_p_adic_prod.p_restrict_restrict' by simp
  moreover have restr_0: "(0 :: 'a p_adic_prod) = 0 prestrict ((≠) p)"
    using global_p_depth_p_adic_prod.p_restrict_zero by metis
  ultimately have
    "x prestrict ((=) p) + 0 prestrict ((≠) p) ∈
      (λx. x prestrict ((=) p)) ` Rep_adelic_int ` A +
      range (λx. x prestrict ((≠) p))"
    by fast
  with A(1) 𝒜'_def show "x prestrict ((=) p) ∈ ⋃ 𝒜'" using restr_0 by auto
qed

lemma adelic_int_lift_local_p_open:
  fixes p :: "'a::nontrivial_factorial_unique_euclidean_bezout prime"
  and   A :: "'a adelic_int set"
  defines
    "A' ≡
      (λx. x prestrict ((=) p)) ` Rep_adelic_int ` A +
      range (λx. x prestrict ((≠) p))"
  assumes adelic_int_p_open: "generate_topology (adelic_int_local_p_open_nbhds p) A"
  shows "generate_topology (p_adic_prod_local_p_open_nbhds p) A'"
    unfolding A'_def set_plus_def
proof (rule iffD2, rule global_p_depth_p_adic_prod.p_open_nbhds_open_subopen, clarify)
  define f f' :: "'a p_adic_prod ⇒ 'a p_adic_prod"
    where "f  ≡ λx. x prestrict ((=) p)"
    and   "f' ≡ λx. x prestrict ((≠) p)"
  fix a b assume a: "a ∈ A"
  with adelic_int_p_open obtain n where n: "adelic_int_p_open_nbhd p (int (nat n)) a ⊆ A"
    using global_p_depth_adelic_int.p_open_nbhds_open_subopen[of p A]
          adelic_int_p_open_nbhd_bound[of a p]
    by    presburger
  hence *:
    "p_adic_prod_p_open_nbhd p (int (nat n)) (Rep_adelic_int a)
      ∩ 𝒪∀p
      ⊆ Rep_adelic_int ` A"
    using adelic_int_p_open_nbhd_rep_eq by blast
  have
    "p_adic_prod_p_open_nbhd p (int (nat n)) (f (Rep_adelic_int a) + f' b) ⊆
      f ` Rep_adelic_int ` A + range f'"
  proof
    fix y
    assume "y ∈ p_adic_prod_p_open_nbhd p (int (nat n)) (f (Rep_adelic_int a) + f' b)"
    with f_def f'_def have y: "y ∈ p_adic_prod_p_open_nbhd p (int (nat n)) (Rep_adelic_int a)"
      by (simp add: global_p_depth_p_adic_prod.p_open_nbhd_p_restrict_add_mixed_drop_right)
    have f_y: "f y ∈ 𝒪∀p"
      unfolding f_def global_depth_set_p_adic_prod_def
    proof (
      intro global_p_depth_p_adic_prod.global_depth_set_p_restrictI
            global_p_depth_p_adic_prod.p_depth_setI,
      clarify
    )
      assume y_n0: "y ¬≃⇩p 0"
      show "(y°⇧p) ≥ 0"
      proof (cases "y ≃⇩p (Rep_adelic_int a)")
        case True thus ?thesis
          using global_p_depth_p_adic_prod.depth_equiv p_depth_adelic_int_def adelic_int_depth
          by    metis
      next
        case y_a_nequiv: False
        hence y_a_depth: "((y - Rep_adelic_int a)°⇧p) ≥ int (nat n)"
          using y global_p_depth_p_adic_prod.p_open_nbhd_eq_circle by blast
        show ?thesis
        proof (cases "Rep_adelic_int a ≃⇩p 0")
          case True thus ?thesis
            using y_a_depth
                  global_p_depth_p_adic_prod.depth_diff_equiv0_right[of p "Rep_adelic_int a" y]
            by    linarith
        next
          case False
          from y_n0 have
            "(y°⇧p) < ((Rep_adelic_int a)°⇧p) ⟹ ?thesis"
            using y_a_depth
                  global_p_depth_p_adic_prod.depth_pre_nonarch_diff_left[
                    of p y "Rep_adelic_int a"
                  ]
            by    linarith
          moreover from False have
            "(y°⇧p) ≥ ((Rep_adelic_int a)°⇧p) ⟹
              ?thesis"
            using global_p_depth_p_adic_prod.depth_pre_nonarch_diff_right[
                    of p "Rep_adelic_int a" y
                  ]
                  p_depth_adelic_int_def[of p a] adelic_int_depth[of p a]
            by    simp
          ultimately show ?thesis by fastforce
        qed
      qed
    qed
    with y f_def have "f y ∈ Rep_adelic_int ` A"
      using * global_p_depth_p_adic_prod.p_open_nbhd_circle_multicentre'[of y]
            global_p_depth_p_adic_prod.p_open_nbhd_circle_multicentre'[of "f y"]
            global_p_depth_p_adic_prod.p_open_nbhd_p_restrict
      by    fast
    moreover from f_def f'_def have "y = f (f y) + f' y"
      using global_p_depth_p_adic_prod.p_restrict_restrict'
            global_p_depth_p_adic_prod.p_restrict_decomp
      by    auto
    ultimately show "y ∈ f ` Rep_adelic_int ` A + range f'"
      using set_plus_def by fast
  qed
  thus
    "∃n. p_adic_prod_p_open_nbhd p n (f (Rep_adelic_int a) + f' b)
      ⊆ {c. ∃a∈f ` Rep_adelic_int ` A. ∃b∈range f'. c = a + b}"
    using set_plus_def by blast
qed


text ‹Sequences›

abbreviation
  "adelic_int_p_limseq_condition ≡ global_p_depth_adelic_int.p_limseq_condition"
abbreviation
  "adelic_int_p_cauchy_condition ≡ global_p_depth_adelic_int.p_cauchy_condition"
abbreviation "adelic_int_p_limseq            ≡ global_p_depth_adelic_int.p_limseq"
abbreviation "adelic_int_p_cauchy            ≡ global_p_depth_adelic_int.p_cauchy"
abbreviation "adelic_int_p_open_nbhds_limseq ≡ global_p_depth_adelic_int.p_open_nbhds_LIMSEQ"

context
  fixes p :: "'a::nontrivial_factorial_idom prime"
    and X :: "nat ⇒ 'a p_adic_prod"
    and Y :: "nat ⇒ 'a adelic_int"
  defines "Y ≡ λn. Abs_adelic_int (X n)"
  assumes range_X: "range X ⊆ 𝒪∀p"
begin

lemma adelic_int_p_limseq_condition_abs_eq:
  "adelic_int_p_limseq_condition p Y (Abs_adelic_int x) =
    p_adic_prod_p_limseq_condition p X x"
  if "x ∈ 𝒪∀p"
proof (standard, standard)
  fix n :: int and N :: nat
  from range_X have "∀n. X n ∈ 𝒪∀p" by blast
  with that Y_def have
    "adelic_int_p_limseq_condition p Y (Abs_adelic_int x) n N =
      (∀k≥N. (X k) ¬≃⇩p x ⟶
        ((X k - x)°⇧p) > n)"
    using global_p_depth_adelic_int.p_limseq_condition_def p_equal_adelic_int_abs_eq
          p_depth_adelic_int_diff_abs_eq
    by    metis
  thus
    "adelic_int_p_limseq_condition p Y (Abs_adelic_int x) n N =
      p_adic_prod_p_limseq_condition p X x n N"
    using global_p_depth_p_adic_prod.p_limseq_condition_def by blast
qed

lemma adelic_int_p_limseq_abs_eq:
  "adelic_int_p_limseq p Y (Abs_adelic_int x) = p_adic_prod_p_limseq p X x"
  if "x ∈ 𝒪∀p"
  using that adelic_int_p_limseq_condition_abs_eq by auto

lemma adelic_int_p_cauchy_condition_abs_eq:
  "adelic_int_p_cauchy_condition p Y = p_adic_prod_p_cauchy_condition p X"
proof (standard, standard)
  fix n :: int and K :: nat
  from range_X have "∀n. X n ∈ 𝒪∀p" by blast
  moreover from this Y_def
    have  "∀n n'. ((Y n - Y n')°⇧p) = ((X n - X n')°⇧p)"
    using p_equal_adelic_int_abs_eq p_depth_adelic_int_diff_abs_eq
    by    blast
  ultimately have
    "adelic_int_p_cauchy_condition p Y n K =
      (∀k1≥K. ∀k2≥K.
        (X k1) ¬≃⇩p (X k2) ⟶
          ((X k1 - X k2)°⇧p) > n)"
    using Y_def global_p_depth_adelic_int.p_cauchy_condition_def p_equal_adelic_int_abs_eq by metis
  thus "adelic_int_p_cauchy_condition p Y n K = p_adic_prod_p_cauchy_condition p X n K"
    using global_p_depth_p_adic_prod.p_cauchy_condition_def by blast
qed

lemma adelic_int_p_cauchy_abs_eq: "adelic_int_p_cauchy p Y = p_adic_prod_p_cauchy p X"
  using adelic_int_p_cauchy_condition_abs_eq by simp

end (* context p_adic_prod int ring seq *)

lemma adelic_int_p_open_nbhds_limseq_abs_eq:
  "adelic_int_p_open_nbhds_limseq (λn. Abs_adelic_int (X n)) (Abs_adelic_int x) =
    p_adic_prod_p_open_nbhds_limseq X x"
  if "range X ⊆ 𝒪∀p" and "x ∈ 𝒪∀p"
  using that adelic_int_p_limseq_abs_eq
        global_p_depth_p_adic_prod.globally_limseq_iff_locally_limseq[of X x]
        global_p_depth_adelic_int.globally_limseq_iff_locally_limseq[of
          "λn. Abs_adelic_int (X n)" "Abs_adelic_int x"
        ]
  by    blast

subsubsection ‹Topology via global depth›

text ‹The metric›
instantiation adelic_int :: (nontrivial_factorial_idom) metric_space
begin

definition "dist = global_p_depth_adelic_int.bdd_global_dist"
declare dist_adelic_int_def [simp]

definition "uniformity = global_p_depth_adelic_int.bdd_global_uniformity"
declare uniformity_adelic_int_def [simp]

definition open_adelic_int :: "'a adelic_int set ⇒ bool"
  where
    "open_adelic_int U =
      (∀x∈U.
        eventually (λ(x', y). x' = x ⟶ y ∈ U) uniformity
      )"

instance
  by (
    standard,
    simp_all add: global_p_depth_adelic_int.bdd_global_uniformity_def open_adelic_int_def
                  global_p_depth_adelic_int.metric_space_by_bdd_depth.dist_triangle2
  )

end (* instantiation adelic_int metric_space *)

abbreviation "adelic_int_global_depth  ≡ global_p_depth_adelic_int.bdd_global_depth"

lemma adelic_int_bdd_global_depth_abs_eq:
  "adelic_int_global_depth (Abs_adelic_int x) = p_adic_prod_global_depth x"
  if "x ∈ 𝒪∀p" for x :: "'a::nontrivial_factorial_idom p_adic_prod"
proof (cases "x = 0")
  case True thus ?thesis
    using     global_p_depth_adelic_int.bdd_global_depth_0
              global_p_depth_p_adic_prod.bdd_global_depth_0
    unfolding zero_adelic_int_def
    by        force
next
  case False
  moreover from this that have "Abs_adelic_int x ≠ 0"
    using     Abs_adelic_int_inject global_p_depth_p_adic_prod.global_depth_set_0
    unfolding zero_adelic_int_def
    by        auto
  ultimately show ?thesis
    using that Abs_adelic_int_inject global_p_depth_adelic_int.bdd_global_depthD
          p_equal_adelic_int_abs_eq0 p_depth_adelic_int_abs_eq
          global_p_depth_p_adic_prod.bdd_global_depthD
          global_p_depth_adelic_int.global_eq_iff
    by    fastforce
qed

lemma dist_adelic_int_abs_eq:
  "dist (Abs_adelic_int x) (Abs_adelic_int y) = dist x y"
  if "x ∈ 𝒪∀p" and "y ∈ 𝒪∀p"
  for x y :: "'a::nontrivial_factorial_idom p_adic_prod"
proof (cases "x = y")
  case True with that show ?thesis
    using Abs_adelic_int_inject global_p_depth_adelic_int.bdd_global_dist_eqD
          global_p_depth_p_adic_prod.bdd_global_dist_eqD
    by    auto
next
  case False with that show ?thesis
    using dist_adelic_int_def Abs_adelic_int_inject global_p_depth_adelic_int.bdd_global_distD
          minus_adelic_int_abs_eq global_p_depth_p_adic_prod.global_depth_set_minus
          adelic_int_bdd_global_depth_abs_eq global_depth_set_p_adic_prod_def
          global_p_depth_p_adic_prod.bdd_global_distD dist_p_adic_prod_def
          global_p_depth_p_adic_prod.global_eq_iff global_p_depth_adelic_int.global_eq_iff
    by    metis
qed

lemma adelic_int_limseq_abs_eq:
  "(λn. Abs_adelic_int (X n)) ⇢ Abs_adelic_int x
    ⟷ X ⇢ x"
  if "range X ⊆ 𝒪∀p" and "x ∈ 𝒪∀p"
proof-
  from that have "∀n. dist (Abs_adelic_int (X n)) (Abs_adelic_int x) = dist (X n) x"
    using dist_adelic_int_abs_eq[of "X _" x] by blast
  thus ?thesis
    using tendsto_iff[of "λn. Abs_adelic_int (X n)" "Abs_adelic_int x"] tendsto_iff[of X x]
    by    presburger
qed

lemma adelic_int_bdd_metric_LIMSEQ:
  "X ⇢ x = global_p_depth_adelic_int.metric_space_by_bdd_depth.LIMSEQ X x"
  for X :: "nat ⇒ 'a::nontrivial_factorial_idom adelic_int" and x :: "'a adelic_int"
  unfolding tendsto_iff global_p_depth_adelic_int.metric_space_by_bdd_depth.tendsto_iff
            dist_adelic_int_def
  by        fast

lemma adelic_int_global_depth_set_lim_closed:
  "x ∈ 𝒫∀p⇧n"
  if  lim  : "X ⇢ x"
  and depth: "∀F k in sequentially. X k ∈ 𝒫∀p⇧n"
  for X :: "nat ⇒ 'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
  and x :: "'a adelic_int"
proof (
  cases "n ≤ 0", use nonpos_global_depth_set_adelic_int in blast,
  cases X x rule: adelic_int_seq_cases[case_product Abs_adelic_int_cases]
)
  case False case (Abs_adelic_int_Abs_adelic_int F a)
  with lim have "F ⇢ a" using adelic_int_limseq_abs_eq by blast
  moreover have
    "∀F k in sequentially. F k ∈ 𝒫∀p⇧n"
  proof-
    from depth obtain K where K: "∀k≥K. X k ∈ 𝒫∀p⇧n"
      using eventually_sequentially by auto
    have "∀k≥K. F k ∈ 𝒫∀p⇧n"
    proof clarify
      fix k assume "k ≥ K"
      with False Abs_adelic_int_Abs_adelic_int(1) K obtain z
        where "z ∈ 𝒫∀p⇧n"
        and   "Abs_adelic_int (F k) = Abs_adelic_int z"
        using nonneg_global_depth_set_adelic_int_eq_projection[of n]
        by    auto
      with False Abs_adelic_int_Abs_adelic_int(2)
        show  "F k ∈ 𝒫∀p⇧n"
        using Abs_adelic_int_inject[of "F k" z]
              global_p_depth_p_adic_prod.global_depth_set_antimono[of 0 n]
        by    auto
    qed
    thus ?thesis using eventually_sequentially by blast
  qed
  ultimately have "a ∈ 𝒫∀p⇧n"
    using p_adic_prod_global_depth_set_lim_closed by auto
  with False Abs_adelic_int_Abs_adelic_int(3) show ?thesis
    using nonneg_global_depth_set_adelic_int_eq_projection[of n] by auto
qed

lemma adelic_int_metric_ball_multicentre:
  "ball y e = ball x e" if "y ∈ ball x e" for x y :: "'a::nontrivial_factorial_idom adelic_int"
  using     that global_p_depth_adelic_int.bdd_global_dist_ball_multicentre
  unfolding ball_def dist_adelic_int_def
  by        blast

lemma adelic_int_metric_ball_at_0:
  "ball (0::'a::nontrivial_factorial_idom adelic_int) (inverse (2 ^ n)) = global_depth_set (int n)"
  using     global_p_depth_adelic_int.bdd_global_dist_ball_at_0
  unfolding ball_def dist_adelic_int_def global_depth_set_adelic_int_def
  by        auto

lemma adelic_int_metric_ball_at_0_normalize:
  "ball (0::'a::nontrivial_factorial_idom adelic_int) e =
    global_depth_set ⌊log 2 (inverse e)⌋"
  if "e > 0" and "e ≤ 1"
  using     that global_p_depth_adelic_int.bdd_global_dist_ball_at_0_normalize
  unfolding ball_def dist_adelic_int_def global_depth_set_adelic_int_def
  by        blast

lemma adelic_int_metric_ball_translate:
  "ball x e = x +o ball 0 e" for x :: "'a::nontrivial_factorial_idom adelic_int"
  using     global_p_depth_adelic_int.bdd_global_dist_ball_translate
  unfolding ball_def dist_adelic_int_def
  by        blast

lemma adelic_int_metric_ball_UNIV:
  "ball x e = UNIV" if "e ≥ 1" for x :: "'a::nontrivial_factorial_idom adelic_int"
proof (cases "e = 1")
  case False with that have "e > 1" by linarith
  thus ?thesis
    using     that global_p_depth_adelic_int.bdd_global_dist_ball_UNIV
    unfolding ball_def dist_adelic_int_def
    by        blast
next
  case True
  have "ball x e = x +o ball 0 e" using adelic_int_metric_ball_translate by auto
  also from True have "… = x +o 𝒪∀p"
    using adelic_int_metric_ball_at_0_normalize by force
  finally show ?thesis
    using global_p_depth_adelic_int.global_depth_set_elt_set_plus nonpos_global_depth_set_adelic_int
    by    fastforce
qed

lemma adelic_int_left_translate_metric_continuous:
  "continuous_on UNIV ((+) x)" for x :: "'a::nontrivial_factorial_idom adelic_int"
proof
  fix e :: real and z :: "'a adelic_int"
  assume e: "e > 0"
  moreover have "∀y. dist y z < e ⟶ dist (x + y) (x + z) ≤ e"
    using global_p_depth_adelic_int.bdd_global_dist_left_translate_continuous[of
            _ _ e x
          ]
    unfolding dist_p_adic_prod_def
    by        fastforce
  ultimately show
    "∃d>0. ∀x'∈UNIV.
      dist x' z < d ⟶ dist (x + x') (x + z) ≤ e"
    by    auto
qed

lemma adelic_int_right_translate_metric_continuous:
  "continuous_on UNIV (λz. z + x)" for x :: "'a::nontrivial_factorial_idom adelic_int"
proof-
  have "(λz. z + x) = (+) x" by (auto simp add: add.commute)
  thus ?thesis using adelic_int_left_translate_metric_continuous by metis
qed

lemma adelic_int_left_mult_bdd_metric_continuous:
  "continuous_on UNIV ((*) x)"
  for x :: "'a::nontrivial_factorial_idom adelic_int"
proof
  fix e :: real and z :: "'a adelic_int"
  assume e: "e > 0"
  moreover define d where "d ≡ min (e * inverse 2) 1"
  moreover have "inverse (2::real) = 2 powi (-1)" using power_int_def by force
  ultimately have "∀y. dist y z < d ⟶ dist (x * y) (x * z) ≤ e"
    using global_p_depth_adelic_int.bdd_global_dist_bdd_mult_continuous[of e x 0] adelic_int_depth
    by    fastforce
  moreover from e d_def have "d > 0" by auto
  ultimately show
    "∃d>0. ∀y∈UNIV. dist y z < d ⟶ dist (x * y) (x * z) ≤ e"
    by    blast
qed

lemma adelic_int_bdd_metric_limseq_mult:
  "(λk. w * X k) ⇢ (w * x)" if "X ⇢ x"
  for w x :: "'a::nontrivial_factorial_idom adelic_int" and X :: "nat ⇒ 'a adelic_int"
  using that adelic_int_left_mult_bdd_metric_continuous continuous_on_tendsto_compose
  by    fastforce

lemma adelic_int_global_depth_set_open:
  "open ((𝒫∀p⇧n) :: 'a::nontrivial_factorial_idom adelic_int set)"
proof (cases "n ≥ 0")
  case True
  hence "(𝒫∀p⇧n) = ball (0::'a adelic_int) (inverse (2 ^ nat n))"
    using adelic_int_metric_ball_at_0 by fastforce
  thus ?thesis by simp
next
  case False
  hence "(𝒫∀p⇧n) = (UNIV :: 'a adelic_int set)"
    using nonpos_global_depth_set_adelic_int[of n] by simp
  thus ?thesis using open_UNIV by fastforce
qed

lemma adelic_int_ball_abs_eq:
  "Abs_adelic_int ` ball x e = ball (Abs_adelic_int x) e"
  if "x ∈ 𝒪∀p" and "e ≤ 1"
  for x :: "'a::nontrivial_factorial_idom p_adic_prod"
proof safe
  fix y assume "y ∈ ball x e"
  moreover from this that(2) have "y ∈ ball x 1" by fastforce
  ultimately show "Abs_adelic_int y ∈ ball (Abs_adelic_int x) e"
    using that(1) p_adic_prod_nonpos_global_depth_set_open mem_ball dist_adelic_int_abs_eq
    by    fastforce
next
  fix y assume "y ∈ ball (Abs_adelic_int x) e"
  with that(1) show "y ∈ Abs_adelic_int ` ball x e"
    unfolding ball_def using dist_adelic_int_abs_eq by (cases y) fastforce
qed

lemma open_adelic_int_abs_eq:
  "open U = open (Abs_adelic_int ` U)" if "U ⊆ (𝒪∀p)"
  for U :: "'a::nontrivial_factorial_idom p_adic_prod set"
proof (standard, standard, clarify)
  fix u assume u: "u ∈ U"
  moreover assume "open U"
  ultimately obtain e where e: "e > 0" "ball u e ⊆ U"
    by (elim Elementary_Metric_Spaces.openE)
  define e' where "e' ≡ min e 1"
  with e(2) have "ball u e' ⊆ U" by force
  with that u e'_def have "ball (Abs_adelic_int u) e' ⊆ Abs_adelic_int ` U"
    using adelic_int_ball_abs_eq[of u e'] by auto
  moreover from e(1) e'_def have "e' > 0" by auto
  ultimately show "∃e>0. ball (Abs_adelic_int u) e ⊆ Abs_adelic_int ` U"
    using e(1) e'_def by blast
next
  assume U: "open (Abs_adelic_int ` U)"
  show "open U"
  proof
    have inj_abs: "inj_on Abs_adelic_int (𝒪∀p)"
      using Abs_adelic_int_inject inj_onI by meson
    fix u assume u: "u ∈ U"
    with U obtain e where e: "e > 0" "ball (Abs_adelic_int u) e ⊆ Abs_adelic_int ` U"
      using Elementary_Metric_Spaces.openE by blast
    define e' where "e' ≡ min e 1"
    with that e(2) u have "Abs_adelic_int ` ball u e' ⊆ Abs_adelic_int ` U"
      using adelic_int_ball_abs_eq[of u e'] by fastforce
    moreover from that u e'_def have "ball u e' ⊆ (𝒪∀p)"
      using p_adic_prod_nonpos_global_depth_set_open[of 0] by fastforce
    ultimately have "ball u e' ⊆ U" using that inj_on_vimage_image_eq[OF inj_abs] by blast
    moreover from e(1) e'_def have "e' > 0" by simp
    ultimately show "∃e>0. ball u e ⊆ U" by blast
  qed
qed

text ‹Completeness›

abbreviation "adelic_int_globally_cauchy  ≡ global_p_depth_adelic_int.globally_cauchy"
abbreviation
  "adelic_int_global_cauchy_condition  ≡ global_p_depth_adelic_int.global_cauchy_condition"

lemma adelic_int_global_cauchy_condition_abs_eq:
  "adelic_int_global_cauchy_condition (λn. Abs_adelic_int (X n)) =
    p_adic_prod_global_cauchy_condition X"
  if "range X ⊆ 𝒪∀p"
  unfolding global_p_depth_adelic_int.global_cauchy_condition_def
            global_p_depth_p_adic_prod.global_cauchy_condition_def
  by        (
              standard, standard,
              metis that subsetD rangeI p_equal_adelic_int_abs_eq p_depth_adelic_int_diff_abs_eq
            )

lemma adelic_int_globally_cauchy_abs_eq:
  "adelic_int_globally_cauchy (λn. Abs_adelic_int (X n)) = p_adic_prod_globally_cauchy X"
  if "range X ⊆ 𝒪∀p"
  using that adelic_int_global_cauchy_condition_abs_eq by metis

lemma adelic_int_globally_cauchy_vs_bdd_metric_Cauchy:
  "adelic_int_globally_cauchy X = Cauchy X"
  for X :: "nat ⇒ 'a::nontrivial_factorial_idom adelic_int"
  using     global_p_depth_adelic_int.globally_cauchy_vs_bdd_metric_Cauchy
  unfolding global_p_depth_adelic_int.metric_space_by_bdd_depth.Cauchy_def Cauchy_def
  by        auto

lemma adelic_int_Cauchy_abs_eq:
  "Cauchy (λn. Abs_adelic_int (X n)) = Cauchy X"
  if  "range X ⊆ 𝒪∀p"
  for X :: "nat ⇒ 'a::nontrivial_factorial_idom p_adic_prod"
  using that adelic_int_globally_cauchy_vs_bdd_metric_Cauchy adelic_int_globally_cauchy_abs_eq
        p_adic_prod_globally_cauchy_vs_bdd_metric_Cauchy
  by    fast

abbreviation
  "adelic_int_cauchy_lim X ≡
    Abs_adelic_int (p_adic_prod_cauchy_lim (λn. Rep_adelic_int (X n)))"

lemma adelic_int_bdd_metric_complete':
  "X ⇢ adelic_int_cauchy_lim X" if "Cauchy X"
  for X :: "nat ⇒ 'a::nontrivial_factorial_unique_euclidean_bezout adelic_int"
proof (cases X rule: adelic_int_seq_cases)
  case (Abs_adelic_int F)
  with that have "F ⇢ p_adic_prod_cauchy_lim F"
    using adelic_int_Cauchy_abs_eq p_adic_prod_bdd_metric_complete' by blast
  moreover from this Abs_adelic_int(2)
    have  "p_adic_prod_cauchy_lim F ∈ 𝒪∀p"
    using eventually_sequentially p_adic_prod_global_depth_set_lim_closed[of F]
    by    force
  ultimately have "X ⇢ Abs_adelic_int (p_adic_prod_cauchy_lim F)"
    using Abs_adelic_int adelic_int_limseq_abs_eq by blast
  moreover have "F = (λn. Rep_adelic_int (X n))"
    unfolding Abs_adelic_int(1)
  proof
    fix n from Abs_adelic_int(2) show "F n = Rep_adelic_int (Abs_adelic_int (F n))"
      using Abs_adelic_int_inverse[of "F n"] by fastforce
  qed
  ultimately show ?thesis by meson
qed

lemma adelic_int_bdd_metric_complete:
  "complete (UNIV :: 'a::nontrivial_factorial_unique_euclidean_bezout adelic_int set)"
  using adelic_int_bdd_metric_complete' completeI by blast


end  (* theory *)