text:
import category_theory.sites.limits

import for_mathlib.abelian_sheaves.functor_category
import for_mathlib.sheaf
import category_theory.sites.left_exact

namespace category_theory
namespace Sheaf

noncomputable theory

universes w v u
variables {C : Type (max v u)} [category.{v} C] {J : grothendieck_topology C}
variables {A : Type w} [category.{max v u} A]

section has_zero_morphisms

variables [limits.has_zero_morphisms A]

instance : limits.has_zero_morphisms (Sheaf J A) :=
{ has_zero := λ X Y, ⟨⟨0⟩⟩,
  comp_zero' := λ X Y f Z, Sheaf.hom.ext _ _ $ limits.comp_zero,
  zero_comp' := λ X Y Z f, Sheaf.hom.ext _ _ $ limits.zero_comp }

end has_zero_morphisms

section parallel_pair

def parallel_pair_iso {F G : Sheaf J A} (η γ : F ⟶ G) :
  limits.parallel_pair η γ ⋙ Sheaf_to_presheaf J A ≅ limits.parallel_pair η.val γ.val :=
nat_iso.of_components
(λ x,
match x with
| limits.walking_parallel_pair.zero := eq_to_iso rfl
| limits.walking_parallel_pair.one := eq_to_iso rfl
end) begin
  rintro (x|x) (y|y) (f|f|f),
  any_goals { refl },
  any_goals { ext, dsimp [parallel_pair_iso._match_1], simp },
end

end parallel_pair

section kernels

--variables [limits.has_zero_morphisms A]
-- TODO: Add some instances that derive the following from `[has_kernels A]`.
--variables [limits.has_limits_of_shape limits.walking_parallel_pair A]
variables [limits.has_finite_limits A]

instance has_finite_limits : limits.has_finite_limits (Sheaf J A) :=
begin
  apply limits.has_finite_limits_of_has_finite_limits_of_size.{max v u},
  introsI K _ _,
  apply_instance,
end

instance preserves_finite_limits : limits.preserves_finite_limits (Sheaf_to_presheaf J A) :=
begin
  apply limits.preserves_finite_limits_of_preserves_finite_limits_of_size.{max v u},
  introsI K _ _,
  apply_instance,
end

variables [limits.has_zero_morphisms A]

def kernel_iso {F G : Sheaf J A} (η : F ⟶ G) :
  (Sheaf_to_presheaf J A).obj (limits.kernel η) ≅
  limits.kernel ((Sheaf_to_presheaf J A).map η) :=
limits.preserves_kernel.iso (Sheaf_to_presheaf J A) η

def kernel_sheaf {F G : Sheaf J A} (η : F ⟶ G) : Sheaf J A :=
{ val := limits.kernel.{(max v u)} ((Sheaf_to_presheaf J A).map η),
  cond := begin
    apply presheaf.is_sheaf_of_iso J (kernel_iso η).symm,
    exact Sheaf.cond _,
  end }

def kernel_ι {F G : Sheaf J A} (η : F ⟶ G) : kernel_sheaf η ⟶ F :=
⟨limits.kernel.ι _⟩

def kernel_fork {F G : Sheaf J A} (η : F ⟶ G) : limits.fork η 0 :=
limits.fork.of_ι (kernel_ι η) $
by { simp only [limits.comp_zero], ext1, apply limits.kernel.condition }

def is_limit_kernel_fork {F G : Sheaf J A} (η : F ⟶ G) : limits.is_limit (kernel_fork η) :=
limits.is_limit_aux _ (λ S, ⟨limits.kernel.lift _ S.ι.val $ congr_arg Sheaf.hom.val S.condition⟩)
(by { intros S, ext1, apply limits.kernel.lift_ι, })
begin
  intros S m hm,
  ext : 2,
  simp only [limits.kernel.lift_ι],
  exact congr_arg Sheaf.hom.val hm,
end

-- Sanity check
example : limits.has_kernels (Sheaf J A) := by apply_instance

def kernel_iso_kernel_sheaf {F G : Sheaf J A} (η : F ⟶ G) :
  limits.kernel η ≅ kernel_sheaf η :=
(limits.limit.is_limit _).cone_point_unique_up_to_iso (is_limit_kernel_fork _)

@[simp, reassoc]
lemma kernel_iso_kernel_sheaf_hom_ι {F G : Sheaf J A} (η : F ⟶ G) :
  (kernel_iso_kernel_sheaf η).hom ≫ kernel_ι η = limits.kernel.ι _ :=
((limits.limit.is_limit _).unique_up_to_iso (is_limit_kernel_fork η)).hom.w
  limits.walking_parallel_pair.zero

@[simp, reassoc]
lemma kernel_iso_kernel_sheaf_hom_ι_val {F G : Sheaf J A} (η : F ⟶ G) :
  (kernel_iso_kernel_sheaf η).hom.val ≫ (kernel_ι η).val = (limits.kernel.ι η).val :=
begin
  change ((kernel_iso_kernel_sheaf η).hom ≫ (kernel_ι η)).val = (limits.kernel.ι η).val,
  simp,
end

@[simp, reassoc]
lemma kernel_iso_kernel_sheaf_inv_ι {F G : Sheaf J A} (η : F ⟶ G) :
  (kernel_iso_kernel_sheaf η).inv ≫ limits.kernel.ι _ = kernel_ι η :=
by simp only [← kernel_iso_kernel_sheaf_hom_ι, iso.inv_hom_id_assoc]

@[simp, reassoc]
lemma kernel_iso_kernel_sheaf_inv_ι_val {F G : Sheaf J A} (η : F ⟶ G) :
  (kernel_iso_kernel_sheaf η).inv.val ≫ (limits.kernel.ι η).val = (kernel_ι η).val :=
begin
  change ((kernel_iso_kernel_sheaf η).inv ≫ (limits.kernel.ι η)).val = (kernel_ι η).val,
  simp,
end

end kernels

section cokernels

--variables [limits.has_zero_morphisms A]
-- TODO: Add some instances that derive the following from `[has_cokernels A]`.
--variables [limits.has_colimits_of_shape.{_ (max v u)} limits.walking_parallel_pair A]
variables [limits.has_finite_colimits A]

-- We will need to sheafify....
variables [concrete_category.{max v u} A]
variables [∀ (P : Cᵒᵖ ⥤ A) (X : C) (S : J.cover X), limits.has_multiequalizer (S.index P)]
variables [limits.preserves_limits (forget A)]
variables [∀ (X : C), limits.has_colimits_of_shape (J.cover X)ᵒᵖ A]
variables [∀ (X : C), limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (forget A)]
variables [reflects_isomorphisms (forget A)]

instance has_finite_colimits : limits.has_finite_colimits (Sheaf J A) :=
begin
  apply limits.has_finite_colimits_of_has_finite_colimits_of_size.{max v u},
  introsI K _ _,
  apply_instance,
end

variables [limits.has_zero_morphisms A]

def cokernel_sheaf {F G : Sheaf J A} (η : F ⟶ G) : Sheaf J A :=
{ val := J.sheafify (limits.cokernel ((Sheaf_to_presheaf J A).map η)), -- ;-)
  cond := grothendieck_topology.plus.is_sheaf_plus_plus _ _ }

def cokernel_π {F G : Sheaf J A} (η : F ⟶ G) : G ⟶ cokernel_sheaf η :=
⟨show (Sheaf_to_presheaf J A).obj G ⟶ J.sheafify (limits.cokernel ((Sheaf_to_presheaf J A).map η)),
from limits.cokernel.π ((Sheaf_to_presheaf J A).map η) ≫
  J.to_sheafify (limits.cokernel ((Sheaf_to_presheaf J A).map η))⟩

def cokernel_cofork {F G : Sheaf J A} (η : F ⟶ G) : limits.cofork η 0 :=
limits.cofork.of_π (cokernel_π η) begin
  ext1,
  rw [limits.zero_comp],
  dsimp only [cokernel_π],
  show η.val ≫ _ = 0,
  erw [← category.assoc, limits.cokernel.condition, limits.zero_comp],
end

def is_colimit_cokernel_cofork {F G : Sheaf J A} (η : F ⟶ G) :
  limits.is_colimit (cokernel_cofork η) :=
limits.is_colimit_aux _ (λ S,
  ⟨J.sheafify_lift
    (limits.cokernel.desc ((Sheaf_to_presheaf J A).map η) S.π.val $
      congr_arg Sheaf.hom.val S.condition)
    (S.X.2)⟩)
begin
  intros S, ext1,
  change (_ ≫ _) ≫ _ = _,
  rw [category.assoc, J.to_sheafify_sheafify_lift, limits.cokernel.π_desc],
end begin
  intros S m hm, ext1,
  apply J.sheafify_lift_unique,
  rw Sheaf.hom.ext_iff at hm,
  change (_ ≫ _) ≫ _ = _ at hm,
  rw category.assoc at hm,
  ext1,
  rw [hm, limits.cokernel.π_desc],
end

-- Sanity check
example : limits.has_cokernels (Sheaf J A) := by apply_instance

def cokernel_iso_cokernel_sheaf {F G : Sheaf J A} (η : F ⟶ G) :
  limits.cokernel η ≅ cokernel_sheaf η :=
(limits.colimit.is_colimit _).cocone_point_unique_up_to_iso (is_colimit_cokernel_cofork _)

@[simp]
lemma cokernel_iso_cokernel_sheaf_hom_π {F G : Sheaf J A} (η : F ⟶ G) :
  limits.cokernel.π η ≫ (cokernel_iso_cokernel_sheaf η).hom = cokernel_π _ :=
((limits.colimit.is_colimit _).unique_up_to_iso (is_colimit_cokernel_cofork η)).hom.w
  limits.walking_parallel_pair.one

@[simp]
lemma cokernel_iso_cokernel_sheaf_inv_π {F G : Sheaf J A} (η : F ⟶ G) :
  cokernel_π η ≫ (cokernel_iso_cokernel_sheaf η).inv = limits.cokernel.π η :=
by simp only [← cokernel_iso_cokernel_sheaf_hom_π,
  category.assoc, iso.hom_inv_id, category.comp_id]

end cokernels

section kernels_and_cokernels

-- TODO: use has kernels and cokernels, when possible... see above
--variables [limits.has_colimits_of_shape.{_ (max v u)} limits.walking_parallel_pair A]
--variables [limits.has_limits_of_shape.{_ (max v u)} limits.walking_parallel_pair A]
variables [limits.has_zero_morphisms A] [limits.has_finite_limits A] [limits.has_finite_colimits A]

-- We will need to sheafify....
variables [concrete_category.{max v u} A]
variables [∀ (P : Cᵒᵖ ⥤ A) (X : C) (S : J.cover X), limits.has_multiequalizer (S.index P)]
variables [limits.preserves_limits (forget A)]
variables [∀ (X : C), limits.has_colimits_of_shape (J.cover X)ᵒᵖ A]
variables [∀ (X : C), limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (forget A)]
variables [reflects_isomorphisms (forget A)]

def coim_to_im'_aux {F G : Sheaf J A} (η : F ⟶ G) :
  abelian.coimage ((Sheaf_to_presheaf J A).map η) ⟶
    (Sheaf_to_presheaf J A).obj (kernel_sheaf (cokernel_π η)) :=
(abelian.coimage_image_comparison _ ≫ limits.kernel.lift _ (limits.kernel.ι _) begin
  dsimp [cokernel_π],
  rw [← category.assoc, limits.kernel.condition],
  simp only [limits.zero_comp],
end)

def coim_to_im' {F G : Sheaf J A} (η : F ⟶ G) :
  cokernel_sheaf (kernel_ι η) ⟶ kernel_sheaf (cokernel_π η) :=
⟨J.sheafify_lift (coim_to_im'_aux η) (kernel_sheaf _).2⟩

def kernel_sheaf_cokernel_π_iso {F G : Sheaf J A} (η : F ⟶ G) :
  kernel_sheaf (limits.cokernel.π η) ≅ kernel_sheaf (cokernel_π η) :=
{ hom := ⟨limits.kernel.map _ _ (𝟙 _)
    ((Sheaf_to_presheaf J A).map (cokernel_iso_cokernel_sheaf η).hom) begin
      rw ← functor.map_comp,
      dsimp [cokernel_iso_cokernel_sheaf, limits.is_colimit.cocone_point_unique_up_to_iso,
        cokernel_cofork],
      show Sheaf.hom.val (limits.cokernel.π η ≫ _) = _,
      simp only [limits.coequalizer.π_desc, category.id_comp],
    end⟩,
  inv := ⟨limits.kernel.map _ _ (𝟙 _)
    ((Sheaf_to_presheaf J A).map (cokernel_iso_cokernel_sheaf η).inv) begin
      rw ← functor.map_comp,
      dsimp [cokernel_iso_cokernel_sheaf, limits.is_colimit.cocone_point_unique_up_to_iso,
        cokernel_π, is_colimit_cokernel_cofork, limits.is_colimit_aux],
      erw [category.id_comp, category.assoc, J.to_sheafify_sheafify_lift,
        limits.cokernel.π_desc],
    end⟩,
  hom_inv_id' := begin
    ext : 2,
    delta limits.kernel.map,
    dsimp,
    erw [category.assoc, limits.kernel.lift_ι, ← category.assoc, limits.kernel.lift_ι,
      category.comp_id, category.comp_id, category.id_comp],
  end,
  inv_hom_id' := begin
    ext : 2,
    delta limits.kernel.map,
    dsimp,
    erw [category.assoc, limits.kernel.lift_ι, ← category.assoc, limits.kernel.lift_ι,
      category.comp_id, category.comp_id, category.id_comp],
  end }

def cokernel_sheaf_kernel_ι_iso {F G : Sheaf J A} (η : F ⟶ G) :
  cokernel_sheaf (limits.kernel.ι η) ≅ cokernel_sheaf (kernel_ι η) :=
{ hom := ⟨J.sheafify_lift
    (limits.cokernel.map _ _ ((Sheaf_to_presheaf J A).map (kernel_iso_kernel_sheaf η).hom) (𝟙 _)
      (by rw [category.comp_id, ← functor.map_comp, kernel_iso_kernel_sheaf_hom_ι])
      ≫ J.to_sheafify _) (cokernel_sheaf _).2⟩,
  inv := ⟨J.sheafify_lift
    (limits.cokernel.map _ _ ((Sheaf_to_presheaf J A).map (kernel_iso_kernel_sheaf η).inv) (𝟙 _)
      (by rw [category.comp_id, ← functor.map_comp, kernel_iso_kernel_sheaf_inv_ι])
      ≫ J.to_sheafify _)
    (cokernel_sheaf _).2⟩,
  hom_inv_id' := begin
    ext1,
    apply J.sheafify_hom_ext _ _ (cokernel_sheaf _).2,
    erw [← category.assoc, J.to_sheafify_sheafify_lift, category.assoc,
      J.to_sheafify_sheafify_lift, ← category.assoc],
    conv_rhs { erw category.comp_id },
    convert category.id_comp _,
    ext1,
    delta limits.cokernel.map,
    erw [← category.assoc, limits.coequalizer.π_desc, category.id_comp,
      limits.coequalizer.π_desc, category.id_comp, category.comp_id],
  end,
  inv_hom_id' := begin
    ext1,
    apply J.sheafify_hom_ext _ _ (cokernel_sheaf _).2,
    erw [← category.assoc, J.to_sheafify_sheafify_lift, category.assoc,
      J.to_sheafify_sheafify_lift, ← category.assoc],
    conv_rhs { erw category.comp_id },
    convert category.id_comp _,
    ext1,
    delta limits.cokernel.map,
    erw [← category.assoc, limits.coequalizer.π_desc, category.id_comp,
      limits.coequalizer.π_desc, category.id_comp, category.comp_id],
  end }

lemma eq_coim_to_im' {F G : Sheaf J A} (η : F ⟶ G) :
  (cokernel_sheaf_kernel_ι_iso η).inv ≫
  (cokernel_iso_cokernel_sheaf _).inv ≫
  abelian.coimage_image_comparison η  ≫
  (kernel_iso_kernel_sheaf _).hom ≫
  (kernel_sheaf_cokernel_π_iso η).hom
  = coim_to_im' η :=
begin
  dsimp [abelian.coimage_image_comparison, cokernel_sheaf_kernel_ι_iso,
    coim_to_im', coim_to_im'_aux, kernel_sheaf_cokernel_π_iso,
    limits.is_colimit.cocone_point_unique_up_to_iso,
    limits.is_limit.cone_point_unique_up_to_iso],
  delta limits.kernel.map limits.cokernel.map,
  ext1,
  apply J.sheafify_lift_unique,
  ext : 2,
  conv_rhs {
    erw [← category.assoc, limits.cokernel.π_desc,
      category.assoc, limits.kernel.lift_ι, limits.kernel.lift_ι] },
  dsimp,
  simp only [category.assoc, category.comp_id, category.id_comp,
    J.to_sheafify_sheafify_lift_assoc, kernel_iso_kernel_sheaf_hom_ι_val,
      limits.kernel.lift_ι, limits.cokernel.π_desc_assoc],
  dsimp [cokernel_iso_cokernel_sheaf, limits.is_colimit.cocone_point_unique_up_to_iso,
    is_colimit_cokernel_cofork, limits.is_colimit_aux],
  rw J.to_sheafify_sheafify_lift_assoc,
  simp only [limits.cokernel.π_desc_assoc, ← category.assoc, ← Sheaf.hom.comp_val,
    limits.cokernel.π_desc],
  simp only [category_theory.category_comp_val, category.assoc],
  erw kernel_iso_kernel_sheaf_hom_ι_val,
  rw [← Sheaf.hom.comp_val, limits.kernel.lift_ι],
end

lemma coim_to_im_eq {F G : Sheaf J A} (η : F ⟶ G) :
  abelian.coimage_image_comparison η =
  (cokernel_iso_cokernel_sheaf _).hom ≫
  (cokernel_sheaf_kernel_ι_iso η).hom ≫
  coim_to_im' η ≫
  (kernel_sheaf_cokernel_π_iso η).inv ≫
  (kernel_iso_kernel_sheaf _).inv
  :=
begin
  rw ← eq_coim_to_im',
  simp only [category.assoc, iso.hom_inv_id, iso.inv_hom_id,
    iso.hom_inv_id_assoc, iso.inv_hom_id_assoc, category.comp_id],
end

end kernels_and_cokernels

section preadditive

variable [preadditive A]

/-
instance : preadditive (Sheaf J A) :=
{ hom_group := λ P Q,
  { add := λ f g, ⟨f.val + g.val⟩,
    add_assoc := by { intros, ext1, apply add_assoc },
    zero := ⟨0⟩,
    zero_add := by { intros, ext1, apply zero_add },
    add_zero := by { intros, ext1, apply add_zero },
    nsmul := λ n f, ⟨n • f.val⟩,
    nsmul_zero' := by { intros, ext1, simpa },
    nsmul_succ' := by { intros, ext1, simpa },
    neg := λ f, ⟨-f.val⟩,
    sub := λ f g, ⟨f.val - g.val⟩,
    sub_eq_add_neg := by { intros, ext1, apply sub_eq_add_neg },
    zsmul := λ n f, ⟨n • f.val⟩,
    zsmul_zero' := by { intros, ext1, simpa },
    zsmul_succ' := by { intros, ext1, simpa },
    zsmul_neg' := by { intros, ext1, simpa },
    add_left_neg := by { intros, ext1, apply add_left_neg },
    add_comm := by { intros, ext1, apply add_comm } },
  add_comp' := λ P Q R f g h, by { ext1, apply preadditive.add_comp },
  comp_add' := λ P Q R f g h, by { ext1, apply preadditive.comp_add } }
-/

end preadditive

section additive

variables [additive_category A] --[limits.has_finite_limits A]

instance : additive_category (Sheaf J A) :=
{ has_biproducts_of_shape := begin
    introsI K _,
    constructor,
    intros F,
    apply limits.has_biproduct.of_has_product F,
  end,
  ..(by apply_instance : preadditive (Sheaf J A)) }

end additive

section abelian

variables [abelian A]
-- We need sheafification
variables [concrete_category.{max v u} A]
variables [∀ (P : Cᵒᵖ ⥤ A) (X : C) (S : J.cover X), limits.has_multiequalizer (S.index P)]
variables [limits.preserves_limits (forget A)]
--variables [limits.has_finite_limits A]
variables [∀ (X : C), limits.has_colimits_of_shape (J.cover X)ᵒᵖ A]
variables [∀ (X : C), limits.preserves_colimits_of_shape (J.cover X)ᵒᵖ (forget A)]
variables [reflects_isomorphisms (forget A)]

open grothendieck_topology

def parallel_pair_sheafification {F G : Sheaf J A} (η : F ⟶ G) : limits.parallel_pair
  (limits.cokernel.π η.val) 0 ⋙ J.sheafification A ≅
  limits.parallel_pair (cokernel_π η).val 0 :=
nat_iso.of_components
(λ x,
match x with
| limits.walking_parallel_pair.zero := by { dsimp, refine (J.iso_sheafify G.2).symm }
| limits.walking_parallel_pair.one := by { dsimp, exact eq_to_iso rfl }
end)
begin
  -- This proof is SLOW :-(
  rintros (a|a) (b|b) (f|f|f),
  { dsimp [parallel_pair_sheafification._match_1],
    simp only [iso.eq_inv_comp, functor.map_id],
    dsimp [grothendieck_topology.iso_sheafify],
    rw [← category.assoc, is_iso.comp_inv_eq, category.id_comp],
    change J.to_sheafify _ ≫ (sheafification J A).map _ = _,
    erw [functor.map_id, category.comp_id] },
  { dsimp [parallel_pair_sheafification._match_1],
    rw [category.comp_id, iso.eq_inv_comp],
    dsimp [grothendieck_topology.iso_sheafify, cokernel_π],
    change (to_sheafification J A).app _ ≫ (sheafification J A).map _ = _,
    rw ← (to_sheafification J A).naturality,
    refl },
  { dsimp [parallel_pair_sheafification._match_1],
    simp only [limits.comp_zero, category.comp_id],
    change (sheafification J A).map _ = _,
    apply J.sheafify_hom_ext,
    { exact plus.is_sheaf_plus_plus J (limits.cokernel η.val) },
    erw ← (to_sheafification J A).naturality,
    simp },
  { dsimp [parallel_pair_sheafification._match_1],
    simp only [limits.comp_zero, category.id_comp, category.comp_id],
    change (sheafification J A).map _ = _,
    simp only [functor.map_id],
    erw (sheafification J A).map_id, refl },
end .

def kernel_cokernel_π_iso {F G : Sheaf J A} (η : F ⟶ G) :
  J.sheafify (limits.kernel (limits.cokernel.π ((Sheaf_to_presheaf J A).map η))) ≅
  limits.kernel ((Sheaf_to_presheaf J A).map (cokernel_π η)) :=
begin
  let e := (limits.is_limit_of_preserves (sheafification J A)
      (limits.limit.is_limit
      (limits.parallel_pair (limits.cokernel.π
      ((Sheaf_to_presheaf J A).map η)) 0))).cone_point_unique_up_to_iso (limits.limit.is_limit _),
  refine e ≪≫ _,
  change limits.limit _ ≅ _,
  refine limits.has_limit.iso_of_nat_iso _,
  apply parallel_pair_sheafification,
end

/-
{ hom := J.sheafify_lift (limits.kernel.map _ _ (𝟙 _) (J.to_sheafify _) (by admit)) (by admit),
  inv := begin
    let e : J.sheafify ((Sheaf_to_presheaf J A).obj G) ⟶
      J.sheafify (limits.cokernel ((Sheaf_to_presheaf J A).map η)) :=
        (sheafification J A).map (limits.cokernel.π _),
    let ee : limits.kernel ((Sheaf_to_presheaf J A).map (cokernel_π η)) ⟶ limits.kernel e,
    { refine limits.kernel.map _ _ (J.to_sheafify _) (𝟙 _) _,
      rw category.comp_id,
      dsimp only [e],
      rw ← grothendieck_topology.to_sheafification_app,
      rw ← (to_sheafification J A).naturality,
      refl },
    refine ee ≫ _,
    dsimp only [e],
    change limits.kernel ((Sheaf_to_presheaf J A).map ((presheaf_to_Sheaf J A).map _)) ⟶ _,
    refine (Sheaf_to_presheaf J A).map (kernel_iso_kernel_sheaf _).inv ≫ _,
    change _ ⟶ (Sheaf_to_presheaf J A).obj ((presheaf_to_Sheaf J A).obj _),
    refine (Sheaf_to_presheaf J A).map _,
    haveI : is_left_adjoint (presheaf_to_Sheaf J A) := by admit,
    -- Now we need to use the fact that finite limits commute with sheafification,
    -- i.e. that sheafification is left exact.
    admit
  end,
  hom_inv_id' := by admit,
  inv_hom_id' := by admit }
-/

lemma coim_to_im'_eq {F G : Sheaf J A} (η : F ⟶ G) :
  (Sheaf_to_presheaf J A).map (coim_to_im' η) =
  (sheafification J A).map (abelian.coimage_image_comparison _) ≫ (kernel_cokernel_π_iso η).hom :=
begin
  dsimp only [kernel_cokernel_π_iso, limits.is_limit.cone_point_unique_up_to_iso,
    functor.map_iso, iso.trans_hom],
  simp only [category.assoc],
  dsimp only [id, limits.is_limit.unique_up_to_iso, limits.cones.forget,
    limits.is_limit.lift_cone_morphism, functor.map_cone],
  apply limits.equalizer.hom_ext,
  simp only [category.assoc],
  --delta limits.equalizer.ι,
  erw limits.has_limit.iso_of_nat_iso_hom_π,
  dsimp only [parallel_pair_sheafification, nat_iso.of_components, id, iso_sheafify,
    as_iso, iso.symm],
  simp only [← category.assoc],
  rw is_iso.eq_comp_inv,
  simp only [category.assoc],
  erw limits.limit.lift_π,
  dsimp [limits.cones.functoriality, sheafify_map],
  simp_rw [← plus_functor_map, ← functor.comp_map, ← functor.map_comp],
  dsimp [coim_to_im', abelian.coimage_image_comparison, coim_to_im'_aux],
  apply J.sheafify_hom_ext,
  { exact plus.is_sheaf_plus_plus J G.val, },
  simp_rw ← category.assoc,
  erw J.to_sheafify_sheafify_lift,
  change _ = (to_sheafification J A).app _ ≫ (sheafification J A).map _,
  erw ← (to_sheafification J A).naturality,
  simp only [category.assoc, limits.kernel.lift_ι],
  dsimp,
  erw category.assoc,
end

instance is_iso_coim_to_im {F G : Sheaf J A} (η : F ⟶ G) :
  is_iso (abelian.coimage_image_comparison η) :=
begin
  rw coim_to_im_eq,
  suffices : is_iso (coim_to_im' η),
  { resetI, apply is_iso.comp_is_iso },
  suffices : is_iso ((Sheaf_to_presheaf J A).map (coim_to_im' η)),
  { resetI, apply is_iso_of_fully_faithful (Sheaf_to_presheaf J A) },
  rw coim_to_im'_eq,
  apply is_iso.comp_is_iso,
end

instance abelian : abelian (Sheaf J A) :=
abelian.of_coimage_image_comparison_is_iso

end abelian

end Sheaf
end category_theory

repo: lean-liquid


text:
/-
Copyright (c) 2019 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison, Johannes Hölzl
-/
import algebra.category.CommRing.basic
import data.mv_polynomial.comm_ring

/-!
Multivariable polynomials on a type is the left adjoint of the
forgetful functor from commutative rings to types.
-/

noncomputable theory

universe u

open mv_polynomial
open category_theory

namespace CommRing

open_locale classical

/--
The free functor `Type u ⥤ CommRing` sending a type `X` to the multivariable (commutative)
polynomials with variables `x : X`.
-/
def free : Type u ⥤ CommRing.{u} :=
{ obj := λ α, of (mv_polynomial α ℤ),
  map := λ X Y f,
    (↑(rename f : _ →ₐ[ℤ] _) : (mv_polynomial X ℤ →+* mv_polynomial Y ℤ)),
  -- TODO these next two fields can be done by `tidy`, but the calls in `dsimp` and `simp` it
  -- generates are too slow.
  map_id' := λ X, ring_hom.ext $ rename_id,
  map_comp' := λ X Y Z f g, ring_hom.ext $ λ p, (rename_rename f g p).symm }

@[simp] lemma free_obj_coe {α : Type u} :
  (free.obj α : Type u) = mv_polynomial α ℤ := rfl

@[simp] lemma free_map_coe {α β : Type u} {f : α → β} :
  ⇑(free.map f) = rename f := rfl

/--
The free-forgetful adjunction for commutative rings.
-/
def adj : free ⊣ forget CommRing.{u} :=
adjunction.mk_of_hom_equiv
{ hom_equiv := λ X R, hom_equiv,
  hom_equiv_naturality_left_symm' :=
    λ _ _ Y f g, ring_hom.ext $ λ x, eval₂_cast_comp f (int.cast_ring_hom Y) g x }

instance : is_right_adjoint (forget CommRing.{u}) := ⟨_, adj⟩

end CommRing

author: jjaassoonn


text:
/-
Copyright (c) 2020 Yury Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury Kudryashov
-/
import analysis.calculus.local_extr

/-!
# Darboux's theorem

In this file we prove that the derivative of a differentiable function on an interval takes all
intermediate values. The proof is based on the
[Wikipedia](https://en.wikipedia.org/wiki/Darboux%27s_theorem_(analysis)) page about this theorem.
-/

open filter set
open_locale topology classical

variables {a b : ℝ} {f f' : ℝ → ℝ}

/-- **Darboux's theorem**: if `a ≤ b` and `f' a < m < f' b`, then `f' c = m` for some
`c ∈ [a, b]`. -/
theorem exists_has_deriv_within_at_eq_of_gt_of_lt
  (hab : a ≤ b) (hf : ∀ x ∈ (Icc a b), has_deriv_within_at f (f' x) (Icc a b) x)
  {m : ℝ} (hma : f' a < m) (hmb : m < f' b) :
  m ∈ f' '' (Icc a b) :=
begin
  have hab' : a < b,
  { refine lt_of_le_of_ne hab (λ hab', _),
    subst b,
    exact lt_asymm hma hmb },
  set g : ℝ → ℝ := λ x, f x - m * x,
  have hg : ∀ x ∈ Icc a b, has_deriv_within_at g (f' x - m) (Icc a b) x,
  { intros x hx,
    simpa using (hf x hx).sub ((has_deriv_within_at_id x _).const_mul m) },
  obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Icc a b, is_min_on g (Icc a b) c,
    from is_compact_Icc.exists_forall_le (nonempty_Icc.2 $ hab)
      (λ x hx, (hg x hx).continuous_within_at),
  have cmem' : c ∈ Ioo a b,
  { cases eq_or_lt_of_le cmem.1 with hac hac,
    -- Show that `c` can't be equal to `a`
    { subst c,
      refine absurd (sub_nonneg.1 $ nonneg_of_mul_nonneg_right _ (sub_pos.2 hab'))
        (not_le_of_lt hma),
      have : b - a ∈ pos_tangent_cone_at (Icc a b) a,
        from mem_pos_tangent_cone_at_of_segment_subset (segment_eq_Icc hab ▸ subset.refl _),
      simpa [-sub_nonneg, -continuous_linear_map.map_sub]
        using hc.localize.has_fderiv_within_at_nonneg (hg a (left_mem_Icc.2 hab)) this },
    cases eq_or_lt_of_le cmem.2 with hbc hbc,
    -- Show that `c` can't be equal to `b`
    { subst c,
      refine absurd (sub_nonpos.1 $ nonpos_of_mul_nonneg_right _ (sub_lt_zero.2 hab'))
        (not_le_of_lt hmb),
      have : a - b ∈ pos_tangent_cone_at (Icc a b) b,
        from mem_pos_tangent_cone_at_of_segment_subset (by rw [segment_symm, segment_eq_Icc hab]),
      simpa [-sub_nonneg, -continuous_linear_map.map_sub]
        using hc.localize.has_fderiv_within_at_nonneg (hg b (right_mem_Icc.2 hab)) this },
    exact ⟨hac, hbc⟩ },
  use [c, cmem],
  rw [← sub_eq_zero],
  have : Icc a b ∈ 𝓝 c, by rwa [← mem_interior_iff_mem_nhds, interior_Icc],
  exact (hc.is_local_min this).has_deriv_at_eq_zero ((hg c cmem).has_deriv_at this)
end

/-- **Darboux's theorem**: if `a ≤ b` and `f' a > m > f' b`, then `f' c = m` for some `c ∈ [a, b]`.
-/
theorem exists_has_deriv_within_at_eq_of_lt_of_gt
  (hab : a ≤ b) (hf : ∀ x ∈ (Icc a b), has_deriv_within_at f (f' x) (Icc a b) x)
  {m : ℝ} (hma : m < f' a) (hmb : f' b < m) :
  m ∈ f' '' (Icc a b) :=
let ⟨c, cmem, hc⟩ := exists_has_deriv_within_at_eq_of_gt_of_lt hab (λ x hx, (hf x hx).neg)
  (neg_lt_neg hma) (neg_lt_neg hmb)
in ⟨c, cmem, neg_injective hc⟩

/-- **Darboux's theorem**: the image of a convex set under `f'` is a convex set. -/
theorem convex_image_has_deriv_at {s : set ℝ} (hs : convex ℝ s)
  (hf : ∀ x ∈ s, has_deriv_at f (f' x) x) :
  convex ℝ (f' '' s) :=
begin
  refine ord_connected.convex ⟨_⟩,
  rintros _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ m ⟨hma, hmb⟩,
  cases eq_or_lt_of_le hma with hma hma,
    by exact hma ▸ mem_image_of_mem f' ha,
  cases eq_or_lt_of_le hmb with hmb hmb,
    by exact hmb.symm ▸ mem_image_of_mem f' hb,
  cases le_total a b with hab hab,
  { have : Icc a b ⊆ s, from hs.ord_connected.out ha hb,
    rcases exists_has_deriv_within_at_eq_of_gt_of_lt hab
      (λ x hx, (hf x $ this hx).has_deriv_within_at) hma hmb
      with ⟨c, cmem, hc⟩,
    exact ⟨c, this cmem, hc⟩ },
  { have : Icc b a ⊆ s, from hs.ord_connected.out hb ha,
    rcases exists_has_deriv_within_at_eq_of_lt_of_gt hab
      (λ x hx, (hf x $ this hx).has_deriv_within_at) hmb hma
      with ⟨c, cmem, hc⟩,
    exact ⟨c, this cmem, hc⟩ }
end

/-- If the derivative of a function is never equal to `m`, then either
it is always greater than `m`, or it is always less than `m`. -/
theorem deriv_forall_lt_or_forall_gt_of_forall_ne {s : set ℝ} (hs : convex ℝ s)
  (hf : ∀ x ∈ s, has_deriv_at f (f' x) x) {m : ℝ} (hf' : ∀ x ∈ s, f' x ≠ m) :
  (∀ x ∈ s, f' x < m) ∨ (∀ x ∈ s, m < f' x) :=
begin
  contrapose! hf',
  rcases hf' with ⟨⟨b, hb, hmb⟩, ⟨a, ha, hma⟩⟩,
  exact (convex_image_has_deriv_at hs hf).ord_connected.out (mem_image_of_mem f' ha)
    (mem_image_of_mem f' hb) ⟨hma, hmb⟩
end

author: leanprover-community

repo: mathlib


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

! This file was ported from Lean 3 source module data.list.nodup_equiv_fin
! leanprover-community/mathlib commit 008205aa645b3f194c1da47025c5f110c8406eab
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fin.Basic
import Mathlib.Data.List.Sort
import Mathlib.Data.List.Duplicate

/-!
# Equivalence between `Fin (length l)` and elements of a list

Given a list `l`,

* if `l` has no duplicates, then `List.Nodup.getEquiv` is the equivalence between
  `Fin (length l)` and `{x // x ∈ l}` sending `i` to `⟨get l i, _⟩` with the inverse
  sending `⟨x, hx⟩` to `⟨indexOf x l, _⟩`;

* if `l` has no duplicates and contains every element of a type `α`, then
  `List.Nodup.getEquivOfForallMemList` defines an equivalence between
  `Fin (length l)` and `α`;  if `α` does not have decidable equality, then
  there is a bijection `List.Nodup.getBijectionOfForallMemList`;

* if `l` is sorted w.r.t. `(<)`, then `List.Sorted.getIso` is the same bijection reinterpreted
  as an `OrderIso`.

-/

namespace List

variable {α : Type _}

namespace Nodup

/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
a bijection `Fin l.length → α`.  See `List.Nodup.getEquivOfForallMemList`
for a version giving an equivalence when there is decidable equality. -/
@[simps]
def getBijectionOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) :
    { f : Fin l.length → α // Function.Bijective f } :=
  ⟨fun i => l.get i, fun _ _ h => Fin.ext <| (nd.nthLe_inj_iff _ _).1 h,
   fun x =>
    let ⟨i, hl⟩ := List.mem_iff_get.1 (h x)
    ⟨i, hl⟩⟩
#align list.nodup.nth_le_bijection_of_forall_mem_list List.Nodup.getBijectionOfForallMemList

variable [DecidableEq α]

/-- If `l` has no duplicates, then `List.get` defines an equivalence between `Fin (length l)` and
the set of elements of `l`. -/
@[simps]
def getEquiv (l : List α) (H : Nodup l) : Fin (length l) ≃ { x // x ∈ l } where
  toFun i := ⟨get l i, get_mem l i i.2⟩
  invFun x := ⟨indexOf (↑x) l, indexOf_lt_length.2 x.2⟩
  left_inv i := by simp only [List.get_indexOf, eq_self_iff_true, Fin.eta, Subtype.coe_mk, H]
  right_inv x := by simp
#align list.nodup.nth_le_equiv List.Nodup.getEquiv

/-- If `l` lists all the elements of `α` without duplicates, then `List.get` defines
an equivalence between `Fin l.length` and `α`.

See `List.Nodup.getBijectionOfForallMemList` for a version without
decidable equality. -/
@[simps]
def getEquivOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) : Fin l.length ≃ α
    where
  toFun i := l.get i
  invFun a := ⟨_, indexOf_lt_length.2 (h a)⟩
  left_inv i := by simp [List.get_indexOf, nd]
  right_inv a := by simp
#align list.nodup.nth_le_equiv_of_forall_mem_list List.Nodup.getEquivOfForallMemList

end Nodup

namespace Sorted

variable [Preorder α] {l : List α}

theorem get_mono (h : l.Sorted (· ≤ ·)) : Monotone l.get := fun _ _ => h.rel_get_of_le
#align list.sorted.nth_le_mono List.Sorted.get_mono

theorem get_strictMono (h : l.Sorted (· < ·)) : StrictMono l.get := fun _ _ => h.rel_get_of_lt
#align list.sorted.nth_le_strict_mono List.Sorted.get_strictMono

variable [DecidableEq α]

/-- If `l` is a list sorted w.r.t. `(<)`, then `List.get` defines an order isomorphism between
`Fin (length l)` and the set of elements of `l`. -/
def getIso (l : List α) (H : Sorted (· < ·) l) : Fin (length l) ≃o { x // x ∈ l } where
  toEquiv := H.nodup.getEquiv l
  map_rel_iff' := H.get_strictMono.le_iff_le
#align list.sorted.nth_le_iso List.Sorted.getIso

variable (H : Sorted (· < ·) l) {x : { x // x ∈ l }} {i : Fin l.length}

@[simp]
theorem coe_getIso_apply : (H.getIso l i : α) = get l i :=
  rfl
#align list.sorted.coe_nth_le_iso_apply List.Sorted.coe_getIso_apply

@[simp]
theorem coe_getIso_symm_apply : ((H.getIso l).symm x : ℕ) = indexOf (↑x) l :=
  rfl
#align list.sorted.coe_nth_le_iso_symm_apply List.Sorted.coe_getIso_symm_apply

end Sorted

section Sublist

/-- If there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`,
then `Sublist l l'`.
-/
theorem sublist_of_orderEmbedding_get?_eq {l l' : List α} (f : ℕ ↪o ℕ)
    (hf : ∀ ix : ℕ, l.get? ix = l'.get? (f ix)) : l <+ l' := by
  induction' l with hd tl IH generalizing l' f
  · simp
  have : some hd = _ := hf 0
  rw [eq_comm, List.get?_eq_some] at this
  obtain ⟨w, h⟩ := this
  let f' : ℕ ↪o ℕ :=
    OrderEmbedding.ofMapLEIff (fun i => f (i + 1) - (f 0 + 1)) fun a b => by
      dsimp only
      rw [tsub_le_tsub_iff_right, OrderEmbedding.le_iff_le, Nat.succ_le_succ_iff]
      rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
      exact b.succ_pos
  have : ∀ ix, tl.get? ix = (l'.drop (f 0 + 1)).get? (f' ix) := by
    intro ix
    rw [List.get?_drop, OrderEmbedding.coe_ofMapLEIff, add_tsub_cancel_of_le, ←hf, List.get?]
    rw [Nat.succ_le_iff, OrderEmbedding.lt_iff_lt]
    exact ix.succ_pos
  rw [← List.take_append_drop (f 0 + 1) l', ← List.singleton_append]
  apply List.Sublist.append _ (IH _ this)
  rw [List.singleton_sublist, ← h, l'.get_take _ (Nat.lt_succ_self _)]
  apply List.get_mem
#align list.sublist_of_order_embedding_nth_eq List.sublist_of_orderEmbedding_get?_eq

/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `ℕ` into `ℕ` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
-/
theorem sublist_iff_exists_orderEmbedding_get?_eq {l l' : List α} :
    l <+ l' ↔ ∃ f : ℕ ↪o ℕ, ∀ ix : ℕ, l.get? ix = l'.get? (f ix) := by
  constructor
  · intro H
    induction' H with xs ys y _H IH xs ys x _H IH
    · simp
    · obtain ⟨f, hf⟩ := IH
      refine' ⟨f.trans (OrderEmbedding.ofStrictMono (· + 1) fun _ => by simp), _⟩
      simpa using hf
    · obtain ⟨f, hf⟩ := IH
      refine'
        ⟨OrderEmbedding.ofMapLEIff (fun ix : ℕ => if ix = 0 then 0 else (f ix.pred).succ) _, _⟩
      · rintro ⟨_ | a⟩ ⟨_ | b⟩ <;> simp [Nat.succ_le_succ_iff]
      · rintro ⟨_ | i⟩
        · simp
        · simpa using hf _
  · rintro ⟨f, hf⟩
    exact sublist_of_orderEmbedding_get?_eq f hf
#align list.sublist_iff_exists_order_embedding_nth_eq List.sublist_iff_exists_orderEmbedding_get?_eq

/-- A `l : List α` is `Sublist l l'` for `l' : List α` iff
there is `f`, an order-preserving embedding of `Fin l.length` into `Fin l'.length` such that
any element of `l` found at index `ix` can be found at index `f ix` in `l'`.
-/
theorem sublist_iff_exists_fin_orderEmbedding_get_eq {l l' : List α} :
    l <+ l' ↔
      ∃ f : Fin l.length ↪o Fin l'.length,
        ∀ ix : Fin l.length, l.get ix = l'.get (f ix) := by
  rw [sublist_iff_exists_orderEmbedding_get?_eq]
  constructor
  · rintro ⟨f, hf⟩
    have h : ∀ {i : ℕ} (_ : i < l.length), f i < l'.length :=
      by
      intro i hi
      specialize hf i
      rw [get?_eq_get hi, eq_comm, get?_eq_some] at hf
      obtain ⟨h, -⟩ := hf
      exact h
    refine' ⟨OrderEmbedding.ofMapLEIff (fun ix => ⟨f ix, h ix.is_lt⟩) _, _⟩
    · simp
    · intro i
      apply Option.some_injective
      simpa [get?_eq_get i.2, get?_eq_get (h i.2)] using hf i
  · rintro ⟨f, hf⟩
    refine'
      ⟨OrderEmbedding.ofStrictMono (fun i => if hi : i < l.length then f ⟨i, hi⟩ else i + l'.length)
          _,
        _⟩
    · intro i j h
      dsimp only
      split_ifs with hi hj hj
      · rwa [Fin.val_fin_lt, f.lt_iff_lt]
      · rw [add_comm]
        exact lt_add_of_lt_of_pos (Fin.is_lt _) (i.zero_le.trans_lt h)
      · exact absurd (h.trans hj) hi
      · simpa using h
    · intro i
      simp only [OrderEmbedding.coe_ofStrictMono]
      split_ifs with hi
      · rw [get?_eq_get hi, get?_eq_get, ← hf]
      · rw [get?_eq_none.mpr, get?_eq_none.mpr]
        · simp
        · simpa using hi
#align
  list.sublist_iff_exists_fin_order_embedding_nth_le_eq
  List.sublist_iff_exists_fin_orderEmbedding_get_eq

/-- An element `x : α` of `l : List α` is a duplicate iff it can be found
at two distinct indices `n m : ℕ` inside the list `l`.
-/
theorem duplicate_iff_exists_distinct_get {l : List α} {x : α} :
    l.Duplicate x ↔
      ∃ (n m : Fin l.length) (_ : n < m),
        x = l.get n ∧ x = l.get m := by
  classical
    rw [duplicate_iff_two_le_count, le_count_iff_replicate_sublist,
      sublist_iff_exists_fin_orderEmbedding_get_eq]
    constructor
    · rintro ⟨f, hf⟩
      refine' ⟨f ⟨0, by simp⟩, f ⟨1, by simp⟩,
        f.lt_iff_lt.2 (show (0 : ℕ) < 1 from zero_lt_one), _⟩
      · rw [← hf, ← hf]; simp
    · rintro ⟨n, m, hnm, h, h'⟩
      refine' ⟨OrderEmbedding.ofStrictMono (fun i => if (i : ℕ) = 0 then n else m) _, _⟩
      · rintro ⟨⟨_ | i⟩, hi⟩ ⟨⟨_ | j⟩, hj⟩
        · simp
        · simp [hnm]
        · simp
        · simp only [Nat.lt_succ_iff, Nat.succ_le_succ_iff, replicate, length,
            nonpos_iff_eq_zero] at hi hj
          simp [hi, hj]
      · rintro ⟨⟨_ | i⟩, hi⟩
        · simpa using h
        · simpa using h'

/-- An element `x : α` of `l : List α` is a duplicate iff it can be found
at two distinct indices `n m : ℕ` inside the list `l`.
-/
@[deprecated duplicate_iff_exists_distinct_get]
theorem duplicate_iff_exists_distinct_nthLe {l : List α} {x : α} :
    l.Duplicate x ↔
      ∃ (n : ℕ) (hn : n < l.length) (m : ℕ) (hm : m < l.length) (_ : n < m),
        x = l.nthLe n hn ∧ x = l.nthLe m hm :=
  duplicate_iff_exists_distinct_get.trans
    ⟨fun ⟨n, m, h⟩ => ⟨n.1, n.2, m.1, m.2, h⟩,
    fun ⟨n, hn, m, hm, h⟩ => ⟨⟨n, hn⟩, ⟨m, hm⟩, h⟩⟩
#align list.duplicate_iff_exists_distinct_nth_le List.duplicate_iff_exists_distinct_nthLe

end Sublist

end List


text:
/-
Copyright (c) 2022 Yury G. Kudryashov. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yury G. Kudryashov
-/
import topology.algebra.uniform_group
import topology.uniform_space.completion

/-!
# Multiplicative action on the completion of a uniform space

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

In this file we define typeclasses `has_uniform_continuous_const_vadd` and
`has_uniform_continuous_const_smul` and prove that a multiplicative action on `X` with uniformly
continuous `(•) c` can be extended to a multiplicative action on `uniform_space.completion X`.

In later files once the additive group structure is set up, we provide
* `uniform_space.completion.distrib_mul_action`
* `uniform_space.completion.mul_action_with_zero`
* `uniform_space.completion.module`

TODO: Generalise the results here from the concrete `completion` to any `abstract_completion`.
-/

universes u v w x y z

noncomputable theory

variables (R : Type u) (M : Type v) (N : Type w) (X : Type x) (Y : Type y)
  [uniform_space X] [uniform_space Y]

/-- An additive action such that for all `c`, the map `λ x, c +ᵥ x` is uniformly continuous. -/
class has_uniform_continuous_const_vadd [has_vadd M X] : Prop :=
(uniform_continuous_const_vadd : ∀ (c : M), uniform_continuous ((+ᵥ) c : X → X))

/-- A multiplicative action such that for all `c`, the map `λ x, c • x` is uniformly continuous. -/
@[to_additive]
class has_uniform_continuous_const_smul [has_smul M X] : Prop :=
(uniform_continuous_const_smul : ∀ (c : M), uniform_continuous ((•) c : X → X))

export has_uniform_continuous_const_vadd (uniform_continuous_const_vadd)
  has_uniform_continuous_const_smul (uniform_continuous_const_smul)

instance add_monoid.has_uniform_continuous_const_smul_nat [add_group X] [uniform_add_group X] :
  has_uniform_continuous_const_smul ℕ X :=
⟨uniform_continuous_const_nsmul⟩

instance add_group.has_uniform_continuous_const_smul_int [add_group X] [uniform_add_group X] :
  has_uniform_continuous_const_smul ℤ X :=
⟨uniform_continuous_const_zsmul⟩

/-- A `distrib_mul_action` that is continuous on a uniform group is uniformly continuous.
This can't be an instance due to it forming a loop with
`has_uniform_continuous_const_smul.to_has_continuous_const_smul` -/
lemma has_uniform_continuous_const_smul_of_continuous_const_smul [monoid R] [add_comm_group M]
  [distrib_mul_action R M] [uniform_space M] [uniform_add_group M] [has_continuous_const_smul R M] :
  has_uniform_continuous_const_smul R M :=
⟨λ r, uniform_continuous_of_continuous_at_zero (distrib_mul_action.to_add_monoid_hom M r)
  (continuous.continuous_at (continuous_const_smul r))⟩

/-- The action of `semiring.to_module` is uniformly continuous. -/
instance ring.has_uniform_continuous_const_smul [ring R] [uniform_space R]
  [uniform_add_group R] [has_continuous_mul R] : has_uniform_continuous_const_smul R R :=
has_uniform_continuous_const_smul_of_continuous_const_smul _ _

/-- The action of `semiring.to_opposite_module` is uniformly continuous. -/
instance ring.has_uniform_continuous_const_op_smul [ring R] [uniform_space R]
  [uniform_add_group R] [has_continuous_mul R] : has_uniform_continuous_const_smul Rᵐᵒᵖ R :=
has_uniform_continuous_const_smul_of_continuous_const_smul _ _

section has_smul

variable [has_smul M X]

@[priority 100, to_additive]
instance has_uniform_continuous_const_smul.to_has_continuous_const_smul
  [has_uniform_continuous_const_smul M X] : has_continuous_const_smul M X :=
⟨λ c, (uniform_continuous_const_smul c).continuous⟩

variables {M X Y}

@[to_additive] lemma uniform_continuous.const_smul [has_uniform_continuous_const_smul M X]
  {f : Y → X} (hf : uniform_continuous f) (c : M) :
  uniform_continuous (c • f) :=
(uniform_continuous_const_smul c).comp hf

/-- If a scalar action is central, then its right action is uniform continuous when its left action
is. -/
@[priority 100, to_additive "If an additive action is central, then its right action is uniform
continuous when its left action,is."]
instance has_uniform_continuous_const_smul.op [has_smul Mᵐᵒᵖ X] [is_central_scalar M X]
  [has_uniform_continuous_const_smul M X] : has_uniform_continuous_const_smul Mᵐᵒᵖ X :=
⟨mul_opposite.rec $ λ c, begin
  change uniform_continuous (λ m, mul_opposite.op c • m),
  simp_rw op_smul_eq_smul,
  exact uniform_continuous_const_smul c,
end⟩

@[to_additive] instance mul_opposite.has_uniform_continuous_const_smul
  [has_uniform_continuous_const_smul M X] : has_uniform_continuous_const_smul M Xᵐᵒᵖ :=
⟨λ c, mul_opposite.uniform_continuous_op.comp $ mul_opposite.uniform_continuous_unop.const_smul c⟩

end has_smul

@[to_additive] instance uniform_group.to_has_uniform_continuous_const_smul
  {G : Type u} [group G] [uniform_space G] [uniform_group G] :
  has_uniform_continuous_const_smul G G :=
⟨λ c, uniform_continuous_const.mul uniform_continuous_id⟩

namespace uniform_space

namespace completion

section has_smul

variable [has_smul M X]

@[to_additive] instance : has_smul M (completion X) :=
⟨λ c, completion.map ((•) c)⟩

@[to_additive] lemma smul_def (c : M) (x : completion X) : c • x = completion.map ((•) c) x := rfl

@[to_additive] instance : has_uniform_continuous_const_smul M (completion X) :=
⟨λ c, uniform_continuous_map⟩

@[to_additive] instance [has_smul N X] [has_smul M N]
  [has_uniform_continuous_const_smul M X] [has_uniform_continuous_const_smul N X]
  [is_scalar_tower M N X] : is_scalar_tower M N (completion X) :=
⟨λ m n x, begin
  have : _ = (_ : completion X → completion X) :=
    map_comp (uniform_continuous_const_smul m) (uniform_continuous_const_smul n),
  refine eq.trans _ (congr_fun this.symm x),
  exact congr_arg (λ f, completion.map f x) (by exact funext (smul_assoc _ _)),
end⟩

@[to_additive] instance [has_smul N X] [smul_comm_class M N X]
  [has_uniform_continuous_const_smul M X] [has_uniform_continuous_const_smul N X] :
  smul_comm_class M N (completion X) :=
⟨λ m n x, begin
  have hmn : m • n • x =
    (( completion.map (has_smul.smul m)) ∘ (completion.map (has_smul.smul n))) x := rfl,
  have hnm : n • m • x =
    (( completion.map (has_smul.smul n)) ∘ (completion.map (has_smul.smul m))) x := rfl,
  rw [hmn, hnm, map_comp, map_comp],
  exact congr_arg (λ f, completion.map f x) (by exact funext (smul_comm _ _)),
  repeat{ exact uniform_continuous_const_smul _},
 end⟩

@[to_additive]
instance [has_smul Mᵐᵒᵖ X] [is_central_scalar M X] : is_central_scalar M (completion X) :=
⟨λ c a, congr_arg (λ f, completion.map f a) $ by exact funext (op_smul_eq_smul c)⟩

variables {M X} [has_uniform_continuous_const_smul M X]

@[simp, norm_cast, to_additive]

end has_smul

@[to_additive] instance [monoid M] [mul_action M X] [has_uniform_continuous_const_smul M X] :
  mul_action M (completion X) :=
{ smul := (•),
  one_smul := ext' (continuous_const_smul _) continuous_id $ λ a, by rw [← coe_smul, one_smul],
  mul_smul := λ x y, ext' (continuous_const_smul _) ((continuous_const_smul _).const_smul _) $
    λ a, by simp only [← coe_smul, mul_smul] }

end completion

end uniform_space


text:
import tactic topology.basic
open classical topological_space

-- El conjunt buit és un conjunt obert en qualsevol topologia.
theorem BuitObert {X: Type} (h1: topological_space X) : (h1.is_open (∅ : set X)) :=
begin
	let Z := (∅ : set (set X)),
	have h2 : ∀ z ∈ Z, h1.is_open z,
	intro z,
	assume h3,
	exact false.elim h3,
	sorry,
end

-- La topologia discreta és una topologia.
instance TopDisc {X: Type} : topological_space X :=
begin
	-- Definim la topologia discreta
	let TD : set X → Prop := λ(U: set X), true,

	use TD,
	-- Objectiu 1: Intersecció
	{ intros A B,
	  assume h1 h2,
	  exact true.intro, },
	-- Objectiu 2: Unió arbitrària
	{ intro I,
	  intro A,
	  exact true.intro, },
end

-- La topologia trivial és una topologia.
instance TopTriv {X: Type} : topological_space X :=
begin
	-- Definim la topologia trivial
	let TT: set X → Prop :=
	begin
		intro U,
		exact (U = set.univ) ∨ (U = (∅ : set X)),
  end,

	use TT,
	-- Objectiu 1: Total
	{ have h1: set.univ = set.univ,
		 refl,
	 exact or.inl h1, },

	-- Objectiu 2: Intersecció
	{ intros A B,
		assume h1 h2,
		cases h1 with hAU hAE,
		-- Cas 2.1: A = set.univ
		{ have h3 : A ∩ B = B,
				ext z,
				split,
				-- Subojectiu 2.1.1
				{ assume h4,
					exact and.elim_right h4, },
				-- Subojectiu 2.1.2
				{ assume h4,
					have h5 : z ∈ A,
						exact filter.mem_top.mpr hAU z,
					exact and.intro h5 h4, },
					rw h3,
					exact h2, },
		-- Cas 2.2: A = ∅
		{ have h3: A∩B = (∅: set X),
				ext z,
				split,
				-- Subojectiu 2.2.1
				{ rw hAE,
					assume h3,
					exact and.elim_left h3, },
				-- Subojectiu 2.2.2
				{ rw hAE,
					assume h3,
					exact false.rec (z ∈ ∅ ∩ B) h3, },
			rw h3,
			have h4: ∅ = ∅,
				refl,
			exact or.inr h4, }, },

	-- Objectiu 3: Unió arbitrària
	-- TODO: Corregir l'estil del codi
	{ intro 𝔸,
		intro h1,
		have h2: ∀ (t : set X), t ∈ 𝔸 → t = set.univ ∨ t = (∅: set X),
			exact h1,
		have h3: (∀ (t: set X), t ∈ 𝔸 → t = (∅: set X)) ∨ ¬(∀ (t: set X), t ∈ 𝔸 → t = (∅: set X)),
			exact classical.em (∀ (t : set X), t ∈ 𝔸 → t = ∅),
		cases h3 with h3A h3B,
		have h4: ⋃₀ 𝔸 = (∅ : set X),
		ext z,
		split,
		assume h4,
		cases h4 with T hT,
		cases hT with hT hz,
		have h5: T = (∅: set X),
		apply h3A,
		exact hT,
		rw h5 at hz,
		exact hz,
		assume h4,
		exact false.rec (z ∈ ⋃₀ 𝔸) h4,
		rw h4,
		have h5: ∅ = ∅,
			refl,
		exact or.inr h5,
		have h5 : ∃ (t : set X), ¬(t ∈ 𝔸 → t = (∅ : set X)),
		exact not_forall.mp h3B,
		cases h5 with T hT,
		simp at hT,
		cases hT with hT hT1,
		have h6 : TT T,
		exact h1 T hT,
		have h7 : T = set.univ,
		cases h6,
		assumption, --exact h6,
		by_contra,
		exact hT1 h6,
		have h8 : ⋃₀ 𝔸 = set.univ,
		ext z,
		split,
		assume h8,
		exact set.mem_univ z,
		assume h8,
		rw h7.symm at h8,
		use T,
		exact and.intro hT h8,
		exact or.inl h8, },
end

-- La topologia cofinita és una topologia.
instance TopCof (X: Type) : topological_space X :=
begin
	-- Definim la topologia cofinita
	let TC : set X → Prop := λ(A: set X), (A = (∅ : set X)) ∨ (set.finite (Aᶜ)),

	use TC,
	sorry,
	sorry,
	sorry,
end

author: mariovagomarzal


text:
import order order.complete_lattice

open lattice

reserve infixl ` ⇒ `:60
reserve infixl ` ⊢ `:50
reserve infixl ` & `:70

infix ⇒ := has_imp.imp

universes u v

inductive rlist (A : Type u) : Type u
| nil {} : rlist
| snoc {} : rlist → A → rlist

infix & := rlist.snoc

namespace rlist

def map {A : Type u} {B : Type v} (f : A → B) : rlist A → rlist B
| nil := nil
| (xs & x) := map xs & f x

inductive mem {A : Type u} : A → rlist A → Prop
| here : ∀ x xs, mem x (xs & x)
| there : ∀ x y ys, mem x ys → mem x (ys & y)

instance has_mem (A : Type u) : has_mem A (rlist A)
:= ⟨ mem ⟩

instance mem_decidable (A : Type u) [decidable_eq A]
  (x : A) (xs : rlist A) : decidable (x ∈ xs)
:= begin
induction xs,
{ apply decidable.is_false, intros contra, cases contra, },
{ induction ih_1,
  { apply (if H : x = a_1 then _ else _),
    subst a_1, apply decidable.is_true, constructor,
    apply decidable.is_false, intros contra,
    cases contra, cc, apply a_2, assumption,
  },
  { apply decidable.is_true, constructor, assumption }
}
end

lemma map_mem {A : Type u} {B : Type v} (f : A → B) (x : A)
  (xs : rlist A)
  (H : x ∈ xs) : f x ∈ xs.map f
:= begin
induction H; dsimp [map], constructor, constructor, assumption,
end

end rlist

/-- complete heyting algebra -/
class cha (α : Type u) extends complete_lattice α, has_imp α : Type u :=
  (intro : ∀ {Γ P Q : α}, (Γ ⊓ P ≤ Q) → (Γ ≤ P ⇒ Q))
  (revert : ∀ {Γ P Q : α}, (Γ ≤ P ⇒ Q) → (Γ ⊓ P ≤ Q))

namespace cha
section cha_facts
parameters (α : Type u) [cha α]

def imp_adjunction {Γ P Q : α}
  : (Γ ⊓ P ≤ Q) = (Γ ≤ P ⇒ Q)
:= begin
apply propext, split, apply cha.intro, apply cha.revert,
end

end cha_facts
end cha

namespace sequent
section entails
parameters {α : Type u} [bounded_lattice α]

def conjunction  : rlist α → α
| rlist.nil := ⊤
| (Ps & P) := conjunction Ps ⊓ P

def entails (Γ : rlist α) (A : α)
  := conjunction Γ ≤ A
end entails

infix ⊢ := entails

section logic
parameters {α : Type u} [cha α]

def assumption {Γ : rlist α} {P : α} (H : P ∈ Γ)
  : Γ ⊢ P
:= begin
unfold entails,
induction H; dsimp [conjunction],
{ apply inf_le_right, },
{ apply le_trans, apply inf_le_left, assumption, }
end

def intro {Γ : rlist α} {P Q : α}
  (H : (Γ & P) ⊢ Q)
     : Γ ⊢ (P ⇒ Q)
:= begin
dsimp [entails, conjunction] at H,
apply cha.intro, assumption
end

def revert {Γ : rlist α} {P Q : α}
  (H : Γ ⊢ (P ⇒ Q))
  : (Γ & P) ⊢ Q
:= begin
dsimp [entails, conjunction],
apply cha.revert, assumption
end

def entails_top {Γ : rlist α}
  : Γ ⊢ ⊤
:= begin
dsimp [entails], apply le_top,
end

def split {Γ : rlist α} {P Q : α}
  (HP : Γ ⊢ P)
  (HQ : Γ ⊢ Q)
  : Γ ⊢ P ⊓ Q
:= begin
dsimp [entails] at *,
apply le_inf; assumption
end

def left {Γ : rlist α} {P Q : α}
  (HP : Γ ⊢ P)
  : Γ ⊢ P ⊔ Q
:= begin
dsimp [entails] at *,
apply le_trans, assumption, apply le_sup_left,
end

def right {Γ : rlist α} {P Q : α}
  (HP : Γ ⊢ Q)
  : Γ ⊢ P ⊔ Q
:= begin
dsimp [entails] at *,
apply le_trans, assumption, apply le_sup_right,
end

def apply_lemma_conj {Γ Δ : rlist α} {P : α}
   (H : Δ ⊢ P)
   (Hassumptions : Γ ⊢ conjunction Δ)
   : Γ ⊢ P
:= begin
apply le_trans; assumption,
end

def prove_conjunction_helper (Γ : rlist α)
  : rlist α → Prop
| rlist.nil := true
| (xs & x) := prove_conjunction_helper xs ∧ Γ ⊢ x

def prove_conjunction {Γ Δ : rlist α}
  (H : prove_conjunction_helper Γ Δ)
  : Γ ⊢ conjunction Δ
:= begin
induction Δ;
  dsimp [prove_conjunction_helper] at H;
  dsimp [conjunction],
apply entails_top, induction H with H1 H2,
apply split, apply ih_1, assumption, assumption,
end

def apply_lemma (Γ : rlist α) (P : α)
   {Δ : rlist α}
   (H : Δ ⊢ P)
   (Hassumptions : prove_conjunction_helper Γ Δ)
   : Γ ⊢ P
:= begin
apply apply_lemma_conj, assumption,
apply prove_conjunction, assumption,
end

def cut (Γ : rlist α) (Q : α) (P : α)
  (HP : Γ ⊢ P)
  (H : Γ & P ⊢ Q)
  : Γ ⊢ Q
:= begin
apply apply_lemma_conj H,
dsimp [conjunction], apply split,
apply le_refl, assumption
end

lemma test (P Q : α) : rlist.nil & P & Q ⊢ Q :=
begin
apply assumption, constructor,
end

end logic

end sequent

author: GaloisInc

repo: lean-protocol-support


text:
/-
Copyright (c) 2021 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import linear_algebra.affine_space.independent
import linear_algebra.basis

/-!
# Affine bases and barycentric coordinates

Suppose `P` is an affine space modelled on the module `V` over the ring `k`, and `p : ι → P` is an
affine-independent family of points spanning `P`. Given this data, each point `q : P` may be written
uniquely as an affine combination: `q = w₀ p₀ + w₁ p₁ + ⋯` for some (finitely-supported) weights
`wᵢ`. For each `i : ι`, we thus have an affine map `P →ᵃ[k] k`, namely `q ↦ wᵢ`. This family of
maps is known as the family of barycentric coordinates. It is defined in this file.

## The construction

Fixing `i : ι`, and allowing `j : ι` to range over the values `j ≠ i`, we obtain a basis `bᵢ` of `V`
defined by `bᵢ j = p j -ᵥ p i`. Let `fᵢ j : V →ₗ[k] k` be the corresponding dual basis and let
`fᵢ = ∑ j, fᵢ j : V →ₗ[k] k` be the corresponding "sum of all coordinates" form. Then the `i`th
barycentric coordinate of `q : P` is `1 - fᵢ (q -ᵥ p i)`.

## Main definitions

 * `affine_basis`: a structure representing an affine basis of an affine space.
 * `affine_basis.coord`: the map `P →ᵃ[k] k` corresponding to `i : ι`.
 * `affine_basis.coord_apply_eq`: the behaviour of `affine_basis.coord i` on `p i`.
 * `affine_basis.coord_apply_ne`: the behaviour of `affine_basis.coord i` on `p j` when `j ≠ i`.
 * `affine_basis.coord_apply`: the behaviour of `affine_basis.coord i` on `p j` for general `j`.
 * `affine_basis.coord_apply_combination`: the characterisation of `affine_basis.coord i` in terms
    of affine combinations, i.e., `affine_basis.coord i (w₀ p₀ + w₁ p₁ + ⋯) = wᵢ`.

## TODO

 * Construct the affine equivalence between `P` and `{ f : ι →₀ k | f.sum = 1 }`.

-/

open_locale affine big_operators
open set

universes u₁ u₂ u₃ u₄

/-- An affine basis is a family of affine-independent points whose span is the top subspace. -/
@[protect_proj]
structure affine_basis (ι : Type u₁) (k : Type u₂) {V : Type u₃} (P : Type u₄)
  [add_comm_group V] [affine_space V P] [ring k] [module k V] :=
(to_fun : ι → P)
(ind' : affine_independent k to_fun)
(tot' : affine_span k (range to_fun) = ⊤)

variables {ι ι' k V P : Type*} [add_comm_group V] [affine_space V P]

namespace affine_basis

section ring

variables [ring k] [module k V] (b : affine_basis ι k P) {s : finset ι} {i j : ι} (e : ι ≃ ι')

/-- The unique point in a single-point space is the simplest example of an affine basis. -/
instance : inhabited (affine_basis punit k punit) :=
⟨⟨id, affine_independent_of_subsingleton k id, by simp⟩⟩

include V

instance fun_like : fun_like (affine_basis ι k P) ι (λ _, P) :=
{ coe := affine_basis.to_fun,
  coe_injective' := λ f g h, by cases f; cases g; congr' }

@[ext]
lemma ext {b₁ b₂ : affine_basis ι k P} (h : (b₁ : ι → P) = b₂) : b₁ = b₂ := fun_like.coe_injective h

lemma ind : affine_independent k b := b.ind'
lemma tot : affine_span k (range b) = ⊤ := b.tot'

include b

protected

/-- Composition of an affine basis and an equivalence of index types. -/
def reindex (e : ι ≃ ι') : affine_basis ι' k P :=
⟨b ∘ e.symm, b.ind.comp_embedding e.symm.to_embedding,
  by { rw [e.symm.surjective.range_comp], exact b.3 }⟩

@[simp, norm_cast] lemma coe_reindex : ⇑(b.reindex e) = b ∘ e.symm := rfl
@[simp] lemma reindex_apply (i' : ι') : b.reindex e i' = b (e.symm i') := rfl

@[simp] lemma reindex_refl : b.reindex (equiv.refl _) = b := ext rfl

/-- Given an affine basis for an affine space `P`, if we single out one member of the family, we
obtain a linear basis for the model space `V`.

The linear basis corresponding to the singled-out member `i : ι` is indexed by `{j : ι // j ≠ i}`
and its `j`th element is `b j -ᵥ b i`. (See `basis_of_apply`.) -/
noncomputable def basis_of (i : ι) : basis {j : ι // j ≠ i} k V :=
basis.mk ((affine_independent_iff_linear_independent_vsub k b i).mp b.ind)
begin
  suffices : submodule.span k (range (λ (j : {x // x ≠ i}), b ↑j -ᵥ b i)) =
             vector_span k (range b),
  { rw [this, ← direction_affine_span, b.tot, affine_subspace.direction_top], exact le_rfl },
  conv_rhs { rw ← image_univ, },
  rw vector_span_image_eq_span_vsub_set_right_ne k b (mem_univ i),
  congr,
  ext v,
  simp,
end

@[simp] lemma basis_of_apply (i : ι) (j : {j : ι // j ≠ i}) :
  b.basis_of i j = b ↑j -ᵥ b i :=
by simp [basis_of]

@[simp] lemma basis_of_reindex (i : ι') :
  (b.reindex e).basis_of i =
    (b.basis_of $ e.symm i).reindex (e.subtype_equiv $ λ _, e.eq_symm_apply.not) :=
by { ext j, simp }

/-- The `i`th barycentric coordinate of a point. -/
noncomputable def coord (i : ι) : P →ᵃ[k] k :=
{ to_fun    := λ q, 1 - (b.basis_of i).sum_coords (q -ᵥ b i),
  linear    := -(b.basis_of i).sum_coords,
  map_vadd' := λ q v, by rw [vadd_vsub_assoc, linear_map.map_add, vadd_eq_add, linear_map.neg_apply,
    sub_add_eq_sub_sub_swap, add_comm, sub_eq_add_neg], }

@[simp] lemma linear_eq_sum_coords (i : ι) :
  (b.coord i).linear = -(b.basis_of i).sum_coords :=
rfl

@[simp] lemma coord_reindex (i : ι') :
  (b.reindex e).coord i = b.coord (e.symm i) :=
by { ext, classical, simp [affine_basis.coord] }

@[simp] lemma coord_apply_eq (i : ι) : b.coord i (b i) = 1 :=
by simp only [coord, basis.coe_sum_coords, linear_equiv.map_zero, linear_equiv.coe_coe,
  sub_zero, affine_map.coe_mk, finsupp.sum_zero_index, vsub_self]

@[simp] lemma coord_apply_ne (h : i ≠ j) : b.coord i (b j) = 0 :=
by rw [coord, affine_map.coe_mk, ← subtype.coe_mk j h.symm, ← b.basis_of_apply,
  basis.sum_coords_self_apply, sub_self]

lemma coord_apply [decidable_eq ι] (i j : ι) : b.coord i (b j) = if i = j then 1 else 0 :=
by cases eq_or_ne i j; simp [h]

@[simp] lemma coord_apply_combination_of_mem (hi : i ∈ s) {w : ι → k} (hw : s.sum w = 1) :
  b.coord i (s.affine_combination k b w) = w i :=
begin
  classical,
  simp only [coord_apply, hi, finset.affine_combination_eq_linear_combination, if_true, mul_boole,
    hw, function.comp_app, smul_eq_mul, s.sum_ite_eq, s.map_affine_combination b w hw],
end

@[simp] lemma coord_apply_combination_of_not_mem (hi : i ∉ s) {w : ι → k} (hw : s.sum w = 1) :
  b.coord i (s.affine_combination k b w) = 0 :=
begin
  classical,
  simp only [coord_apply, hi, finset.affine_combination_eq_linear_combination, if_false, mul_boole,
    hw, function.comp_app, smul_eq_mul, s.sum_ite_eq, s.map_affine_combination b w hw],
end

@[simp] lemma sum_coord_apply_eq_one [fintype ι] (q : P) :
  ∑ i, b.coord i q = 1 :=
begin
  have hq : q ∈ affine_span k (range b), { rw b.tot, exact affine_subspace.mem_top k V q, },
  obtain ⟨w, hw, rfl⟩ := eq_affine_combination_of_mem_affine_span_of_fintype hq,
  convert hw,
  ext i,
  exact b.coord_apply_combination_of_mem (finset.mem_univ i) hw,
end

@[simp] lemma affine_combination_coord_eq_self [fintype ι] (q : P) :
  finset.univ.affine_combination k b (λ i, b.coord i q) = q :=
begin
  have hq : q ∈ affine_span k (range b), { rw b.tot, exact affine_subspace.mem_top k V q, },
  obtain ⟨w, hw, rfl⟩ := eq_affine_combination_of_mem_affine_span_of_fintype hq,
  congr,
  ext i,
  exact b.coord_apply_combination_of_mem (finset.mem_univ i) hw,
end

/-- A variant of `affine_basis.affine_combination_coord_eq_self` for the special case when the
affine space is a module so we can talk about linear combinations. -/
@[simp] lemma linear_combination_coord_eq_self [fintype ι] (b : affine_basis ι k V) (v : V) :
  ∑ i, b.coord i v • b i = v :=
begin
  have hb := b.affine_combination_coord_eq_self v,
  rwa finset.univ.affine_combination_eq_linear_combination _ _ (b.sum_coord_apply_eq_one v) at hb,
end

lemma ext_elem [finite ι] {q₁ q₂ : P} (h : ∀ i, b.coord i q₁ = b.coord i q₂) : q₁ = q₂ :=
begin
  casesI nonempty_fintype ι,
  rw [← b.affine_combination_coord_eq_self q₁, ← b.affine_combination_coord_eq_self q₂],
  simp only [h],
end

@[simp] lemma coe_coord_of_subsingleton_eq_one [subsingleton ι] (i : ι) :
  (b.coord i : P → k) = 1 :=
begin
  ext q,
  have hp : (range b).subsingleton,
  { rw ← image_univ,
    apply subsingleton.image,
    apply subsingleton_of_subsingleton, },
  haveI := affine_subspace.subsingleton_of_subsingleton_span_eq_top hp b.tot,
  let s : finset ι := {i},
  have hi : i ∈ s, { simp, },
  have hw : s.sum (function.const ι (1 : k)) = 1, { simp, },
  have hq : q = s.affine_combination k b (function.const ι (1 : k)), { simp, },
  rw [pi.one_apply, hq, b.coord_apply_combination_of_mem hi hw],
end

lemma surjective_coord [nontrivial ι] (i : ι) :
  function.surjective $ b.coord i :=
begin
  classical,
  intros x,
  obtain ⟨j, hij⟩ := exists_ne i,
  let s : finset ι := {i, j},
  have hi : i ∈ s, { simp, },
  have hj : j ∈ s, { simp, },
  let w : ι → k := λ j', if j' = i then x else 1-x,
  have hw : s.sum w = 1, { simp [hij, finset.sum_ite, finset.filter_insert, finset.filter_eq'], },
  use s.affine_combination k b w,
  simp [b.coord_apply_combination_of_mem hi hw],
end

/-- Barycentric coordinates as an affine map. -/
noncomputable def coords : P →ᵃ[k] ι → k :=
{ to_fun    := λ q i, b.coord i q,
  linear    :=
  { to_fun    := λ v i, -(b.basis_of i).sum_coords v,
    map_add'  := λ v w, by { ext i, simp only [linear_map.map_add, pi.add_apply, neg_add], },
    map_smul' := λ t v, by { ext i, simpa only [linear_map.map_smul, pi.smul_apply, smul_neg] } },
  map_vadd' := λ p v, by
    { ext i,
      simp only [linear_eq_sum_coords, linear_map.coe_mk, linear_map.neg_apply, pi.vadd_apply',
        affine_map.map_vadd], }, }

@[simp] lemma coords_apply (q : P) (i : ι) :
  b.coords q i = b.coord i q :=
rfl

end ring

section division_ring

variables [division_ring k] [module k V]
include V

@[simp] lemma coord_apply_centroid [char_zero k] (b : affine_basis ι k P) {s : finset ι} {i : ι}
  (hi : i ∈ s) :
  b.coord i (s.centroid k b) = (s.card : k) ⁻¹ :=
by rw [finset.centroid, b.coord_apply_combination_of_mem hi
  (s.sum_centroid_weights_eq_one_of_nonempty _ ⟨i, hi⟩), finset.centroid_weights]

lemma exists_affine_subbasis {t : set P} (ht : affine_span k t = ⊤) :
  ∃ (s ⊆ t) (b : affine_basis ↥s k P), ⇑b = coe :=
begin
  obtain ⟨s, hst, h_tot, h_ind⟩ := exists_affine_independent k V t,
  refine ⟨s, hst, ⟨coe, h_ind, _⟩, rfl⟩,
  rw [subtype.range_coe, h_tot, ht]
end

variables (k V P)

lemma exists_affine_basis : ∃ (s : set P) (b : affine_basis ↥s k P), ⇑b = coe :=
let ⟨s, _, hs⟩ := exists_affine_subbasis (affine_subspace.span_univ k V P) in ⟨s, hs⟩

end division_ring

end affine_basis


text:
universe u

inductive vector (α : Type u) : nat → Type u
| nil {} : vector 0
| cons   : Π {n}, α → vector n → vector (n+1)

namespace vector
local notation h :: t := cons h t

#check @vector.cases_on
-- Π {α : Type}
--   {C : Π (a : ℕ), vector α a → Type}
--   {a : ℕ}
--   (n : vector α a),
--   (e1 : C 0 nil)
--   (e2 : Π {n : ℕ} (a : α) (a_1 : vector α n),
--           C (n + 1) (cons a a_1)),
--   C a n

def vap_cons {α: Type}: Π {n: nat}, α → vector α n → vector α (n+1)
| 0 h nil := cons h nil
| (n+1) h (h2::t) := h::(vap_cons h2 t)

def to_l {α : Type} {n: nat} (v: vector α n): { l : list α // l.length = n} := begin
induction n, exact ⟨[], rfl⟩,
case nat.succ: n ih {
  cases v with α h t,
  let l1 := (ih t),
  let l2 := list.cons h l1.val,
  have: list.length l2 = n + 1, by {
    simp [list.length_cons l2],
    rw [l1.2, nat.add_comm],
  },
  exact ⟨l2, this⟩
}
end

lemma nat_add_eq_eq (a b c: nat) (h: a + c = b + c): a = b := begin
induction c, exact h,
case nat.succ: c ih {
  simp [nat.add_succ] at h,
  exact (ih h)
}
end

def from_l {α : Type}: Π {n: nat}, { l: list α // l.length = n} -> vector α n
| 0 ⟨[], _⟩ := nil
| (n+1) ⟨list.cons h t, p⟩ := begin
  have: list.length t = n, by {
    rw [list.length_cons h t] at p,
    rw [nat_add_eq_eq (list.length t) n 1],
    assumption,
  },
  exact (h::(from_l ⟨t, this⟩))
end

theorem triv (m n: nat): m + n + 1 = m + 1 + n := by simp[add_comm]

def vappend {α : Type} : Π {m n}, vector α m -> vector α n -> vector α (m+n)
| 0 0 nil nil := nil
| m 0 v nil := v
| 0 (n+1) nil (h::v) := h::(vappend nil v)
| (m+1) n (h::u) v :=
  let l := to_l (h::(vappend u v)) in
  let l': { l : list α // list.length l = (m+1+n) } := ⟨l.1, (triv m n) ▸ l.2⟩ in
  from_l l'
.
end vector

author: ntabee

repo: lean-exercise

save_path: github-repos/lean/ntabee-lean-exercise


text:
-- Chapter 2
namespace ch2

/-
1. Define the function Do_Twice
-/
def Do_Twice (f: ℕ → ℕ) (n : ℕ) : ℕ := f (f n)

#check Do_Twice
#reduce Do_Twice (λ x, x * 3) 2

/-
2. Define the functions curry and uncurry
-/

def curry (f : ℕ × ℕ → ℕ) (a b : ℕ) : ℕ := f (a, b)
def uncurry (f : ℕ → ℕ → ℕ) (c : ℕ × ℕ) : ℕ := f c.1 c.2

/-
3. Above, we used the example vec α n for vectors of elements of type α of
length n. Declare a constant vec_add that could represent a function that adds
two vectors of natural numbers of the same length, and a constant vec_reverse
that can represent a function that reverses its argument. Use implicit arguments
for parameters that can be inferred. Declare some variables and check some
expressions involving the constants that you have declared.
-/

universe u
variables {α : Type u} {n m o : ℕ}

constant vector : Type u → ℕ -> Type u

namespace vector
  constant empty : vector α 0
  constant cons : α → vector α n → vector α (n + 1)

  #check empty
  #check cons 1 empty
  #check (cons 5 (cons 10 (cons 3 (empty))))

  constant add : vector α n → vector α m -> vector α (n + m)
  #check add (cons 1 (cons 2 (empty))) (cons 3 (empty))

  constant reverse : vector α n → vector α n
  #check reverse (cons 1 (cons 2 (empty)))
end vector

/-
4. Similarly, declare a constant matrix so that matrix α m n could
represent the type of m by n matrices. Declare some constants to
represent functions on this type, such as matrix addition and
multiplication, and (using vec) multiplication of a matrix by a
vector. Once again, declare some variables and check some
expressions involving the constants that you have declared.
-/

constant matrix : Type u → ℕ → ℕ → Type u

namespace matrix
end matrix
  constant add : matrix α n m → matrix α n m → matrix α n m
  constant mult : matrix α n m → matrix α m o → matrix α n o
end ch2

-- Chapter 3
namespace ch3
/-
1. Prove as many identities from the previous section as you can, replacing the “sorry” placeholders with actual proofs.
-/
universe u
variables p q r s : Prop

def id {α : Type u} (a : α) : α := a

-- Explicit (de)structuring
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
iff.intro
  (assume h : (p ∧ q) ∧ r,
    show p ∧ (q ∧ r), from
      and.intro
        (and.left (and.left h))
        (and.intro
          (and.right (and.left h))
          (and.right h)))
  (assume h : p ∧ (q ∧ r),
    show (p ∧ q) ∧ r, from
      and.intro
        (and.intro
          (and.left h)
          (and.left (and.right h)))
        (and.right (and.right h)))

#check @or.inr

-- Alternate form
example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
iff.intro
  (λ h, ⟨h.left.left, h.left.right, h.right⟩)
  (λ h, ⟨⟨h.left, h.right.left⟩, h.right.right⟩)

#check p ∨ (q ∨ r)

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
iff.intro
  (assume h : (p ∨ q) ∨ r,
    h.elim (λ i, i.elim or.inl (or.inr ∘ or.inl)) (or.inr ∘ or.inr))
  (assume h : p ∨ (q ∨ r),
    h.elim (or.inl ∘ or.inl) (λ i, i.elim (or.inl ∘ or.inr) or.inr))

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
iff.intro
  (λ h, h.elim (λ i, i.elim or.inl (or.inr ∘ or.inl)) (or.inr ∘ or.inr))
  (λ h, h.elim (or.inl ∘ or.inl) (λ i, i.elim (or.inl ∘ or.inr) or.inr))

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
iff.intro
  (assume h : p ∧ (q ∨ r),
    have hp : p, from and.left h,
    have hqr : q ∨ r, from and.right h,
    show (p ∧ q) ∨ (p ∧ r),
      from hqr.elim (assume hq : q, or.inl ⟨hp, hq⟩)
                    (assume hr : r, or.inr ⟨hp, hr⟩))
  (assume h : (p ∧ q) ∨ (p ∧ r),
    show p ∧ (q ∨ r), from
    h.elim
      (assume i : p ∧ q, ⟨and.left i, or.inl (and.right i)⟩)
      (assume i : p ∧ r, ⟨and.left i, or.inr (and.right i)⟩))

example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
iff.intro
  (assume h : p ∨ (q ∧ r), h.elim (λ p, ⟨or.inl p, or.inl p⟩) (λ qr, ⟨or.inr (and.left qr), or.inr (and.right qr)⟩))
  (assume h : (p ∨ q) ∧ (p ∨ r),
    h.left.elim or.inl (λ q', h.right.elim or.inl (λ r', or.inr ⟨q', r'⟩)))

example: (p → (q → r)) ↔ (p ∧ q → r) :=
iff.intro
  (assume f, λ p, f p.1 p.2)
  (assume g, λ a, λ b, g ⟨a, b⟩)

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
iff.intro
  (assume f, ⟨f ∘ or.inl, f ∘ or.inr⟩)
  (assume h, λ pq, pq.elim h.left h.right)

example: ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
iff.intro
  (assume npq : ¬(p ∨ q), ⟨npq ∘ or.inl, npq ∘ or.inr⟩)
  (assume h : ¬p ∧ ¬q, assume pq, pq.elim h.left h.right)

example: ¬p ∨ ¬q → ¬(p ∧ q) :=
assume h : ¬p ∨ ¬q,
assume pq : p ∧ q,
h.elim (λ np, np pq.left) (λ nq, nq pq.right)

example : ¬(p ∧ ¬p) := λ h, absurd h.left h.right

example: p ∧ ¬q → ¬(p → q) := λ pnq h, absurd (h pnq.left) pnq.right

example: ¬p → (p → q) := λ np p, absurd p np

example: (¬p ∨ q) → (p → q) :=
  assume npq : ¬p ∨ q,
  assume hp : p,
  npq.elim (absurd hp) (λ q, q)

example : p ∨ false ↔ p :=
iff.intro
  (λ h, h.elim (λ p, p) false.elim)
  or.inl

example : p ∧ false ↔ false :=
iff.intro and.right false.elim

example : (p → q) → (¬q → ¬p) := λ pq nq, nq ∘ pq

namespace with_classical
open classical

example : ¬(p ↔ ¬p) :=
assume h : p ↔ ¬p,
(em p).elim
  (λ p, h.mp p p)
  (λ np, absurd (h.mpr np) np)

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
assume f,
(em r).elim
  (λ r, or.inl (λ _, r))
  (λ nr, or.inr (λ p, (f p).elim (λ r, absurd r nr) (λ s, s)))

example : ¬(p ∧ q) → ¬p ∨ ¬q :=
assume npq : ¬(p ∧ q),
(em p).elim (λ hp, (em q).elim (λ hq, absurd (and.intro hp hq) npq) or.inr) or.inl

example : ¬(p → q) → p ∧ ¬q :=
assume npq : ¬(p → q),
(em p).elim
  -- (λ p, ⟨p, λ q, npq (λ _, q)⟩)
  (assume hp : p,
    have nq : ¬q, from (λ q', npq (λ _, q')),
    show p ∧ ¬q, from ⟨hp, nq⟩)
  (assume hnp : ¬p,
    have pq : p → q, from (λ p, absurd p hnp),
    absurd pq npq)

example : (p → q) → (¬p ∨ q) :=
(em p).elim
  (λ p pq, or.inr (pq p))
  (λ np _, or.inl np)

example : (¬q → ¬p) → (p → q) :=
(em q).elim
  (λ q _ _, q)
  (λ nq nqp p, absurd p (nqp nq))

example : p ∨ ¬p := by exact (em p)

example : (((p → q) → p) → p) :=
(em q).elim
  (λ q f, f (λ _, q))
  ((em p).elim
    (λ p _ _, p)
    (λ np nq f, f (λ p', absurd p' np)))

end with_classical

/-
2. Prove ¬(p ↔ ¬p) without using classical logic.
-/

example (p : Prop): ¬(p ↔ ¬p) := by simp

-- TODO: Provide a direct proof
example (p : Prop): ¬(p ↔ ¬p) := sorry

end ch3

-- Chapter 4
namespace ch4

namespace ex1
/-
Prove these equivalences.
You should also try to understand why the reverse implication is not derivable
in the last example.
-/

variables (α : Type) (p q : α → Prop)

example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
iff.intro
  (λ h, ⟨λ y, (h y).left, λ y, (h y).right⟩)
  (λ h x, ⟨h.left(x), h.right(x)⟩)

example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
assume pq,
assume p,
assume x : α,
show q x, from pq x (p x)

example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
λ pq p x, pq x (p x)

example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
λ h, h.elim (λ px x, or.inl (px x)) (λ qx x, or.inr (qx x))

end ex1

namespace ex2
/-
It is often possible to bring a component of a formula outside a universal
quantifier, when it does not depend on the quantified variable. Try proving
these (one direction of the second of these requires classical logic):
-/

variables (α : Type) (p q : α → Prop)
variable r : Prop

example : α → ((∀ x: α, r) ↔ r) :=
λ y, iff.intro (λ f, f y) (λ r _, r)

open classical
example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r :=
iff.intro
  -- This branch requires classical reasoning
  (λ h, (em r).elim or.inr
    (λ nr, or.inl (λ x, (h x).elim id (λ r, absurd r nr))))
  (λ h x, h.elim (λ px, or.inl(px x)) or.inr)

example : (∀ x, r → p x) ↔ (r → ∀ x, p x) :=
iff.intro (λ f r _, f _ r) (λ f _ r, f r _)

end ex2

namespace ex3
/-
Consider the “barber paradox,” that is, the claim that in a certain town there
is a (male) barber that shaves all and only the men who do not shave themselves.
Prove that this is a contradiction:
-/
variables (men : Type) (barber : men)
variable (shaves : men → men → Prop)

open classical -- This is expedient, but not necessary; c.f. ex 3.2
example (h : ∀ x : men, shaves barber x ↔ ¬ shaves x x) : false :=
(em (shaves barber barber)).elim
  (assume s : shaves barber barber,
  have ns : ¬shaves barber barber, from (h barber).mp(s),
  absurd s ns)
  (assume ns : ¬shaves barber barber,
  have s : shaves barber barber, from (h barber).mpr(ns),
  absurd s ns)

end ex3

namespace ex4
/-
Below, we have put definitions of divides and even in a special namespace to
avoid conflicts with definitions in the library. The instance declaration make
it possible to use the notation m | n for divides m n. Don’t worry about how it
works; you will learn about that later.
-/
def divides (m n: ℕ) : Prop := ∃ k, m * k = n

instance : has_dvd nat := ⟨divides⟩

def even (n: ℕ) : Prop := 2 ∣ n

variables m n : ℕ

#check m ∣ n
#check m ^ n
#check even (m ^ n +3)

/-
Remember that, without any parameters, an expression of type Prop is just an
assertion. Fill in the definitions of prime and Fermat_prime below, and
construct the given assertion. For example, you can say that there are
infinitely many primes by asserting that for every natural number n, there is a
prime number greater than n. Goldbach’s weak conjecture states that every odd
number greater than 5 is the sum of three primes. Look up the definition of a
Fermat prime or any of the other statements, if necessary.
-/

def prime (n : ℕ) : Prop := ∀m, m ∣ n → m = 1 ∨ m = n

def infinitely_many_primes : Prop := ∀ n, ∃ k, k > n ∧ prime k

def Fermat_prime (n : ℕ) : Prop := ∃ k : ℕ, n = 2 ^ (2 ^ k) ∧ prime n

def infinitely_many_Fermat_primes : Prop := ∀ n, ∃ k, k > n ∧ Fermat_prime k

def goldbach_conjecture : Prop := ∀ n, ∃ p₁ p₂, n = p₁ + p₂ ∧ prime p₁ ∧ prime p₂

def Goldbach's_weak_conjecture : Prop := ∀ n, ∃ p₁ p₂ p₃, n = p₁ + p₂ + p₃ ∧ prime p₁ ∧ prime p₂

def Fermat's_last_theorem : Prop :=
  ∀ (a b c n : ℕ), a > 0 -> b > 0 -> c > 0 -> a^n + b^n = c^n -> n ≤ 2

end ex4

namespace ex5
/-
Prove as many of the identities listed in Section 4.4 as you can.
-/

variables (α : Type) (p q : α → Prop)
variable a : α
variable r : Prop

example : (∃ x : α, r) → r := λ ⟨_, hr⟩, hr

example : r → (∃ x : α, r) := λ r, exists.intro a r

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
iff.intro
  (λ ⟨x, pxar⟩, ⟨exists.intro x pxar.left, pxar.right⟩)
  (λ ⟨⟨x, px⟩, r⟩, exists.intro x ⟨px, r⟩)

example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
iff.intro
  (λ ⟨x, pqx⟩, pqx.elim
    (or.inl ∘ exists.intro x)
    (or.inr ∘ exists.intro x))
  (λ h, h.elim
    (λ ⟨x, px⟩, exists.intro x (or.inl px))
    (λ ⟨x, qx⟩, exists.intro x (or.inr qx)))

example : (¬ ∃ x, p x) ↔ (∀ x, ¬ p x) :=
iff.intro
  (λ nep x px, nep (exists.intro x px))
  (λ nax ⟨x, px⟩, nax x px)

example : (∀ x, p x → r) ↔ (∃ x, p x) → r :=
iff.intro
  (λ apxr ⟨x, px⟩, apxr x px)
  (λ epxr _ px, epxr (exists.intro _ px))

open classical
-- TODO: do these all _require_ classical reasoning?

example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) :=
iff.intro
  (λ axpx ⟨_, npx,⟩, npx (axpx _))
  (λ nexnpx x, by_contradiction (λ npx, nexnpx (exists.intro x npx)))

example : (∃ x, p x) ↔ ¬ (∀ x, ¬ p x) :=
iff.intro
  (λ ⟨_, px⟩ axnpx, axnpx _ px)
  sorry

example : (¬ ∀ x, p x) ↔ (∃ x, ¬ p x) :=
iff.intro
  (λ naxpx, sorry)
  (λ ⟨_, npx⟩ axpx, npx (axpx _))

example : (∃ x, p x → r) ↔ (∀ x, p x) → r :=
iff.intro
  (λ ⟨x, pxr⟩ y, pxr(y(x)))
  sorry

example : (∃ x, r → p x) ↔ (r → ∃ x, p x) :=
iff.intro
  (λ ⟨x, rpx⟩ r, exists.intro x (rpx r))
  (λ repx, (em r).elim
    (λ hr, let ⟨x, px⟩ := repx hr in exists.intro x (λ _, px))
    (λ nr, exists.intro a (λ r, absurd r nr)))

end ex5

namespace ex6
/-
Give a calculational proof of the theorem log_mul below.
-/
variables (real : Type) [ordered_ring real]
variables (log exp : real → real)
variable log_exp_eq : ∀ x, log (exp x) = x
variable exp_log_eq : ∀ {x}, x > 0 → exp (log x) = x
variable exp_pos : ∀ x, exp x > 0
variable exp_add : ∀ x y, exp (x + y) = exp x * exp y

-- this ensures the assumptions are available in tactic proofs
include log_exp_eq exp_log_eq exp_pos exp_add

example (x y z : real) :
  exp (x + y + z) = exp x * exp y * exp z :=
by rw [exp_add, exp_add]

example (y : real) (h : y > 0) : exp (log y) = y :=
  exp_log_eq h

theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) :
  log (x * y) = log x + log y :=
calc log (x * y) = log (exp (log x) * y)           : by rw (exp_log_eq hx)
             ... = log (exp (log x) * exp (log y)) : by rw (exp_log_eq hy)
             ... = log (exp (log x + log y))       : by rw ←exp_add
             ... = log x + log y                   : by rw log_exp_eq

end ex6

namespace ex7
/-
Prove the theorem below, using only the ring properties of Z enumerated in
Section 4.2 and the theorem sub_self
-/

#check sub_self
example (x: ℤ) : x * 0 = 0 :=
calc x * 0 = x * (1 - 1)   : by rw ←sub_self
       ... = x * 1 - x * 1 : by rw mul_sub
       ... = 0             : by rw sub_self

example (x: ℤ) : x * 0 = 0 :=
by simp [sub_self, mul_sub]

end ex7

end ch4

namespace ch5

namespace scratch

example (p q : Prop) : p ∨ q → q ∨ p :=
begin
  intro h,
  cases h with hp hq,
  right, exact hp,
  left, exact hq
end

example (p q : Prop) : p ∧ q → q ∧ p :=
begin
  intro h,
  cases h with hp hq,
  constructor, exact hq, exact hp
end

example (p q r : Prop) : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
begin
  apply iff.intro,
  intro h,
    cases h with hp hqr,
    cases hqr with hq hr,
      left, constructor, repeat { assumption },
      right, constructor, repeat { assumption },
  intro h,
    cases h with hpq hpr,
      cases hpq with hp hq,
        constructor, exact hp, left, exact hq,
      cases hpr with hp hr,
        constructor, exact hp, right, exact hr
end

example (p q : ℕ → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x :=
begin
  intro h,
  cases h with x px,
  constructor, left, exact px
end

example (p q : ℕ → Prop) : (∃ x, p x) → ∃ x, p x ∨ q x :=
begin
  intro h,
  cases h with x px,
  existsi x, left, exact px
end

example (p q: ℕ → Prop): (∃ x, p x ∧ q x) → ∃ x,q x ∧ p x :=
begin
  intro h,
  cases h with x hpq,
  cases hpq with hp hq,
  existsi x,
  split; assumption
end

universes u v

def swap_pair {α : Type u} {β : Type v} : α × β → β × α :=
begin
  intro p,
  cases p with ha hb,
  split ; assumption
end

#reduce swap_pair (1, 2)

def swap_sum {α : Type u} {β : Type v} : α ⊕ β → β ⊕ α :=
begin
  intro p,
  cases p with ha hb,
  right, exact ha,
  left, exact hb
end

open nat

example (P : ℕ → Prop) (h₀ : P 0) (h₁ : ∀ n, P (succ n)) (m : ℕ) :=
begin
  cases m with m', exact h₀, exact h₁ m'
end

example (p q : Prop) : p ∧ ¬ p → q :=
begin
  intro h,
  cases h,
  contradiction
end

example (p q r : Prop) : p ∧ (q ∨ r) → (p ∧ q) ∨ (p ∧ r) :=
begin
  intro h,
  cases h with hp hqr,
  cases hqr with hq hr,
    left, exact ⟨hp, hq⟩,
    right, exact ⟨hp, hr⟩
end

end scratch

namespace ex1
/-
Go back to the exercises in Chapter 3 and Chapter 4 and redo as many as you can
now with tactic proofs, using also rw and simp as appropriate.
-/

namespace from_chapter_3

universe u
variables p q r s : Prop

def id {α : Type u} (a : α) : α := a

example : (p ∧ q) ∧ r ↔ p ∧ (q ∧ r) :=
begin
  apply iff.intro,
  intro h,
    cases h with hpq hr,
    cases hpq with hp hq,
    constructor, assumption,
    constructor; assumption,
  intro h,
    cases h with hp hqr,
    cases hqr with hq hr,
    repeat { constructor }; assumption
end

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
begin
  apply iff.intro,
  intro h,
    cases h with hpq hr,
    cases hpq with hp hq,
    left, exact hp,
    right, left, exact hq,
    right, right, exact hr,
  intro h,
    cases h with hp hqr,
    left, left, exact hp,
    cases hqr with hq hr,
    left, right, exact hq,
    right, exact hr
end

example : (p ∨ q) ∨ r ↔ p ∨ (q ∨ r) :=
sorry

example : p ∧ (q ∨ r) ↔ (p ∧ q) ∨ (p ∧ r) :=
sorry

example : p ∨ (q ∧ r) ↔ (p ∨ q) ∧ (p ∨ r) :=
sorry

example: (p → (q → r)) ↔ (p ∧ q → r) :=
sorry

example : ((p ∨ q) → r) ↔ (p → r) ∧ (q → r) :=
sorry

example: ¬(p ∨ q) ↔ ¬p ∧ ¬q :=
sorry

example: ¬p ∨ ¬q → ¬(p ∧ q) :=
sorry

example : ¬(p ∧ ¬p) := by simp

example: p ∧ ¬q → ¬(p → q) :=
sorry

example: ¬p → (p → q) :=
sorry

example: (¬p ∨ q) → (p → q) :=
sorry

example : p ∨ false ↔ p := by simp

example : p ∧ false ↔ false := by simp

example : (p → q) → (¬q → ¬p) :=
sorry

namespace with_classical
open classical

example : ¬(p ↔ ¬p) :=
sorry

example : (p → r ∨ s) → ((p → r) ∨ (p → s)) :=
sorry

example : ¬(p ∧ q) → ¬p ∨ ¬q :=
sorry

example : ¬(p → q) → p ∧ ¬q :=
begin
  intro h,
  cases (em p) with hp np,
    constructor,
      exact hp,
      assume hq : q,
      have : p → q := λ _, hq,
      exact (h this),
    have : p → q, by { intro, contradiction },
      contradiction
end

example : (p → q) → (¬p ∨ q) :=
sorry

example : (¬q → ¬p) → (p → q) :=
sorry

example : p ∨ ¬p := em p

example : (((p → q) → p) → p) :=
sorry

end with_classical
end from_chapter_3
end ex1

namespace ex2
/-
Use tactic combinators to obtain a one line proof of the following:
-/
example (p q r : Prop) (hp : p) :
(p ∨ q ∨ r) ∧ (q ∨ p ∨ r) ∧ (q ∨ r ∨ p) :=
by simp [hp]

end ex2

end ch5

/- Chapter 6 -/
namespace ch6

namespace scratch

namespace x

universe u
variables {α : Type u} (r : α → α → Prop)

def reflexive : Prop := ∀ (a : α), r a a
def symmetric : Prop := ∀ {a b : α}, r a b → r b a
def transitive : Prop := ∀ {a b c : α}, r a b → r b c → r a c
def euclidean : Prop := ∀ {a b c : α}, r a b → r a c → r b c

variable {r}

theorem th1 (reflr : reflexive r) (euclr : euclidean r) :
  symmetric r :=
assume (a b : α),
assume : r a b,
show r b a, from euclr this (reflr _)

theorem th2 (symmr : symmetric r) (euclr : euclidean r) :
  transitive r :=
assume (a b c : α),
assume rab : r a b,
assume rbc : r b c,
show r a c, from euclr (symmr rab) rbc

theorem th3 (reflr : reflexive r) (euclr : euclidean r) :
  transitive r :=
@th2 _ _ (@th1 _ _ reflr @euclr) @euclr

end x

namespace y

universe u
variables {α : Type u} (r : α → α → Prop)

def reflexive : Prop := ∀ (a : α), r a a
def symmetric : Prop := ∀ ⦃ a b : α ⦄ , r a b → r b a
def transitive : Prop := ∀ ⦃ a b c : α ⦄, r a b → r b c → r a c
def euclidean : Prop := ∀ ⦃ a b c : α ⦄, r a b → r a c → r b c

variable {r}

theorem th1 (reflr : reflexive r) (euclr : euclidean r) :
  symmetric r :=
assume (a b : α),
assume : r a b,
show r b a, from euclr this (reflr _)

theorem th2 (symmr : symmetric r) (euclr : euclidean r) :
  transitive r :=
assume (a b c : α),
assume rab : r a b,
assume rbc : r b c,
show r a c, from euclr (symmr rab) rbc

theorem th3 (reflr : reflexive r) (euclr : euclidean r) :
  transitive r := th2 (th1 reflr euclr) euclr

end y

end scratch

end ch6

author: jamesdabbs

repo: proofs

save_path: github-repos/lean/jamesdabbs-proofs


text:
/-
Copyright (c) 2021 Kalle Kytölä. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Kalle Kytölä
-/
import tactic
import measure_theory.measurable_space
import measure_theory.integration
import measure_theory.borel_space
import measure_theory.bochner_integration
import topology.metric_space.basic
import topology.instances.real
import topology.instances.ennreal
import order.liminf_limsup
import portmanteau_definitions
import portmanteau_integrals
import portmanteau_cont_imp_closed
import portmanteau_open_imp_cont
import portmanteau_open_closed_imp_borel
import portmanteau_borel_imp_closed_cond

noncomputable theory
open set
open classical
open measure_theory
open measurable_space
open filter
open_locale topological_space

namespace portmanteau

section concluding_the_equivalence_of_portmanteau_conditions

/-- `tfae_weak_conv_seq'` :
    Equivalent conditions for the weak convergence of a sequence of Borel probability
    measures on a topological space, in terms of integrals of bounded continuous functions.
    The second of these is the "textbook definition".
    (Further equivalent conditions can be obtained if one assumes that the space is a
    complete separable metric space, or at least that it is a metric space, or at least
    that indicators of all closed sets have decreasing continuous bounded approximations.) -/
theorem tfae_weak_conv_seq' {α : Type*} [topological_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tfae  [ tendsto μseq at_top (𝓝 μ) ,
            ∀ (f : α → ℝ) , continuous f → bdd_Rval f →
              tendsto (λ n, (@integral α ℝ (borel(α)) _ _ _ _ _ _ (μseq(n)) f)) at_top (𝓝 (@integral α ℝ (borel(α)) _ _ _ _ _ _ μ f)) ,
            ∀ (f : cont_bdd_ennval α) ,
              tendsto (λ n, integrate_cont_bdd_ennval (μseq(n)) f) at_top (𝓝 (integrate_cont_bdd_ennval μ f)) ] :=
begin
  have equiv₁ := @weak_conv_seq_iff α _ μseq μ ,
  have equiv₂ := @weak_conv_seq_iff' α _ μseq μ ,
  tfae_finish ,
end

theorem weak_conv_seq_iff_portmanteau_open' {α : Type*} [metric_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tendsto μseq at_top (𝓝 μ)
      ↔ portmanteau_open (λ n , (μseq(n)).val) μ.val :=
begin
  split ,
  { intros hdefcond ,
    have hcontcond := weak_conv_seq_iff_portmanteau_continuous_ennval.mp hdefcond,
    have has_approx := metric_space_has_cont_approx_of_closed α ,
    have hclcond := @portmanteau_continuous_imp_closed_cond α _ has_approx (λ n , (μseq(n)).val) (λ n , (μseq(n)).prop) μ.val μ.prop hcontcond ,
    exact (portmanteau_closed_and_open_cond_equivalent (λ n , (μseq(n)).val) (λ n , (μseq(n)).prop) μ.val μ.prop).mp hclcond , } ,
  { intros hopcond ,
    have textbook' := portmanteau_open_imp_cont (λ n , (μseq(n)).val) (λ n , (μseq(n)).prop) μ.val μ.prop hopcond ,
    apply weak_conv_seq_iff'.mpr ,
    intros f ,
    exact textbook' f.val f.prop.1 f.prop.2 , } ,
end

/-- `weak_conv_seq_iff_portmanteau_open'` :
    Equivalent characterization for the weak convergence of a sequence of Borel probability
    measures using open sets. -/
theorem weak_conv_seq_iff_portmanteau_open {α : Type*} [metric_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tendsto μseq at_top (𝓝 μ)
      ↔ ( ∀ (G : set α) , (is_open G) → μ(G) ≤ liminf at_top (λ n , (μseq(n))(G)) ) :=
begin
  split ,
  { intros h ,
    exact weak_conv_seq_iff_portmanteau_open'.mp h , } ,
  { intros h ,
    exact weak_conv_seq_iff_portmanteau_open'.mpr h , } ,
end

theorem weak_conv_seq_iff_portmanteau_closed' {α : Type*} [metric_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tendsto μseq at_top (𝓝 μ)
      ↔ portmanteau_closed (λ n , (μseq(n)).val) μ.val :=
begin
  have eq_open_closed := portmanteau_closed_and_open_cond_equivalent (λ n , (μseq(n)).val) (λ n , (μseq(n)).prop) μ.val μ.prop ,
  have eq_open_def := @weak_conv_seq_iff_portmanteau_open' _ _ μseq μ ,
  cc ,
end

/-- `weak_conv_seq_iff_portmanteau_closed'` :
    Equivalent characterization for the weak convergence of a sequence of Borel probability
    measures using closed sets. -/
theorem weak_conv_seq_iff_portmanteau_closed {α : Type*} [metric_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tendsto μseq at_top (𝓝 μ)
      ↔ ( ∀ (F : set α) , (is_closed F) → limsup at_top (λ n , (μseq(n))(F)) ≤ μ(F) ) :=
begin
  split ,
  { intros h ,
    exact weak_conv_seq_iff_portmanteau_closed'.mp h , } ,
  { intros h ,
    exact weak_conv_seq_iff_portmanteau_closed'.mpr h , } ,
end

theorem weak_conv_seq_iff_portmanteau_borel' {α : Type*} [metric_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tendsto μseq at_top (𝓝 μ)
      ↔ portmanteau_borel (λ n , (μseq(n)).val) μ.val :=
begin
  have closed_imp_borel := portmanteau_closed_imp_borel (λ n , (μseq(n)).val) (λ n , (μseq(n)).prop) μ.val μ.prop ,
  have borel_imp_closed := portmanteau_borel_imp_closed (λ n , (μseq(n)).val) (λ n , (μseq(n)).prop) μ.val μ.prop ,
  have eq_closed_def := @weak_conv_seq_iff_portmanteau_closed _ _ μseq μ ,
  split ,
  { intros hdefcond ,
    exact closed_imp_borel (eq_closed_def.mp hdefcond) , } ,
  { intros hborcond ,
    exact eq_closed_def.mpr (borel_imp_closed hborcond) , } ,
end

/-- `weak_conv_seq_iff_portmanteau_borel'` :
    Equivalent characterization for the weak convergence of a sequence of Borel probability
    measures using Borel sets whose frontiers (boundaries) carry no probability mass in the
    limit measure. -/
theorem weak_conv_seq_iff_portmanteau_borel {α : Type*} [metric_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tendsto μseq at_top (𝓝 μ)
      ↔ ( ∀ (E : set α) , (borel_set(α) E) → (μ(frontier E) = 0)
          → (tendsto (λ n , (μseq(n))(E)) at_top (𝓝 (μ(E))) ) ) :=
begin
  split ,
  { intros h ,
    exact weak_conv_seq_iff_portmanteau_borel'.mp h , } ,
  { intros h ,
    exact weak_conv_seq_iff_portmanteau_borel'.mpr h , } ,
end

/-- `tfae_weak_conv_seq` :
    Equivalent conditions for the weak convergence of a sequence of Borel probability
    measures on a metric space. -/
theorem tfae_weak_conv_seq {α : Type*} [metric_space α]
  {μseq : ℕ → borel_proba α} {μ : borel_proba α} :
    tfae  [ tendsto μseq at_top (𝓝 μ) ,
            ∀ (f : α → ℝ) , continuous f → bdd_Rval f →
              tendsto (λ n, (@integral α ℝ (borel(α)) _ _ _ _ _ _ (μseq(n)) f)) at_top (𝓝 (@integral α ℝ (borel(α)) _ _ _ _ _ _ μ f)) ,
            ∀ (f : cont_bdd_ennval α) ,
              tendsto (λ n, integrate_cont_bdd_ennval (μseq(n)) f) at_top (𝓝 (integrate_cont_bdd_ennval μ f)) ,
            ( ∀ (G : set α) , (is_open G) → μ(G) ≤ liminf at_top (λ n , (μseq(n))(G)) ) ,
            ( ∀ (F : set α) , (is_closed F) → limsup at_top (λ n , (μseq(n))(F)) ≤ μ(F) ) ,
            ( ∀ (E : set α) , (borel_set(α) E) → (μ(frontier E) = 0) → (tendsto (λ n , (μseq(n))(E)) at_top (𝓝 (μ(E))) ) ) ] :=
begin
  have equiv₁ := @weak_conv_seq_iff α _ μseq μ ,
  have equiv₂ := @weak_conv_seq_iff' α _ μseq μ ,
  have equiv₃ := @weak_conv_seq_iff_portmanteau_open α _ μseq μ ,
  have equiv₄ := @weak_conv_seq_iff_portmanteau_closed α _ μseq μ ,
  have equiv₅ := @weak_conv_seq_iff_portmanteau_borel α _ μseq μ ,
  tfae_finish ,
end

end concluding_the_equivalence_of_portmanteau_conditions

end portmanteau

author: kkytola


text:
def P := 0 = 0
def Q := 1 = 1
#check Q

lemma proofP : P := eq.refl 0
lemma proofQ : Q := sorry

theorem and1 : P ∧ Q
    := and.intro proofP proofQ
#check and1
#check and.intro proofQ proofP

theorem pfPQ : P ∧ Q :=
begin
    apply and.intro,
    exact eq.refl 0,
    exact eq.refl 1
end

theorem pfPQ' : P ∧ Q :=
begin
    have A := eq.refl 0,
    have B := eq.refl 1,
    apply and.intro A B
end

#check and.right pfPQ

axiom f : false
#check f

theorem zeroEqualToOne : "" = "asghar" := false.elim f
#check zeroEqualToOne

theorem pfPnP : P ∧ ¬P := sorry
#check pfPnP

theorem pfParrQ : P ∧ ¬P -> false := sorry

#check pfParrQ pfPnP

author: osoulim

repo: LEAN

save_path: github-repos/lean/osoulim-LEAN