text:
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.SizeOf
import Init.Data.Nat.Basic

universe u v

set_option codegen false

inductive Acc {α : Sort u} (r : α → α → Prop) : α → Prop where
  | intro (x : α) (h : (y : α) → r y x → Acc r y) : Acc r x

abbrev Acc.ndrec.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
    (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
    {a : α} (n : Acc r a) : C a :=
Acc.rec (motive := fun α _ => C α) m n

abbrev Acc.ndrecOn.{u1, u2} {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1}
    {a : α} (n : Acc r a)
    (m : (x : α) → ((y : α) → r y x → Acc r y) → ((y : α) → (a : r y x) → C y) → C x)
    : C a :=
Acc.rec (motive := fun α _ => C α) m n

namespace Acc
variable {α : Sort u} {r : α → α → Prop}

def inv {x y : α} (h₁ : Acc r x) (h₂ : r y x) : Acc r y :=
Acc.recOn (motive := fun (x : α) _ => r y x → Acc r y)
  h₁ (fun x₁ ac₁ ih h₂ => ac₁ y h₂) h₂

end Acc

inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop where
  | intro (h : ∀ a, Acc r a) : WellFounded r

class WellFoundedRelation (α : Sort u) where
  rel : α → α → Prop
  wf  : WellFounded rel

namespace WellFounded
def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a :=
  WellFounded.recOn (motive := fun x => (y : α) → Acc r y)
    wf (fun p => p) a

section
variable {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r)

theorem recursion {C : α → Sort v} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a := by
  induction (apply hwf a) with
  | intro x₁ ac₁ ih => exact h x₁ ih

theorem induction {C : α → Prop} (a : α) (h : ∀ x, (∀ y, r y x → C y) → C x) : C a :=
  recursion hwf a h

variable {C : α → Sort v}
variable (F : ∀ x, (∀ y, r y x → C y) → C x)

def fixF (x : α) (a : Acc r x) : C x := by
  induction a with
  | intro x₁ ac₁ ih => exact F x₁ ih

def fixFEq (x : α) (acx : Acc r x) : fixF F x acx = F x (fun (y : α) (p : r y x) => fixF F y (Acc.inv acx p)) := by
  induction acx with
  | intro x r ih => exact rfl

end

variable {α : Sort u} {C : α → Sort v} {r : α → α → Prop}

-- Well-founded fixpoint
def fix (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
  fixF F x (apply hwf x)

-- Well-founded fixpoint satisfies fixpoint equation
theorem fix_eq (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) :
    fix hwf F x = F x (fun y h => fix hwf F y) :=
  fixFEq F x (apply hwf x)
end WellFounded

open WellFounded

-- Empty relation is well-founded
def emptyWf {α : Sort u} : WellFoundedRelation α where
  rel := emptyRelation
  wf  := by
    apply WellFounded.intro
    intro a
    apply Acc.intro a
    intro b h
    cases h

-- Subrelation of a well-founded relation is well-founded
namespace Subrelation
variable {α : Sort u} {r q : α → α → Prop}

def accessible {a : α} (h₁ : Subrelation q r) (ac : Acc r a) : Acc q a := by
  induction ac with
  | intro x ax ih =>
    apply Acc.intro
    intro y h
    exact ih y (h₁ h)

def wf (h₁ : Subrelation q r) (h₂ : WellFounded r) : WellFounded q :=
  ⟨fun a => accessible @h₁ (apply h₂ a)⟩
end Subrelation

-- The inverse image of a well-founded relation is well-founded
namespace InvImage
variable {α : Sort u} {β : Sort v} {r : β → β → Prop}

private def accAux (f : α → β) {b : β} (ac : Acc r b) : (x : α) → f x = b → Acc (InvImage r f) x := by
  induction ac with
  | intro x acx ih =>
    intro z e
    apply Acc.intro
    intro y lt
    subst x
    apply ih (f y) lt y rfl

def accessible {a : α} (f : α → β) (ac : Acc r (f a)) : Acc (InvImage r f) a :=
  accAux f ac a rfl

def wf (f : α → β) (h : WellFounded r) : WellFounded (InvImage r f) :=
  ⟨fun a => accessible f (apply h (f a))⟩
end InvImage

@[reducible] def invImage (f : α → β) (h : WellFoundedRelation β) : WellFoundedRelation α where
  rel := InvImage h.rel f
  wf  := InvImage.wf f h.wf

-- The transitive closure of a well-founded relation is well-founded
namespace TC
variable {α : Sort u} {r : α → α → Prop}

def accessible {z : α} (ac : Acc r z) : Acc (TC r) z := by
  induction ac with
  | intro x acx ih =>
    apply Acc.intro x
    intro y rel
    induction rel with
    | base a b rab => exact ih a rab
    | trans a b c rab rbc ih₁ ih₂ => apply Acc.inv (ih₂ acx ih) rab

def wf (h : WellFounded r) : WellFounded (TC r) :=
  ⟨fun a => accessible (apply h a)⟩
end TC

-- less-than is well-founded
def Nat.lt_wfRel : WellFoundedRelation Nat where
  rel := Nat.lt
  wf  := by
  apply WellFounded.intro
  intro n
  induction n with
  | zero      =>
    apply Acc.intro 0
    intro _ h
    apply absurd h (Nat.not_lt_zero _)
  | succ n ih =>
    apply Acc.intro (Nat.succ n)
    intro m h
    have : m = n ∨ m < n := Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ h)
    match this with
    | Or.inl e => subst e; assumption
    | Or.inr e => exact Acc.inv ih e

def Measure {α : Sort u} : (α → Nat) → α → α → Prop :=
  InvImage (fun a b => a < b)

abbrev measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α :=
  invImage f Nat.lt_wfRel

def SizeOfRef (α : Sort u) [SizeOf α] : α → α → Prop :=
  Measure sizeOf

abbrev sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α :=
  measure sizeOf

instance (priority := low) [SizeOf α] : WellFoundedRelation α :=
  sizeOfWFRel

namespace Prod
open WellFounded

section
variable {α : Type u} {β : Type v}
variable  (ra  : α → α → Prop)
variable  (rb  : β → β → Prop)

-- Lexicographical order based on ra and rb
inductive Lex : α × β → α × β → Prop where
  | left  {a₁} (b₁) {a₂} (b₂) (h : ra a₁ a₂) : Lex (a₁, b₁) (a₂, b₂)
  | right (a) {b₁ b₂} (h : rb b₁ b₂)         : Lex (a, b₁)  (a, b₂)

-- relational product based on ra and rb
inductive RProd : α × β → α × β → Prop where
  | intro {a₁ b₁ a₂ b₂} (h₁ : ra a₁ a₂) (h₂ : rb b₁ b₂) : RProd (a₁, b₁) (a₂, b₂)
end

section

variable {α : Type u} {β : Type v}
variable {ra  : α → α → Prop} {rb  : β → β → Prop}

def lexAccessible (aca : (a : α) → Acc ra a) (acb : (b : β) → Acc rb b) (a : α) (b : β) : Acc (Lex ra rb) (a, b) := by
  induction (aca a) generalizing b with
  | intro xa aca iha =>
    induction (acb b) with
    | intro xb acb ihb =>
      apply Acc.intro (xa, xb)
      intro p lt
      cases lt with
      | left  _ _ h => apply iha _ h
      | right _ h   => apply ihb _ h

-- The lexicographical order of well founded relations is well-founded
@[reducible] def lex (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β) where
  rel := Lex ha.rel hb.rel
  wf  := ⟨fun (a, b) => lexAccessible (WellFounded.apply ha.wf) (WellFounded.apply hb.wf) a b⟩

instance [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFoundedRelation (α × β) :=
  lex ha hb

-- relational product is a Subrelation of the Lex
def RProdSubLex (a : α × β) (b : α × β) (h : RProd ra rb a b) : Lex ra rb a b := by
  cases h with
  | intro h₁ h₂ => exact Lex.left _ _ h₁

-- The relational product of well founded relations is well-founded
def rprod (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β) where
  rel := RProd ha.rel hb.rel
  wf  := by
  apply Subrelation.wf (r := Lex ha.rel hb.rel) (h₂ := (lex ha hb).wf)
  intro a b h
  exact RProdSubLex a b h

end

end Prod

namespace PSigma
section
variable {α : Sort u} {β : α → Sort v}
variable  (r  : α → α → Prop)
variable  (s  : ∀ a, β a → β a → Prop)

-- Lexicographical order based on r and s
inductive Lex : PSigma β → PSigma β → Prop where
  | left  : ∀ {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂ → Lex ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
  | right : ∀ (a : α)  {b₁ b₂ : β a}, s a b₁ b₂ → Lex ⟨a, b₁⟩ ⟨a, b₂⟩
end

section
variable {α : Sort u} {β : α → Sort v}
variable {r  : α → α → Prop} {s : ∀ (a : α), β a → β a → Prop}

def lexAccessible {a} (aca : Acc r a) (acb : (a : α) → WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩ := by
  induction aca with
  | intro xa aca iha =>
    induction (WellFounded.apply (acb xa) b) with
    | intro xb acb ihb =>
      apply Acc.intro
      intro p lt
      cases lt with
      | left  => apply iha; assumption
      | right => apply ihb; assumption

-- The lexicographical order of well founded relations is well-founded
@[reducible] def lex (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) : WellFoundedRelation (PSigma β) where
  rel := Lex ha.rel (fun a => hb a |>.rel)
  wf  := WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha.wf a) (fun a => hb a |>.wf) b

instance [ha : WellFoundedRelation α] [hb : (a : α) → WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β) :=
  lex ha hb

end

section
variable {α : Sort u} {β : Sort v}

def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
  Lex r (fun a => s)

def lexNdepWf {r  : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
  WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun x => hb) b
end

section
variable {α : Sort u} {β : Sort v}

-- Reverse lexicographical order based on r and s
inductive RevLex (r  : α → α → Prop) (s  : β → β → Prop) : @PSigma α (fun a => β) → @PSigma α (fun a => β) → Prop where
  | left  : {a₁ a₂ : α} → (b : β) → r a₁ a₂ → RevLex r s ⟨a₁, b⟩ ⟨a₂, b⟩
  | right : (a₁ : α) → {b₁ : β} → (a₂ : α) → {b₂ : β} → s b₁ b₂ → RevLex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
end

section
open WellFounded
variable {α : Sort u} {β : Sort v}
variable {r  : α → α → Prop} {s : β → β → Prop}

def revLexAccessible {b} (acb : Acc s b) (aca : (a : α) → Acc r a): (a : α) → Acc (RevLex r s) ⟨a, b⟩ := by
  induction acb with
  | intro xb acb ihb =>
    intro a
    induction (aca a) with
    | intro xa aca iha =>
      apply Acc.intro
      intro p lt
      cases lt with
      | left  => apply iha; assumption
      | right => apply ihb; assumption

def revLex (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s) :=
  WellFounded.intro fun ⟨a, b⟩ => revLexAccessible (apply hb b) (WellFounded.apply ha) a
end

section
def SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : @PSigma α (fun a => β) → @PSigma α (fun a => β) → Prop :=
  RevLex emptyRelation s

def skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFoundedRelation (PSigma fun a : α => β) where
  rel := SkipLeft α hb.rel
  wf  := revLex emptyWf.wf hb.wf

def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ :=
  RevLex.right _ _ h
end

end PSigma

author: Kha


text:
import for_mathlib.abelian_category
import for_mathlib.int
import for_mathlib.neg_one_pow

universes v u

open category_theory category_theory.limits
open category_theory.preadditive

variables {A : Type u} [category.{v} A] [preadditive A] {X Y : A} (f : X ⟶ Y)

-- Move This
@[simp] lemma is_iso_neg_iff : is_iso (-f) ↔ is_iso f :=
begin
  split; rintro ⟨g, hg⟩; refine ⟨⟨-g, _⟩⟩;
  simpa only [preadditive.comp_neg, preadditive.neg_comp, neg_neg] using hg,
end

-- move me
instance is_iso_neg [is_iso f] : is_iso (-f) :=
by rwa is_iso_neg_iff

-- Move This
@[simp] lemma is_iso_neg_one_pow_iff (i : ℤ) :
  is_iso (i.neg_one_pow • f) ↔ is_iso f :=
begin
  induction i using int.induction_on_iff with i,
  { simp only [int.neg_one_pow_neg_zero, one_zsmul] },
  dsimp,
  simp only [int.neg_one_pow_add, int.neg_one_pow_one, mul_neg, mul_one, neg_smul, is_iso_neg_iff],
end

author: leanprover-community

repo: lean-liquid


text:
/-
Copyright (c) 2020 Sébastien Gouëzel. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Anatole Dedecker, Sébastien Gouëzel, Yury G. Kudryashov, Dylan MacKenzie, Patrick Massot
-/
import algebra.order.field
import analysis.asymptotics.asymptotics
import analysis.specific_limits.basic

/-!
# A collection of specific limit computations

This file contains important specific limit computations in (semi-)normed groups/rings/spaces, as
as well as such computations in `ℝ` when the natural proof passes through a fact about normed
spaces.

-/

noncomputable theory
open classical set function filter finset metric asymptotics

open_locale classical topological_space nat big_operators uniformity nnreal ennreal

variables {α : Type*} {β : Type*} {ι : Type*}

lemma tendsto_norm_at_top_at_top : tendsto (norm : ℝ → ℝ) at_top at_top :=
tendsto_abs_at_top_at_top

lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
  (∃r, tendsto (λn, (∑ i in range n, |f i|)) at_top (𝓝 r)) → summable f
| ⟨r, hr⟩ :=
  begin
    refine summable_of_summable_norm ⟨r, (has_sum_iff_tendsto_nat_of_nonneg _ _).2 _⟩,
    exact assume i, norm_nonneg _,
    simpa only using hr
  end

/-! ### Powers -/

lemma tendsto_norm_zero' {𝕜 : Type*} [normed_group 𝕜] :
  tendsto (norm : 𝕜 → ℝ) (𝓝[≠] 0) (𝓝[>] 0) :=
tendsto_norm_zero.inf $ tendsto_principal_principal.2 $ λ x hx, norm_pos_iff.2 hx

namespace normed_field

lemma tendsto_norm_inverse_nhds_within_0_at_top {𝕜 : Type*} [normed_field 𝕜] :
  tendsto (λ x:𝕜, ∥x⁻¹∥) (𝓝[≠] 0) at_top :=
(tendsto_inv_zero_at_top.comp tendsto_norm_zero').congr $ λ x, (norm_inv x).symm

lemma tendsto_norm_zpow_nhds_within_0_at_top {𝕜 : Type*} [normed_field 𝕜] {m : ℤ}
  (hm : m < 0) :
  tendsto (λ x : 𝕜, ∥x ^ m∥) (𝓝[≠] 0) at_top :=
begin
  rcases neg_surjective m with ⟨m, rfl⟩,
  rw neg_lt_zero at hm, lift m to ℕ using hm.le, rw int.coe_nat_pos at hm,
  simp only [norm_pow, zpow_neg, zpow_coe_nat, ← inv_pow],
  exact (tendsto_pow_at_top hm).comp normed_field.tendsto_norm_inverse_nhds_within_0_at_top
end

/-- The (scalar) product of a sequence that tends to zero with a bounded one also tends to zero. -/
lemma tendsto_zero_smul_of_tendsto_zero_of_bounded {ι 𝕜 𝔸 : Type*} [normed_field 𝕜]
  [normed_group 𝔸] [normed_space 𝕜 𝔸] {l : filter ι} {ε : ι → 𝕜} {f : ι → 𝔸}
  (hε : tendsto ε l (𝓝 0)) (hf : filter.is_bounded_under (≤) l (norm ∘ f)) :
  tendsto (ε • f) l (𝓝 0) :=
begin
  rw ← is_o_one_iff 𝕜 at hε ⊢,
  simpa using is_o.smul_is_O hε (hf.is_O_const (one_ne_zero : (1 : 𝕜) ≠ 0))
end

@[simp] lemma continuous_at_zpow {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {m : ℤ} {x : 𝕜} :
  continuous_at (λ x, x ^ m) x ↔ x ≠ 0 ∨ 0 ≤ m :=
begin
  refine ⟨_, continuous_at_zpow₀ _ _⟩,
  contrapose!, rintro ⟨rfl, hm⟩ hc,
  exact not_tendsto_at_top_of_tendsto_nhds (hc.tendsto.mono_left nhds_within_le_nhds).norm
      (tendsto_norm_zpow_nhds_within_0_at_top hm)
end

@[simp] lemma continuous_at_inv {𝕜 : Type*} [nondiscrete_normed_field 𝕜] {x : 𝕜} :
  continuous_at has_inv.inv x ↔ x ≠ 0 :=
by simpa [(@zero_lt_one ℤ _ _).not_le] using @continuous_at_zpow _ _ (-1) x

end normed_field

lemma is_o_pow_pow_of_lt_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ < r₂) :
  (λ n : ℕ, r₁ ^ n) =o[at_top] (λ n, r₂ ^ n) :=
have H : 0 < r₂ := h₁.trans_lt h₂,
is_o_of_tendsto (λ n hn, false.elim $ H.ne' $ pow_eq_zero hn) $
  (tendsto_pow_at_top_nhds_0_of_lt_1 (div_nonneg h₁ (h₁.trans h₂.le)) ((div_lt_one H).2 h₂)).congr
    (λ n, div_pow _ _ _)

lemma is_O_pow_pow_of_le_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ ≤ r₂) :
  (λ n : ℕ, r₁ ^ n) =O[at_top] (λ n, r₂ ^ n) :=
h₂.eq_or_lt.elim (λ h, h ▸ is_O_refl _ _) (λ h, (is_o_pow_pow_of_lt_left h₁ h).is_O)

lemma is_o_pow_pow_of_abs_lt_left {r₁ r₂ : ℝ} (h : |r₁| < |r₂|) :
  (λ n : ℕ, r₁ ^ n) =o[at_top] (λ n, r₂ ^ n) :=
begin
  refine (is_o.of_norm_left _).of_norm_right,
  exact (is_o_pow_pow_of_lt_left (abs_nonneg r₁) h).congr (pow_abs r₁) (pow_abs r₂)
end

/-- Various statements equivalent to the fact that `f n` grows exponentially slower than `R ^ n`.

* 0: $f n = o(a ^ n)$ for some $-R < a < R$;
* 1: $f n = o(a ^ n)$ for some $0 < a < R$;
* 2: $f n = O(a ^ n)$ for some $-R < a < R$;
* 3: $f n = O(a ^ n)$ for some $0 < a < R$;
* 4: there exist `a < R` and `C` such that one of `C` and `R` is positive and $|f n| ≤ Ca^n$
     for all `n`;
* 5: there exists `0 < a < R` and a positive `C` such that $|f n| ≤ Ca^n$ for all `n`;
* 6: there exists `a < R` such that $|f n| ≤ a ^ n$ for sufficiently large `n`;
* 7: there exists `0 < a < R` such that $|f n| ≤ a ^ n$ for sufficiently large `n`.

NB: For backwards compatibility, if you add more items to the list, please append them at the end of
the list. -/
lemma tfae_exists_lt_is_o_pow (f : ℕ → ℝ) (R : ℝ) :
  tfae [∃ a ∈ Ioo (-R) R, f =o[at_top] pow a,
    ∃ a ∈ Ioo 0 R, f =o[at_top] (pow a),
    ∃ a ∈ Ioo (-R) R, f =O[at_top] pow a,
    ∃ a ∈ Ioo 0 R, f =O[at_top] pow a,
    ∃ (a < R) C (h₀ : 0 < C ∨ 0 < R), ∀ n, |f n| ≤ C * a ^ n,
    ∃ (a ∈ Ioo 0 R) (C > 0), ∀ n, |f n| ≤ C * a ^ n,
    ∃ a < R, ∀ᶠ n in at_top, |f n| ≤ a ^ n,
    ∃ a ∈ Ioo 0 R, ∀ᶠ n in at_top, |f n| ≤ a ^ n] :=
begin
  have A : Ico 0 R ⊆ Ioo (-R) R,
    from λ x hx, ⟨(neg_lt_zero.2 (hx.1.trans_lt hx.2)).trans_le hx.1, hx.2⟩,
  have B : Ioo 0 R ⊆ Ioo (-R) R := subset.trans Ioo_subset_Ico_self A,
  -- First we prove that 1-4 are equivalent using 2 → 3 → 4, 1 → 3, and 2 → 1
  tfae_have : 1 → 3, from λ ⟨a, ha, H⟩, ⟨a, ha, H.is_O⟩,
  tfae_have : 2 → 1, from λ ⟨a, ha, H⟩, ⟨a, B ha, H⟩,
  tfae_have : 3 → 2,
  { rintro ⟨a, ha, H⟩,
    rcases exists_between (abs_lt.2 ha) with ⟨b, hab, hbR⟩,
    exact ⟨b, ⟨(abs_nonneg a).trans_lt hab, hbR⟩,
      H.trans_is_o (is_o_pow_pow_of_abs_lt_left (hab.trans_le (le_abs_self b)))⟩ },
  tfae_have : 2 → 4, from λ ⟨a, ha, H⟩, ⟨a, ha, H.is_O⟩,
  tfae_have : 4 → 3, from λ ⟨a, ha, H⟩, ⟨a, B ha, H⟩,
  -- Add 5 and 6 using 4 → 6 → 5 → 3
  tfae_have : 4 → 6,
  { rintro ⟨a, ha, H⟩,
    rcases bound_of_is_O_nat_at_top H with ⟨C, hC₀, hC⟩,
    refine ⟨a, ha, C, hC₀, λ n, _⟩,
    simpa only [real.norm_eq_abs, abs_pow, abs_of_nonneg ha.1.le]
      using hC (pow_ne_zero n ha.1.ne') },
  tfae_have : 6 → 5, from λ ⟨a, ha, C, H₀, H⟩, ⟨a, ha.2, C, or.inl H₀, H⟩,
  tfae_have : 5 → 3,
  { rintro ⟨a, ha, C, h₀, H⟩,
    rcases sign_cases_of_C_mul_pow_nonneg (λ n, (abs_nonneg _).trans (H n)) with rfl | ⟨hC₀, ha₀⟩,
    { obtain rfl : f = 0, by { ext n, simpa using H n },
      simp only [lt_irrefl, false_or] at h₀,
      exact ⟨0, ⟨neg_lt_zero.2 h₀, h₀⟩, is_O_zero _ _⟩ },
    exact ⟨a, A ⟨ha₀, ha⟩,
      is_O_of_le' _ (λ n, (H n).trans $ mul_le_mul_of_nonneg_left (le_abs_self _) hC₀.le)⟩ },
  -- Add 7 and 8 using 2 → 8 → 7 → 3
  tfae_have : 2 → 8,
  { rintro ⟨a, ha, H⟩,
    refine ⟨a, ha, (H.def zero_lt_one).mono (λ n hn, _)⟩,
    rwa [real.norm_eq_abs, real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn },
  tfae_have : 8 → 7, from λ ⟨a, ha, H⟩, ⟨a, ha.2, H⟩,
  tfae_have : 7 → 3,
  { rintro ⟨a, ha, H⟩,
    have : 0 ≤ a, from nonneg_of_eventually_pow_nonneg (H.mono $ λ n, (abs_nonneg _).trans),
    refine ⟨a, A ⟨this, ha⟩, is_O.of_bound 1 _⟩,
    simpa only [real.norm_eq_abs, one_mul, abs_pow, abs_of_nonneg this] },
  tfae_finish
end

/-- For any natural `k` and a real `r > 1` we have `n ^ k = o(r ^ n)` as `n → ∞`. -/
lemma is_o_pow_const_const_pow_of_one_lt {R : Type*} [normed_ring R] (k : ℕ) {r : ℝ} (hr : 1 < r) :
  (λ n, n ^ k : ℕ → R) =o[at_top] (λ n, r ^ n) :=
begin
  have : tendsto (λ x : ℝ, x ^ k) (𝓝[>] 1) (𝓝 1),
    from ((continuous_id.pow k).tendsto' (1 : ℝ) 1 (one_pow _)).mono_left inf_le_left,
  obtain ⟨r' : ℝ, hr' : r' ^ k < r, h1 : 1 < r'⟩ :=
    ((this.eventually (gt_mem_nhds hr)).and self_mem_nhds_within).exists,
  have h0 : 0 ≤ r' := zero_le_one.trans h1.le,
  suffices : (λ n, n ^ k : ℕ → R) =O[at_top] (λ n : ℕ, (r' ^ k) ^ n),
    from this.trans_is_o (is_o_pow_pow_of_lt_left (pow_nonneg h0 _) hr'),
  conv in ((r' ^ _) ^ _) { rw [← pow_mul, mul_comm, pow_mul] },
  suffices : ∀ n : ℕ, ∥(n : R)∥ ≤ (r' - 1)⁻¹ * ∥(1 : R)∥ * ∥r' ^ n∥,
    from (is_O_of_le' _ this).pow _,
  intro n, rw mul_right_comm,
  refine n.norm_cast_le.trans (mul_le_mul_of_nonneg_right _ (norm_nonneg _)),
  simpa [div_eq_inv_mul, real.norm_eq_abs, abs_of_nonneg h0] using n.cast_le_pow_div_sub h1
end

/-- For a real `r > 1` we have `n = o(r ^ n)` as `n → ∞`. -/
lemma is_o_coe_const_pow_of_one_lt {R : Type*} [normed_ring R] {r : ℝ} (hr : 1 < r) :
  (coe : ℕ → R) =o[at_top] (λ n, r ^ n) :=
by simpa only [pow_one] using @is_o_pow_const_const_pow_of_one_lt R _ 1 _ hr

/-- If `∥r₁∥ < r₂`, then for any naturak `k` we have `n ^ k r₁ ^ n = o (r₂ ^ n)` as `n → ∞`. -/
lemma is_o_pow_const_mul_const_pow_const_pow_of_norm_lt {R : Type*} [normed_ring R] (k : ℕ)
  {r₁ : R} {r₂ : ℝ} (h : ∥r₁∥ < r₂) :
  (λ n, n ^ k * r₁ ^ n : ℕ → R) =o[at_top] (λ n, r₂ ^ n) :=
begin
  by_cases h0 : r₁ = 0,
  { refine (is_o_zero _ _).congr' (mem_at_top_sets.2 $ ⟨1, λ n hn, _⟩) eventually_eq.rfl,
    simp [zero_pow (zero_lt_one.trans_le hn), h0] },
  rw [← ne.def, ← norm_pos_iff] at h0,
  have A : (λ n, n ^ k : ℕ → R) =o[at_top] (λ n, (r₂ / ∥r₁∥) ^ n),
    from is_o_pow_const_const_pow_of_one_lt k ((one_lt_div h0).2 h),
  suffices : (λ n, r₁ ^ n) =O[at_top] (λ n, ∥r₁∥ ^ n),
    by simpa [div_mul_cancel _ (pow_pos h0 _).ne'] using A.mul_is_O this,
  exact is_O.of_bound 1 (by simpa using eventually_norm_pow_le r₁)
end

lemma tendsto_pow_const_div_const_pow_of_one_lt (k : ℕ) {r : ℝ} (hr : 1 < r) :
  tendsto (λ n, n ^ k / r ^ n : ℕ → ℝ) at_top (𝓝 0) :=
(is_o_pow_const_const_pow_of_one_lt k hr).tendsto_div_nhds_zero

/-- If `|r| < 1`, then `n ^ k r ^ n` tends to zero for any natural `k`. -/
lemma tendsto_pow_const_mul_const_pow_of_abs_lt_one (k : ℕ) {r : ℝ} (hr : |r| < 1) :
  tendsto (λ n, n ^ k * r ^ n : ℕ → ℝ) at_top (𝓝 0) :=
begin
  by_cases h0 : r = 0,
  { exact tendsto_const_nhds.congr'
      (mem_at_top_sets.2 ⟨1, λ n hn, by simp [zero_lt_one.trans_le hn, h0]⟩) },
  have hr' : 1 < (|r|)⁻¹, from one_lt_inv (abs_pos.2 h0) hr,
  rw tendsto_zero_iff_norm_tendsto_zero,
  simpa [div_eq_mul_inv] using tendsto_pow_const_div_const_pow_of_one_lt k hr'
end

/-- If `0 ≤ r < 1`, then `n ^ k r ^ n` tends to zero for any natural `k`.
This is a specialized version of `tendsto_pow_const_mul_const_pow_of_abs_lt_one`, singled out
for ease of application. -/
lemma tendsto_pow_const_mul_const_pow_of_lt_one (k : ℕ) {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :
  tendsto (λ n, n ^ k * r ^ n : ℕ → ℝ) at_top (𝓝 0) :=
tendsto_pow_const_mul_const_pow_of_abs_lt_one k (abs_lt.2 ⟨neg_one_lt_zero.trans_le hr, h'r⟩)

/-- If `|r| < 1`, then `n * r ^ n` tends to zero. -/
lemma tendsto_self_mul_const_pow_of_abs_lt_one {r : ℝ} (hr : |r| < 1) :
  tendsto (λ n, n * r ^ n : ℕ → ℝ) at_top (𝓝 0) :=
by simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_abs_lt_one 1 hr

/-- If `0 ≤ r < 1`, then `n * r ^ n` tends to zero. This is a specialized version of
`tendsto_self_mul_const_pow_of_abs_lt_one`, singled out for ease of application. -/
lemma tendsto_self_mul_const_pow_of_lt_one {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :
  tendsto (λ n, n * r ^ n : ℕ → ℝ) at_top (𝓝 0) :=
by simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_lt_one 1 hr h'r

/-- In a normed ring, the powers of an element x with `∥x∥ < 1` tend to zero. -/
lemma tendsto_pow_at_top_nhds_0_of_norm_lt_1 {R : Type*} [normed_ring R] {x : R}
  (h : ∥x∥ < 1) : tendsto (λ (n : ℕ), x ^ n) at_top (𝓝 0) :=
begin
  apply squeeze_zero_norm' (eventually_norm_pow_le x),
  exact tendsto_pow_at_top_nhds_0_of_lt_1 (norm_nonneg _) h,
end

lemma tendsto_pow_at_top_nhds_0_of_abs_lt_1 {r : ℝ} (h : |r| < 1) :
  tendsto (λn:ℕ, r^n) at_top (𝓝 0) :=
tendsto_pow_at_top_nhds_0_of_norm_lt_1 h

/-! ### Geometric series-/
section geometric

variables {K : Type*} [normed_field K] {ξ : K}

lemma has_sum_geometric_of_norm_lt_1 (h : ∥ξ∥ < 1) : has_sum (λn:ℕ, ξ ^ n) (1 - ξ)⁻¹ :=
begin
  have xi_ne_one : ξ ≠ 1, by { contrapose! h, simp [h] },
  have A : tendsto (λn, (ξ ^ n - 1) * (ξ - 1)⁻¹) at_top (𝓝 ((0 - 1) * (ξ - 1)⁻¹)),
    from ((tendsto_pow_at_top_nhds_0_of_norm_lt_1 h).sub tendsto_const_nhds).mul tendsto_const_nhds,
  rw [has_sum_iff_tendsto_nat_of_summable_norm],
  { simpa [geom_sum_eq, xi_ne_one, neg_inv, div_eq_mul_inv] using A },
  { simp [norm_pow, summable_geometric_of_lt_1 (norm_nonneg _) h] }
end

lemma summable_geometric_of_norm_lt_1 (h : ∥ξ∥ < 1) : summable (λn:ℕ, ξ ^ n) :=
⟨_, has_sum_geometric_of_norm_lt_1 h⟩

lemma tsum_geometric_of_norm_lt_1 (h : ∥ξ∥ < 1) : ∑'n:ℕ, ξ ^ n = (1 - ξ)⁻¹ :=
(has_sum_geometric_of_norm_lt_1 h).tsum_eq

lemma has_sum_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) : has_sum (λn:ℕ, r ^ n) (1 - r)⁻¹ :=
has_sum_geometric_of_norm_lt_1 h

lemma summable_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) : summable (λn:ℕ, r ^ n) :=
summable_geometric_of_norm_lt_1 h

lemma tsum_geometric_of_abs_lt_1 {r : ℝ} (h : |r| < 1) : ∑'n:ℕ, r ^ n = (1 - r)⁻¹ :=
tsum_geometric_of_norm_lt_1 h

/-- A geometric series in a normed field is summable iff the norm of the common ratio is less than
one. -/
@[simp] lemma summable_geometric_iff_norm_lt_1 : summable (λ n : ℕ, ξ ^ n) ↔ ∥ξ∥ < 1 :=
begin
  refine ⟨λ h, _, summable_geometric_of_norm_lt_1⟩,
  obtain ⟨k : ℕ, hk : dist (ξ ^ k) 0 < 1⟩ :=
    (h.tendsto_cofinite_zero.eventually (ball_mem_nhds _ zero_lt_one)).exists,
  simp only [norm_pow, dist_zero_right] at hk,
  rw [← one_pow k] at hk,
  exact lt_of_pow_lt_pow _ zero_le_one hk
end

end geometric

section mul_geometric

lemma summable_norm_pow_mul_geometric_of_norm_lt_1 {R : Type*} [normed_ring R]
  (k : ℕ) {r : R} (hr : ∥r∥ < 1) : summable (λ n : ℕ, ∥(n ^ k * r ^ n : R)∥) :=
begin
  rcases exists_between hr with ⟨r', hrr', h⟩,
  exact summable_of_is_O_nat (summable_geometric_of_lt_1 ((norm_nonneg _).trans hrr'.le) h)
    (is_o_pow_const_mul_const_pow_const_pow_of_norm_lt _ hrr').is_O.norm_left
end

lemma summable_pow_mul_geometric_of_norm_lt_1 {R : Type*} [normed_ring R] [complete_space R]
  (k : ℕ) {r : R} (hr : ∥r∥ < 1) : summable (λ n, n ^ k * r ^ n : ℕ → R) :=
summable_of_summable_norm $ summable_norm_pow_mul_geometric_of_norm_lt_1 _ hr

/-- If `∥r∥ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`, `has_sum` version. -/
lemma has_sum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type*} [normed_field 𝕜] [complete_space 𝕜]
  {r : 𝕜} (hr : ∥r∥ < 1) : has_sum (λ n, n * r ^ n : ℕ → 𝕜) (r / (1 - r) ^ 2) :=
begin
  have A : summable (λ n, n * r ^ n : ℕ → 𝕜),
    by simpa using summable_pow_mul_geometric_of_norm_lt_1 1 hr,
  have B : has_sum (pow r : ℕ → 𝕜) (1 - r)⁻¹, from has_sum_geometric_of_norm_lt_1 hr,
  refine A.has_sum_iff.2 _,
  have hr' : r ≠ 1, by { rintro rfl, simpa [lt_irrefl] using hr },
  set s : 𝕜 := ∑' n : ℕ, n * r ^ n,
  calc s = (1 - r) * s / (1 - r) : (mul_div_cancel_left _ (sub_ne_zero.2 hr'.symm)).symm
  ... = (s - r * s) / (1 - r) : by rw [sub_mul, one_mul]
  ... = ((0 : ℕ) * r ^ 0 + (∑' n : ℕ, (n + 1 : ℕ) * r ^ (n + 1)) - r * s) / (1 - r) :
    by rw ← tsum_eq_zero_add A
  ... = (r * (∑' n : ℕ, (n + 1) * r ^ n) - r * s) / (1 - r) :
    by simp [pow_succ, mul_left_comm _ r, tsum_mul_left]
  ... = r / (1 - r) ^ 2 :
    by simp [add_mul, tsum_add A B.summable, mul_add, B.tsum_eq, ← div_eq_mul_inv, sq,
      div_div]
end

/-- If `∥r∥ < 1`, then `∑' n : ℕ, n * r ^ n = r / (1 - r) ^ 2`. -/
lemma tsum_coe_mul_geometric_of_norm_lt_1 {𝕜 : Type*} [normed_field 𝕜] [complete_space 𝕜]
  {r : 𝕜} (hr : ∥r∥ < 1) :
  (∑' n : ℕ, n * r ^ n : 𝕜) = (r / (1 - r) ^ 2) :=
(has_sum_coe_mul_geometric_of_norm_lt_1 hr).tsum_eq

end mul_geometric

section summable_le_geometric

variables [semi_normed_group α] {r C : ℝ} {f : ℕ → α}

lemma semi_normed_group.cauchy_seq_of_le_geometric {C : ℝ} {r : ℝ} (hr : r < 1)
  {u : ℕ → α} (h : ∀ n, ∥u n - u (n + 1)∥ ≤ C*r^n) : cauchy_seq u :=
cauchy_seq_of_le_geometric r C hr (by simpa [dist_eq_norm] using h)

lemma dist_partial_sum_le_of_le_geometric (hf : ∀n, ∥f n∥ ≤ C * r^n) (n : ℕ) :
  dist (∑ i in range n, f i) (∑ i in range (n+1), f i) ≤ C * r ^ n :=
begin
  rw [sum_range_succ, dist_eq_norm, ← norm_neg, neg_sub, add_sub_cancel'],
  exact hf n,
end

/-- If `∥f n∥ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` form a
Cauchy sequence. This lemma does not assume `0 ≤ r` or `0 ≤ C`. -/
lemma cauchy_seq_finset_of_geometric_bound (hr : r < 1) (hf : ∀n, ∥f n∥ ≤ C * r^n) :
  cauchy_seq (λ s : finset (ℕ), ∑ x in s, f x) :=
cauchy_seq_finset_of_norm_bounded _
  (aux_has_sum_of_le_geometric hr (dist_partial_sum_le_of_le_geometric hf)).summable hf

/-- If `∥f n∥ ≤ C * r ^ n` for all `n : ℕ` and some `r < 1`, then the partial sums of `f` are within
distance `C * r ^ n / (1 - r)` of the sum of the series. This lemma does not assume `0 ≤ r` or
`0 ≤ C`. -/
lemma norm_sub_le_of_geometric_bound_of_has_sum (hr : r < 1) (hf : ∀n, ∥f n∥ ≤ C * r^n)
  {a : α} (ha : has_sum f a) (n : ℕ) :
  ∥(∑ x in finset.range n, f x) - a∥ ≤ (C * r ^ n) / (1 - r) :=
begin
  rw ← dist_eq_norm,
  apply dist_le_of_le_geometric_of_tendsto r C hr (dist_partial_sum_le_of_le_geometric hf),
  exact ha.tendsto_sum_nat
end

@[simp] lemma dist_partial_sum (u : ℕ → α) (n : ℕ) :
 dist (∑ k in range (n + 1), u k) (∑ k in range n, u k) = ∥u n∥ :=
by simp [dist_eq_norm, sum_range_succ]

@[simp] lemma dist_partial_sum' (u : ℕ → α) (n : ℕ) :
 dist (∑ k in range n, u k) (∑ k in range (n+1), u k) = ∥u n∥ :=
by simp [dist_eq_norm', sum_range_succ]

lemma cauchy_series_of_le_geometric {C : ℝ} {u : ℕ → α}
  {r : ℝ} (hr : r < 1) (h : ∀ n, ∥u n∥ ≤ C*r^n) : cauchy_seq (λ n, ∑ k in range n, u k) :=
cauchy_seq_of_le_geometric r C hr (by simp [h])

lemma normed_group.cauchy_series_of_le_geometric' {C : ℝ} {u : ℕ → α} {r : ℝ} (hr : r < 1)
  (h : ∀ n, ∥u n∥ ≤ C*r^n) : cauchy_seq (λ n, ∑ k in range (n + 1), u k) :=
(cauchy_series_of_le_geometric hr h).comp_tendsto $ tendsto_add_at_top_nat 1

lemma normed_group.cauchy_series_of_le_geometric'' {C : ℝ} {u : ℕ → α} {N : ℕ} {r : ℝ}
  (hr₀ : 0 < r) (hr₁ : r < 1)
  (h : ∀ n ≥ N, ∥u n∥ ≤ C*r^n) : cauchy_seq (λ n, ∑ k in range (n + 1), u k) :=
begin
  set v : ℕ → α := λ n, if n < N then 0 else u n,
  have hC : 0 ≤ C,
    from (zero_le_mul_right $ pow_pos hr₀ N).mp ((norm_nonneg _).trans $ h N $ le_refl N),
  have : ∀ n ≥ N, u n = v n,
  { intros n hn,
    simp [v, hn, if_neg (not_lt.mpr hn)] },
  refine cauchy_seq_sum_of_eventually_eq this (normed_group.cauchy_series_of_le_geometric' hr₁ _),
  { exact C },
  intro n,
  dsimp [v],
  split_ifs with H H,
  { rw norm_zero,
    exact mul_nonneg hC (pow_nonneg hr₀.le _) },
  { push_neg at H,
    exact h _ H }
end

end summable_le_geometric

section normed_ring_geometric
variables {R : Type*} [normed_ring R] [complete_space R]

open normed_space

/-- A geometric series in a complete normed ring is summable.
Proved above (same name, different namespace) for not-necessarily-complete normed fields. -/
lemma normed_ring.summable_geometric_of_norm_lt_1
  (x : R) (h : ∥x∥ < 1) : summable (λ (n:ℕ), x ^ n) :=
begin
  have h1 : summable (λ (n:ℕ), ∥x∥ ^ n) := summable_geometric_of_lt_1 (norm_nonneg _) h,
  refine summable_of_norm_bounded_eventually _ h1 _,
  rw nat.cofinite_eq_at_top,
  exact eventually_norm_pow_le x,
end

/-- Bound for the sum of a geometric series in a normed ring.  This formula does not assume that the
normed ring satisfies the axiom `∥1∥ = 1`. -/
lemma normed_ring.tsum_geometric_of_norm_lt_1
  (x : R) (h : ∥x∥ < 1) : ∥∑' n:ℕ, x ^ n∥ ≤ ∥(1:R)∥ - 1 + (1 - ∥x∥)⁻¹ :=
begin
  rw tsum_eq_zero_add (normed_ring.summable_geometric_of_norm_lt_1 x h),
  simp only [pow_zero],
  refine le_trans (norm_add_le _ _) _,
  have : ∥∑' b : ℕ, (λ n, x ^ (n + 1)) b∥ ≤ (1 - ∥x∥)⁻¹ - 1,
  { refine tsum_of_norm_bounded _ (λ b, norm_pow_le' _ (nat.succ_pos b)),
    convert (has_sum_nat_add_iff' 1).mpr (has_sum_geometric_of_lt_1 (norm_nonneg x) h),
    simp },
  linarith
end

lemma geom_series_mul_neg (x : R) (h : ∥x∥ < 1) :
  (∑' i:ℕ, x ^ i) * (1 - x) = 1 :=
begin
  have := ((normed_ring.summable_geometric_of_norm_lt_1 x h).has_sum.mul_right (1 - x)),
  refine tendsto_nhds_unique this.tendsto_sum_nat _,
  have : tendsto (λ (n : ℕ), 1 - x ^ n) at_top (𝓝 1),
  { simpa using tendsto_const_nhds.sub (tendsto_pow_at_top_nhds_0_of_norm_lt_1 h) },
  convert ← this,
  ext n,
  rw [←geom_sum_mul_neg, finset.sum_mul],
end

lemma mul_neg_geom_series (x : R) (h : ∥x∥ < 1) :
  (1 - x) * ∑' i:ℕ, x ^ i = 1 :=
begin
  have := (normed_ring.summable_geometric_of_norm_lt_1 x h).has_sum.mul_left (1 - x),
  refine tendsto_nhds_unique this.tendsto_sum_nat _,
  have : tendsto (λ (n : ℕ), 1 - x ^ n) at_top (nhds 1),
  { simpa using tendsto_const_nhds.sub
      (tendsto_pow_at_top_nhds_0_of_norm_lt_1 h) },
  convert ← this,
  ext n,
  rw [←mul_neg_geom_sum, finset.mul_sum]
end

end normed_ring_geometric

/-! ### Summability tests based on comparison with geometric series -/

lemma summable_of_ratio_norm_eventually_le {α : Type*} [semi_normed_group α] [complete_space α]
  {f : ℕ → α} {r : ℝ} (hr₁ : r < 1)
  (h : ∀ᶠ n in at_top, ∥f (n+1)∥ ≤ r * ∥f n∥) : summable f :=
begin
  by_cases hr₀ : 0 ≤ r,
  { rw eventually_at_top at h,
    rcases h with ⟨N, hN⟩,
    rw ← @summable_nat_add_iff α _ _ _ _ N,
    refine summable_of_norm_bounded (λ n, ∥f N∥ * r^n)
      (summable.mul_left _ $ summable_geometric_of_lt_1 hr₀ hr₁) (λ n, _),
    conv_rhs {rw [mul_comm, ← zero_add N]},
    refine le_geom hr₀ n (λ i _, _),
    convert hN (i + N) (N.le_add_left i) using 3,
    ac_refl },
  { push_neg at hr₀,
    refine summable_of_norm_bounded_eventually 0 summable_zero _,
    rw nat.cofinite_eq_at_top,
    filter_upwards [h] with _ hn,
    by_contra' h,
    exact not_lt.mpr (norm_nonneg _) (lt_of_le_of_lt hn $ mul_neg_of_neg_of_pos hr₀ h), },
end

lemma summable_of_ratio_test_tendsto_lt_one {α : Type*} [normed_group α] [complete_space α]
  {f : ℕ → α} {l : ℝ} (hl₁ : l < 1) (hf : ∀ᶠ n in at_top, f n ≠ 0)
  (h : tendsto (λ n, ∥f (n+1)∥/∥f n∥) at_top (𝓝 l)) : summable f :=
begin
  rcases exists_between hl₁ with ⟨r, hr₀, hr₁⟩,
  refine summable_of_ratio_norm_eventually_le hr₁ _,
  filter_upwards [eventually_le_of_tendsto_lt hr₀ h, hf] with _ _ h₁,
  rwa ← div_le_iff (norm_pos_iff.mpr h₁),
end

lemma not_summable_of_ratio_norm_eventually_ge {α : Type*} [semi_normed_group α]
  {f : ℕ → α} {r : ℝ} (hr : 1 < r) (hf : ∃ᶠ n in at_top, ∥f n∥ ≠ 0)
  (h : ∀ᶠ n in at_top, r * ∥f n∥ ≤ ∥f (n+1)∥) : ¬ summable f :=
begin
  rw eventually_at_top at h,
  rcases h with ⟨N₀, hN₀⟩,
  rw frequently_at_top at hf,
  rcases hf N₀ with ⟨N, hNN₀ : N₀ ≤ N, hN⟩,
  rw ← @summable_nat_add_iff α _ _ _ _ N,
  refine mt summable.tendsto_at_top_zero
    (λ h', not_tendsto_at_top_of_tendsto_nhds (tendsto_norm_zero.comp h') _),
  convert tendsto_at_top_of_geom_le _ hr _,
  { refine lt_of_le_of_ne (norm_nonneg _) _,
    intro h'',
    specialize hN₀ N hNN₀,
    simp only [comp_app, zero_add] at h'',
    exact hN h''.symm },
  { intro i,
    dsimp only [comp_app],
    convert (hN₀ (i + N) (hNN₀.trans (N.le_add_left i))) using 3,
    ac_refl }
end

lemma not_summable_of_ratio_test_tendsto_gt_one {α : Type*} [semi_normed_group α]
  {f : ℕ → α} {l : ℝ} (hl : 1 < l)
  (h : tendsto (λ n, ∥f (n+1)∥/∥f n∥) at_top (𝓝 l)) : ¬ summable f :=
begin
  have key : ∀ᶠ n in at_top, ∥f n∥ ≠ 0,
  { filter_upwards [eventually_ge_of_tendsto_gt hl h] with _ hn hc,
    rw [hc, div_zero] at hn,
    linarith },
  rcases exists_between hl with ⟨r, hr₀, hr₁⟩,
  refine not_summable_of_ratio_norm_eventually_ge hr₀ key.frequently _,
  filter_upwards [eventually_ge_of_tendsto_gt hr₁ h, key] with _ _ h₁,
  rwa ← le_div_iff (lt_of_le_of_ne (norm_nonneg _) h₁.symm)
end

section
/-! ### Dirichlet and alternating series tests -/

variables {E : Type*} [normed_group E] [normed_space ℝ E]
variables {b : ℝ} {f : ℕ → ℝ} {z : ℕ → E}

/-- **Dirichlet's Test** for monotone sequences. -/
theorem monotone.cauchy_seq_series_mul_of_tendsto_zero_of_bounded
  (hfa : monotone f) (hf0 : tendsto f at_top (𝓝 0)) (hgb : ∀ n, ∥∑ i in range n, z i∥ ≤ b) :
  cauchy_seq (λ n, ∑ i in range (n + 1), (f i) • z i) :=
begin
  simp_rw [finset.sum_range_by_parts _ _ (nat.succ _), sub_eq_add_neg,
           nat.succ_sub_succ_eq_sub, tsub_zero],
  apply (normed_field.tendsto_zero_smul_of_tendsto_zero_of_bounded hf0
    ⟨b, eventually_map.mpr $ eventually_of_forall $ λ n, hgb $ n+1⟩).cauchy_seq.add,
  apply (cauchy_seq_range_of_norm_bounded _ _ (_ : ∀ n, _ ≤ b * |f(n+1) - f(n)|)).neg,
  { exact normed_uniform_group },
  { simp_rw [abs_of_nonneg (sub_nonneg_of_le (hfa (nat.le_succ _))), ← mul_sum],
    apply real.uniform_continuous_mul_const.comp_cauchy_seq,
    simp_rw [sum_range_sub, sub_eq_add_neg],
    exact (tendsto.cauchy_seq hf0).add_const },
  { intro n,
    rw [norm_smul, mul_comm],
    exact mul_le_mul_of_nonneg_right (hgb _) (abs_nonneg _) },
end

/-- **Dirichlet's test** for antitone sequences. -/
theorem antitone.cauchy_seq_series_mul_of_tendsto_zero_of_bounded
  (hfa : antitone f) (hf0 : tendsto f at_top (𝓝 0)) (hzb : ∀ n, ∥∑ i in range n, z i∥ ≤ b) :
  cauchy_seq (λ n, ∑ i in range (n+1), (f i) • z i) :=
begin
  have hfa': monotone (λ n, -f n) := λ _ _ hab, neg_le_neg $ hfa hab,
  have hf0': tendsto (λ n, -f n) at_top (𝓝 0) := by { convert hf0.neg, norm_num },
  convert (hfa'.cauchy_seq_series_mul_of_tendsto_zero_of_bounded hf0' hzb).neg,
  funext,
  simp
end

lemma norm_sum_neg_one_pow_le (n : ℕ) : ∥∑ i in range n, (-1 : ℝ) ^ i∥ ≤ 1 :=
by { rw [neg_one_geom_sum], split_ifs; norm_num }

/-- The **alternating series test** for monotone sequences.
See also `tendsto_alternating_series_of_monotone_tendsto_zero`. -/
theorem monotone.cauchy_seq_alternating_series_of_tendsto_zero
  (hfa : monotone f) (hf0 : tendsto f at_top (𝓝 0)) :
  cauchy_seq (λ n, ∑ i in range (n+1), (-1) ^ i * f i) :=
begin
  simp_rw [mul_comm],
  exact hfa.cauchy_seq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le
end

/-- The **alternating series test** for monotone sequences. -/
theorem monotone.tendsto_alternating_series_of_tendsto_zero
  (hfa : monotone f) (hf0 : tendsto f at_top (𝓝 0)) :
  ∃ l, tendsto (λ n, ∑ i in range (n+1), (-1) ^ i * f i) at_top (𝓝 l) :=
cauchy_seq_tendsto_of_complete $ hfa.cauchy_seq_alternating_series_of_tendsto_zero hf0

/-- The **alternating series test** for antitone sequences.
See also `tendsto_alternating_series_of_antitone_tendsto_zero`. -/
theorem antitone.cauchy_seq_alternating_series_of_tendsto_zero
  (hfa : antitone f) (hf0 : tendsto f at_top (𝓝 0)) :
  cauchy_seq (λ n, ∑ i in range (n+1), (-1) ^ i * f i) :=
begin
  simp_rw [mul_comm],
  exact
    hfa.cauchy_seq_series_mul_of_tendsto_zero_of_bounded hf0 norm_sum_neg_one_pow_le
end

/-- The **alternating series test** for antitone sequences. -/
theorem antitone.tendsto_alternating_series_of_tendsto_zero
  (hfa : antitone f) (hf0 : tendsto f at_top (𝓝 0)) :
  ∃ l, tendsto (λ n, ∑ i in range (n+1), (-1) ^ i * f i) at_top (𝓝 l) :=
cauchy_seq_tendsto_of_complete $ hfa.cauchy_seq_alternating_series_of_tendsto_zero hf0

end

/-!
### Factorial
-/

/-- The series `∑' n, x ^ n / n!` is summable of any `x : ℝ`. See also `exp_series_div_summable`
for a version that also works in `ℂ`, and `exp_series_summable'` for a version that works in
any normed algebra over `ℝ` or `ℂ`. -/
lemma real.summable_pow_div_factorial (x : ℝ) :
  summable (λ n, x ^ n / n! : ℕ → ℝ) :=
begin
  -- We start with trivial extimates
  have A : (0 : ℝ) < ⌊∥x∥⌋₊ + 1, from zero_lt_one.trans_le (by simp),
  have B : ∥x∥ / (⌊∥x∥⌋₊ + 1) < 1, from (div_lt_one A).2 (nat.lt_floor_add_one _),
  -- Then we apply the ratio test. The estimate works for `n ≥ ⌊∥x∥⌋₊`.
  suffices : ∀ n ≥ ⌊∥x∥⌋₊, ∥x ^ (n + 1) / (n + 1)!∥ ≤ ∥x∥ / (⌊∥x∥⌋₊ + 1) * ∥x ^ n / ↑n!∥,
    from summable_of_ratio_norm_eventually_le B (eventually_at_top.2 ⟨⌊∥x∥⌋₊, this⟩),
  -- Finally, we prove the upper estimate
  intros n hn,
  calc ∥x ^ (n + 1) / (n + 1)!∥ = (∥x∥ / (n + 1)) * ∥x ^ n / n!∥ :
    by rw [pow_succ, nat.factorial_succ, nat.cast_mul, ← div_mul_div_comm,
      norm_mul, norm_div, real.norm_coe_nat, nat.cast_succ]
  ... ≤ (∥x∥ / (⌊∥x∥⌋₊ + 1)) * ∥x ^ n / n!∥ :
    by mono* with [0 ≤ ∥x ^ n / n!∥, 0 ≤ ∥x∥]; apply norm_nonneg
end

lemma real.tendsto_pow_div_factorial_at_top (x : ℝ) :
  tendsto (λ n, x ^ n / n! : ℕ → ℝ) at_top (𝓝 0) :=
(real.summable_pow_div_factorial x).tendsto_at_top_zero

author: nick-kuhn

repo: leantools

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


text:
import data.matrix .matrix_pequiv tactic.linarith data.zmod.basic

variables {α : Type*}

open equiv pequiv matrix

local infix ` ⬝ `:70 := matrix.mul
local postfix `ᵀ` : 1500 := transpose

namespace pequiv

def diagonal_ul (m n r : ℕ) : fin m ≃. fin n :=
{ to_fun := λ i, if hi : i.1 < r ∧ i.1 < n then some ⟨i.1, hi.2⟩ else none,
  inv_fun := λ j, if hj : j.1 < r ∧ j.1 < m then some ⟨j.1, hj.2⟩ else none,
  inv := λ ⟨i, hi⟩ ⟨j, hj⟩, begin
    clear_aux_decl,
    dsimp,
    split_ifs,
    { simp [eq_comm] },
    { simp, intros h, simp [*, -not_lt] at * },
    { simp, intro h, simp [*, -not_lt] at * },
    { simp }
  end }

lemma symm_diagonal_ul (m n r : ℕ) : (diagonal_ul m n r).symm =
  diagonal_ul n m r := rfl

def equiv.anti_diagonal (n : ℕ) : fin n ≃ fin n :=
{ to_fun := λ i, ⟨n - (i.1 + 1), nat.sub_lt (lt_of_le_of_lt (nat.zero_le _) i.2) (nat.succ_pos _)⟩,
  inv_fun := λ i, ⟨n - (i.1 + 1), nat.sub_lt (lt_of_le_of_lt (nat.zero_le _) i.2) (nat.succ_pos _)⟩,
  left_inv := λ ⟨i, hi⟩, fin.eq_of_veq $
    by dsimp; rw [nat.sub_add_eq_add_sub hi, nat.succ_sub_succ, nat.sub_sub_self (le_of_lt hi)],
  right_inv := λ ⟨i, hi⟩, fin.eq_of_veq $
    by dsimp; rw [nat.sub_add_eq_add_sub hi, nat.succ_sub_succ, nat.sub_sub_self (le_of_lt hi)] }

def diagonal_dr (m n r : ℕ) : fin m ≃. fin n :=
((equiv.anti_diagonal m).to_pequiv.trans (diagonal_ul m n r)).trans
  (equiv.anti_diagonal n).to_pequiv

end pequiv

/-- pick a matrix element that matches a given property or return none in case of no match. -/
def pick (p : α → Prop) [decidable_pred p] {m n : ℕ} (A : matrix (fin m) (fin n) α) :
  option (fin m × fin n) :=
if h : ∃ (ij : fin m × fin n), p (A ij.1 ij.2) then some (encodable.choose h) else none

open pequiv

def Gaussian_elimination [discrete_field α] : Π {m n}, matrix (fin m) (fin n) α →
   (matrix (fin m) (fin m) α × matrix (fin n) (fin n) α × ℕ)
| (x+1) (y+1) A :=
  match pick (λ el : α, el ≠ 0) A with
  | none        := (1, 1, 0)
  | some (i, j) :=
    let B := (swap 0 i).to_pequiv.to_matrix ⬝ A ⬝
      (swap 0 j).to_pequiv.to_matrix in
    let ur := (diagonal_ul 1 (x+1) 1).to_matrix ⬝ B ⬝
      (diagonal_dr (y+1) y y).to_matrix in
    let dl := (A i j)⁻¹ • (diagonal_dr x (x+1) x).to_matrix ⬝ B ⬝
      (diagonal_ul (y+1) 1 1).to_matrix in
    let dr := (diagonal_dr x (x+1) x).to_matrix ⬝ B ⬝
      (diagonal_dr (y+1) y y).to_matrix in
    let ⟨L, U, r⟩ := Gaussian_elimination (dr - dl ⬝ ur) in
    --L
    ((swap 0 i).to_pequiv.to_matrix ⬝
      ((single 0 0).to_matrix +
      (diagonal_dr (x+1) x x).to_matrix ⬝
      (dl ⬝ (diagonal_ul 1 (x+1) 1).to_matrix +
        L ⬝ (diagonal_dr x (x+1) x).to_matrix)),
    --U
    (A i j • (single 0 0).to_matrix +
        ((diagonal_dr _ _ y).to_matrix ⬝ U +
         (diagonal_ul _ _ y).to_matrix ⬝ ur) ⬝
        (diagonal_dr y (y+1) y).to_matrix)
      ⬝ (swap 0 j).to_pequiv.to_matrix,
    --r
    r+1)
  end
| x y A := ((1 : matrix (fin x) (fin x) α),
  (1 : matrix (fin y) (fin y) α),
  0)

instance C {p : ℕ} (hp : nat.prime p) : has_repr (zmodp p hp) := fin.has_repr _

instance matrix.has_repr_fin_fun {n : ℕ} {α : Type*} [has_repr α] : has_repr (fin n → α) :=
⟨λ f, repr (vector.of_fn f).to_list⟩

instance {m n} {α : Type*} [has_repr α]: has_repr (matrix (fin m) (fin n) α) :=
matrix.has_repr_fin_fun

def list.to_matrix (m :ℕ) (n : ℕ) (l : list (list ℚ)) :
  matrix (fin m) (fin n) ℚ :=
λ i j, (l.nth_le i sorry).nth_le j sorry

#eval ((diagonal_ul 5 4 3).to_matrix : matrix _ _ ℚ)

def M := list.to_matrix 2 4 [[1,2,1,0], [4,5,0,1]]

#eval let S := Gaussian_elimination M in S.1 ⬝ (list.to_matrix 2 4 [[1,0,0,0], [0,1,0,0]]) ⬝
S.2.1

repo: LP


text:
-- Cancelativa_de_la_suma_por_la_izquierda.lean
-- Cancelativa de la suma por la izquierda.
-- José A. Alonso Jiménez <https://jaalonso.github.io>
-- Sevilla, 31-agosto-2022
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Demostrar que si R es un anillo y a, b, c ∈ R tales que
--    a + b = a + c
-- entonces
--    b = c
-- ---------------------------------------------------------------------

import algebra.ring
import tactic

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

-- 1ª demostración
-- ===============

example
  (h : a + b = a + c)
  : b = c :=
calc b
     = 0 + b        : by rw zero_add
 ... = (-a + a) + b : by rw add_left_neg
 ... = -a + (a + b) : by rw add_assoc
 ... = -a + (a + c) : by rw h
 ... = (-a + a) + c : by rw ←add_assoc
 ... = 0 + c        : by rw add_left_neg
 ... = c            : by rw zero_add

-- 2ª demostración
-- ===============

example
  (h : a + b = a + c)
  : b = c :=
calc b
     = 0 + b        : by simp
 ... = (-a + a) + b : by simp
 ... = -a + (a + b) : by simp
 ... = -a + (a + c) : by rw h
 ... = (-a + a) + c : by simp
 ... = 0 + c        : by simp
 ... = c            : by simp

-- 3ª demostración
-- ===============

lemma aux : -a + (a + b) = b :=
by finish

example
  (h : a + b = a + c)
  : b = c :=
calc b
     = -a + (a + b) : aux.symm
 ... = -a + (a + c) : congr_arg (λ x, -a + x) h
 ... = c            : aux

-- 4ª demostración
-- ===============

example
  (h : a + b = a + c)
  : b = c :=
-- by library_search
(add_right_inj a).mp h

-- 4ª demostración
-- ===============

example
  (h : a + b = a + c)
  : b = c :=
-- by hint
by finish

author: jaalonso

repo: Calculemus

save_path: github-repos/lean/jaalonso-Calculemus


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

import algebra.group.conj_finite
import group_theory.perm.fin
import group_theory.subgroup.simple
import tactic.interval_cases

/-!
# Alternating Groups

The alternating group on a finite type `α` is the subgroup of the permutation group `perm α`
consisting of the even permutations.

## Main definitions

* `alternating_group α` is the alternating group on `α`, defined as a `subgroup (perm α)`.

## Main results
* `two_mul_card_alternating_group` shows that the alternating group is half as large as
  the permutation group it is a subgroup of.

* `closure_three_cycles_eq_alternating` shows that the alternating group is
  generated by 3-cycles.

* `alternating_group.is_simple_group_five` shows that the alternating group on `fin 5` is simple.
  The proof shows that the normal closure of any non-identity element of this group contains a
  3-cycle.

## Tags
alternating group permutation

## TODO
* Show that `alternating_group α` is simple if and only if `fintype.card α ≠ 4`.

-/

open equiv equiv.perm subgroup fintype
variables (α : Type*) [fintype α] [decidable_eq α]

/-- The alternating group on a finite type, realized as a subgroup of `equiv.perm`.
  For $A_n$, use `alternating_group (fin n)`. -/
@[derive fintype] def alternating_group : subgroup (perm α) :=
sign.ker

instance [subsingleton α] : unique (alternating_group α) :=
⟨⟨1⟩, λ ⟨p, hp⟩, subtype.eq (subsingleton.elim p _)⟩

variables {α}

lemma alternating_group_eq_sign_ker : alternating_group α = sign.ker := rfl

namespace equiv.perm

@[simp]
lemma mem_alternating_group {f : perm α} :
  f ∈ alternating_group α ↔ sign f = 1 :=
sign.mem_ker

lemma prod_list_swap_mem_alternating_group_iff_even_length {l : list (perm α)}
  (hl : ∀ g ∈ l, is_swap g) :
  l.prod ∈ alternating_group α ↔ even l.length :=
begin
  rw [mem_alternating_group, sign_prod_list_swap hl, ← units.coe_eq_one, units.coe_pow,
    units.coe_neg_one, neg_one_pow_eq_one_iff_even],
  dec_trivial
end

lemma is_three_cycle.mem_alternating_group {f : perm α} (h : is_three_cycle f) :
  f ∈ alternating_group α :=
mem_alternating_group.2 h.sign

lemma fin_rotate_bit1_mem_alternating_group {n : ℕ} :
  fin_rotate (bit1 n) ∈ alternating_group (fin (bit1 n)) :=
by rw [mem_alternating_group, bit1, sign_fin_rotate, pow_bit0', int.units_mul_self, one_pow]

end equiv.perm

lemma two_mul_card_alternating_group [nontrivial α] :
  2 * card (alternating_group α) = card (perm α) :=
begin
  let := (quotient_group.quotient_ker_equiv_of_surjective _ (sign_surjective α)).to_equiv,
  rw [←fintype.card_units_int, ←fintype.card_congr this],
  exact (subgroup.card_eq_card_quotient_mul_card_subgroup _).symm,
end

namespace alternating_group
open equiv.perm

instance normal : (alternating_group α).normal := sign.normal_ker

lemma is_conj_of {σ τ : alternating_group α}
  (hc : is_conj (σ : perm α) (τ : perm α)) (hσ : (σ : perm α).support.card + 2 ≤ fintype.card α) :
  is_conj σ τ :=
begin
  obtain ⟨σ, hσ⟩ := σ,
  obtain ⟨τ, hτ⟩ := τ,
  obtain ⟨π, hπ⟩ := is_conj_iff.1 hc,
  rw [subtype.coe_mk, subtype.coe_mk] at hπ,
  cases int.units_eq_one_or (sign π) with h h,
  { rw is_conj_iff,
    refine ⟨⟨π, mem_alternating_group.mp h⟩, subtype.val_injective _⟩,
    simpa only [subtype.val_eq_coe, subgroup.coe_mul, coe_inv, coe_mk] using hπ },
  { have h2 : 2 ≤ σ.supportᶜ.card,
    { rw [finset.card_compl, le_tsub_iff_left σ.support.card_le_univ],
      exact hσ },
    obtain ⟨a, ha, b, hb, ab⟩ := finset.one_lt_card.1 h2,
    refine is_conj_iff.2 ⟨⟨π * swap a b, _⟩, subtype.val_injective _⟩,
    { rw [mem_alternating_group, monoid_hom.map_mul, h, sign_swap ab, int.units_mul_self] },
    { simp only [←hπ, coe_mk, subgroup.coe_mul, subtype.val_eq_coe],
      have hd : disjoint (swap a b) σ,
      { rw [disjoint_iff_disjoint_support, support_swap ab, finset.disjoint_insert_left,
          finset.disjoint_singleton_left],
        exact ⟨finset.mem_compl.1 ha, finset.mem_compl.1 hb⟩ },
      rw [mul_assoc π _ σ, hd.commute.eq, coe_inv, coe_mk],
      simp [mul_assoc] } }
end

lemma is_three_cycle_is_conj (h5 : 5 ≤ fintype.card α)
  {σ τ : alternating_group α}
  (hσ : is_three_cycle (σ : perm α)) (hτ : is_three_cycle (τ : perm α)) :
  is_conj σ τ :=
alternating_group.is_conj_of (is_conj_iff_cycle_type_eq.2 (hσ.trans hτ.symm))
  (by rwa hσ.card_support)

end alternating_group

namespace equiv.perm
open alternating_group

@[simp]
theorem closure_three_cycles_eq_alternating :
  closure {σ : perm α | is_three_cycle σ} = alternating_group α :=
closure_eq_of_le _ (λ σ hσ, mem_alternating_group.2 hσ.sign) $ λ σ hσ, begin
  suffices hind : ∀ (n : ℕ) (l : list (perm α)) (hl : ∀ g, g ∈ l → is_swap g)
    (hn : l.length = 2 * n), l.prod ∈ closure {σ : perm α | is_three_cycle σ},
  { obtain ⟨l, rfl, hl⟩ := trunc_swap_factors σ,
    obtain ⟨n, hn⟩ := (prod_list_swap_mem_alternating_group_iff_even_length hl).1 hσ,
    rw ← two_mul at hn,
    exact hind n l hl hn },
  intro n,
  induction n with n ih; intros l hl hn,
  { simp [list.length_eq_zero.1 hn, one_mem] },
  rw [nat.mul_succ] at hn,
  obtain ⟨a, l, rfl⟩ := l.exists_of_length_succ hn,
  rw [list.length_cons, nat.succ_inj'] at hn,
  obtain ⟨b, l, rfl⟩ := l.exists_of_length_succ hn,
  rw [list.prod_cons, list.prod_cons, ← mul_assoc],
  rw [list.length_cons, nat.succ_inj'] at hn,
  exact mul_mem (is_swap.mul_mem_closure_three_cycles (hl a (list.mem_cons_self a _))
    (hl b (list.mem_cons_of_mem a (l.mem_cons_self b))))
    (ih _ (λ g hg, hl g (list.mem_cons_of_mem _ (list.mem_cons_of_mem _ hg))) hn),
end

/-- A key lemma to prove $A_5$ is simple. Shows that any normal subgroup of an alternating group on
  at least 5 elements is the entire alternating group if it contains a 3-cycle. -/
lemma is_three_cycle.alternating_normal_closure (h5 : 5 ≤ fintype.card α)
  {f : perm α} (hf : is_three_cycle f) :
  normal_closure ({⟨f, hf.mem_alternating_group⟩} : set (alternating_group α)) = ⊤ :=
eq_top_iff.2 begin
  have hi : function.injective (alternating_group α).subtype := subtype.coe_injective,
  refine eq_top_iff.1 (map_injective hi (le_antisymm (map_mono le_top) _)),
  rw [← monoid_hom.range_eq_map, subtype_range, normal_closure, monoid_hom.map_closure],
  refine (le_of_eq closure_three_cycles_eq_alternating.symm).trans (closure_mono _),
  intros g h,
  obtain ⟨c, rfl⟩ := is_conj_iff.1 (is_conj_iff_cycle_type_eq.2 (hf.trans h.symm)),
  refine ⟨⟨c * f * c⁻¹, h.mem_alternating_group⟩, _, rfl⟩,
  rw group.mem_conjugates_of_set_iff,
  exact ⟨⟨f, hf.mem_alternating_group⟩, set.mem_singleton _, is_three_cycle_is_conj h5 hf h⟩
end

/-- Part of proving $A_5$ is simple. Shows that the square of any element of $A_5$ with a 3-cycle in
  its cycle decomposition is a 3-cycle, so the normal closure of the original element must be
  $A_5$. -/
lemma is_three_cycle_sq_of_three_mem_cycle_type_five {g : perm (fin 5)} (h : 3 ∈ cycle_type g) :
  is_three_cycle (g * g) :=
begin
  obtain ⟨c, g', rfl, hd, hc, h3⟩ := mem_cycle_type_iff.1 h,
  simp only [mul_assoc],
  rw [hd.commute.eq, ← mul_assoc g'],
  suffices hg' : order_of g' ∣ 2,
  { rw [← pow_two, order_of_dvd_iff_pow_eq_one.1 hg', one_mul],
    exact (card_support_eq_three_iff.1 h3).is_three_cycle_sq },
  rw [← lcm_cycle_type, multiset.lcm_dvd],
  intros n hn,
  rw le_antisymm (two_le_of_mem_cycle_type hn) (le_trans (le_card_support_of_mem_cycle_type hn) _),
  apply le_of_add_le_add_left,
  rw [← hd.card_support_mul, h3],
  exact (c * g').support.card_le_univ,
end

end equiv.perm

namespace alternating_group
open equiv.perm

lemma nontrivial_of_three_le_card (h3 : 3 ≤ card α) : nontrivial (alternating_group α) :=
begin
  haveI := fintype.one_lt_card_iff_nontrivial.1 (lt_trans dec_trivial h3),
  rw ← fintype.one_lt_card_iff_nontrivial,
  refine lt_of_mul_lt_mul_left _ (le_of_lt nat.prime_two.pos),
  rw [two_mul_card_alternating_group, card_perm, ← nat.succ_le_iff],
  exact le_trans h3 (card α).self_le_factorial,
end

instance {n : ℕ} : nontrivial (alternating_group (fin (n + 3))) :=
nontrivial_of_three_le_card (by { rw card_fin, exact le_add_left (le_refl 3) })

/-- The normal closure of the 5-cycle `fin_rotate 5` within $A_5$ is the whole group. This will be
  used to show that the normal closure of any 5-cycle within $A_5$ is the whole group. -/

/-- The normal closure of $(04)(13)$ within $A_5$ is the whole group. This will be
  used to show that the normal closure of any permutation of cycle type $(2,2)$ is the whole group.
  -/
lemma normal_closure_swap_mul_swap_five :
  (normal_closure ({⟨swap 0 4 * swap 1 3, mem_alternating_group.2 dec_trivial⟩} :
    set (alternating_group (fin 5)))) = ⊤ :=
begin
  let g1 := (⟨swap 0 2 * swap 0 1, mem_alternating_group.2 dec_trivial⟩ :
    alternating_group (fin 5)),
  let g2 := (⟨swap 0 4 * swap 1 3, mem_alternating_group.2 dec_trivial⟩ :
    alternating_group (fin 5)),
  have h5 : g1 * g2 * g1⁻¹ * g2⁻¹ = ⟨fin_rotate 5, fin_rotate_bit1_mem_alternating_group⟩,
  { rw subtype.ext_iff,
    simp only [fin.coe_mk, subgroup.coe_mul, subgroup.coe_inv, fin.coe_mk],
    dec_trivial },
  rw [eq_top_iff, ← normal_closure_fin_rotate_five],
  refine normal_closure_le_normal _,
  rw [set.singleton_subset_iff, set_like.mem_coe, ← h5],
  have h : g2 ∈ normal_closure {g2} :=
    set_like.mem_coe.1 (subset_normal_closure (set.mem_singleton _)),
  exact mul_mem (subgroup.normal_closure_normal.conj_mem _ h g1) (inv_mem h),
end

/-- Shows that any non-identity element of $A_5$ whose cycle decomposition consists only of swaps
  is conjugate to $(04)(13)$. This is used to show that the normal closure of such a permutation
  in $A_5$ is $A_5$. -/
lemma is_conj_swap_mul_swap_of_cycle_type_two {g : perm (fin 5)}
  (ha : g ∈ alternating_group (fin 5))
  (h1 : g ≠ 1)
  (h2 : ∀ n, n ∈ cycle_type (g : perm (fin 5)) → n = 2) :
  is_conj (swap 0 4 * swap 1 3) g :=
begin
  have h := g.support.card_le_univ,
  rw [← multiset.eq_replicate_card] at h2,
  rw [← sum_cycle_type, h2, multiset.sum_replicate, smul_eq_mul] at h,
  have h : g.cycle_type.card ≤ 3 := le_of_mul_le_mul_right (le_trans h dec_trivial) dec_trivial,
  rw [mem_alternating_group, sign_of_cycle_type, h2] at ha,
  norm_num at ha,
  rw [pow_add, pow_mul, int.units_pow_two,one_mul,
      units.ext_iff, units.coe_one, units.coe_pow, units.coe_neg_one,
      neg_one_pow_eq_one_iff_even _] at ha,
  swap, { dec_trivial },
  rw [is_conj_iff_cycle_type_eq, h2],
  interval_cases multiset.card g.cycle_type,
  { exact (h1 (card_cycle_type_eq_zero.1 h_1)).elim },
  { contrapose! ha,
    simp [h_1] },
  { have h04 : (0 : fin 5) ≠ 4 := dec_trivial,
    have h13 : (1 : fin 5) ≠ 3 := dec_trivial,
    rw [h_1, disjoint.cycle_type, (is_cycle_swap h04).cycle_type, (is_cycle_swap h13).cycle_type,
      card_support_swap h04, card_support_swap h13],
    { refl },
    { rw [disjoint_iff_disjoint_support, support_swap h04, support_swap h13],
      dec_trivial } },
  { contrapose! ha,
    simp [h_1] }
end

/-- Shows that $A_5$ is simple by taking an arbitrary non-identity element and showing by casework
  on its cycle type that its normal closure is all of $A_5$.   -/
instance is_simple_group_five : is_simple_group (alternating_group (fin 5)) :=
⟨exists_pair_ne _, λ H, begin
  introI Hn,
  refine or_not.imp (id) (λ Hb, _),
  rw [eq_bot_iff_forall] at Hb,
  push_neg at Hb,
  obtain ⟨⟨g, gA⟩, gH, g1⟩ : ∃ (x : ↥(alternating_group (fin 5))), x ∈ H ∧ x ≠ 1 := Hb,
  -- `g` is a non-identity alternating permutation in a normal subgroup `H` of $A_5$.
  rw [← set_like.mem_coe, ← set.singleton_subset_iff] at gH,
  refine eq_top_iff.2 (le_trans (ge_of_eq _) (normal_closure_le_normal gH)),
  -- It suffices to show that the normal closure of `g` in $A_5$ is $A_5$.
  by_cases h2 : ∀ n ∈ g.cycle_type, n = 2,
  { -- If the cycle decomposition of `g` consists entirely of swaps, then the cycle type is $(2,2)$.
    -- This means that it is conjugate to $(04)(13)$, whose normal closure is $A_5$.
    rw [ne.def, subtype.ext_iff] at g1,
    exact (is_conj_swap_mul_swap_of_cycle_type_two gA g1 h2).normal_closure_eq_top_of
      normal_closure_swap_mul_swap_five },
  push_neg at h2,
  obtain ⟨n, ng, n2⟩ : ∃ (n : ℕ), n ∈ g.cycle_type ∧ n ≠ 2 := h2,
  -- `n` is the size of a non-swap cycle in the decomposition of `g`.
  have n2' : 2 < n := lt_of_le_of_ne (two_le_of_mem_cycle_type ng) n2.symm,
  have n5 : n ≤ 5 := le_trans _ g.support.card_le_univ,
  -- We check that `2 < n ≤ 5`, so that `interval_cases` has a precise range to check.
  swap, { obtain ⟨m, hm⟩ := multiset.exists_cons_of_mem ng,
    rw [← sum_cycle_type, hm, multiset.sum_cons],
    exact le_add_right le_rfl },
  interval_cases n, -- This breaks into cases `n = 3`, `n = 4`, `n = 5`.
  { -- If `n = 3`, then `g` has a 3-cycle in its decomposition, so `g^2` is a 3-cycle.
    -- `g^2` is in the normal closure of `g`, so that normal closure must be $A_5$.
    rw [eq_top_iff, ← (is_three_cycle_sq_of_three_mem_cycle_type_five ng).alternating_normal_closure
      (by rw card_fin )],
    refine normal_closure_le_normal _,
    rw [set.singleton_subset_iff, set_like.mem_coe],
    have h := set_like.mem_coe.1 (subset_normal_closure (set.mem_singleton _)),
    exact mul_mem h h },
  { -- The case `n = 4` leads to contradiction, as no element of $A_5$ includes a 4-cycle.
    have con := mem_alternating_group.1 gA,
    contrapose! con,
    rw [sign_of_cycle_type,
      cycle_type_of_card_le_mem_cycle_type_add_two dec_trivial ng],
    dec_trivial },
  { -- If `n = 5`, then `g` is itself a 5-cycle, conjugate to `fin_rotate 5`.
    refine (is_conj_iff_cycle_type_eq.2 _).normal_closure_eq_top_of
      normal_closure_fin_rotate_five,
    rw [cycle_type_of_card_le_mem_cycle_type_add_two dec_trivial ng, cycle_type_fin_rotate] }
end⟩

end alternating_group

repo: mathlib


text:
import MyNat.Definition
namespace MyNat
/-!
# Tutorial world

## Level 1: the rfl tactic

Let's learn some tactics! Let's start with the `rfl` tactic. `rfl` stands for "reflexivity", which is
a fancy way of saying that it will prove any goal of the form `A = A`. It doesn't matter how
complicated `A` is, all that matters is that the left hand side is exactly equal to the right hand
side (a computer scientist would say "definitionally equal"). I really mean "press the same buttons
on your computer in the same order" equal. For example, `x * y + z = x * y + z` can be proved by `rfl`,
but `x + y = y + x` cannot.

Each level in this world involves proving a theorem or a lemma (a lemma is just a baby theorem). The
goal of the theorem will be a mathematical statement with a `⊢` just before it. We will use tactics
to manipulate and ultimately close (i.e. prove) these goals.

> Note that while lean4 does not define the keyword `lemma` it has been added to the `mathlib4`
library so it is coming from the `import Mathlib.Tactic.Basic` that is included in `MyNat.Definition`.

Let's see `rfl` in action! At the bottom of the text in this box, there's a lemma, which says that
if `x`, `y` and `z` are natural numbers then `xy + z = xy + z`. Locate this lemma (if you can't see
the lemma and these instructions at the same time, make this box wider by dragging the sides). Let's
supply the proof. Click on the word sorry and then delete it. When the system finishes being busy,
you'll be able to see your goal in the Visual Studio Code InfoView.

Remember that the goal is the thing with the unicode symbol `⊢` just before it. The goal in this
case is `x * y + z = x * y + z`, where `x`, `y` and `z` are some of your very own natural numbers.
That's a pretty easy goal to prove -- you can just prove it with the `rfl` tactic. Where it used to
say sorry, write `rfl`.

**Lemma**

For all natural numbers `x`, `y` and `z`, we have `xy + z = xy + z`.
-/

lemma example1 (x y z : MyNat) : x * y + z = x * y + z := by
  rfl
/-!
If all goes well Lean will print `Goals accomplished 🎉` in the InfoView.
You just did the first level of the tutorial!

For each level, the idea is to get Lean into this state: with the InfoView saying "`Goals accomplished 🎉`"
when the cursor is placed at the end of the line that completes the proof.

If you want to be reminded about the `rfl` tactic, you can hover the mouse over the `rfl` keyword and
a tooltip will appear with information about this tactic.  You can also press F12 to jump to the
definition of that tactic were there will be lots more handy information.
We have also included a [Tactics Section](../Tactics.lean.md) that lists all the tactics we use in this tutorial.

Now click on "next level" in the top right of your browser to go onto the second level of tutorial
world, where we'll learn about the rw tactic.

Now you are ready for [Level2.lean](./Level2.lean.md).
-/

author: leanprover


text:
/-
Copyright (c) 2020 Eric Weiser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Weiser

! This file was ported from Lean 3 source module algebra.star.free
! leanprover-community/mathlib commit cb3ceec8485239a61ed51d944cb9a95b68c6bafc
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Algebra.Star.Basic
import Mathbin.Algebra.FreeAlgebra

/-!
# A *-algebra structure on the free algebra.

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

Reversing words gives a *-structure on the free monoid or on the free algebra on a type.

## Implementation note
We have this in a separate file, rather than in `algebra.free_monoid` and `algebra.free_algebra`,
to avoid importing `algebra.star.basic` into the entire hierarchy.
-/

namespace FreeMonoid

variable {α : Type _}

instance : StarSemigroup (FreeMonoid α)
    where
  unit := List.reverse
  star_involutive := List.reverse_reverse
  star_mul := List.reverse_append

/- warning: free_monoid.star_of -> FreeMonoid.star_of is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} (x : α), Eq.{succ u1} (FreeMonoid.{u1} α) (Star.star.{u1} (FreeMonoid.{u1} α) (InvolutiveStar.toHasStar.{u1} (FreeMonoid.{u1} α) (StarSemigroup.toHasInvolutiveStar.{u1} (FreeMonoid.{u1} α) (Monoid.toSemigroup.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.cancelMonoid.{u1} α)))) (FreeMonoid.starSemigroup.{u1} α))) (FreeMonoid.of.{u1} α x)) (FreeMonoid.of.{u1} α x)
but is expected to have type
  forall {α : Type.{u1}} (x : α), Eq.{succ u1} (FreeMonoid.{u1} α) (Star.star.{u1} (FreeMonoid.{u1} α) (InvolutiveStar.toStar.{u1} (FreeMonoid.{u1} α) (StarSemigroup.toInvolutiveStar.{u1} (FreeMonoid.{u1} α) (Monoid.toSemigroup.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.instCancelMonoidFreeMonoid.{u1} α)))) (FreeMonoid.instStarSemigroupFreeMonoidToSemigroupToMonoidToRightCancelMonoidInstCancelMonoidFreeMonoid.{u1} α))) (FreeMonoid.of.{u1} α x)) (FreeMonoid.of.{u1} α x)
Case conversion may be inaccurate. Consider using '#align free_monoid.star_of FreeMonoid.star_ofₓ'. -/
@[simp]
theorem star_of (x : α) : star (of x) = of x :=
  rfl
#align free_monoid.star_of FreeMonoid.star_of

/- warning: free_monoid.star_one -> FreeMonoid.star_one is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}}, Eq.{succ u1} (FreeMonoid.{u1} α) (Star.star.{u1} (FreeMonoid.{u1} α) (InvolutiveStar.toHasStar.{u1} (FreeMonoid.{u1} α) (StarSemigroup.toHasInvolutiveStar.{u1} (FreeMonoid.{u1} α) (Monoid.toSemigroup.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.cancelMonoid.{u1} α)))) (FreeMonoid.starSemigroup.{u1} α))) (OfNat.ofNat.{u1} (FreeMonoid.{u1} α) 1 (OfNat.mk.{u1} (FreeMonoid.{u1} α) 1 (One.one.{u1} (FreeMonoid.{u1} α) (MulOneClass.toHasOne.{u1} (FreeMonoid.{u1} α) (Monoid.toMulOneClass.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.cancelMonoid.{u1} α))))))))) (OfNat.ofNat.{u1} (FreeMonoid.{u1} α) 1 (OfNat.mk.{u1} (FreeMonoid.{u1} α) 1 (One.one.{u1} (FreeMonoid.{u1} α) (MulOneClass.toHasOne.{u1} (FreeMonoid.{u1} α) (Monoid.toMulOneClass.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.cancelMonoid.{u1} α))))))))
but is expected to have type
  forall {α : Type.{u1}}, Eq.{succ u1} (FreeMonoid.{u1} α) (Star.star.{u1} (FreeMonoid.{u1} α) (InvolutiveStar.toStar.{u1} (FreeMonoid.{u1} α) (StarSemigroup.toInvolutiveStar.{u1} (FreeMonoid.{u1} α) (Monoid.toSemigroup.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toMonoid.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.instCancelMonoidFreeMonoid.{u1} α)))) (FreeMonoid.instStarSemigroupFreeMonoidToSemigroupToMonoidToRightCancelMonoidInstCancelMonoidFreeMonoid.{u1} α))) (OfNat.ofNat.{u1} (FreeMonoid.{u1} α) 1 (One.toOfNat1.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toOne.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.instCancelMonoidFreeMonoid.{u1} α)))))) (OfNat.ofNat.{u1} (FreeMonoid.{u1} α) 1 (One.toOfNat1.{u1} (FreeMonoid.{u1} α) (RightCancelMonoid.toOne.{u1} (FreeMonoid.{u1} α) (CancelMonoid.toRightCancelMonoid.{u1} (FreeMonoid.{u1} α) (FreeMonoid.instCancelMonoidFreeMonoid.{u1} α)))))
Case conversion may be inaccurate. Consider using '#align free_monoid.star_one FreeMonoid.star_oneₓ'. -/
/-- Note that `star_one` is already a global simp lemma, but this one works with dsimp too -/
@[simp]
theorem star_one : star (1 : FreeMonoid α) = 1 :=
  rfl
#align free_monoid.star_one FreeMonoid.star_one

end FreeMonoid

namespace FreeAlgebra

variable {R : Type _} [CommSemiring R] {X : Type _}

/-- The star ring formed by reversing the elements of products -/
instance : StarRing (FreeAlgebra R X)
    where
  unit := MulOpposite.unop ∘ lift R (MulOpposite.op ∘ ι R)
  star_involutive x := by
    unfold Star.star
    simp only [Function.comp_apply]
    refine' FreeAlgebra.induction R X _ _ _ _ x
    · intros
      simp only [AlgHom.commutes, MulOpposite.algebraMap_apply, MulOpposite.unop_op]
    · intros
      simp only [lift_ι_apply, MulOpposite.unop_op]
    · intros
      simp only [*, map_mul, MulOpposite.unop_mul]
    · intros
      simp only [*, map_add, MulOpposite.unop_add]
  star_mul a b := by simp only [Function.comp_apply, map_mul, MulOpposite.unop_mul]
  star_add a b := by simp only [Function.comp_apply, map_add, MulOpposite.unop_add]

/- warning: free_algebra.star_ι -> FreeAlgebra.star_ι is a dubious translation:
lean 3 declaration is
  forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}} (x : X), Eq.{succ (max u1 u2)} (FreeAlgebra.{u1, u2} R _inst_1 X) (Star.star.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (InvolutiveStar.toHasStar.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (StarAddMonoid.toHasInvolutiveStar.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (AddCommMonoid.toAddMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))))) (StarRing.toStarAddMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X)) (FreeAlgebra.starRing.{u1, u2} R _inst_1 X)))) (FreeAlgebra.ι.{u1, u2} R _inst_1 X x)) (FreeAlgebra.ι.{u1, u2} R _inst_1 X x)
but is expected to have type
  forall {R : Type.{u2}} [_inst_1 : CommSemiring.{u2} R] {X : Type.{u1}} (x : X), Eq.{max (succ u2) (succ u1)} (FreeAlgebra.{u2, u1} R _inst_1 X) (Star.star.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (InvolutiveStar.toStar.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (StarAddMonoid.toInvolutiveStar.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (AddMonoidWithOne.toAddMonoid.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (AddCommMonoidWithOne.toAddMonoidWithOne.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toAddCommMonoidWithOne.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))))) (StarRing.toStarAddMonoid.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) (FreeAlgebra.instStarRingFreeAlgebraToNonUnitalSemiringInstSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))) (FreeAlgebra.ι.{u2, u1} R _inst_1 X x)) (FreeAlgebra.ι.{u2, u1} R _inst_1 X x)
Case conversion may be inaccurate. Consider using '#align free_algebra.star_ι FreeAlgebra.star_ιₓ'. -/
@[simp]
theorem star_ι (x : X) : star (ι R x) = ι R x := by simp [star, Star.star]
#align free_algebra.star_ι FreeAlgebra.star_ι

/- warning: free_algebra.star_algebra_map -> FreeAlgebra.star_algebraMap is a dubious translation:
lean 3 declaration is
  forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}} (r : R), Eq.{succ (max u1 u2)} (FreeAlgebra.{u1, u2} R _inst_1 X) (Star.star.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (InvolutiveStar.toHasStar.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (StarAddMonoid.toHasInvolutiveStar.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (AddCommMonoid.toAddMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (NonUnitalNonAssocSemiring.toAddCommMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (NonUnitalSemiring.toNonUnitalNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))))) (StarRing.toStarAddMonoid.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonUnitalSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X)) (FreeAlgebra.starRing.{u1, u2} R _inst_1 X)))) (coeFn.{max (succ u1) (succ (max u1 u2)), max (succ u1) (succ (max u1 u2))} (RingHom.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) (fun (_x : RingHom.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) => R -> (FreeAlgebra.{u1, u2} R _inst_1 X)) (RingHom.hasCoeToFun.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) (algebraMap.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) (FreeAlgebra.algebra.{u1, u2} R _inst_1 X)) r)) (coeFn.{max (succ u1) (succ (max u1 u2)), max (succ u1) (succ (max u1 u2))} (RingHom.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) (fun (_x : RingHom.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) => R -> (FreeAlgebra.{u1, u2} R _inst_1 X)) (RingHom.hasCoeToFun.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (Semiring.toNonAssocSemiring.{u1} R (CommSemiring.toSemiring.{u1} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X))) (algebraMap.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) (FreeAlgebra.algebra.{u1, u2} R _inst_1 X)) r)
but is expected to have type
  forall {R : Type.{u2}} [_inst_1 : CommSemiring.{u2} R] {X : Type.{u1}} (r : R), Eq.{max (succ u2) (succ u1)} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (Star.star.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (InvolutiveStar.toStar.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (StarAddMonoid.toInvolutiveStar.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (AddMonoidWithOne.toAddMonoid.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (AddCommMonoidWithOne.toAddMonoidWithOne.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (NonAssocSemiring.toAddCommMonoidWithOne.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (Semiring.toNonAssocSemiring.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))))) (StarRing.toStarAddMonoid.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (Semiring.toNonUnitalSemiring.{max u2 u1} ((fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) r) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) (FreeAlgebra.instStarRingFreeAlgebraToNonUnitalSemiringInstSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))) (FunLike.coe.{max (succ u2) (succ u1), succ u2, max (succ u2) (succ u1)} (RingHom.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) _x) (MulHomClass.toFunLike.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) (RingHom.instRingHomClassRingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u1 u2} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))))) (algebraMap.{u2, max u1 u2} R (FreeAlgebra.{u2, u1} R _inst_1 X) _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) r)) (FunLike.coe.{max (succ u2) (succ (max u2 u1)), succ u2, succ (max u2 u1)} (RingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (fun (_x : R) => (fun (x._@.Mathlib.Algebra.Hom.Group._hyg.2391 : R) => FreeAlgebra.{u2, u1} R _inst_1 X) _x) (MulHomClass.toFunLike.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (NonUnitalNonAssocSemiring.toMul.{u2} R (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)))) (NonUnitalNonAssocSemiring.toMul.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))) (NonUnitalRingHomClass.toMulHomClass.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{u2} R (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1))) (NonAssocSemiring.toNonUnitalNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) (RingHomClass.toNonUnitalRingHomClass.{max u2 u1, u2, max u2 u1} (RingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X))) R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) (RingHom.instRingHomClassRingHom.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) (Semiring.toNonAssocSemiring.{u2} R (CommSemiring.toSemiring.{u2} R _inst_1)) (Semiring.toNonAssocSemiring.{max u2 u1} (FreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X)))))) (algebraMap.{u2, max u2 u1} R (FreeAlgebra.{u2, u1} R _inst_1 X) _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u2, u1} R _inst_1 X) (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u2, u1} R _inst_1 X)) r)
