Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2021 Damiano Testa. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Damiano Testa

! This file was ported from Lean 3 source module algebra.covariant_and_contravariant
! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Defs
import Mathlib.Order.Basic
import Mathlib.Order.Monotone.Basic

/-!

# Covariants and contravariants

This file contains general lemmas and instances to work with the interactions between a relation and
an action on a Type.

The intended application is the splitting of the ordering from the algebraic assumptions on the
operations in the `Ordered[...]` hierarchy.

The strategy is to introduce two more flexible typeclasses, `CovariantClass` and
`ContravariantClass`:

* `CovariantClass` models the implication `a ≤ b → c * a ≤ c * b` (multiplication is monotone),
* `ContravariantClass` models the implication `a * b < a * c → b < c`.

Since `Co(ntra)variantClass` takes as input the operation (typically `(+)` or `(*)`) and the order
relation (typically `(≤)` or `(<)`), these are the only two typeclasses that I have used.

The general approach is to formulate the lemma that you are interested in and prove it, with the
`Ordered[...]` typeclass of your liking.  After that, you convert the single typeclass,
say `[OrderedCancelMonoid M]`, into three typeclasses, e.g.
`[LeftCancelSemigroup M] [PartialOrder M] [CovariantClass M M (Function.swap (*)) (≤)]`
and have a go at seeing if the proof still works!

Note that it is possible to combine several `Co(ntra)variantClass` assumptions together.
Indeed, the usual ordered typeclasses arise from assuming the pair
`[CovariantClass M M (*) (≤)] [ContravariantClass M M (*) (<)]`
on top of order/algebraic assumptions.

A formal remark is that normally `CovariantClass` uses the `(≤)`-relation, while
`ContravariantClass` uses the `(<)`-relation. This need not be the case in general, but seems to be
the most common usage. In the opposite direction, the implication
```lean
[Semigroup α] [PartialOrder α] [ContravariantClass α α (*) (≤)] => LeftCancelSemigroup α
```
holds -- note the `Co*ntra*` assumption on the `(≤)`-relation.

# Formalization notes

We stick to the convention of using `Function.swap (*)` (or `Function.swap (+)`), for the
typeclass assumptions, since `Function.swap` is slightly better behaved than `flip`.
However, sometimes as a **non-typeclass** assumption, we prefer `flip (*)` (or `flip (+)`),
as it is easier to use.

-/


-- TODO: convert `ExistsMulOfLE`, `ExistsAddOfLE`?
-- TODO: relationship with `Con/AddCon`
-- TODO: include equivalence of `LeftCancelSemigroup` with
-- `Semigroup PartialOrder ContravariantClass α α (*) (≤)`?
-- TODO : use ⇒, as per Eric's suggestion?  See
-- https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/ordered.20stuff/near/236148738
-- for a discussion.
open Function

section Variants

variable {
M: Type ?u.3475
M
N: Type ?u.23
N
:
Type _: Type (?u.3475+1)
Type _
} (
μ: M → N → N
μ
:
M: Type ?u.20
M
→
N: Type ?u.5
N
→
N: Type ?u.8040
N
) (
r: N → N → Prop
r
:
N: Type ?u.23
N
→
N: Type ?u.5
N
→
Prop: Type
Prop
) variable (
M: ?m.38
M
N: ?m.41
N
) /-- `Covariant` is useful to formulate succintly statements about the interactions between an action of a Type on another one and a relation on the acted-upon Type. See the `CovariantClass` doc-string for its meaning. -/ def
Covariant: Prop
Covariant
:
Prop: Type
Prop
:= ∀ (
m: ?m.64
m
) {
n₁: ?m.67
n₁
n₂: ?m.70
n₂
},
r: N → N → Prop
r
n₁: ?m.67
n₁
n₂: ?m.70
n₂
→
r: N → N → Prop
r
(
μ: M → N → N
μ
m: ?m.64
m
n₁: ?m.67
n₁
) (
μ: M → N → N
μ
m: ?m.64
m
n₂: ?m.70
n₂
) #align covariant
Covariant: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
Covariant
/-- `Contravariant` is useful to formulate succintly statements about the interactions between an action of a Type on another one and a relation on the acted-upon Type. See the `ContravariantClass` doc-string for its meaning. -/ def
Contravariant: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
:
Prop: Type
Prop
:= ∀ (
m: ?m.124
m
) {
n₁: ?m.127
n₁
n₂: ?m.130
n₂
},
r: N → N → Prop
r
(
μ: M → N → N
μ
m: ?m.124
m
n₁: ?m.127
n₁
) (
μ: M → N → N
μ
m: ?m.124
m
n₂: ?m.130
n₂
) →
r: N → N → Prop
r
n₁: ?m.127
n₁
n₂: ?m.130
n₂
#align contravariant
Contravariant: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
/-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the `CovariantClass` says that "the action `μ` preserves the relation `r`." More precisely, the `CovariantClass` is a class taking two Types `M N`, together with an "action" `μ : M → N → N` and a relation `r : N → N → Prop`. Its unique field `elim` is the assertion that for all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair `(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)`, obtained from `(n₁, n₂)` by acting upon it by `m`. If `m : M` and `h : r n₁ n₂`, then `CovariantClass.elim m h : r (μ m n₁) (μ m n₂)`. -/ class
CovariantClass: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
:
Prop: Type
Prop
where /-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair `(n₁, n₂)`, then, the relation `r` also holds for the pair `(μ m n₁, μ m n₂)` -/ protected
elim: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
elim
:
Covariant: (M : Type ?u.184) → (N : Type ?u.183) → (M → N → N) → (N → N → Prop) → Prop
Covariant
M: Type ?u.164
M
N: Type ?u.167
N
μ: M → N → N
μ
r: N → N → Prop
r
#align covariant_class
CovariantClass: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
/-- Given an action `μ` of a Type `M` on a Type `N` and a relation `r` on `N`, informally, the `ContravariantClass` says that "if the result of the action `μ` on a pair satisfies the relation `r`, then the initial pair satisfied the relation `r`." More precisely, the `ContravariantClass` is a class taking two Types `M N`, together with an "action" `μ : M → N → N` and a relation `r : N → N → Prop`. Its unique field `elim` is the assertion that for all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation `r` also holds for the pair `(n₁, n₂)`. If `m : M` and `h : r (μ m n₁) (μ m n₂)`, then `ContravariantClass.elim m h : r n₁ n₂`. -/ class
ContravariantClass: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Contravariant M N μ r → ContravariantClass M N μ r
ContravariantClass
:
Prop: Type
Prop
where /-- For all `m ∈ M` and all elements `n₁, n₂ ∈ N`, if the relation `r` holds for the pair `(μ m n₁, μ m n₂)` obtained from `(n₁, n₂)` by acting upon it by `m`, then, the relation `r` also holds for the pair `(n₁, n₂)`. -/ protected
elim: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r], Contravariant M N μ r
elim
:
Contravariant: (M : Type ?u.229) → (N : Type ?u.228) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
M: Type ?u.209
M
N: Type ?u.212
N
μ: M → N → N
μ
r: N → N → Prop
r
#align contravariant_class
ContravariantClass: (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
theorem
rel_iff_cov: ∀ [inst : CovariantClass M N μ r] [inst : ContravariantClass M N μ r] (m : M) {a b : N}, r (μ m a) (μ m b) ↔ r a b
rel_iff_cov
[
CovariantClass: (M : Type ?u.273) → (N : Type ?u.272) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
M: Type ?u.254
M
N: Type ?u.257
N
μ: M → N → N
μ
r: N → N → Prop
r
] [
ContravariantClass: (M : Type ?u.281) → (N : Type ?u.280) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
M: Type ?u.254
M
N: Type ?u.257
N
μ: M → N → N
μ
r: N → N → Prop
r
] (
m: M
m
:
M: Type ?u.254
M
) {
a: N
a
b: N
b
:
N: Type ?u.257
N
} :
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
a: N
a
) (
μ: M → N → N
μ
m: M
m
b: N
b
) ↔
r: N → N → Prop
r
a: N
a
b: N
b
:= ⟨
ContravariantClass.elim: ∀ {M : Type ?u.309} {N : Type ?u.308} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r], Contravariant M N μ r
ContravariantClass.elim
_: ?m.310
_
,
CovariantClass.elim: ∀ {M : Type ?u.346} {N : Type ?u.345} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
CovariantClass.elim
_: ?m.347
_
⟩ #align rel_iff_cov
rel_iff_cov: ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) (r : N → N → Prop) [inst : CovariantClass M N μ r] [inst : ContravariantClass M N μ r] (m : M) {a b : N}, r (μ m a) (μ m b) ↔ r a b
rel_iff_cov
section flip variable {
M: ?m.414
M
N: ?m.417
N
μ: ?m.420
μ
r: ?m.423
r
} theorem
Covariant.flip: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Covariant M N μ r → Covariant M N μ (_root_.flip r)
Covariant.flip
(
h: Covariant M N μ r
h
:
Covariant: (M : Type ?u.445) → (N : Type ?u.444) → (M → N → N) → (N → N → Prop) → Prop
Covariant
M: Type ?u.426
M
N: Type ?u.429
N
μ: M → N → N
μ
r: N → N → Prop
r
) :
Covariant: (M : Type ?u.453) → (N : Type ?u.452) → (M → N → N) → (N → N → Prop) → Prop
Covariant
M: Type ?u.426
M
N: Type ?u.429
N
μ: M → N → N
μ
(
flip: {α : Sort ?u.458} → {β : Sort ?u.457} → {φ : Sort ?u.456} → (α → β → φ) → β → α → φ
flip
r: N → N → Prop
r
) := fun
a: ?m.482
a
_: ?m.485
_
_: ?m.488
_
hbc: ?m.491
hbc
↦
h: Covariant M N μ r
h
a: ?m.482
a
hbc: ?m.491
hbc
#align covariant.flip
Covariant.flip: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Covariant M N μ r → Covariant M N μ (flip r)
Covariant.flip
theorem
Contravariant.flip: Contravariant M N μ r → Contravariant M N μ (_root_.flip r)
Contravariant.flip
(
h: Contravariant M N μ r
h
:
Contravariant: (M : Type ?u.540) → (N : Type ?u.539) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
M: Type ?u.521
M
N: Type ?u.524
N
μ: M → N → N
μ
r: N → N → Prop
r
) :
Contravariant: (M : Type ?u.548) → (N : Type ?u.547) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
M: Type ?u.521
M
N: Type ?u.524
N
μ: M → N → N
μ
(
flip: {α : Sort ?u.553} → {β : Sort ?u.552} → {φ : Sort ?u.551} → (α → β → φ) → β → α → φ
flip
r: N → N → Prop
r
) := fun
a: ?m.577
a
_: ?m.580
_
_: ?m.583
_
hbc: ?m.586
hbc
↦
h: Contravariant M N μ r
h
a: ?m.577
a
hbc: ?m.586
hbc
#align contravariant.flip
Contravariant.flip: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Contravariant M N μ r → Contravariant M N μ (flip r)
Contravariant.flip
end flip section Covariant variable {
M: ?m.632
M
N: ?m.635
N
μ: ?m.638
μ
r: ?m.641
r
} [
CovariantClass: (M : Type ?u.766) → (N : Type ?u.765) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
M: ?m.632
M
N: ?m.635
N
μ: M → N → N
μ
r: N → N → Prop
r
] theorem
act_rel_act_of_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] (m : M) {a b : N}, r a b → r (μ m a) (μ m b)
act_rel_act_of_rel
(
m: M
m
:
M: Type ?u.652
M
) {
a: N
a
b: N
b
:
N: Type ?u.655
N
} (
ab: r a b
ab
:
r: N → N → Prop
r
a: N
a
b: N
b
) :
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
a: N
a
) (
μ: M → N → N
μ
m: M
m
b: N
b
) :=
CovariantClass.elim: ∀ {M : Type ?u.692} {N : Type ?u.691} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
CovariantClass.elim
_: ?m.693
_
ab: r a b
ab
#align act_rel_act_of_rel
act_rel_act_of_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] (m : M) {a b : N}, r a b → r (μ m a) (μ m b)
act_rel_act_of_rel
@[
to_additive: ∀ {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N], Covariant N N (fun x x_1 => x + x_1) r ↔ Contravariant N N (fun x x_1 => x + x_1) r
to_additive
] theorem
Group.covariant_iff_contravariant: ∀ {N : Type u_1} {r : N → N → Prop} [inst : Group N], Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
Group.covariant_iff_contravariant
[
Group: Type ?u.773 → Type ?u.773
Group
N: Type ?u.750
N
] :
Covariant: (M : Type ?u.777) → (N : Type ?u.776) → (M → N → N) → (N → N → Prop) → Prop
Covariant
N: Type ?u.750
N
N: Type ?u.750
N
(· * ·): N → N → N
(· * ·)
r: N → N → Prop
r
↔
Contravariant: (M : Type ?u.870) → (N : Type ?u.869) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
N: Type ?u.750
N
N: Type ?u.750
N
(· * ·): N → N → N
(· * ·)
r: N → N → Prop
r
:=

Goals accomplished! 🐙
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N


Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N


Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r (a⁻¹ * (a * b)) c
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)


refine_1
r b c

Goals accomplished! 🐙
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N


Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r (a⁻¹ * (a * b)) c


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r (a⁻¹ * (a * b)) (a⁻¹ * (a * c))


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)
M: Type ?u.747

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r ((fun x x_1 => x * x_1) a b) ((fun x x_1 => x * x_1) a c)

Goals accomplished! 🐙
#align group.covariant_iff_contravariant
Group.covariant_iff_contravariant: ∀ {N : Type u_1} {r : N → N → Prop} [inst : Group N], Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
Group.covariant_iff_contravariant
#align add_group.covariant_iff_contravariant
AddGroup.covariant_iff_contravariant: ∀ {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N], Covariant N N (fun x x_1 => x + x_1) r ↔ Contravariant N N (fun x x_1 => x + x_1) r
AddGroup.covariant_iff_contravariant
@[
to_additive: ∀ {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N] [inst_1 : CovariantClass N N (fun x x_1 => x + x_1) r], ContravariantClass N N (fun x x_1 => x + x_1) r
to_additive
] instance (priority := 100)
Group.covconv: ∀ [inst : Group N] [inst_1 : CovariantClass N N (fun x x_1 => x * x_1) r], ContravariantClass N N (fun x x_1 => x * x_1) r
Group.covconv
[
Group: Type ?u.1218 → Type ?u.1218
Group
N: Type ?u.1195
N
] [
CovariantClass: (M : Type ?u.1222) → (N : Type ?u.1221) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.1195
N
N: Type ?u.1195
N
(· * ·): N → N → N
(· * ·)
r: N → N → Prop
r
] :
ContravariantClass: (M : Type ?u.1317) → (N : Type ?u.1316) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.1195
N
N: Type ?u.1195
N
(· * ·): N → N → N
(· * ·)
r: N → N → Prop
r
:= ⟨
Group.covariant_iff_contravariant: ∀ {N : Type ?u.1422} {r : N → N → Prop} [inst : Group N], Covariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
Group.covariant_iff_contravariant
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
CovariantClass.elim: ∀ {M : Type ?u.1466} {N : Type ?u.1465} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
CovariantClass.elim
⟩ @[
to_additive: ∀ {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N], Covariant N N (swap fun x x_1 => x + x_1) r ↔ Contravariant N N (swap fun x x_1 => x + x_1) r
to_additive
] theorem
Group.covariant_swap_iff_contravariant_swap: ∀ {N : Type u_1} {r : N → N → Prop} [inst : Group N], Covariant N N (swap fun x x_1 => x * x_1) r ↔ Contravariant N N (swap fun x x_1 => x * x_1) r
Group.covariant_swap_iff_contravariant_swap
[
Group: Type ?u.1671 → Type ?u.1671
Group
N: Type ?u.1648
N
] :
Covariant: (M : Type ?u.1675) → (N : Type ?u.1674) → (M → N → N) → (N → N → Prop) → Prop
Covariant
N: Type ?u.1648
N
N: Type ?u.1648
N
(
swap: {α : Sort ?u.1678} → {β : Sort ?u.1677} → {φ : α → β → Sort ?u.1676} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
r: N → N → Prop
r
↔
Contravariant: (M : Type ?u.1790) → (N : Type ?u.1789) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
N: Type ?u.1648
N
N: Type ?u.1648
N
(
swap: {α : Sort ?u.1793} → {β : Sort ?u.1792} → {φ : α → β → Sort ?u.1791} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
r: N → N → Prop
r
:=

Goals accomplished! 🐙
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N


Covariant N N (swap fun x x_1 => x * x_1) r ↔ Contravariant N N (swap fun x x_1 => x * x_1) r
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N


Covariant N N (swap fun x x_1 => x * x_1) r ↔ Contravariant N N (swap fun x x_1 => x * x_1) r
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r (b * a * a⁻¹) c
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r b c
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r (b * a * a⁻¹) (c * a * a⁻¹)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r (b * a * a⁻¹) (c * a * a⁻¹)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Covariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)


refine_1
r b c

Goals accomplished! 🐙
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N


Covariant N N (swap fun x x_1 => x * x_1) r ↔ Contravariant N N (swap fun x x_1 => x * x_1) r
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (b * a * a⁻¹) c


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (b * a * a⁻¹) (c * a * a⁻¹)


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (b * a * a⁻¹) (c * a * a⁻¹)


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r (b * a * a⁻¹) (c * a * a⁻¹)


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)
M: Type ?u.1645

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝¹: CovariantClass M N μ r

inst✝: Group N

h: Contravariant N N (swap fun x x_1 => x * x_1) r

a, b, c: N

bc: r b c


refine_2
r (swap (fun x x_1 => x * x_1) a b) (swap (fun x x_1 => x * x_1) a c)

Goals accomplished! 🐙
#align group.covariant_swap_iff_contravariant_swap
Group.covariant_swap_iff_contravariant_swap: ∀ {N : Type u_1} {r : N → N → Prop} [inst : Group N], Covariant N N (swap fun x x_1 => x * x_1) r ↔ Contravariant N N (swap fun x x_1 => x * x_1) r
Group.covariant_swap_iff_contravariant_swap
#align add_group.covariant_swap_iff_contravariant_swap
AddGroup.covariant_swap_iff_contravariant_swap: ∀ {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N], Covariant N N (swap fun x x_1 => x + x_1) r ↔ Contravariant N N (swap fun x x_1 => x + x_1) r
AddGroup.covariant_swap_iff_contravariant_swap
@[
to_additive: ∀ {N : Type u_1} {r : N → N → Prop} [inst : AddGroup N] [inst_1 : CovariantClass N N (swap fun x x_1 => x + x_1) r], ContravariantClass N N (swap fun x x_1 => x + x_1) r
to_additive
] instance (priority := 100)
Group.covconv_swap: ∀ {N : Type u_1} {r : N → N → Prop} [inst : Group N] [inst_1 : CovariantClass N N (swap fun x x_1 => x * x_1) r], ContravariantClass N N (swap fun x x_1 => x * x_1) r
Group.covconv_swap
[
Group: Type ?u.2172 → Type ?u.2172
Group
N: Type ?u.2149
N
] [
CovariantClass: (M : Type ?u.2176) → (N : Type ?u.2175) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.2149
N
N: Type ?u.2149
N
(
swap: {α : Sort ?u.2179} → {β : Sort ?u.2178} → {φ : α → β → Sort ?u.2177} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
r: N → N → Prop
r
] :
ContravariantClass: (M : Type ?u.2293) → (N : Type ?u.2292) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.2149
N
N: Type ?u.2149
N
(
swap: {α : Sort ?u.2296} → {β : Sort ?u.2295} → {φ : α → β → Sort ?u.2294} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
r: N → N → Prop
r
:= ⟨
Group.covariant_swap_iff_contravariant_swap: ∀ {N : Type ?u.2418} {r : N → N → Prop} [inst : Group N], Covariant N N (swap fun x x_1 => x * x_1) r ↔ Contravariant N N (swap fun x x_1 => x * x_1) r
Group.covariant_swap_iff_contravariant_swap
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
CovariantClass.elim: ∀ {M : Type ?u.2470} {N : Type ?u.2469} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
CovariantClass.elim
⟩ section Trans variable [
IsTrans: (α : Type ?u.2685) → (α → α → Prop) → Prop
IsTrans
N: Type ?u.2662
N
r: N → N → Prop
r
] (
m: M
m
n: M
n
:
M: Type ?u.2659
M
) {
a: N
a
b: N
b
c: N
c
d: N
d
:
N: Type ?u.2662
N
} -- Lemmas with 3 elements. theorem
act_rel_of_rel_of_act_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] [inst : IsTrans N r] (m : M) {a b c : N}, r a b → r (μ m b) c → r (μ m a) c
act_rel_of_rel_of_act_rel
(
ab: r a b
ab
:
r: N → N → Prop
r
a: N
a
b: N
b
) (
rl: r (μ m b) c
rl
:
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
b: N
b
)
c: N
c
) :
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
a: N
a
)
c: N
c
:=
_root_.trans: ∀ {α : Type ?u.2752} {r : α → α → Prop} [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
_root_.trans
(
act_rel_act_of_rel: ∀ {M : Type ?u.2783} {N : Type ?u.2782} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] (m : M) {a b : N}, r a b → r (μ m a) (μ m b)
act_rel_act_of_rel
m: M
m
ab: r a b
ab
)
rl: r (μ m b) c
rl
#align act_rel_of_rel_of_act_rel
act_rel_of_rel_of_act_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] [inst : IsTrans N r] (m : M) {a b c : N}, r a b → r (μ m b) c → r (μ m a) c
act_rel_of_rel_of_act_rel
theorem
rel_act_of_rel_of_rel_act: r a b → r c (μ m a) → r c (μ m b)
rel_act_of_rel_of_rel_act
(
ab: r a b
ab
:
r: N → N → Prop
r
a: N
a
b: N
b
) (
rr: r c (μ m a)
rr
:
r: N → N → Prop
r
c: N
c
(
μ: M → N → N
μ
m: M
m
a: N
a
)) :
r: N → N → Prop
r
c: N
c
(
μ: M → N → N
μ
m: M
m
b: N
b
) :=
_root_.trans: ∀ {α : Type ?u.2905} {r : α → α → Prop} [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
_root_.trans
rr: r c (μ m a)
rr
(
act_rel_act_of_rel: ∀ {M : Type ?u.2938} {N : Type ?u.2937} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] (m : M) {a b : N}, r a b → r (μ m a) (μ m b)
act_rel_act_of_rel
_: ?m.2939
_
ab: r a b
ab
) #align rel_act_of_rel_of_rel_act
rel_act_of_rel_of_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] [inst : IsTrans N r] (m : M) {a b c : N}, r a b → r c (μ m a) → r c (μ m b)
rel_act_of_rel_of_rel_act
end Trans end Covariant -- Lemma with 4 elements. section MEqN variable {
M: ?m.3029
M
N: ?m.3032
N
μ: ?m.3035
μ
r: ?m.3038
r
} {
mu: N → N → N
mu
:
N: ?m.3032
N
→
N: Type ?u.3103
N
→
N: Type ?u.3103
N
} [
IsTrans: (α : Type ?u.3124) → (α → α → Prop) → Prop
IsTrans
N: ?m.3032
N
r: ?m.3038
r
] [
i: CovariantClass N N mu r
i
:
CovariantClass: (M : Type ?u.3130) → (N : Type ?u.3129) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.3103
N
N: ?m.3032
N
mu: N → N → N
mu
r: ?m.3038
r
] [
i': CovariantClass N N (swap mu) r
i'
:
CovariantClass: (M : Type ?u.3061) → (N : Type ?u.3060) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.3103
N
N: ?m.3032
N
(
swap: {α : Sort ?u.3141} → {β : Sort ?u.3140} → {φ : α → β → Sort ?u.3139} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
mu: N → N → N
mu
)
r: N → N → Prop
r
] {
a: N
a
b: N
b
c: N
c
d: N
d
:
N: ?m.3032
N
} theorem
act_rel_act_of_rel_of_rel: r a b → r c d → r (mu a c) (mu b d)
act_rel_act_of_rel_of_rel
(
ab: r a b
ab
:
r: N → N → Prop
r
a: N
a
b: N
b
) (
cd: r c d
cd
:
r: N → N → Prop
r
c: N
c
d: N
d
) :
r: N → N → Prop
r
(
mu: N → N → N
mu
a: N
a
c: N
c
) (
mu: N → N → N
mu
b: N
b
d: N
d
) :=
_root_.trans: ∀ {α : Type ?u.3184} {r : α → α → Prop} [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
_root_.trans
(@
act_rel_act_of_rel: ∀ {M : Type ?u.3215} {N : Type ?u.3214} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] (m : M) {a b : N}, r a b → r (μ m a) (μ m b)
act_rel_act_of_rel
_: Type ?u.3215
_
_: Type ?u.3214
_
(
swap: {α : Sort ?u.3220} → {β : Sort ?u.3219} → {φ : α → β → Sort ?u.3218} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
mu: N → N → N
mu
)
r: N → N → Prop
r
_
c: N
c
_: ?m.3217
_
_: ?m.3217
_
ab: r a b
ab
) (
act_rel_act_of_rel: ∀ {M : Type ?u.3276} {N : Type ?u.3275} {μ : M → N → N} {r : N → N → Prop} [inst : CovariantClass M N μ r] (m : M) {a b : N}, r a b → r (μ m a) (μ m b)
act_rel_act_of_rel
b: N
b
cd: r c d
cd
) #align act_rel_act_of_rel_of_rel
act_rel_act_of_rel_of_rel: ∀ {N : Type u_1} {r : N → N → Prop} {mu : N → N → N} [inst : IsTrans N r] [i : CovariantClass N N mu r] [i' : CovariantClass N N (swap mu) r] {a b c d : N}, r a b → r c d → r (mu a c) (mu b d)
act_rel_act_of_rel_of_rel
end MEqN section Contravariant variable {
M: ?m.3356
M
N: ?m.3359
N
μ: ?m.3362
μ
r: ?m.3365
r
} [
ContravariantClass: (M : Type ?u.3369) → (N : Type ?u.3368) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
M: Type ?u.3376
M
N: Type ?u.3379
N
μ: M → N → N
μ
r: ?m.3365
r
] theorem
rel_of_act_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClass M N μ r] (m : M) {a b : N}, r (μ m a) (μ m b) → r a b
rel_of_act_rel_act
(
m: M
m
:
M: Type ?u.3376
M
) {
a: N
a
b: N
b
:
N: Type ?u.3379
N
} (
ab: r (μ m a) (μ m b)
ab
:
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
a: N
a
) (
μ: M → N → N
μ
m: M
m
b: N
b
)) :
r: N → N → Prop
r
a: N
a
b: N
b
:=
ContravariantClass.elim: ∀ {M : Type ?u.3416} {N : Type ?u.3415} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r], Contravariant M N μ r
ContravariantClass.elim
_: ?m.3417
_
ab: r (μ m a) (μ m b)
ab
#align rel_of_act_rel_act
rel_of_act_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClass M N μ r] (m : M) {a b : N}, r (μ m a) (μ m b) → r a b
rel_of_act_rel_act
section Trans variable [
IsTrans: (α : Type ?u.3701) → (α → α → Prop) → Prop
IsTrans
N: Type ?u.3521
N
r: N → N → Prop
r
] (
m: M
m
n: M
n
:
M: Type ?u.3475
M
) {
a: N
a
b: N
b
c: N
c
d: N
d
:
N: Type ?u.3478
N
} -- Lemmas with 3 elements. theorem
act_rel_of_act_rel_of_rel_act_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClass M N μ r] [inst : IsTrans N r] (m : M) {a b c : N}, r (μ m a) b → r (μ m b) (μ m c) → r (μ m a) c
act_rel_of_act_rel_of_rel_act_rel
(
ab: r (μ m a) b
ab
:
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
a: N
a
)
b: N
b
) (
rl: r (μ m b) (μ m c)
rl
:
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
b: N
b
) (
μ: M → N → N
μ
m: M
m
c: N
c
)) :
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
a: N
a
)
c: N
c
:=
_root_.trans: ∀ {α : Type ?u.3568} {r : α → α → Prop} [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
_root_.trans
ab: r (μ m a) b
ab
(
rel_of_act_rel_act: ∀ {M : Type ?u.3601} {N : Type ?u.3600} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClass M N μ r] (m : M) {a b : N}, r (μ m a) (μ m b) → r a b
rel_of_act_rel_act
m: M
m
rl: r (μ m b) (μ m c)
rl
) #align act_rel_of_act_rel_of_rel_act_rel
act_rel_of_act_rel_of_rel_act_rel: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClass M N μ r] [inst : IsTrans N r] (m : M) {a b c : N}, r (μ m a) b → r (μ m b) (μ m c) → r (μ m a) c
act_rel_of_act_rel_of_rel_act_rel
theorem
rel_act_of_act_rel_act_of_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClass M N μ r] [inst : IsTrans N r] (m : M) {a b c : N}, r (μ m a) (μ m b) → r b (μ m c) → r a (μ m c)
rel_act_of_act_rel_act_of_rel_act
(
ab: r (μ m a) (μ m b)
ab
:
r: N → N → Prop
r
(
μ: M → N → N
μ
m: M
m
a: N
a
) (
μ: M → N → N
μ
m: M
m
b: N
b
)) (
rr: r b (μ m c)
rr
:
r: N → N → Prop
r
b: N
b
(
μ: M → N → N
μ
m: M
m
c: N
c
)) :
r: N → N → Prop
r
a: N
a
(
μ: M → N → N
μ
m: M
m
c: N
c
) :=
_root_.trans: ∀ {α : Type ?u.3725} {r : α → α → Prop} [inst : IsTrans α r] {a b c : α}, r a b → r b c → r a c
_root_.trans
(
rel_of_act_rel_act: ∀ {M : Type ?u.3756} {N : Type ?u.3755} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClass M N μ r] (m : M) {a b : N}, r (μ m a) (μ m b) → r a b
rel_of_act_rel_act
m: M
m
ab: r (μ m a) (μ m b)
ab
)
rr: r b (μ m c)
rr
#align rel_act_of_act_rel_act_of_rel_act
rel_act_of_act_rel_act_of_rel_act: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop} [inst : ContravariantClass M N μ r] [inst : IsTrans N r] (m : M) {a b c : N}, r (μ m a) (μ m b) → r b (μ m c) → r a (μ m c)
rel_act_of_act_rel_act_of_rel_act
end Trans end Contravariant section Monotone variable {
α: Type ?u.4082
α
:
Type _: Type (?u.3852+1)
Type _
} {
M: ?m.3855
M
N: ?m.3858
N
μ: ?m.3861
μ
} [
Preorder: Type ?u.4307 → Type ?u.4307
Preorder
α: Type ?u.3888
α
] [
Preorder: Type ?u.3867 → Type ?u.3867
Preorder
N: ?m.3858
N
] variable {
f: N → α
f
:
N: Type ?u.3904
N
→
α: Type ?u.4082
α
} /-- The partial application of a constant to a covariant operator is monotone. -/ theorem
Covariant.monotone_of_const: ∀ [inst : CovariantClass M N μ fun x x_1 => x ≤ x_1] (m : M), Monotone (μ m)
Covariant.monotone_of_const
[
CovariantClass: (M : Type ?u.3933) → (N : Type ?u.3932) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
M: Type ?u.3901
M
N: Type ?u.3904
N
μ: M → N → N
μ
(· ≤ ·): N → N → Prop
(· ≤ ·)
] (
m: M
m
:
M: Type ?u.3901
M
) :
Monotone: {α : Type ?u.3962} → {β : Type ?u.3961} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
(
μ: M → N → N
μ
m: M
m
) := fun
_: ?m.3998
_
_: ?m.4001
_
ha: ?m.4004
ha
↦
CovariantClass.elim: ∀ {M : Type ?u.4007} {N : Type ?u.4006} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
CovariantClass.elim
m: M
m
ha: ?m.4004
ha
#align covariant.monotone_of_const
Covariant.monotone_of_const: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} [inst : Preorder N] [inst_1 : CovariantClass M N μ fun x x_1 => x ≤ x_1] (m : M), Monotone (μ m)
Covariant.monotone_of_const
/-- A monotone function remains monotone when composed with the partial application of a covariant operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (λ n, f (m + n))`. -/ theorem
Monotone.covariant_of_const: ∀ [inst : CovariantClass M N μ fun x x_1 => x ≤ x_1], Monotone f → ∀ (m : M), Monotone fun n => f (μ m n)
Monotone.covariant_of_const
[
CovariantClass: (M : Type ?u.4096) → (N : Type ?u.4095) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
M: Type ?u.4064
M
N: Type ?u.4067
N
μ: M → N → N
μ
(· ≤ ·): N → N → Prop
(· ≤ ·)
] (
hf: Monotone f
hf
:
Monotone: {α : Type ?u.4123} → {β : Type ?u.4122} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
f: N → α
f
) (
m: M
m
:
M: Type ?u.4064
M
) :
Monotone: {α : Type ?u.4160} → {β : Type ?u.4159} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
fun
n: ?m.4184
n
↦
f: N → α
f
(
μ: M → N → N
μ
m: M
m
n: ?m.4184
n
) := fun
_: ?m.4196
_
_: ?m.4199
_
x: ?m.4202
x
↦
hf: Monotone f
hf
(
Covariant.monotone_of_const: ∀ {M : Type ?u.4211} {N : Type ?u.4212} {μ : M → N → N} [inst : Preorder N] [inst_1 : CovariantClass M N μ fun x x_1 => x ≤ x_1] (m : M), Monotone (μ m)
Covariant.monotone_of_const
m: M
m
x: ?m.4202
x
) #align monotone.covariant_of_const
Monotone.covariant_of_const: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} [inst_2 : CovariantClass M N μ fun x x_1 => x ≤ x_1], Monotone f → ∀ (m : M), Monotone fun n => f (μ m n)
Monotone.covariant_of_const
/-- Same as `Monotone.covariant_of_const`, but with the constant on the other side of the operator. E.g., `∀ (m : ℕ), Monotone f → Monotone (λ n, f (n + m))`. -/ theorem
Monotone.covariant_of_const': ∀ {N : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} {μ : N → N → N} [inst_2 : CovariantClass N N (swap μ) fun x x_1 => x ≤ x_1], Monotone f → ∀ (m : N), Monotone fun n => f (μ n m)
Monotone.covariant_of_const'
{
μ: N → N → N
μ
:
N: Type ?u.4289
N
→
N: Type ?u.4289
N
→
N: Type ?u.4289
N
} [
CovariantClass: (M : Type ?u.4324) → (N : Type ?u.4323) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.4289
N
N: Type ?u.4289
N
(
swap: {α : Sort ?u.4327} → {β : Sort ?u.4326} → {φ : α → β → Sort ?u.4325} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
μ: N → N → N
μ
)
(· ≤ ·): N → N → Prop
(· ≤ ·)
] (
hf: Monotone f
hf
:
Monotone: {α : Type ?u.4375} → {β : Type ?u.4374} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
f: N → α
f
) (
m: N
m
:
N: Type ?u.4289
N
) :
Monotone: {α : Type ?u.4412} → {β : Type ?u.4411} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Monotone
fun
n: ?m.4436
n
↦
f: N → α
f
(
μ: N → N → N
μ
n: ?m.4436
n
m: N
m
) := fun
_: ?m.4450
_
_: ?m.4453
_
x: ?m.4456
x
↦
hf: Monotone f
hf
(@
Covariant.monotone_of_const: ∀ {M : Type ?u.4465} {N : Type ?u.4466} {μ : M → N → N} [inst : Preorder N] [inst_1 : CovariantClass M N μ fun x x_1 => x ≤ x_1] (m : M), Monotone (μ m)
Covariant.monotone_of_const
_: Type ?u.4465
_
_: Type ?u.4466
_
(
swap: {α : Sort ?u.4471} → {β : Sort ?u.4470} → {φ : α → β → Sort ?u.4469} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
μ: N → N → N
μ
) _ _
m: N
m
_: ?m.4468
_
_: ?m.4468
_
x: ?m.4456
x
) #align monotone.covariant_of_const'
Monotone.covariant_of_const': ∀ {N : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} {μ : N → N → N} [inst_2 : CovariantClass N N (swap μ) fun x x_1 => x ≤ x_1], Monotone f → ∀ (m : N), Monotone fun n => f (μ n m)
Monotone.covariant_of_const'
/-- Dual of `Monotone.covariant_of_const` -/ theorem
Antitone.covariant_of_const: ∀ [inst : CovariantClass M N μ fun x x_1 => x ≤ x_1], Antitone f → ∀ (m : M), Antitone fun n => f (μ m n)
Antitone.covariant_of_const
[
CovariantClass: (M : Type ?u.4583) → (N : Type ?u.4582) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
M: Type ?u.4551
M
N: Type ?u.4554
N
μ: M → N → N
μ
(· ≤ ·): N → N → Prop
(· ≤ ·)
] (
hf: Antitone f
hf
:
Antitone: {α : Type ?u.4610} → {β : Type ?u.4609} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone
f: N → α
f
) (
m: M
m
:
M: Type ?u.4551
M
) :
Antitone: {α : Type ?u.4647} → {β : Type ?u.4646} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone
fun
n: ?m.4671
n
↦
f: N → α
f
(
μ: M → N → N
μ
m: M
m
n: ?m.4671
n
) :=
hf: Antitone f
hf
.
comp_monotone: ∀ {α : Type ?u.4684} {β : Type ?u.4683} {γ : Type ?u.4682} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ} {f : α → β}, Antitone g → Monotone f → Antitone (g ∘ f)
comp_monotone
<|
Covariant.monotone_of_const: ∀ {M : Type ?u.4737} {N : Type ?u.4738} {μ : M → N → N} [inst : Preorder N] [inst_1 : CovariantClass M N μ fun x x_1 => x ≤ x_1] (m : M), Monotone (μ m)
Covariant.monotone_of_const
m: M
m
#align antitone.covariant_of_const
Antitone.covariant_of_const: ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} [inst_2 : CovariantClass M N μ fun x x_1 => x ≤ x_1], Antitone f → ∀ (m : M), Antitone fun n => f (μ m n)
Antitone.covariant_of_const
/-- Dual of `Monotone.covariant_of_const'` -/ theorem
Antitone.covariant_of_const': ∀ {μ : N → N → N} [inst : CovariantClass N N (swap μ) fun x x_1 => x ≤ x_1], Antitone f → ∀ (m : N), Antitone fun n => f (μ n m)
Antitone.covariant_of_const'
{
μ: N → N → N
μ
:
N: Type ?u.4808
N
→
N: Type ?u.4808
N
→
N: Type ?u.4808
N
} [
CovariantClass: (M : Type ?u.4843) → (N : Type ?u.4842) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.4808
N
N: Type ?u.4808
N
(
swap: {α : Sort ?u.4846} → {β : Sort ?u.4845} → {φ : α → β → Sort ?u.4844} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
μ: N → N → N
μ
)
(· ≤ ·): N → N → Prop
(· ≤ ·)
] (
hf: Antitone f
hf
:
Antitone: {α : Type ?u.4894} → {β : Type ?u.4893} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone
f: N → α
f
) (
m: N
m
:
N: Type ?u.4808
N
) :
Antitone: {α : Type ?u.4931} → {β : Type ?u.4930} → [inst : Preorder α] → [inst : Preorder β] → (α → β) → Prop
Antitone
fun
n: ?m.4955
n
↦
f: N → α
f
(
μ: N → N → N
μ
n: ?m.4955
n
m: N
m
) :=
hf: Antitone f
hf
.
comp_monotone: ∀ {α : Type ?u.4970} {β : Type ?u.4969} {γ : Type ?u.4968} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ} {f : α → β}, Antitone g → Monotone f → Antitone (g ∘ f)
comp_monotone
<| @
Covariant.monotone_of_const: ∀ {M : Type ?u.5023} {N : Type ?u.5024} {μ : M → N → N} [inst : Preorder N] [inst_1 : CovariantClass M N μ fun x x_1 => x ≤ x_1] (m : M), Monotone (μ m)
Covariant.monotone_of_const
_: Type ?u.5023
_
_: Type ?u.5024
_
(
swap: {α : Sort ?u.5029} → {β : Sort ?u.5028} → {φ : α → β → Sort ?u.5027} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
μ: N → N → N
μ
) _ _
m: N
m
#align antitone.covariant_of_const'
Antitone.covariant_of_const': ∀ {N : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} {μ : N → N → N} [inst_2 : CovariantClass N N (swap μ) fun x x_1 => x ≤ x_1], Antitone f → ∀ (m : N), Antitone fun n => f (μ n m)
Antitone.covariant_of_const'
end Monotone theorem
covariant_le_of_covariant_lt: ∀ [inst : PartialOrder N], (Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
covariant_le_of_covariant_lt
[
PartialOrder: Type ?u.5113 → Type ?u.5113
PartialOrder
N: Type ?u.5098
N
] :
Covariant: (M : Type ?u.5118) → (N : Type ?u.5117) → (M → N → N) → (N → N → Prop) → Prop
Covariant
M: Type ?u.5095
M
N: Type ?u.5098
N
μ: M → N → N
μ
(· < ·): N → N → Prop
(· < ·)
→
Covariant: (M : Type ?u.5149) → (N : Type ?u.5148) → (M → N → N) → (N → N → Prop) → Prop
Covariant
M: Type ?u.5095
M
N: Type ?u.5098
N
μ: M → N → N
μ
(· ≤ ·): N → N → Prop
(· ≤ ·)
:=

Goals accomplished! 🐙
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N


(Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Covariant M N μ fun x x_1 => x < x_1

a: M

b, c: N

bc: b ≤ c


μ a b ≤ μ a c
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N


(Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Covariant M N μ fun x x_1 => x < x_1

a: M

b: N

bc: b ≤ b


inl
μ a b ≤ μ a b
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Covariant M N μ fun x x_1 => x < x_1

a: M

b, c: N

bc✝: b ≤ c

bc: b < c


inr
μ a b ≤ μ a c
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N


(Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Covariant M N μ fun x x_1 => x < x_1

a: M

b: N

bc: b ≤ b


inl
μ a b ≤ μ a b
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Covariant M N μ fun x x_1 => x < x_1

a: M

b: N

bc: b ≤ b


inl
μ a b ≤ μ a b
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Covariant M N μ fun x x_1 => x < x_1

a: M

b, c: N

bc✝: b ≤ c

bc: b < c


inr
μ a b ≤ μ a c

Goals accomplished! 🐙
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N


(Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Covariant M N μ fun x x_1 => x < x_1

a: M

b, c: N

bc✝: b ≤ c

bc: b < c


inr
μ a b ≤ μ a c
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Covariant M N μ fun x x_1 => x < x_1

a: M

b, c: N

bc✝: b ≤ c

bc: b < c


inr
μ a b ≤ μ a c

Goals accomplished! 🐙
#align covariant_le_of_covariant_lt
covariant_le_of_covariant_lt: ∀ (M : Type u_2) (N : Type u_1) (μ : M → N → N) [inst : PartialOrder N], (Covariant M N μ fun x x_1 => x < x_1) → Covariant M N μ fun x x_1 => x ≤ x_1
covariant_le_of_covariant_lt
theorem
contravariant_lt_of_contravariant_le: ∀ [inst : PartialOrder N], (Contravariant M N μ fun x x_1 => x ≤ x_1) → Contravariant M N μ fun x x_1 => x < x_1
contravariant_lt_of_contravariant_le
[
PartialOrder: Type ?u.5363 → Type ?u.5363
PartialOrder
N: Type ?u.5348
N
] :
Contravariant: (M : Type ?u.5368) → (N : Type ?u.5367) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
M: Type ?u.5345
M
N: Type ?u.5348
N
μ: M → N → N
μ
(· ≤ ·): N → N → Prop
(· ≤ ·)
→
Contravariant: (M : Type ?u.5399) → (N : Type ?u.5398) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
M: Type ?u.5345
M
N: Type ?u.5348
N
μ: M → N → N
μ
(· < ·): N → N → Prop
(· < ·)
:=

Goals accomplished! 🐙
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N


(Contravariant M N μ fun x x_1 => x ≤ x_1) → Contravariant M N μ fun x x_1 => x < x_1
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Contravariant M N μ fun x x_1 => x ≤ x_1

a: M

b, c: N

bc: (fun x x_1 => x < x_1) (μ a b) (μ a c)


b ≠ c
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N


(Contravariant M N μ fun x x_1 => x ≤ x_1) → Contravariant M N μ fun x x_1 => x < x_1
M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Contravariant M N μ fun x x_1 => x ≤ x_1

a: M

b: N

bc: μ a b < μ a b


M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N

h: Contravariant M N μ fun x x_1 => x ≤ x_1

a: M

b: N

bc: μ a b < μ a b


M: Type u_2

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: PartialOrder N


(Contravariant M N μ fun x x_1 => x ≤ x_1) → Contravariant M N μ fun x x_1 => x < x_1

Goals accomplished! 🐙
#align contravariant_lt_of_contravariant_le
contravariant_lt_of_contravariant_le: ∀ (M : Type u_2) (N : Type u_1) (μ : M → N → N) [inst : PartialOrder N], (Contravariant M N μ fun x x_1 => x ≤ x_1) → Contravariant M N μ fun x x_1 => x < x_1
contravariant_lt_of_contravariant_le
theorem
covariant_le_iff_contravariant_lt: ∀ (M : Type u_2) (N : Type u_1) (μ : M → N → N) [inst : LinearOrder N], (Covariant M N μ fun x x_1 => x ≤ x_1) ↔ Contravariant M N μ fun x x_1 => x < x_1
covariant_le_iff_contravariant_lt
[
LinearOrder: Type ?u.5589 → Type ?u.5589
LinearOrder
N: Type ?u.5574
N
] :
Covariant: (M : Type ?u.5593) → (N : Type ?u.5592) → (M → N → N) → (N → N → Prop) → Prop
Covariant
M: Type ?u.5571
M
N: Type ?u.5574
N
μ: M → N → N
μ
(· ≤ ·): N → N → Prop
(· ≤ ·)
↔
Contravariant: (M : Type ?u.5627) → (N : Type ?u.5626) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
M: Type ?u.5571
M
N: Type ?u.5574
N
μ: M → N → N
μ
(· < ·): N → N → Prop
(· < ·)
:= ⟨fun
h: ?m.5664
h
_: ?m.5667
_
_: ?m.5670
_
_: ?m.5673
_
bc: ?m.5676
bc
↦
not_le: ∀ {α : Type ?u.5680} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_le
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
fun
k: ?m.5699
k
↦
not_le: ∀ {α : Type ?u.5701} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_le
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
bc: ?m.5676
bc
(
h: ?m.5664
h
_: M
_
k: ?m.5699
k
), fun
h: ?m.5739
h
_: ?m.5742
_
_: ?m.5745
_
_: ?m.5748
_
bc: ?m.5751
bc
↦
not_lt: ∀ {α : Type ?u.5755} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
not_lt
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
fun
k: ?m.5769
k
↦
not_lt: ∀ {α : Type ?u.5771} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
not_lt
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
bc: ?m.5751
bc
(
h: ?m.5739
h
_: M
_
k: ?m.5769
k
)⟩ #align covariant_le_iff_contravariant_lt
covariant_le_iff_contravariant_lt: ∀ (M : Type u_2) (N : Type u_1) (μ : M → N → N) [inst : LinearOrder N], (Covariant M N μ fun x x_1 => x ≤ x_1) ↔ Contravariant M N μ fun x x_1 => x < x_1
covariant_le_iff_contravariant_lt
theorem
covariant_lt_iff_contravariant_le: ∀ [inst : LinearOrder N], (Covariant M N μ fun x x_1 => x < x_1) ↔ Contravariant M N μ fun x x_1 => x ≤ x_1
covariant_lt_iff_contravariant_le
[
LinearOrder: Type ?u.5843 → Type ?u.5843
LinearOrder
N: Type ?u.5828
N
] :
Covariant: (M : Type ?u.5847) → (N : Type ?u.5846) → (M → N → N) → (N → N → Prop) → Prop
Covariant
M: Type ?u.5825
M
N: Type ?u.5828
N
μ: M → N → N
μ
(· < ·): N → N → Prop
(· < ·)
↔
Contravariant: (M : Type ?u.5881) → (N : Type ?u.5880) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
M: Type ?u.5825
M
N: Type ?u.5828
N
μ: M → N → N
μ
(· ≤ ·): N → N → Prop
(· ≤ ·)
:= ⟨fun
h: ?m.5918
h
_: ?m.5921
_
_: ?m.5924
_
_: ?m.5927
_
bc: ?m.5930
bc
↦
not_lt: ∀ {α : Type ?u.5934} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
not_lt
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
fun
k: ?m.5953
k
↦
not_lt: ∀ {α : Type ?u.5955} [inst : LinearOrder α] {a b : α}, ¬a < b ↔ b ≤ a
not_lt
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
bc: ?m.5930
bc
(
h: ?m.5918
h
_: M
_
k: ?m.5953
k
), fun
h: ?m.5993
h
_: ?m.5996
_
_: ?m.5999
_
_: ?m.6002
_
bc: ?m.6005
bc
↦
not_le: ∀ {α : Type ?u.6009} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_le
.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
fun
k: ?m.6023
k
↦
not_le: ∀ {α : Type ?u.6025} [inst : LinearOrder α] {a b : α}, ¬a ≤ b ↔ b < a
not_le
.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
bc: ?m.6005
bc
(
h: ?m.5993
h
_: M
_
k: ?m.6023
k
)⟩ #align covariant_lt_iff_contravariant_le
covariant_lt_iff_contravariant_le: ∀ (M : Type u_2) (N : Type u_1) (μ : M → N → N) [inst : LinearOrder N], (Covariant M N μ fun x x_1 => x < x_1) ↔ Contravariant M N μ fun x x_1 => x ≤ x_1
covariant_lt_iff_contravariant_le
-- Porting note: `covariant_flip_mul_iff` used to use the `IsSymmOp` typeclass from Lean 3 core. -- To avoid it, we prove the relevant lemma here. @[
to_additive: ∀ (N : Type u_1) [inst : AddCommSemigroup N], (flip fun x x_1 => x + x_1) = fun x x_1 => x + x_1
to_additive
] lemma
flip_mul: ∀ (N : Type u_1) [inst : CommSemigroup N], (flip fun x x_1 => x * x_1) = fun x x_1 => x * x_1
flip_mul
[
CommSemigroup: Type ?u.6097 → Type ?u.6097
CommSemigroup
N: Type ?u.6082
N
] : (
flip: {α : Sort ?u.6108} → {β : Sort ?u.6107} → {φ : Sort ?u.6106} → (α → β → φ) → β → α → φ
flip
(· * ·): N → N → N
(· * ·)
:
N: Type ?u.6082
N
→
N: Type ?u.6082
N
→
N: Type ?u.6082
N
) =
(· * ·): N → N → N
(· * ·)
:=
funext: ∀ {α : Sort ?u.6470} {β : α → Sort ?u.6469} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext
fun
a: ?m.6487
a
↦
funext: ∀ {α : Sort ?u.6490} {β : α → Sort ?u.6489} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext
fun
b: ?m.6502
b
↦
mul_comm: ∀ {G : Type ?u.6504} [inst : CommSemigroup G] (a b : G), a * b = b * a
mul_comm
b: ?m.6502
b
a: ?m.6487
a
@[
to_additive: ∀ (N : Type u_1) (r : N → N → Prop) [inst : AddCommSemigroup N], Covariant N N (flip fun x x_1 => x + x_1) r ↔ Covariant N N (fun x x_1 => x + x_1) r
to_additive
] theorem
covariant_flip_mul_iff: ∀ (N : Type u_1) (r : N → N → Prop) [inst : CommSemigroup N], Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r
covariant_flip_mul_iff
[
CommSemigroup: Type ?u.6571 → Type ?u.6571
CommSemigroup
N: Type ?u.6556
N
] :
Covariant: (M : Type ?u.6575) → (N : Type ?u.6574) → (M → N → N) → (N → N → Prop) → Prop
Covariant
N: Type ?u.6556
N
N: Type ?u.6556
N
(
flip: {α : Sort ?u.6578} → {β : Sort ?u.6577} → {φ : Sort ?u.6576} → (α → β → φ) → β → α → φ
flip
(· * ·): N → N → N
(· * ·)
)
r: N → N → Prop
r
↔
Covariant: (M : Type ?u.6846) → (N : Type ?u.6845) → (M → N → N) → (N → N → Prop) → Prop
Covariant
N: Type ?u.6556
N
N: Type ?u.6556
N
(· * ·): N → N → N
(· * ·)
r: N → N → Prop
r
:=

Goals accomplished! 🐙
M: Type ?u.6553

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: CommSemigroup N


Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r
M: Type ?u.6553

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: CommSemigroup N


Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r
M: Type ?u.6553

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: CommSemigroup N


Covariant N N (fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r

Goals accomplished! 🐙
#align covariant_flip_mul_iff
covariant_flip_mul_iff: ∀ (N : Type u_1) (r : N → N → Prop) [inst : CommSemigroup N], Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r
covariant_flip_mul_iff
#align covariant_flip_add_iff
covariant_flip_add_iff: ∀ (N : Type u_1) (r : N → N → Prop) [inst : AddCommSemigroup N], Covariant N N (flip fun x x_1 => x + x_1) r ↔ Covariant N N (fun x x_1 => x + x_1) r
covariant_flip_add_iff
@[
to_additive: ∀ (N : Type u_1) (r : N → N → Prop) [inst : AddCommSemigroup N], Contravariant N N (flip fun x x_1 => x + x_1) r ↔ Contravariant N N (fun x x_1 => x + x_1) r
to_additive
] theorem
contravariant_flip_mul_iff: ∀ (N : Type u_1) (r : N → N → Prop) [inst : CommSemigroup N], Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
contravariant_flip_mul_iff
[
CommSemigroup: Type ?u.7086 → Type ?u.7086
CommSemigroup
N: Type ?u.7071
N
] :
Contravariant: (M : Type ?u.7090) → (N : Type ?u.7089) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
N: Type ?u.7071
N
N: Type ?u.7071
N
(
flip: {α : Sort ?u.7093} → {β : Sort ?u.7092} → {φ : Sort ?u.7091} → (α → β → φ) → β → α → φ
flip
(· * ·): N → N → N
(· * ·)
)
r: N → N → Prop
r
↔
Contravariant: (M : Type ?u.7361) → (N : Type ?u.7360) → (M → N → N) → (N → N → Prop) → Prop
Contravariant
N: Type ?u.7071
N
N: Type ?u.7071
N
(· * ·): N → N → N
(· * ·)
r: N → N → Prop
r
:=

Goals accomplished! 🐙
M: Type ?u.7068

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: CommSemigroup N


Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
M: Type ?u.7068

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: CommSemigroup N


Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
M: Type ?u.7068

N: Type u_1

μ: M → N → N

r: N → N → Prop

inst✝: CommSemigroup N


Contravariant N N (fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r

Goals accomplished! 🐙
#align contravariant_flip_mul_iff
contravariant_flip_mul_iff: ∀ (N : Type u_1) (r : N → N → Prop) [inst : CommSemigroup N], Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
contravariant_flip_mul_iff
#align contravariant_flip_add_iff
contravariant_flip_add_iff: ∀ (N : Type u_1) (r : N → N → Prop) [inst : AddCommSemigroup N], Contravariant N N (flip fun x x_1 => x + x_1) r ↔ Contravariant N N (fun x x_1 => x + x_1) r
contravariant_flip_add_iff
@[
to_additive: ∀ (N : Type u_1) [inst : Add N] [inst_1 : LinearOrder N] [inst_2 : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1
to_additive
] instance
contravariant_mul_lt_of_covariant_mul_le: ∀ (N : Type u_1) [inst : Mul N] [inst_1 : LinearOrder N] [inst_2 : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1], ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
contravariant_mul_lt_of_covariant_mul_le
[
Mul: Type ?u.7601 → Type ?u.7601
Mul
N: Type ?u.7586
N
] [
LinearOrder: Type ?u.7604 → Type ?u.7604
LinearOrder
N: Type ?u.7586
N
] [
CovariantClass: (M : Type ?u.7608) → (N : Type ?u.7607) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.7586
N
N: Type ?u.7586
N
(· * ·): N → N → N
(· * ·)
(· ≤ ·): N → N → Prop
(· ≤ ·)
] :
ContravariantClass: (M : Type ?u.7689) → (N : Type ?u.7688) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.7586
N
N: Type ?u.7586
N
(· * ·): N → N → N
(· * ·)
(· < ·): N → N → Prop
(· < ·)
where elim := (
covariant_le_iff_contravariant_lt: ∀ (M : Type ?u.7782) (N : Type ?u.7781) (μ : M → N → N) [inst : LinearOrder N], (Covariant M N μ fun x x_1 => x ≤ x_1) ↔ Contravariant M N μ fun x x_1 => x < x_1
covariant_le_iff_contravariant_lt
N: Type ?u.7586
N
N: Type ?u.7586
N
(· * ·): N → N → N
(· * ·)
).
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp
CovariantClass.elim: ∀ {M : Type ?u.7840} {N : Type ?u.7839} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
CovariantClass.elim
@[
to_additive: ∀ (N : Type u_1) [inst : Add N] [inst_1 : LinearOrder N] [inst_2 : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1
to_additive
] instance
covariant_mul_lt_of_contravariant_mul_le: ∀ (N : Type u_1) [inst : Mul N] [inst_1 : LinearOrder N] [inst_2 : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1], CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
covariant_mul_lt_of_contravariant_mul_le
[
Mul: Type ?u.8055 → Type ?u.8055
Mul
N: Type ?u.8040
N
] [
LinearOrder: Type ?u.8058 → Type ?u.8058
LinearOrder
N: Type ?u.8040
N
] [
ContravariantClass: (M : Type ?u.8062) → (N : Type ?u.8061) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.8040
N
N: Type ?u.8040
N
(· * ·): N → N → N
(· * ·)
(· ≤ ·): N → N → Prop
(· ≤ ·)
] :
CovariantClass: (M : Type ?u.8143) → (N : Type ?u.8142) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.8040
N
N: Type ?u.8040
N
(· * ·): N → N → N
(· * ·)
(· < ·): N → N → Prop
(· < ·)
where elim := (
covariant_lt_iff_contravariant_le: ∀ (M : Type ?u.8236) (N : Type ?u.8235) (μ : M → N → N) [inst : LinearOrder N], (Covariant M N μ fun x x_1 => x < x_1) ↔ Contravariant M N μ fun x x_1 => x ≤ x_1
covariant_lt_iff_contravariant_le
N: Type ?u.8040
N
N: Type ?u.8040
N
(· * ·): N → N → N
(· * ·)
).
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
ContravariantClass.elim: ∀ {M : Type ?u.8294} {N : Type ?u.8293} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r], Contravariant M N μ r
ContravariantClass.elim
@[
to_additive: ∀ (N : Type u_1) [inst : AddCommSemigroup N] [inst_1 : LE N] [inst_2 : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], CovariantClass N N (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
to_additive
] instance
covariant_swap_mul_le_of_covariant_mul_le: ∀ (N : Type u_1) [inst : CommSemigroup N] [inst_1 : LE N] [inst_2 : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1], CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
covariant_swap_mul_le_of_covariant_mul_le
[
CommSemigroup: Type ?u.8516 → Type ?u.8516
CommSemigroup
N: Type ?u.8501
N
] [
LE: Type ?u.8519 → Type ?u.8519
LE
N: Type ?u.8501
N
] [
CovariantClass: (M : Type ?u.8523) → (N : Type ?u.8522) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.8501
N
N: Type ?u.8501
N
(· * ·): N → N → N
(· * ·)
(· ≤ ·): N → N → Prop
(· ≤ ·)
] :
CovariantClass: (M : Type ?u.8791) → (N : Type ?u.8790) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.8501
N
N: Type ?u.8501
N
(
swap: {α : Sort ?u.8794} → {β : Sort ?u.8793} → {φ : α → β → Sort ?u.8792} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
(· ≤ ·): N → N → Prop
(· ≤ ·)
where elim := (
covariant_flip_mul_iff: ∀ (N : Type ?u.9065) (r : N → N → Prop) [inst : CommSemigroup N], Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r
covariant_flip_mul_iff
N: Type ?u.8501
N
(· ≤ ·): N → N → Prop
(· ≤ ·)
).
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
CovariantClass.elim: ∀ {M : Type ?u.9110} {N : Type ?u.9109} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
CovariantClass.elim
@[
to_additive: ∀ (N : Type u_1) [inst : AddCommSemigroup N] [inst_1 : LE N] [inst_2 : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], ContravariantClass N N (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
to_additive
] instance
contravariant_swap_mul_le_of_contravariant_mul_le: ∀ (N : Type u_1) [inst : CommSemigroup N] [inst_1 : LE N] [inst_2 : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1], ContravariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
contravariant_swap_mul_le_of_contravariant_mul_le
[
CommSemigroup: Type ?u.9325 → Type ?u.9325
CommSemigroup
N: Type ?u.9310
N
] [
LE: Type ?u.9328 → Type ?u.9328
LE
N: Type ?u.9310
N
] [
ContravariantClass: (M : Type ?u.9332) → (N : Type ?u.9331) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.9310
N
N: Type ?u.9310
N
(· * ·): N → N → N
(· * ·)
(· ≤ ·): N → N → Prop
(· ≤ ·)
] :
ContravariantClass: (M : Type ?u.9600) → (N : Type ?u.9599) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.9310
N
N: Type ?u.9310
N
(
swap: {α : Sort ?u.9603} → {β : Sort ?u.9602} → {φ : α → β → Sort ?u.9601} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
(· ≤ ·): N → N → Prop
(· ≤ ·)
where elim := (
contravariant_flip_mul_iff: ∀ (N : Type ?u.9874) (r : N → N → Prop) [inst : CommSemigroup N], Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
contravariant_flip_mul_iff
N: Type ?u.9310
N
(· ≤ ·): N → N → Prop
(· ≤ ·)
).
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
ContravariantClass.elim: ∀ {M : Type ?u.9919} {N : Type ?u.9918} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r], Contravariant M N μ r
ContravariantClass.elim
@[
to_additive: ∀ (N : Type u_1) [inst : AddCommSemigroup N] [inst_1 : LT N] [inst_2 : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1], ContravariantClass N N (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
to_additive
] instance
contravariant_swap_mul_lt_of_contravariant_mul_lt: ∀ [inst : CommSemigroup N] [inst_1 : LT N] [inst_2 : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1], ContravariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
contravariant_swap_mul_lt_of_contravariant_mul_lt
[
CommSemigroup: Type ?u.10139 → Type ?u.10139
CommSemigroup
N: Type ?u.10124
N
] [
LT: Type ?u.10142 → Type ?u.10142
LT
N: Type ?u.10124
N
] [
ContravariantClass: (M : Type ?u.10146) → (N : Type ?u.10145) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.10124
N
N: Type ?u.10124
N
(· * ·): N → N → N
(· * ·)
(· < ·): N → N → Prop
(· < ·)
] :
ContravariantClass: (M : Type ?u.10414) → (N : Type ?u.10413) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.10124
N
N: Type ?u.10124
N
(
swap: {α : Sort ?u.10417} → {β : Sort ?u.10416} → {φ : α → β → Sort ?u.10415} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
(· < ·): N → N → Prop
(· < ·)
where elim := (
contravariant_flip_mul_iff: ∀ (N : Type ?u.10688) (r : N → N → Prop) [inst : CommSemigroup N], Contravariant N N (flip fun x x_1 => x * x_1) r ↔ Contravariant N N (fun x x_1 => x * x_1) r
contravariant_flip_mul_iff
N: Type ?u.10124
N
(· < ·): N → N → Prop
(· < ·)
).
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
ContravariantClass.elim: ∀ {M : Type ?u.10733} {N : Type ?u.10732} {μ : M → N → N} {r : N → N → Prop} [self : ContravariantClass M N μ r], Contravariant M N μ r
ContravariantClass.elim
@[
to_additive: ∀ (N : Type u_1) [inst : AddCommSemigroup N] [inst_1 : LT N] [inst_2 : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1], CovariantClass N N (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
to_additive
] instance
covariant_swap_mul_lt_of_covariant_mul_lt: ∀ (N : Type u_1) [inst : CommSemigroup N] [inst_1 : LT N] [inst_2 : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1], CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
covariant_swap_mul_lt_of_covariant_mul_lt
[
CommSemigroup: Type ?u.10956 → Type ?u.10956
CommSemigroup
N: Type ?u.10941
N
] [
LT: Type ?u.10959 → Type ?u.10959
LT
N: Type ?u.10941
N
] [
CovariantClass: (M : Type ?u.10963) → (N : Type ?u.10962) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.10941
N
N: Type ?u.10941
N
(· * ·): N → N → N
(· * ·)
(· < ·): N → N → Prop
(· < ·)
] :
CovariantClass: (M : Type ?u.11231) → (N : Type ?u.11230) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.10941
N
N: Type ?u.10941
N
(
swap: {α : Sort ?u.11234} → {β : Sort ?u.11233} → {φ : α → β → Sort ?u.11232} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
(· < ·): N → N → Prop
(· < ·)
where elim := (
covariant_flip_mul_iff: ∀ (N : Type ?u.11505) (r : N → N → Prop) [inst : CommSemigroup N], Covariant N N (flip fun x x_1 => x * x_1) r ↔ Covariant N N (fun x x_1 => x * x_1) r
covariant_flip_mul_iff
N: Type ?u.10941
N
(· < ·): N → N → Prop
(· < ·)
).
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr
CovariantClass.elim: ∀ {M : Type ?u.11550} {N : Type ?u.11549} {μ : M → N → N} {r : N → N → Prop} [self : CovariantClass M N μ r], Covariant M N μ r
CovariantClass.elim
@[
to_additive: ∀ (N : Type u_1) [inst : AddLeftCancelSemigroup N] [inst_1 : PartialOrder N] [inst_2 : CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], CovariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1
to_additive
] instance
LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le: ∀ [inst : LeftCancelSemigroup N] [inst_1 : PartialOrder N] [inst_2 : CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1], CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1
LeftCancelSemigroup.covariant_mul_lt_of_covariant_mul_le
[
LeftCancelSemigroup: Type ?u.11768 → Type ?u.11768
LeftCancelSemigroup
N: Type ?u.11753
N
] [
PartialOrder: Type ?u.11771 → Type ?u.11771
PartialOrder
N: Type ?u.11753
N
] [
CovariantClass: (M : Type ?u.11775) → (N : Type ?u.11774) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.11753
N
N: Type ?u.11753
N
(· * ·): N → N → N
(· * ·)
(· ≤ ·): N → N → Prop
(· ≤ ·)
] :
CovariantClass: (M : Type ?u.12042) → (N : Type ?u.12041) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.11753
N
N: Type ?u.11753
N
(· * ·): N → N → N
(· * ·)
(· < ·): N → N → Prop
(· < ·)
where elim
a: ?m.12295
a
b: ?m.12298
b
c: ?m.12301
c
bc: ?m.12304
bc
:=

Goals accomplished! 🐙
M: Type ?u.11750

N: Type ?u.11753

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

a, b, c: N

bc: b < c


a * b < a * c
M: Type ?u.11750

N: Type ?u.11753

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

a, b, c: N

bc✝: b < c

bc: b ≤ c

cb: b ≠ c


intro
a * b < a * c
M: Type ?u.11750

N: Type ?u.11753

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: CovariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

a, b, c: N

bc: b < c


a * b < a * c

Goals accomplished! 🐙
@[
to_additive: ∀ (N : Type u_1) [inst : AddRightCancelSemigroup N] [inst_1 : PartialOrder N] [inst_2 : CovariantClass N N (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1], CovariantClass N N (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1
to_additive
] instance
RightCancelSemigroup.covariant_swap_mul_lt_of_covariant_swap_mul_le: ∀ [inst : RightCancelSemigroup N] [inst_1 : PartialOrder N] [inst_2 : CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1], CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
RightCancelSemigroup.covariant_swap_mul_lt_of_covariant_swap_mul_le
[
RightCancelSemigroup: Type ?u.12775 → Type ?u.12775
RightCancelSemigroup
N: Type ?u.12760
N
] [
PartialOrder: Type ?u.12778 → Type ?u.12778
PartialOrder
N: Type ?u.12760
N
] [
CovariantClass: (M : Type ?u.12782) → (N : Type ?u.12781) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.12760
N
N: Type ?u.12760
N
(
swap: {α : Sort ?u.12785} → {β : Sort ?u.12784} → {φ : α → β → Sort ?u.12783} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
(· ≤ ·): N → N → Prop
(· ≤ ·)
] :
CovariantClass: (M : Type ?u.13059) → (N : Type ?u.13058) → (M → N → N) → (N → N → Prop) → Prop
CovariantClass
N: Type ?u.12760
N
N: Type ?u.12760
N
(
swap: {α : Sort ?u.13062} → {β : Sort ?u.13061} → {φ : α → β → Sort ?u.13060} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
(· * ·): N → N → N
(· * ·)
)
(· < ·): N → N → Prop
(· < ·)
where elim
a: ?m.13322
a
b: ?m.13325
b
c: ?m.13328
c
bc: ?m.13331
bc
:=

Goals accomplished! 🐙
M: Type ?u.12757

N: Type ?u.12760

μ: M → N → N

r: N → N → Prop

inst✝²: RightCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

a, b, c: N

bc: b < c


swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c
M: Type ?u.12757

N: Type ?u.12760

μ: M → N → N

r: N → N → Prop

inst✝²: RightCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

a, b, c: N

bc✝: b < c

bc: b ≤ c

cb: b ≠ c


intro
swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c
M: Type ?u.12757

N: Type ?u.12760

μ: M → N → N

r: N → N → Prop

inst✝²: RightCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: CovariantClass N N (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1

a, b, c: N

bc: b < c


swap (fun x x_1 => x * x_1) a b < swap (fun x x_1 => x * x_1) a c

Goals accomplished! 🐙
@[
to_additive: ∀ (N : Type u_1) [inst : AddLeftCancelSemigroup N] [inst_1 : PartialOrder N] [inst_2 : ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x < x_1], ContravariantClass N N (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
to_additive
] instance
LeftCancelSemigroup.contravariant_mul_le_of_contravariant_mul_lt: ∀ [inst : LeftCancelSemigroup N] [inst_1 : PartialOrder N] [inst_2 : ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1], ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
LeftCancelSemigroup.contravariant_mul_le_of_contravariant_mul_lt
[
LeftCancelSemigroup: Type ?u.13823 → Type ?u.13823
LeftCancelSemigroup
N: Type ?u.13808
N
] [
PartialOrder: Type ?u.13826 → Type ?u.13826
PartialOrder
N: Type ?u.13808
N
] [
ContravariantClass: (M : Type ?u.13830) → (N : Type ?u.13829) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.13808
N
N: Type ?u.13808
N
(· * ·): N → N → N
(· * ·)
(· < ·): N → N → Prop
(· < ·)
] :
ContravariantClass: (M : Type ?u.14097) → (N : Type ?u.14096) → (M → N → N) → (N → N → Prop) → Prop
ContravariantClass
N: Type ?u.13808
N
N: Type ?u.13808
N
(· * ·): N → N → N
(· * ·)
(· ≤ ·): N → N → Prop
(· ≤ ·)
where elim
a: ?m.14350
a
b: ?m.14353
b
c: ?m.14356
c
bc: ?m.14359
bc
:=

Goals accomplished! 🐙
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c


b ≤ c
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c

h: a * b = a * c


inl
b ≤ c
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c

h: a * b < a * c


inr
b ≤ c
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c


b ≤ c
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c

h: a * b = a * c


inl
b ≤ c
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c

h: a * b = a * c


inl
b ≤ c
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c

h: a * b < a * c


inr
b ≤ c

Goals accomplished! 🐙
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c


b ≤ c
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c

h: a * b < a * c


inr
b ≤ c
M: Type ?u.13805

N: Type ?u.13808

μ: M → N → N

r: N → N → Prop

inst✝²: LeftCancelSemigroup N

inst✝¹: PartialOrder N

inst✝: ContravariantClass N N (fun x x_1 => x * x_1) fun x x_1 => x < x_1

a, b, c: N

bc: a * b ≤ a * c

h: a * b < a * c


inr
b ≤ c

Goals accomplished! 🐙
@[