mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteBooleanAlgebra β
⊢ CompleteBooleanAlgebra α

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b ∈ Ι a c → c ∈ Ι a b → b = c

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
ha : a ≤ c
hb : b ≤ c
⊢ a ∉ Ι b c → b ∉ Ι a c → a = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
s : Set ι
f : ι → α
⊢ (s.PairwiseDisjoint fun i ↦ {f i}) ↔ InjOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective fun b ↦ Ι b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ Injective (Ι a)

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α
⊢ (Pairwise fun i j ↦ ¬f i = f j) ↔ Injective f

Tactic:
by

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: α : Type u_1
ι : Type u_4
f : ι → α
⊢ (Pairwise fun i j ↦ f i ≠ f j) ↔ Injective f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ uIoo a b = Ioo a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
h : b ≤ a
⊢ uIoo a b = Ioo b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b = uIoo b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
⊢ uIoo a a = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ a ∉ uIoo a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ b ∉ uIoo a b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b ⊆ [[a, b]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
a b : α
inst✝ : DenselyOrdered α
⊢ (uIoo a b).Nonempty ↔ a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ (Ι a b).Nonempty ↔ a ≠ b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ uIoo a b = Ioo a b ∪ Ioo b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
e : α ≃ β
inst✝ : CompleteAtomicBooleanAlgebra β
⊢ CompleteAtomicBooleanAlgebra α

Tactic:
by

Goal state after:
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
i : SetLike A B
inst✝ : Subsingleton B
S : A
h : Nonempty ↥S
b : B
⊢ b ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
i : SetLike A B
inst✝¹ : LE A
inst✝ : OrderTop A
s : A
hs : s ≠ ⊤
h_top : ↑⊤ = Set.univ
⊢ ∃ b, ¬b ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : LE A
inst✝ : IsConcreteLE A B
S T : A
⊢ S ≤ T ↔ ∀ ⦃x : B⦄, x ∈ S → x ∈ T

Tactic:
by

Goal state after:
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : LE A
inst✝ : IsConcreteLE A B
p q : A
⊢ ¬p ≤ q ↔ ∃ x, x ∈ p ∧ ¬x ∈ q

Tactic:
by

Goal state after:
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
S T : A
⊢ ↑S ⊂ ↑T ↔ S < T

Tactic:
by

Goal state after:
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
p q : A
⊢ p < q → ∃ x, x ∈ q ∧ ¬x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Data.SetLike.Basic

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝² : SetLike A B
inst✝¹ : PartialOrder A
inst✝ : IsConcreteLE A B
p q : A
⊢ p < q ↔ p ≤ q ∧ ∃ x, x ∈ q ∧ ¬x ∈ p

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ s.OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Icc x y = Icc (e x) (e y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IsChain r univ ↔ Std.Trichotomous r

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ico x y = Ico (e x) (e y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ioc x y = Ioc (e x) (e y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : α → β
hf : Function.Injective f
h : ∀ (x y : α), s (f x) (f y) → r x y
c : Set β
hrc : IsChain s c
⊢ IsChain r (f ⁻¹' c)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : (range ⇑e).OrdConnected
x y : α
⊢ ⇑e '' Ioo x y = Ioo (e x) (e y)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : s.OrdConnected
x y : ↑s
⊢ (range ⇑(OrderEmbedding.subtype fun x ↦ x ∈ s)).OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain r (s ∪ t) ↔ IsChain r s ∧ IsChain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∨ r b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
hf : Monotone f
⊢ IsChain (fun x1 x2 ↦ x1 ≤ x2) (range f)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsChain (fun x1 x2 ↦ r ↑x1 ↑x2) (s ↓∩ t) ↔ IsChain r (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsChain (fun x1 x2 ↦ r ↑x1 ↑x2) univ ↔ IsChain r s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
h : (⇑ofDual ⁻¹' s).OrdConnected
⊢ s.OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_3
inst✝ : PartialOrder α
a : α
⊢ {a}.OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : β → α
c : Set β
h : IsChain (f ⁻¹'o r) c
x✝¹ x✝ : { a // a ∈ c }
a : β
ha : a ∈ c
b : β
hb : b ∈ c
hab : a = b
⊢ ∃ z, r ((fun x ↦ f ↑x) ⟨a, ha⟩) ((fun x ↦ f ↑x) z) ∧ r ((fun x ↦ f ↑x) ⟨b, hb⟩) ((fun x ↦ f ↑x) z)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
s : Set α
hs : s.OrdConnected
⊢ (⇑e '' s).OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
E : Type u_3
inst✝¹ : EquivLike E α β
inst✝ : OrderIsoClass E α β
e : E
⊢ (range ⇑e).OrdConnected

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
inst✝¹ : Std.Refl r
hchain : IsChain r s
inst✝ : IsTrans α r
a b c : α
mem1 : a ∈ s
mem2 : b ∈ s
mem3 : c ∈ s
⊢ ∃ z, ∃ (_ : z ∈ s), r a z ∧ r b z ∧ r c z

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
r : α → α → Prop
c c₁ c₂ s✝ t : Set α
a b x y : α
inst✝¹ : PartialOrder α
inst✝ : DecidableLE α
s : Set α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
⊢ ∀ (a b : ↑s), a ≤ b ∨ b ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
⊢ s.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : Preorder α
hs : IsChain (fun x1 x2 ↦ x1 ≤ x2) s
x y : α
hx : x ∈ s
hy : y ∈ s
h : ¬x < y
⊢ y ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
inst✝ : Std.Trichotomous r
h : IsAntichain r s
⊢ s.Subsingleton

Tactic:
by
  rintro a ha b hb
  obtain hab | hab | hab := trichotomous_of r a b
  · exact h.eq ha hb hab
  · exact hab
  · exact h.eq' ha hb hab

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
⊢ IsAntichain r' (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
u : Set β := {x | (∃ y ∈ t, y ≤ x ∧ f y ∈ s) ∧ ∃ z ∈ t, x ≤ z ∧ f z ∈ s}
x : β
xt : x ∈ t
xs : x ∈ f ⁻¹' s
⊢ x ∈ t ∩ u

Tactic:
exact ⟨xt, ⟨x, xt, le_rfl, xs⟩, ⟨x, xt, le_rfl, xs⟩⟩

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxChain r c
t : Set β
ht : IsChain s t
hf : ⇑e '' c ⊆ t
⊢ ⇑e '' c = t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ IsEmpty α ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxChain r s
⊢ ¬Nonempty α ↔ ¬s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ SuperChain r s (SuccChain r s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : φ a ≠ φ a'
h₂ : r' (φ a) (φ a')
haa' : a = a'
⊢ φ a = φ a'

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
⊢ IsChain r (SuccChain r s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
⊢ IsAntichain r' (⇑φ '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsAntichain (fun x1 x2 ↦ r ↑x1 ↑x2) (s ↓∩ t) ↔ IsAntichain r (s ∩ t)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : β → α
t : Set β
s : Set α
hs : s.OrdConnected
hf : MonotoneOn f t
⊢ ∃ u, u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ IsAntichain (fun x1 x2 ↦ r ↑x1 ↑x2) univ ↔ IsAntichain r s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ SuperChain r s (SuccChain r s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
⊢ s ⊆ SuccChain r s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
z : α
hz : z ∈ Icc x y
⊢ z ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ (s ∩ Icc x y).OrdConnected ↔ Ioo x y ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
⊢ s.Subsingleton

Tactic:
by

Goal state after:
Module: Mathlib.Order.Preorder.Chain

Goal state before:
pp: α : Type u_1
β : Type u_2
F : Type u_3
inst✝ : LE α
s✝ t✝ : Flag α
a : α
s t : Flag α
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsChain r s
ht : IsAntichain r t
⊢ s ∩ t ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Set α
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ ¬(s ∩ Icc x y).OrdConnected ↔ ∃ z ∉ s, z ∈ Ioo x y

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s t : Set α
hs : IsChain r s
ht : IsAntichain r t
⊢ s ∩ t ⊆ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsLeast s a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
h : ∀ y ∈ s, [[x, y]] ⊆ s
y : α
hy : y ∈ s
z : α
hz : z ∈ s
⊢ [[y, x]] ∪ [[x, z]] = [[x, y]] ∪ [[x, z]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s : Set α
a : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s ∧ IsGreatest s a

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s : Set α
x : α
hx : x ∈ s
⊢ s.OrdConnected ↔ ∀ ⦃y : α⦄, y ∈ s → [[y, x]] ⊆ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : s.OrdConnected
a b : ↑s
⊢ Subtype.val '' [[a, b]] = [[↑a, ↑b]]

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : s.OrdConnected
a b : ↑s
⊢ Subtype.val '' Ι a b = Ι ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : s.OrdConnected
a b : ↑s
⊢ Subtype.val '' uIoo a b = uIoo ↑a ↑b

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
s t : Set α
inst✝ : Preorder α
ht : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun x ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun x ↦ x ∈ s) b
⊢ {x | Maximal (fun x ↦ x ∈ s) x} = t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
⊢ IsStrongAntichain r' (f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : ⇑e '' c ⊆ t
⊢ ⇑e '' c = t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ IsEmpty α ↔ s = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Order.Antichain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ ¬Nonempty α ↔ ¬s.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
⊢ 0 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ a * b ≤ a * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b : β
ab : a ≤ b
c : β
⊢ f (a * c) ≤ f (b * c)

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
a : S
ha : 0 ≤ a
b c : S
hbc : b ≤ c
⊢ b * a ≤ c * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : Preorder β
f : β → α
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a b c : β
bc : a * b ≤ a * c
⊢ f a * f b ≤ f a * f c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Basic

Goal state before:
pp: α : Type u
β : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : Preorder α
inst✝² : IsOrderedCancelMonoid α
inst✝¹ : CommMonoid β
inst✝ : LinearOrder β
f : β → α
hf : StrictMono f
mul : ∀ (x y : β), f (x * y) = f x * f y
a b c : β
h : a * b ≤ a * c
⊢ b ≤ c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ a * b < a * c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Ring.InjSurj

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : Semiring R
inst✝³ : PartialOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : Semiring S
inst✝ : PartialOrder S
f : S → R
zero : f 0 = 0
one : f 1 = 1
add : ∀ (x y : S), f (x + y) = f x + f y
mul : ∀ (x y : S), f (x * y) = f x * f y
le : ∀ {x y : S}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : S}, f x < f y ↔ x < y
a : S
ha : 0 < a
b c : S
hbc : b < c
⊢ b * a < c * a

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
⊢ sSup ∅ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : ↑a ≤ ↑b
c : α
hc : ↑b = ↑a + c
⊢ b = a + ⟨c, ?m.49⟩

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : ExistsAddOfLE α
a b : { x // 0 ≤ x }
h : a ≤ b
⊢ ∃ c, b = a + c

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Nontrivial α
inst✝² : AddGroup α
inst✝¹ : LinearOrder α
inst✝ : AddLeftMono α
⊢ Nontrivial { x // 0 ≤ x }

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝³ : Semiring α
inst✝² : PartialOrder α
inst✝¹ : IsOrderedRing α
inst✝ : NoZeroDivisors α
⊢ ∀ {a b : { x // 0 ≤ x }}, a * b = 0 → a = 0 ∨ b = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Order.Nonneg.Ring

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
⊢ ∀ (a b c : { x // 0 ≤ x }), a - b ≤ c ↔ a ≤ c + b

Tactic:
by

Goal state after:
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : SupSet α
inst✝ : Inhabited ↑s
t : Set ↑s
h' : t.Nonempty
h'' : BddAbove t
h : sSup (Subtype.val '' t) ∈ s
⊢ sSup (Subtype.val '' t) = ↑(sSup t)

Tactic:
by

Goal state after: