text:
/-
Copyright (c) 2021 Paul Lezeau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anne Baanen, Paul Lezeau
-/
import algebra.is_prime_pow
import algebra.squarefree
import order.hom.bounded
import algebra.gcd_monoid.basic

/-!

# Chains of divisors

The results in this file show that in the monoid `associates M` of a `unique_factorization_monoid`
`M`, an element `a` is an n-th prime power iff its set of divisors is a strictly increasing chain
of length `n + 1`, meaning that we can find a strictly increasing bijection between `fin (n + 1)`
and the set of factors of `a`.

## Main results
- `divisor_chain.exists_chain_of_prime_pow` : existence of a chain for prime powers.
- `divisor_chain.is_prime_pow_of_has_chain` : elements that have a chain are prime powers.
- `multiplicity_prime_eq_multiplicity_image_by_factor_order_iso` : if there is a
  monotone bijection `d` between the set of factors of `a : associates M` and the set of factors of
  `b : associates N` then for any prime `p ∣ a`, `multiplicity p a = multiplicity (d p) b`.
- `multiplicity_eq_multiplicity_factor_dvd_iso_of_mem_normalized_factor` : if there is a bijection
  between the set of factors of `a : M` and `b : N` then for any prime `p ∣ a`,
  `multiplicity p a = multiplicity (d p) b`

## Todo
- Create a structure for chains of divisors.
- Simplify proof of `mem_normalized_factors_factor_dvd_iso_of_mem_normalized_factors` using
  `mem_normalized_factors_factor_order_iso_of_mem_normalized_factors` or vice versa.

-/

variables {M : Type*} [cancel_comm_monoid_with_zero M]

lemma associates.is_atom_iff {p : associates M} (h₁ : p ≠ 0) :
  is_atom p ↔ irreducible p :=
⟨λ hp, ⟨by simpa only [associates.is_unit_iff_eq_one] using hp.1,
        λ a b h, (hp.le_iff.mp ⟨_, h⟩).cases_on
          (λ ha, or.inl (a.is_unit_iff_eq_one.mpr ha))
          (λ ha, or.inr (show is_unit b, by {rw ha at h, apply is_unit_of_associated_mul
          (show associated (p * b) p, by conv_rhs {rw h}) h₁ }))⟩,
 λ hp, ⟨by simpa only [associates.is_unit_iff_eq_one, associates.bot_eq_one] using hp.1,
        λ b ⟨⟨a, hab⟩, hb⟩, (hp.is_unit_or_is_unit hab).cases_on
          (λ hb, show b = ⊥, by rwa [associates.is_unit_iff_eq_one, ← associates.bot_eq_one] at hb)
          (λ ha, absurd (show p ∣ b, from ⟨(ha.unit⁻¹ : units _), by simp [hab]; rw mul_assoc;
            rw is_unit.mul_coe_inv ha; rw mul_one⟩) hb)⟩⟩

open unique_factorization_monoid multiplicity irreducible associates

namespace divisor_chain

lemma exists_chain_of_prime_pow {p : associates M} {n : ℕ} (hn : n ≠ 0) (hp : prime p) :
  ∃ c : fin (n + 1) → associates M,
    c 1 = p ∧ strict_mono c ∧
    ∀ {r : associates M}, r ≤ p^n ↔ ∃ i, r = c i :=
