text:
/-
Copyright (c) 2018 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.category_theory.natural_isomorphism
import Mathlib.data.equiv.basic
import Mathlib.PostPort

universes v₁ v₂ u₁ u₂ l v₃ u₃

namespace Mathlib

namespace category_theory

/--
A functor `F : C ⥤ D` is full if for each `X Y : C`, `F.map` is surjective.
In fact, we use a constructive definition, so the `full F` typeclass contains data,
specifying a particular preimage of each `f : F.obj X ⟶ F.obj Y`.

See https://stacks.math.columbia.edu/tag/001C.
-/
class full {C : Type u₁} [category C] {D : Type u₂} [category D] (F : C ⥤ D) where
  preimage : {X Y : C} → (functor.obj F X ⟶ functor.obj F Y) → (X ⟶ Y)
  witness' :
    autoParam (∀ {X Y : C} (f : functor.obj F X ⟶ functor.obj F Y), functor.map F (preimage f) = f)
      (Lean.Syntax.ident Lean.SourceInfo.none (String.toSubstring "Mathlib.obviously")
        (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Mathlib") "obviously") [])

@[simp] theorem full.witness {C : Type u₁} [category C] {D : Type u₂} [category D] {F : C ⥤ D}
    [c : full F] {X : C} {Y : C} (f : functor.obj F X ⟶ functor.obj F Y) :
    functor.map F (full.preimage f) = f :=
  sorry

/--
A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective.

See https://stacks.math.columbia.edu/tag/001C.
-/
class faithful {C : Type u₁} [category C] {D : Type u₂} [category D] (F : C ⥤ D) where
  map_injective' :
    autoParam (∀ {X Y : C}, function.injective (functor.map F))
      (Lean.Syntax.ident Lean.SourceInfo.none (String.toSubstring "Mathlib.obviously")
        (Lean.Name.mkStr (Lean.Name.mkStr Lean.Name.anonymous "Mathlib") "obviously") [])

theorem faithful.map_injective {C : Type u₁} [category C] {D : Type u₂} [category D] (F : C ⥤ D)
    [c : faithful F] {X : C} {Y : C} : function.injective (functor.map F) :=
  sorry

namespace functor

theorem map_injective {C : Type u₁} [category C] {D : Type u₂} [category D] (F : C ⥤ D) [faithful F]
    {X : C} {Y : C} : function.injective (map F) :=
  faithful.map_injective F

/-- The specified preimage of a morphism under a full functor. -/
def preimage {C : Type u₁} [category C] {D : Type u₂} [category D] (F : C ⥤ D) [full F] {X : C}
    {Y : C} (f : obj F X ⟶ obj F Y) : X ⟶ Y :=
  full.preimage f

@[simp] theorem image_preimage {C : Type u₁} [category C] {D : Type u₂} [category D] (F : C ⥤ D)
    [full F] {X : C} {Y : C} (f : obj F X ⟶ obj F Y) : map F (preimage F f) = f :=
  sorry

end functor

@[simp] theorem preimage_id {C : Type u₁} [category C] {D : Type u₂} [category D] {F : C ⥤ D}
    [full F] [faithful F] {X : C} : functor.preimage F 𝟙 = 𝟙 :=
  sorry

@[simp] theorem preimage_comp {C : Type u₁} [category C] {D : Type u₂} [category D] {F : C ⥤ D}
    [full F] [faithful F] {X : C} {Y : C} {Z : C} (f : functor.obj F X ⟶ functor.obj F Y)
    (g : functor.obj F Y ⟶ functor.obj F Z) :
    functor.preimage F (f ≫ g) = functor.preimage F f ≫ functor.preimage F g :=
  sorry

@[simp] theorem preimage_map {C : Type u₁} [category C] {D : Type u₂} [category D] {F : C ⥤ D}
    [full F] [faithful F] {X : C} {Y : C} (f : X ⟶ Y) : functor.preimage F (functor.map F f) = f :=
  sorry

/-- If `F : C ⥤ D` is fully faithful, every isomorphism `F.obj X ≅ F.obj Y` has a preimage. -/
def preimage_iso {C : Type u₁} [category C] {D : Type u₂} [category D] {F : C ⥤ D} [full F]
    [faithful F] {X : C} {Y : C} (f : functor.obj F X ≅ functor.obj F Y) : X ≅ Y :=
  iso.mk (functor.preimage F (iso.hom f)) (functor.preimage F (iso.inv f))

@[simp] theorem preimage_iso_hom {C : Type u₁} [category C] {D : Type u₂} [category D] {F : C ⥤ D}
    [full F] [faithful F] {X : C} {Y : C} (f : functor.obj F X ≅ functor.obj F Y) :
    iso.hom (preimage_iso f) = functor.preimage F (iso.hom f) :=
  rfl

@[simp] theorem preimage_iso_inv {C : Type u₁} [category C] {D : Type u₂} [category D] {F : C ⥤ D}
    [full F] [faithful F] {X : C} {Y : C} (f : functor.obj F X ≅ functor.obj F Y) :
    iso.inv (preimage_iso f) = functor.preimage F (iso.inv f) :=
  rfl

@[simp] theorem preimage_iso_map_iso {C : Type u₁} [category C] {D : Type u₂} [category D]
    {F : C ⥤ D} [full F] [faithful F] {X : C} {Y : C} (f : X ≅ Y) :
    preimage_iso (functor.map_iso F f) = f :=
  sorry

/--
If the image of a morphism under a fully faithful functor in an isomorphism,
then the original morphisms is also an isomorphism.
-/
def is_iso_of_fully_faithful {C : Type u₁} [category C] {D : Type u₂} [category D] (F : C ⥤ D)
    [full F] [faithful F] {X : C} {Y : C} (f : X ⟶ Y) [is_iso (functor.map F f)] : is_iso f :=
  is_iso.mk (functor.preimage F (inv (functor.map F f)))

/-- If `F` is fully faithful, we have an equivalence of hom-sets `X ⟶ Y` and `F X ⟶ F Y`. -/
def equiv_of_fully_faithful {C : Type u₁} [category C] {D : Type u₂} [category D] (F : C ⥤ D)
    [full F] [faithful F] {X : C} {Y : C} : (X ⟶ Y) ≃ (functor.obj F X ⟶ functor.obj F Y) :=
  equiv.mk (fun (f : X ⟶ Y) => functor.map F f)
    (fun (f : functor.obj F X ⟶ functor.obj F Y) => functor.preimage F f) sorry sorry

@[simp] theorem equiv_of_fully_faithful_apply {C : Type u₁} [category C] {D : Type u₂} [category D]
    (F : C ⥤ D) [full F] [faithful F] {X : C} {Y : C} (f : X ⟶ Y) :
    coe_fn (equiv_of_fully_faithful F) f = functor.map F f :=
  rfl

@[simp] theorem equiv_of_fully_faithful_symm_apply {C : Type u₁} [category C] {D : Type u₂}
    [category D] (F : C ⥤ D) [full F] [faithful F] {X : C} {Y : C}
    (f : functor.obj F X ⟶ functor.obj F Y) :
    coe_fn (equiv.symm (equiv_of_fully_faithful F)) f = functor.preimage F f :=
  rfl

end category_theory

namespace category_theory

protected instance full.id {C : Type u₁} [category C] : full 𝟭 :=
  full.mk fun (_x _x_1 : C) (f : functor.obj 𝟭 _x ⟶ functor.obj 𝟭 _x_1) => f

protected instance faithful.id {C : Type u₁} [category C] : faithful 𝟭 := faithful.mk

protected instance faithful.comp {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] (F : C ⥤ D) (G : D ⥤ E) [faithful F] [faithful G] : faithful (F ⋙ G) :=
  faithful.mk

theorem faithful.of_comp {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] (F : C ⥤ D) (G : D ⥤ E) [faithful (F ⋙ G)] : faithful F :=
  faithful.mk

theorem faithful.of_iso {C : Type u₁} [category C] {D : Type u₂} [category D] {F : C ⥤ D}
    {F' : C ⥤ D} [faithful F] (α : F ≅ F') : faithful F' :=
  faithful.mk

theorem faithful.of_comp_iso {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : faithful H] (h : F ⋙ G ≅ H) :
    faithful F :=
  faithful.of_comp F G

theorem iso.faithful_of_comp {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : faithful H] (h : F ⋙ G ≅ H) :
    faithful F :=
  faithful.of_comp_iso

-- We could prove this from `faithful.of_comp_iso` using `eq_to_iso`,

-- but that would introduce a cyclic import.

theorem faithful.of_comp_eq {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : faithful H] (h : F ⋙ G = H) :
    faithful F :=
  faithful.of_comp F G

theorem Mathlib.eq.faithful_of_comp {C : Type u₁} [category C] {D : Type u₂} [category D]
    {E : Type u₃} [category E] {F : C ⥤ D} {G : D ⥤ E} {H : C ⥤ E} [ℋ : faithful H]
    (h : F ⋙ G = H) : faithful F :=
  faithful.of_comp_eq

/-- “Divide” a functor by a faithful functor. -/
protected def faithful.div {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] (F : C ⥤ E) (G : D ⥤ E) [faithful G] (obj : C → D)
    (h_obj : ∀ (X : C), functor.obj G (obj X) = functor.obj F X)
    (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y : C} {f : X ⟶ Y}, functor.map G (map f) == functor.map F f) : C ⥤ D :=
  functor.mk obj map

-- This follows immediately from `functor.hext` (`functor.hext h_obj @h_map`),

-- but importing `category_theory.eq_to_hom` causes an import loop:

-- category_theory.eq_to_hom → category_theory.opposites →

-- category_theory.equivalence → category_theory.fully_faithful

theorem faithful.div_comp {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] (F : C ⥤ E) [faithful F] (G : D ⥤ E) [faithful G] (obj : C → D)
    (h_obj : ∀ (X : C), functor.obj G (obj X) = functor.obj F X)
    (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y : C} {f : X ⟶ Y}, functor.map G (map f) == functor.map F f) :
    faithful.div F G obj h_obj map h_map ⋙ G = F :=
  sorry