Case conversion may be inaccurate. Consider using '#align free_algebra.star_algebra_map FreeAlgebra.star_algebraMapₓ'. -/
@[simp]
theorem star_algebraMap (r : R) : star (algebraMap R (FreeAlgebra R X) r) = algebraMap R _ r := by
  simp [star, Star.star]
#align free_algebra.star_algebra_map FreeAlgebra.star_algebraMap

/- warning: free_algebra.star_hom -> FreeAlgebra.starHom is a dubious translation:
lean 3 declaration is
  forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}}, AlgEquiv.{u1, max u1 u2, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) (MulOpposite.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X)) _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) (MulOpposite.semiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.semiring.{u1, u2} R _inst_1 X)) (FreeAlgebra.algebra.{u1, u2} R _inst_1 X) (MulOpposite.algebra.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) _inst_1 (FreeAlgebra.semiring.{u1, u2} R _inst_1 X) (FreeAlgebra.algebra.{u1, u2} R _inst_1 X))
but is expected to have type
  forall {R : Type.{u1}} [_inst_1 : CommSemiring.{u1} R] {X : Type.{u2}}, AlgEquiv.{u1, max u2 u1, max u2 u1} R (FreeAlgebra.{u1, u2} R _inst_1 X) (MulOpposite.{max u2 u1} (FreeAlgebra.{u1, u2} R _inst_1 X)) _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u1, u2} R _inst_1 X) (MulOpposite.semiring.{max u1 u2} (FreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.instSemiringFreeAlgebra.{u1, u2} R _inst_1 X)) (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u1, u2} R _inst_1 X) (MulOpposite.instAlgebraMulOppositeSemiring.{u1, max u1 u2} R (FreeAlgebra.{u1, u2} R _inst_1 X) _inst_1 (FreeAlgebra.instSemiringFreeAlgebra.{u1, u2} R _inst_1 X) (FreeAlgebra.instAlgebraFreeAlgebraInstSemiringFreeAlgebra.{u1, u2} R _inst_1 X))
Case conversion may be inaccurate. Consider using '#align free_algebra.star_hom FreeAlgebra.starHomₓ'. -/
/-- `star` as an `alg_equiv` -/
def starHom : FreeAlgebra R X ≃ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ :=
  { starRingEquiv with commutes' := fun r => by simp [star_algebra_map] }
#align free_algebra.star_hom FreeAlgebra.starHom

end FreeAlgebra


text:
/-
This is the second homework assignment for UVa CS2101, Spring 2019.

If you are in Professor Sullivan's class, you are to complete problems 1 - 8.
If you are in Prof. Hocking's class, you are to complete problems 9 - 13.

The first eight problems require that you carefully read the updated class
notes on relations vs. functions and on properties of functions: from the
start of 2.4 through 2.4.4. For all of the remaining problems, you must
have read the rest of the chapter, on higher-order functions.

The collaboration policy for this assignment has two parts. First, you must
complete this work on your own. Second, please do not discuss your results
with anyone in the other professor's class, even after the deadline for the
homework has passed, as your assignment this week will be part of their
assignment next week.

To complete this homework, first make a copy of this file in the "work"
directory of your class repository. Do not edit this file directly in the
hw directory. Make a copy first. Then fill in answers as required, save
your changes, and submit your work by uploading the completed file on Collab.

Make a copy of this file in your work directory; complete the work using
that copy; then upload the resulting file, after saving it, through Collab
before the due date.
-/

/-
1. Is the function, G, as defined in the reading, total? Explain.

Answer here:
Yes, G is total because its domain is its entire domain of definition. {1,2,3}, its domain, is the same as {1,2,3}, its domain of definition.
-/

/-
2. Give an example of a value in the domain of definition the function, F,
as defined in the reading, that proves that F is strictly partial, i.e.,
for which F is not defined.

Answer here:
4 is a value in the domain of definition that isn't defined in the domain of F, meaning there is at least one value in its
domain of definition where there is no corresponding value in the codomain, proving F is strictly partial.
-/

/-
3. Give an example of a value in the codomain of F that proves that F is
not surjective.

Answer here:
11 is a value in the codomain of F that proves that F is not surjective because its not in the range of F.
-/

/-
4. Is our example function, G, strictly partial? Explain.

Answer here:
G is not strictly partial because its defined domain is its entire domain of definition, meaning every value in the domain
of definition has a corresponding image y in the codomain.
-/

/-
5. Identify a value in the codomain of F that is not the image of any
value value in its domain of definition.

Answer here:
40 is a value in the codomain of F that is not the image of any value in its domain of definition.
-/

/-
6. Translate our logical definition of injective into mathematically
precise English following the examples for other properties of functions
given in the reading.

Answer here:
A function is considered injective if each value in its domain has exactly one unique image, meaning no two domain values
can have the same value in its range.
-/

/-
7. Is the function, f(x) = log(x) over the real numbers, injective?
Is it surjective? Is it bijective? Explain each of your answers briefly.

Answer here:
log(x) is injective because for each value in its domain (all real numbers), there is a unique value in its range.
It's surjective because its range is its entire codomain (all real numbers). It's bijective because no two domain
values have the same range value.
-/

/-
8. Is the relation, 3x^2 + 4y^2 = 4, single-valued? Explain your answers.

Answer here:
No, the relation is not single-valued because the same x can be paired with at least two different y's (positive and
negative) and still satisfy the relation.
-/

/-
Complete each of the following partial definitions in Lean by replacing
the underscore characters with code to define functions of the specified
types using lambda notation. We only care that you define some function
of each required type, not what particular function you define.

In preparation, note that if you hover your mouse over an underscore,
Lean will tell you what type of term you is needed to fill that hole.
The type that Lean requires appears after the "turnstile" symbol, |-,
in the message Lean will give you. Even more interestingly, if you
fill in a hole with a term of the right type that itself has one or
more remaining holes, Lean will tell you what types of terms are needed
to fill in those holes! You can thus fill a hole in an incremental manner,
refining a partial solution at each step until all holes are filled,
guided by the types that Lean tells you are needed for any given hole.
We recommend that you try developing your answers in this "top-down
structured" style of programming. That said, we will grade you only on
your answers and not on how you developed them.
-/

-- 9.
def hw2_1: ℕ → ℕ :=
    λ(x: ℕ),
        _

-- 10.
def hw2_2: ℕ → ℕ → ℕ :=
    _

-- 11.
def hw2_3: (ℕ → ℕ) → (ℕ → ℕ) :=
    _

-- 12.
def hw2_4: (ℕ → ℕ) → ((ℕ → ℕ) → ℕ) :=
    _

-- 13.
def hw2_5: (ℕ → ℕ) → ((ℕ → ℕ) → (ℕ → ℕ)) :=
    _

