text:
/-
Copyright (c) 2020 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import Mathlib.PrePort
import Mathlib.Lean3Lib.init.default
import Mathlib.algebra.category.Mon.limits
import Mathlib.algebra.category.Group.preadditive
import Mathlib.category_theory.over
import Mathlib.category_theory.limits.concrete_category
import Mathlib.category_theory.limits.shapes.concrete_category
import Mathlib.group_theory.subgroup
import Mathlib.PostPort

universes u u_1

namespace Mathlib

/-!
# The category of (commutative) (additive) groups has all limits

Further, these limits are preserved by the forgetful functor --- that is,
the underlying types are just the limits in the category of types.

-/

namespace Group

protected instance Mathlib.AddGroup.add_group_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ AddGroup) (j : J) : add_group (category_theory.functor.obj (F ⋙ category_theory.forget AddGroup) j) :=
  id (AddGroup.add_group (category_theory.functor.obj F j))

/--
The flat sections of a functor into `Group` form a subgroup of all sections.
-/
def Mathlib.AddGroup.sections_add_subgroup {J : Type u} [category_theory.small_category J] (F : J ⥤ AddGroup) : add_subgroup ((j : J) → ↥(category_theory.functor.obj F j)) :=
  add_subgroup.mk (category_theory.functor.sections (F ⋙ category_theory.forget AddGroup)) sorry sorry sorry

protected instance limit_group {J : Type u} [category_theory.small_category J] (F : J ⥤ Group) : group (category_theory.limits.cone.X (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget Group))) :=
  id (subgroup.to_group (sections_subgroup F))

/--
We show that the forgetful functor `Group ⥤ Mon` creates limits.

All we need to do is notice that the limit point has a `group` instance available,
and then reuse the existing limit.
-/
protected instance category_theory.forget₂.category_theory.creates_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ Group) : category_theory.creates_limit F (category_theory.forget₂ Group Mon) := sorry

/--
A choice of limit cone for a functor into `Group`.
(Generally, you'll just want to use `limit F`.)
-/
def Mathlib.AddGroup.limit_cone {J : Type u} [category_theory.small_category J] (F : J ⥤ AddGroup) : category_theory.limits.cone F :=
  category_theory.lift_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ AddGroup AddMon))

/--
The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)
-/
def Mathlib.AddGroup.limit_cone_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ AddGroup) : category_theory.limits.is_limit (AddGroup.limit_cone F) :=
  category_theory.lifted_limit_is_limit
    (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ AddGroup AddMon))

/-- The category of groups has all limits. -/
protected instance has_limits : category_theory.limits.has_limits Group :=
  category_theory.limits.has_limits.mk
    fun (J : Type u_1) (𝒥 : category_theory.small_category J) =>
      category_theory.limits.has_limits_of_shape.mk
        fun (F : J ⥤ Group) => category_theory.has_limit_of_created F (category_theory.forget₂ Group Mon)

/--
The forgetful functor from groups to monoids preserves all limits.
(That is, the underlying monoid could have been computed instead as limits in the category
of monoids.)
-/
protected instance Mathlib.AddGroup.forget₂_AddMon_preserves_limits : category_theory.limits.preserves_limits (category_theory.forget₂ AddGroup AddMon) :=
  category_theory.limits.preserves_limits.mk
    fun (J : Type u_1) (𝒥 : category_theory.small_category J) =>
      category_theory.limits.preserves_limits_of_shape.mk
        fun (F : J ⥤ AddGroup) =>
          category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ AddGroup AddMon)

/--
The forgetful functor from groups to types preserves all limits. (That is, the underlying
types could have been computed instead as limits in the category of types.)
-/
protected instance forget_preserves_limits : category_theory.limits.preserves_limits (category_theory.forget Group) :=
  category_theory.limits.preserves_limits.mk
    fun (J : Type u_1) (𝒥 : category_theory.small_category J) =>
      category_theory.limits.preserves_limits_of_shape.mk
        fun (F : J ⥤ Group) =>
          category_theory.limits.comp_preserves_limit (category_theory.forget₂ Group Mon) (category_theory.forget Mon)

end Group

namespace CommGroup

protected instance Mathlib.AddCommGroup.add_comm_group_obj {J : Type u} [category_theory.small_category J] (F : J ⥤ AddCommGroup) (j : J) : add_comm_group (category_theory.functor.obj (F ⋙ category_theory.forget AddCommGroup) j) :=
  id (AddCommGroup.add_comm_group_instance (category_theory.functor.obj F j))

protected instance limit_comm_group {J : Type u} [category_theory.small_category J] (F : J ⥤ CommGroup) : comm_group
  (category_theory.limits.cone.X (category_theory.limits.types.limit_cone (F ⋙ category_theory.forget CommGroup))) :=
  subgroup.to_comm_group (Group.sections_subgroup (F ⋙ category_theory.forget₂ CommGroup Group))

/--
We show that the forgetful functor `CommGroup ⥤ Group` creates limits.

All we need to do is notice that the limit point has a `comm_group` instance available,
and then reuse the existing limit.
-/
protected instance Mathlib.AddCommGroup.category_theory.forget₂.category_theory.creates_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ AddCommGroup) : category_theory.creates_limit F (category_theory.forget₂ AddCommGroup AddGroup) := sorry

/--
A choice of limit cone for a functor into `CommGroup`.
(Generally, you'll just want to use `limit F`.)
-/
def Mathlib.AddCommGroup.limit_cone {J : Type u} [category_theory.small_category J] (F : J ⥤ AddCommGroup) : category_theory.limits.cone F :=
  category_theory.lift_limit (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ AddCommGroup AddGroup))

/--
The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)
-/
def limit_cone_is_limit {J : Type u} [category_theory.small_category J] (F : J ⥤ CommGroup) : category_theory.limits.is_limit (limit_cone F) :=
  category_theory.lifted_limit_is_limit
    (category_theory.limits.limit.is_limit (F ⋙ category_theory.forget₂ CommGroup Group))

/-- The category of commutative groups has all limits. -/
protected instance has_limits : category_theory.limits.has_limits CommGroup :=
  category_theory.limits.has_limits.mk
    fun (J : Type u_1) (𝒥 : category_theory.small_category J) =>
      category_theory.limits.has_limits_of_shape.mk
        fun (F : J ⥤ CommGroup) => category_theory.has_limit_of_created F (category_theory.forget₂ CommGroup Group)

/--
The forgetful functor from commutative groups to groups preserves all limits.
(That is, the underlying group could have been computed instead as limits in the category
of groups.)
-/
protected instance Mathlib.AddCommGroup.forget₂_AddGroup_preserves_limits : category_theory.limits.preserves_limits (category_theory.forget₂ AddCommGroup AddGroup) :=
  category_theory.limits.preserves_limits.mk
    fun (J : Type u_1) (𝒥 : category_theory.small_category J) =>
      category_theory.limits.preserves_limits_of_shape.mk
        fun (F : J ⥤ AddCommGroup) =>
          category_theory.preserves_limit_of_creates_limit_and_has_limit F (category_theory.forget₂ AddCommGroup AddGroup)

/--
An auxiliary declaration to speed up typechecking.
-/
def forget₂_CommMon_preserves_limits_aux {J : Type u} [category_theory.small_category J] (F : J ⥤ CommGroup) : category_theory.limits.is_limit
  (category_theory.functor.map_cone (category_theory.forget₂ CommGroup CommMon) (limit_cone F)) :=
  CommMon.limit_cone_is_limit (F ⋙ category_theory.forget₂ CommGroup CommMon)

/--
The forgetful functor from commutative groups to commutative monoids preserves all limits.
(That is, the underlying commutative monoids could have been computed instead as limits
in the category of commutative monoids.)
-/
protected instance forget₂_CommMon_preserves_limits : category_theory.limits.preserves_limits (category_theory.forget₂ CommGroup CommMon) :=
  category_theory.limits.preserves_limits.mk
    fun (J : Type u_1) (𝒥 : category_theory.small_category J) =>
      category_theory.limits.preserves_limits_of_shape.mk
        fun (F : J ⥤ CommGroup) =>
          category_theory.limits.preserves_limit_of_preserves_limit_cone (limit_cone_is_limit F)
            (forget₂_CommMon_preserves_limits_aux F)

/--
The forgetful functor from commutative groups to types preserves all limits. (That is, the
underlying types could have been computed instead as limits in the category of types.)
-/
protected instance forget_preserves_limits : category_theory.limits.preserves_limits (category_theory.forget CommGroup) :=
  category_theory.limits.preserves_limits.mk
    fun (J : Type u_1) (𝒥 : category_theory.small_category J) =>
      category_theory.limits.preserves_limits_of_shape.mk
        fun (F : J ⥤ CommGroup) =>
          category_theory.limits.comp_preserves_limit (category_theory.forget₂ CommGroup Group)
            (category_theory.forget Group)

end CommGroup

namespace AddCommGroup

/--
The categorical kernel of a morphism in `AddCommGroup`
agrees with the usual group-theoretical kernel.
-/
def kernel_iso_ker {G : AddCommGroup} {H : AddCommGroup} (f : G ⟶ H) : category_theory.limits.kernel f ≅ of ↥(add_monoid_hom.ker f) :=
  category_theory.iso.mk
    (add_monoid_hom.mk
      (fun (g : ↥(category_theory.limits.kernel f)) =>
        { val := coe_fn (category_theory.limits.kernel.ι f) g, property := sorry })
      sorry sorry)
    (category_theory.limits.kernel.lift f (add_subgroup.subtype (add_monoid_hom.ker f)) sorry)

@[simp] theorem kernel_iso_ker_hom_comp_subtype {G : AddCommGroup} {H : AddCommGroup} (f : G ⟶ H) : category_theory.iso.hom (kernel_iso_ker f) ≫ add_subgroup.subtype (add_monoid_hom.ker f) =
  category_theory.limits.kernel.ι f := sorry

@[simp] theorem kernel_iso_ker_inv_comp_ι {G : AddCommGroup} {H : AddCommGroup} (f : G ⟶ H) : category_theory.iso.inv (kernel_iso_ker f) ≫ category_theory.limits.kernel.ι f =
  add_subgroup.subtype (add_monoid_hom.ker f) := sorry

/--
The categorical kernel inclusion for `f : G ⟶ H`, as an object over `G`,
agrees with the `subtype` map.
-/
@[simp] theorem kernel_iso_ker_over_inv_left {G : AddCommGroup} {H : AddCommGroup} (f : G ⟶ H) : category_theory.comma_morphism.left (category_theory.iso.inv (kernel_iso_ker_over f)) =
  category_theory.iso.inv (kernel_iso_ker f) :=
  Eq.refl (category_theory.iso.inv (kernel_iso_ker f))

author: AurelienSaue


text:
import .main

meta def ex01 : expr := `(∀ {x y z w v : int}, 100 = x → x = y → y = z → z = w → w = v → v = 100)
meta def ex02 : expr := `(∀ x : int, (x = 5 ∨ x = 7) → 2 < x)
meta def ex03 : expr := `(∀ x : int, x ≤ -x → x ≤ 0)
meta def ex04 : expr := `(∀ x y : int, (x ≤ 5 ∧ y ≤ 3) → x + y ≤ 8 )
meta def ex05 : expr := `(∀ (x y z : int), x < y → y < z → x < z )
meta def ex06 : expr := `(∀ (x y z : int), x - y ≤ x - z → z ≤ y)
meta def ex07 : expr := `(∀ x : int, (x = -5 ∨ x = 7) → ¬x = 0 )
meta def ex08 : expr := `(∀ x : int, 31 * x > 0 → x > 0 )
meta def ex09 : expr := `(∀ x y : int, (-x - y < x - y) → (x - y < x + y) → (x > 0 ∧ y > 0))
meta def ex10 : expr := `(∀ (x : int), (x ≥ -1 ∧ x ≤ 1) → (x = -1 ∨ x = 0 ∨ x = 1))
meta def ex11 : expr := `(∀ (x : int), 5 * x = 5 → x = 1 )
meta def ex12 : expr := `(∀ x y z w v : int, x = y → y = z → x = z )
meta def ex13 : expr := `(∀ x : int, x < 349 ∨ x > 123 )
meta def ex14 : expr := `(∀ x y : int, x ≤ 3 * y → 3 * x ≤ 9 * y )
meta def ex15 : expr := `(∀ x : int, (x < 43 ∧ x > 513) → ¬x = x )
meta def ex16 : expr := `(∀ (x y z w : int), x ≤ y → y ≤ z → z ≤ w → x ≤ w)

meta def ex17 : expr := `(forall (x : nat),  31 * x > 0 → x > 0)
meta def ex18 : expr := `(forall (x y : nat),  (x ≤ 5 ∧ y ≤ 3) → x + y ≤ 8)
meta def ex19 : expr := `(forall (x y z y : nat),  ¬(2 * x + 1 = 2 * y))
meta def ex20 : expr := `(forall (x y : nat),  x > 0 → x + y > 0)
meta def ex21 : expr := `(forall (x : nat),  x < 349 ∨ x > 123)
meta def ex22 : expr := `(forall (x y : nat),  x ≤ 3 * y → 3 * x ≤ 9 * y)
meta def ex23 : expr := `(forall (x y z : nat), (x ≤ y) → (z > y) → (x - z = 0))
meta def ex24 : expr := `(forall (x y z : nat), x - 5 > 122 → y ≤ 127 → y < x)

open tactic

meta def batch_test (slv : tactic unit) : nat → list expr → tactic unit
| _ [] := tactic.triv
| idx (exp::exps) :=
  ((do gs ← tactic.get_goals,
       g ← tactic.mk_meta_var exp,
       tactic.set_goals (g::gs), slv)
    <|> (trace (("Failed ex " : format) ++ format.of_nat idx) >> skip))
    >> batch_test (idx+1) exps

meta def int.tests : list expr :=
[ex01,ex02,ex03,ex04,ex05,ex06,ex07,ex08,ex09,ex10,
 ex11,ex12,ex13,ex14,ex15,ex16]