theorem faithful.div_faithful {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] (F : C ⥤ E) [faithful F] (G : D ⥤ E) [faithful G] (obj : C → D)
    (h_obj : ∀ (X : C), functor.obj G (obj X) = functor.obj F X)
    (map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y))
    (h_map : ∀ {X Y : C} {f : X ⟶ Y}, functor.map G (map f) == functor.map F f) :
    faithful (faithful.div F G obj h_obj map h_map) :=
  eq.faithful_of_comp
    (faithful.div_comp F G (fun (X : C) => obj X) h_obj (fun (X Y : C) (f : X ⟶ Y) => map f) h_map)

protected instance full.comp {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] (F : C ⥤ D) (G : D ⥤ E) [full F] [full G] : full (F ⋙ G) :=
  full.mk
    fun (_x _x_1 : C) (f : functor.obj (F ⋙ G) _x ⟶ functor.obj (F ⋙ G) _x_1) =>
      functor.preimage F (functor.preimage G f)

/--
Given a natural isomorphism between `F ⋙ H` and `G ⋙ H` for a fully faithful functor `H`, we
can 'cancel' it to give a natural iso between `F` and `G`.
-/
def fully_faithful_cancel_right {C : Type u₁} [category C] {D : Type u₂} [category D] {E : Type u₃}
    [category E] {F : C ⥤ D} {G : C ⥤ D} (H : D ⥤ E) [full H] [faithful H]
    (comp_iso : F ⋙ H ≅ G ⋙ H) : F ≅ G :=
  nat_iso.of_components (fun (X : C) => preimage_iso (iso.app comp_iso X)) sorry

@[simp] theorem fully_faithful_cancel_right_hom_app {C : Type u₁} [category C] {D : Type u₂}
    [category D] {E : Type u₃} [category E] {F : C ⥤ D} {G : C ⥤ D} {H : D ⥤ E} [full H]
    [faithful H] (comp_iso : F ⋙ H ≅ G ⋙ H) (X : C) :
    nat_trans.app (iso.hom (fully_faithful_cancel_right H comp_iso)) X =
        functor.preimage H (nat_trans.app (iso.hom comp_iso) X) :=
  rfl

@[simp] theorem fully_faithful_cancel_right_inv_app {C : Type u₁} [category C] {D : Type u₂}
    [category D] {E : Type u₃} [category E] {F : C ⥤ D} {G : C ⥤ D} {H : D ⥤ E} [full H]
    [faithful H] (comp_iso : F ⋙ H ≅ G ⋙ H) (X : C) :
    nat_trans.app (iso.inv (fully_faithful_cancel_right H comp_iso)) X =
        functor.preimage H (nat_trans.app (iso.inv comp_iso) X) :=
  rfl

end Mathlib


text:
/-
Implemetation of:

Wim Veldman and Marc Bezem, Ramsey's Theorem and the Pigeon Hole
Principle in intuitionistic mathematics, Journal of the London
Mathematical Society (2), Vol. 47, April 1993, pp. 193-211.

Adapted from https://github.com/coq-contribs/ramsey/blob/master/Ramsey.v
-/

namespace constructive.pigeon

def increasing (f : ℕ → ℕ) :=
  ∀ x y : ℕ, x < y → f x < f y

def full (A : ℕ → Prop) (Y : (ℕ → ℕ) → ℕ) :=
∀ f : ℕ → ℕ, increasing f → A (f (Y f))

def almost_full (A : ℕ → Prop) := ∃ Y : (ℕ → ℕ) → ℕ, full A Y

lemma compose_increasing (f g : ℕ → ℕ) :
  increasing f → increasing g → increasing (λ x, f (g x)) :=
    λ (hf : increasing f) (hg : increasing g) (x y : ℕ) (h : x < y),
      hf (g x) (g y) (hg x y h)

lemma increasing_by_step (f : ℕ → ℕ) : (∀ n : ℕ, f n < f (n+1)) → increasing f :=
λ (hf : ∀ n : ℕ, f n < f (n+1)) (x y : ℕ),
  nat.rec_on y
    (λ (contr : x < 0), absurd contr (nat.not_succ_le_zero x))
    (λ (z : ℕ) (ih : x < z → f x < f z) (h : x < nat.succ z),
      or.cases_on (nat.eq_or_lt_of_le (nat.le_of_lt_succ h))
        (λ hxz : x = z, hxz ▸ (hf x))
        (λ (hxz : x < z), nat.lt_trans (ih hxz) (hf z)))

def enumerate (Y : (ℕ → ℕ) → ℕ) : ℕ → ℕ
  | 0 := Y (id)
  | (n+1) := Y (λ m, m + (enumerate n) + 1) + (enumerate n) + 1

lemma  increasing_enumerate (Y : (ℕ → ℕ) → ℕ) : increasing (enumerate Y) :=
λ x : ℕ,
increasing_by_step (λ (x : ℕ), enumerate Y x)
 (λ (n : ℕ),
   nat.le_add_left
     ((enumerate Y n)+1)
     (Y (λ (m : ℕ), m + enumerate Y (nat.add n 0) + 1))) x

variables A B : ℕ → Prop
variables YA YB : (ℕ → ℕ)  → ℕ

def FYA (x n : ℕ) := n + nat.succ (enumerate YA x)

lemma increasing_FYA : ∀ x : ℕ, increasing (FYA YA x) :=
λ (x : ℕ) (y z : ℕ) (h : y < z),
  nat.add_lt_add_right h (nat.succ (enumerate YA x))

lemma enumerate_YA : full A YA → ∀ x : ℕ, A (enumerate YA x) :=
λ (fYA : full A YA) (x : ℕ),
  nat.cases_on x
    (fYA id (λ (x y : ℕ) (h : x < y), h))
    (λ (x : ℕ), fYA (FYA YA x) (increasing_FYA YA x))

lemma YB_enumerate_YA : full B YB -> B (enumerate YA (YB (enumerate YA))) :=
λ YBfull : full B YB,
  YBfull (enumerate YA) (increasing_enumerate YA)

lemma pre_pidgeon : full A YA → full B YB →
  A (enumerate YA (YB (enumerate YA))) ∧ B (enumerate YA (YB (enumerate YA))) :=
λ (YAfull : full A YA) (YBfull : full B YB),
  ⟨enumerate_YA A YA YAfull (YB (enumerate YA)), YB_enumerate_YA B YA YB YBfull⟩

def inter (A B : ℕ -> Prop) (n : ℕ) := A n ∧ B n
infix `∩` := inter

def restrict (Y : (ℕ → ℕ) → ℕ) (f : ℕ → ℕ) := λ g : ℕ → ℕ, Y (f ∘ g)

def combine (YA YB : (ℕ → ℕ) -> ℕ) (f : ℕ → ℕ) :=
  enumerate (restrict YA f) ((restrict YB f) (enumerate (restrict YA f)))
infix `⊙` : 50 := combine

theorem constr_pidgeon_with_wits (A B : nat -> Prop)
  (YA YB : (nat -> nat) -> nat) :
    full A YA → full B YB → full (A ∩ B) (YA ⊙ YB) :=
λ (YAfull : full A YA) (YBfull : full B YB),
    λ (f : ℕ → ℕ) (incrf : increasing f),
       pre_pidgeon (A ∘ f) (B ∘ f) (restrict YA f) (restrict YB f)
         (λ (g : ℕ → ℕ) (incrg : increasing g),
           YAfull (f ∘ g) (compose_increasing f g incrf incrg))
         (λ (g : ℕ → ℕ) (incrg : increasing g),
           YBfull (f ∘ g) (compose_increasing f g incrf incrg))

theorem constr_pigeon (A B : nat -> Prop) :
  almost_full A → almost_full B → almost_full (A ∩ B) :=