begin
  refine ⟨λ i, p^(i : ℕ), _, λ n m h, _, λ y, ⟨λ h, _, _⟩⟩,
  { rw [fin.coe_one', nat.mod_eq_of_lt, pow_one],
    exact nat.lt_succ_of_le (nat.one_le_iff_ne_zero.mpr hn) },
  { exact associates.dvd_not_unit_iff_lt.mp ⟨pow_ne_zero n hp.ne_zero, p^(m - n : ℕ),
      not_is_unit_of_not_is_unit_dvd hp.not_unit (dvd_pow dvd_rfl (nat.sub_pos_of_lt h).ne'),
      (pow_mul_pow_sub p h.le).symm⟩ },
  { obtain ⟨i, i_le, hi⟩ := (dvd_prime_pow hp n).1 h,
    rw associated_iff_eq at hi,
    exact ⟨⟨i, nat.lt_succ_of_le i_le⟩, hi⟩ },
  { rintro ⟨i, rfl⟩,
    exact ⟨p^(n - i : ℕ), (pow_mul_pow_sub p (nat.succ_le_succ_iff.mp i.2)).symm⟩ }
end

lemma element_of_chain_not_is_unit_of_index_ne_zero {n : ℕ} {i : fin (n + 1)} (i_pos : i ≠ 0)
  {c : fin (n + 1) → associates M} (h₁ : strict_mono c) :
  ¬ is_unit (c i) :=
dvd_not_unit.not_unit (associates.dvd_not_unit_iff_lt.2
  (h₁ $ show (0 : fin (n + 1)) < i, from i.pos_iff_ne_zero.mpr i_pos))

lemma first_of_chain_is_unit {q : associates M} {n : ℕ} {c : fin (n + 1) → associates M}
  (h₁ : strict_mono c) (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i) : is_unit (c 0) :=
begin
  obtain ⟨i, hr⟩ := h₂.mp associates.one_le,
  rw [associates.is_unit_iff_eq_one, ← associates.le_one_iff, hr],
  exact h₁.monotone (fin.zero_le i)
end

/-- The second element of a chain is irreducible. -/
lemma second_of_chain_is_irreducible {q : associates M} {n : ℕ} (hn : n ≠ 0)
  {c : fin (n + 1) → associates M} (h₁ : strict_mono c) (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i)
  (hq : q ≠ 0) : irreducible (c 1) :=
begin
  cases n, { contradiction },
  refine (associates.is_atom_iff (ne_zero_of_dvd_ne_zero hq (h₂.2 ⟨1, rfl⟩))).mp ⟨_, λ b hb, _⟩,
  { exact ne_bot_of_gt (h₁ (show (0 : fin (n + 2)) < 1, from fin.one_pos)) },
  obtain ⟨⟨i, hi⟩, rfl⟩ := h₂.1 (hb.le.trans (h₂.2 ⟨1, rfl⟩)),
  cases i,
  { exact (associates.is_unit_iff_eq_one _).mp (first_of_chain_is_unit h₁ @h₂) },
  { simpa [fin.lt_iff_coe_lt_coe] using h₁.lt_iff_lt.mp hb },
end

lemma eq_second_of_chain_of_prime_dvd {p q r : associates M} {n : ℕ} (hn : n ≠ 0)
  {c : fin (n + 1) → associates M} (h₁ : strict_mono c)
  (h₂ : ∀ {r : associates M}, r ≤ q ↔ ∃ i, r = c i) (hp : prime p) (hr : r ∣ q) (hp' : p ∣ r) :
  p = c 1 :=
begin
  cases n,
  { contradiction },
  obtain ⟨i, rfl⟩ := h₂.1 (dvd_trans hp' hr),
  refine congr_arg c (eq_of_ge_of_not_gt _ $ λ hi, _),
  { rw [fin.le_iff_coe_le_coe, fin.coe_one, nat.succ_le_iff, ← fin.coe_zero (n.succ + 1),
        ← fin.lt_iff_coe_lt_coe, fin.pos_iff_ne_zero],
    rintro rfl,
    exact hp.not_unit (first_of_chain_is_unit h₁ @h₂) },
  obtain (rfl | ⟨j, rfl⟩) := i.eq_zero_or_eq_succ,
  { cases hi },
  refine not_irreducible_of_not_unit_dvd_not_unit
    (dvd_not_unit.not_unit (associates.dvd_not_unit_iff_lt.2
    (h₁ (show (0 : fin (n + 2)) < j, from _)) )) _ hp.irreducible,
  { simpa [fin.succ_lt_succ_iff, fin.lt_iff_coe_lt_coe] using hi },
  { refine associates.dvd_not_unit_iff_lt.2 (h₁ _),
    simpa only [fin.coe_eq_cast_succ] using fin.lt_succ }
end

lemma card_subset_divisors_le_length_of_chain {q : associates M}
  {n : ℕ} {c : fin (n + 1) → associates M} (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i)
  {m : finset (associates M)} (hm : ∀ r, r ∈ m → r ≤ q) : m.card ≤ n + 1 :=
begin
  classical,
  have mem_image : ∀ (r : associates M), r ≤ q → r ∈ finset.univ.image c,
  { intros r hr,
    obtain ⟨i, hi⟩ := h₂.1 hr,
    exact finset.mem_image.2 ⟨i, finset.mem_univ _, hi.symm⟩ },
  rw ←finset.card_fin (n + 1),
  exact (finset.card_le_of_subset $ λ x hx, mem_image x $ hm x hx).trans finset.card_image_le,
end

variables [unique_factorization_monoid M]

lemma element_of_chain_eq_pow_second_of_chain {q r : associates M} {n : ℕ} (hn : n ≠ 0)
  {c : fin (n + 1) → associates M} (h₁ : strict_mono c)
  (h₂ : ∀ {r}, r ≤ q ↔ ∃ i, r = c i) (hr : r ∣ q)
  (hq : q ≠ 0) : ∃ (i : fin (n + 1)), r = (c 1) ^ (i : ℕ) :=
begin
  classical,
  let i := (normalized_factors r).card,
  have hi : normalized_factors r = multiset.replicate i (c 1),
  { apply multiset.eq_replicate_of_mem,
    intros b hb,
    refine eq_second_of_chain_of_prime_dvd hn h₁ (λ r', h₂) (prime_of_normalized_factor b hb) hr
      (dvd_of_mem_normalized_factors hb) },
  have H : r = (c 1)^i,
  { have := unique_factorization_monoid.normalized_factors_prod (ne_zero_of_dvd_ne_zero hq hr),
    rw [associated_iff_eq, hi, multiset.prod_replicate] at this,
    rw this },

  refine ⟨⟨i, _⟩, H⟩,
  have : (finset.univ.image (λ (m : fin (i + 1)), (c 1) ^ (m : ℕ))).card = i + 1,
  { conv_rhs { rw [← finset.card_fin (i+1)] },
    cases n, { contradiction },
    rw finset.card_image_iff,
    refine set.inj_on_of_injective (λ m m' h, fin.ext _) _,
    refine pow_injective_of_not_unit
      (element_of_chain_not_is_unit_of_index_ne_zero (by simp) h₁) _ h,
    exact irreducible.ne_zero (second_of_chain_is_irreducible hn h₁ @h₂ hq) },

  suffices H' : ∀ r ∈ (finset.univ.image (λ (m : fin (i + 1)), (c 1) ^ (m : ℕ))), r ≤ q,
  { simp only [← nat.succ_le_iff, nat.succ_eq_add_one, ← this],
    apply card_subset_divisors_le_length_of_chain @h₂ H' },

  simp only [finset.mem_image],
  rintros r ⟨a, ha, rfl⟩,
  refine dvd_trans _ hr,
  use (c 1)^(i - a),
  rw pow_mul_pow_sub (c 1),
  { exact H },
  { exact nat.succ_le_succ_iff.mp a.2 }
end

lemma eq_pow_second_of_chain_of_has_chain {q : associates M} {n : ℕ} (hn : n ≠ 0)
  {c : fin (n + 1) → associates M} (h₁ : strict_mono c)
  (h₂ : ∀ {r : associates M}, r ≤ q ↔ ∃ i, r = c i) (hq : q ≠ 0) : q = (c 1)^n :=
begin
  classical,
  obtain ⟨i, hi'⟩ := element_of_chain_eq_pow_second_of_chain hn h₁ (λ r, h₂) (dvd_refl q) hq,
  convert hi',
  refine (nat.lt_succ_iff.1 i.prop).antisymm' (nat.le_of_succ_le_succ _),
  calc n + 1 = (finset.univ : finset (fin (n + 1))).card : (finset.card_fin _).symm
         ... = (finset.univ.image c).card :
    (finset.card_image_iff.mpr (h₁.injective.inj_on _)).symm
         ... ≤ (finset.univ.image (λ (m : fin (i + 1)), (c 1)^(m : ℕ))).card :
          finset.card_le_of_subset _
         ... ≤ (finset.univ : finset (fin (i + 1))).card : finset.card_image_le
         ... = i + 1 : finset.card_fin _,
  intros r hr,
  obtain ⟨j, -, rfl⟩ := finset.mem_image.1 hr,
  have := h₂.2 ⟨j, rfl⟩,
  rw hi' at this,
  obtain ⟨u, hu, hu'⟩ := (dvd_prime_pow (show prime (c 1), from _) i).1 this,
  refine finset.mem_image.mpr ⟨u, finset.mem_univ _, _⟩,
  { rw associated_iff_eq at hu', rw [fin.coe_coe_of_lt (nat.lt_succ_of_le hu), hu'] },
  { rw ← irreducible_iff_prime, exact second_of_chain_is_irreducible hn h₁ @h₂ hq, }
end

lemma is_prime_pow_of_has_chain {q : associates M} {n : ℕ} (hn : n ≠ 0)
  {c : fin (n + 1) → associates M} (h₁ : strict_mono c)
  (h₂ : ∀ {r : associates M}, r ≤ q ↔ ∃ i, r = c i) (hq : q ≠ 0) : is_prime_pow q :=
⟨c 1, n, irreducible_iff_prime.mp (second_of_chain_is_irreducible hn h₁ @h₂ hq),
  zero_lt_iff.mpr hn, (eq_pow_second_of_chain_of_has_chain hn h₁ @h₂ hq).symm⟩

end divisor_chain

variables {N : Type*} [cancel_comm_monoid_with_zero N]

lemma factor_order_iso_map_one_eq_bot {m : associates M} {n : associates N}
  (d : {l : associates M // l ≤ m} ≃o {l : associates N // l ≤ n}) :
  (d ⟨1, one_dvd m⟩ : associates N) = 1 :=
begin
  letI : order_bot {l : associates M // l ≤ m} := subtype.order_bot bot_le,
  letI : order_bot {l : associates N // l ≤ n} := subtype.order_bot bot_le,
  simp [←associates.bot_eq_one]
end

lemma coe_factor_order_iso_map_eq_one_iff {m u : associates M} {n : associates N}
  (hu' : u ≤ m) (d : set.Iic m ≃o set.Iic n) :
  (d ⟨u, hu'⟩ : associates N) = 1 ↔ u = 1 :=
⟨λ hu, by { rw (show u = ↑(d.symm ⟨↑(d ⟨u, hu'⟩), (d ⟨u, hu'⟩).prop⟩), by simp only
    [subtype.coe_eta, order_iso.symm_apply_apply, subtype.coe_mk]),
  convert factor_order_iso_map_one_eq_bot d.symm },
  λ hu, by {simp_rw hu, convert factor_order_iso_map_one_eq_bot d } ⟩

section

variables [unique_factorization_monoid N] [unique_factorization_monoid M]

open divisor_chain

lemma pow_image_of_prime_by_factor_order_iso_dvd [decidable_eq (associates M)] {m p : associates M}
  {n : associates N} (hn : n ≠ 0) (hp : p ∈ normalized_factors m)
  (d : set.Iic m ≃o set.Iic n) {s : ℕ} (hs' : p^s ≤ m) :
  (d ⟨p, dvd_of_mem_normalized_factors hp⟩ : associates N)^s ≤ n :=
begin
  by_cases hs : s = 0,
  { simp [hs], },
  suffices : (d ⟨p, dvd_of_mem_normalized_factors hp⟩ : associates N)^s = ↑(d ⟨p^s, hs'⟩),
  { rw this,
    apply subtype.prop (d ⟨p^s, hs'⟩) },
  obtain ⟨c₁, rfl, hc₁', hc₁''⟩ := exists_chain_of_prime_pow hs (prime_of_normalized_factor p hp),

  set c₂ : fin (s + 1) → associates N := λ t, d ⟨c₁ t, le_trans (hc₁''.2 ⟨t, by simp⟩) hs'⟩,
  have c₂.def : ∀ (t), c₂ t = d ⟨c₁ t, _⟩ := λ t, rfl,
  refine (congr_arg (^s) (c₂.def 1).symm).trans _,
  refine (eq_pow_second_of_chain_of_has_chain hs (λ t u h, _) (λ r, ⟨λ hr, _, _⟩) _).symm,
  { rw [c₂.def, c₂.def, subtype.coe_lt_coe, d.lt_iff_lt, subtype.mk_lt_mk, (hc₁').lt_iff_lt],
    exact h },
  { have : r ≤ n := hr.trans (d ⟨c₁ 1 ^ s, _⟩).2,
    suffices : d.symm ⟨r, this⟩ ≤ ⟨c₁ 1 ^ s, hs'⟩,
    { obtain ⟨i, hi⟩ := hc₁''.1 this,
      use i,
      simp only [c₂.def, ← hi, d.apply_symm_apply, subtype.coe_eta, subtype.coe_mk] },
    conv_rhs { rw ← d.symm_apply_apply ⟨c₁ 1 ^ s, hs'⟩ },
    rw d.symm.le_iff_le,
    simpa only [← subtype.coe_le_coe, subtype.coe_mk] using hr },
  { rintros ⟨i, hr⟩,
    rw [hr, c₂.def, subtype.coe_le_coe, d.le_iff_le],
    simpa [subtype.mk_le_mk] using hc₁''.2 ⟨i, rfl⟩ },
  exact ne_zero_of_dvd_ne_zero hn (subtype.prop (d ⟨c₁ 1 ^ s, _⟩))
end

lemma map_prime_of_factor_order_iso [decidable_eq (associates M)]
  {m p : associates M} {n : associates N} (hn : n ≠ 0) (hp : p ∈ normalized_factors m)
  (d : set.Iic m ≃o set.Iic n) : prime (d ⟨p, dvd_of_mem_normalized_factors hp⟩ : associates N) :=
begin
  rw ← irreducible_iff_prime,
  refine (associates.is_atom_iff $ ne_zero_of_dvd_ne_zero hn (d ⟨p, _⟩).prop).mp ⟨_, λ b hb, _⟩,
  { rw [ne.def, ← associates.is_unit_iff_eq_bot, associates.is_unit_iff_eq_one,
      coe_factor_order_iso_map_eq_one_iff _ d],
    rintro rfl,
    exact (prime_of_normalized_factor 1 hp).not_unit is_unit_one },
  { obtain ⟨x, hx⟩ := d.surjective ⟨b, le_trans (le_of_lt hb)
      (d ⟨p, dvd_of_mem_normalized_factors hp⟩).prop⟩,
    rw [← subtype.coe_mk b _ , subtype.coe_lt_coe, ← hx] at hb,
    letI : order_bot {l : associates M // l ≤ m} := subtype.order_bot bot_le,
    letI : order_bot {l : associates N // l ≤ n} := subtype.order_bot bot_le,
    suffices : x = ⊥,
    { rw [this, order_iso.map_bot d] at hx,
      refine (subtype.mk_eq_bot_iff _ _).mp hx.symm,
      exact bot_le },
    obtain ⟨a, ha⟩ := x,
    rw subtype.mk_eq_bot_iff,
    { exact ((associates.is_atom_iff $ prime.ne_zero $ prime_of_normalized_factor p hp).mpr $
      irreducible_of_normalized_factor p hp).right a (subtype.mk_lt_mk.mp $ d.lt_iff_lt.mp hb) },
  exact bot_le }
end

lemma mem_normalized_factors_factor_order_iso_of_mem_normalized_factors
  [decidable_eq (associates M)] [decidable_eq (associates N)] {m p : associates M}
  {n : associates N} (hn : n ≠ 0) (hp : p ∈ normalized_factors m)
  (d : set.Iic m ≃o set.Iic n) :
  ↑(d ⟨p, dvd_of_mem_normalized_factors hp⟩) ∈ normalized_factors n :=
begin
  obtain ⟨q, hq, hq'⟩ := exists_mem_normalized_factors_of_dvd hn
    (map_prime_of_factor_order_iso hn hp d).irreducible
    (d ⟨p, dvd_of_mem_normalized_factors hp⟩).prop,
  rw associated_iff_eq at hq',
  rwa hq'
end

variables [decidable_rel ((∣) : M → M → Prop)] [decidable_rel ((∣) : N → N → Prop)]

lemma multiplicity_prime_le_multiplicity_image_by_factor_order_iso [decidable_eq (associates M)]
  {m p : associates M} {n : associates N} (hp : p ∈ normalized_factors m)
  (d : set.Iic m ≃o set.Iic n) :
  multiplicity p m ≤ multiplicity ↑(d ⟨p, dvd_of_mem_normalized_factors hp⟩) n :=
begin
  by_cases hn : n = 0,
  { simp [hn], },
  by_cases hm : m = 0,
  { simpa [hm] using hp, },
  rw [← part_enat.coe_get
    (finite_iff_dom.1 $ finite_prime_left (prime_of_normalized_factor p hp) hm),
    ← pow_dvd_iff_le_multiplicity],
  exact pow_image_of_prime_by_factor_order_iso_dvd hn hp d (pow_multiplicity_dvd _),
end

lemma multiplicity_prime_eq_multiplicity_image_by_factor_order_iso [decidable_eq (associates M)]
  {m p : associates M} {n : associates N} (hn : n ≠ 0)
  (hp : p ∈ normalized_factors m) (d : set.Iic m ≃o set.Iic n) :
  multiplicity p m = multiplicity ↑(d ⟨p, dvd_of_mem_normalized_factors hp⟩) n :=
begin
  refine le_antisymm (multiplicity_prime_le_multiplicity_image_by_factor_order_iso hp d) _,
  suffices : multiplicity ↑(d ⟨p, dvd_of_mem_normalized_factors hp⟩) n ≤
    multiplicity ↑(d.symm (d ⟨p, dvd_of_mem_normalized_factors hp⟩)) m,
  { rw [d.symm_apply_apply ⟨p, dvd_of_mem_normalized_factors hp⟩, subtype.coe_mk] at this,
    exact this },
  letI := classical.dec_eq (associates N),
  simpa only [subtype.coe_eta] using
    (multiplicity_prime_le_multiplicity_image_by_factor_order_iso
      (mem_normalized_factors_factor_order_iso_of_mem_normalized_factors hn hp d) d.symm),
end

end

variables [unique (Mˣ)] [unique (Nˣ)]

/-- The order isomorphism between the factors of `mk m` and the factors of `mk n` induced by a
  bijection between the factors of `m` and the factors of `n` that preserves `∣`. -/
@[simps]
def mk_factor_order_iso_of_factor_dvd_equiv
  {m : M} {n : N} {d : {l : M // l ∣ m} ≃ {l : N // l ∣ n}}
  (hd : ∀ l l', ((d l) : N) ∣ (d l') ↔ (l : M) ∣ (l' : M)) :
   set.Iic (associates.mk m) ≃o set.Iic (associates.mk n) :=
{ to_fun := λ l, ⟨associates.mk (d ⟨associates_equiv_of_unique_units ↑l,
    by { obtain ⟨x, hx⟩ := l, rw [subtype.coe_mk,  associates_equiv_of_unique_units_apply,
      out_dvd_iff], exact hx } ⟩),
    mk_le_mk_iff_dvd_iff.mpr (subtype.prop (d ⟨associates_equiv_of_unique_units ↑l, _ ⟩)) ⟩,
  inv_fun := λ l, ⟨associates.mk (d.symm (⟨(associates_equiv_of_unique_units ↑l),
      by obtain ⟨x, hx⟩ := l ; rw [subtype.coe_mk, associates_equiv_of_unique_units_apply,
      out_dvd_iff] ; exact hx ⟩)),
    mk_le_mk_iff_dvd_iff.mpr (subtype.prop (d.symm ⟨associates_equiv_of_unique_units ↑l, _ ⟩)) ⟩,
  left_inv := λ ⟨l, hl⟩, by simp only [subtype.coe_eta, equiv.symm_apply_apply, subtype.coe_mk,
    associates_equiv_of_unique_units_apply, mk_out, out_mk, normalize_eq],
  right_inv := λ ⟨l, hl⟩, by simp only [subtype.coe_eta, equiv.apply_symm_apply, subtype.coe_mk,
    associates_equiv_of_unique_units_apply, out_mk, normalize_eq, mk_out],
  map_rel_iff' :=
    by rintros ⟨a, ha⟩ ⟨b, hb⟩ ; simp only [equiv.coe_fn_mk, subtype.mk_le_mk,
      associates.mk_le_mk_iff_dvd_iff, hd, subtype.coe_mk, associates_equiv_of_unique_units_apply,
      out_dvd_iff, mk_out] }

variables [unique_factorization_monoid M] [unique_factorization_monoid N]
  [decidable_eq M]

lemma mem_normalized_factors_factor_dvd_iso_of_mem_normalized_factors [decidable_eq N] {m p : M}
  {n : N} (hm : m ≠ 0) (hn : n ≠ 0) (hp : p ∈ normalized_factors m)
  {d : {l : M // l ∣ m} ≃ {l : N // l ∣ n}}
  (hd : ∀ l l', ((d l) : N) ∣ (d l') ↔ (l : M) ∣ (l' : M)) :
    ↑(d ⟨p, dvd_of_mem_normalized_factors hp⟩) ∈ normalized_factors n :=
begin
  suffices : prime ↑(d ⟨associates_equiv_of_unique_units (associates_equiv_of_unique_units.symm p),
    by simp [dvd_of_mem_normalized_factors hp]⟩),
  { simp only [associates_equiv_of_unique_units_apply, out_mk, normalize_eq,
      associates_equiv_of_unique_units_symm_apply] at this,
    obtain ⟨q, hq, hq'⟩ := exists_mem_normalized_factors_of_dvd hn (this.irreducible)
      (d ⟨p, by apply dvd_of_mem_normalized_factors ; convert hp⟩).prop,
    rwa associated_iff_eq.mp hq' },
  have : associates.mk ↑(d ⟨associates_equiv_of_unique_units
    (associates_equiv_of_unique_units.symm p), by simp only [dvd_of_mem_normalized_factors hp,
      associates_equiv_of_unique_units_apply, out_mk, normalize_eq,
      associates_equiv_of_unique_units_symm_apply] ⟩)
    = ↑(mk_factor_order_iso_of_factor_dvd_equiv hd ⟨( associates_equiv_of_unique_units.symm p),
      by simp only [associates_equiv_of_unique_units_symm_apply] ;
        exact mk_dvd_mk.mpr (dvd_of_mem_normalized_factors hp) ⟩),
  { rw mk_factor_order_iso_of_factor_dvd_equiv_apply_coe,
    simp only [subtype.coe_mk] },
  rw [ ← associates.prime_mk, this],
  letI := classical.dec_eq (associates M),
  refine map_prime_of_factor_order_iso (mk_ne_zero.mpr hn) _ _,
  obtain ⟨q, hq, hq'⟩ := exists_mem_normalized_factors_of_dvd (mk_ne_zero.mpr hm)
    ((prime_mk p).mpr (prime_of_normalized_factor p (by convert hp))).irreducible
      (mk_le_mk_of_dvd (dvd_of_mem_normalized_factors hp)),
  simpa only [associated_iff_eq.mp hq', associates_equiv_of_unique_units_symm_apply] using hq,
end

variables [decidable_rel ((∣) : M → M → Prop)] [decidable_rel ((∣) : N → N → Prop)]

lemma multiplicity_factor_dvd_iso_eq_multiplicity_of_mem_normalized_factor {m p : M} {n : N}
  (hm : m ≠ 0) (hn : n ≠ 0) (hp : p ∈ normalized_factors m)
  {d : {l : M // l ∣ m} ≃ {l : N // l ∣ n}} (hd : ∀ l l', ((d l) : N) ∣ (d l') ↔ (l : M) ∣ l') :
    multiplicity ((d ⟨p, dvd_of_mem_normalized_factors hp⟩) : N) n = multiplicity p m :=
begin
  apply eq.symm,
  suffices : multiplicity (associates.mk p) (associates.mk m) = multiplicity (associates.mk
    ↑(d ⟨associates_equiv_of_unique_units (associates_equiv_of_unique_units.symm p),
      by simp [dvd_of_mem_normalized_factors hp]⟩))
    (associates.mk n),
  { simpa only [multiplicity_mk_eq_multiplicity, associates_equiv_of_unique_units_symm_apply,
      associates_equiv_of_unique_units_apply, out_mk, normalize_eq] using this },
  have : associates.mk ↑(d ⟨associates_equiv_of_unique_units
    (associates_equiv_of_unique_units.symm p), by simp only [dvd_of_mem_normalized_factors hp,
      associates_equiv_of_unique_units_symm_apply, associates_equiv_of_unique_units_apply,
      out_mk, normalize_eq] ⟩)
      = ↑(mk_factor_order_iso_of_factor_dvd_equiv hd ⟨(associates_equiv_of_unique_units.symm p),
        by rw [associates_equiv_of_unique_units_symm_apply] ;
          exact mk_le_mk_of_dvd (dvd_of_mem_normalized_factors hp) ⟩),
  { rw mk_factor_order_iso_of_factor_dvd_equiv_apply_coe, refl },
  rw this,
  letI := classical.dec_eq (associates M),
  refine multiplicity_prime_eq_multiplicity_image_by_factor_order_iso (mk_ne_zero.mpr hn) _
    (mk_factor_order_iso_of_factor_dvd_equiv hd),
  obtain ⟨q, hq, hq'⟩ := exists_mem_normalized_factors_of_dvd (mk_ne_zero.mpr hm)
    ((prime_mk p).mpr (prime_of_normalized_factor p hp)).irreducible
      (mk_le_mk_of_dvd (dvd_of_mem_normalized_factors hp)),
  rwa associated_iff_eq.mp hq',
end


text:
import lib.m154

namespace m154
open nat M154
-- Dans toute la suite, x, a, b, c et d désignent des nombres réels.
variables {x a b c d : ℝ}

/-
# Conjonctions

Ce fichier aborde l'étude du connecteur logique de conjonction, le « et » logique.
Il est noté `∧` par l'ordinateur et simplement `et` sur papier la plupart du temps.

Lorsqu'on dispose d'un résultat de la forme `P ∧ Q`, on peut utiliser que `P` est vrai
et que `Q` est vrai. Il y a deux possibilités pour cela. On peut explicitement
obtenir les deux énoncés à l'aide de la commande `Par ... on obtient ...` comme
dans l'exemple suivant.
-/

example (h : 0 ≤ a ∧ b ≤ 1) : b ≤ 1 :=
begin
  Par h on obtient (ha : 0 ≤ a) (hb : b ≤ 1),
  On conclut par hb,
end

/-
Cette méthode est un peu lourde quand l'hypothèse est directement accessible et
qu'on ne compte s'en servir qu'une fois.
On peut alors raccourcir en utilisant les suffixes `.1` et `.2` pour accéder aux
deux énoncés.
-/

example (h : 0 ≤ a ∧ b ≤ 1) : b ≤ 1 :=
begin
  On conclut par h.2,
end

example (h : 0 ≤ a ∧ b ≤ 1) : 0 ≤ a :=
begin
  sorry
end

/-
Pour démontrer un énoncé de la forme `P ∧ Q`, il faut fournir une démonstration de `P`
et une démonstration de `Q`. On utilise la commande `Montrons que` pour annoncer le début
de la démonstration de `P`. On peut aussi réutiliser cette commande au début de la
démonstration de `Q` mais ce n'est pas obligatoire.
-/

example (ha : a > 0) : a^2 > 0 ∧ |a| > 0 :=
begin
  Montrons que a^2 > 0,
    On conclut par carre_pos appliqué à ha,
  Montrons que |a| > 0,
    On applique non_zero_abs_pos,
    -- Notez dans la ligne suivante que la commande `On conclut` fait pour nous le
    -- travail de déduire `a ≠ 0` de `ha : a > 0`
    On conclut par ha,
end

/-
Dans l'exercice suivant, on pourra réutiliser le lemme
`inferieur_mul_droite (hc : 0 ≤ c) (hab : a ≤ b) : a*c ≤ b*c`
-/

example (hb : a ≤ b ∧ b ≤ c) (hd : 0 ≤ d) : a * d ≤ b * d ∧ b * d ≤ c * d :=
begin
  sorry
end

end m154

author: PatrickMassot


text:
/-
Copyright (c) 2022 Thomas Browning. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Thomas Browning
-/
import group_theory.abelianization
import group_theory.group_action.conj_act
import group_theory.index

/-!
# Commuting Probability
This file introduces the commuting probability of finite groups.

## Main definitions
* `comm_prob`: The commuting probability of a finite type with a multiplication operation.

## Todo
* Neumann's theorem.
-/

noncomputable theory
open_locale classical
open_locale big_operators

open fintype

variables (M : Type*) [fintype M] [has_mul M]

/-- The commuting probability of a finite type with a multiplication operation -/
def comm_prob : ℚ := card {p : M × M // p.1 * p.2 = p.2 * p.1} / card M ^ 2

lemma comm_prob_def : comm_prob M = card {p : M × M // p.1 * p.2 = p.2 * p.1} / card M ^ 2 :=
rfl

lemma comm_prob_pos [h : nonempty M] : 0 < comm_prob M :=
h.elim (λ x, div_pos (nat.cast_pos.mpr (card_pos_iff.mpr ⟨⟨(x, x), rfl⟩⟩))
  (pow_pos (nat.cast_pos.mpr card_pos) 2))

lemma comm_prob_le_one : comm_prob M ≤ 1 :=
begin
  refine div_le_one_of_le _ (sq_nonneg (card M)),
  rw [←nat.cast_pow, nat.cast_le, sq, ←card_prod],
  apply set_fintype_card_le_univ,
end

variables {M}

lemma comm_prob_eq_one_iff [h : nonempty M] : comm_prob M = 1 ↔ commutative ((*) : M → M → M) :=
begin
  change (card {p : M × M | p.1 * p.2 = p.2 * p.1} : ℚ) / _ = 1 ↔ _,
  rw [div_eq_one_iff_eq, ←nat.cast_pow, nat.cast_inj, sq, ←card_prod,
      set_fintype_card_eq_univ_iff, set.eq_univ_iff_forall],
  { exact ⟨λ h x y, h (x, y), λ h x, h x.1 x.2⟩ },
  { exact pow_ne_zero 2 (nat.cast_ne_zero.mpr card_ne_zero) },
end

variables (G : Type*) [group G] [fintype G]

lemma card_comm_eq_card_conj_classes_mul_card [h : fintype (conj_classes G)] :
  card {p : G × G // p.1 * p.2 = p.2 * p.1} = @card (conj_classes G) h * card G :=
by convert calc card {p : G × G // p.1 * p.2 = p.2 * p.1} = card (Σ g, {h // g * h = h * g}) :
  card_congr (equiv.subtype_prod_equiv_sigma_subtype (λ g h : G, g * h = h * g))
... = ∑ g, card {h // g * h = h * g} : card_sigma _
... = ∑ g, card (mul_action.fixed_by (conj_act G) G g) : sum_equiv conj_act.to_conj_act.to_equiv
  _ _ (λ g, card_congr' $ congr_arg _ $ funext $ λ h, mul_inv_eq_iff_eq_mul.symm.to_eq)
... = card (quotient (mul_action.orbit_rel (conj_act G) G)) * card G :
  mul_action.sum_card_fixed_by_eq_card_orbits_mul_card_group (conj_act G) G
... = card (quotient (is_conj.setoid G)) * card G :
  have this : mul_action.orbit_rel (conj_act G) G = is_conj.setoid G :=
    setoid.ext (λ g h, (setoid.comm' _).trans is_conj_iff.symm),
  by cc

lemma comm_prob_def' : comm_prob G = card (conj_classes G) / card G :=
begin
  rw [comm_prob, card_comm_eq_card_conj_classes_mul_card, nat.cast_mul, sq],
  exact mul_div_mul_right (card (conj_classes G)) (card G) (nat.cast_ne_zero.mpr card_ne_zero),
end

variables {G} (H : subgroup G)

lemma subgroup.comm_prob_subgroup_le : comm_prob H ≤ comm_prob G * H.index ^ 2 :=
begin
  /- After rewriting with `comm_prob_def`, we reduce to showing that `G` has at least as many
    commuting pairs as `H`. -/
  rw [comm_prob_def, comm_prob_def, div_le_iff, mul_assoc, ←mul_pow, ←nat.cast_mul,
      H.index_mul_card, div_mul_cancel, nat.cast_le],
  { apply card_le_of_injective _ _,
    exact λ p, ⟨⟨p.1.1, p.1.2⟩, subtype.ext_iff.mp p.2⟩,
    exact λ p q h, by simpa only [subtype.ext_iff, prod.ext_iff] using h },
  { exact pow_ne_zero 2 (nat.cast_ne_zero.mpr card_ne_zero) },
  { exact pow_pos (nat.cast_pos.mpr card_pos) 2 },
end

lemma subgroup.comm_prob_quotient_le [H.normal] : comm_prob (G ⧸ H) ≤ comm_prob G * card H :=
begin
  /- After rewriting with `comm_prob_def'`, we reduce to showing that `G` has at least as many
    conjugacy classes as `G ⧸ H`. -/
  rw [comm_prob_def', comm_prob_def', div_le_iff, mul_assoc, ←nat.cast_mul, mul_comm (card H),
      ←subgroup.card_eq_card_quotient_mul_card_subgroup, div_mul_cancel, nat.cast_le],
  { apply card_le_of_surjective,
    show function.surjective (conj_classes.map (quotient_group.mk' H)),
    exact (conj_classes.map_surjective quotient.surjective_quotient_mk') },
  { exact nat.cast_ne_zero.mpr card_ne_zero },
  { exact nat.cast_pos.mpr card_pos },
end

variables (G)

lemma inv_card_commutator_le_comm_prob : (↑(card (commutator G)))⁻¹ ≤ comm_prob G :=
(inv_pos_le_iff_one_le_mul (by exact nat.cast_pos.mpr card_pos)).mpr
  (le_trans (ge_of_eq (comm_prob_eq_one_iff.mpr (abelianization.comm_group G).mul_comm))
    (commutator G).comm_prob_quotient_le)

author: nick-kuhn

repo: leantools

save_path: github-repos/lean/nick-kuhn-leantools


text:
/-
Copyright (c) 2022 María Inés de Frutos-Fernández. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: María Inés de Frutos-Fernández
-/
import data.real.basic
import number_theory.number_field
import ring_theory.tensor_product
import topology.metric_space.basic
import adeles_R

/-!
# The ring of adèles of a number field
We define the ring of finite adèles and the ring of adèles of a number field, both of which are
topological commutative rings.

## Main definitions
- `number_field.A_K_f` : The finite adèle ring of the number field `K`.
- `number_field.A_K`   : The adèle ring of the number field `K`.
- `number_field.inj_K_f` : The map from `K` to `A_K_f K` sending `k ∈ K ↦ (k)_v`
- `number_field.inj_K` :  The map from `K` to `A_K K` sending `k ∈ K ↦ ((k)_v, 1 ⊗ k)`.

## Main results
- `number_field.inj_K_f.injective` : The map `inj_K_f` is injective.
- `number_field.inj_K_f.ring_hom` : The injection `inj_K_f` is a ring homomorphism from `K` to
  `A_K_f K`. Hence we can regard `K` as a subring of `A_K_f K`.
- `number_field.inj_K.injective` : The map `inj_K` is injective.
- `number_field.inj_K.ring_hom` : The injection `inj_K` is a ring homomorphism from `K` to `A_K K`.
  Hence we can regard `K` as a subring of `A_K K`.

## References
* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic]

## Tags
adèle ring, number field
-/

noncomputable theory

open function

open_locale tensor_product

namespace number_field
/-! ### The adèle ring of a number field
We define the (finite) adèle ring of a number field `K`, with its topological ring structure. -/
variables (K : Type) [field K] [number_field K]

/-- The finite adèle ring of `K`.-/
def A_K_f := finite_adele_ring' (ring_of_integers K) K
/-- The adèle ring of `K`.-/
def A_K := (A_K_f K) × (ℝ ⊗[ℚ] K)

-- We define the topological ring structure on `ℝ ⊗[ℚ] K`.
-- ℝ^n is a topological ring with the product topology.
variables (n : ℕ)
instance : ring (fin n → ℝ) := pi.ring
instance : topological_space (fin n → ℝ) := Pi.topological_space
instance : has_continuous_add (fin n → ℝ) := pi.has_continuous_add'
instance : has_continuous_mul (fin n → ℝ) := pi.has_continuous_mul'
instance : topological_semiring (fin n → ℝ) := topological_semiring.mk
instance : topological_ring (fin n → ℝ) := topological_ring.mk

open_locale big_operators
/-- `K` is isomorphic to `ℚ^(dim_ℚ(K))`. -/
def linear_equiv.Q_basis : (fin (finite_dimensional.finrank ℚ K) → ℚ) ≃ₗ[ℚ] K :=
linear_equiv.symm (basis.equiv_fun (finite_dimensional.fin_basis ℚ K))

/-- The natural linear map from `ℝ^n` to `ℝ ⊗[ℚ] ℚ^n`. -/
def linear_map.Rn_to_R_tensor_Qn (n : ℕ) : (fin n → ℝ) →ₗ[ℝ] (ℝ ⊗[ℚ] (fin n → ℚ)) :=
{ to_fun    := λ x, ∑ (m : fin n), tensor_product.mk _ _ _ (x m) (λ k : (fin n), (1 : ℚ)),
  map_add'  := λ x y, by simp only [map_add, tensor_product.mk_apply, pi.add_apply,
    linear_map.add_apply, finset.sum_add_distrib],
  map_smul' := λ r x, begin
    simp only [tensor_product.mk_apply, ring_hom.id_apply, pi.smul_apply, finset.smul_sum], refl,
  end, }

/-- The map `ℝ ⊗[ℚ] ℚ^(dim_ℚ(K)) → ℝ ⊗[ℚ] K` obtained as a base change of `linear_equiv.Q_basis`. -/
def linear_map.base_change :
(ℝ ⊗[ℚ] (fin (finite_dimensional.finrank ℚ K) → ℚ)) →ₗ[ℝ] (ℝ ⊗[ℚ] K) :=
linear_map.base_change ℝ (linear_equiv.Q_basis K).to_linear_map

/-- The resulting linear map from `ℝ^(dim_ℚ(K))` to `ℝ ⊗[ℚ] K`. -/
def linear_map.Rn_to_R_tensor_K : (fin (finite_dimensional.finrank ℚ K) → ℝ) →ₗ[ℝ] (ℝ ⊗[ℚ] K) :=
linear_map.comp (linear_map.base_change K) (linear_map.Rn_to_R_tensor_Qn _)

instance : comm_ring (A_K_f K) :=
finite_adele_ring'.comm_ring (ring_of_integers K) K
instance : comm_ring (A_K K) := prod.comm_ring
instance : inhabited (A_K_f K) := ⟨0⟩
instance : inhabited (A_K K) := ⟨0⟩
instance : topological_space (A_K_f K) :=
finite_adele_ring'.topological_space (ring_of_integers K) K
instance : topological_ring (A_K_f K) :=
finite_adele_ring'.topological_ring (ring_of_integers K) K
/-- The topological ring structure on `ℝ ⊗[ℚ] K`. -/
def infinite_adeles.ring_topology : ring_topology (ℝ ⊗[ℚ] K) :=
ring_topology.coinduced (linear_map.Rn_to_R_tensor_K K)
instance : topological_space (ℝ ⊗[ℚ] K) := (infinite_adeles.ring_topology K).to_topological_space
instance : topological_ring (ℝ ⊗[ℚ] K) := (infinite_adeles.ring_topology K).to_topological_ring
instance : topological_space (A_K K) := prod.topological_space
instance : topological_ring (A_K K) := prod.topological_ring

/-- The ring ℤ is not a field. -/
lemma int.not_field : ¬ is_field ℤ :=
begin
  rw ring.not_is_field_iff_exists_ideal_bot_lt_and_lt_top,
  use ideal.span{(2 : ℤ)},
  split,
  { simp only [bot_lt_iff_ne_bot, ne.def, not_false_iff, bit0_eq_zero, one_ne_zero,
      ideal.span_singleton_eq_bot] },
  { rw [lt_top_iff_ne_top, ne.def, ideal.eq_top_iff_one, ideal.mem_span_singleton],
    intro h2,
    have h2_nonneg: 0 ≤ (2 : ℤ) := by simp only [zero_le_bit0, zero_le_one],
    have : (2 : ℤ) = 1 := int.eq_one_of_dvd_one h2_nonneg h2,
    linarith, },
end

/-- The ring of integers of a number field is not a field. -/
lemma ring_of_integers.not_field : ¬ is_field (ring_of_integers K) :=
begin
  have h_int :  algebra.is_integral ℤ (ring_of_integers K),
  { apply is_integral_closure.is_integral_algebra ℤ K,
    { apply_instance },
    { exact ring_of_integers.is_integral_closure },
    { apply_instance }} ,
  have h_inj: function.injective ⇑(algebra_map ℤ ↥(ring_of_integers K)),
  { rw [ring_hom.injective_iff_ker_eq_bot, ring_hom.ker_eq_bot_iff_eq_zero],
    intros a ha,
    rw [ring_hom.eq_int_cast, int.cast_eq_zero] at ha,
    exact ha, },
  by_contra hf,
  rw ← is_integral.is_field_iff_is_field h_int h_inj at hf,
  exact int.not_field hf,
end

/-- There exists a nonzero prime ideal of the ring of integers of a number field. -/
instance : inhabited (maximal_spectrum (ring_of_integers K)) :=
begin
  set M := classical.some(ideal.exists_maximal (ring_of_integers K)) with hM_def,
  set hM := classical.some_spec(ideal.exists_maximal (ring_of_integers K)),
  use [M, ideal.is_maximal.is_prime hM],
  { simp only [ideal.zero_eq_bot, ne.def],
    apply ring.ne_bot_of_is_maximal_of_not_is_field hM (ring_of_integers.not_field K),
  }
end

/-- The map from `K` to `A_K_f K` sending `k ∈ K ↦ (k)_v`. -/
def inj_K_f : K → A_K_f K := inj_K (ring_of_integers K) K

lemma inj_K_f.injective : injective (inj_K_f K) := inj_K.injective _ _

/-- The injection `inj_K_f` is a ring homomorphism from `K` to `A_K_f K`. Hence we can regard `K`
as a subring of `A_K_f K`. -/
def inj_K_f.ring_hom : ring_hom K (A_K_f K) := inj_K.ring_hom (ring_of_integers K) K

lemma inj_K_f.ring_hom.v_comp (v : maximal_spectrum (ring_of_integers K)) (k : K) :
  ((inj_K_f.ring_hom K) k).val v = (coe : K → v.adic_completion K) k := rfl

/-- The map from `K` to `A_K K` sending `k ∈ K ↦ ((k)_v, 1 ⊗ k)`. -/
def inj_K : K → A_K K := λ x, ⟨inj_K_f K x, algebra.tensor_product.include_right x⟩

lemma inj_K.injective : injective (inj_K K) :=
begin
  intros x y hxy,
  rw [inj_K, prod.mk.inj_iff] at hxy,
  exact inj_K_f.injective K hxy.1,
end

/-- The injection `inj_K` is a ring homomorphism from `K` to `A_K K`. Hence we can regard `K`
as a subring of `A_K K`. -/
def inj_K.ring_hom : ring_hom K (A_K K) :=
ring_hom.prod (inj_K_f.ring_hom K) (@algebra.tensor_product.include_right ℚ _ ℝ _ _ K _ _ )

end number_field

author: mariainesdff

repo: ideles-journal


text:
/-
Copyright (c) 2022 Kevin Buzzard. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author : Kevin Buzzard
-/

import tactic -- imports all the Lean tactics
import data.real.basic -- imports the real numbers
import solutions.section02reals.sheet3 -- import the definition of `tendsto` from a previous sheet

-- you can maybe do this one now
theorem tendsto_neg {a : ℕ → ℝ} {t : ℝ} (ha : tendsto a t) :
  tendsto (λ n, - a n) (-t) :=
begin
  rw tendsto_def at *,
  have h : ∀ n, |a n - t| = | -a n - -t|,
  { intro n,
    rw abs_sub_comm,
    congr' 1,
    ring },
  simpa [h] using ha,
end

/-
`tendsto_add` is quite a challenge. In a few weeks' time I'll
show you a two-line proof using filters, but right now
as you're still learning I think it's important that you
try and suffer and struggle through the first principles proof.
BIG piece of advice: write down a complete maths proof first,
with all the details there. Then, once you know the maths
proof, try translating it into Lean. Note that a bunch
of the results we proved in sheet 4 will be helpful.
-/

/-- If `a(n)` tends to `t` and `b(n)` tends to `u` then `a(n) + b(n)`
tends to `t + u`. -/
theorem tendsto_add {a b : ℕ → ℝ} {t u : ℝ}
  (ha : tendsto a t) (hb : tendsto b u) :
  tendsto (λ n, a n + b n) (t + u) :=
begin
  rw tendsto_def at *,
  -- let ε > 0 be arbitrary
  intros ε hε,
  --  There's a bound X such that if n≥X then a(n) is within ε/2 of t
  specialize ha (ε/2) (by linarith),
  cases ha with X hX,
  --  There's a bound Y such that if n≥Y then b(n) is within ε/2 of u
  obtain ⟨Y, hY⟩ := hb (ε/2) (by linarith),
  --  use max(X,Y),
  use max X Y,
  -- now say n ≥ max(X,Y)
  intros n hn,
  rw max_le_iff at hn,
  specialize hX n hn.1,
  specialize hY n hn.2,
  --  Then easy.
  rw abs_lt at *,
  split; -- semicolon means "do next tactic to all goals produced by this tactic"
  linarith,
end

/-- If `a(n)` tends to t and `b(n)` tends to `u` then `a(n) - b(n)`
tends to `t - u`. -/
theorem tendsto_sub {a b : ℕ → ℝ} {t u : ℝ}
  (ha : tendsto a t) (hb : tendsto b u) :
  tendsto (λ n, a n - b n) (t - u) :=
begin
  simpa [sub_eq_add_neg] using tendsto_add ha (tendsto_neg hb),
end

author: ImperialCollegeLondon