author: justinqcai


text:
import data.nat.basic

open nat

/-- Statement of "what the islanders know". Given a day number `d`, and the actual number of blue eyed
islanders `b`, and a hypothesized number of blue eyed islanders `B`, it returns whether or not `B` is a possible
number of blue eyed islanders from the blue eyed islanders perspective. -/
def island_rules : ℕ → ℕ → ℕ → Prop
/- on day 0 there are two possibilities for the number of blue eyed islanders `b` and `b - 1`
  unless `b = 1`, in which case there is only one possibility, since it is also known that the actual number is greater than zero -/
| 0     b B := (B = b ∨ B = b - 1) ∧ 0 < B
/- On subsequent days, a hypothesized value `B` is possible if and only if it was possible the previous day and
  it is consistent with whether or not islanders left the previous day -/
| (d+1) b B := island_rules d b B ∧
  ((∀ C, island_rules d b C → C = b) ↔ ∀ C, island_rules d B C → C = B)

lemma island_rules_zero_of_island_rules : ∀ {d b B : ℕ}, island_rules d b B → (B = b ∨ B = b - 1) ∧ 0 < B
| 0     b B h := h
| (d+1) b B h := island_rules_zero_of_island_rules h.left

theorem blue_eyed_islander_mp : ∀ {d b}, 0 < b → b ≤ d + 1 → ∀ B, island_rules d b B → B = b
| 0 b hb0 hdb B hir := begin
    have : b = 1, from le_antisymm hdb (succ_le_of_lt hb0),
    unfold island_rules at hir,
    cases hir.left with h h,
    { exact h },
    { simp [this, *, lt_irrefl] at * }
  end