λ (afA : almost_full A) (afB : almost_full B),
  exists.elim afA
    (λ (YA : (ℕ → ℕ) → ℕ) (hYA : full A YA),
       exists.elim afB
         (λ (YB : (ℕ → ℕ) → ℕ) (hYB : full B YB),
              (exists.intro
                (YA⊙YB) (constr_pidgeon_with_wits A B YA YB hYA hYB))))

end constructive.pigeon

author: JaredCorduan

repo: ramsey

save_path: github-repos/lean/JaredCorduan-ramsey


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

import tactic.norm_num
import algebra.ring.pi

/-!
# Tests for `norm_num` extensions
-/

constant real : Type
notation `ℝ` := real
@[instance] constant real.linear_ordered_ring : linear_ordered_field ℝ

constant complex : Type
notation `ℂ` := complex
@[instance] constant complex.field : field ℂ
@[instance] constant complex.char_zero : char_zero ℂ

example : 374 + (32 - (2 * 8123) : ℤ) - 61 * 50 = 86 + 32 * 32 - 4 * 5000
      ∧ 43 ≤ 74 + (33 : ℤ) := by norm_num

example : ¬ (7-2)/(2*3) ≥ (1:ℝ) + 2/(3^2) := by norm_num
example : (6:real) + 9 = 15 := by norm_num
example : (2:real)/4 + 4 = 3*3/2 := by norm_num
example : (((3:real)/4)-12)<6 := by norm_num
example : (5:real) ≠ 8 := by norm_num
example : (10:real) > 7 := by norm_num
example : (2:real) * 2 + 3 = 7 := by norm_num
example : (6:real) < 10 := by norm_num
example : (7:real)/2 > 3 := by norm_num
example : (4:real)⁻¹ < 1 := by norm_num
example : ((1:real) / 2)⁻¹ = 2 := by norm_num
example : 2 ^ 17 - 1 = 131071 :=
by {norm_num, tactic.try_for 200 (tactic.result >>= tactic.type_check)}
example : (3 : real) ^ (-2 : ℤ) = 1/9 := by norm_num
example : (3 : real) ^ (-2 : ℤ) = 1/9 := by norm_num1
example : (-3 : real) ^ (0 : ℤ) = 1 := by norm_num
example : (-3 : real) ^ (-1 : ℤ) = -1/3 := by norm_num
example : (-3 : real) ^ (2 : ℤ) = 9 := by norm_num

example : (1:complex) ≠ 2 := by norm_num
example : (1:complex) / 3 ≠ 2 / 7 := by norm_num

example : (1:real) ≠ 2 := by norm_num
example {α} [semiring α] [char_zero α] : (1:α) ≠ 2 := by norm_num
example {α} [ring α] [char_zero α] : (-1:α) ≠ 2 := by norm_num
example {α} [division_ring α] [char_zero α] : (-1:α) ≠ 2 := by norm_num
example {α} [division_ring α] [char_zero α] : (1:α) / 3 ≠ 2 / 7 := by norm_num
example {α} [division_ring α] [char_zero α] : (1:α) / 3 ≠ 0 := by norm_num

example : (5 / 2:ℕ) = 2 := by norm_num
example : (5 / -2:ℤ) < -1 := by norm_num
example : (0 + 1) / 2 < 0 + 1 := by norm_num
example : nat.succ (nat.succ (2 ^ 3)) = 10 := by norm_num
example : 10 = (-1 : ℤ) % 11 := by norm_num
example : (12321 - 2 : ℤ) = 12319 := by norm_num
example : (63:ℚ) ≥ 5 := by norm_num

example : nat.zero.succ.succ.succ.succ.succ.succ % 4 = 2 := by norm_num1

example (x : ℤ) (h : 1000 + 2000 < x) : 100 * 30 < x :=
by norm_num at *; try_for 100 {exact h}

example : (1103 : ℤ) ≤ (2102 : ℤ) := by norm_num
example : (110474 : ℤ) ≤ (210485 : ℤ) := by norm_num
example : (11047462383473829263 : ℤ) ≤ (21048574677772382462 : ℤ) := by norm_num
example : (210485742382937847263 : ℤ) ≤ (1104857462382937847262 : ℤ) := by norm_num
example : (210485987642382937847263 : ℕ) ≤ (11048512347462382937847262 : ℕ) := by norm_num
example : (210485987642382937847263 : ℚ) ≤ (11048512347462382937847262 : ℚ) := by norm_num
example : (2 * 12868 + 25705) * 11621 ^ 2 ≤ 23235 ^ 2 * 12868 := by norm_num

example (x : ℕ) : ℕ := begin
  let n : ℕ, {apply_normed (2^32 - 71)},
  exact n
end

example (a : ℚ) (h : 3⁻¹ * a = a) : true :=
begin
  norm_num at h,
  guard_hyp h : 1 / 3 * a = a,
  trivial
end

example (h : (5 : ℤ) ∣ 2) : false := by norm_num at h
example (h : false) : false := by norm_num at h
example : true := by norm_num
example : true ∧ true := by { split, norm_num, norm_num }

example : 10 + 2 = 1 + 11 := by norm_num

example : 10 - 1 = 9 := by norm_num
example : 12 - 5 = 3 + 4 := by norm_num
example : 5 - 20 = 0 := by norm_num
example : 0 - 2 = 0 := by norm_num
example : 4 - (5 - 10) = 2 + (3 - 1) := by norm_num
example : 0 - 0 = 0 := by norm_num
example : 100 - 100 = 0 := by norm_num
example : 5 * (2 - 3) = 0 := by norm_num
example : 10 - 5 * 5 + (7 - 3) * 6 = 27 - 3 := by norm_num

def foo : ℕ := 1

@[norm_num] meta def eval_foo : expr → tactic (expr × expr)
| `(foo) := pure (`(1:ℕ), `(eq.refl 1))
| _ := tactic.failed

example : foo = 1 := by norm_num

-- ordered field examples

variable {α : Type}
variable [linear_ordered_field α]

example : (-1 :α) * 1 = -1 := by norm_num
example : (-2 :α) * 1 = -2 := by norm_num
example : (-2 :α) * -1 = 2 := by norm_num
example : (-2 :α) * -2 = 4 := by norm_num
example : (1 : α) * 0 = 0 := by norm_num

example : ((1 : α) + 1) * 5 = 6 + 4 := by norm_num

example : (1 : α) = 0 + 1 := by norm_num
example : (1 : α) = 1 + 0 := by norm_num
example : (2 : α) = 1 + 1 := by norm_num
example : (2 : α) = 0 + 2 := by norm_num
example : (3 : α) = 1 + 2 := by norm_num
example : (3 : α) = 2 + 1 := by norm_num
example : (4 : α) = 3 + 1 := by norm_num
example : (4 : α) = 2 + 2 := by norm_num
example : (5 : α) = 4 + 1 := by norm_num
example : (5 : α) = 3 + 2 := by norm_num
example : (5 : α) = 2 + 3 := by norm_num
example : (6 : α) = 0 + 6 := by norm_num
example : (6 : α) = 3 + 3 := by norm_num
example : (6 : α) = 4 + 2 := by norm_num
example : (6 : α) = 5 + 1 := by norm_num
example : (7 : α) = 4 + 3 := by norm_num
example : (7 : α) = 1 + 6 := by norm_num
example : (7 : α) = 6 + 1 := by norm_num
example : 33 = 5 + (28 : α) := by norm_num

example : (12 : α) = 0 + (2 + 3) + 7 := by norm_num
example : (105 : α) = 70 + (33 + 2) := by norm_num

example : (45000000000 : α) = 23000000000 + 22000000000 := by norm_num

example : (0 : α) - 3 = -3 := by norm_num
example : (0 : α) - 2 = -2 := by norm_num
example : (1 : α) - 3 = -2 := by norm_num
example : (1 : α) - 1 = 0 := by norm_num
example : (0 : α) - 3 = -3 := by norm_num
example : (0 : α) - 3 = -3 := by norm_num

example : (12 : α) - 4 - (5 + -2) = 5 := by norm_num
example : (12 : α) - 4 - (5 + -2) - 20 = -15 := by norm_num

example : (0 : α) * 0 = 0 := by norm_num
example : (0 : α) * 1 = 0 := by norm_num
example : (0 : α) * 2 = 0 := by norm_num
example : (2 : α) * 0 = 0 := by norm_num
example : (1 : α) * 0 = 0 := by norm_num
example : (1 : α) * 1 = 1 := by norm_num
example : (2 : α) * 1 = 2 := by norm_num
example : (1 : α) * 2 = 2 := by norm_num
example : (2 : α) * 2 = 4 := by norm_num
example : (3 : α) * 2 = 6 := by norm_num
example : (2 : α) * 3 = 6 := by norm_num
example : (4 : α) * 1 = 4 := by norm_num
example : (1 : α) * 4 = 4 := by norm_num
example : (3 : α) * 3 = 9 := by norm_num
example : (3 : α) * 4 = 12 := by norm_num
example : (4 : α) * 4 = 16 := by norm_num
example : (11 : α) * 2 = 22 := by norm_num
example : (15 : α) * 6 = 90 := by norm_num
example : (123456 : α) * 123456 = 15241383936 := by norm_num

example : (4 : α) / 2 = 2 := by norm_num
example : (4 : α) / 1 = 4 := by norm_num
example : (4 : α) / 3 = 4 / 3 := by norm_num
example : (50 : α) / 5 = 10 := by norm_num
example : (1056 : α) / 1 = 1056 := by norm_num
example : (6 : α) / 4 = 3/2 := by norm_num
example : (0 : α) / 3 = 0 := by norm_num
example : (3 : α) / 0 = 0 := by norm_num
example : (9 * 9 * 9) * (12 : α) / 27 = 81 * (2 + 2) := by norm_num
example : (-2 : α) * 4 / 3 = -8 / 3 := by norm_num
example : - (-4 / 3) = 1 / (3 / (4 : α)) := by norm_num

-- user command

set_option trace.silence_norm_num_if_true true
#norm_num 1 = 1
example : 1 = 1 := by norm_num
#norm_num 2^4-1 ∣ 2^16-1
example : 2^4-1 ∣ 2^16-1 := by norm_num
#norm_num (3 : real) ^ (-2 : ℤ) = 1/9
example : (3 : real) ^ (-2 : ℤ) = 1/9 := by norm_num

section norm_num_cmd_variable
variables (x y : ℕ)

#norm_num bit0 x < bit0 (y + x) ↔ 0 < y
example : bit0 x < bit0 (y + x) ↔ 0 < y := by norm_num
#norm_num bit0 x < bit0 (y + (2^10%11 - 1) + x) ↔ 0 < y
example : bit0 x < bit0 (y + (2^10%11 - 1) + x) ↔ 0 < y := by norm_num
#norm_num bit0 x < bit0 (y + (2^10%11 - 1) + x) + 3*2-6 ↔ 0 < y
example : bit0 x < bit0 (y + (2^10%11 - 1) + x) + 3*2-6 ↔ 0 < y := by norm_num

end norm_num_cmd_variable

-- auto gen tests
example : ((25 * (1 / 1)) + (30 - 16)) = (39 : α) := by norm_num
example : ((19 * (- 2 - 3)) / 6) = (-95/6 : α) := by norm_num
example : - (3 * 28) = (-84 : α) := by norm_num
example : - - (16 / ((11 / (- - (6 * 19) + 12)) * 21)) = (96/11 : α) := by norm_num
example : (- (- 21 + 24) - - (- - (28 + (- 21 / - (16 / ((1 * 26) * ((0 * - 11) + 13))))) * 21)) =
  (79209/8 : α) := by norm_num
example : (27 * (((16 + - (12 + 4)) + (22 - - 19)) - 23)) = (486 : α) := by norm_num
example : - (13 * (- 30 / ((7 / 24) + - 7))) = (-9360/161 : α) := by norm_num
example : - (0 + 20) = (-20 : α) := by norm_num
example : (- 2 - (27 + (((2 / 14) - (7 + 21)) + (16 - - - 14)))) = (-22/7 : α) := by norm_num
example : (25 + ((8 - 2) + 16)) = (47 : α) := by norm_num
example : (- - 26 / 27) = (26/27 : α) := by norm_num
example : ((((16 * (22 / 14)) - 18) / 11) + 30) = (2360/77 : α) := by norm_num
example : (((- 28 * 28) / (29 - 24)) * 24) = (-18816/5 : α) := by norm_num
example : ((- (18 - ((- - (10 + - 2) - - (23 / 5)) / 5)) - (21 * 22)) -
  (((20 / - ((((19 + 18) + 15) + 3) + - 22)) + 14) / 17)) = (-394571/825 : α) := by norm_num
example : ((3 + 25) - - 4) = (32 : α) := by norm_num
example : ((1 - 0) - 22) = (-21 : α) := by norm_num
example : (((- (8 / 7) / 14) + 20) + 22) = (2054/49 : α) := by norm_num
example : ((21 / 20) - 29) = (-559/20 : α) := by norm_num
example : - - 20 = (20 : α) := by norm_num
example : (24 - (- 9 / 4)) = (105/4 : α) := by norm_num
example : (((7 / ((23 * 19) + (27 * 10))) - ((28 - - 15) * 24)) + (9 / - (10 * - 3))) =
  (-1042007/1010 : α) := by norm_num
example : (26 - (- 29 + (12 / 25))) = (1363/25 : α) := by norm_num
example : ((11 * 27) / (4 - 5)) = (-297 : α) := by norm_num
example : (24 - (9 + 15)) = (0 : α) := by norm_num
example : (- 9 - - 0) = (-9 : α) := by norm_num
example : (- 10 / (30 + 10)) = (-1/4 : α) := by norm_num
example : (22 - (6 * (28 * - 8))) = (1366 : α) := by norm_num
example : ((- - 2 * (9 * - 3)) + (22 / 30)) = (-799/15 : α) := by norm_num
example : - (26 / ((3 + 7) / - (27 * (12 / - 16)))) = (-1053/20 : α) := by norm_num
example : ((- 29 / 1) + 28) = (-1 : α) := by norm_num
example : ((21 * ((10 - (((17 + 28) - - 0) + 20)) + 26)) + ((17 + - 16) * 7)) = (-602 : α) :=
by norm_num
example : (((- 5 - ((24 + - - 8) + 3)) + 20) + - 23) = (-43 : α) := by norm_num
example : ((- ((14 - 15) * (14 + 8)) + ((- (18 - 27) - 0) + 12)) - 11) = (32 : α) := by norm_num
example : (((15 / 17) * (26 / 27)) + 28) = (4414/153 : α) := by norm_num
example : (14 - ((- 16 - 3) * - (20 * 19))) = (-7206 : α) := by norm_num
example : (21 - - - (28 - (12 * 11))) = (125 : α) := by norm_num
example : ((0 + (7 + (25 + 8))) * - (11 * 27)) = (-11880 : α) := by norm_num
example : (19 * - 5) = (-95 : α) := by norm_num
example : (29 * - 8) = (-232 : α) := by norm_num
example : ((22 / 9) - 29) = (-239/9 : α) := by norm_num
example : (3 + (19 / 12)) = (55/12 : α) := by norm_num
example : - (13 + 30) = (-43 : α) := by norm_num
example : - - - (((21 * - - ((- 25 - (- (30 - 5) / (- 5 - 5))) /
  (((6 + ((25 * - 13) + 22)) - 3) / 2))) / (- 3 / 10)) * (- 8 - 0)) = (-308/3 : α) := by norm_num
example : - (2 * - (- 24 * 22)) = (-1056 : α) := by norm_num
example : - - (((28 / - ((- 13 * - 5) / - (((7 - 30) / 16) + 6))) * 0) - 24) = (-24 : α) :=
by norm_num
example : ((13 + 24) - (27 / (21 * 13))) = (3358/91 : α) := by norm_num
example : ((3 / - 21) * 25) = (-25/7 : α) := by norm_num
example : (17 - (29 - 18)) = (6 : α) := by norm_num
example : ((28 / 20) * 15) = (21 : α) := by norm_num
example : ((((26 * (- (23 - 13) - 3)) / 20) / (14 - (10 + 20))) / ((16 / 6) / (16 * - (3 / 28)))) =
(-1521/2240 : α) := by norm_num

example : (46 / (- ((- 17 * 28) - 77) + 87)) = (23/320 : α) := by norm_num
example : (73 * - (67 - (74 * - - 11))) = (54531 : α) := by norm_num
example : ((8 * (25 / 9)) + 59) = (731/9 : α) := by norm_num
example : - ((59 + 85) * - 70) = (10080 : α) := by norm_num
example : (66 + (70 * 58)) = (4126 : α) := by norm_num
example : (- - 49 * 0) = (0 : α) := by norm_num
example : ((- 78 - 69) * 9) = (-1323 : α) := by norm_num
example : - - (7 - - (50 * 79)) = (3957 : α) := by norm_num
example : - (85 * (((4 * 93) * 19) * - 31)) = (18624180 : α) := by norm_num
example : (21 + (- 5 / ((74 * 85) / 45))) = (26373/1258 : α) := by norm_num
example : (42 - ((27 + 64) + 26)) = (-75 : α) := by norm_num
example : (- ((38 - - 17) + 86) - (74 + 58)) = (-273 : α) := by norm_num
example : ((29 * - (75 + - 68)) + (- 41 / 28)) = (-5725/28 : α) := by norm_num
example : (- - (40 - 11) - (68 * 86)) = (-5819 : α) := by norm_num
example : (6 + ((65 - 14) + - 89)) = (-32 : α) := by norm_num
example : (97 * - (29 * 35)) = (-98455 : α) := by norm_num
example : - (66 / 33) = (-2 : α) := by norm_num
example : - ((94 * 89) + (79 - (23 - (((- 1 / 55) + 95) * (28 - (54 / - - - 22)))))) =
(-1369070/121 : α) := by norm_num
example : (- 23 + 61) = (38 : α) := by norm_num
example : - (93 / 69) = (-31/23 : α) := by norm_num
example : (- - ((68 / (39 + (((45 * - (59 - (37 + 35))) / (53 - 75)) -
 - (100 + - (50 / (- 30 - 59)))))) - (69 - (23 * 30))) / (57 + 17)) = (137496481/16368578 : α) :=
by norm_num
example : (- 19 * - - (75 * - - 41)) = (-58425 : α) := by norm_num
example : ((3 / ((- 28 * 45) * (19 + ((- (- 88 - (- (- 1 + 90) + 8)) + 87) * 48)))) + 1) =
  (1903019/1903020 : α) := by norm_num
example : ((- - (28 + 48) / 75) + ((- 59 - 14) - 0)) = (-5399/75 : α) := by norm_num
example : (- ((- (((66 - 86) - 36) / 94) - 3) / - - (77 / (56 - - - 79))) + 87) =
  (312254/3619 : α) := by norm_num

example : 2 ^ 13 - 1 = int.of_nat 8191 := by norm_num

-- `^` and `•` do not have to match `monoid.has_pow` and `add_monoid.has_smul` syntactically
example {α} [ring α] : (2 ^ 3 : ℕ → α) = 8 := by norm_num
example {α} [ring α] : (2 • 3 : ℕ → α) = 6 := by norm_num

/-! Test the behaviour of removing one `norm_num` extension tactic. -/
section remove_extension

-- turn off the `norm_num` extension which deals with `/`, `%`, `∣`
local attribute [-norm_num] norm_num.eval_nat_int_ext

example : (5 / 2:ℕ) = 2 := by  success_if_fail { solve1 { norm_num } }; refl

example : 10 = (-1 : ℤ) % 11 := by success_if_fail { solve1 { norm_num } }; refl

example (h : (5 : ℤ) ∣ 2) : false :=
begin
  success_if_fail { norm_num at h },
  have : (2:ℤ) ≠ 0 := by norm_num,
  exact this (int.mod_eq_zero_of_dvd h),
end

example : 2^4-1 ∣ 2^16-1 :=
begin
  success_if_fail { solve1 { norm_num } },
  use 4369,
  norm_num,
end

end remove_extension

author: leanprover-community

repo: mathlib


text:
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl

! This file was ported from Lean 3 source module algebra.order.monoid.min_max
! leanprover-community/mathlib commit de87d5053a9fe5cbde723172c0fb7e27e7436473
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathbin.Order.MinMax
import Mathbin.Algebra.Order.Monoid.Lemmas

/-!
# Lemmas about `min` and `max` in an ordered monoid.

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

open Function

variable {α β : Type _}

/-! Some lemmas about types that have an ordering and a binary operation, with no
  rules relating them. -/

/- warning: fn_min_mul_fn_max -> fn_min_mul_fn_max is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} {β : Type.{u2}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : CommSemigroup.{u2} β] (f : α -> β) (n : α) (m : α), Eq.{succ u2} β (HMul.hMul.{u2, u2, u2} β β β (instHMul.{u2} β (Semigroup.toHasMul.{u2} β (CommSemigroup.toSemigroup.{u2} β _inst_2))) (f (LinearOrder.min.{u1} α _inst_1 n m)) (f (LinearOrder.max.{u1} α _inst_1 n m))) (HMul.hMul.{u2, u2, u2} β β β (instHMul.{u2} β (Semigroup.toHasMul.{u2} β (CommSemigroup.toSemigroup.{u2} β _inst_2))) (f n) (f m))
but is expected to have type
  forall {α : Type.{u2}} {β : Type.{u1}} [_inst_1 : LinearOrder.{u2} α] [_inst_2 : CommSemigroup.{u1} β] (f : α -> β) (n : α) (m : α), Eq.{succ u1} β (HMul.hMul.{u1, u1, u1} β β β (instHMul.{u1} β (Semigroup.toMul.{u1} β (CommSemigroup.toSemigroup.{u1} β _inst_2))) (f (Min.min.{u2} α (LinearOrder.toMin.{u2} α _inst_1) n m)) (f (Max.max.{u2} α (LinearOrder.toMax.{u2} α _inst_1) n m))) (HMul.hMul.{u1, u1, u1} β β β (instHMul.{u1} β (Semigroup.toMul.{u1} β (CommSemigroup.toSemigroup.{u1} β _inst_2))) (f n) (f m))
Case conversion may be inaccurate. Consider using '#align fn_min_mul_fn_max fn_min_mul_fn_maxₓ'. -/
@[to_additive]
theorem fn_min_mul_fn_max [LinearOrder α] [CommSemigroup β] (f : α → β) (n m : α) :
    f (min n m) * f (max n m) = f n * f m := by cases' le_total n m with h h <;> simp [h, mul_comm]
#align fn_min_mul_fn_max fn_min_mul_fn_max
#align fn_min_add_fn_max fn_min_add_fn_max

/- warning: min_mul_max -> min_mul_max is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : CommSemigroup.{u1} α] (n : α) (m : α), Eq.{succ u1} α (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (Semigroup.toHasMul.{u1} α (CommSemigroup.toSemigroup.{u1} α _inst_2))) (LinearOrder.min.{u1} α _inst_1 n m) (LinearOrder.max.{u1} α _inst_1 n m)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (Semigroup.toHasMul.{u1} α (CommSemigroup.toSemigroup.{u1} α _inst_2))) n m)
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : CommSemigroup.{u1} α] (n : α) (m : α), Eq.{succ u1} α (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (Semigroup.toMul.{u1} α (CommSemigroup.toSemigroup.{u1} α _inst_2))) (Min.min.{u1} α (LinearOrder.toMin.{u1} α _inst_1) n m) (Max.max.{u1} α (LinearOrder.toMax.{u1} α _inst_1) n m)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (Semigroup.toMul.{u1} α (CommSemigroup.toSemigroup.{u1} α _inst_2))) n m)
Case conversion may be inaccurate. Consider using '#align min_mul_max min_mul_maxₓ'. -/
@[to_additive]
theorem min_mul_max [LinearOrder α] [CommSemigroup α] (n m : α) : min n m * max n m = n * m :=
  fn_min_mul_fn_max id n m
#align min_mul_max min_mul_max
#align min_add_max min_add_max

section CovariantClassMulLe

variable [LinearOrder α]

section Mul

variable [Mul α]

section Left

variable [CovariantClass α α (· * ·) (· ≤ ·)]

/- warning: min_mul_mul_left -> min_mul_mul_left is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : Mul.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2)) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))))] (a : α) (b : α) (c : α), Eq.{succ u1} α (LinearOrder.min.{u1} α _inst_1 (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a c)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a (LinearOrder.min.{u1} α _inst_1 b c))
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : Mul.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.181 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.183 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.181 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.183) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.196 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.198 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.196 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.198)] (a : α) (b : α) (c : α), Eq.{succ u1} α (Min.min.{u1} α (LinearOrder.toMin.{u1} α _inst_1) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a c)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a (Min.min.{u1} α (LinearOrder.toMin.{u1} α _inst_1) b c))
Case conversion may be inaccurate. Consider using '#align min_mul_mul_left min_mul_mul_leftₓ'. -/
@[to_additive]
theorem min_mul_mul_left (a b c : α) : min (a * b) (a * c) = a * min b c :=
  (monotone_id.const_mul' a).map_min.symm
#align min_mul_mul_left min_mul_mul_left
#align min_add_add_left min_add_add_left

/- warning: max_mul_mul_left -> max_mul_mul_left is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : Mul.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2)) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))))] (a : α) (b : α) (c : α), Eq.{succ u1} α (LinearOrder.max.{u1} α _inst_1 (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a c)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a (LinearOrder.max.{u1} α _inst_1 b c))
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : Mul.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.257 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.259 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.257 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.259) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.272 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.274 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.272 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.274)] (a : α) (b : α) (c : α), Eq.{succ u1} α (Max.max.{u1} α (LinearOrder.toMax.{u1} α _inst_1) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a c)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a (Max.max.{u1} α (LinearOrder.toMax.{u1} α _inst_1) b c))
Case conversion may be inaccurate. Consider using '#align max_mul_mul_left max_mul_mul_leftₓ'. -/
@[to_additive]
theorem max_mul_mul_left (a b c : α) : max (a * b) (a * c) = a * max b c :=
  (monotone_id.const_mul' a).map_max.symm
#align max_mul_mul_left max_mul_mul_left
#align max_add_add_left max_add_add_left

end Left

section Right

variable [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)]

/- warning: min_mul_mul_right -> min_mul_mul_right is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : Mul.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (Function.swap.{succ u1, succ u1, succ u1} α α (fun (ᾰ : α) (ᾰ : α) => α) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2))) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))))] (a : α) (b : α) (c : α), Eq.{succ u1} α (LinearOrder.min.{u1} α _inst_1 (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a c) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) b c)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) (LinearOrder.min.{u1} α _inst_1 a b) c)
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : Mul.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (Function.swap.{succ u1, succ u1, succ u1} α α (fun (ᾰ : α) (ᾰ : α) => α) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.385 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.387 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.385 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.387)) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.400 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.402 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.400 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.402)] (a : α) (b : α) (c : α), Eq.{succ u1} α (Min.min.{u1} α (LinearOrder.toMin.{u1} α _inst_1) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a c) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) b c)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) (Min.min.{u1} α (LinearOrder.toMin.{u1} α _inst_1) a b) c)
Case conversion may be inaccurate. Consider using '#align min_mul_mul_right min_mul_mul_rightₓ'. -/
@[to_additive]
theorem min_mul_mul_right (a b c : α) : min (a * c) (b * c) = min a b * c :=
  (monotone_id.mul_const' c).map_min.symm
#align min_mul_mul_right min_mul_mul_right
#align min_add_add_right min_add_add_right

/- warning: max_mul_mul_right -> max_mul_mul_right is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : Mul.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (Function.swap.{succ u1, succ u1, succ u1} α α (fun (ᾰ : α) (ᾰ : α) => α) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2))) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))))] (a : α) (b : α) (c : α), Eq.{succ u1} α (LinearOrder.max.{u1} α _inst_1 (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a c) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) b c)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) (LinearOrder.max.{u1} α _inst_1 a b) c)
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : Mul.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (Function.swap.{succ u1, succ u1, succ u1} α α (fun (ᾰ : α) (ᾰ : α) => α) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.464 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.466 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.464 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.466)) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.479 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.481 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.479 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.481)] (a : α) (b : α) (c : α), Eq.{succ u1} α (Max.max.{u1} α (LinearOrder.toMax.{u1} α _inst_1) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) a c) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) b c)) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α _inst_2) (Max.max.{u1} α (LinearOrder.toMax.{u1} α _inst_1) a b) c)
Case conversion may be inaccurate. Consider using '#align max_mul_mul_right max_mul_mul_rightₓ'. -/
@[to_additive]
theorem max_mul_mul_right (a b c : α) : max (a * c) (b * c) = max a b * c :=
  (monotone_id.mul_const' c).map_max.symm
#align max_mul_mul_right max_mul_mul_right
#align max_add_add_right max_add_add_right

end Right

#print lt_or_lt_of_mul_lt_mul /-
@[to_additive]
theorem lt_or_lt_of_mul_lt_mul [CovariantClass α α (· * ·) (· ≤ ·)]
    [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂ :=
  by
  contrapose!
  exact fun h => mul_le_mul' h.1 h.2
#align lt_or_lt_of_mul_lt_mul lt_or_lt_of_mul_lt_mul
#align lt_or_lt_of_add_lt_add lt_or_lt_of_add_lt_add
-/

#print le_or_lt_of_mul_le_mul /-
@[to_additive]
theorem le_or_lt_of_mul_le_mul [CovariantClass α α (· * ·) (· ≤ ·)]
    [CovariantClass α α (swap (· * ·)) (· < ·)] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ < b₂ :=
  by
  contrapose!
  exact fun h => mul_lt_mul_of_lt_of_le h.1 h.2
#align le_or_lt_of_mul_le_mul le_or_lt_of_mul_le_mul
#align le_or_lt_of_add_le_add le_or_lt_of_add_le_add
-/

#print lt_or_le_of_mul_le_mul /-
@[to_additive]
theorem lt_or_le_of_mul_le_mul [CovariantClass α α (· * ·) (· < ·)]
    [CovariantClass α α (swap (· * ·)) (· ≤ ·)] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ < a₂ ∨ b₁ ≤ b₂ :=
  by
  contrapose!
  exact fun h => mul_lt_mul_of_le_of_lt h.1 h.2
#align lt_or_le_of_mul_le_mul lt_or_le_of_mul_le_mul
#align lt_or_le_of_add_le_add lt_or_le_of_add_le_add
-/

#print le_or_le_of_mul_le_mul /-
@[to_additive]
theorem le_or_le_of_mul_le_mul [CovariantClass α α (· * ·) (· < ·)]
    [CovariantClass α α (swap (· * ·)) (· < ·)] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂ :=
  by
  contrapose!
  exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2
#align le_or_le_of_mul_le_mul le_or_le_of_mul_le_mul
#align le_or_le_of_add_le_add le_or_le_of_add_le_add
-/

#print mul_lt_mul_iff_of_le_of_le /-
@[to_additive]
theorem mul_lt_mul_iff_of_le_of_le [CovariantClass α α (· * ·) (· ≤ ·)]
    [CovariantClass α α (swap (· * ·)) (· ≤ ·)] [CovariantClass α α (· * ·) (· < ·)]
    [CovariantClass α α (swap (· * ·)) (· < ·)] {a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) :
    a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂ :=
  by
  refine' ⟨lt_or_lt_of_mul_lt_mul, _⟩
  rintro (ha | hb)
  · exact mul_lt_mul_of_lt_of_le ha hb
  · exact mul_lt_mul_of_le_of_lt ha hb
#align mul_lt_mul_iff_of_le_of_le mul_lt_mul_iff_of_le_of_le
#align add_lt_add_iff_of_le_of_le add_lt_add_iff_of_le_of_le
-/

end Mul

variable [MulOneClass α]

/- warning: min_le_mul_of_one_le_right -> min_le_mul_of_one_le_right is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : MulOneClass.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toHasMul.{u1} α _inst_2))) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))))] {a : α} {b : α}, (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))) (OfNat.ofNat.{u1} α 1 (OfNat.mk.{u1} α 1 (One.one.{u1} α (MulOneClass.toHasOne.{u1} α _inst_2)))) b) -> (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))) (LinearOrder.min.{u1} α _inst_1 a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toHasMul.{u1} α _inst_2)) a b))
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : MulOneClass.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1296 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1298 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toMul.{u1} α _inst_2)) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1296 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1298) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1311 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1313 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1311 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1313)] {a : α} {b : α}, (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) (OfNat.ofNat.{u1} α 1 (One.toOfNat1.{u1} α (MulOneClass.toOne.{u1} α _inst_2))) b) -> (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) (Min.min.{u1} α (LinearOrder.toMin.{u1} α _inst_1) a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toMul.{u1} α _inst_2)) a b))
Case conversion may be inaccurate. Consider using '#align min_le_mul_of_one_le_right min_le_mul_of_one_le_rightₓ'. -/
@[to_additive]
theorem min_le_mul_of_one_le_right [CovariantClass α α (· * ·) (· ≤ ·)] {a b : α} (hb : 1 ≤ b) :
    min a b ≤ a * b :=
  min_le_iff.2 <| Or.inl <| le_mul_of_one_le_right' hb
#align min_le_mul_of_one_le_right min_le_mul_of_one_le_right
#align min_le_add_of_nonneg_right min_le_add_of_nonneg_right

/- warning: min_le_mul_of_one_le_left -> min_le_mul_of_one_le_left is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : MulOneClass.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (Function.swap.{succ u1, succ u1, succ u1} α α (fun (ᾰ : α) (ᾰ : α) => α) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toHasMul.{u1} α _inst_2)))) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))))] {a : α} {b : α}, (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))) (OfNat.ofNat.{u1} α 1 (OfNat.mk.{u1} α 1 (One.one.{u1} α (MulOneClass.toHasOne.{u1} α _inst_2)))) a) -> (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))) (LinearOrder.min.{u1} α _inst_1 a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toHasMul.{u1} α _inst_2)) a b))
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : MulOneClass.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (Function.swap.{succ u1, succ u1, succ u1} α α (fun (ᾰ : α) (ᾰ : α) => α) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1368 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1370 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toMul.{u1} α _inst_2)) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1368 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1370)) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1383 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1385 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1383 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1385)] {a : α} {b : α}, (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) (OfNat.ofNat.{u1} α 1 (One.toOfNat1.{u1} α (MulOneClass.toOne.{u1} α _inst_2))) a) -> (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) (Min.min.{u1} α (LinearOrder.toMin.{u1} α _inst_1) a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toMul.{u1} α _inst_2)) a b))
Case conversion may be inaccurate. Consider using '#align min_le_mul_of_one_le_left min_le_mul_of_one_le_leftₓ'. -/
@[to_additive]
theorem min_le_mul_of_one_le_left [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a b : α}
    (ha : 1 ≤ a) : min a b ≤ a * b :=
  min_le_iff.2 <| Or.inr <| le_mul_of_one_le_left' ha
#align min_le_mul_of_one_le_left min_le_mul_of_one_le_left
#align min_le_add_of_nonneg_left min_le_add_of_nonneg_left

/- warning: max_le_mul_of_one_le -> max_le_mul_of_one_le is a dubious translation:
lean 3 declaration is
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : MulOneClass.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toHasMul.{u1} α _inst_2))) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))))] [_inst_4 : CovariantClass.{u1, u1} α α (Function.swap.{succ u1, succ u1, succ u1} α α (fun (ᾰ : α) (ᾰ : α) => α) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toHasMul.{u1} α _inst_2)))) (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))))] {a : α} {b : α}, (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))) (OfNat.ofNat.{u1} α 1 (OfNat.mk.{u1} α 1 (One.one.{u1} α (MulOneClass.toHasOne.{u1} α _inst_2)))) a) -> (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))) (OfNat.ofNat.{u1} α 1 (OfNat.mk.{u1} α 1 (One.one.{u1} α (MulOneClass.toHasOne.{u1} α _inst_2)))) b) -> (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (LinearOrder.toLattice.{u1} α _inst_1))))) (LinearOrder.max.{u1} α _inst_1 a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toHasMul.{u1} α _inst_2)) a b))
but is expected to have type
  forall {α : Type.{u1}} [_inst_1 : LinearOrder.{u1} α] [_inst_2 : MulOneClass.{u1} α] [_inst_3 : CovariantClass.{u1, u1} α α (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1437 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1439 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toMul.{u1} α _inst_2)) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1437 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1439) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1452 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1454 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1452 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1454)] [_inst_4 : CovariantClass.{u1, u1} α α (Function.swap.{succ u1, succ u1, succ u1} α α (fun (ᾰ : α) (ᾰ : α) => α) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1474 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1476 : α) => HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toMul.{u1} α _inst_2)) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1474 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1476)) (fun (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1489 : α) (x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1491 : α) => LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1489 x._@.Mathlib.Algebra.Order.Monoid.MinMax._hyg.1491)] {a : α} {b : α}, (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) (OfNat.ofNat.{u1} α 1 (One.toOfNat1.{u1} α (MulOneClass.toOne.{u1} α _inst_2))) a) -> (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) (OfNat.ofNat.{u1} α 1 (One.toOfNat1.{u1} α (MulOneClass.toOne.{u1} α _inst_2))) b) -> (LE.le.{u1} α (Preorder.toLE.{u1} α (PartialOrder.toPreorder.{u1} α (SemilatticeInf.toPartialOrder.{u1} α (Lattice.toSemilatticeInf.{u1} α (DistribLattice.toLattice.{u1} α (instDistribLattice.{u1} α _inst_1)))))) (Max.max.{u1} α (LinearOrder.toMax.{u1} α _inst_1) a b) (HMul.hMul.{u1, u1, u1} α α α (instHMul.{u1} α (MulOneClass.toMul.{u1} α _inst_2)) a b))
Case conversion may be inaccurate. Consider using '#align max_le_mul_of_one_le max_le_mul_of_one_leₓ'. -/
@[to_additive]
theorem max_le_mul_of_one_le [CovariantClass α α (· * ·) (· ≤ ·)]
    [CovariantClass α α (Function.swap (· * ·)) (· ≤ ·)] {a b : α} (ha : 1 ≤ a) (hb : 1 ≤ b) :
    max a b ≤ a * b :=
  max_le_iff.2 ⟨le_mul_of_one_le_right' hb, le_mul_of_one_le_left' ha⟩
#align max_le_mul_of_one_le max_le_mul_of_one_le
#align max_le_add_of_nonneg max_le_add_of_nonneg

end CovariantClassMulLe


text:
import tactic.tidy data.pnat

universes u v w

@[derive decidable_eq]inductive dvector (α : Type u) : ℕ → Type u
| nil {} : dvector 0
| cons : ∀{n} (x : α) (xs : dvector n), dvector (n+1)

@[derive decidable_eq]inductive dfin : ℕ → Type
| fz {n} : dfin (n+1)
| fs {n} : dfin n → dfin (n+1)

namespace dfin
@[simp] def to_nat : ∀ {n}, dfin n → ℕ
| _ fz := 0
| _ (fs n) := n.to_nat + 1

theorem to_nat_lt : ∀ {n} (x : dfin n), x.to_nat < n
| _ fz := nat.succ_pos _
| _ (fs n) := nat.succ_lt_succ (to_nat_lt n)

def to_fin : ∀ {n}, dfin n → fin n
| 0 x := by {cases x}
| (n+1) x := ⟨to_nat x, by apply to_nat_lt⟩

@[extensionality] theorem to_nat_inj {n} {x y : dfin n} (e : x.to_nat = y.to_nat) : x = y :=
by induction x; cases y; injection e with e; [refl, rw x_ih e]

def raise : ∀ {n}, dfin n → dfin (n+1)
| _ fz := fz
| _ (fs n) := fs n.raise

def elim0 {α : Sort*} : dfin 0 → α.

def cast_le : ∀ {m n}, n ≤ m → dfin n → dfin m
| 0 n h x := false.elim (by cases h; cases x)
| (m+1) _ _ fz := fz
| (m+1) _ h (@fs n s) :=
  fs (s.cast_le (nat.le_of_succ_le_succ h))

@[simp] theorem cast_le_to_nat : ∀ {m n}
  (h : n ≤ m) (x : dfin n), (x.cast_le h).to_nat = x.to_nat
| 0 n h x := false.elim (by cases h; cases x)
| (m+1) _ _ fz := rfl
| (m+1) _ h (@fs n s) :=
  congr_arg (+1) (cast_le_to_nat _ _)

theorem cast_le_rfl {n} (x : dfin n) : x.cast_le (le_refl _) = x :=
to_nat_inj (by simp)

def last : ∀ n, dfin (n+1)
| 0 := fz
| (n+1) := fs (last n)

def of_nat : ∀ n, ℕ → option (dfin n)
| 0 m := none
| (n+1) 0 := some fz
| (n+1) (m+1) := fs <$> of_nat n m

def of_nat_lt : ∀ {n} m, m < n → dfin n
| 0 m h := (nat.not_lt_zero _ h).elim
| (n+1) 0 _ := fz
| (n+1) (m+1) h := fs (of_nat_lt m (nat.lt_of_succ_lt_succ h))

@[simp] theorem of_nat_lt_to_nat : ∀ {n m} (h : m < n),
  (of_nat_lt m h).to_nat = m
| 0 m h := (nat.not_lt_zero _ h).elim
| (n+1) 0 _ := rfl
| (n+1) (m+1) h := congr_arg (+1)
  (of_nat_lt_to_nat (nat.lt_of_succ_lt_succ h))

def of_fin : ∀{n}, fin n → dfin n
| n ⟨val, h⟩ := of_nat_lt val h

meta instance reflect : ∀ n, has_reflect (dfin n)
| _ fz := `(fz)
| _ (fs n) := `(fs).subst (reflect _ n)

def fz' : Π{n : ℕ+}, dfin n
| ⟨0,   h⟩ := false.elim (lt_irrefl 0 h)
| ⟨k+1, h⟩ := fz

end dfin

meta def tactic.interactive.to_dfin (m : ℕ) : tactic unit := do
  n ← do {
    `(dfin %%n) ← tactic.target | return (m+1),
    tactic.eval_expr ℕ n },
  m ← dfin.of_nat n m,
  tactic.exact (reflect m)

