import data.set.basic data.set.lattice data.finset ring_theory.principal_ideal_domain

variables {R : Type*} {M : Type*} [integral_domain R]
[is_principal_ideal_ring R] [add_comm_group M] [module R M] {A : submodule R M}

open_locale classical

theorem not_mem_diff_singleton {α : Type*} {s : set α} {x : α} : x ∉ s \ {x} :=
λ h, set.not_mem_of_mem_diff h (set.mem_singleton x)

lemma insert_to_set' {α : Type*} {s : finset α} {a : α} :
   (↑(insert a s) : set α) = insert a (↑s : set α) :=
begin
  ext,
  erw finset.mem_coe,
  rw set.mem_insert_iff,
  rw finset.mem_insert,
  refl,
end

lemma subset_singleton {M : Type*} {c : M} {l : finset M} (h : l ⊆ {c}) : l = ∅ ∨ l = {c} :=
begin
  cases (finset.eq_empty_or_nonempty l),
  left,
  exact h_1,
  right,
  erw finset.eq_singleton_iff_unique_mem,
  cases h_1 with w hw,
  have := finset.mem_singleton.1 (h hw),
  rw ←this,
  split,
  exact hw,
  intros x hx,
  rw this,
  exact finset.mem_singleton.1 (h hx),
end

/-- Given a function `f : α → β` and multisets `s ⊆ β, t ⊆ α`, if `s ⊆ f's image on t`, there
exists a multiset `u ⊆ α` such that f's image on u equals s. -/
lemma subset_map {α : Type*} {β : Type*} {f : α → β} {s : multiset β}
  {t : multiset α} (h : s ≤ multiset.map f t) : ∃ u : multiset α, s = multiset.map f u :=
begin
  revert f,
  apply multiset.induction_on s,
  intros f hf, use 0, exact multiset.map_zero f,
  intros a s hf f hs,
  cases multiset.mem_map.1 (show a ∈ multiset.map f t, from multiset.mem_of_le hs (multiset.mem_cons_self a s)),
  cases hf (le_trans (multiset.le_cons_self s a) hs) with u hu,
  use w :: u,
  rw multiset.map_cons,
  rw h.2, rw ←hu,
end

theorem eq_insert_erase_of_mem {α : Type*} (s : set α) (x : α) (hx : x ∈ s) :
  s = insert x (s \ {x}) :=
begin
  symmetry,
  rw set.insert_diff_singleton,
  exact set.insert_eq_of_mem hx,
end

theorem submodule_eq_bot {M : Type*} (R : Type*) [integral_domain R]
  [is_principal_ideal_ring R] [add_comm_group M]
  [module R M] (A : submodule R M) (h : A = ⊥ )
   (S : submodule R A) : S = ⊥ :=
begin
  ext,
  split,
  intro hx,
  cases x with x1 x2,
  rw submodule.mem_bot,
  rw subtype.ext_iff,
  rw h at x2,
  exact (submodule.mem_bot R).1 x2,
  intro hx,
  rw submodule.mem_bot at hx,
  rw hx,
  exact S.zero_mem,
end

/-- Given a multiset s of elements of an integral domain, the product of elements of s equals
zero iff zero is in s. -/
theorem prod_eq_zero_iff' {α : Type*} [integral_domain α] {s : multiset α} :
  s.prod = 0 ↔ (0 : α) ∈ s :=
begin
  apply multiset.induction_on s,
  simp only [iff_self, one_ne_zero, multiset.not_mem_zero, multiset.prod_zero],
  intros a s h,
  rw multiset.prod_cons,split,
  intro h0,
  cases mul_eq_zero.1 h0,
  rw h_1, exact multiset.mem_cons_self _ _,
  exact multiset.mem_cons.2 (or.inr $ h.1 h_1),
  intro h0,
  cases multiset.mem_cons.1 h0,
  rw ←h_1,
  rw zero_mul,
  rw h.2 h_1,
  exact mul_zero a,
end

/-- Given a finset s of elements of an integral domain, the product of elements of s equals
zero iff zero is in s. -/
theorem finset_prod_eq_zero_iff {α : Type*} [integral_domain α] {s : finset α} :
  s.prod id = 0 ↔ (0 : α) ∈ s :=
begin
  erw prod_eq_zero_iff',
  erw multiset.map_id', refl,
end

lemma exists_repr_of_mem_span {α : Type*} [comm_ring α] : ∀ (s : finset α) (x : α),
  x ∈ submodule.span α (↑s : set α) → ∃ ι : α → α, x = s.sum (λ r, (ι r) * r) :=
begin
  intro s,
  apply finset.induction_on s,
    intros,
    rw [finset.coe_empty, submodule.span_empty] at a,
    use id,
    rw (submodule.mem_bot α).1 a, simp,
  intros x t h H y hy,
  rw finset.coe_insert at hy,
  rcases ideal.mem_span_insert.1 hy with ⟨a, z, hz, hs⟩,
  cases H z hz with τ hn,
  rw [hs, hn],
  use (λ b, ite (b ∈ t) (τ b) a),
  rw finset.sum_insert h,
  split_ifs,
  rw add_right_inj,
  apply finset.sum_congr,
    simp,
  intros b hb,
  split_ifs,
  simp,
end

lemma sum_mem_span {α : Type*} [ring α]
  {M : Type*} {R : Type*}
  [ring R] [add_comm_group M] [module R M] {ι : R → R}
  {x : M} {c : finset R} {p : set α} {f : p → submodule R M}
  (H : ∀ s ∈ c, ∃ m, (ι s * s) • x ∈ f m) :
  c.sum (λ y, (ι y * y) • x) ∈ submodule.span R (⋃ m, (f m).carrier) :=
begin
  refine submodule.sum_mem _ _,
  intros y hy,
  cases H y hy with m hm,
  apply submodule.subset_span, apply set.mem_Union.2,
  use m, exact hm,
end

lemma dvd_prod_finset {α : Type*}{β : Type*} [comm_semiring β]
  {a : α} {f : α → β} {s : finset α} : a ∈ s → f a ∣ s.prod f :=
begin
  intro h,
  use (s.erase a).prod f,
  conv {to_lhs, rw ←finset.insert_erase h},
  rw finset.prod_insert (finset.not_mem_erase _ _),
end

lemma insert_to_set {α : Type*} {s : finset α} {a : α} :
  (↑(insert a s) : set α) = insert a (↑s : set _) :=
begin
  ext,
  erw finset.mem_coe,
  rw set.mem_insert_iff,
  rw finset.mem_insert,
  refl,
end

lemma span_insert (s t : finset M) (hs : submodule.span R (↑s : set _) = A)
  (x : M) (hx : x ∈ s)
  (ht : submodule.span R (↑t : set _) = submodule.span R (↑(s.erase x) : set M)) :
  submodule.span R (↑(insert x t) : set _) = A :=
begin
  ext y,
  split,
  intro h,
  rw insert_to_set at h,
  rcases submodule.mem_span_insert.1 h with ⟨z, b, hb, hbz⟩,
  rw ←hs,
  rw ←finset.insert_erase hx,
  rw insert_to_set,
  rw submodule.mem_span_insert,
  use z, use b, split,
  rw ←ht, exact hb,
  exact hbz,
  intro h,
  rw insert_to_set,
  rw submodule.mem_span_insert,
  rw ←hs at h,
  rw ←finset.insert_erase hx at h,
  rw insert_to_set at h,
  rcases submodule.mem_span_insert.1 h with ⟨z, b, hb, hbz⟩,
  use z, use b,
  split,
  rw ht,
  exact hb,
  exact hbz,
end

lemma span_insert' (s : set M) (a : M) :
  submodule.span R (insert a s) = submodule.span R s ⊔ submodule.span R {a} :=
begin
  rw ←submodule.span_union,
  rw set.union_singleton,
end

lemma singleton_erase {α : Type*} (a : α) : ({a} : finset α).erase a = ∅ :=
finset.erase_insert (finset.not_mem_empty _)

lemma mem_max {α : Type*}
  (s : finset α) (h : s.nonempty) (f : α → ℕ) :
  ∃ x ∈ s, finset.fold max 0 f s = f x :=
begin
  unfreezingI {revert h},
  apply finset.induction_on s,
  intro h, exfalso,
  cases h with x hx,
  exact hx,
  intros y s hy hs h,
  cases (classical.em s.nonempty) with H H,
  rcases hs H with ⟨x, hxm, hx⟩,
  have := @finset.fold_insert_idem α ℕ max _ _ f 0 s y _ _,
  unfold max at this,
  cases (classical.em (finset.fold max 0 f s ≤ f y)) with hl hr,
  rw if_pos hl at this,
  use y, split, exact finset.mem_insert.2 (or.inl rfl),
  rw this,
  rw if_neg hr at this,
  use x, split,
  exact finset.mem_insert.2 (or.inr hxm),
  rw this, rw hx,
  have : s = ∅ := or.resolve_right s.eq_empty_or_nonempty H,
  use y, split,
  exact finset.mem_insert.2 (or.inl rfl),
  rw this, erw finset.fold_singleton,
  unfold max, rw if_pos, exact nat.zero_le _,
end

lemma exists_max {α : Type*}
  {s : finset α} (hs : s.nonempty) {P : α → ℕ → Prop}
  (h : ∀ a, a ∈ s → ∃! n, P a n) : ∃ (a : α) (n : ℕ), a ∈ s ∧
  P a n ∧ (∀ (b : α) (m : ℕ), b ∈ s ∧ P b m → m ≤ n) :=
begin
  rcases mem_max s hs (λ a, if ha : a ∈ s then
    classical.some (h a ha) else 0) with ⟨x, hxm, hx⟩,
  set N := finset.fold max 0 (λ a, if ha : a ∈ s then
    classical.some (h a ha) else 0) s,
  use x,
  use N,
  split,
  exact hxm,
  split,
  dsimp at hx,
  erw dif_pos hxm at hx,
  rw hx,
  exact (classical.some_spec (h x hxm)).1,
  intros b m hb,
  rw finset.le_fold_max m,
  right,
  use b,
  split,
  exact hb.1,
  rw dif_pos hb.1,
  rw ←(classical.some_spec (h b hb.1)).2 m hb.2,
end

lemma span_insert_zero_eq {s : set M} :
  submodule.span R (insert (0 : M) s) = submodule.span R s :=
begin
  rw ←set.union_singleton,
  rw submodule.span_union,
  rw submodule.span_singleton_eq_bot.2 rfl,
  rw sup_bot_eq,
end

lemma map_inf' (C : submodule R A) (x : M) (hx : x ∈ A) :
  submodule.span R {x} ⊓ C.map A.subtype = (C ⊓ submodule.span R {⟨x, hx⟩}).map A.subtype :=
begin
  rw inf_comm,
  convert submodule.map_inf_eq_map_inf_comap,
  ext y,
  split,
  intro h,
  cases submodule.mem_span_singleton.1 h with c hc,
  exact submodule.mem_span_singleton.2 ⟨c, by {rw ←hc, rw A.subtype.map_smul, refl,}⟩,
  intro h,
  cases submodule.mem_span_singleton.1 h with c hc,
  exact submodule.mem_span_singleton.2 ⟨c, subtype.ext_iff.2 $
    by {rw ←(show c • x = (y : M), from hc), refl,}⟩
end

lemma map_sup' (C : submodule R A) (x : M) (hx : x ∈ A) :
  submodule.span R {x} ⊔ C.map A.subtype = (C ⊔ submodule.span R {⟨x, hx⟩}).map A.subtype :=
begin
  rw submodule.map_sup,
  rw sup_comm,
  congr,
    ext y,
    split,
    intro h,
     cases submodule.mem_span_singleton.1 h with c hc,
    exact ⟨c • ⟨x, hx⟩, submodule.mem_span_singleton.2 ⟨c, rfl⟩, by {rw ←hc, refl}⟩,
  intro h, rcases h with ⟨z, hzm, hz⟩,
  cases submodule.mem_span_singleton.1 hzm with c hc,
  exact submodule.mem_span_singleton.2 ⟨c, by {rw ←hz, rw ←hc, refl}⟩,
end

lemma map_singleton {x y : M} (hx : x ∈ A) (hy : y ∈ A) :
  y ∈ submodule.span R ({x} : set M) ↔ (⟨y, hy⟩ : A) ∈ submodule.span R ({⟨x, hx⟩} : set A) :=
begin
  rw submodule.mem_span_singleton, rw submodule.mem_span_singleton,
  split,
  rintro ⟨r, hr⟩,
  use r, apply subtype.ext_iff.2,
  dsimp, exact hr,
  rintro ⟨r, hr⟩,
  use r,
  rw subtype.ext_iff at hr,
  dsimp at hr,
  rw ←hr,
end

lemma erase_insert_eq {S : finset M} {x b : M} (h : b ∈ S) (hx : x ≠ b) :
  (insert x S).erase b = insert x (S.erase b) :=
begin
  ext y,
  split,
  intro hy,
  cases finset.mem_insert.1 (finset.erase_subset _ _ hy) with h1 h2,
  exact finset.mem_insert.2 (or.inl h1),
  refine finset.mem_insert.2 (or.inr _),
  rw finset.mem_erase, split,
  exact (finset.mem_erase.1 hy).1, exact h2,
  intro hy,
  cases finset.mem_insert.1 hy with h1 h2,
  rw finset.mem_erase,
  split,
  rw h1, exact hx,
  exact finset.mem_insert.2 (or.inl h1),
  rw finset.mem_erase,
  split,
  exact (finset.mem_erase.1 h2).1,
  exact finset.mem_insert.2 (or.inr (finset.erase_subset _ _ h2)),
end

lemma subset_span' {s : finset M} (hs : submodule.span R (↑s : set M) = A) :
  (↑s : set M) ⊆ A :=
λ x hx, by rw ←hs; exact submodule.subset_span hx

noncomputable def subtype_mk' {α : Type*} (s : finset α) (t : set α) (h :  (↑s : set α) ⊆ t) :
  finset t :=
finset.image (λ x : (↑s : set α), ⟨x.1, h x.2⟩) finset.univ

lemma mem_subtype_mk' {α : Type*} {s : finset α} {t : set α} (h :  (↑s : set α) ⊆ t) {x} :
  x ∈ subtype_mk' s t h ↔ (x : α) ∈ s :=
begin
  unfold subtype_mk',
  rw finset.mem_image,
  split, rintro ⟨y, hmy, hy⟩,
  rw ←hy,
  exact y.2,
  intro hx,
  use ⟨x, hx⟩,
  split,
  exact finset.mem_univ _,
  simp only [subtype.coe_eta],
end

lemma subtype_ne {α : Type*} {p : α → Prop} {x y : subtype p} :
  (x : α) ≠ y ↔ x ≠ y :=
⟨λ hn h, hn $ h ▸ rfl, λ hn h, hn $ subtype.ext h⟩

lemma subtype_mk'_erase {α : Type*} {s : finset α} {t : set α} (h :  (↑s : set α) ⊆ t) {x} (hx : x ∈ s):
  subtype_mk' (s.erase x) t (set.subset.trans (finset.erase_subset x s) h) =
  (subtype_mk' s t h).erase ⟨x, h hx⟩ :=
begin
  ext,
  rw finset.mem_erase,
  rw mem_subtype_mk', rw mem_subtype_mk',
  rw ←subtype_ne,
  exact finset.mem_erase,
end

lemma subtype_mk'_insert {α : Type*} [decidable_eq α] {s : finset α} {t : set α} (h :  (↑s : set α) ⊆ t) {x} (hx : x ∈ t) :
  subtype_mk' (insert x s) t (by {rw finset.coe_insert, exact set.insert_subset.2 ⟨hx, h⟩}) = insert (⟨x, hx⟩ : t) (subtype_mk' s t h) :=
begin
  ext y,
  split,
  intro H,
  rw mem_subtype_mk' at H,
  cases finset.mem_insert.1 H with hl hr,
  rw finset.mem_insert, left,
  apply subtype.ext,
  exact hl,
  rw finset.mem_insert, right,
  exact (mem_subtype_mk' _).2 hr,
  intro H,
  cases finset.mem_insert.1 H with hl hr,
  rw mem_subtype_mk',
  rw finset.mem_insert,
  left,
  rw hl,
  refl,
  rw mem_subtype_mk' at hr ⊢,
  rw finset.mem_insert,
  right,
  exact hr,
end

lemma span_subtype {s : finset M} (h : submodule.span R (↑s : set M) = A) :
  submodule.span R (↑(subtype_mk' s A (subset_span' h)) : set A) = ⊤ :=
begin
  have : (↑s : set M) = A.subtype '' (↑(subtype_mk' s A (h ▸ submodule.subset_span)) : set A) :=
    by {
    ext, split, intro hx, simp, exact
      ⟨by {rw ←h, exact ⟨x, submodule.subset_span hx⟩},
      by {unfold subtype_mk', erw finset.mem_image, use x, exact hx, split, exact finset.mem_univ _,
      cases h, refl, cases h, refl}⟩,
    rintro ⟨y, hym, hy⟩,
    dsimp at hy, rw ←hy, erw mem_subtype_mk' at hym, exact hym},
  rw this at h, rw submodule.span_image at h,
  apply linear_map.map_injective A.ker_subtype,
  rw A.map_subtype_top, exact h,
end

lemma card_indep {α : Type*} {s : set α} [h1 : fintype s] (h : s.finite) :
  @fintype.card s h1 = @fintype.card s (set.finite.fintype h) :=
begin
  finish,
end

lemma univ_card {α : Type*} (s : finset α) : s.card = (@finset.univ (↑s : set α) _).card :=
begin
  rw finset.card_univ,
  simp only [fintype.card_coe],
end

lemma univ_card'' {α : Type*} {h1 : fintype (@set.univ α)} {h : fintype α} : @fintype.card (@set.univ α) h1 = fintype.card α :=
begin
  rw ←fintype.of_equiv_card (equiv.set.univ α), finish,
end

theorem card_insert' {α : Type*} {a : α} (s : set α)
  {h1 : fintype s} (h : a ∉ s) {d : fintype (insert a s : set α)} :
  @fintype.card _ d = fintype.card s + 1 :=
by rw ← set.card_fintype_insert' s h; congr


text:
/-
Justin Cai, jc5pz
-/

/- 1a.

Implement a function, bool_implies, that takes
two bool values, b1 and b2 (not propositions),
and that returns the the value of b1 → b2.
Here the → operator means implication in Boolean
algebra. To know what your function should do,
write out the truth table for implication. You
may  not use Lean's → operator (which does work
for bool values, by the way) in your answer.
-/

def bool_implies : bool → bool → bool
|   tt tt := tt
|   tt ff := ff
|   ff tt := tt
|   ff ff := tt

/- 1b.
Given your implementation of bool_implies,
prove the following proposition. Use induction
rather than the cases tactic to do case
analysis on Boolean values.
-/

example : ∀ b1 b2 : bool,
    (bool_implies b1 b2 = tt) → (b2 = tt ∨ b1 = ff) :=
begin
    intros b1 b2,
    assume bitt,
    induction b1,
    apply or.inr,
    exact rfl,
    induction b2,
    contradiction,
    apply or.inl,
    exact rfl,
end

/- 2a.

A tree of natural numbers is either empty or
it is constructed from a natural number and
two smaller trees of natural numbers. Give
an inductive definition of the type of such
trees. Call you datatype tree_nat. Your type
will have two constructors. Call the first
one "empty", and call the second "node".
Hint: The second will take three arguments.
-/

inductive tree_nat : Type
| empty : tree_nat
| node : ℕ → tree_nat → tree_nat → tree_nat

/- 2b.

Define aTree to be a node containing the
value 3 and two trees, the first one empty
and the second one a node containing the
value 2 and two empty trees.
-/

def aTree :=
tree_nat.node 3 tree_nat.empty
    (tree_nat.node 2 tree_nat.empty tree_nat.empty)

/- 3. Define a polymorphic type, "tree",
just like tree_nat, but where the value stored
in a node can be of any type, T. Then define
aTree' to be the same as aTree except that it's
now of type tree rather than of type tree_nat.
Make the type argument implicit. Finally
define a tree of strings, aTree'', just like
aTree' except that 3 is replaced by "Hi!" and
2 is replaced by "Jo".
-/

-- Your answer here
inductive tree {T: Type}: Type
| empty : tree
| node : T → tree → tree → tree

def aTree' := tree.node 3 tree.empty (tree.node 2 tree.empty tree.empty)

def aTree'' := tree.node("Hi!") tree.empty (tree.node "Jo" tree.empty tree.empty)

/- 4.

Write a recursive function, num_nodes,
that takes a value of type tree T, as an
argument, where T is some type, and that
returns the number of nodes in the tree.
The number of nodes in an empty tree is zero,
while the number of nodes in a non-empty
tree is one (for the "top" node) plus the
number of nodes in each of the subtrees.

The "at sign" before "tree" in the following
function signature tells Lean that even though
tree takes its type argument implicitly, in
this case we want to give it explicitly. We
need to specify T explicitly here because Lean
has no way of knowing that's what we want.
-/

def num_nodes : ∀ {T : Type}, @tree T → nat
| T tree.empty := 0
| T (tree.node n1 n2 n3) := 1 + num_nodes(n2) + num_nodes(n3)

/-
The following questions use our definition of
the nas to practice proof by induction. Here is
our nat type and the implementations of addition
and multiplication.
-/

inductive mynat : Type
| zero : mynat
| succ : mynat → mynat

def add_mynat: mynat → mynat → mynat
| mynat.zero m := m
| (mynat.succ n') m :=
    mynat.succ (add_mynat n' m)

def mult_mynat: mynat → mynat → mynat
| mynat.zero m := mynat.zero
| (mynat.succ n') m :=
    add_mynat m (mult_mynat n' m)

/-
Here's a proof that zero is a right identity
for addition. We explain details in comments.
You will want to use some of the same ideas in
your proofs.
-/

theorem zero_right_id_add : ∀ (n : mynat),
    add_mynat n mynat.zero = n :=
begin
-- forall introduction
intro n,
-- induction
induction n with n' ih,

-- base case
exact rfl,

-- recursive case
-- first simplify based on definition of add_mynat
simp [add_mynat],
-- now apply induction hypothesis
exact ih,
end

/- #5

Prove the following by induction on n in Lean.
-/

-- 5b. Prove that succ (n + m) = n + (succ m).
theorem add_succ': ∀ (n m : mynat) , mynat.succ (add_mynat n m) = add_mynat n (mynat.succ m) :=
begin
    intros n m,
    induction n with n' ih,
    simp[add_mynat],
    simp[add_mynat],
    assumption,
end

theorem add_succ : ∀ (n m : mynat),
    mynat.succ (add_mynat n m) = add_mynat n (mynat.succ m) :=
begin
    intros n m,
    induction n with n' ih,
    exact rfl,
    simp [add_mynat],
    assumption,
end

-- 5a. Prove zero is a right identity for mult.
theorem zero_right_absorb_mult' : ∀ (n : mynat),
    mult_mynat n mynat.zero = mynat.zero :=
begin
    intro n,
    induction n with n' ih,
    trivial,
    simp[mult_mynat],
    assumption,
end

theorem zero_right_absorb_mult : ∀ (n : mynat),
  mult_mynat n mynat.zero = mynat.zero :=
begin
    intros n,
    induction n with n' ih,
    exact rfl,
    induction n',
    exact rfl,
    simp [mult_mynat],
    assumption,
end

-- 5b. Prove addition is associative.
theorem addition_assoc' :
    ∀ (n m p : mynat),
        add_mynat (add_mynat n m) p =
        add_mynat n (add_mynat m p) :=
begin
    intros n m p,
    induction n with n' ih,
    trivial,
    simp[add_mynat],
    assumption,
end

theorem addition_assoc :
    ∀ (n m p : mynat),
        add_mynat (add_mynat n m) p =
        add_mynat n (add_mynat m p) :=
begin
    intros n m p,
    induction n,
    exact rfl,
    simp [add_mynat],
    assumption,
end

-- 5c. Prove addition is commutative.
lemma add_n_succ_m':
    ∀ n m : mynat,
        add_mynat n (mynat.succ m) =
            mynat.succ (add_mynat n m) :=
    begin
        intros n m,
        induction n with n' ih,
        trivial,
        simp[add_mynat],
        assumption,
    end
lemma add_n_succ_m :
    ∀ n m : mynat,
        add_mynat n (mynat.succ m) =
            mynat.succ (add_mynat n m) :=
    begin
        intros n m,
        induction n with n' h,
            apply rfl,
            simp[add_mynat],
            assumption,
    end

theorem addition_comm' :
    ∀ (n m : mynat), add_mynat n m = add_mynat m n :=
begin
    intros n m,
    induction n,
    simp[add_mynat],
    induction m,
    trivial,
    simp[add_mynat],
    assumption,
    simp[add_mynat],
    rw n_ih,
    rw add_succ,
end

theorem addition_comm :
    ∀ (n m : mynat), add_mynat n m = add_mynat m n :=
begin
    intros n m,
    induction n with n' ih,
    induction m with m' ih2,
    exact rfl,
    simp[add_mynat],
    assumption,
    simp[add_mynat],
    rw ih,
    rw add_n_succ_m,
    -- induction m with m' ih',
    --     simp [add_mynat],
    --     simp[add_mynat],

end

/- 6a.

Complete then test the following definition of
a function that computes the n'th Fibonacci
number when given n as an argument.
-/
def fib' : ℕ → ℕ
| nat.zero := 0
| (nat.succ nat.zero) := 1
| (n + 2) := fib'(n + 1) + fib'(n)

def fib : ℕ → ℕ
| nat.zero := 0
| (nat.succ nat.zero) := 1
| (n + 2 ) := (fib (n+1)) + fib n

#eval fib 8

/- 6b.

Implement the factorial function. You will need to
define the function for both its base and recursive
cases.
-/

def fac : ℕ → ℕ
| nat.zero := 1
| (nat.succ n) := (nat.succ n) * (fac n)

/- 7.

Give an *informal* proof by induction of the proposition
that forall natural numbers, n, the sum of the natural
numbers from 0 to n is n * (n + 1) / 2.

1. Let n be a number. Prove by induction
    a. Base case
        1. The sum of all numbers from 0-n is equal to n * (n + 1) / 2
        2. The sum of all numbers from 0-n is 0 if n = 0
    b. Inductive case
        1. Assume relationship is true for P(n) and prove for P(n+1)
        2. 0+1+...+(n-1)+n = n*(n + 1)/2
        3. Substitute 0+1+...+(n-1)+n  with n * (n + 1) / 2
        4. Simplify left side by commutative property: (n + 1) * (n + 2) / 2
        5. Distribute: (n^2 + 3n + 2) / 2
        6. Distribute the left side: (n^2 + 3n + 2) / 2 + (n + 1) = (n^2 + 3n + 2)
        7. Separate terms: (n^2) / (2+)n / 2 + (n+1) = (n^2) / (2+3n) / (2+2) / 2
        8. Eliminate from both sides: (n + 1) = 2n / 2 + 2 / 2
        9. Simplify: (n + 1) = n + 1
2. Proven for base and induction case, therefore this is true for all natrual numbers
-/

author: justinqcai


text:
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import order.category.BddOrd
import order.category.Lat
import order.category.Semilat

/-!
# The category of bounded lattices

This file defines `BddLat`, the category of bounded lattices.

In literature, this is sometimes called `Lat`, the category of lattices, because being a lattice is
understood to entail having a bottom and a top element.
-/

universes u

open category_theory

/-- The category of bounded lattices with bounded lattice morphisms. -/
structure BddLat :=
(to_Lat : Lat)
[is_bounded_order : bounded_order to_Lat]

namespace BddLat

instance : has_coe_to_sort BddLat Type* := ⟨λ X, X.to_Lat⟩
instance (X : BddLat) : lattice X := X.to_Lat.str

attribute [instance] BddLat.is_bounded_order

/-- Construct a bundled `BddLat` from `lattice` + `bounded_order`. -/
def of (α : Type*) [lattice α] [bounded_order α] : BddLat := ⟨⟨α⟩⟩

@[simp] lemma coe_of (α : Type*) [lattice α] [bounded_order α] : ↥(of α) = α := rfl

instance : inhabited BddLat := ⟨of punit⟩

instance : large_category.{u} BddLat :=
{ hom := λ X Y, bounded_lattice_hom X Y,
  id := λ X, bounded_lattice_hom.id X,
  comp := λ X Y Z f g, g.comp f,
  id_comp' := λ X Y, bounded_lattice_hom.comp_id,
  comp_id' := λ X Y, bounded_lattice_hom.id_comp,
  assoc' := λ W X Y Z _ _ _, bounded_lattice_hom.comp_assoc _ _ _ }

instance : concrete_category BddLat :=
{ forget := ⟨coe_sort, λ X Y, coe_fn, λ X, rfl, λ X Y Z f g, rfl⟩,
  forget_faithful := ⟨λ X Y, by convert fun_like.coe_injective⟩ }

instance has_forget_to_BddOrd : has_forget₂ BddLat BddOrd :=
{ forget₂ := { obj := λ X, BddOrd.of X,
               map := λ X Y, bounded_lattice_hom.to_bounded_order_hom } }

instance has_forget_to_Lat : has_forget₂ BddLat Lat :=
{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y, bounded_lattice_hom.to_lattice_hom } }

instance has_forget_to_SemilatSup : has_forget₂ BddLat SemilatSup :=
{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y, bounded_lattice_hom.to_sup_bot_hom } }

instance has_forget_to_SemilatInf : has_forget₂ BddLat SemilatInf :=
{ forget₂ := { obj := λ X, ⟨X⟩, map := λ X Y, bounded_lattice_hom.to_inf_top_hom } }

@[simp] lemma coe_forget_to_BddOrd (X : BddLat) :
  ↥((forget₂ BddLat BddOrd).obj X) = ↥X := rfl

@[simp] lemma coe_forget_to_Lat (X : BddLat) :
  ↥((forget₂ BddLat Lat).obj X) = ↥X := rfl

@[simp] lemma coe_forget_to_SemilatSup (X : BddLat) :
  ↥((forget₂ BddLat SemilatSup).obj X) = ↥X := rfl

@[simp] lemma coe_forget_to_SemilatInf (X : BddLat) :
  ↥((forget₂ BddLat SemilatInf).obj X) = ↥X := rfl

lemma forget_Lat_PartOrd_eq_forget_BddOrd_PartOrd :
  forget₂ BddLat Lat ⋙ forget₂ Lat PartOrd =
    forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd := rfl

lemma forget_SemilatSup_PartOrd_eq_forget_BddOrd_PartOrd :
  forget₂ BddLat SemilatSup ⋙ forget₂ SemilatSup PartOrd =
    forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd := rfl

lemma forget_SemilatInf_PartOrd_eq_forget_BddOrd_PartOrd :
  forget₂ BddLat SemilatInf ⋙ forget₂ SemilatInf PartOrd =
    forget₂ BddLat BddOrd ⋙ forget₂ BddOrd PartOrd := rfl

/-- Constructs an equivalence between bounded lattices from an order isomorphism
between them. -/
@[simps] def iso.mk {α β : BddLat.{u}} (e : α ≃o β) : α ≅ β :=
{ hom := e,
  inv := e.symm,
  hom_inv_id' := by { ext, exact e.symm_apply_apply _ },
  inv_hom_id' := by { ext, exact e.apply_symm_apply _ } }

/-- `order_dual` as a functor. -/
@[simps] def dual : BddLat ⥤ BddLat :=
{ obj := λ X, of Xᵒᵈ, map := λ X Y, bounded_lattice_hom.dual }

/-- The equivalence between `BddLat` and itself induced by `order_dual` both ways. -/
@[simps functor inverse] def dual_equiv : BddLat ≌ BddLat :=
equivalence.mk dual dual
  (nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)
  (nat_iso.of_components (λ X, iso.mk $ order_iso.dual_dual X) $ λ X Y f, rfl)

end BddLat

lemma BddLat_dual_comp_forget_to_BddOrd :
  BddLat.dual ⋙ forget₂ BddLat BddOrd =
    forget₂ BddLat BddOrd ⋙ BddOrd.dual := rfl

lemma BddLat_dual_comp_forget_to_Lat :
  BddLat.dual ⋙ forget₂ BddLat Lat =
    forget₂ BddLat Lat ⋙ Lat.dual := rfl

lemma BddLat_dual_comp_forget_to_SemilatSup :
  BddLat.dual ⋙ forget₂ BddLat SemilatSup =
    forget₂ BddLat SemilatInf ⋙ SemilatInf.dual := rfl

lemma BddLat_dual_comp_forget_to_SemilatInf :
  BddLat.dual ⋙ forget₂ BddLat SemilatInf =
    forget₂ BddLat SemilatSup ⋙ SemilatSup.dual := rfl

author: leanprover-community

repo: mathlib


text:
example (P Q R : Prop) (HP : P) (HQ : Q) : P :=
begin
  sorry,
end

theorem easy (P Q : Prop) (HP : P) (HPQ : P → Q) : Q :=
begin
  sorry
end

theorem prove_P_implies_Q (P Q : Prop) (HQ : Q) : P → Q :=
begin
  sorry,
end

theorem P_implies_P (P : Prop) : P → P :=
begin
  sorry,
end

theorem needs_intros (P Q R : Prop) (HR : R) : P → (Q → R) :=
begin
  sorry,
end

theorem very_easy : true :=
begin
  sorry
end

theorem false_implies_false : false → false :=
begin
  sorry
end

theorem not_not (P : Prop) : P → ¬ (¬ P) :=
begin
  sorry,
end

author: kbuzzard

repo: xena

save_path: github-repos/lean/kbuzzard-xena


text:
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
-/
import algebra.char_p.two
import data.nat.factorization.basic
import data.nat.periodic
import data.zmod.basic

/-!
# Euler's totient function

This file defines [Euler's totient function](https://en.wikipedia.org/wiki/Euler's_totient_function)
`nat.totient n` which counts the number of naturals less than `n` that are coprime with `n`.
We prove the divisor sum formula, namely that `n` equals `φ` summed over the divisors of `n`. See
`sum_totient`. We also prove two lemmas to help compute totients, namely `totient_mul` and
`totient_prime_pow`.
-/

open finset
open_locale big_operators

namespace nat

/-- Euler's totient function. This counts the number of naturals strictly less than `n` which are
coprime with `n`. -/
def totient (n : ℕ) : ℕ := ((range n).filter n.coprime).card

localized "notation (name := nat.totient) `φ` := nat.totient" in nat

@[simp] theorem totient_zero : φ 0 = 0 := rfl

@[simp] theorem totient_one : φ 1 = 1 :=
by simp [totient]

lemma totient_eq_card_coprime (n : ℕ) : φ n = ((range n).filter n.coprime).card := rfl

/-- A characterisation of `nat.totient` that avoids `finset`. -/
lemma totient_eq_card_lt_and_coprime (n : ℕ) : φ n = nat.card {m | m < n ∧ n.coprime m} :=
begin
  let e : {m | m < n ∧ n.coprime m} ≃ finset.filter n.coprime (finset.range n) :=
  { to_fun  := λ m, ⟨m, by simpa only [finset.mem_filter, finset.mem_range] using m.property⟩,
    inv_fun := λ m, ⟨m, by simpa only [finset.mem_filter, finset.mem_range] using m.property⟩,
    left_inv  := λ m, by simp only [subtype.coe_mk, subtype.coe_eta],
    right_inv := λ m, by simp only [subtype.coe_mk, subtype.coe_eta] },
  rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, fintype.card_coe],
end

lemma totient_le (n : ℕ) : φ n ≤ n :=
((range n).card_filter_le _).trans_eq (card_range n)

lemma totient_lt (n : ℕ) (hn : 1 < n) : φ n < n :=
(card_lt_card (filter_ssubset.2 ⟨0, by simp [hn.ne', pos_of_gt hn]⟩)).trans_eq (card_range n)

lemma totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n
| 0 := dec_trivial
| 1 := by simp [totient]
| (n+2) := λ h, card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 dec_trivial, coprime_one_right _⟩⟩

lemma filter_coprime_Ico_eq_totient (a n : ℕ) :
  ((Ico n (n+a)).filter (coprime a)).card = totient a :=
begin
  rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range],
  exact periodic_coprime a,
end

lemma Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_pos : 0 < a) :
  ((Ico k (k + n)).filter (coprime a)).card ≤ totient a * (n / a + 1) :=
begin
  conv_lhs { rw ←nat.mod_add_div n a },
  induction n / a with i ih,
  { rw ←filter_coprime_Ico_eq_totient a k,
    simp only [add_zero, mul_one, mul_zero, le_of_lt (mod_lt n a_pos)],
    mono,
    refine monotone_filter_left a.coprime _,
    simp only [finset.le_eq_subset],
    exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n a_pos)) k), },
  simp only [mul_succ],
  simp_rw ←add_assoc at ih ⊢,
  calc (filter a.coprime (Ico k (k + n % a + a * i + a))).card
      = (filter a.coprime (Ico k (k + n % a + a * i)
                            ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))).card :
        begin
          congr,
          rw Ico_union_Ico_eq_Ico,
          rw add_assoc,
          exact le_self_add,
          exact le_self_add,
        end
  ... ≤ (filter a.coprime (Ico k (k + n % a + a * i))).card + a.totient :
        begin
          rw [filter_union, ←filter_coprime_Ico_eq_totient a (k + n % a + a * i)],
          apply card_union_le,
        end
  ... ≤ a.totient * i + a.totient + a.totient : add_le_add_right ih (totient a),
end

open zmod

/-- Note this takes an explicit `fintype ((zmod n)ˣ)` argument to avoid trouble with instance
diamonds. -/
@[simp] lemma _root_.zmod.card_units_eq_totient (n : ℕ) [ne_zero n] [fintype ((zmod n)ˣ)] :
  fintype.card ((zmod n)ˣ) = φ n :=
calc fintype.card ((zmod n)ˣ) = fintype.card {x : zmod n // x.val.coprime n} :
  fintype.card_congr zmod.units_equiv_coprime
... = φ n :
begin
  unfreezingI { obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero ne_zero.out },
  simp only [totient, finset.card_eq_sum_ones, fintype.card_subtype, finset.sum_filter,
    ← fin.sum_univ_eq_sum_range, @nat.coprime_comm (m + 1)],
  refl
end

lemma totient_even {n : ℕ} (hn : 2 < n) : even n.totient :=
begin
  haveI : fact (1 < n) := ⟨one_lt_two.trans hn⟩,
  haveI : ne_zero n := ne_zero.of_gt hn,
  suffices : 2 = order_of (-1 : (zmod n)ˣ),
  { rw [← zmod.card_units_eq_totient, even_iff_two_dvd, this], exact order_of_dvd_card_univ },
  rw [←order_of_units, units.coe_neg_one, order_of_neg_one, ring_char.eq (zmod n) n, if_neg hn.ne'],
end

lemma totient_mul {m n : ℕ} (h : m.coprime n) : φ (m * n) = φ m * φ n :=
if hmn0 : m * n = 0
  then by cases nat.mul_eq_zero.1 hmn0 with h h;
    simp only [totient_zero, mul_zero, zero_mul, h]
  else
  begin
    haveI : ne_zero (m * n) := ⟨hmn0⟩,
    haveI : ne_zero m := ⟨left_ne_zero_of_mul hmn0⟩,
    haveI : ne_zero n := ⟨right_ne_zero_of_mul hmn0⟩,
    simp only [← zmod.card_units_eq_totient],
    rw [fintype.card_congr (units.map_equiv (zmod.chinese_remainder h).to_mul_equiv).to_equiv,
      fintype.card_congr (@mul_equiv.prod_units (zmod m) (zmod n) _ _).to_equiv,
      fintype.card_prod]
  end

/-- For `d ∣ n`, the totient of `n/d` equals the number of values `k < n` such that `gcd n k = d` -/
lemma totient_div_of_dvd {n d : ℕ} (hnd : d ∣ n) :
  φ (n/d) = (filter (λ (k : ℕ), n.gcd k = d) (range n)).card :=
begin
  rcases d.eq_zero_or_pos with rfl | hd0, { simp [eq_zero_of_zero_dvd hnd] },
  rcases hnd with ⟨x, rfl⟩,
  rw nat.mul_div_cancel_left x hd0,
  apply finset.card_congr (λ k _, d * k),
  { simp only [mem_filter, mem_range, and_imp, coprime],
    refine λ a ha1 ha2, ⟨(mul_lt_mul_left hd0).2 ha1, _⟩,
    rw [gcd_mul_left, ha2, mul_one] },
  { simp [hd0.ne'] },
  { simp only [mem_filter, mem_range, exists_prop, and_imp],
    refine λ b hb1 hb2, _,
    have : d ∣ b, { rw ←hb2, apply gcd_dvd_right },
    rcases this with ⟨q, rfl⟩,
    refine ⟨q, ⟨⟨(mul_lt_mul_left hd0).1 hb1, _⟩, rfl⟩⟩,
    rwa [gcd_mul_left, mul_right_eq_self_iff hd0] at hb2 },
end

lemma sum_totient' (n : ℕ) : ∑ m in (range n.succ).filter (∣ n), φ m = n :=
begin
  convert sum_totient _ using 1,
  simp only [nat.divisors, sum_filter, range_eq_Ico],
  rw sum_eq_sum_Ico_succ_bot; simp
end

/-- When `p` is prime, then the totient of `p ^ (n + 1)` is `p ^ n * (p - 1)` -/
lemma totient_prime_pow_succ {p : ℕ} (hp : p.prime) (n : ℕ) :
  φ (p ^ (n + 1)) = p ^ n * (p - 1) :=
calc φ (p ^ (n + 1))
    = ((range (p ^ (n + 1))).filter (coprime (p ^ (n + 1)))).card :
  totient_eq_card_coprime _
... = (range (p ^ (n + 1)) \ ((range (p ^ n)).image (* p))).card :
  congr_arg card begin
    rw [sdiff_eq_filter],
    apply filter_congr,
    simp only [mem_range, mem_filter, coprime_pow_left_iff n.succ_pos,
      mem_image, not_exists, hp.coprime_iff_not_dvd],
    intros a ha,
    split,
    { rintros hap b _ rfl,
      exact hap (dvd_mul_left _ _) },
    { rintros h ⟨b, rfl⟩,
      rw [pow_succ] at ha,
      exact h b (lt_of_mul_lt_mul_left ha (zero_le _)) (mul_comm _ _) }
  end
... = _ :
have h1 : function.injective (* p),
  from mul_left_injective₀ hp.ne_zero,
have h2 : (range (p ^ n)).image (* p) ⊆ range (p ^ (n + 1)),
  from λ a, begin
    simp only [mem_image, mem_range, exists_imp_distrib],
    rintros b h rfl,
    rw [pow_succ'],
    exact (mul_lt_mul_right hp.pos).2 h
  end,
begin
  rw [card_sdiff h2, card_image_of_inj_on (h1.inj_on _), card_range,
    card_range, ← one_mul (p ^ n), pow_succ, ← tsub_mul,
    one_mul, mul_comm]
end

/-- When `p` is prime, then the totient of `p ^ n` is `p ^ (n - 1) * (p - 1)` -/
lemma totient_prime_pow {p : ℕ} (hp : p.prime) {n : ℕ} (hn : 0 < n) :
  φ (p ^ n) = p ^ (n - 1) * (p - 1) :=
by rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩;
  exact totient_prime_pow_succ hp _

lemma totient_prime {p : ℕ} (hp : p.prime) : φ p = p - 1 :=
by rw [← pow_one p, totient_prime_pow hp]; simp

lemma totient_eq_iff_prime {p : ℕ} (hp : 0 < p) : p.totient = p - 1 ↔ p.prime :=
begin
  refine ⟨λ h, _, totient_prime⟩,
  replace hp : 1 < p,
  { apply lt_of_le_of_ne,
    { rwa succ_le_iff },
    { rintro rfl,
      rw [totient_one, tsub_self] at h,
      exact one_ne_zero h } },
  rw [totient_eq_card_coprime, range_eq_Ico, ←Ico_insert_succ_left hp.le, finset.filter_insert,
      if_neg (not_coprime_of_dvd_of_dvd hp (dvd_refl p) (dvd_zero p)), ←nat.card_Ico 1 p] at h,
  refine p.prime_of_coprime hp (λ n hn hnz, finset.filter_card_eq h n $ finset.mem_Ico.mpr ⟨_, hn⟩),
  rwa [succ_le_iff, pos_iff_ne_zero],
end

lemma card_units_zmod_lt_sub_one {p : ℕ} (hp : 1 < p) [fintype ((zmod p)ˣ)] :
  fintype.card ((zmod p)ˣ) ≤ p - 1 :=
begin
  haveI : ne_zero p := ⟨(pos_of_gt hp).ne'⟩,
  rw zmod.card_units_eq_totient p,
  exact nat.le_pred_of_lt (nat.totient_lt p hp),
end

lemma prime_iff_card_units (p : ℕ) [fintype ((zmod p)ˣ)] :
  p.prime ↔ fintype.card ((zmod p)ˣ) = p - 1 :=
begin
  casesI eq_zero_or_ne_zero p with hp hp,
  { substI hp,
    simp only [zmod, not_prime_zero, false_iff, zero_tsub],
    -- the substI created an non-defeq but subsingleton instance diamond; resolve it
    suffices : fintype.card ℤˣ ≠ 0, { convert this },
    simp },
  rw [zmod.card_units_eq_totient, nat.totient_eq_iff_prime $ ne_zero.pos p],
end

@[simp] lemma totient_two : φ 2 = 1 :=
(totient_prime prime_two).trans rfl

lemma totient_eq_one_iff : ∀ {n : ℕ}, n.totient = 1 ↔ n = 1 ∨ n = 2
| 0 := by simp
| 1 := by simp
| 2 := by simp
| (n+3) :=
begin
  have : 3 ≤ n + 3 := le_add_self,
  simp only [succ_succ_ne_one, false_or],
  exact ⟨λ h, not_even_one.elim $ h ▸ totient_even this, by rintro ⟨⟩⟩,
end

/-! ### Euler's product formula for the totient function

We prove several different statements of this formula. -/

/-- Euler's product formula for the totient function. -/
theorem totient_eq_prod_factorization {n : ℕ} (hn : n ≠ 0) :
  φ n = n.factorization.prod (λ p k, p ^ (k - 1) * (p - 1)) :=
begin
  rw multiplicative_factorization φ @totient_mul totient_one hn,
  apply finsupp.prod_congr (λ p hp, _),
  have h := zero_lt_iff.mpr (finsupp.mem_support_iff.mp hp),
  rw [totient_prime_pow (prime_of_mem_factorization hp) h],
end

/-- Euler's product formula for the totient function. -/
theorem totient_mul_prod_factors (n : ℕ) :
  φ n * ∏ p in n.factors.to_finset, p = n * ∏ p in n.factors.to_finset, (p - 1) :=
begin
  by_cases hn : n = 0, { simp [hn] },
  rw totient_eq_prod_factorization hn,
  nth_rewrite 2 ←factorization_prod_pow_eq_self hn,
  simp only [←prod_factorization_eq_prod_factors, ←finsupp.prod_mul],
  refine finsupp.prod_congr (λ p hp, _),
  rw [finsupp.mem_support_iff, ← zero_lt_iff] at hp,
  rw [mul_comm, ←mul_assoc, ←pow_succ, nat.sub_add_cancel hp],
end

/-- Euler's product formula for the totient function. -/
theorem totient_eq_div_factors_mul (n : ℕ) :
  φ n = n / (∏ p in n.factors.to_finset, p) * (∏ p in n.factors.to_finset, (p - 1)) :=
begin
  rw [← mul_div_left n.totient, totient_mul_prod_factors, mul_comm,
      nat.mul_div_assoc _ (prod_prime_factors_dvd n), mul_comm],
  simpa [prod_factorization_eq_prod_factors] using prod_pos (λ p, pos_of_mem_factorization),
end

/-- Euler's product formula for the totient function. -/
theorem totient_eq_mul_prod_factors (n : ℕ) :
  (φ n : ℚ) = n * ∏ p in n.factors.to_finset, (1 - p⁻¹) :=
begin
  by_cases hn : n = 0, { simp [hn] },
  have hn' : (n : ℚ) ≠ 0, { simp [hn] },
  have hpQ : ∏ p in n.factors.to_finset, (p : ℚ) ≠ 0,
  { rw [←cast_prod, cast_ne_zero, ←zero_lt_iff, ←prod_factorization_eq_prod_factors],
    exact prod_pos (λ p hp, pos_of_mem_factorization hp) },
  simp only [totient_eq_div_factors_mul n, prod_prime_factors_dvd n, cast_mul, cast_prod,
      cast_div_char_zero, mul_comm_div, mul_right_inj' hn', div_eq_iff hpQ, ←prod_mul_distrib],
  refine prod_congr rfl (λ p hp, _),
  have hp := pos_of_mem_factors (list.mem_to_finset.mp hp),
  have hp' : (p : ℚ) ≠ 0 := cast_ne_zero.mpr hp.ne.symm,
  rw [sub_mul, one_mul, mul_comm, mul_inv_cancel hp', cast_pred hp],
end

lemma totient_gcd_mul_totient_mul (a b : ℕ) : φ (a.gcd b) * φ (a * b) = φ a * φ b * (a.gcd b) :=
begin
  have shuffle : ∀ a1 a2 b1 b2 c1 c2 : ℕ, b1 ∣ a1 → b2 ∣ a2 →
    (a1/b1 * c1) * (a2/b2 * c2) = (a1*a2)/(b1*b2) * (c1*c2),
  { intros a1 a2 b1 b2 c1 c2 h1 h2,
    calc
      (a1/b1 * c1) * (a2/b2 * c2) = ((a1/b1) * (a2/b2)) * (c1*c2) : by apply mul_mul_mul_comm
      ... = (a1*a2)/(b1*b2) * (c1*c2) : by { congr' 1, exact div_mul_div_comm h1 h2 } },
  simp only [totient_eq_div_factors_mul],
  rw [shuffle, shuffle],
  rotate, repeat { apply prod_prime_factors_dvd },
  { simp only [prod_factors_gcd_mul_prod_factors_mul],
    rw [eq_comm, mul_comm, ←mul_assoc, ←nat.mul_div_assoc],
    exact mul_dvd_mul (prod_prime_factors_dvd a) (prod_prime_factors_dvd b) }
end

lemma totient_super_multiplicative (a b : ℕ) : φ a * φ b ≤ φ (a * b) :=
begin
  let d := a.gcd b,
  rcases (zero_le a).eq_or_lt with rfl | ha0, { simp },
  have hd0 : 0 < d, from nat.gcd_pos_of_pos_left _ ha0,
  rw [←mul_le_mul_right hd0, ←totient_gcd_mul_totient_mul a b, mul_comm],
  apply mul_le_mul_left' (nat.totient_le d),
end

lemma totient_dvd_of_dvd {a b : ℕ} (h : a ∣ b) : φ a ∣ φ b :=
begin
  rcases eq_or_ne a 0 with rfl | ha0, { simp [zero_dvd_iff.1 h] },
  rcases eq_or_ne b 0 with rfl | hb0, { simp },
  have hab' : a.factorization.support ⊆ b.factorization.support,
  { intro p,
    simp only [support_factorization, list.mem_to_finset],
    apply factors_subset_of_dvd h hb0 },
  rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0],
  refine finsupp.prod_dvd_prod_of_subset_of_dvd hab' (λ p hp, mul_dvd_mul _ dvd_rfl),
  exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1),
end

lemma totient_mul_of_prime_of_dvd {p n : ℕ} (hp : p.prime) (h : p ∣ n) :
  (p * n).totient = p * n.totient :=
begin
  have h1 := totient_gcd_mul_totient_mul p n,
  rw [(gcd_eq_left h), mul_assoc] at h1,
  simpa [(totient_pos hp.pos).ne', mul_comm] using h1,
end

lemma totient_mul_of_prime_of_not_dvd {p n : ℕ} (hp : p.prime) (h : ¬ p ∣ n) :
  (p * n).totient = (p - 1) * n.totient :=
begin
  rw [totient_mul _, totient_prime hp],
  simpa [h] using coprime_or_dvd_of_prime hp n,
end

end nat


text:
/-
Copyright (c) 2018 Simon Hudon. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Simon Hudon
-/
import data.dlist
import tactic.core

namespace tactic
open expr list

meta def match_fn (fn : expr) : expr → tactic (expr × expr)
| (app (app fn' e₀) e₁) := unify fn fn' $> (e₀, e₁)
| _ := failed

meta def fill_args : expr → tactic (expr × list expr)
| (pi n bi d b) :=
do v ← mk_meta_var d,
   (r, vs) ← fill_args (b.instantiate_var v),
   return (r, v::vs)
| e := return (e, [])

meta def mk_assoc_pattern' (fn : expr) : expr → tactic (dlist expr)
| e :=
  (do (e₀, e₁) ← match_fn fn e,
      (++) <$> mk_assoc_pattern' e₀ <*> mk_assoc_pattern' e₁) <|>
  pure (dlist.singleton e)

meta def mk_assoc_pattern (fn e : expr) : tactic (list expr) :=
dlist.to_list <$> mk_assoc_pattern' fn e

meta def mk_assoc (fn : expr) : list expr → tactic expr
| [] := failed
| [x] := pure x
| (x₀ :: x₁ :: xs) := mk_assoc (fn x₀ x₁ :: xs)

meta def chain_eq_trans : list expr → tactic expr
| [] := to_expr ``(rfl)
| [e] := pure e
| (e :: es) := chain_eq_trans es >>= mk_eq_trans e

meta def unify_prefix : list expr → list expr → tactic unit
| [] _ := pure ()
| _ [] := failed
| (x :: xs) (y :: ys) :=
unify x y >> unify_prefix xs ys

meta def match_assoc_pattern' (p : list expr) : list expr → tactic (list expr × list expr) | es :=
unify_prefix p es $> ([], es.drop p.length) <|>
  match es with
  | [] := failed
  | (x :: xs) := prod.map (cons x) id <$> match_assoc_pattern' xs
  end

meta def match_assoc_pattern (fn p e : expr) : tactic (list expr × list expr) :=
do p' ← mk_assoc_pattern fn p,
   e' ← mk_assoc_pattern fn e,
   match_assoc_pattern' p' e'

meta def mk_eq_proof (fn : expr) (e₀ e₁ : list expr) (p : expr) : tactic (expr × expr × expr) :=
do (l, r) ← infer_type p >>= match_eq,
   if e₀.empty ∧ e₁.empty then pure (l, r, p)
   else do
     l' ← mk_assoc fn (e₀ ++ [l] ++ e₁),
     r' ← mk_assoc fn (e₀ ++ [r] ++ e₁),
     t  ← infer_type l',
     v  ← mk_local_def `x t,
     e  ← mk_assoc fn (e₀ ++ [v] ++ e₁),
     p  ← mk_congr_arg (e.lambdas [v]) p,
     p' ← mk_id_eq l' r' p,
     return (l', r', p')

meta def assoc_root (fn assoc : expr) : expr → tactic (expr × expr) | e :=
(do (e₀, e₁) ← match_fn fn e,
    (ea, eb) ← match_fn fn e₁,
    let e' := fn (fn e₀ ea) eb,
    p' ← mk_eq_symm (assoc e₀ ea eb),
    (e'', p'') ← assoc_root e',
    prod.mk e'' <$> mk_eq_trans p' p'') <|>
prod.mk e <$> mk_eq_refl e

meta def assoc_refl' (fn assoc : expr) : expr → expr → tactic expr
| l r := (is_def_eq l r >> mk_eq_refl l) <|> do
  (l', l_p)  ← assoc_root fn assoc l <|> fail "A",
  (el₀, el₁) ← match_fn   fn l' <|> fail "B",
  (r', r_p)  ← assoc_root fn assoc r <|> fail "C",
  (er₀, er₁) ← match_fn   fn r' <|> fail "D",
  p₀ ← assoc_refl' el₀ er₀,
  p₁ ← is_def_eq el₁ er₁ >> mk_eq_refl el₁,
  f_eq ← mk_congr_arg fn p₀ <|> fail "G",
  p' ← mk_congr f_eq p₁ <|> fail "H",
  r_p' ← mk_eq_symm r_p,
  chain_eq_trans [l_p, p', r_p']

meta def assoc_refl (fn : expr) : tactic unit :=
do (l, r) ← target >>= match_eq,
   assoc ← mk_mapp ``is_associative.assoc [none, fn, none]
     <|> fail format!"{fn} is not associative",
   assoc_refl' fn assoc l r >>= tactic.exact

meta def flatten (fn assoc e : expr) : tactic (expr × expr) :=
do ls ← mk_assoc_pattern fn e,
   e' ← mk_assoc fn ls,
   p  ← assoc_refl' fn assoc e e',
   return (e', p)

meta def assoc_rewrite_intl (assoc h e : expr) : tactic (expr × expr) :=
do t ← infer_type h,
   (lhs, rhs) ← match_eq t,
   let fn  := lhs.app_fn.app_fn,
   (l, r) ← match_assoc_pattern fn lhs e,
   (lhs', rhs', h') ← mk_eq_proof fn l r h,
   e_p ← assoc_refl' fn assoc e lhs',
   (rhs'', rhs_p) ← flatten fn assoc rhs',
   final_p ← chain_eq_trans [e_p, h', rhs_p],
   return (rhs'', final_p)

-- TODO(Simon): visit expressions built of `fn` nested inside other such expressions:
-- e.g.: x + f (a + b + c) + y should generate two rewrite candidates
meta def enum_assoc_subexpr' (fn : expr) : expr → tactic (dlist expr)
| e :=
  dlist.singleton e <$ (match_fn fn e >> guard (¬ e.has_var)) <|>
  expr.mfoldl (λ es e', (++ es) <$> enum_assoc_subexpr' e') dlist.empty e

meta def enum_assoc_subexpr (fn e : expr) : tactic (list expr) :=
dlist.to_list <$> enum_assoc_subexpr' fn e

meta def mk_assoc_instance (fn : expr) : tactic expr :=
do t ← mk_mapp ``is_associative [none, fn],
   inst ← prod.snd <$> solve_aux t assumption <|>
     (mk_instance t >>= assertv `_inst t) <|>
     fail format!"{fn} is not associative",
   mk_mapp ``is_associative.assoc [none, fn, inst]

meta def assoc_rewrite (h e : expr) (opt_assoc : option expr := none) :
  tactic (expr × expr × list expr) :=
do (t, vs) ← infer_type h >>= fill_args,
   (lhs, rhs) ← match_eq t,
   let fn := lhs.app_fn.app_fn,
   es ← enum_assoc_subexpr fn e,
   assoc ← match opt_assoc with
           | none := mk_assoc_instance fn
           | (some assoc) := pure assoc
           end,
   (_, p) ← mfirst (assoc_rewrite_intl assoc $ h.mk_app vs) es,
   (e', p', _) ← tactic.rewrite p e,
   pure (e', p', vs)

meta def assoc_rewrite_target (h : expr) (opt_assoc : option expr :=  none) :
  tactic unit :=
do tgt ← target,
   (tgt', p, _) ← assoc_rewrite h tgt opt_assoc,
   replace_target tgt' p

meta def assoc_rewrite_hyp (h hyp : expr) (opt_assoc : option expr := none) :
  tactic expr :=
do tgt ← infer_type hyp,
   (tgt', p, _) ← assoc_rewrite h tgt opt_assoc,
   replace_hyp hyp tgt' p

namespace interactive

open lean.parser interactive interactive.types tactic

private meta def assoc_rw_goal (rs : list rw_rule) : tactic unit :=
rs.mmap' $ λ r, do
 save_info r.pos,
 eq_lemmas ← get_rule_eqn_lemmas r,
 orelse'
   (do e ← to_expr' r.rule, assoc_rewrite_target e)
   (eq_lemmas.mfirst $ λ n, do e ← mk_const n, assoc_rewrite_target e)
   (eq_lemmas.empty)

private meta def uses_hyp (e : expr) (h : expr) : bool :=
e.fold ff $ λ t _ r, r || (t = h)

private meta def assoc_rw_hyp : list rw_rule → expr → tactic unit
| []      hyp := skip
| (r::rs) hyp := do
  save_info r.pos,
  eq_lemmas ← get_rule_eqn_lemmas r,
  orelse'
    (do e ← to_expr' r.rule, when (¬ uses_hyp e hyp) $ assoc_rewrite_hyp e hyp >>= assoc_rw_hyp rs)
    (eq_lemmas.mfirst $ λ n, do e ← mk_const n, assoc_rewrite_hyp e hyp >>= assoc_rw_hyp rs)
    (eq_lemmas.empty)

private meta def assoc_rw_core (rs : parse rw_rules) (loca : parse location) : tactic unit :=
match loca with
| loc.wildcard := loca.try_apply (assoc_rw_hyp rs.rules) (assoc_rw_goal rs.rules)
| _            := loca.apply (assoc_rw_hyp rs.rules) (assoc_rw_goal rs.rules)
end >> try reflexivity
    >> try (returnopt rs.end_pos >>= save_info)

/--
`assoc_rewrite [h₀,← h₁] at ⊢ h₂` behaves like `rewrite [h₀,← h₁] at ⊢ h₂`
with the exception that associativity is used implicitly to make rewriting
possible.

It works for any function `f` for which an `is_associative f` instance can be found.

```
example {α : Type*} (f : α → α → α) [is_associative α f] (a b c d x : α) :
  let infix `~` := f in
  b ~ c = x → (a ~ b ~ c ~ d) = (a ~ x ~ d) :=
begin
  intro h,
  assoc_rw h,
end
```
-/
meta def assoc_rewrite (q : parse rw_rules) (l : parse location) : tactic unit :=
propagate_tags (assoc_rw_core q l)

/-- synonym for `assoc_rewrite` -/
meta def assoc_rw (q : parse rw_rules) (l : parse location) : tactic unit :=
assoc_rewrite q l

add_tactic_doc
{ name                     := "assoc_rewrite",
  category                 := doc_category.tactic,
  decl_names               := [`tactic.interactive.assoc_rewrite, `tactic.interactive.assoc_rw],
  tags                     := ["rewriting"],
  inherit_description_from := `tactic.interactive.assoc_rewrite }

end interactive
end tactic

author: JLimperg


text:
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Mathlib.Init.SetNotation
import Mathlib.Init.Data.List.Basic

/-!
# Extra definitions on `Option`

This file defines more operations involving `Option α`. Lemmas about them are located in other
files under `Data.Option.`.
Other basic operations on `Option` are defined in the core library.
-/

namespace Option

variable {α : Type _} {β : Type _}

/-- An elimination principle for `Option`. It is a nondependent version of `Option.rec_on`. -/
@[simp]
protected def elim : Option α → β → (α → β) → β
| some x, y, f => f x
| none, y, f => y

instance : Membership α (Option α) :=
  ⟨fun a b => b = some a⟩

@[simp]
theorem mem_def {a : α} {b : Option α} : a ∈ b ↔ b = some a :=
  Iff.rfl

theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = a :=
  Iff.rfl

theorem isNone_iff_eq_none {o : Option α} : o.isNone ↔ o = none :=
  ⟨Option.eq_none_of_isNone, fun e => e.symm ▸ rfl⟩

theorem some_inj {a b : α} : some a = some b ↔ a = b := by simp

/--
`o = none` is decidable even if the wrapped type does not have decidable equality.
This is not an instance because it is not definitionally equal to `Option.decidable_eq`.
Try to use `o.is_none` or `o.is_some` instead.
-/
@[inline]
def decidable_eq_none {o : Option α} : Decidable (o = none) :=
  decidable_of_decidable_of_iff isNone_iff_eq_none

instance decidable_forall_mem {p : α → Prop} [DecidablePred p] :
  ∀ o : Option α, Decidable (∀ a ∈ o, p a)
| none => isTrue (by simp)
| some a =>
  if h : p a then isTrue fun o e => some_inj.1 e ▸ h
  else isFalse $ mt (fun H => H _ rfl) h

instance decidable_exists_mem {p : α → Prop} [DecidablePred p] : ∀ o : Option α, Decidable (∃ a ∈ o, p a)
| none => isFalse fun ⟨a, ⟨h, _⟩⟩ => by cases h
| some a => if h : p a then isTrue ⟨_, rfl, h⟩ else isFalse fun ⟨_, ⟨rfl, hn⟩⟩ => h hn

/-- `guard p a` returns `some a` if `p a` holds, otherwise `none`. -/
def guard (p : α → Prop) [DecidablePred p] (a : α) : Option α :=
  if p a then some a else none

/-- Cast of `Option` to `List`. Returns `[a]` if the input is `some a`, and `[]` if it is
`none`. -/
def toList : Option α → List α
| none => []
| some a => [a]

@[simp]
theorem mem_toList {a : α} {o : Option α} : a ∈ toList o ↔ a ∈ o := by
  cases o <;> simp [toList, eq_comm]

/-- Two arguments failsafe function. Returns `f a b` if the inputs are `some a` and `some b`, and
"does nothing" otherwise. -/
def lift_or_get (f : α → α → α) : Option α → Option α → Option α
| none, none => none
| some a, none => some a
| none, some b => some b
| some a, some b => some (f a b)

/-- Lifts a relation `α → β → Prop` to a relation `option α → option β → Prop` by just adding
`none ~ none`. -/
inductive rel (r : α → β → Prop) : Option α → Option β → Prop
| /-- If `a ~ b`, then `some a ~ some b` -/
  some {a b} : r a b → rel r (some a) (some b)
| /-- `none ~ none` -/
  none : rel r none none

/-- Partial bind. If for some `x : option α`, `f : Π (a : α), a ∈ x → option β` is a
  partial function defined on `a : α` giving an `option β`, where `some a = x`,
  then `pbind x f h` is essentially the same as `bind x f`
  but is defined only when all `x = some a`, using the proof to apply `f`. -/
@[simp]
def pbind : ∀ x : Option α, (∀ a : α, a ∈ x → Option β) → Option β
| none, _ => none
| some a, f => f a rfl

-- ././Mathport/Syntax/Translate/Basic.lean:452:2: warning: expanding binder collection (a «expr ∈ » x)
/-- Partial map. If `f : Π a, p a → β` is a partial function defined on `a : α` satisfying `p`,
then `pmap f x h` is essentially the same as `map f x` but is defined only when all members of `x`
satisfy `p`, using the proof to apply `f`. -/
@[simp]
def pmap {p : α → Prop} (f : ∀ a : α, p a → β) : ∀ x : Option α, (∀ a ∈ x, p a) → Option β
| none, _ => none
| some a, H => some (f a (H a (mem_def.mpr rfl)))

/-- Flatten an `option` of `option`, a specialization of `mjoin`. -/
@[simp]
def join : Option (Option α) → Option α :=
  fun x => x.bind id

protected def traverse.{u, v} {F : Type u → Type v} [Applicative F] {α β : Type _} (f : α → F β) :
  Option α → F (Option β)
| none => pure none
| some x => some <$> f x

/-- If you maybe have a monadic computation in a `[monad m]` which produces a term of type `α`, then
there is a naturally associated way to always perform a computation in `m` which maybe produces a
result. -/
def maybe.{u, v} {m : Type u → Type v} [Monad m] {α : Type u} : Option (m α) → m (Option α)
| none => pure none
| some fn => some <$> fn

/-- Map a monadic function `f : α → m β` over an `o : option α`, maybe producing a result. -/
def mmap.{u, v, w} {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (o : Option α) :
  m (Option β) :=
  (o.map f).maybe

/-- A monadic analogue of `Option.elim`. -/
def melim {α β : Type _} {m : Type _ → Type _} [Monad m] (x : m (Option α)) (y : m β) (z : α → m β) : m β :=
  do (← x).elim y z

/-- A monadic analogue of `Option.getD`. -/
def mgetD {α : Type _} {m : Type _ → Type _} [Monad m] (x : m (Option α)) (y : m α) : m α :=
  melim x y pure

end Option

author: JOSHCLUNE


text:
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module init.data.nat.bitwise
! leanprover-community/lean commit 53e8520d8964c7632989880372d91ba0cecbaf00
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Init.Data.Nat.Lemmas
import Init.WFTactics
import Mathlib.Data.Bool.Basic
import Mathlib.Init.Data.Bool.Lemmas
import Mathlib.Init.ZeroOne
import Mathlib.Tactic.Cases
import Mathlib.Tactic.PermuteGoals

/-!
# Lemmas about bitwise operations on natural numbers.

Possibly only of archaeological significance.
-/

universe u

-- Once we're in the `Nat` namespace, `xor` will inconventiently resolve to `Nat.xor`.
/-- `bxor` denotes the `xor` function i.e. the exclusive-or function on type `Bool`. -/
local notation "bxor" => _root_.xor

namespace Nat
set_option linter.deprecated false

/-- `boddDiv2 n` returns a 2-tuple of type `(Bool,Nat)`
    where the `Bool` value indicates whether `n` is odd or not
    and the `Nat` value returns `⌊n/2⌋` -/
def boddDiv2 : ℕ → Bool × ℕ
  | 0 => (false, 0)
  | succ n =>
    match boddDiv2 n with
    | (false, m) => (true, m)
    | (true, m) => (false, succ m)
#align nat.bodd_div2 Nat.boddDiv2

/-- `div2 n = ⌊n/2⌋` the greatest integer smaller than `n/2`-/
def div2 (n : ℕ) : ℕ :=
  (boddDiv2 n).2
#align nat.div2 Nat.div2

/-- `bodd n` returns `true` if `n` is odd-/
def bodd (n : ℕ) : Bool :=
  (boddDiv2 n).1
#align nat.bodd Nat.bodd

@[simp]
theorem bodd_zero : bodd 0 = false :=
  rfl
#align nat.bodd_zero Nat.bodd_zero

theorem bodd_one : bodd 1 = true :=
  rfl
#align nat.bodd_one Nat.bodd_one

theorem bodd_two : bodd 2 = false :=
  rfl
#align nat.bodd_two Nat.bodd_two

@[simp]
theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
  simp only [bodd, boddDiv2]
  let ⟨b,m⟩ := boddDiv2 n
  cases b <;> rfl
#align nat.bodd_succ Nat.bodd_succ

@[simp]
theorem bodd_add (m n : ℕ) : bodd (m + n) = bxor (bodd m) (bodd n) := by
  induction' n with n IH
  · simp
  · simp [add_succ, IH]
    cases bodd m <;> cases bodd n <;> rfl
#align nat.bodd_add Nat.bodd_add

@[simp]
theorem bodd_mul (m n : ℕ) : bodd (m * n) = (bodd m && bodd n) := by
  induction' n with n IH
  · simp
  · simp [mul_succ, IH]
    cases bodd m <;> cases bodd n <;> rfl
#align nat.bodd_mul Nat.bodd_mul

theorem mod_two_of_bodd (n : ℕ) : n % 2 = cond (bodd n) 1 0 := by
  have := congr_arg bodd (mod_add_div n 2)
  simp [not] at this
  have _ : ∀ b, and false b = false := by
    intro b
    cases b <;> rfl
  have _ : ∀ b, bxor b false = b := by
    intro b
    cases b <;> rfl
  rw [← this]
  cases' mod_two_eq_zero_or_one n with h h <;> rw [h] <;> rfl
#align nat.mod_two_of_bodd Nat.mod_two_of_bodd

@[simp]
theorem div2_zero : div2 0 = 0 :=
  rfl
#align nat.div2_zero Nat.div2_zero

theorem div2_one : div2 1 = 0 :=
  rfl
#align nat.div2_one Nat.div2_one

theorem div2_two : div2 2 = 1 :=
  rfl
#align nat.div2_two Nat.div2_two

@[simp]
theorem div2_succ (n : ℕ) : div2 (succ n) = cond (bodd n) (succ (div2 n)) (div2 n) := by
  simp only [bodd, boddDiv2, div2]
  cases' boddDiv2 n with fst snd
  cases fst
  case mk.false =>
    simp
  case mk.true =>
    simp

#align nat.div2_succ Nat.div2_succ

attribute [local simp] Nat.add_comm Nat.add_assoc Nat.add_left_comm Nat.mul_comm Nat.mul_assoc

theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
  | 0 => rfl
  | succ n => by
    simp
    refine' Eq.trans _ (congr_arg succ (bodd_add_div2 n))
    cases bodd n <;> simp [cond, not]
    · rw [Nat.add_comm, Nat.add_succ]
    · rw [succ_mul, Nat.add_comm 1, Nat.add_succ]
#align nat.bodd_add_div2 Nat.bodd_add_div2

theorem div2_val (n) : div2 n = n / 2 := by
  refine'
    Nat.eq_of_mul_eq_mul_left (by decide)
      (Nat.add_left_cancel (Eq.trans _ (Nat.mod_add_div n 2).symm))
  rw [mod_two_of_bodd, bodd_add_div2]
#align nat.div2_val Nat.div2_val

/-- `bit b` appends the digit `b` to the binary representation of
  its natural number input. -/
def bit (b : Bool) : ℕ → ℕ :=
  cond b bit1 bit0
#align nat.bit Nat.bit

theorem bit0_val (n : Nat) : bit0 n = 2 * n :=
  calc
    n + n = 0 + n + n := by rw [Nat.zero_add]
    _ = n * 2 := rfl
    _ = 2 * n := Nat.mul_comm _ _

#align nat.bit0_val Nat.bit0_val

theorem bit1_val (n : Nat) : bit1 n = 2 * n + 1 :=
  congr_arg succ (bit0_val _)
#align nat.bit1_val Nat.bit1_val

theorem bit_val (b n) : bit b n = 2 * n + cond b 1 0 := by
  cases b
  apply bit0_val
  apply bit1_val
#align nat.bit_val Nat.bit_val

theorem bit_decomp (n : Nat) : bit (bodd n) (div2 n) = n :=
  (bit_val _ _).trans <| (Nat.add_comm _ _).trans <| bodd_add_div2 _
#align nat.bit_decomp Nat.bit_decomp

/-- For a predicate `C : Nat → Sort _`, if instances can be
  constructed for natural numbers of the form `bit b n`,
  they can be constructed for any given natural number. -/
def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h _ _
#align nat.bit_cases_on Nat.bitCasesOn

theorem bit_zero : bit false 0 = 0 :=
  rfl
#align nat.bit_zero Nat.bit_zero

/--`shiftl' b m n` performs a left shift of `m` `n` times
 and adds the bit `b` as the least significant bit each time.
 Returns the corresponding natural number-/
def shiftl' (b : Bool) (m : ℕ) : ℕ → ℕ
  | 0 => m
  | n + 1 => bit b (shiftl' b m n)
#align nat.shiftl' Nat.shiftl'

/-- `shiftl m n` produces a natural number whose binary representation
  is obtained by left-shifting the binary representation of `m` by `n` places -/
def shiftl : ℕ → ℕ → ℕ :=
  shiftl' false
#align nat.shiftl Nat.shiftl

@[simp]
theorem shiftl_zero (m) : shiftl m 0 = m :=
  rfl
#align nat.shiftl_zero Nat.shiftl_zero

@[simp]
theorem shiftl_succ (m n) : shiftl m (n + 1) = bit0 (shiftl m n) :=
  rfl
#align nat.shiftl_succ Nat.shiftl_succ

/--`shiftr n m` performs returns the `m`-step right shift operation on `n` and
returns the resultant number. This is equivalent to performing `⌊n/2ᵐ⌋`-/
def shiftr : ℕ → ℕ → ℕ
  | m, 0 => m
  | m, n + 1 => div2 (shiftr m n)
#align nat.shiftr Nat.shiftr

theorem shiftr_zero : ∀ n, shiftr 0 n = 0 := by
  intro n
  induction' n with n IH
  case zero =>
    rw [shiftr]
  case succ =>
    rw [shiftr, div2, IH]
    rfl

/-- `testBit m n` returns whether the `(n+1)ˢᵗ` least significant bit is `1` or `0`-/
def testBit (m n : ℕ) : Bool :=
  bodd (shiftr m n)
#align nat.test_bit Nat.testBit

lemma binaryRec_decreasing (h : n ≠ 0) : div2 n < n := by
  rw [div2_val]
  apply (div_lt_iff_lt_mul <| succ_pos 1).2
  have := Nat.mul_lt_mul_of_pos_left (lt_succ_self 1)
    (lt_of_le_of_ne n.zero_le h.symm)
  rwa [Nat.mul_one] at this

/-- A recursion principle for `bit` representations of natural numbers.
  For a predicate `C : Nat → Sort _`, if instances can be
  constructed for natural numbers of the form `bit b n`,
  they can be constructed for all natural numbers. -/
def binaryRec {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) : ∀ n, C n :=
  fun n =>
    if n0 : n = 0 then
      by
        simp [n0]
        exact z
    else by
      let n' := div2 n
      have _x : bit (bodd n) n' = n := by
        apply bit_decomp n
      rw [←_x]
      exact f (bodd n) n' (binaryRec z f n')
  decreasing_by exact binaryRec_decreasing n0

#align nat.binary_rec Nat.binaryRec

/-- `size n` : Returns the size of a natural number in
bits i.e. the length of its binary representation -/
def size : ℕ → ℕ :=
  binaryRec 0 fun _ _ => succ
#align nat.size Nat.size

/-- `bits n` returns a list of Bools which correspond to the binary representation of n-/
def bits : ℕ → List Bool :=
  binaryRec [] fun b _ IH => b :: IH
#align nat.bits Nat.bits

-- Porting note: There is a `Nat.bitwise` in Lean 4 core,
-- but it is different from the one in mathlib3, so we just port blindly here.
/-- `Nat.bitwise'` (different from `Nat.bitwise` in Lean 4 core)
  applies the function `f` to pairs of bits in the same position in
  the binary representations of its inputs. -/
def bitwise' (f : Bool → Bool → Bool) : ℕ → ℕ → ℕ :=
  binaryRec (fun n => cond (f false true) n 0) fun a m Ia =>
    binaryRec (cond (f true false) (bit a m) 0) fun b n _ => bit (f a b) (Ia n)
#align nat.bitwise Nat.bitwise'

/--`lor'` takes two natural numbers and returns their bitwise `or`-/
def lor' : ℕ → ℕ → ℕ :=
  bitwise' or
#align nat.lor Nat.lor'

/--`land'` takes two naturals numbers and returns their `and`-/
def land' : ℕ → ℕ → ℕ :=
  bitwise' and
#align nat.land Nat.land'

/--`ldiff' a b` performs bitwise set difference. For each corresponding
  pair of bits taken as booleans, say `aᵢ` and `bᵢ`, it applies the
  boolean operation `aᵢ  ∧ bᵢ` to obtain the `iᵗʰ` bit of the result.-/
def ldiff' : ℕ → ℕ → ℕ :=
  bitwise' fun a b => a && not b
#align nat.ldiff Nat.ldiff'

/--`lxor'` computes the bitwise `xor` of two natural numbers-/
def lxor' : ℕ → ℕ → ℕ :=
  bitwise' bxor
#align nat.lxor Nat.lxor'

@[simp]
theorem binaryRec_zero {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) :
    binaryRec z f 0 = z := by
  rw [binaryRec]
  rfl
#align nat.binary_rec_zero Nat.binaryRec_zero

/-! bitwise ops -/

theorem bodd_bit (b n) : bodd (bit b n) = b := by
  rw [bit_val]
  simp
  cases b <;> cases bodd n <;> rfl
#align nat.bodd_bit Nat.bodd_bit

theorem div2_bit (b n) : div2 (bit b n) = n := by
  rw [bit_val, div2_val, Nat.add_comm, add_mul_div_left, div_eq_of_lt, Nat.zero_add]
  <;> cases b
  <;> exact by decide
#align nat.div2_bit Nat.div2_bit

theorem shiftl'_add (b m n) : ∀ k, shiftl' b m (n + k) = shiftl' b (shiftl' b m n) k
  | 0 => rfl
  | k + 1 => congr_arg (bit b) (shiftl'_add b m n k)
#align nat.shiftl'_add Nat.shiftl'_add

theorem shiftl_add : ∀ m n k, shiftl m (n + k) = shiftl (shiftl m n) k :=
  shiftl'_add _
#align nat.shiftl_add Nat.shiftl_add

theorem shiftr_add (m n) : ∀ k, shiftr m (n + k) = shiftr (shiftr m n) k
  | 0 => rfl
  | k + 1 => congr_arg div2 (shiftr_add m n k)
#align nat.shiftr_add Nat.shiftr_add

theorem shiftl'_sub (b m) : ∀ {n k}, k ≤ n → shiftl' b m (n - k) = shiftr (shiftl' b m n) k
  | n, 0, _ => rfl
  | n + 1, k + 1, h => by
    simp [shiftl']
    rw [Nat.add_comm, shiftr_add]
    simp [shiftr, div2_bit]
    simp [shiftl'_sub, (Nat.le_of_succ_le_succ h)]
#align nat.shiftl'_sub Nat.shiftl'_sub

theorem shiftl_sub : ∀ (m) {n k}, k ≤ n → shiftl m (n - k) = shiftr (shiftl m n) k :=
  shiftl'_sub _
#align nat.shiftl_sub Nat.shiftl_sub

@[simp]
theorem testBit_zero (b n) : testBit (bit b n) 0 = b :=
  bodd_bit _ _
#align nat.test_bit_zero Nat.testBit_zero

theorem testBit_succ (m b n) : testBit (bit b n) (succ m) = testBit n m := by
  have : bodd (shiftr (shiftr (bit b n) 1) m) = bodd (shiftr n m) := by
    dsimp [shiftr]
    rw [div2_bit]
  rw [← shiftr_add, Nat.add_comm] at this
  exact this
#align nat.test_bit_succ Nat.testBit_succ

theorem binaryRec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit b n)}
    (h : f false 0 z = z) (b n) : binaryRec z f (bit b n) = f b n (binaryRec z f n) := by
  rw [binaryRec]
  by_cases h : bit b n = 0
  -- Note: this renames the original `h : f false 0 z = z` to `h'` and leaves `h : bit b n = 0`
  case pos h' =>
    simp [dif_pos h]
    generalize binaryRec z f (bit b n) = e
    revert e
    have bf := bodd_bit b n
    have n0 := div2_bit b n
    rw [h] at bf n0
    simp at bf n0
    subst bf n0
    rw [binaryRec_zero]
    intros
    rw [h']
    rfl
  case neg h' =>
    simp [dif_neg h]
    generalize @id (C (bit b n) = C (bit (bodd (bit b n)) (div2 (bit b n))))
      (Eq.symm (bit_decomp (bit b n)) ▸ Eq.refl (C (bit b n))) = e
    revert e
    rw [bodd_bit, div2_bit]
    intros ; rfl
#align nat.binary_rec_eq Nat.binaryRec_eq

theorem bitwise'_bit_aux {f : Bool → Bool → Bool} (h : f false false = false) :
    (@binaryRec (fun _ => ℕ) (cond (f true false) (bit false 0) 0) fun b n _ =>
        bit (f false b) (cond (f false true) n 0)) =
      fun n : ℕ => cond (f false true) n 0 := by
  funext n
  apply bitCasesOn n
  intro b n
  rw [binaryRec_eq]
  · cases b
    <;> try rw [h]
    <;> induction' fft : f false true
    <;> simp [cond]
    cases f false true
    case h.true.false => simp
    case h.true.true => simp
  · rw [h, show cond (f false true) 0 0 = 0 by cases f false true <;> rfl,
        show cond (f true false) (bit false 0) 0 = 0 by cases f true false <;> rfl]
    rfl
#align nat.bitwise_bit_aux Nat.bitwise'_bit_aux

-- Porting Note : This was a @[simp] lemma in mathlib3
theorem bitwise'_zero_left (f : Bool → Bool → Bool) (n) :
    bitwise' f 0 n = cond (f false true) n 0 := by
  unfold bitwise'; rw [binaryRec_zero]

#align nat.bitwise_zero_left Nat.bitwise'_zero_left

@[simp]
theorem bitwise'_zero_right (f : Bool → Bool → Bool) (h : f false false = false) (m) :
    bitwise' f m 0 = cond (f true false) m 0 := by
  unfold bitwise'; apply bitCasesOn m; intros; rw [binaryRec_eq, binaryRec_zero];
    exact bitwise'_bit_aux h

#align nat.bitwise_zero_right Nat.bitwise'_zero_right

@[simp]
theorem bitwise'_zero (f : Bool → Bool → Bool) : bitwise' f 0 0 = 0 := by
  rw [bitwise'_zero_left]
  cases f false true <;> rfl
#align nat.bitwise_zero Nat.bitwise'_zero

@[simp]
theorem bitwise'_bit {f : Bool → Bool → Bool} (h : f false false = false) (a m b n) :
    bitwise' f (bit a m) (bit b n) = bit (f a b) (bitwise' f m n) := by
  unfold bitwise'
  rw [binaryRec_eq, binaryRec_eq]
  · induction' ftf : f true false
    rw [show f a false = false by cases a <;> assumption]
    apply @congr_arg _ _ _ 0 (bit false)
    swap
    rw [show f a false = a by cases a <;> assumption]
    apply congr_arg (bit a)
    all_goals
    { apply bitCasesOn m
      intro a m
      rw [binaryRec_eq, binaryRec_zero]
      · rfl
      · rw [← bitwise'_bit_aux h, ftf] }
  · exact bitwise'_bit_aux h
#align nat.bitwise_bit Nat.bitwise'_bit

theorem bitwise'_swap {f : Bool → Bool → Bool} (h : f false false = false) :
    bitwise' (Function.swap f) = Function.swap (bitwise' f) := by
  funext m n; revert n
  dsimp [Function.swap]
  apply binaryRec _ _ m <;> intro n
  · rw [bitwise'_zero_left, bitwise'_zero_right]
    exact h
  · intros a ih m'
    apply bitCasesOn m'; intro b n'
    rw [bitwise'_bit, bitwise'_bit, ih] <;> exact h
#align nat.bitwise_swap Nat.bitwise'_swap

-- Porting note:
-- If someone wants to merge `bitwise` and `bitwise'`
-- (and similarly `lor` / `lor'` and `land` / `land'`)
-- they could start by proving the next theorem:
-- lemma bitwise_eq_bitwise' (f : Bool → Bool → Bool) :
--     bitwise f = bitwise' f := by
--   sorry

-- @[simp]
-- theorem bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false) (a m b n) :
--     bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by
--   simp only [bitwise_eq_bitwise', bitwise'_bit h]

@[simp]
theorem lor'_bit : ∀ a m b n, lor' (bit a m) (bit b n) = bit (a || b) (lor' m n) :=
  bitwise'_bit rfl
#align nat.lor_bit Nat.lor'_bit

@[simp]
theorem land'_bit : ∀ a m b n, land' (bit a m) (bit b n) = bit (a && b) (land' m n) :=
  bitwise'_bit rfl
#align nat.land_bit Nat.land'_bit

@[simp]
theorem ldiff'_bit : ∀ a m b n, ldiff' (bit a m) (bit b n) = bit (a && not b) (ldiff' m n) :=
  bitwise'_bit rfl
#align nat.ldiff_bit Nat.ldiff'_bit

@[simp]
theorem lxor'_bit : ∀ a m b n, lxor' (bit a m) (bit b n) = bit (bxor a b) (lxor' m n) :=
  bitwise'_bit rfl
#align nat.lxor_bit Nat.lxor'_bit

@[simp]
theorem testBit_bitwise' {f : Bool → Bool → Bool} (h : f false false = false) (m n k) :
    testBit (bitwise' f m n) k = f (testBit m k) (testBit n k) := by
  revert m n; induction' k with k IH <;>
  intros m n <;>
  apply bitCasesOn m <;> intros a m' <;>
  apply bitCasesOn n <;> intros b n' <;>
  rw [bitwise'_bit h]
  · simp [testBit_zero]
  · simp [testBit_succ, IH]
#align nat.test_bit_bitwise Nat.testBit_bitwise'

@[simp]
theorem testBit_lor' : ∀ m n k, testBit (lor' m n) k = (testBit m k || testBit n k) :=
  testBit_bitwise' rfl
#align nat.test_bit_lor Nat.testBit_lor'

@[simp]
theorem testBit_land' : ∀ m n k, testBit (land' m n) k = (testBit m k && testBit n k) :=
  testBit_bitwise' rfl
#align nat.test_bit_land Nat.testBit_land'

@[simp]
theorem testBit_ldiff' : ∀ m n k, testBit (ldiff' m n) k = (testBit m k && not (testBit n k)) :=
  testBit_bitwise' rfl
#align nat.test_bit_ldiff Nat.testBit_ldiff'

@[simp]
theorem testBit_lxor' : ∀ m n k, testBit (lxor' m n) k = bxor (testBit m k) (testBit n k) :=
  testBit_bitwise' rfl
#align nat.test_bit_lxor Nat.testBit_lxor'

end Nat


text:
/-
Copyright (c) 2020 Kevin Kappelmann. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kevin Kappelmann
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.algebra.continued_fractions.continuants_recurrence
import Mathlib.algebra.continued_fractions.terminated_stable
import Mathlib.tactic.linarith.default
import Mathlib.tactic.field_simp
import Mathlib.PostPort

universes u_1

namespace Mathlib

/-!
# Equivalence of Recursive and Direct Computations of `gcf` Convergents

## Summary

We show the equivalence of two computations of convergents (recurrence relation (`convergents`) vs.
direct evaluation (`convergents'`)) for `gcf`s on linear ordered fields. We follow the proof from
[hardy2008introduction], Chapter 10. Here's a sketch:

Let `c` be a continued fraction `[h; (a₀, b₀), (a₁, b₁), (a₂, b₂),...]`, visually:
                                a₀
                h + ---------------------------
                                  a₁
                      b₀ + --------------------
                                    a₂
                            b₁ + --------------
                                        a₃
                                  b₂ + --------
                                      b₃ + ...

One can compute the convergents of `c` in two ways:
1. Directly evaluating the fraction described by `c` up to a given `n` (`convergents'`)
2. Using the recurrence (`convergents`):
  - `A₋₁ = 1,  A₀ = h,  Aₙ = bₙ₋₁ * Aₙ₋₁ + aₙ₋₁ * Aₙ₋₂`, and
  - `B₋₁ = 0,  B₀ = 1,  Bₙ = bₙ₋₁ * Bₙ₋₁ + aₙ₋₁ * Bₙ₋₂`.

To show the equivalence of the computations in the main theorem of this file
`convergents_eq_convergents'`, we proceed by induction. The case `n = 0` is trivial.

For `n + 1`, we first "squash" the `n + 1`th position of `c` into the `n`th position to obtain
another continued fraction
  `c' := [h; (a₀, b₀),..., (aₙ-₁, bₙ-₁), (aₙ, bₙ + aₙ₊₁ / bₙ₊₁), (aₙ₊₁, bₙ₊₁),...]`.
This squashing process is formalised in section `squash`. Note that directly evaluating `c` up to
position `n + 1` is equal to evaluating `c'` up to `n`. This is shown in lemma
`succ_nth_convergent'_eq_squash_gcf_nth_convergent'`.

By the inductive hypothesis, the two computations for the `n`th convergent of `c` coincide.
So all that is left to show is that the recurrence relation for `c` at `n + 1` and and `c'` at
`n` coincide. This can be shown by another induction.
The corresponding lemma in this file is `succ_nth_convergent_eq_squash_gcf_nth_convergent`.

## Main Theorems

- `generalized_continued_fraction.convergents_eq_convergents'` shows the equivalence under a strict
positivity restriction on the sequence.
- `continued_fractions.convergents_eq_convergents'` shows the equivalence for (regular) continued
fractions.

## References

- https://en.wikipedia.org/wiki/Generalized_continued_fraction
- [*Hardy, GH and Wright, EM and Heath-Brown, Roger and Silverman, Joseph*][hardy2008introduction]

## Tags

fractions, recurrence, equivalence
-/

namespace generalized_continued_fraction

/-!
We will show the equivalence of the computations by induction. To make the induction work, we need
to be able to *squash* the nth and (n + 1)th value of a sequence. This squashing itself and the
lemmas about it are not very interesting. As a reader, you hence might want to skip this section.
-/

/--
Given a sequence of gcf.pairs `s = [(a₀, bₒ), (a₁, b₁), ...]`, `squash_seq s n`
combines `⟨aₙ, bₙ⟩` and `⟨aₙ₊₁, bₙ₊₁⟩` at position `n` to `⟨aₙ, bₙ + aₙ₊₁ / bₙ₊₁⟩`. For example,
`squash_seq s 0 = [(a₀, bₒ + a₁ / b₁), (a₁, b₁),...]`.
If `s.terminated_at (n + 1)`, then `squash_seq s n = s`.
-/
def squash_seq {K : Type u_1} [division_ring K] (s : seq (pair K)) (n : ℕ) : seq (pair K) :=
  sorry

/-! We now prove some simple lemmas about the squashed sequence -/

/-- If the sequence already terminated at position `n + 1`, nothing gets squashed. -/
theorem squash_seq_eq_self_of_terminated {K : Type u_1} {n : ℕ} {s : seq (pair K)} [division_ring K] (terminated_at_succ_n : seq.terminated_at s (n + 1)) : squash_seq s n = s := sorry

/-- If the sequence has not terminated before position `n + 1`, the value at `n + 1` gets
squashed into position `n`. -/
theorem squash_seq_nth_of_not_terminated {K : Type u_1} {n : ℕ} {s : seq (pair K)} [division_ring K] {gp_n : pair K} {gp_succ_n : pair K} (s_nth_eq : seq.nth s n = some gp_n) (s_succ_nth_eq : seq.nth s (n + 1) = some gp_succ_n) : seq.nth (squash_seq s n) n = some (pair.mk (pair.a gp_n) (pair.b gp_n + pair.a gp_succ_n / pair.b gp_succ_n)) := sorry

/-- The values before the squashed position stay the same. -/
theorem squash_seq_nth_of_lt {K : Type u_1} {n : ℕ} {s : seq (pair K)} [division_ring K] {m : ℕ} (m_lt_n : m < n) : seq.nth (squash_seq s n) m = seq.nth s m := sorry

/-- Squashing at position `n + 1` and taking the tail is the same as squashing the tail of the
sequence at position `n`. -/
theorem squash_seq_succ_n_tail_eq_squash_seq_tail_n {K : Type u_1} {n : ℕ} {s : seq (pair K)} [division_ring K] : seq.tail (squash_seq s (n + 1)) = squash_seq (seq.tail s) n := sorry

/-- The auxiliary function `convergents'_aux` returns the same value for a sequence and the
corresponding squashed sequence at the squashed position. -/
theorem succ_succ_nth_convergent'_aux_eq_succ_nth_convergent'_aux_squash_seq {K : Type u_1} {n : ℕ} {s : seq (pair K)} [division_ring K] : convergents'_aux s (n + bit0 1) = convergents'_aux (squash_seq s n) (n + 1) := sorry

/-! Let us now lift the squashing operation to gcfs. -/

/--
Given a gcf `g = [h; (a₀, bₒ), (a₁, b₁), ...]`, we have
- `squash_nth.gcf g 0 = [h + a₀ / b₀); (a₀, bₒ), ...]`,
- `squash_nth.gcf g (n + 1) = ⟨g.h, squash_seq g.s n⟩`
-/
def squash_gcf {K : Type u_1} [division_ring K] (g : generalized_continued_fraction K) : ℕ → generalized_continued_fraction K :=
  sorry

/-! Again, we derive some simple lemmas that are not really of interest. This time for the
squashed gcf. -/

/-- If the gcf already terminated at position `n`, nothing gets squashed. -/
theorem squash_gcf_eq_self_of_terminated {K : Type u_1} {n : ℕ} {g : generalized_continued_fraction K} [division_ring K] (terminated_at_n : terminated_at g n) : squash_gcf g n = g := sorry

/-- The values before the squashed position stay the same. -/
theorem squash_gcf_nth_of_lt {K : Type u_1} {n : ℕ} {g : generalized_continued_fraction K} [division_ring K] {m : ℕ} (m_lt_n : m < n) : seq.nth (s (squash_gcf g (n + 1))) m = seq.nth (s g) m := sorry

/-- `convergents'` returns the same value for a gcf and the corresponding squashed gcf at the
squashed position. -/
theorem succ_nth_convergent'_eq_squash_gcf_nth_convergent' {K : Type u_1} {n : ℕ} {g : generalized_continued_fraction K} [division_ring K] : convergents' g (n + 1) = convergents' (squash_gcf g n) n := sorry

/-- The auxiliary continuants before the squashed position stay the same. -/
theorem continuants_aux_eq_continuants_aux_squash_gcf_of_le {K : Type u_1} {n : ℕ} {g : generalized_continued_fraction K} [division_ring K] {m : ℕ} : m ≤ n → continuants_aux g m = continuants_aux (squash_gcf g n) m := sorry

/-- The convergents coincide in the expected way at the squashed position if the partial denominator
at the squashed position is not zero. -/
theorem succ_nth_convergent_eq_squash_gcf_nth_convergent {K : Type u_1} {n : ℕ} {g : generalized_continued_fraction K} [field K] (nth_part_denom_ne_zero : ∀ {b : K}, seq.nth (partial_denominators g) n = some b → b ≠ 0) : convergents g (n + 1) = convergents (squash_gcf g n) n := sorry

/-- Shows that the recurrence relation (`convergents`) and direct evaluation (`convergents'`) of the
gcf coincide at position `n` if the sequence of fractions contains strictly positive values only.
Requiring positivity of all values is just one possible condition to obtain this result.
For example, the dual - sequences with strictly negative values only - would also work.

In practice, one most commonly deals with (regular) continued fractions, which satisfy the
positivity criterion required here. The analogous result for them
(see `continued_fractions.convergents_eq_convergents`) hence follows directly from this theorem.
-/
theorem convergents_eq_convergents' {K : Type u_1} {n : ℕ} {g : generalized_continued_fraction K} [linear_ordered_field K] (s_pos : ∀ {gp : pair K} {m : ℕ}, m < n → seq.nth (s g) m = some gp → 0 < pair.a gp ∧ 0 < pair.b gp) : convergents g n = convergents' g n := sorry

end generalized_continued_fraction

namespace continued_fraction

/-- Shows that the recurrence relation (`convergents`) and direct evaluation (`convergents'`) of a
(regular) continued fraction coincide. -/
theorem convergents_eq_convergents' {K : Type u_1} [linear_ordered_field K] {c : continued_fraction K} : generalized_continued_fraction.convergents ↑c = generalized_continued_fraction.convergents' ↑c := sorry

author: AurelienSaue


text:
/-
Copyright (c) 2018 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Johannes Hölzl, Reid Barton, Sean Leather

! This file was ported from Lean 3 source module category_theory.concrete_category.bundled
! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Std.Tactic.Lint.Frontend
import Std.Tactic.Lint.Misc
import Mathlib.Mathport.Rename

/-!
# Bundled types

`Bundled c` provides a uniform structure for bundling a type equipped with a type class.

We provide `Category` instances for these in `CategoryTheory/UnbundledHom.lean`
(for categories with unbundled homs, e.g. topological spaces)
and in `CategoryTheory/BundledHom.lean` (for categories with bundled homs, e.g. monoids).
-/

universe u v

namespace CategoryTheory

variable {c d : Type u → Type v} {α : Type u}

/-- `Bundled` is a type bundled with a type class instance for that type. Only
the type class is exposed as a parameter. -/
structure Bundled (c : Type u → Type v) : Type max (u + 1) v where
  /-- The underlying type of the bundled type -/
  α : Type u
  /-- The corresponding instance of the bundled type class -/
  str : c α := by infer_instance
#align category_theory.bundled CategoryTheory.Bundled

namespace Bundled

-- This is needed so that we can ask for an instance of `c α` below even though Lean doesn't know
-- that `c α` is a typeclass.
set_option checkBinderAnnotations false in

-- Usually explicit instances will provide their own version of this, e.g. `Mon.of` and `Top.of`.
/-- A generic function for lifting a type equipped with an instance to a bundled object. -/
def of {c : Type u → Type v} (α : Type u) [str : c α] : Bundled c :=
  ⟨α, str⟩
#align category_theory.bundled.of CategoryTheory.Bundled.of

instance coeSort : CoeSort (Bundled c) (Type u) :=
  ⟨Bundled.α⟩

theorem coe_mk (α) (str) : (@Bundled.mk c α str : Type u) = α :=
  rfl
#align category_theory.bundled.coe_mk CategoryTheory.Bundled.coe_mk

/-
`Bundled.map` is reducible so that, if we define a category

  def Ring : Type (u+1) := induced_category SemiRing (bundled.map @ring.to_semiring)

instance search is able to "see" that a morphism R ⟶ S in Ring is really
a (semi)ring homomorphism from R.α to S.α, and not merely from
`(Bundled.map @Ring.toSemiring R).α` to `(Bundled.map @Ring.toSemiring S).α`.

TODO: Once at least one use of this has been ported, check if this still needs to be reducible in
Lean 4.
-/
/-- Map over the bundled structure -/
def map (f : ∀ {α}, c α → d α) (b : Bundled c) : Bundled d :=
  ⟨b, f b.str⟩
#align category_theory.bundled.map CategoryTheory.Bundled.map

end Bundled

end CategoryTheory


text:
/-
Copyright (c) 2021 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies

! This file was ported from Lean 3 source module order.antichain
! leanprover-community/mathlib commit c227d107bbada5d0d9d20287e3282c0a7f1651a0
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Set.Pairwise.Basic
import Mathlib.Order.Bounds.Basic
import Mathlib.Order.Directed
import Mathlib.Order.Hom.Set

/-!
# Antichains

This file defines antichains. An antichain is a set where any two distinct elements are not related.
If the relation is `(≤)`, this corresponds to incomparability and usual order antichains. If the
relation is `G.adj` for `G : SimpleGraph α`, this corresponds to independent sets of `G`.

## Definitions

* `IsAntichain r s`: Any two elements of `s : Set α` are unrelated by `r : α → α → Prop`.
* `IsStrongAntichain r s`: Any two elements of `s : Set α` are not related by `r : α → α → Prop`
  to a common element.
* `IsAntichain.mk r s`: Turns `s` into an antichain by keeping only the "maximal" elements.
-/

open Function Set

section General

variable {α β : Type _} {r r₁ r₂ : α → α → Prop} {r' : β → β → Prop} {s t : Set α} {a b : α}

protected theorem Symmetric.compl (h : Symmetric r) : Symmetric (rᶜ) := fun _ _ hr hr' =>
  hr <| h hr'
#align symmetric.compl Symmetric.compl

/-- An antichain is a set such that no two distinct elements are related. -/
def IsAntichain (r : α → α → Prop) (s : Set α) : Prop :=
  s.Pairwise (rᶜ)
#align is_antichain IsAntichain

namespace IsAntichain

protected theorem subset (hs : IsAntichain r s) (h : t ⊆ s) : IsAntichain r t :=
  hs.mono h
#align is_antichain.subset IsAntichain.subset

theorem mono (hs : IsAntichain r₁ s) (h : r₂ ≤ r₁) : IsAntichain r₂ s :=
  hs.mono' <| compl_le_compl h
#align is_antichain.mono IsAntichain.mono

theorem mono_on (hs : IsAntichain r₁ s) (h : s.Pairwise fun ⦃a b⦄ => r₂ a b → r₁ a b) :
    IsAntichain r₂ s :=
  hs.imp_on <| h.imp fun _ _ h h₁ h₂ => h₁ <| h h₂
#align is_antichain.mono_on IsAntichain.mono_on

protected theorem eq (hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r a b) :
    a = b :=
  Set.Pairwise.eq hs ha hb <| not_not_intro h
#align is_antichain.eq IsAntichain.eq

protected theorem eq' (hs : IsAntichain r s) {a b : α} (ha : a ∈ s) (hb : b ∈ s) (h : r b a) :
    a = b :=
  (hs.eq hb ha h).symm
#align is_antichain.eq' IsAntichain.eq'

protected theorem isAntisymm (h : IsAntichain r univ) : IsAntisymm α r :=
  ⟨fun _ _ ha _ => h.eq trivial trivial ha⟩
#align is_antichain.is_antisymm IsAntichain.isAntisymm

protected theorem subsingleton [IsTrichotomous α r] (h : IsAntichain r s) : s.Subsingleton := by
  rintro a ha b hb
  obtain hab | hab | hab := trichotomous_of r a b
  · exact h.eq ha hb hab
  · exact hab
  · exact h.eq' ha hb hab
#align is_antichain.subsingleton IsAntichain.subsingleton

protected theorem flip (hs : IsAntichain r s) : IsAntichain (flip r) s := fun _ ha _ hb h =>
  hs hb ha h.symm
#align is_antichain.flip IsAntichain.flip

theorem swap (hs : IsAntichain r s) : IsAntichain (swap r) s :=
  hs.flip
#align is_antichain.swap IsAntichain.swap

theorem image (hs : IsAntichain r s) (f : α → β) (h : ∀ ⦃a b⦄, r' (f a) (f b) → r a b) :
    IsAntichain r' (f '' s) := by
  rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ hbc hr
  exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)
#align is_antichain.image IsAntichain.image

theorem preimage (hs : IsAntichain r s) {f : β → α} (hf : Injective f)
    (h : ∀ ⦃a b⦄, r' a b → r (f a) (f b)) : IsAntichain r' (f ⁻¹' s) := fun _ hb _ hc hbc hr =>
  hs hb hc (hf.ne hbc) <| h hr
#align is_antichain.preimage IsAntichain.preimage

theorem _root_.isAntichain_insert :
    IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b ∧ ¬r b a :=
  Set.pairwise_insert
#align is_antichain_insert isAntichain_insert

protected theorem insert (hs : IsAntichain r s) (hl : ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r b a)
    (hr : ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b) : IsAntichain r (insert a s) :=
  isAntichain_insert.2 ⟨hs, fun _ hb hab => ⟨hr hb hab, hl hb hab⟩⟩
#align is_antichain.insert IsAntichain.insert

theorem _root_.isAntichain_insert_of_symmetric (hr : Symmetric r) :
    IsAntichain r (insert a s) ↔ IsAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b :=
  pairwise_insert_of_symmetric hr.compl
#align is_antichain_insert_of_symmetric isAntichain_insert_of_symmetric

theorem insert_of_symmetric (hs : IsAntichain r s) (hr : Symmetric r)
    (h : ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬r a b) : IsAntichain r (insert a s) :=
  (isAntichain_insert_of_symmetric hr).2 ⟨hs, h⟩
#align is_antichain.insert_of_symmetric IsAntichain.insert_of_symmetric

theorem image_relEmbedding (hs : IsAntichain r s) (φ : r ↪r r') : IsAntichain r' (φ '' s) := by
  intro b hb b' hb' h₁ h₂
  rw [Set.mem_image] at hb hb'
  obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
  exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)
#align is_antichain.image_rel_embedding IsAntichain.image_relEmbedding

theorem preimage_relEmbedding {t : Set β} (ht : IsAntichain r' t) (φ : r ↪r r') :
    IsAntichain r (φ ⁻¹' t) := fun _ ha _s ha' hne hle =>
  ht ha ha' (fun h => hne (φ.injective h)) (φ.map_rel_iff.mpr hle)
#align is_antichain.preimage_rel_embedding IsAntichain.preimage_relEmbedding

theorem image_relIso (hs : IsAntichain r s) (φ : r ≃r r') : IsAntichain r' (φ '' s) :=
  hs.image_relEmbedding φ
#align is_antichain.image_rel_iso IsAntichain.image_relIso

theorem preimage_relIso {t : Set β} (hs : IsAntichain r' t) (φ : r ≃r r') :
    IsAntichain r (φ ⁻¹' t) :=
  hs.preimage_relEmbedding φ
#align is_antichain.preimage_rel_iso IsAntichain.preimage_relIso

theorem image_relEmbedding_iff {φ : r ↪r r'} : IsAntichain r' (φ '' s) ↔ IsAntichain r s :=
  ⟨fun h => (φ.injective.preimage_image s).subst (h.preimage_relEmbedding φ), fun h =>
    h.image_relEmbedding φ⟩
#align is_antichain.image_rel_embedding_iff IsAntichain.image_relEmbedding_iff

theorem image_relIso_iff {φ : r ≃r r'} : IsAntichain r' (φ '' s) ↔ IsAntichain r s :=
  @image_relEmbedding_iff _ _ _ _ _ (φ : r ↪r r')
#align is_antichain.image_rel_iso_iff IsAntichain.image_relIso_iff

theorem image_embedding [LE α] [LE β] (hs : IsAntichain (· ≤ ·) s) (φ : α ↪o β) :
    IsAntichain (· ≤ ·) (φ '' s) :=
  image_relEmbedding hs _
#align is_antichain.image_embedding IsAntichain.image_embedding

theorem preimage_embedding [LE α] [LE β] {t : Set β} (ht : IsAntichain (· ≤ ·) t) (φ : α ↪o β) :
    IsAntichain (· ≤ ·) (φ ⁻¹' t) :=
  preimage_relEmbedding ht _
#align is_antichain.preimage_embedding IsAntichain.preimage_embedding

theorem image_embedding_iff [LE α] [LE β] {φ : α ↪o β} :
    IsAntichain (· ≤ ·) (φ '' s) ↔ IsAntichain (· ≤ ·) s :=
  image_relEmbedding_iff
#align is_antichain.image_embedding_iff IsAntichain.image_embedding_iff

theorem image_iso [LE α] [LE β] (hs : IsAntichain (· ≤ ·) s) (φ : α ≃o β) :
    IsAntichain (· ≤ ·) (φ '' s) :=
  image_relEmbedding hs _
#align is_antichain.image_iso IsAntichain.image_iso

theorem preimage_iso [LE α] [LE β] {t : Set β} (ht : IsAntichain (· ≤ ·) t) (φ : α ≃o β) :
    IsAntichain (· ≤ ·) (φ ⁻¹' t) :=
  preimage_relEmbedding ht _
#align is_antichain.preimage_iso IsAntichain.preimage_iso

theorem preimage_iso_iff [LE α] [LE β] {t : Set β} {φ : α ≃o β} :
    IsAntichain (· ≤ ·) (φ ⁻¹' t) ↔ IsAntichain (· ≤ ·) t :=
  ⟨fun h => (φ.image_preimage t).subst (h.image_iso φ), fun h => h.preimage_iso _⟩
#align is_antichain.preimage_iso_iff IsAntichain.preimage_iso_iff

theorem to_dual [LE α] (hs : IsAntichain (· ≤ ·) s) : @IsAntichain αᵒᵈ (· ≤ ·) s :=
  fun _ ha _ hb hab => hs hb ha hab.symm
#align is_antichain.to_dual IsAntichain.to_dual

theorem to_dual_iff [LE α] : IsAntichain (· ≤ ·) s ↔ @IsAntichain αᵒᵈ (· ≤ ·) s :=
  ⟨to_dual, to_dual⟩
#align is_antichain.to_dual_iff IsAntichain.to_dual_iff

theorem image_compl [BooleanAlgebra α] (hs : IsAntichain (· ≤ ·) s) :
    IsAntichain (· ≤ ·) (compl '' s) :=
  (hs.image_embedding (OrderIso.compl α).toOrderEmbedding).flip
#align is_antichain.image_compl IsAntichain.image_compl

theorem preimage_compl [BooleanAlgebra α] (hs : IsAntichain (· ≤ ·) s) :
    IsAntichain (· ≤ ·) (compl ⁻¹' s) := fun _ ha _ ha' hne hle =>
  hs ha' ha (fun h => hne (compl_inj_iff.mp h.symm)) (compl_le_compl hle)
#align is_antichain.preimage_compl IsAntichain.preimage_compl

end IsAntichain

theorem isAntichain_singleton (a : α) (r : α → α → Prop) : IsAntichain r {a} :=
  pairwise_singleton _ _
#align is_antichain_singleton isAntichain_singleton

theorem Set.Subsingleton.isAntichain (hs : s.Subsingleton) (r : α → α → Prop) : IsAntichain r s :=
  hs.pairwise _
#align set.subsingleton.is_antichain Set.Subsingleton.isAntichain

section Preorder

variable [Preorder α]

theorem IsAntichain.not_lt (hs : IsAntichain (· ≤ ·) s) (ha : a ∈ s) (hb : b ∈ s) : ¬a < b :=
  fun h => hs ha hb h.ne h.le
#align is_antichain.not_lt IsAntichain.not_lt

theorem isAntichain_and_least_iff : IsAntichain (· ≤ ·) s ∧ IsLeast s a ↔ s = {a} :=
  ⟨fun h => eq_singleton_iff_unique_mem.2 ⟨h.2.1, fun b hb => h.1.eq' hb h.2.1 (h.2.2 hb)⟩, by
    rintro rfl
    exact ⟨isAntichain_singleton _ _, isLeast_singleton⟩⟩
#align is_antichain_and_least_iff isAntichain_and_least_iff

theorem isAntichain_and_greatest_iff : IsAntichain (· ≤ ·) s ∧ IsGreatest s a ↔ s = {a} :=
  ⟨fun h => eq_singleton_iff_unique_mem.2 ⟨h.2.1, fun b hb => h.1.eq hb h.2.1 (h.2.2 hb)⟩, by
    rintro rfl
    exact ⟨isAntichain_singleton _ _, isGreatest_singleton⟩⟩
#align is_antichain_and_greatest_iff isAntichain_and_greatest_iff

theorem IsAntichain.least_iff (hs : IsAntichain (· ≤ ·) s) : IsLeast s a ↔ s = {a} :=
  (and_iff_right hs).symm.trans isAntichain_and_least_iff
#align is_antichain.least_iff IsAntichain.least_iff

theorem IsAntichain.greatest_iff (hs : IsAntichain (· ≤ ·) s) : IsGreatest s a ↔ s = {a} :=
  (and_iff_right hs).symm.trans isAntichain_and_greatest_iff
#align is_antichain.greatest_iff IsAntichain.greatest_iff

theorem IsLeast.antichain_iff (hs : IsLeast s a) : IsAntichain (· ≤ ·) s ↔ s = {a} :=
  (and_iff_left hs).symm.trans isAntichain_and_least_iff
#align is_least.antichain_iff IsLeast.antichain_iff

theorem IsGreatest.antichain_iff (hs : IsGreatest s a) : IsAntichain (· ≤ ·) s ↔ s = {a} :=
  (and_iff_left hs).symm.trans isAntichain_and_greatest_iff
#align is_greatest.antichain_iff IsGreatest.antichain_iff

theorem IsAntichain.bot_mem_iff [OrderBot α] (hs : IsAntichain (· ≤ ·) s) : ⊥ ∈ s ↔ s = {⊥} :=
  isLeast_bot_iff.symm.trans hs.least_iff
#align is_antichain.bot_mem_iff IsAntichain.bot_mem_iff

theorem IsAntichain.top_mem_iff [OrderTop α] (hs : IsAntichain (· ≤ ·) s) : ⊤ ∈ s ↔ s = {⊤} :=
  isGreatest_top_iff.symm.trans hs.greatest_iff
#align is_antichain.top_mem_iff IsAntichain.top_mem_iff

end Preorder

section PartialOrder

variable [PartialOrder α]

theorem isAntichain_iff_forall_not_lt :
    IsAntichain (· ≤ ·) s ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → ¬a < b :=
  ⟨fun hs _ ha _ => hs.not_lt ha, fun hs _ ha _ hb h h' => hs ha hb <| h'.lt_of_ne h⟩
#align is_antichain_iff_forall_not_lt isAntichain_iff_forall_not_lt

end PartialOrder

/-! ### Strong antichains -/

/-- A strong (upward) antichain is a set such that no two distinct elements are related to a common
element. -/
def IsStrongAntichain (r : α → α → Prop) (s : Set α) : Prop :=
  s.Pairwise fun a b => ∀ c, ¬r a c ∨ ¬r b c
#align is_strong_antichain IsStrongAntichain

namespace IsStrongAntichain

protected theorem subset (hs : IsStrongAntichain r s) (h : t ⊆ s) : IsStrongAntichain r t :=
  hs.mono h
#align is_strong_antichain.subset IsStrongAntichain.subset

theorem mono (hs : IsStrongAntichain r₁ s) (h : r₂ ≤ r₁) : IsStrongAntichain r₂ s :=
  hs.mono' fun _ _ hab c => (hab c).imp (compl_le_compl h _ _) (compl_le_compl h _ _)
#align is_strong_antichain.mono IsStrongAntichain.mono

theorem eq (hs : IsStrongAntichain r s) {a b c : α} (ha : a ∈ s) (hb : b ∈ s) (hac : r a c)
    (hbc : r b c) : a = b :=
  (Set.Pairwise.eq hs ha hb) fun h =>
    False.elim <| (h c).elim (not_not_intro hac) (not_not_intro hbc)
#align is_strong_antichain.eq IsStrongAntichain.eq

protected theorem isAntichain [IsRefl α r] (h : IsStrongAntichain r s) : IsAntichain r s :=
  h.imp fun _ b hab => (hab b).resolve_right (not_not_intro <| refl _)
#align is_strong_antichain.is_antichain IsStrongAntichain.isAntichain

protected theorem subsingleton [IsDirected α r] (h : IsStrongAntichain r s) : s.Subsingleton :=
  fun a ha b hb =>
  let ⟨_, hac, hbc⟩ := directed_of r a b
  h.eq ha hb hac hbc
#align is_strong_antichain.subsingleton IsStrongAntichain.subsingleton

protected theorem flip [IsSymm α r] (hs : IsStrongAntichain r s) : IsStrongAntichain (flip r) s :=
  fun _ ha _ hb h c => (hs ha hb h c).imp (mt <| symm_of r) (mt <| symm_of r)
#align is_strong_antichain.flip IsStrongAntichain.flip

theorem swap [IsSymm α r] (hs : IsStrongAntichain r s) : IsStrongAntichain (swap r) s :=
  hs.flip
#align is_strong_antichain.swap IsStrongAntichain.swap

theorem image (hs : IsStrongAntichain r s) {f : α → β} (hf : Surjective f)
    (h : ∀ a b, r' (f a) (f b) → r a b) : IsStrongAntichain r' (f '' s) := by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c
  obtain ⟨c, rfl⟩ := hf c
  exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)
#align is_strong_antichain.image IsStrongAntichain.image

theorem preimage (hs : IsStrongAntichain r s) {f : β → α} (hf : Injective f)
    (h : ∀ a b, r' a b → r (f a) (f b)) : IsStrongAntichain r' (f ⁻¹' s) := fun _ ha _ hb hab _ =>
  (hs ha hb (hf.ne hab) _).imp (mt <| h _ _) (mt <| h _ _)
#align is_strong_antichain.preimage IsStrongAntichain.preimage

theorem _root_.isStrongAntichain_insert :
    IsStrongAntichain r (insert a s) ↔
      IsStrongAntichain r s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬r a c ∨ ¬r b c :=
  Set.pairwise_insert_of_symmetric fun _ _ h c => (h c).symm
#align is_strong_antichain_insert isStrongAntichain_insert

protected theorem insert (hs : IsStrongAntichain r s)
    (h : ∀ ⦃b⦄, b ∈ s → a ≠ b → ∀ c, ¬r a c ∨ ¬r b c) : IsStrongAntichain r (insert a s) :=
  isStrongAntichain_insert.2 ⟨hs, h⟩
#align is_strong_antichain.insert IsStrongAntichain.insert

end IsStrongAntichain

theorem Set.Subsingleton.isStrongAntichain (hs : s.Subsingleton) (r : α → α → Prop) :
    IsStrongAntichain r s :=
  hs.pairwise _
#align set.subsingleton.is_strong_antichain Set.Subsingleton.isStrongAntichain

end General

/-! ### Weak antichains -/

section Pi

variable {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] {s t : Set (∀ i, α i)}
  {a b c : ∀ i, α i}

@[inherit_doc]
local infixl:50 " ≺ " => StrongLT

/-- A weak antichain in `Π i, α i` is a set such that no two distinct elements are strongly less
than each other. -/
def IsWeakAntichain (s : Set (∀ i, α i)) : Prop :=
  IsAntichain (· ≺ ·) s
#align is_weak_antichain IsWeakAntichain

namespace IsWeakAntichain

protected theorem subset (hs : IsWeakAntichain s) : t ⊆ s → IsWeakAntichain t :=
  IsAntichain.subset hs
#align is_weak_antichain.subset IsWeakAntichain.subset

protected theorem eq (hs : IsWeakAntichain s) : a ∈ s → b ∈ s → a ≺ b → a = b :=
  IsAntichain.eq hs
#align is_weak_antichain.eq IsWeakAntichain.eq

protected theorem insert (hs : IsWeakAntichain s) :
    (∀ ⦃b⦄, b ∈ s → a ≠ b → ¬b ≺ a) →
      (∀ ⦃b⦄, b ∈ s → a ≠ b → ¬a ≺ b) → IsWeakAntichain (insert a s) :=
  IsAntichain.insert hs
#align is_weak_antichain.insert IsWeakAntichain.insert

end IsWeakAntichain

theorem _root_.isWeakAntichain_insert :
    IsWeakAntichain (insert a s) ↔ IsWeakAntichain s ∧ ∀ ⦃b⦄, b ∈ s → a ≠ b → ¬a ≺ b ∧ ¬b ≺ a :=
  isAntichain_insert
#align is_weak_antichain_insert isWeakAntichain_insert

protected theorem IsAntichain.isWeakAntichain (hs : IsAntichain (· ≤ ·) s) : IsWeakAntichain s :=
  hs.mono fun _ _ => le_of_strongLT
#align is_antichain.is_weak_antichain IsAntichain.isWeakAntichain

theorem Set.Subsingleton.isWeakAntichain (hs : s.Subsingleton) : IsWeakAntichain s :=
  hs.isAntichain _
#align set.subsingleton.is_weak_antichain Set.Subsingleton.isWeakAntichain

end Pi