| (d+1) b hb hdbB B hir :=
  have (B = b ∨ B = b - 1) ∧ 0 < B, from island_rules_zero_of_island_rules hir,
  begin
    unfold island_rules at hir,
    cases this.left with h h,
    { exact h },
    { /- the case B = b - 1 -/
      have hb0 : 0 < b - 1, from h ▸ this.right,
      have hb1 : 1 ≤ b, from le_trans (succ_le_of_lt hb0) (nat.sub_le_self _ _),
      have hdbB' : b - 1 ≤ d + 1, from nat.sub_le_right_iff_le_add.2 hdbB,
      /- by our induction hypothesis, they would have left on day d if the actual number was b - 1 -/
      have ih : ∀ C : ℕ, island_rules d B C → C = B, from h.symm ▸ blue_eyed_islander_mp hb0 hdbB',
      /- From the definition of island_rules, this means they left yesterday -/
      rw ← hir.right at ih,
      /- Slightly strange proof, even though we know B = b - 1 and we're trying to prove
        B = b, we don't find a contradiction, we just prove B = b directly -/
      exact ih B hir.left }
  end

/-- This seems to come up over and over again, so I proved it seperately -/
theorem nat.sub_one_ne_self_of_pos {a : ℕ} (ha : 0 < a) : a - 1 ≠ a :=
ne_of_lt (nat.sub_lt_self ha dec_trivial)