namespace dfin

instance has_zero_dfin {n} : has_zero $ dfin (n+1) := ⟨fz⟩

instance has_one_dfin : ∀ {n}, has_one (dfin (nat.succ n))
| 0 := ⟨fz⟩
| (n+1) := ⟨fs fz⟩

instance has_zero_dfin_pnat {n : ℕ+} : has_zero (dfin n) := ⟨fz'⟩
instance has_one_dfin_pnat : Π{n : ℕ+}, has_one (dfin n)
| ⟨0, h⟩   := false.elim (lt_irrefl 0 h)
| ⟨1, h⟩   := ⟨fz⟩
| ⟨n+2, h⟩ := ⟨fs fz⟩

instance has_add_dfin {n} : has_add (dfin(n)) :=
  ⟨λ x y, of_fin $ (to_fin x) + (to_fin y)⟩

def max : ∀{n}, dfin n → dfin n → dfin n
  | 0 x y                 := by cases x
  | (n+1) (fz) y          := y
  | (n+1) x (fz)          := x
  | (n+1) (fs k₁) (fs k₂) := fs $ max k₁ k₂

end dfin

local notation h :: t  := dvector.cons h t
local notation `[` l:(foldr `, ` (h t, dvector.cons h t) dvector.nil `]`) := l

namespace dvector
variables {α : Type u} {β : Type v} {γ : Type w} {n : ℕ}