meta def nat.tests : list expr :=
[ex17,ex18,ex19,ex20,ex21,ex22,ex23,ex24]

meta def tests : list expr := int.tests ++ nat.tests

set_option profiler true

example : true :=
by do batch_test omega 0 tests

author: skbaek

repo: omega

save_path: github-repos/lean/skbaek-omega


text:
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Kenny Lau

Fixed point construction on complete lattices.
-/
import order.complete_lattice

universes u v w
variables {α : Type u} {β : Type v} {γ : Type w}

namespace lattice

def fixed_points (f : α → α) : set α := { x | f x = x }

section fixedpoint
variables [complete_lattice α] {f : α → α}

/-- Least fixed point of a monotone function -/
def lfp (f : α → α) : α := Inf {a | f a ≤ a}
/-- Greatest fixed point of a monotone function -/
def gfp (f : α → α) : α := Sup {a | a ≤ f a}

theorem lfp_le {a : α} (h : f a ≤ a) : lfp f ≤ a :=
Inf_le h

theorem le_lfp {a : α} (h : ∀b, f b ≤ b → a ≤ b) : a ≤ lfp f :=
le_Inf h

theorem lfp_eq (m : monotone f) : lfp f = f (lfp f) :=
have f (lfp f) ≤ lfp f,
  from le_lfp $ assume b, assume h : f b ≤ b, le_trans (m (lfp_le h)) h,
le_antisymm (lfp_le (m this)) this

theorem lfp_induct {p : α → Prop} (m : monotone f)
  (step : ∀a, p a → a ≤ lfp f → p (f a)) (sup : ∀s, (∀a∈s, p a) → p (Sup s)) :
p (lfp f) :=
let s := {a | a ≤ lfp f ∧ p a} in
have p_s : p (Sup s),
  from sup s (assume a ⟨_, h⟩, h),
have Sup s ≤ lfp f,
  from le_lfp $ assume a, assume h : f a ≤ a, Sup_le $ assume b ⟨b_le, _⟩, le_trans b_le (lfp_le h),
have Sup s = lfp f,
  from le_antisymm this $ lfp_le $ le_Sup
    ⟨le_trans (m this) $ ge_of_eq $ lfp_eq m, step _ p_s this⟩,
this ▸ p_s

theorem monotone_lfp : monotone (@lfp α _) :=
assume f g, assume : f ≤ g, le_lfp $ assume a, assume : g a ≤ a, lfp_le $ le_trans (‹f ≤ g› a) this

theorem le_gfp {a : α} (h : a ≤ f a) : a ≤ gfp f :=
le_Sup h

theorem gfp_le {a : α} (h : ∀b, b ≤ f b → b ≤ a) : gfp f ≤ a :=
Sup_le h

theorem gfp_eq (m : monotone f) : gfp f = f (gfp f) :=
have gfp f ≤ f (gfp f),
  from gfp_le $ assume b, assume h : b ≤ f b, le_trans h (m (le_gfp h)),
le_antisymm this (le_gfp (m this))

theorem gfp_induct {p : α → Prop} (m : monotone f)
  (step : ∀a, p a → gfp f ≤ a → p (f a)) (inf : ∀s, (∀a∈s, p a) → p (Inf s)) :
p (gfp f) :=
let s := {a | gfp f ≤ a ∧ p a} in
have p_s : p (Inf s),
  from inf s (assume a ⟨_, h⟩, h),
have gfp f ≤ Inf s,
  from gfp_le $ assume a, assume h : a ≤ f a, le_Inf $ assume b ⟨le_b, _⟩, le_trans (le_gfp h) le_b,
have Inf s = gfp f,
  from le_antisymm (le_gfp $ Inf_le
    ⟨le_trans (le_of_eq $ gfp_eq m) (m this), step _ p_s this⟩) this,
this ▸ p_s

theorem monotone_gfp : monotone (@gfp α _) :=
assume f g, assume : f ≤ g, gfp_le $ assume a, assume : a ≤ f a, le_gfp $ le_trans this (‹f ≤ g› a)

end fixedpoint

section fixedpoint_eqn
variables [complete_lattice α] [complete_lattice β] {f : β → α} {g : α → β}

-- Rolling rule
theorem lfp_comp (m_f : monotone f) (m_g : monotone g) : lfp (f ∘ g) = f (lfp (g ∘ f)) :=
le_antisymm
  (lfp_le $ m_f $ ge_of_eq $ lfp_eq $ monotone_comp m_f m_g)
  (le_lfp $ assume a fg_le,
    le_trans (m_f $ lfp_le $ show (g ∘ f) (g a) ≤ g a, from m_g fg_le) fg_le)

theorem gfp_comp (m_f : monotone f) (m_g : monotone g) : gfp (f ∘ g) = f (gfp (g ∘ f)) :=
le_antisymm
  (gfp_le $ assume a fg_le,
    le_trans fg_le $ m_f $ le_gfp $ show g a ≤ (g ∘ f) (g a), from m_g fg_le)
  (le_gfp $ m_f $ le_of_eq $ gfp_eq $ monotone_comp m_f m_g)

-- Diagonal rule
theorem lfp_lfp {h : α → α → α} (m : ∀⦃a b c d⦄, a ≤ b → c ≤ d → h a c ≤ h b d) :
  lfp (lfp ∘ h) = lfp (λx, h x x) :=
let f := lfp (lfp ∘ h) in
have f_eq : f = lfp (h f),
  from lfp_eq $ monotone_comp (assume a b h x, m h (le_refl _)) monotone_lfp,
le_antisymm
  (lfp_le $ lfp_le $ ge_of_eq $ lfp_eq $ assume a b h, m h h)
  (lfp_le $ ge_of_eq $
    calc f = lfp (h f)       : f_eq
       ... = h f (lfp (h f)) : lfp_eq $ assume a b h, m (le_refl _) h
       ... = h f f           : congr_arg (h f) f_eq.symm)

theorem gfp_gfp {h : α → α → α} (m : ∀⦃a b c d⦄, a ≤ b → c ≤ d → h a c ≤ h b d) :
  gfp (gfp ∘ h) = gfp (λx, h x x) :=
let f := gfp (gfp ∘ h) in
have f_eq : f = gfp (h f),
  from gfp_eq $ monotone_comp (assume a b h x, m h (le_refl _)) monotone_gfp,
le_antisymm
  (le_gfp $ le_of_eq $
    calc f = gfp (h f)       : f_eq
       ... = h f (gfp (h f)) : gfp_eq $ assume a b h, m (le_refl _) h
       ... = h f f           : congr_arg (h f) f_eq.symm)
  (le_gfp $ le_gfp $ le_of_eq $ gfp_eq $ assume a b h, m h h)

end fixedpoint_eqn

/- The complete lattice of fixed points of a function f -/
namespace fixed_points
variables [complete_lattice α] (f : α → α) (hf : monotone f)

def prev (x : α) : α := gfp (λ z, x ⊓ f z)
def next (x : α) : α := lfp (λ z, x ⊔ f z)

variable {f}

theorem prev_le {x : α} : prev f x ≤ x := gfp_le $ λ z hz, le_trans hz inf_le_left

lemma prev_eq (hf : monotone f) {a : α} (h : f a ≤ a) : prev f a = f (prev f a) :=
calc prev f a = a ⊓ f (prev f a) :
    gfp_eq $ show monotone (λz, a ⊓ f z), from assume x y h, inf_le_inf (le_refl _) (hf h)
  ... = f (prev f a) :
    by rw [inf_of_le_right]; exact le_trans (hf prev_le) h

def prev_fixed (hf : monotone f) (a : α) (h : f a ≤ a) : fixed_points f :=
⟨prev f a, (prev_eq hf h).symm⟩

theorem next_le {x : α} : x ≤ next f x := le_lfp $ λ z hz, le_trans le_sup_left hz

lemma next_eq (hf : monotone f) {a : α} (h : a ≤ f a) : next f a = f (next f a) :=
calc next f a = a ⊔ f (next f a):
    lfp_eq $ show monotone (λz, a ⊔ f z), from assume x y h, sup_le_sup (le_refl _) (hf h)
 ... = f (next f a):
    by rw [sup_of_le_right]; exact le_trans h (hf next_le)

def next_fixed (hf : monotone f) (a : α) (h : a ≤ f a) : fixed_points f :=
⟨next f a, (next_eq hf h).symm⟩

variable f

theorem sup_le_f_of_fixed_points (x y : fixed_points f) : x.1 ⊔ y.1 ≤ f (x.1 ⊔ y.1) :=
sup_le
  (x.2 ▸ (hf $ show x.1 ≤ f x.1 ⊔ y.1, from x.2.symm ▸ le_sup_left))
  (y.2 ▸ (hf $ show y.1 ≤ x.1 ⊔ f y.1, from y.2.symm ▸ le_sup_right))

theorem f_le_inf_of_fixed_points (x y : fixed_points f) : f (x.1 ⊓ y.1) ≤ x.1 ⊓ y.1 :=
le_inf
  (x.2 ▸ (hf $ show f (x.1) ⊓ y.1 ≤ x.1, from x.2.symm ▸ inf_le_left))
  (y.2 ▸ (hf $ show x.1 ⊓ f (y.1) ≤ y.1, from y.2.symm ▸ inf_le_right))

theorem Sup_le_f_of_fixed_points (A : set α) (HA : A ⊆ fixed_points f) : Sup A ≤ f (Sup A) :=
Sup_le $ λ x hxA, (HA hxA) ▸ (hf $ le_Sup hxA)

theorem f_le_Inf_of_fixed_points (A : set α) (HA : A ⊆ fixed_points f) : f (Inf A) ≤ Inf A :=
le_Inf $ λ x hxA, (HA hxA) ▸ (hf $ Inf_le hxA)

instance : complete_lattice (fixed_points f) :=
{ le           := λx y, x.1 ≤ y.1,
  le_refl      := λ x, le_refl x,
  le_trans     := λ x y z, le_trans,
  le_antisymm  := λ x y hx hy, subtype.eq $ le_antisymm hx hy,

  sup          := λ x y, next_fixed hf (x.1 ⊔ y.1) (sup_le_f_of_fixed_points f hf x y),
  le_sup_left  := λ x y, show x.1 ≤ _, from le_trans le_sup_left next_le,
  le_sup_right := λ x y, show y.1 ≤ _, from le_trans le_sup_right next_le,
  sup_le       := λ x y z hxz hyz, lfp_le $ sup_le (sup_le hxz hyz) (z.2.symm ▸ le_refl z.1),

  inf          := λ x y, prev_fixed hf (x.1 ⊓ y.1) (f_le_inf_of_fixed_points f hf x y),
  inf_le_left  := λ x y, show _ ≤ x.1, from le_trans prev_le inf_le_left,
  inf_le_right := λ x y, show _ ≤ y.1, from le_trans prev_le inf_le_right,
  le_inf       := λ x y z hxy hxz, le_gfp $ le_inf (le_inf hxy hxz) (x.2.symm ▸ le_refl x),

  top          := prev_fixed hf ⊤ le_top,
  le_top       := λ ⟨x, H⟩, le_gfp $ le_inf le_top (H.symm ▸ le_refl x),

  bot          := next_fixed hf ⊥ bot_le,
  bot_le       := λ ⟨x, H⟩, lfp_le $ sup_le bot_le (H.symm ▸ le_refl x),

  Sup          := λ A, next_fixed hf (Sup $ subtype.val '' A)
    (Sup_le_f_of_fixed_points f hf (subtype.val '' A) (λ z ⟨x, hx⟩, hx.2 ▸ x.2)),
  le_Sup       := λ A x hxA, show x.1 ≤ _, from le_trans
    (le_Sup $ show x.1 ∈ subtype.val '' A, from ⟨x, hxA, rfl⟩)
    next_le,
  Sup_le       := λ A x Hx, lfp_le $ sup_le (Sup_le $ λ z ⟨y, hyA, hyz⟩, hyz ▸ Hx y hyA) (x.2.symm ▸ le_refl x),

  Inf          := λ A, prev_fixed hf (Inf $ subtype.val '' A)
    (f_le_Inf_of_fixed_points f hf (subtype.val '' A) (λ z ⟨x, hx⟩, hx.2 ▸ x.2)),
  le_Inf       := λ A x Hx, le_gfp $ le_inf (le_Inf $ λ z ⟨y, hyA, hyz⟩, hyz ▸ Hx y hyA) (x.2.symm ▸ le_refl x.1),
  Inf_le       := λ A x hxA, show _ ≤ x.1, from le_trans
    prev_le
    (Inf_le $ show x.1 ∈ subtype.val '' A, from ⟨x, hxA, rfl⟩) }

end fixed_points

end lattice

author: khoek

repo: mathlib-tidy

save_path: github-repos/lean/khoek-mathlib-tidy


text:
/-
Copyright (c) 2021 Vladimir Goryachev. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies, Vladimir Goryachev, Kyle Miller, Scott Morrison, Eric Rodriguez
-/
import data.nat.count
import order.order_iso_nat

/-!
# The `n`th Number Satisfying a Predicate

This file defines a function for "what is the `n`th number that satisifies a given predicate `p`",
and provides lemmas that deal with this function and its connection to `nat.count`.

## Main definitions

* `nth p n`: The `n`-th natural `k` (zero-indexed) such that `p k`. If there is no
  such natural (that is, `p` is true for at most `n` naturals), then `nth p n = 0`.

## Main results

* `nat.nth_set_card`: For a fintely-often true `p`, gives the cardinality of the set of numbers
  satisfying `p` above particular values of `nth p`
* `nat.count_nth_gc`: Establishes a Galois connection between `nth p` and `count p`.
* `nat.nth_eq_order_iso_of_nat`: For an infinitely-ofter true predicate, `nth` agrees with the
  order-isomorphism of the subtype to the natural numbers.

There has been some discussion on the subject of whether both of `nth` and
`nat.subtype.order_iso_of_nat` should exist. See discussion
[here](https://github.com/leanprover-community/mathlib/pull/9457#pullrequestreview-767221180).
Future work should address how lemmas that use these should be written.

-/

open finset

namespace nat
variable (p : ℕ → Prop)

/-- Find the `n`-th natural number satisfying `p` (indexed from `0`, so `nth p 0` is the first
natural number satisfying `p`), or `0` if there is no such number. See also
`subtype.order_iso_of_nat` for the order isomorphism with ℕ when `p` is infinitely often true. -/
noncomputable def nth : ℕ → ℕ
| n := Inf { i : ℕ | p i ∧ ∀ k < n, nth k < i }

lemma nth_zero : nth p 0 = Inf { i : ℕ | p i } := by { rw nth, simp }

@[simp] lemma nth_zero_of_zero (h : p 0) : nth p 0 = 0 :=
by simp [nth_zero, h]

lemma nth_set_card_aux {n : ℕ} (hp : (set_of p).finite)
  (hp' : {i : ℕ | p i ∧ ∀ t < n, nth p t < i}.finite) (hle : n ≤ hp.to_finset.card) :
  hp'.to_finset.card = hp.to_finset.card - n :=
begin
  unfreezingI { induction n with k hk },
  { congr,
    simp only [is_empty.forall_iff, nat.not_lt_zero, forall_const, and_true] },
  have hp'': {i : ℕ | p i ∧ ∀ t, t < k → nth p t < i}.finite,
  { refine hp.subset (λ x hx, _),
    rw set.mem_set_of_eq at hx,
    exact hx.left },
  have hle' := nat.sub_pos_of_lt hle,
  specialize hk hp'' (k.le_succ.trans hle),
  rw [nat.sub_succ', ←hk],
  convert_to (finset.erase hp''.to_finset (nth p k)).card = _,
  { congr,
    ext a,
    simp only [set.finite.mem_to_finset, ne.def, set.mem_set_of_eq, finset.mem_erase],
    refine ⟨λ ⟨hp, hlt⟩,
              ⟨(hlt _ (lt_add_one k)).ne', ⟨hp, λ n hn, hlt n (hn.trans_le k.le_succ)⟩⟩, _⟩,
    rintro ⟨hak : _ ≠ _, hp, hlt⟩,
    refine ⟨hp, λ n hn, _⟩,
    rw lt_succ_iff at hn,
    obtain hnk | rfl := hn.lt_or_eq,
    { exact hlt _ hnk },
    { refine lt_of_le_of_ne _ (ne.symm hak),
      rw nth,
      apply nat.Inf_le,
      simpa [hp] using hlt } },
  apply finset.card_erase_of_mem,
  rw [nth, set.finite.mem_to_finset],
  apply Inf_mem,
  rwa [←hp''.to_finset_nonempty, ←finset.card_pos, hk],
end

lemma nth_set_card {n : ℕ} (hp : (set_of p).finite)
  (hp' : {i : ℕ | p i ∧ ∀ k < n, nth p k < i}.finite) :
  hp'.to_finset.card = hp.to_finset.card - n :=
begin
  obtain hn | hn := le_or_lt n hp.to_finset.card,
  { exact nth_set_card_aux p hp _ hn },
  rw nat.sub_eq_zero_of_le hn.le,
  simp only [finset.card_eq_zero, set.finite.to_finset_eq_empty, ←set.subset_empty_iff],
  convert_to _ ⊆ {i : ℕ | p i ∧ ∀ (k : ℕ), k < hp.to_finset.card → nth p k < i},
  { symmetry,
    rw [←set.finite.to_finset_eq_empty, ←finset.card_eq_zero,
        ←nat.sub_self hp.to_finset.card],
    { apply nth_set_card_aux p hp _ le_rfl },
    { exact hp.subset (λ x hx, hx.1) } },
  exact λ x hx, ⟨hx.1, λ k hk, hx.2 _ (hk.trans hn)⟩,
end

lemma nth_set_nonempty_of_lt_card {n : ℕ} (hp : (set_of p).finite) (hlt: n < hp.to_finset.card) :
  {i : ℕ | p i ∧ ∀ k < n, nth p k < i}.nonempty :=
begin
  have hp': {i : ℕ | p i ∧ ∀ (k : ℕ), k < n → nth p k < i}.finite,
  { exact hp.subset (λ x hx, hx.1) },
  rw [←hp'.to_finset_nonempty, ←finset.card_pos, nth_set_card p hp],
  exact nat.sub_pos_of_lt hlt,
end

lemma nth_mem_of_lt_card_finite_aux (n : ℕ) (hp : (set_of p).finite) (hlt : n < hp.to_finset.card) :
  nth p n ∈ {i : ℕ | p i ∧ ∀ k < n, nth p k < i} :=
begin
  rw nth,
  apply Inf_mem,
  exact nth_set_nonempty_of_lt_card _ _ hlt,
end

lemma nth_mem_of_lt_card_finite {n : ℕ} (hp : (set_of p).finite) (hlt : n < hp.to_finset.card) :
  p (nth p n) := (nth_mem_of_lt_card_finite_aux p n hp hlt).1

lemma nth_strict_mono_of_finite {m n : ℕ} (hp : (set_of p).finite)
  (hlt : n < hp.to_finset.card) (hmn : m < n) : nth p m < nth p n :=
(nth_mem_of_lt_card_finite_aux p _ hp hlt).2 _ hmn

lemma nth_mem_of_infinite_aux (hp : (set_of p).infinite) (n : ℕ) :
  nth p n ∈ { i : ℕ | p i ∧ ∀ k < n, nth p k < i } :=
begin
  rw nth,
  apply Inf_mem,
  let s : set ℕ := ⋃ (k < n), { i : ℕ | nth p k ≥ i },
  convert_to ((set_of p) \ s).nonempty,
  { ext i,
    simp },
  refine (hp.diff $ (set.finite_lt_nat _).bUnion _).nonempty,
  exact λ k h, set.finite_le_nat _,
end

lemma nth_mem_of_infinite (hp : (set_of p).infinite) (n : ℕ) : p (nth p n) :=
(nth_mem_of_infinite_aux p hp n).1

lemma nth_strict_mono (hp : (set_of p).infinite) : strict_mono (nth p) :=
λ a b, (nth_mem_of_infinite_aux p hp b).2 _

lemma nth_injective_of_infinite (hp : (set_of p).infinite) : function.injective (nth p) :=
begin
  intros m n h,
  wlog h' : m ≤ n,
  { exact (this p hp h.symm (le_of_not_le h')).symm },
  rw le_iff_lt_or_eq at h',
  obtain (h' | rfl) := h',
  { simpa [h] using nth_strict_mono p hp h' },
  { refl },
end

lemma nth_monotone (hp : (set_of p).infinite) : monotone (nth p) :=
(nth_strict_mono p hp).monotone

lemma nth_mono_of_finite {a b : ℕ} (hp : (set_of p).finite) (hb : b < hp.to_finset.card)
  (hab : a ≤ b) : nth p a ≤ nth p b :=
begin
  obtain rfl | h := hab.eq_or_lt,
  { exact le_rfl },
  { exact (nth_strict_mono_of_finite p hp hb h).le }
end

lemma le_nth_of_lt_nth_succ_finite {k a : ℕ} (hp : (set_of p).finite)
  (hlt : k.succ < hp.to_finset.card) (h : a < nth p k.succ) (ha : p a) :
  a ≤ nth p k :=
begin
  by_contra' hak,
  refine h.not_le _,
  rw nth,
  apply nat.Inf_le,
  refine ⟨ha, λ n hn, lt_of_le_of_lt _ hak⟩,
  exact nth_mono_of_finite p hp (k.le_succ.trans_lt hlt) (le_of_lt_succ hn),
end

lemma le_nth_of_lt_nth_succ_infinite {k a : ℕ} (hp : (set_of p).infinite)
  (h : a < nth p k.succ) (ha : p a) :
  a ≤ nth p k :=
begin
  by_contra' hak,
  refine h.not_le _,
  rw nth,
  apply nat.Inf_le,
  exact ⟨ha, λ n hn, (nth_monotone p hp (le_of_lt_succ hn)).trans_lt hak⟩,
end

section count
variables [decidable_pred p]

@[simp] lemma count_nth_zero : count p (nth p 0) = 0 :=
begin
  rw [count_eq_card_filter_range, finset.card_eq_zero, nth_zero],
  ext a,
  simp_rw [not_mem_empty, mem_filter, mem_range, iff_false],
  rintro ⟨ha, hp⟩,
  exact ha.not_le (nat.Inf_le hp),
end

lemma filter_range_nth_eq_insert_of_finite (hp : (set_of p).finite) {k : ℕ}
  (hlt : k.succ < hp.to_finset.card) :
  finset.filter p (finset.range (nth p k.succ)) =
    insert (nth p k) (finset.filter p (finset.range (nth p k))) :=
begin
  ext a,
  simp_rw [mem_insert, mem_filter, mem_range],
  split,
  { rintro ⟨ha, hpa⟩,
    refine or_iff_not_imp_left.mpr (λ h, ⟨lt_of_le_of_ne _ h, hpa⟩),
    exact le_nth_of_lt_nth_succ_finite p hp hlt ha hpa },
  { rintro (ha | ⟨ha, hpa⟩),
    { rw ha,
      refine ⟨nth_strict_mono_of_finite p hp hlt (lt_add_one _), _⟩,
      apply nth_mem_of_lt_card_finite p hp,
      exact (k.le_succ).trans_lt hlt },
    refine ⟨ha.trans _, hpa⟩,
    exact nth_strict_mono_of_finite p hp hlt (lt_add_one _) }
end

lemma count_nth_of_lt_card_finite {n : ℕ} (hp : (set_of p).finite)
  (hlt : n < hp.to_finset.card) : count p (nth p n) = n :=
begin
  induction n with k hk,
  { exact count_nth_zero _ },
  { rw [count_eq_card_filter_range, filter_range_nth_eq_insert_of_finite p hp hlt,
      finset.card_insert_of_not_mem, ←count_eq_card_filter_range, hk (lt_of_succ_lt hlt)],
    simp, },
end

lemma filter_range_nth_eq_insert_of_infinite (hp : (set_of p).infinite) (k : ℕ) :
  (finset.range (nth p k.succ)).filter p = insert (nth p k) ((finset.range (nth p k)).filter p) :=
begin
  ext a,
  simp_rw [mem_insert, mem_filter, mem_range],
  split,
  { rintro ⟨ha, hpa⟩,
    rw nth at ha,
    refine or_iff_not_imp_left.mpr (λ hne, ⟨(le_of_not_lt $ λ h, _).lt_of_ne hne, hpa⟩),
    exact ha.not_le (nat.Inf_le ⟨hpa, λ b hb, (nth_monotone p hp (le_of_lt_succ hb)).trans_lt h⟩) },
  { rintro (rfl | ⟨ha, hpa⟩),
    { exact ⟨nth_strict_mono p hp (lt_succ_self k), nth_mem_of_infinite p hp _⟩ },
    { exact ⟨ha.trans (nth_strict_mono p hp (lt_succ_self k)), hpa⟩ } }
end

lemma count_nth_of_infinite (hp : (set_of p).infinite) (n : ℕ) : count p (nth p n) = n :=
begin
  induction n with k hk,
  { exact count_nth_zero _ },
  { rw [count_eq_card_filter_range, filter_range_nth_eq_insert_of_infinite p hp,
      finset.card_insert_of_not_mem, ←count_eq_card_filter_range, hk],
    simp, },
end

@[simp] lemma nth_count {n : ℕ} (hpn : p n) : nth p (count p n) = n :=
begin
  obtain hp | hp := em (set_of p).finite,
  { refine count_injective _ hpn _,
    { apply nth_mem_of_lt_card_finite p hp,
      exact count_lt_card hp hpn },
    { exact count_nth_of_lt_card_finite _ _ (count_lt_card hp hpn) } },
  { apply count_injective (nth_mem_of_infinite _ hp _) hpn,
  apply count_nth_of_infinite p hp }
end

lemma nth_count_eq_Inf {n : ℕ} : nth p (count p n) = Inf {i : ℕ | p i ∧ n ≤ i} :=
begin
  rw nth,
  congr,
  ext a,
  simp only [set.mem_set_of_eq, and.congr_right_iff],
  intro hpa,
  refine ⟨λ h, _, λ hn k hk, lt_of_lt_of_le _ hn⟩,
  { by_contra ha,
    simp only [not_le] at ha,
    have hn : nth p (count p a) < a := h _ (count_strict_mono hpa ha),
    rwa [nth_count p hpa, lt_self_iff_false] at hn },
  { apply (count_monotone p).reflect_lt,
    convert hk,
    obtain hp | hp : (set_of p).finite ∨ (set_of p).infinite := em (set_of p).finite,
    { rw count_nth_of_lt_card_finite _ hp,
      exact hk.trans ((count_monotone _ hn).trans_lt (count_lt_card hp hpa)) },
    { apply count_nth_of_infinite p hp } }
end

lemma nth_count_le (hp : (set_of p).infinite) (n : ℕ) : n ≤ nth p (count p n) :=
begin
  rw nth_count_eq_Inf,
  suffices h : Inf {i : ℕ | p i ∧ n ≤ i} ∈ {i : ℕ | p i ∧ n ≤ i},
  { exact h.2 },
  apply Inf_mem,
  obtain ⟨m, hp, hn⟩ := hp.exists_nat_lt n,
  exact ⟨m, hp, hn.le⟩
end

lemma count_nth_gc (hp : (set_of p).infinite) : galois_connection (count p) (nth p) :=
begin
  rintro x y,
  rw [nth, le_cInf_iff ⟨0, λ _ _, nat.zero_le _⟩ ⟨nth p y, nth_mem_of_infinite_aux p hp y⟩],
  dsimp,
  refine ⟨_, λ h, _⟩,
  { rintro hy n ⟨hn, h⟩,
    obtain hy' | rfl := hy.lt_or_eq,
    { exact (nth_count_le p hp x).trans (h (count p x) hy').le },
    { specialize h (count p n),
      replace hn : nth p (count p n) = n := nth_count _ hn,
      replace h : count p x ≤ count p n := by rwa [hn, lt_self_iff_false, imp_false, not_lt] at h,
      refine (nth_count_le p hp x).trans _,
      rw ← hn,
      exact nth_monotone p hp h }, },
  { rw ←count_nth_of_infinite p hp y,
    exact count_monotone _ (h (nth p y) ⟨nth_mem_of_infinite p hp y,
      λ k hk, nth_strict_mono p hp hk⟩) }
end

lemma count_le_iff_le_nth (hp : (set_of p).infinite) {a b : ℕ} :
  count p a ≤ b ↔ a ≤ nth p b := count_nth_gc p hp _ _

lemma lt_nth_iff_count_lt (hp : (set_of p).infinite) {a b : ℕ} :
  a < count p b ↔ nth p a < b := lt_iff_lt_of_le_iff_le $ count_le_iff_le_nth p hp

lemma nth_lt_of_lt_count (n k : ℕ) (h : k < count p n) : nth p k < n :=
begin
  obtain hp | hp := em (set_of p).finite,
  { refine (count_monotone p).reflect_lt _,
    rwa count_nth_of_lt_card_finite p hp,
    refine h.trans_le _,
    rw count_eq_card_filter_range,
    exact finset.card_le_of_subset (λ x hx, hp.mem_to_finset.2 (mem_filter.1 hx).2) },
  { rwa ← lt_nth_iff_count_lt _ hp }
end

lemma le_nth_of_count_le (n k : ℕ) (h: n ≤ nth p k) : count p n ≤ k :=
begin
  by_contra hc,
  apply not_lt.mpr h,
  apply nth_lt_of_lt_count,
  simpa using hc
end

end count

lemma nth_zero_of_nth_zero (h₀ : ¬p 0) {a b : ℕ} (hab : a ≤ b) (ha : nth p a = 0) :
  nth p b = 0 :=
begin
  rw [nth, Inf_eq_zero] at ⊢ ha,
  cases ha,
  { exact (h₀ ha.1).elim },
  { refine or.inr (set.eq_empty_of_subset_empty $ λ x hx, _),
    rw ←ha,
    exact ⟨hx.1, λ k hk, hx.2 k $ hk.trans_le hab⟩ }
end

/-- When `p` is true infinitely often, `nth` agrees with `nat.subtype.order_iso_of_nat`. -/
lemma nth_eq_order_iso_of_nat (i : infinite (set_of p)) (n : ℕ) :
  nth p n = nat.subtype.order_iso_of_nat (set_of p) n :=
begin
  classical,
  have hi := set.infinite_coe_iff.mp i,
  induction n with k hk;
  simp only [subtype.order_iso_of_nat_apply, subtype.of_nat, nat_zero_eq_zero],
  { rw [nat.subtype.coe_bot, nth_zero_of_exists], },
  { simp only [nat.subtype.succ, set.mem_set_of_eq, subtype.coe_mk, subtype.val_eq_coe],
    rw [subtype.order_iso_of_nat_apply] at hk,
    set b := nth p k.succ - nth p k - 1 with hb,
    replace hb : p (↑(subtype.of_nat (set_of p) k) + b + 1),
    { rw [hb, ←hk, tsub_right_comm],
      have hn11: nth p k.succ - 1 + 1 = nth p k.succ,
      { rw tsub_add_cancel_iff_le,
        exact succ_le_of_lt (pos_of_gt (nth_strict_mono p hi (lt_add_one k))), },
      rw add_tsub_cancel_of_le,
      { rw hn11,
        apply nth_mem_of_infinite p hi },
      { rw [← lt_succ_iff, ← nat.add_one, hn11],
        apply nth_strict_mono p hi,
        exact lt_add_one k } },
    have H : (∃ n: ℕ , p (↑(subtype.of_nat (set_of p) k) + n + 1)) := ⟨b, hb⟩,
    set t := nat.find H with ht,
    obtain ⟨hp, hmin⟩ := (nat.find_eq_iff _).mp ht,
    rw [←ht, ←hk] at hp hmin ⊢,
    rw [nth, Inf_def ⟨_, nth_mem_of_infinite_aux p hi k.succ⟩, nat.find_eq_iff],
    refine ⟨⟨by convert hp, λ r hr, _⟩, λ n hn, _⟩,
    { rw lt_succ_iff at ⊢ hr,
      exact (nth_monotone p hi hr).trans (by simp) },
    simp only [exists_prop, not_and, not_lt, set.mem_set_of_eq, not_forall],
    refine λ hpn, ⟨k, lt_add_one k, _⟩,
    by_contra' hlt,
    replace hn : n - nth p k - 1 < t,
    { rw tsub_lt_iff_left,
      { rw tsub_lt_iff_left hlt.le,
        convert hn using 1,
        ac_refl },
      exact le_tsub_of_add_le_left (succ_le_of_lt hlt) },
    refine hmin (n - nth p k - 1) hn _,
    convert hpn,
    have hn11 : n - 1 + 1 = n := nat.sub_add_cancel (pos_of_gt hlt),
    rwa [tsub_right_comm, add_tsub_cancel_of_le],
    rwa [←hn11, lt_succ_iff] at hlt },
end

end nat

author: leanprover-community

repo: mathlib


text:
import algebra.category.Module.monoidal
import linear_algebra.tensor_algebra
import algebra.category.CommRing.basic

open category_theory
variables {C : Type*} [category C] [monoidal_category C]
/-

def tensor_power_aux (X : C) : ℕ → C
| 0 := 𝟙_ C
| (n+1) := tensor_power_aux n ⊗ X

instance wtf {R : Type*} [comm_ring R] : monoidal_category (Module R) :=
Module.Module.monoidal_category

def tensor_power {R : Type*} [comm_ring R] (M : Module R) : ℕ → Module R :=
@tensor_power_aux _ _ huh.wtf M-/

universe u
def tpow_aux (R : Type u) [comm_semiring R] (M : Type u) [add_comm_monoid M] [semimodule R M] :
  ℕ → Σ (N : Type*) (h : add_comm_monoid N), @semimodule R N _ h
| 0 := ⟨R, ⟨by apply_instance, by apply_instance⟩⟩
| (n+1) := ⟨@tensor_product R _ (tpow_aux n).1 M (tpow_aux n).2.1 _ (tpow_aux n).2.2 _, ⟨by apply_instance, by apply_instance⟩⟩

def tpow (R : Type u) [comm_semiring R] (M : Type u) [add_comm_monoid M] [semimodule R M] (n : ℕ) :=
(tpow_aux R M n).1

instance tpow_acg (R : Type u) [comm_semiring R] (M : Type u) [add_comm_monoid M] [semimodule R M] (n : ℕ) :
add_comm_monoid (tpow R M n) := (tpow_aux R M n).2.1

instance tpow_semimodule (R : Type u) [comm_semiring R] (M : Type u) [add_comm_monoid M] [semimodule R M] (n : ℕ) :
semimodule R (tpow R M n) := (tpow_aux R M n).2.2

--abbreviation tpow (R : Type u) [comm_ring R] (M : Type u) [add_comm_group M]
--  [module R M] := tensor_power (Module.of R M)

variables {R : Type u} [comm_semiring R] {M : Type u} [add_comm_monoid M] [semimodule R M]

--lemma tpow_zero : tensor_power (Module.of R M) 0 = Module.of R R := rfl

lemma tpow_zero : tpow R M 0 = R := rfl

--def tpow_one : tensor_power (Module.of R M) 1 ≅ Module.of R M :=
--Module.monoidal_category.left_unitor (Module.of R M)
variables (R M)
def tpow_one : linear_equiv R (tpow R M 1) M :=
tensor_product.lid R M

namespace tpow
def algebra_alg_hom (S : Type*) [semiring S] [algebra R S] : R →ₐ[R] S :=
{  commutes' := λ r, rfl,
   ..algebra_map R S }

local attribute [semireducible] tensor_algebra

def of_scalar :
  R →ₗ[R] tensor_algebra R M :=
(((ring_quot.mk_alg_hom R (tensor_algebra.rel R M)).comp
(algebra_alg_hom R (free_algebra R M))) : R →ₐ[R] tensor_algebra R M).to_linear_map

/-def mk : Π (n : ℕ) (f : fin n → M), tpow R M n
| 0 _ := (1 : R)
| (n + 1) f := tensor_product.mk _ _ _ (mk n $ λ y, f y) $ f (n + 1)-/

def mk : Π (n : ℕ) (f : fin n → M), tpow R M n
| 0 _ := (1 : R)
| (n + 1) f := @tensor_product.mk R _ (tpow R M n) M _ _ _ _ (mk n $ λ y, f y) $ f (n + 1)

variables (x : M)

def mk' (n : ℕ) : @multilinear_map R (fin n) (λ _, M) (tpow R M n) _ _ _ _ _ _ :=
{ to_fun := mk R M n,
  map_add' := λ f m x y, sorry,
  map_smul' := sorry }

variables {R M}
lemma mk'_apply (n : ℕ) (x) : mk' R M n x = mk R M n x := rfl

lemma mk_one_lid (x : tensor_product R R M) :
  tensor_product.mk R R M 1 (tensor_product.lid R M x) = x :=
begin
  apply tensor_product.induction_on x,
  rw linear_equiv.map_zero, convert tensor_product.tmul_zero _ _,
  intros y z,
  rw tensor_product.lid_tmul, rw map_smul_eq_smul_map,
  erw tensor_product.smul_tmul',
  rw [algebra.id.smul_eq_mul, mul_one],
  intros y z hy hz,
  simp only [tensor_product.mk_apply, linear_equiv.map_add] at *,
  rw tensor_product.tmul_add, rw hy, rw hz,
end

lemma mk_one_rid (x : tensor_product R M R) :
  tensor_product.mk R M R (tensor_product.rid R M x) 1 = x :=
begin
  apply tensor_product.induction_on x,
  rw linear_equiv.map_zero, convert tensor_product.zero_tmul _ _,
  intros y z,
  erw tensor_product.lid_tmul,
  rw map_smul_eq_smul_map,
  rw linear_map.smul_apply,
  simp only [],
  erw ←tensor_product.tmul_smul,
  rw algebra.id.smul_eq_mul, rw mul_one,
  intros y z hy hz,
  simp only [tensor_product.mk_apply, linear_equiv.map_add] at *,
  rw tensor_product.add_tmul, rw hy, rw hz,
end

variables (R M)
def fin0_to_multilinear (f : (fin 0 → M) → R) :
  @multilinear_map R (fin 0) (λ _, M) R _ _ _ _ _ _ :=
{ to_fun := f,
  map_add' := λ x y a b, fin.elim0 y,
  map_smul' := λ x y, fin.elim0 y }

variables {R M}
@[simp] lemma to_span_singleton_apply (x : M) (r : R) :
  linear_map.to_span_singleton R M x r = r • x := rfl

lemma eq_smul_one (f : R →ₗ[R] M) (x : R) :
  x • f 1 = f x :=
by rw [←f.map_smul, algebra.id.smul_eq_mul, mul_one]

lemma eq_iff_eq_one (f g : R →ₗ[R] M) :
  f = g ↔ f 1 = g 1 :=
⟨λ h, h ▸ rfl, λ h, linear_map.ext $ λ x, by
  rw [←eq_smul_one, h, eq_smul_one]⟩

/-def lift {M : Type u} [add_comm_group M] [module R M] :
  Π (n : ℕ) (P : Type u) {h1 : add_comm_monoid P}, by exactI Π
  {h2 : semimodule R P}, by exactI Π
  (f : @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _),
  tpow R M n →ₗ[R] P
| 0 P h1 h2 g := @linear_map.to_span_singleton R P _ h1 h2 $ g (default _)
| (n + 1) P h1 h2 g := @tensor_product.lift _ _ _ _ _ _ _ h1 _ _ h2
$ lift n _ (@multilinear_map.curry_right _ _ _ _ _ _ h1 _ h2 g)-/

variables (R M)
def lift {M : Type u} [add_comm_monoid M] [semimodule R M] :
  Π (n : ℕ) (P : Type u) {h1 : add_comm_monoid P}, by exactI Π
  {h2 : semimodule R P}, by exactI Π
  (f : @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _),
  tpow R M n →ₗ[R] P
| 0 P h1 h2 g := @linear_map.to_span_singleton R P _ h1 h2 $ g (default (fin 0 → M))
| (n + 1) P h1 h2 g := @tensor_product.lift _ _ _ _ _ _ _ h1 _ _ h2
$ lift n _ (@multilinear_map.curry_right _ _ _ _ _ _ h1 _ h2 g)

variables {R M}
lemma lift_mk {M : Type u} [add_comm_monoid M] [semimodule R M] (n : ℕ) :
  ∀ {P : Type u} [add_comm_monoid P], by exactI ∀ [semimodule R P],
  by exactI ∀
  (f : @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _),
(lift R n P f).comp_multilinear_map (mk' R M n) = f :=
begin
  induction n with n hn,
    intros,
    ext,
    show linear_map.to_span_singleton _ _ _ (1 : R) = _,
    rw linear_map.to_span_singleton_one,
    congr,
  intros,
  ext,
  show tensor_product.lift _ (tensor_product.mk _ _ _ _ _) = _,
  rw tensor_product.mk_apply,
  rw tensor_product.lift.tmul,
  unfreezingI {erw multilinear_map.ext_iff.1 (hn f.curry_right) (λ y : fin n, x y)},
  rw f.curry_right_apply,
  congr,
  sorry -- annoying fin stuff
end

lemma lift_mk_apply {M : Type u} [add_comm_monoid M] [semimodule R M] (n : ℕ)
  {P : Type u} [add_comm_monoid P] [semimodule R P]
  (f : @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _) (x) :
lift R n P f (mk' R M n x) = f x :=
multilinear_map.ext_iff.1 (lift_mk n f) _

lemma lift_unique {M : Type u} [add_comm_monoid M] [semimodule R M] (n : ℕ) :
  ∀ {P : Type u} [add_comm_monoid P], by exactI ∀ [semimodule R P],
  by exactI ∀
  (f : @multilinear_map R (fin n) (λ _, M) P _ _ _ _ _ _)
  (g : tpow R M n →ₗ[R] P)
  (H : ∀ x : fin n → M, g (mk' R M n x) = f x),
  g = lift R n P f :=
begin
  induction n with n hn,
    intros,
    ext,
    rw ←eq_smul_one,
    erw H (default _),
    refl,
  intros,
  unfold lift,
  ext (x : tpow R M n) y,
  rw tensor_product.lift.tmul,
  unfreezingI { rw ←hn f.curry_right (tensor_product.lcurry _ (tpow R M n) _ _ g)
    (λ x, by {ext z,
    rw f.curry_right_apply,rw ← H (fin.snoc x z),
    rw tensor_product.lcurry_apply,
    rw mk'_apply, rw mk'_apply,
    unfold mk,
    rw tensor_product.mk_apply,
    congr,
    specialize H (fin.snoc x z),
    ext,
    sorry, --more stupid fin stuff
    sorry, --same
        }), },
  refl,
end

end tpow

repo: test


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 model_theory.ultraproducts
import model_theory.bundled
import model_theory.skolem

/-!
# First-Order Satisfiability
This file deals with the satisfiability of first-order theories, as well as equivalence over them.

## Main Definitions
* `first_order.language.Theory.is_satisfiable`: `T.is_satisfiable` indicates that `T` has a nonempty
model.
* `first_order.language.Theory.is_finitely_satisfiable`: `T.is_finitely_satisfiable` indicates that
every finite subset of `T` is satisfiable.
* `first_order.language.Theory.is_complete`: `T.is_complete` indicates that `T` is satisfiable and
models each sentence or its negation.
* `first_order.language.Theory.semantically_equivalent`: `T.semantically_equivalent φ ψ` indicates
that `φ` and `ψ` are equivalent formulas or sentences in models of `T`.
* `cardinal.categorical`: A theory is `κ`-categorical if all models of size `κ` are isomorphic.

## Main Results
* The Compactness Theorem, `first_order.language.Theory.is_satisfiable_iff_is_finitely_satisfiable`,
shows that a theory is satisfiable iff it is finitely satisfiable.
* `first_order.language.complete_theory.is_complete`: The complete theory of a structure is
complete.
* `first_order.language.Theory.exists_large_model_of_infinite_model` shows that any theory with an
infinite model has arbitrarily large models.
* `first_order.language.Theory.exists_elementary_embedding_card_eq`: The Upward Löwenheim–Skolem
Theorem: If `κ` is a cardinal greater than the cardinalities of `L` and an infinite `L`-structure
`M`, then `M` has an elementary extension of cardinality `κ`.

## Implementation Details
* Satisfiability of an `L.Theory` `T` is defined in the minimal universe containing all the symbols
of `L`. By Löwenheim-Skolem, this is equivalent to satisfiability in any universe.

-/

universes u v w w'

open cardinal category_theory
open_locale cardinal first_order

namespace first_order
namespace language

variables {L : language.{u v}} {T : L.Theory} {α : Type w} {n : ℕ}

namespace Theory

variable (T)

/-- A theory is satisfiable if a structure models it. -/
def is_satisfiable : Prop := nonempty (Model.{u v (max u v)} T)

/-- A theory is finitely satisfiable if all of its finite subtheories are satisfiable. -/
def is_finitely_satisfiable : Prop :=
∀ (T0 : finset L.sentence), (T0 : L.Theory) ⊆ T → (T0 : L.Theory).is_satisfiable

variables {T} {T' : L.Theory}

lemma model.is_satisfiable (M : Type w) [n : nonempty M]
  [S : L.Structure M] [M ⊨ T] : T.is_satisfiable :=
⟨((⊥ : substructure _ (Model.of T M)).elementary_skolem₁_reduct.to_Model T).shrink⟩

lemma is_satisfiable.mono (h : T'.is_satisfiable) (hs : T ⊆ T') :
  T.is_satisfiable :=
⟨(Theory.model.mono (Model.is_model h.some) hs).bundled⟩

lemma is_satisfiable_empty (L : language.{u v}) :
  is_satisfiable (∅ : L.Theory) :=
⟨default⟩

lemma is_satisfiable_of_is_satisfiable_on_Theory {L' : language.{w w'}} (φ : L →ᴸ L')
  (h : (φ.on_Theory T).is_satisfiable) :
  T.is_satisfiable :=
model.is_satisfiable (h.some.reduct φ)

lemma is_satisfiable.is_finitely_satisfiable (h : T.is_satisfiable) :
  T.is_finitely_satisfiable :=
λ _, h.mono

/-- The Compactness Theorem of first-order logic: A theory is satisfiable if and only if it is
finitely satisfiable. -/
theorem is_satisfiable_iff_is_finitely_satisfiable {T : L.Theory} :
  T.is_satisfiable ↔ T.is_finitely_satisfiable :=
⟨Theory.is_satisfiable.is_finitely_satisfiable, λ h, begin
  classical,
  set M : Π (T0 : finset T), Type (max u v) :=
    λ T0, (h (T0.map (function.embedding.subtype (λ x, x ∈ T)))
      T0.map_subtype_subset).some with hM,
  let M' := filter.product ↑(ultrafilter.of (filter.at_top : filter (finset T))) M,
  haveI h' : M' ⊨ T,
  { refine ⟨λ φ hφ, _⟩,
    rw ultraproduct.sentence_realize,
    refine filter.eventually.filter_mono (ultrafilter.of_le _)
      (filter.eventually_at_top.2 ⟨{⟨φ, hφ⟩},
      λ s h', Theory.realize_sentence_of_mem (s.map (function.embedding.subtype (λ x, x ∈ T))) _⟩),
    simp only [finset.coe_map, function.embedding.coe_subtype, set.mem_image, finset.mem_coe,
      subtype.exists, subtype.coe_mk, exists_and_distrib_right, exists_eq_right],
    exact ⟨hφ, h' (finset.mem_singleton_self _)⟩ },
  exact ⟨Model.of T M'⟩,
end⟩

theorem is_satisfiable_directed_union_iff {ι : Type*} [nonempty ι]
  {T : ι → L.Theory} (h : directed (⊆) T) :
  Theory.is_satisfiable (⋃ i, T i) ↔ ∀ i, (T i).is_satisfiable :=
begin
  refine ⟨λ h' i, h'.mono (set.subset_Union _ _), λ h', _⟩,
  rw [is_satisfiable_iff_is_finitely_satisfiable, is_finitely_satisfiable],
  intros T0 hT0,
  obtain ⟨i, hi⟩ := h.exists_mem_subset_of_finset_subset_bUnion hT0,
  exact (h' i).mono hi,
end

theorem is_satisfiable_union_distinct_constants_theory_of_card_le (T : L.Theory) (s : set α)
  (M : Type w') [nonempty M] [L.Structure M] [M ⊨ T]
  (h : cardinal.lift.{w'} (# s) ≤ cardinal.lift.{w} (# M)) :
  ((L.Lhom_with_constants α).on_Theory T ∪ L.distinct_constants_theory s).is_satisfiable :=
begin
  haveI : inhabited M := classical.inhabited_of_nonempty infer_instance,
  rw [cardinal.lift_mk_le'] at h,
  letI : (constants_on α).Structure M :=
    constants_on.Structure (function.extend coe h.some default),
  haveI : M ⊨ (L.Lhom_with_constants α).on_Theory T ∪ L.distinct_constants_theory s,
  { refine ((Lhom.on_Theory_model _ _).2 infer_instance).union _,
    rw [model_distinct_constants_theory],
    refine λ a as b bs ab, _,
    rw [← subtype.coe_mk a as, ← subtype.coe_mk b bs, ← subtype.ext_iff],
    exact h.some.injective
      ((subtype.coe_injective.extend_apply h.some default ⟨a, as⟩).symm.trans
      (ab.trans (subtype.coe_injective.extend_apply h.some default ⟨b, bs⟩))), },
  exact model.is_satisfiable M,
end

theorem is_satisfiable_union_distinct_constants_theory_of_infinite (T : L.Theory) (s : set α)
  (M : Type w') [L.Structure M] [M ⊨ T] [infinite M] :
  ((L.Lhom_with_constants α).on_Theory T ∪ L.distinct_constants_theory s).is_satisfiable :=
begin
  classical,
  rw [distinct_constants_theory_eq_Union, set.union_Union, is_satisfiable_directed_union_iff],
  { exact λ t, is_satisfiable_union_distinct_constants_theory_of_card_le T _ M ((lift_le_aleph_0.2
      ((finset_card_lt_aleph_0 _).le)).trans (aleph_0_le_lift.2 (aleph_0_le_mk M))) },
  { refine (monotone_const.union (monotone_distinct_constants_theory.comp _)).directed_le,
    simp only [finset.coe_map, function.embedding.coe_subtype],
    exact set.monotone_image.comp (λ _ _, finset.coe_subset.2) }
end

/-- Any theory with an infinite model has arbitrarily large models. -/
lemma exists_large_model_of_infinite_model (T : L.Theory) (κ : cardinal.{w})
  (M : Type w') [L.Structure M] [M ⊨ T] [infinite M] :
  ∃ (N : Model.{_ _ (max u v w)} T), cardinal.lift.{max u v w} κ ≤ # N :=
begin
  obtain ⟨N⟩ :=
    is_satisfiable_union_distinct_constants_theory_of_infinite T (set.univ : set κ.out) M,
  refine ⟨(N.is_model.mono (set.subset_union_left _ _)).bundled.reduct _, _⟩,
  haveI : N ⊨ distinct_constants_theory _ _ := N.is_model.mono (set.subset_union_right _ _),
  simp only [Model.reduct_carrier, coe_of, Model.carrier_eq_coe],
  refine trans (lift_le.2 (le_of_eq (cardinal.mk_out κ).symm)) _,
  rw [← mk_univ],
  refine (card_le_of_model_distinct_constants_theory L set.univ N).trans (lift_le.1 _),
  rw lift_lift,
end

lemma is_satisfiable_Union_iff_is_satisfiable_Union_finset {ι : Type*} (T : ι → L.Theory) :
  is_satisfiable (⋃ i, T i) ↔ ∀ (s : finset ι), is_satisfiable (⋃ (i ∈ s), T i) :=
begin
  classical,
  refine ⟨λ h s, h.mono (set.Union_mono (λ _, set.Union_subset_iff.2 (λ _, refl _))), λ h, _⟩,
  rw is_satisfiable_iff_is_finitely_satisfiable,
  intros s hs,
  rw set.Union_eq_Union_finset at hs,
  obtain ⟨t, ht⟩ := directed.exists_mem_subset_of_finset_subset_bUnion _ hs,
  { exact (h t).mono ht },
  { exact (monotone.directed_le (λ t1 t2 h, set.Union_mono (λ _, set.Union_mono'
    (λ h1, ⟨h h1, refl _⟩)))) },
end

end Theory

variables (L)

/-- A version of The Downward Löwenheim–Skolem theorem where the structure `N` elementarily embeds
into `M`, but is not by type a substructure of `M`, and thus can be chosen to belong to the universe
of the cardinal `κ`.
 -/
lemma exists_elementary_embedding_card_eq_of_le (M : Type w') [L.Structure M] [nonempty M]
  (κ : cardinal.{w})
  (h1 : ℵ₀ ≤ κ)
  (h2 : lift.{w} L.card ≤ cardinal.lift.{max u v} κ)
  (h3 : lift.{w'} κ ≤ cardinal.lift.{w} (# M)) :
  ∃ (N : bundled L.Structure), nonempty (N ↪ₑ[L] M) ∧ # N = κ :=
begin
  obtain ⟨S, _, hS⟩ := exists_elementary_substructure_card_eq L ∅ κ h1 (by simp) h2 h3,
  haveI : small.{w} S,
  { rw [← lift_inj.{_ (w + 1)}, lift_lift, lift_lift] at hS,
    exact small_iff_lift_mk_lt_univ.2 (lt_of_eq_of_lt hS κ.lift_lt_univ') },
  refine ⟨(equiv_shrink S).bundled_induced L,
    ⟨S.subtype.comp (equiv.bundled_induced_equiv L _).symm.to_elementary_embedding⟩,
    lift_inj.1 (trans _ hS)⟩,
  simp only [equiv.bundled_induced_α, lift_mk_shrink'],
end

/-- The Upward Löwenheim–Skolem Theorem: If `κ` is a cardinal greater than the cardinalities of `L`
and an infinite `L`-structure `M`, then `M` has an elementary extension of cardinality `κ`. -/
theorem exists_elementary_embedding_card_eq_of_ge (M : Type w') [L.Structure M] [iM : infinite M]
  (κ : cardinal.{w})
  (h1 : cardinal.lift.{w} L.card ≤ cardinal.lift.{max u v} κ)
  (h2 : cardinal.lift.{w} (# M) ≤ cardinal.lift.{w'} κ) :
  ∃ (N : bundled L.Structure), nonempty (M ↪ₑ[L] N) ∧ # N = κ :=
begin
  obtain ⟨N0, hN0⟩ := (L.elementary_diagram M).exists_large_model_of_infinite_model κ M,
  let f0 := elementary_embedding.of_models_elementary_diagram L M N0,
  rw [← lift_le.{(max w w') (max u v)}, lift_lift, lift_lift] at h2,
  obtain ⟨N, ⟨NN0⟩, hN⟩ := exists_elementary_embedding_card_eq_of_le (L[[M]]) N0 κ
    (aleph_0_le_lift.1 ((aleph_0_le_lift.2 (aleph_0_le_mk M)).trans h2)) _ (hN0.trans _),
  { letI := (Lhom_with_constants L M).reduct N,
    haveI h : N ⊨ L.elementary_diagram M :=
      (NN0.Theory_model_iff (L.elementary_diagram M)).2 infer_instance,
    refine ⟨bundled.of N, ⟨_⟩, hN⟩,
    apply elementary_embedding.of_models_elementary_diagram L M N, },
  { simp only [card_with_constants, lift_add, lift_lift],
    rw [add_comm, add_eq_max (aleph_0_le_lift.2 (infinite_iff.1 iM)), max_le_iff],
    rw [← lift_le.{_ w'}, lift_lift, lift_lift] at h1,
    exact ⟨h2, h1⟩, },
  { rw [← lift_umax', lift_id] },
end

/-- The Löwenheim–Skolem Theorem: If `κ` is a cardinal greater than the cardinalities of `L`
and an infinite `L`-structure `M`, then there is an elementary embedding in the appropriate
direction between then `M` and a structure of cardinality `κ`. -/
theorem exists_elementary_embedding_card_eq (M : Type w') [L.Structure M] [iM : infinite M]
  (κ : cardinal.{w})
  (h1 : ℵ₀ ≤ κ)
  (h2 : lift.{w} L.card ≤ cardinal.lift.{max u v} κ) :
  ∃ (N : bundled L.Structure), (nonempty (N ↪ₑ[L] M) ∨ nonempty (M ↪ₑ[L] N)) ∧ # N = κ :=
begin
  cases le_or_gt (lift.{w'} κ) (cardinal.lift.{w} (# M)),
  { obtain ⟨N, hN1, hN2⟩ := exists_elementary_embedding_card_eq_of_le L M κ h1 h2 h,
    exact ⟨N, or.inl hN1, hN2⟩ },
  { obtain ⟨N, hN1, hN2⟩ := exists_elementary_embedding_card_eq_of_ge L M κ h2 (le_of_lt h),
    exact ⟨N, or.inr hN1, hN2⟩ }
end

/-- A consequence of the Löwenheim–Skolem Theorem: If `κ` is a cardinal greater than the
cardinalities of `L` and an infinite `L`-structure `M`, then there is a structure of cardinality `κ`
elementarily equivalent to `M`. -/
lemma exists_elementarily_equivalent_card_eq (M : Type w') [L.Structure M] [infinite M]
  (κ : cardinal.{w})
  (h1 : ℵ₀ ≤ κ)
  (h2 : lift.{w} L.card ≤ cardinal.lift.{max u v} κ) :
  ∃ (N : category_theory.bundled L.Structure), M ≅[L] N ∧ # N = κ :=
begin
  obtain ⟨N, (NM | MN), hNκ⟩ := exists_elementary_embedding_card_eq L M κ h1 h2,
  { exact ⟨N, NM.some.elementarily_equivalent.symm, hNκ⟩ },
  { exact ⟨N, MN.some.elementarily_equivalent, hNκ⟩ }
end

variable {L}

namespace Theory

theorem exists_model_card_eq
  (h : ∃ (M : Model.{u v (max u v)} T), infinite M)
  (κ : cardinal.{w})
  (h1 : ℵ₀ ≤ κ)
  (h2 : cardinal.lift.{w} L.card ≤ cardinal.lift.{max u v} κ) :
  ∃ (N : Model.{u v w} T), # N = κ :=
begin
  casesI h with M MI,
  obtain ⟨N, hN, rfl⟩ := exists_elementarily_equivalent_card_eq L M κ h1 h2,
  haveI : nonempty N := hN.nonempty,
  exact ⟨hN.Theory_model.bundled, rfl⟩,
end

variable (T)

/-- A theory models a (bounded) formula when any of its nonempty models realizes that formula on all
  inputs.-/
def models_bounded_formula (φ : L.bounded_formula α n) : Prop :=
  ∀ (M : Model.{u v (max u v)} T) (v : α → M) (xs : fin n → M), φ.realize v xs

-- input using \|= or \vDash, but not using \models
infix (name := models_bounded_formula) ` ⊨ `:51 := models_bounded_formula

variable {T}

lemma models_formula_iff {φ : L.formula α} :
  T ⊨ φ ↔ ∀ (M : Model.{u v (max u v)} T) (v : α → M), φ.realize v :=
forall_congr (λ M, forall_congr (λ v, unique.forall_iff))

lemma models_sentence_iff {φ : L.sentence} :
  T ⊨ φ ↔ ∀ (M : Model.{u v (max u v)} T), M ⊨ φ :=
models_formula_iff.trans (forall_congr (λ M, unique.forall_iff))

lemma models_sentence_of_mem {φ : L.sentence} (h : φ ∈ T) :
  T ⊨ φ :=
models_sentence_iff.2 (λ _, realize_sentence_of_mem T h)

lemma models_iff_not_satisfiable (φ : L.sentence) :
  T ⊨ φ ↔ ¬ is_satisfiable (T ∪ {φ.not}) :=
begin
  rw [models_sentence_iff, is_satisfiable],
  refine ⟨λ h1 h2, (sentence.realize_not _).1 (realize_sentence_of_mem (T ∪ {formula.not φ})
    (set.subset_union_right _ _ (set.mem_singleton _)))
    (h1 (h2.some.subtheory_Model (set.subset_union_left _ _))), λ h M, _⟩,
  contrapose! h,
  rw ← sentence.realize_not at h,
  refine ⟨{ carrier := M,
    is_model := ⟨λ ψ hψ, hψ.elim (realize_sentence_of_mem _) (λ h', _)⟩, }⟩,
  rw set.mem_singleton_iff.1 h',
  exact h,
end

lemma models_bounded_formula.realize_sentence {φ : L.sentence} (h : T ⊨ φ)
  (M : Type*) [L.Structure M] [M ⊨ T] [nonempty M] :
  M ⊨ φ :=
begin
  rw models_iff_not_satisfiable at h,
  contrapose! h,
  haveI : M ⊨ (T ∪ {formula.not φ}),
  { simp only [set.union_singleton, model_iff, set.mem_insert_iff, forall_eq_or_imp,
      sentence.realize_not],
    rw ← model_iff,
    exact ⟨h, infer_instance⟩ },
  exact model.is_satisfiable M,
end

/-- A theory is complete when it is satisfiable and models each sentence or its negation. -/
def is_complete (T : L.Theory) : Prop :=
T.is_satisfiable ∧ ∀ (φ : L.sentence), (T ⊨ φ) ∨ (T ⊨ φ.not)

namespace is_complete

lemma models_not_iff (h : T.is_complete) (φ : L.sentence)  :
  T ⊨ φ.not ↔ ¬ T ⊨ φ :=
begin
  cases h.2 φ with hφ hφn,
  { simp only [hφ, not_true, iff_false],
    rw [models_sentence_iff, not_forall],
    refine ⟨h.1.some, _⟩,
    simp only [sentence.realize_not, not_not],
    exact models_sentence_iff.1 hφ _ },
  { simp only [hφn, true_iff],
    intro hφ,
    rw models_sentence_iff at *,
    exact hφn h.1.some (hφ _) }
end

lemma realize_sentence_iff (h : T.is_complete) (φ : L.sentence)
  (M : Type*) [L.Structure M] [M ⊨ T] [nonempty M] :
  M ⊨ φ ↔ T ⊨ φ :=
begin
  cases h.2 φ with hφ hφn,
  { exact iff_of_true (hφ.realize_sentence M) hφ },
  { exact iff_of_false ((sentence.realize_not M).1 (hφn.realize_sentence M))
      ((h.models_not_iff φ).1 hφn), }
end

end is_complete

/-- A theory is maximal when it is satisfiable and contains each sentence or its negation.
  Maximal theories are complete. -/
def is_maximal (T : L.Theory) : Prop :=
T.is_satisfiable ∧ ∀ (φ : L.sentence), φ ∈ T ∨ φ.not ∈ T

lemma is_maximal.is_complete (h : T.is_maximal) : T.is_complete :=
h.imp_right (forall_imp (λ _, or.imp models_sentence_of_mem models_sentence_of_mem))

lemma is_maximal.mem_or_not_mem (h : T.is_maximal) (φ : L.sentence) :
  φ ∈ T ∨ φ.not ∈ T :=
h.2 φ

lemma is_maximal.mem_of_models (h : T.is_maximal) {φ : L.sentence}
  (hφ : T ⊨ φ) :
  φ ∈ T :=
begin
  refine (h.mem_or_not_mem φ).resolve_right (λ con, _),
  rw [models_iff_not_satisfiable, set.union_singleton, set.insert_eq_of_mem con] at hφ,
  exact hφ h.1,
end

lemma is_maximal.mem_iff_models (h : T.is_maximal) (φ : L.sentence) :
  φ ∈ T ↔ T ⊨ φ :=
⟨models_sentence_of_mem, h.mem_of_models⟩

/-- Two (bounded) formulas are semantically equivalent over a theory `T` when they have the same
interpretation in every model of `T`. (This is also known as logical equivalence, which also has a
proof-theoretic definition.) -/
def semantically_equivalent (T : L.Theory) (φ ψ : L.bounded_formula α n) : Prop :=
T ⊨ φ.iff ψ

@[refl] lemma semantically_equivalent.refl (φ : L.bounded_formula α n) :
  T.semantically_equivalent φ φ :=
λ M v xs, by rw bounded_formula.realize_iff

instance : is_refl (L.bounded_formula α n) T.semantically_equivalent :=
⟨semantically_equivalent.refl⟩

@[symm] lemma semantically_equivalent.symm {φ ψ : L.bounded_formula α n}
  (h : T.semantically_equivalent φ ψ) :
  T.semantically_equivalent ψ φ :=
λ M v xs, begin
  rw [bounded_formula.realize_iff, iff.comm, ← bounded_formula.realize_iff],
  exact h M v xs,
end

@[trans] lemma semantically_equivalent.trans {φ ψ θ : L.bounded_formula α n}
  (h1 : T.semantically_equivalent φ ψ) (h2 : T.semantically_equivalent ψ θ) :
  T.semantically_equivalent φ θ :=
λ M v xs, begin
  have h1' := h1 M v xs,
  have h2' := h2 M v xs,
  rw [bounded_formula.realize_iff] at *,
  exact ⟨h2'.1 ∘ h1'.1, h1'.2 ∘ h2'.2⟩,
end

lemma semantically_equivalent.realize_bd_iff {φ ψ : L.bounded_formula α n}
  {M : Type (max u v)} [ne : nonempty M] [str : L.Structure M] [hM : T.model M]
  (h : T.semantically_equivalent φ ψ) {v : α → M} {xs : (fin n → M)} :
  φ.realize v xs ↔ ψ.realize v xs :=
bounded_formula.realize_iff.1 (h (Model.of T M) v xs)

lemma semantically_equivalent.realize_iff {φ ψ : L.formula α}
  {M : Type (max u v)} [ne : nonempty M] [str : L.Structure M] (hM : T.model M)
  (h : T.semantically_equivalent φ ψ) {v : α → M} :
  φ.realize v ↔ ψ.realize v :=
h.realize_bd_iff

/-- Semantic equivalence forms an equivalence relation on formulas. -/
def semantically_equivalent_setoid (T : L.Theory) : setoid (L.bounded_formula α n) :=
{ r := semantically_equivalent T,
  iseqv := ⟨λ _, refl _, λ a b h, h.symm, λ _ _ _ h1 h2, h1.trans h2⟩ }

protected lemma semantically_equivalent.all {φ ψ : L.bounded_formula α (n + 1)}
  (h : T.semantically_equivalent φ ψ) : T.semantically_equivalent φ.all ψ.all :=
begin
  simp_rw [semantically_equivalent, models_bounded_formula, bounded_formula.realize_iff,
    bounded_formula.realize_all],
  exact λ M v xs, forall_congr (λ a, h.realize_bd_iff),
end

protected lemma semantically_equivalent.ex {φ ψ : L.bounded_formula α (n + 1)}
  (h : T.semantically_equivalent φ ψ) : T.semantically_equivalent φ.ex ψ.ex :=
begin
  simp_rw [semantically_equivalent, models_bounded_formula, bounded_formula.realize_iff,
    bounded_formula.realize_ex],
  exact λ M v xs, exists_congr (λ a, h.realize_bd_iff),
end

protected lemma semantically_equivalent.not {φ ψ : L.bounded_formula α n}
  (h : T.semantically_equivalent φ ψ) : T.semantically_equivalent φ.not ψ.not :=
begin
  simp_rw [semantically_equivalent, models_bounded_formula, bounded_formula.realize_iff,
    bounded_formula.realize_not],
  exact λ M v xs, not_congr h.realize_bd_iff,
end

protected lemma semantically_equivalent.imp {φ ψ φ' ψ' : L.bounded_formula α n}
  (h : T.semantically_equivalent φ ψ) (h' : T.semantically_equivalent φ' ψ') :
  T.semantically_equivalent (φ.imp φ') (ψ.imp ψ') :=
begin
  simp_rw [semantically_equivalent, models_bounded_formula, bounded_formula.realize_iff,
    bounded_formula.realize_imp],
  exact λ M v xs, imp_congr h.realize_bd_iff h'.realize_bd_iff,
end

end Theory

namespace complete_theory

variables (L) (M : Type w) [L.Structure M]

lemma is_satisfiable [nonempty M] : (L.complete_theory M).is_satisfiable :=
Theory.model.is_satisfiable M

lemma mem_or_not_mem (φ : L.sentence) :
  φ ∈ L.complete_theory M ∨ φ.not ∈ L.complete_theory M :=
by simp_rw [complete_theory, set.mem_set_of_eq, sentence.realize, formula.realize_not, or_not]

lemma is_maximal [nonempty M] : (L.complete_theory M).is_maximal :=
⟨is_satisfiable L M, mem_or_not_mem L M⟩

lemma is_complete [nonempty M] : (L.complete_theory M).is_complete :=
(complete_theory.is_maximal L M).is_complete

end complete_theory

namespace bounded_formula
variables (φ ψ : L.bounded_formula α n)

lemma semantically_equivalent_not_not :
  T.semantically_equivalent φ φ.not.not :=
λ M v xs, by simp

lemma imp_semantically_equivalent_not_sup :
  T.semantically_equivalent (φ.imp ψ) (φ.not ⊔ ψ) :=
λ M v xs, by simp [imp_iff_not_or]

lemma sup_semantically_equivalent_not_inf_not :
  T.semantically_equivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not :=
λ M v xs, by simp [imp_iff_not_or]

lemma inf_semantically_equivalent_not_sup_not :
  T.semantically_equivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not :=
λ M v xs, by simp [and_iff_not_or_not]

lemma all_semantically_equivalent_not_ex_not (φ : L.bounded_formula α (n + 1)) :
  T.semantically_equivalent φ.all φ.not.ex.not :=
λ M v xs, by simp

lemma ex_semantically_equivalent_not_all_not (φ : L.bounded_formula α (n + 1)) :
  T.semantically_equivalent φ.ex φ.not.all.not :=
λ M v xs, by simp

lemma semantically_equivalent_all_lift_at :
  T.semantically_equivalent φ (φ.lift_at 1 n).all :=
λ M v xs, by { resetI, rw [realize_iff, realize_all_lift_at_one_self] }

end bounded_formula

namespace formula
variables (φ ψ : L.formula α)

lemma semantically_equivalent_not_not :
  T.semantically_equivalent φ φ.not.not :=
φ.semantically_equivalent_not_not

lemma imp_semantically_equivalent_not_sup :
  T.semantically_equivalent (φ.imp ψ) (φ.not ⊔ ψ) :=
φ.imp_semantically_equivalent_not_sup ψ

lemma sup_semantically_equivalent_not_inf_not :
  T.semantically_equivalent (φ ⊔ ψ) (φ.not ⊓ ψ.not).not :=
φ.sup_semantically_equivalent_not_inf_not ψ

lemma inf_semantically_equivalent_not_sup_not :
  T.semantically_equivalent (φ ⊓ ψ) (φ.not ⊔ ψ.not).not :=
φ.inf_semantically_equivalent_not_sup_not ψ
end formula

namespace bounded_formula

lemma is_qf.induction_on_sup_not {P : L.bounded_formula α n → Prop} {φ : L.bounded_formula α n}
  (h : is_qf φ)
  (hf : P (⊥ : L.bounded_formula α n))
  (ha : ∀ (ψ : L.bounded_formula α n), is_atomic ψ → P ψ)
  (hsup : ∀ {φ₁ φ₂} (h₁ : P φ₁) (h₂ : P φ₂), P (φ₁ ⊔ φ₂))
  (hnot : ∀ {φ} (h : P φ), P φ.not)
  (hse : ∀ {φ₁ φ₂ : L.bounded_formula α n}
    (h : Theory.semantically_equivalent ∅ φ₁ φ₂), P φ₁ ↔ P φ₂) :
  P φ :=
is_qf.rec_on h hf ha (λ φ₁ φ₂ _ _ h1 h2,
  (hse (φ₁.imp_semantically_equivalent_not_sup φ₂)).2 (hsup (hnot h1) h2))

lemma is_qf.induction_on_inf_not {P : L.bounded_formula α n → Prop} {φ : L.bounded_formula α n}
  (h : is_qf φ)
  (hf : P (⊥ : L.bounded_formula α n))
  (ha : ∀ (ψ : L.bounded_formula α n), is_atomic ψ → P ψ)
  (hinf : ∀ {φ₁ φ₂} (h₁ : P φ₁) (h₂ : P φ₂), P (φ₁ ⊓ φ₂))
  (hnot : ∀ {φ} (h : P φ), P φ.not)
  (hse : ∀ {φ₁ φ₂ : L.bounded_formula α n}
    (h : Theory.semantically_equivalent ∅ φ₁ φ₂), P φ₁ ↔ P φ₂) :
  P φ :=
h.induction_on_sup_not hf ha (λ φ₁ φ₂ h1 h2,
  ((hse (φ₁.sup_semantically_equivalent_not_inf_not φ₂)).2 (hnot (hinf (hnot h1) (hnot h2)))))
  (λ _, hnot) (λ _ _, hse)

lemma semantically_equivalent_to_prenex (φ : L.bounded_formula α n) :
  (∅ : L.Theory).semantically_equivalent φ φ.to_prenex :=
λ M v xs, by rw [realize_iff, realize_to_prenex]

lemma induction_on_all_ex {P : Π {m}, L.bounded_formula α m → Prop} (φ : L.bounded_formula α n)
  (hqf : ∀ {m} {ψ : L.bounded_formula α m}, is_qf ψ → P ψ)
  (hall : ∀ {m} {ψ  : L.bounded_formula α (m + 1)} (h : P ψ), P ψ.all)
  (hex : ∀ {m} {φ : L.bounded_formula α (m + 1)} (h : P φ), P φ.ex)
  (hse : ∀ {m} {φ₁ φ₂ : L.bounded_formula α m}
    (h : Theory.semantically_equivalent ∅ φ₁ φ₂), P φ₁ ↔ P φ₂) :
  P φ :=
begin
  suffices h' : ∀ {m} {φ : L.bounded_formula α m}, φ.is_prenex → P φ,
  { exact (hse φ.semantically_equivalent_to_prenex).2 (h' φ.to_prenex_is_prenex) },
  intros m φ hφ,
  induction hφ with _ _ hφ _ _ _ hφ _ _ _ hφ,
  { exact hqf hφ },
  { exact hall hφ, },
  { exact hex hφ, },
end

lemma induction_on_exists_not {P : Π {m}, L.bounded_formula α m → Prop} (φ : L.bounded_formula α n)
  (hqf : ∀ {m} {ψ : L.bounded_formula α m}, is_qf ψ → P ψ)
  (hnot : ∀ {m} {φ : L.bounded_formula α m} (h : P φ), P φ.not)
  (hex : ∀ {m} {φ : L.bounded_formula α (m + 1)} (h : P φ), P φ.ex)
  (hse : ∀ {m} {φ₁ φ₂ : L.bounded_formula α m}
    (h : Theory.semantically_equivalent ∅ φ₁ φ₂), P φ₁ ↔ P φ₂) :
  P φ :=
φ.induction_on_all_ex
  (λ _ _, hqf)
  (λ _ φ hφ, (hse φ.all_semantically_equivalent_not_ex_not).2 (hnot (hex (hnot hφ))))
  (λ _ _, hex) (λ _ _ _, hse)

end bounded_formula
end language
end first_order

namespace cardinal
open first_order first_order.language

variables {L : language.{u v}} (κ : cardinal.{w}) (T : L.Theory)

/-- A theory is `κ`-categorical if all models of size `κ` are isomorphic. -/
def categorical : Prop :=
∀ (M N : T.Model), # M = κ → # N = κ → nonempty (M ≃[L] N)

/-- The Łoś–Vaught Test : a criterion for categorical theories to be complete. -/
lemma categorical.is_complete (h : κ.categorical T)
  (h1 : ℵ₀ ≤ κ)
  (h2 : cardinal.lift.{w} L.card ≤ cardinal.lift.{max u v} κ)
  (hS : T.is_satisfiable)
  (hT : ∀ (M : Theory.Model.{u v max u v} T), infinite M) :
  T.is_complete :=
⟨hS, λ φ, begin
  obtain ⟨N, hN⟩ := Theory.exists_model_card_eq ⟨hS.some, hT hS.some⟩ κ h1 h2,
  rw [Theory.models_sentence_iff, Theory.models_sentence_iff],
  by_contra con,
  push_neg at con,
  obtain ⟨⟨MF, hMF⟩, MT, hMT⟩ := con,
  rw [sentence.realize_not, not_not] at hMT,
  refine hMF _,
  haveI := hT MT,
  haveI := hT MF,
  obtain ⟨NT, MNT, hNT⟩ := exists_elementarily_equivalent_card_eq L MT κ h1 h2,
  obtain ⟨NF, MNF, hNF⟩ := exists_elementarily_equivalent_card_eq L MF κ h1 h2,
  obtain ⟨TF⟩ := h (MNT.to_Model T) (MNF.to_Model T) hNT hNF,
  exact ((MNT.realize_sentence φ).trans
    ((TF.realize_sentence φ).trans (MNF.realize_sentence φ).symm)).1 hMT,
end⟩

theorem empty_Theory_categorical (T : language.empty.Theory) :
  κ.categorical T :=
λ M N hM hN, by rw [empty.nonempty_equiv_iff, hM, hN]

theorem empty_infinite_Theory_is_complete :
  language.empty.infinite_theory.is_complete :=
(empty_Theory_categorical ℵ₀ _).is_complete ℵ₀ _ le_rfl (by simp)
  ⟨Theory.model.bundled ((model_infinite_theory_iff language.empty).2 nat.infinite)⟩
  (λ M, (model_infinite_theory_iff language.empty).1 M.is_model)

end cardinal


/-
Copyright (c) 2015 Jacob Gross. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jacob Gross, Jeremy Avigad

Extended reals.
-/
import data.real
open real eq.ops classical

-- This is a hack, to get around the fact that the top level names are inaccessible when
-- defining these theorems in the ereal namespace. Is there a better way?
private definition zero_mul' := @zero_mul
private definition mul_zero' := @mul_zero
private definition neg_neg'  := @neg_neg

noncomputable theory

inductive ereal : Type :=
| of_real : ℝ → ereal
| infty : ereal
| neginfty : ereal

attribute ereal.of_real [coercion]
notation `∞` := ereal.infty
notation `-∞` := ereal.neginfty

namespace ereal

protected definition prio := num.pred real.prio

/- arithmetic operations on the ereals -/

definition ereal_has_zero [instance] [priority ereal.prio] : has_zero ereal :=
has_zero.mk (of_real 0)

definition ereal_has_one [instance] [priority ereal.prio] : has_one ereal :=
has_one.mk (of_real 1)

protected definition add : ereal → ereal → ereal
| (of_real x) (of_real y) := of_real (x + y)
| ∞ _                     := ∞
| _ ∞                     := ∞
| -∞ _                    := -∞
| _ -∞                    := -∞

protected definition neg : ereal → ereal
| (of_real x) := of_real (-x)
| ∞           := -∞
| -∞          := ∞

private definition blow_up [reducible] : ereal → ereal
| (of_real x) := if x = 0 then of_real 0 else if x > 0 then ∞ else -∞
| ∞           := ∞
| -∞          := -∞

protected definition mul : ereal → ereal → ereal
| (of_real x) (of_real y) := of_real (x * y)
| ∞ a                     := blow_up a
| a ∞                     := blow_up a
| -∞ a                    := ereal.neg (blow_up a)
| a -∞                    := ereal.neg (blow_up a)

definition ereal_has_add [instance] [priority ereal.prio] : has_add ereal :=
has_add.mk ereal.add

definition ereal_has_neg [instance] [priority ereal.prio] : has_neg ereal :=
has_neg.mk ereal.neg

protected definition sub (u v : ereal) : ereal := u + -v

definition ereal_has_sub [instance] [priority ereal.prio] : has_sub ereal :=
has_sub.mk ereal.sub

definition ereal_has_mul [instance] [priority ereal.prio] : has_mul ereal :=
has_mul.mk ereal.mul

protected theorem zero_def : (0 : ereal) = of_real 0 := rfl

protected theorem one_def : (1 : ereal) = of_real 1 := rfl

protected theorem add_def (x y : ereal) : x + y = ereal.add x y := rfl

protected theorem neg_def (x : ereal) : -x = ereal.neg x := rfl

protected theorem sub_eq_add_neg (u v : ereal) : u - v = u + -v := rfl

protected theorem mul_def (x y : ereal) : x * y = ereal.mul x y := rfl

theorem of_real.inj {x y : real} (H : of_real x = of_real y) : x = y :=
ereal.no_confusion H (assume H1, H1)

abbreviation eq_of_of_real_eq_of_real := @of_real.inj

theorem of_real_add (x y : real) : of_real (x + y) = of_real x + of_real y := rfl

theorem of_real_mul (x y : real) : of_real (x * y) = of_real x * of_real y := rfl

theorem infty_ne_neg_infty : ∞ ≠ -∞ := ereal.no_confusion

theorem infty_ne_of_real (x : real) : ∞ ≠ of_real x := ereal.no_confusion

theorem neg_infty_ne_of_real (x : real) : -∞ ≠ of_real x := ereal.no_confusion

/- properties of the arithmetic operations -/

protected theorem add_comm : ∀ u v : ereal, u + v = v + u
| (of_real x) (of_real y) := congr_arg of_real !add.comm
| ∞ v                     := by rewrite[*ereal.add_def, ↑ereal.add]
| u ∞                     := by rewrite[*ereal.add_def, ↑ereal.add]
| -∞ v                    := by rewrite[*ereal.add_def, ↑ereal.add]
| u -∞                    := by rewrite[*ereal.add_def, ↑ereal.add]

theorem infty_add : ∀ u, ∞ + u = ∞
| (of_real x) := rfl
| ∞           := rfl
| -∞          := rfl

theorem add_infty : ∀ u, u + ∞ = ∞
| (of_real x) := rfl
| ∞           := rfl
| -∞          := rfl

protected theorem add_assoc : ∀ u v w : ereal, (u + v) + w = u + (v + w)
| (of_real x) (of_real y) (of_real z) := congr_arg of_real !add.assoc
| ∞ v w                               := by rewrite [*infty_add, *add_infty]
| u ∞ w                               := by rewrite [*infty_add, *add_infty, infty_add]
| u v ∞                               := by rewrite [*infty_add, *add_infty]
| (of_real x) (of_real y) -∞          := by rewrite[*ereal.add_def, ↑ereal.add]
| (of_real x) -∞ (of_real z)          := by rewrite[*ereal.add_def, ↑ereal.add]
| -∞ (of_real y) (of_real z)          := by rewrite[*ereal.add_def, ↑ereal.add]
| (of_real x) -∞ -∞                   := by rewrite[*ereal.add_def, ↑ereal.add]
| -∞ (of_real y) -∞                   := rfl
| -∞ -∞ (of_real z)                   := by rewrite[*ereal.add_def, ↑ereal.add]
| -∞ -∞ -∞                            := rfl

protected theorem zero_add : ∀ u : ereal, 0 + u = u
| (of_real x) := congr_arg of_real !real.zero_add
| ∞           := rfl
| -∞          := rfl

protected theorem add_zero : ∀ u : ereal, u + 0 = u :=
by intro u; rewrite [ereal.add_comm, ereal.zero_add]

protected theorem mul_comm : ∀ u v : ereal, u * v = v * u
| (of_real x) (of_real y) := congr_arg of_real !mul.comm
| ∞ a                     := by rewrite [*ereal.mul_def, ↑ereal.mul]
| a ∞                     := by rewrite [*ereal.mul_def, ↑ereal.mul]
| -∞ a                    := by rewrite [*ereal.mul_def, ↑ereal.mul]
| a -∞                    := by rewrite [*ereal.mul_def, ↑ereal.mul]

protected theorem neg_neg : ∀ u : ereal, -(-u) = u
| ∞           := rfl
| (of_real x) := by rewrite [*ereal.neg_def, ↑ereal.neg, ▸*,
                             (neg_neg' x)]
| -∞          := rfl

theorem neg_infty : -∞ = - ∞  := rfl

protected theorem neg_zero : -(0 : ereal) = 0 := rfl

theorem infty_mul_pos {x : real} (H : x > 0) : ∞ * x = ∞ :=
have H1 : x ≠ 0, from ne_of_gt H,
by rewrite [*ereal.mul_def, ↑ereal.mul, if_neg H1, if_pos H]

theorem pos_mul_infty {x : real} (H : x > 0) : x * ∞ = ∞ :=
by rewrite [ereal.mul_comm, infty_mul_pos H]

theorem infty_mul_neg {x : real} (H : x < 0) : ∞ * x = -∞ :=
have H1 : x ≠ 0, from ne_of_lt H,
have H2 : ¬ x > 0, from not_lt_of_gt H,
by rewrite [*ereal.mul_def, ↑ereal.mul, if_neg H1, if_neg H2]

theorem neg_mul_infty {x : real} (H : x < 0) : x * ∞ = -∞ :=
by rewrite [ereal.mul_comm, infty_mul_neg H]

private theorem infty_mul_zero : ∞ * 0 = 0 :=
by rewrite [*ereal.mul_def, ↑ereal.mul, ereal.zero_def, ↑blow_up, if_pos rfl]

private theorem zero_mul_infty : 0 * ∞ = 0 :=
by rewrite [ereal.mul_comm, infty_mul_zero]

theorem infty_mul_infty : ∞ * ∞ = ∞ := rfl

protected theorem neg_of_real (x : real) : -(of_real x) = of_real (-x) :=
rfl

private theorem aux1 : ∀ v : ereal, -∞ * v = -(∞ * v)
| ∞           := rfl
| (of_real x) := rfl
| -∞          := rfl

private theorem aux2 : ∀ u : ereal, -u * ∞ = -(u * ∞)
| ∞ := rfl
| (of_real x) := lt.by_cases
                   (assume H : x < 0,
                      by rewrite [ereal.neg_of_real, pos_mul_infty (neg_pos_of_neg H),
                                  neg_mul_infty H])
                   (assume H : x = 0,
                      by krewrite [H, ereal.neg_zero, *zero_mul_infty, ereal.neg_zero])
                   (assume H : x > 0,
                      by rewrite [ereal.neg_of_real, neg_mul_infty (neg_neg_of_pos H),
                                   pos_mul_infty H])
| -∞ := rfl

theorem ereal_neg_mul : ∀ u v : ereal, -u * v = -(u * v)
| ∞ v                     := aux1 v
| -∞ v                    := by rewrite [aux1, *ereal.neg_neg]
| u ∞                     := by rewrite [-aux2]
| u -∞                    := by rewrite [ereal.mul_comm, ereal.mul_comm u,
                                         *aux1, ereal.mul_comm, aux2, *ereal.neg_neg]
| (of_real x) (of_real y) := congr_arg of_real (eq.symm (neg_mul_eq_neg_mul x y))

theorem ereal_mul_neg (u v : ereal) : u * -v = -(u * v) :=
by rewrite [*ereal.mul_comm u, ereal_neg_mul]

protected theorem mul_zero : ∀ u : ereal, u * 0 = 0
| ∞ := infty_mul_zero
| -∞ := by rewrite [neg_infty, ereal_neg_mul, infty_mul_zero]
| (of_real x) := congr_arg of_real (mul_zero' x)

protected theorem zero_mul (u : ereal) : 0 * u = 0 :=
by rewrite [ereal.mul_comm, ereal.mul_zero]

private theorem aux3 : ∀ u, ∞ * (∞ * u) = ∞ * u
| ∞           := rfl
| (of_real x) := if H : x = 0 then
                   by rewrite [*ereal.mul_def, ↑ereal.mul, ↑blow_up, *H, *if_pos rfl]
                 else if H1 : x > 0 then
                   by rewrite [*ereal.mul_def, ↑ereal.mul, ↑blow_up, if_neg H, if_pos H1]
                 else
                   by rewrite [*ereal.mul_def, ↑ereal.mul, ↑blow_up, if_neg H, if_neg H1]
| -∞          := rfl

private theorem aux4 (x y : real) : ∞ * x * y = ∞ * (x * y) :=
lt.by_cases
  (assume H : x < 0,
    lt.by_cases
      (assume H1 : y < 0, by rewrite [infty_mul_neg H, neg_infty, ereal_neg_mul, -of_real_mul,
                                     infty_mul_neg H1, infty_mul_pos (mul_pos_of_neg_of_neg H H1)])
      (assume H1 : y = 0, by krewrite [H1, *ereal.mul_zero])
      (assume H1 : y > 0, by rewrite [infty_mul_neg H, neg_infty, *ereal_neg_mul, -of_real_mul,
                                     infty_mul_pos H1, infty_mul_neg (mul_neg_of_neg_of_pos H H1)]))
  (assume H : x = 0,
    by krewrite [H, ereal.mul_zero, *ereal.zero_mul, ereal.mul_zero])
  (assume H : x > 0,
    lt.by_cases
      (assume H1 : y < 0, by rewrite [infty_mul_pos H, infty_mul_neg H1, -of_real_mul,
                                     infty_mul_neg (mul_neg_of_pos_of_neg H H1)])
      (assume H1 : y = 0, by krewrite [H1, *ereal.mul_zero])
      (assume H1 : y > 0, by rewrite [infty_mul_pos H, infty_mul_pos H1, -of_real_mul,
                                     infty_mul_pos (mul_pos H H1)]))

private theorem aux5 : ∀ u v, ∞ * u * v = ∞ * (u * v)
| ∞ v  := by rewrite [infty_mul_infty, aux3]
| u ∞  := by rewrite [-*ereal.mul_comm ∞]
| -∞ v := by rewrite [neg_infty, *ereal_neg_mul, *ereal_mul_neg, ereal_neg_mul, infty_mul_infty,
                      aux3]
| u -∞ := by rewrite [neg_infty, *ereal_mul_neg]
| (of_real x) (of_real y) := aux4 x y

protected theorem mul_assoc : ∀ u v w : ereal, u * v * w = u * (v * w)
| ∞ v w  := !aux5
| u ∞ w  := by rewrite [-*ereal.mul_comm ∞, *ereal.mul_comm u, *aux5, *ereal.mul_comm u]
| u v ∞  := by rewrite [-*ereal.mul_comm ∞, *ereal.mul_comm u, aux5]
| -∞ v w := by rewrite [neg_infty, *ereal_neg_mul, aux5]
| u -∞ w := by rewrite [neg_infty, *ereal_mul_neg, *ereal_neg_mul, ereal_mul_neg, *ereal.mul_comm u,
                        *aux5, ereal.mul_comm u]
| u v -∞ := by rewrite [neg_infty, *ereal_mul_neg, *ereal.mul_comm u, -*ereal.mul_comm ∞, aux5]
| (of_real x) (of_real y) (of_real z) := congr_arg of_real (mul.assoc x y z)

protected theorem one_mul : ∀ u : ereal, of_real 1 * u = u
| (of_real x) := !real.one_mul ▸ rfl
| ∞           := pos_mul_infty zero_lt_one
| -∞          := by rewrite [neg_infty, ereal_mul_neg, pos_mul_infty zero_lt_one]

protected theorem mul_one (u : ereal) : u * 1 = u :=
by krewrite [ereal.mul_comm, ereal.one_mul]

/- instantiating arithmetic structures -/

-- Note that distributivity fails, e.g. ∞ ⬝ (-1 + 1) ≠ ∞ * -1 + ∞ * 1

protected definition comm_monoid [trans_instance] : comm_monoid ereal :=
⦃comm_monoid,
  mul       := ereal.mul,
  mul_assoc := ereal.mul_assoc,
  one       := 1,
  one_mul   := ereal.one_mul,
  mul_one   := ereal.mul_one,
  mul_comm  := ereal.mul_comm
⦄

protected definition add_comm_monoid [trans_instance] : add_comm_monoid ereal :=
⦃add_comm_monoid,
  add       := ereal.add,
  add_assoc := ereal.add_assoc,
  zero      := 0,
  zero_add  := ereal.zero_add,
  add_zero  := ereal.add_zero,
  add_comm  := ereal.add_comm
⦄

/- ordering on the ereals -/

protected definition le : ereal → ereal → Prop
| u ∞                     := true
| -∞ v                    := true
| (of_real x) (of_real y) := x ≤ y
| (of_real x) -∞          := false
| ∞ (of_real y)           := false
| ∞ -∞                    := false

definition ereal_has_le [instance] [priority ereal.prio] : has_le ereal :=
has_le.mk ereal.le

theorem of_real_le_of_real (x y : real) : of_real x ≤ of_real y ↔ x ≤ y :=
!iff.refl

theorem le_infty : ∀ u, u ≤ ∞
| ∞           := trivial
| (of_real x) := trivial
| -∞          := trivial

theorem neg_infty_le : ∀ v, -∞ ≤ v
| ∞           := trivial
| (of_real x) := trivial
| -∞          := trivial

protected theorem le_refl : ∀ u : ereal, u ≤ u
| ∞           := trivial
| -∞          := trivial
| (of_real x) := by rewrite [of_real_le_of_real]

protected theorem le_trans : ∀ u v w : ereal, u ≤ v → v ≤ w → u ≤ w
| u v ∞            H1 H2 := !le_infty
| -∞ v w           H1 H2 := !neg_infty_le
| u ∞ (of_real x)  H1 H2 := false.elim H2
| ∞ (of_real x) v  H1 H2 := false.elim H1
| ∞ -∞ v           H1 H2 := false.elim H1
| u (of_real x) -∞ H1 H2 := false.elim H2
| u ∞ -∞           H1 H2 := false.elim H2
| (of_real x) -∞ v H1 H2 := false.elim H1
| (of_real x) (of_real y) (of_real z) H1 H2 :=
    iff.mpr !of_real_le_of_real
      (le.trans (iff.mp !of_real_le_of_real H1) (iff.mp !of_real_le_of_real H2))

protected theorem le_antisymm : ∀ u v : ereal, u ≤ v → v ≤ u → u = v
| ∞ ∞            H1 H2 := rfl
| ∞ (of_real x)  H1 H2 := false.elim H1
| ∞ -∞           H1 H2 := false.elim H1
| -∞ -∞          H1 H2 := rfl
| -∞ (of_real x) H1 H2 := false.elim H2
| -∞ ∞           H1 H2 := false.elim H2
| (of_real x) ∞  H1 H2 := false.elim H2
| (of_real x) -∞ H1 H2 := false.elim H1
| (of_real x) (of_real y) H1 H2 :=
    congr_arg of_real (le.antisymm (iff.mp !of_real_le_of_real H1) (iff.mp !of_real_le_of_real H2))

protected definition lt (x y : ereal) : Prop := x ≤ y ∧ x ≠ y

definition ereal_has_lt [instance] [priority ereal.prio] :
  has_lt ereal :=
has_lt.mk ereal.lt

protected theorem le_iff_lt_or_eq (u v : ereal) : u ≤ v ↔ u < v ∨ u = v :=
iff.intro
  (assume H : u ≤ v,
    by_cases
      (assume H1 : u = v, or.inr H1)
      (assume H1 : u ≠ v, or.inl (and.intro H H1)))
  (assume H : u < v ∨ u = v,
    or.elim H
      (assume H1 : u < v, and.left H1)
      (assume H1 : u = v, by rewrite H1; apply ereal.le_refl))

protected theorem le_total : ∀ u v : ereal, u ≤ v ∨ v ≤ u
| u ∞  := or.inl (le_infty u)
| u -∞ := or.inr (neg_infty_le u)
| ∞ v  := or.inr (le_infty v)
| -∞ v := or.inl (neg_infty_le v)
| (of_real x) (of_real y) :=
    or.elim (le.total x y)
      (assume H : x ≤[real] y, or.inl (iff.mpr !of_real_le_of_real H))
      (assume H : x ≥[real] y, or.inr (iff.mpr !of_real_le_of_real H))

theorem neg_infty_lt_infty : -∞ < ∞ := and.intro trivial (ne.symm infty_ne_neg_infty)

theorem neg_infty_lt_of_real (x : real) : -∞ < of_real x :=  and.intro trivial !neg_infty_ne_of_real

theorem of_real_lt_infty (x : real) : of_real x < ∞ := and.intro trivial (ne.symm !infty_ne_of_real)

protected definition decidable_linear_order [trans_instance] : decidable_linear_order ereal :=
⦃decidable_linear_order,
  le              := ereal.le,
  le_refl         := ereal.le_refl,
  le_trans        := ereal.le_trans,
  le_antisymm     := ereal.le_antisymm,
  lt              := ereal.lt,
  le_iff_lt_or_eq := ereal.le_iff_lt_or_eq,
  lt_irrefl       := abstract λ u H, and.right H rfl end,
  decidable_lt    := abstract λ u v : ereal, prop_decidable (u < v) end,
  le_total        := ereal.le_total
⦄

-- TODO : we still need some properties relating the arithmetic operations and the order.

end ereal