/-- The other direction of the iff, stated in an easier to prove but equivalent way.
  If `d + 1` < b, then there are two possible values.  -/
lemma blue_eyed_islander_mpr : ∀ {d b}, 0 < b → d + 1 < b → ∀ B, island_rules d b B ↔ (B = b ∨ B = b - 1)
| 0     b hb0 hdb B := begin
  unfold island_rules,
  split,
  { exact λ h, h.left },
  { assume hbB,
    split,
    { exact hbB },
    { cases hbB with hbB hbB,
      { exact hbB.symm ▸ hb0 },
      { exact hbB.symm ▸ nat.sub_pos_of_lt hdb } } }
  end
| (succ d) b hb0 hdb B :=
begin
  split,
  { exact λ h, (island_rules_zero_of_island_rules h).left },
  { assume hbB,
    have hb10 : 0 < b - 1, from nat.sub_pos_of_lt (lt_trans dec_trivial hdb),
    have hdb1 : d + 1 < b - 1, from nat.lt_sub_right_of_add_lt hdb,
    /- Use our induction hypothesis twice. For both possible values of B, the islanders
      did not leave the previous day. This means we have no new information -/
    have ihb : ∀ B : ℕ, island_rules d b B ↔ B = b ∨ B = b - 1,
      from blue_eyed_islander_mpr hb0 (lt_trans (lt_succ_self _) hdb),
    have ihb1 : ∀ B : ℕ, island_rules d (b - 1) B ↔ B = b - 1 ∨ B = b - 1 - 1,
      from blue_eyed_islander_mpr hb10 hdb1,
    unfold island_rules,
    split,
    { rw ihb,
      exact hbB },
    /- the interesting part of the proof starts here, we have to prove that either value of B is
      possible -/
    { cases hbB with hbB hbB,
      { /- case B = b is easy -/
        rw hbB },
      { /- case B = b - 1 is harder -/
        /- By our induction hypotheses it was impossible to deduce the value of `b` yesterday in both
          the real world, and for our hypothesized value of `B`, which is `b - 1`. This means both sides
          of the iff statement are false -/
        simp only [ihb, ihb1, hbB],
        /- After applying the induction hypothesis, it is now obvious that both sides are false,
          and the proof is easy from now on -/
        apply iff_of_false,
        { assume h,
          have : b - 1 = b, from h (b - 1) (or.inr rfl),
          exact nat.sub_one_ne_self_of_pos hb0 this },
        { assume h,
          have : b - 1 - 1 = b - 1, from h (b - 1 - 1) (or.inr rfl),
          exact nat.sub_one_ne_self_of_pos hb10 this } } } }
end

lemma blue_eyed_islander {d b} (hb0 : 0 < b) : (∀ B, island_rules d b B → B = b) ↔ b ≤ d + 1 :=
begin
  split,
  { assume h,
    refine le_of_not_gt (λ hbd : d + 1 < b, _),
    have := blue_eyed_islander_mpr hb0 hbd,
    have : b - 1 = b, from h (b - 1) ((this (b - 1)).mpr (or.inr rfl)),
    exact nat.sub_one_ne_self_of_pos hb0 this },
  { exact blue_eyed_islander_mp hb0 }
end

lemma blue_eyed_islander_100 {d : ℕ} : (∀ B, island_rules d 100 B → B = 100) ↔ 100 ≤ d + 1 :=
blue_eyed_islander dec_trivial

repo: leanstuff