@[simp] protected def zero_eq : ∀(xs : dvector α 0), xs = []
| [] := rfl

@[simp] protected def concat : ∀{n : ℕ} (xs : dvector α n) (x : α), dvector α (n+1)
| _ []      x' := [x']
| _ (x::xs) x' := x::concat xs x'

@[simp] protected def nth : ∀{n : ℕ} (xs : dvector α n) (m : ℕ) (h : m < n), α
| _ []      m     h := by exfalso; exact nat.not_lt_zero m h
| _ (x::xs) 0     h := x
| _ (x::xs) (m+1) h := nth xs m (lt_of_add_lt_add_right h)

@[reducible, simp] protected def last {n : ℕ} (xs : dvector α (n+1)) : α :=
  xs.nth n (by {repeat{constructor}})

protected def nth' {n : ℕ} (xs : dvector α n) (m : fin n) : α :=
xs.nth m.1 m.2

protected def nth'' : ∀ {n : ℕ} (xs : dvector α n) (m : dfin n), α
| _ (x::xs) dfin.fz       := x
| _ (x::xs) (dfin.fs (m)) := nth'' xs m

protected def mem : ∀{n : ℕ} (x : α) (xs : dvector α n), Prop
| _ x []       := false
| _ x (x'::xs) := x = x' ∨ mem x xs
instance {n : ℕ} : has_mem α (dvector α n) := ⟨dvector.mem⟩

protected def to_set : ∀{n : ℕ}, dvector α n → set α :=
λ n xs, λ a, dvector.mem a xs

protected def pmem : ∀{n : ℕ} (x : α) (xs : dvector α n), Type
| _ x []       := empty
| _ x (x'::xs) := psum (x = x') (pmem x xs)

protected def mem_of_pmem : ∀{n : ℕ} {x : α} {xs : dvector α n} (hx : xs.pmem x), x ∈ xs
| _ x []       hx := by cases hx
| _ x (x'::xs) hx := by cases hx;[exact or.inl hx, exact or.inr (mem_of_pmem hx)]

@[simp] protected def map (f : α → β) : ∀{n : ℕ}, dvector α n → dvector β n
| _ []      := []
| _ (x::xs) := f x :: map xs

@[simp] protected lemma map_id : ∀{n : ℕ} (xs : dvector α n), xs.map (λx, x) = xs
| _ []      := rfl
| _ (x::xs) := by dsimp; simp*

@[simp] protected lemma map_congr_pmem {f g : α → β} :
  ∀{n : ℕ} {xs : dvector α n} (h : ∀x, xs.pmem x → f x = g x), xs.map f = xs.map g
| _ []      h := rfl
| _ (x::xs) h :=
  begin
    dsimp, congr' 1, exact h x (psum.inl rfl), apply map_congr_pmem,
    intros x hx, apply h, right, exact hx
  end

@[simp] protected lemma map_congr_mem {f g : α → β} {n : ℕ} {xs : dvector α n}
  (h : ∀x, x ∈ xs → f x = g x) : xs.map f = xs.map g :=
dvector.map_congr_pmem $ λx hx, h x $ dvector.mem_of_pmem hx

@[simp] protected lemma map_congr {f g : α → β} (h : ∀x, f x = g x) :
  ∀{n : ℕ} (xs : dvector α n), xs.map f = xs.map g
| _ []      := rfl
| _ (x::xs) := by dsimp; simp*

@[simp] protected lemma map_map (g : β → γ) (f : α → β): ∀{n : ℕ} (xs : dvector α n),
  (xs.map f).map g = xs.map (λx, g (f x))
  | _ []      := rfl
  | _ (x::xs) := by dsimp; simp*

protected lemma map_inj {f : α → β} (hf : ∀{{x x'}}, f x = f x' → x = x') {n : ℕ}
  {xs xs' : dvector α n} (h : xs.map f = xs'.map f) : xs = xs' :=
begin
  induction xs; cases xs', refl, simp at h, congr;[apply hf, apply xs_ih]; simp [h]
end

@[simp] protected lemma map_concat (f : α → β) : ∀{n : ℕ} (xs : dvector α n) (x : α),
  (xs.concat x).map f = (xs.map f).concat (f x)
| _ []      x' := by refl
| _ (x::xs) x' := by dsimp; congr' 1; exact map_concat xs x'

@[simp] protected lemma map_nth (f : α → β) : ∀{n : ℕ} (xs : dvector α n) (m : ℕ) (h : m < n),
  (xs.map f).nth m h = f (xs.nth m h)
| _ []      m     h := by exfalso; exact nat.not_lt_zero m h
| _ (x::xs) 0     h := by refl
| _ (x::xs) (m+1) h := by exact map_nth xs m _

protected lemma concat_nth : ∀{n : ℕ} (xs : dvector α n) (x : α) (m : ℕ) (h' : m < n+1)
  (h : m < n), (xs.concat x).nth m h' = xs.nth m h
| _ []      x' m     h' h := by exfalso; exact nat.not_lt_zero m h
| _ (x::xs) x' 0     h' h := by refl
| _ (x::xs) x' (m+1) h' h := by dsimp; exact concat_nth xs x' m _ _

@[simp] protected lemma concat_nth_last : ∀{n : ℕ} (xs : dvector α n) (x : α) (h : n < n+1),
  (xs.concat x).nth n h = x
| _ []      x' h := by refl
| _ (x::xs) x' h := by dsimp; exact concat_nth_last xs x' _

@[simp] protected lemma concat_nth_last' : ∀{n : ℕ} (xs : dvector α n) (x : α) (h : n < n+1),
  (xs.concat x).last = x
:= by apply dvector.concat_nth_last

@[simp] protected def append : ∀{n m : ℕ} (xs : dvector α n) (xs' : dvector α m), dvector α (m+n)
| _ _ []       xs := xs
| _ _ (x'::xs) xs' := x'::append xs xs'

@[simp]protected def insert : ∀{n : ℕ} (x : α) (k : ℕ) (xs : dvector α n), dvector α (n+1)
| n x 0 xs := (x::xs)
| 0 x k xs := (x::xs)
| (n+1) x (k+1) (y::ys) := (y::insert x k ys)

@[simp] protected lemma insert_at_zero : ∀{n : ℕ} (x : α) (xs : dvector α n), dvector.insert x 0 xs = (x::xs) := by {intros, induction n; refl} -- why doesn't {intros, refl} work?

@[simp] protected lemma insert_nth : ∀{n : ℕ} (x : α) (k : ℕ) (xs : dvector α n) (h : k < n+1), (dvector.insert x k xs).nth k h = x
| 0 x k xs h := by {cases h, refl, exfalso, apply nat.not_lt_zero, exact h_a}
| n x 0 xs h := by {induction n, refl, simp*}
| (n+1) x (k+1) (y::ys) h := by simp*

protected lemma insert_cons {n k} {x y : α} {v : dvector α n} : (x::(v.insert y k)) = (x::v).insert y (k+1) :=
by {induction v, refl, simp*}

/- Given a proof that n ≤ m, return the nth initial segment of -/
@[simp]protected def trunc : ∀ (n) {m : ℕ} (h : n ≤ m) (xs : dvector α m), dvector α n
| 0 0 _ xs := []
| 0 (m+1) _ xs := []
| (n+1) 0 _ xs := by {exfalso, cases _x}
| (n+1) (m+1) h (x::xs) := (x::@trunc n m (nat.le_of_succ_le_succ h) xs)

@[simp]protected lemma trunc_n_n {n : ℕ} {h : n ≤ n} {v : dvector α n} : dvector.trunc n h v = v :=
  by {induction v, refl, solve_by_elim}

@[simp]protected lemma trunc_0_n {n : ℕ} {h : 0 ≤ n} {v : dvector α n} : dvector.trunc 0 h v = [] :=
  by {induction v, refl, simp}

@[simp]protected lemma trunc_nth {n m l: ℕ} {h : n ≤ m} {h' : l < n} {v : dvector α m} : (v.trunc n h).nth l h' = v.nth l (lt_of_lt_of_le h' h) :=
begin
  induction m generalizing n l, have : n = 0, by cases h; simp, subst this, cases h',
  cases n; cases l, {cases h'}, {cases h'}, {cases v, refl},
  cases v, simp only [m_ih, dvector.nth, dvector.trunc]
end

protected lemma nth_irrel1 : ∀{n k : ℕ} {h : k < n + 1} {h' : k < n + 1 + 1} (v : dvector α (n+1)) (x : α),
  (x :: (v.trunc n (nat.le_succ n))).nth k h = (x::v).nth k h' :=
by {intros, apply @dvector.trunc_nth _ _ _ _ (nat.le_succ _) h (x::v)}

protected def cast {n m} (p : n = m) : dvector α n → dvector α m :=
  by subst p; exact id

@[simp] protected lemma cast_irrel {n m} {p p' : n = m} {v : dvector α n} : v.cast p = v.cast p' := by refl

@[simp] protected lemma cast_rfl {n m} {p : n = m} {q : m = n} {v : dvector α n} : (v.cast p).cast q = v := by {subst p, refl}

protected lemma cast_hrfl {n m} {p : n = m} {v : dvector α n} : v.cast p == v :=
  by subst p; refl

@[simp] protected lemma cast_trans {n m o} {p : n = m} {q : m = o} {v : dvector α n} : (v.cast p).cast q = v.cast (trans p q) := by subst p; subst q; refl

@[simp] protected def remove_mth : ∀ {n : ℕ} (m : ℕ) (xs : dvector α (n+1)) , dvector α (n)
  | 0 _ _  := dvector.nil
  | n 0 (dvector.cons y ys) := ys
  | (n+1) (k+1) (dvector.cons y ys) := dvector.cons y (remove_mth k ys)

end dvector

author: formalabstracts

repo: formalabstracts