mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Operations

Goal state before:
pp: α : Type u
β : Type v
f : α → β
p : β → Prop
h : ∀ (a : α), p (f a)
⊢ range (Subtype.coind f h) = Subtype.val ⁻¹' range f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Operations

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → γ
s : Set α
t : Set β
⊢ (f '' s) ×ˢ t = (fun x ↦ (f x.fst, x.snd)) '' s ×ˢ t

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Operations

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → γ
s : Set α
t : Set β
⊢ t ×ˢ (f '' s) = (fun x ↦ (x.fst, f x.snd)) '' t ×ˢ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Operations

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
t : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ univ.pi t ↔ ∀ (i : ι), f i ∈ t i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a b : α
a' b' : β
h : ∀ {o : Ordering}, o.Compares a b → o.Compares a' b'
o : Ordering
⊢ o.Compares a b ↔ o.Compares a' b'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : α
o : Ordering
⊢ o.Compares (toDual a) (toDual b) ↔ o.Compares b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LT α
a b : αᵒᵈ
o : Ordering
⊢ o.Compares (ofDual a) (ofDual b) ↔ o.Compares b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (cmp a b).Compares a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableLT α
a b : α
⊢ (cmp a b).swap = cmp b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
⊢ cmp x x = eq

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ cmp y x = cmp y' x'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp y x = cmp y' x'
⊢ cmp x y = cmp x' y'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x < y ↔ x' < y'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x ≤ y ↔ x' ≤ y'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Compare

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
x y : α
β : Type u_3
inst✝ : LinearOrder β
x' y' : β
h : cmp x y = cmp x' y'
⊢ x = y ↔ x' = y'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f a ≤ f b) = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b ≤ a → f b ≤ f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f b ≤ f a) = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b ≤ a → f a ≤ f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f a < f b) = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b < a → f b < f a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ (∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a < b → f b < f a) = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → b < a → f a < f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
inst✝ : LinearOrder α
f : α → β
h : ∀ (x y : α), x < y → f x ≠ f y
⊢ Injective f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : γ → α
g : γ → β
⊢ (Monotone fun x ↦ (f x, g x)) ↔ Monotone f ∧ Monotone g

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictMono f
hg : StrictMono g
a b : α × β
⊢ a < b → Prod.map f g a < Prod.map f g b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a < b → Prod.map f g b < Prod.map f g a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: ι : Type u_1
α : Type u
β : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (β i)
inst✝ : Preorder α
f : α → (i : ι) → β i
⊢ Monotone f ↔ ∀ (i : ι), Monotone fun x ↦ f x i

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Defs

Goal state before:
pp: ι : Type u_1
α : Type u
β : ι → Type u_4
inst✝¹ : (i : ι) → Preorder (β i)
inst✝ : Preorder α
f : α → (i : ι) → β i
⊢ Antitone f ↔ ∀ (i : ι), Antitone fun x ↦ f x i

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Subsingleton α
⊢ ∀ (a b : α), r a b = emptyRelation a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsStrictOrder α r
x y : α
h : r x y
e : y = x
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsOrderConnected α r
a b c : α
h₁ : ¬r a b
h₂ : ¬r b c
⊢ ¬(r a b ∨ r b c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r✝ : α → α → Prop
s : β → β → Prop
r : α → α → Prop
inst✝ : IsWellOrder α r
a b c : α
hab : r a b
hbc : r b c
⊢ r a c

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
x✝¹ x✝ : α × β
a₁ : α
a₂ : β
b₁ : α
b₂ : β
hab : ¬Prod.Lex r s (a₁, a₂) (b₁, b₂)
hba : ¬Prod.Lex r s (b₁, b₂) (a₁, a₂)
⊢ (a₁, a₂) = (b₁, b₂)

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝³ : Preorder α
inst✝² : WellFoundedLT α
inst✝¹ : Preorder β
inst✝ : WellFoundedLT β
⊢ WellFounded fun x1 x2 ↦ x1 < x2

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Bounded r s ↔ Unbounded r s

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
s : Set α
⊢ ¬Unbounded r s ↔ Bounded r s

Tactic:
by

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
β : Type v
r : α → α → Prop
s : β → β → Prop
inst✝ : LinearOrder α
⊢ ∀ (a b : α), ¬a < b → ¬b < a → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
a b : α
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : OrderBot α
a b : α
ha : a ≠ ⊥
hb : b ≠ ⊥
⊢ min a b ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.BoundedOrder.Lattice

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : WellFoundedGT α
inst✝ : OrderTop α
P : α → Prop
hexists : ∃ M, P M
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ M, M > N ∧ P M
⊢ P ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: p q : Prop
⊢ p ≤ q ∨ q ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ⊢ LinearOrder Prop

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → OrderBot (α' i)
f g : (i : ι) → α' i
⊢ Disjoint f g ↔ ∀ (i : ι), Disjoint (f i) (g i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: ι : Type u_1
α' : ι → Type u_3
inst✝¹ : (i : ι) → PartialOrder (α' i)
inst✝ : (i : ι) → BoundedOrder (α' i)
f g : (i : ι) → α' i
⊢ IsCompl f g ↔ ∀ (i : ι), IsCompl (f i) (g i)

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
h : r = ⊤
⊢ ∀ (a : α), r a a

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
x✝ : Std.Refl r
⊢ ∀ (a b : α), r a b = ⊤ a b

Tactic:
simp [rel_of_subsingleton]

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
x✝ : Std.Refl r
⊢ ∀ (a b : α), r a b = ⊤ a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
h : r = ⊥
⊢ ∀ (a : α), ¬r a a

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: α : Type u_2
inst✝ : Subsingleton α
r : α → α → Prop
x✝ : Std.Irrefl r
⊢ ∀ (a b : α), r a b = ⊥ a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.PropInstances

Goal state before:
pp: P Q : Prop
⊢ IsCompl P Q ↔ ¬(P ↔ Q)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Monotone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Monotone f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ Antitone (⇑toDual ∘ f ∘ ⇑ofDual) ↔ Antitone f

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
x : β
y : δ
hx : condβα (coeβα x, coeδγ y).fst
hy : condδγ (coeβα x, coeδγ y).snd
⊢ map coeβα coeδγ (x, y) = (coeβα x, coeδγ y)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
⊢ ∀ (x : α × γ), condβα x.fst ∧ condδγ x.snd → ∃ y, map coeβα coeδγ y = x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ MonotoneOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Lift

Goal state before:
pp: ι : Sort u_1
α : ι → Sort u_2
ne : ∀ (i : ι), Nonempty (α i)
p : ι → Prop
f : (i : Subtype p) → α i.val
⊢ ∃ g, (fun i ↦ g i.val) = f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ AntitoneOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictMono (⇑toDual ∘ f ∘ ⇑ofDual) ↔ StrictMono f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ StrictAnti (⇑toDual ∘ f ∘ ⇑ofDual) ↔ StrictAnti f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictMonoOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (⇑toDual ∘ f ∘ ⇑ofDual) s ↔ StrictAntiOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ m + f n ≤ f (m + n)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
h : Disjoint a b
x : α
h₁ : x ≤ a
h₂ : x ≤ b
⊢ x = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
ha : a ≠ ⊥
hab : Disjoint a b
h : a = b
⊢ Disjoint a a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
hab : Disjoint a b
⊢ a = b ↔ a = ⊥ ∧ b = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
hab : Disjoint a b
⊢ a ≠ b ↔ a ≠ ⊥ ∨ b ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
h : a ≤ b
⊢ Disjoint a b ↔ a = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
a b : α
h : Disjoint a b
ha : a ≠ ⊥
⊢ b ≠ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
⊢ StrictMono fun x ↦ if p x then f x else g x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ a = b → f a = f b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
⊢ Disjoint a b ↔ Disjoint ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint a (b ⊓ c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint a (b ⊓ c) ↔ Disjoint b (a ⊓ c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊓ b) c ↔ Disjoint (a ⊓ c) b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
⊢ Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
a b c : α
h : a ≤ c ⊔ b
hd : Disjoint a c
⊢ a ≤ b ⊔ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
⊢ Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
⊢ Codisjoint a (b ⊓ c) ↔ Codisjoint a b ∧ Codisjoint a c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : OrderTop α
a b c : α
h : b ⊓ a ≤ c
hd : Codisjoint b c
⊢ a ⊓ b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x y : α
h₁ : x ⊓ y ≤ ⊥
h₂ : ⊤ ≤ x ⊔ y
⊢ Disjoint x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x y : α
h₁ : x ⊓ y ≤ ⊥
h₂ : ⊤ ≤ x ⊔ y
⊢ Codisjoint x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ Disjoint x y ↔ x ≤ z

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔ ∃ a b c, a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
hbc : b < c
⊢ r (f b) (f c)

Tactic:
induction hbc with
  | refl => exact h _ hab
  | step b_lt_k r_b_k => exact _root_.trans r_b_k (h _ (hab.trans_lt b_lt_k).le)

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℕ → β
a : ℕ
h : ∀ (n : ℕ), a ≤ n → r (f n) (f (n + 1))
b c : ℕ
hab : a ≤ b
hbc : b < c
⊢ r (f b) (f c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
k : ℕ
⊢ (Monotone fun n ↦ f (n + k)) ↔ MonotoneOn f {x | k ≤ x}

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
⊢ ∃ f, StrictMono f ∧ f 0 = a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: P : ℕ → Prop
h : ∀ (N : ℕ), ∃ n, n > N ∧ P n
⊢ ∃ φ, StrictMono φ ∧ ∀ (n : ℕ), P (φ n)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: ⊢ Monotone fun n ↦ n ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
x y : α × β
⊢ Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: β : Type v
r : β → β → Prop
inst✝ : IsTrans β r
f : ℤ → β
h : ∀ (n : ℤ), r (f n) (f (n + 1))
a b : ℤ
hab : a < b
⊢ r (f a) (f b)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : BoundedOrder α
inst✝ : BoundedOrder β
x y : α × β
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
x : α
h : IsCompl x ⊥
⊢ x = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : Subsingleton α
⊢ ComplementedLattice α

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a < ↑b ↔ a < b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
⊢ ⟨⊥, ⋯⟩ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
⊢ ⟨⊤, ⋯⟩ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ∃ f, StrictMono f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Monotone f
n : ℕ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℕ
⊢ f a ≠ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℕ → α
hf : Antitone f
n : ℕ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℕ
⊢ f a ≠ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Monotone f
n : ℤ
x : α
h1 : f n < x
h2 : x < f (n + 1)
a : ℤ
⊢ f a ≠ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Basic

Goal state before:
pp: α : Type u
inst✝ : Preorder α
f : ℤ → α
hf : Antitone f
n : ℤ
x : α
h1 : f (n + 1) < x
h2 : x < f n
a : ℤ
⊢ f a ≠ x

Tactic:
by

Goal state after: