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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) ↔ ∃ i, x ∈ C i

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_5
C : ι → Set α
f : (x : ι) → β → ↑(C x)
hf : ∀ (x : ι), Surjective (f x)
x : α
⊢ (∃ i, x ∈ range fun x ↦ ↑(f x i)) ↔ ∃ i, x ∈ C i
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ sSup (range ((fun f ↦ f a) ∘ f)) = sSup (range fun i ↦ f i a)

Tactic:
;

Goal state after:
α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst✝ : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ sSup (range ((fun f ↦ f a) ∘ f)) = sSup (range fun i ↦ f i a)
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsLUB ((fun {y} ↦ f y) '' x✝) (⨆ a ∈ x✝, f a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsLUB ((fun {y} ↦ f y) '' x✝) (⨆ a ∈ x✝, f a)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
i_ne_j : ¬i = j
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
ι : Type u_12
Es : ι → Set α
Es_union : ⋃ i, Es i = univ
Es_disj : Pairwise fun i j ↦ Disjoint (Es i) (Es j)
I : Set ι
x : α
i : ι
hix : x ∈ Es i
J : Set ι
j : ι
j_in_J : j ∈ J
hjx : x ∈ Es j
i_ne_j : ¬i = j
⊢ False
Module: Mathlib.Order.CompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsGLB ((fun {x} ↦ f x) '' x✝) (⨅ a ∈ x✝, f a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst✝⁸ : Max α
inst✝⁷ : Min α
inst✝⁶ : LE α
inst✝⁵ : LT α
inst✝⁴ : SupSet α
inst✝³ : InfSet α
inst✝² : Top α
inst✝¹ : Bot α
inst✝ : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x✝ : Set α
⊢ IsGLB ((fun {x} ↦ f x) '' x✝) (⨅ a ∈ x✝, f a)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
c : α
⊢ c ∈ ⋂ i, Iic (f i) ↔ c ∈ lowerBounds (range f)

Tactic:
;

Goal state after:
α : Type u_1
ι : Sort u_5
inst✝ : Preorder α
f : ι → α
c : α
⊢ c ∈ ⋂ i, Iic (f i) ↔ c ∈ lowerBounds (range f)
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₁, h₂⟩⟩.snd

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ : b₁ ∈ t a₁
a₂ : α
a_eq : a₁ = a₂
h₂ : b₁ ∈ t a₂
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₂, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn a_eq ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₂, ⟨b₁, h₂⟩⟩.snd
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₁, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn ⋯ ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₁, ⟨b₁, h₂⟩⟩.snd

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
t : α → Set β
h : Pairwise (Disjoint on t)
a₁ : α
b₁ : β
h₁ h₂ : b₁ ∈ t a₁
eq : sigmaToiUnion t ⟨a₁, ⟨b₁, h₁⟩⟩ = sigmaToiUnion t ⟨a₁, ⟨b₁, h₂⟩⟩
⊢ ↑(Eq.recOn ⋯ ⟨a₁, ⟨b₁, h₁⟩⟩.snd) = ↑⟨a₁, ⟨b₁, h₂⟩⟩.snd
Module: Mathlib.Data.Set.Lattice

Goal state before:
pp: α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
| ↑x

Tactic:
;

Goal state after:
α : Type u_12
β : Type u_13
t : α → Set β
h : Pairwise (Disjoint on t)
x : ↑(⋃ i, t i)
| ↑x
Module: Mathlib.Order.Interval.Set.Image

Goal state before:
pp: α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} ↔ x✝ ∈ {y | r (↑c) y ∧ q y b}

Tactic:
;

Goal state after:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r (↑c) x → p a x
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r (↑c) y} ↔ x✝ ∈ {y | r (↑c) y ∧ q y b}
Module: Mathlib.Order.Interval.Set.Image

Goal state before:
pp: α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r y ↑c} ↔ x✝ ∈ {y | p a y ∧ r y ↑c}

Tactic:
;

Goal state after:
α : Type u_1
p q r : α → α → Prop
a b : α
c : { x // p a x ∧ q x b }
h : ∀ {x : α}, r x ↑c → q x b
x✝ : α
⊢ x✝ ∈ {x | p a x ∧ q x b} ∩ {y | r y ↑c} ↔ x✝ ∈ {y | p a y ∧ r y ↑c}
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompletelyDistribLattice (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
i : ι
⊢ (⨅ a, ⨆ b, f a b) i = (⨆ g, ⨅ a, f a (g a)) i

Tactic:
;

Goal state after:
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompletelyDistribLattice (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
i : ι
⊢ (⨅ a, ⨆ b, f a b) i = (⨆ g, ⨅ a, f a (g a)) i
Module: Mathlib.Order.CompleteBooleanAlgebra

Goal state before:
pp: α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
x✝ : ι
⊢ (⨅ a, ⨆ b, f a b) x✝ = (⨆ g, ⨅ a, f a (g a)) x✝

Tactic:
;

Goal state after:
α : Type u
β : Type v
ι✝¹ : Sort w
κ : ι✝¹ → Sort w'
ι : Type u_1
π : ι → Type u_2
inst✝ : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι✝ : Type (max u_1 u_2)
κ✝ : ι✝ → Type (max u_1 u_2)
f : (a : ι✝) → κ✝ a → (i : ι) → π i
x✝ : ι
⊢ (⨅ a, ⨆ b, f a b) x✝ = (⨆ g, ⨅ a, f a (g a)) x✝
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case ht
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ BddBelow (f '' t)

pp: case hs
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ (f '' s).Nonempty

Tactic:
;

Goal state after:
case ht
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ BddBelow (f '' t)

case hs
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ (f '' s).Nonempty
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x : α
h : IsTop x
y : α
⊢ y ∈ Ici x ↔ y ∈ {x}

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x : α
h : IsTop x
y : α
⊢ y ∈ Ici x ↔ y ∈ {x}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ Icc a b = ⇑ofDual ⁻¹' Icc a b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : AntitoneOn f (Icc a b)
⊢ Icc a b = ⇑ofDual ⁻¹' Icc a b
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Icc (e x) (e y) ↔ x✝ ∈ Icc x y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Icc (e x) (e y) ↔ x✝ ∈ Icc x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ico (e x) (e y) ↔ x✝ ∈ Ico x y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ico (e x) (e y) ↔ x✝ ∈ Ico x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioc (e x) (e y) ↔ x✝ ∈ Ioc x y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioc (e x) (e y) ↔ x✝ ∈ Ioc x y
Module: Mathlib.Order.Interval.Set.OrderEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioo (e x) (e y) ↔ x✝ ∈ Ioo x y

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
x y x✝ : α
⊢ x✝ ∈ ⇑e ⁻¹' Ioo (e x) (e y) ↔ x✝ ∈ Ioo x y
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂

Tactic:
rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
a₁ a₂ : α
hne : e a₁ ≠ e a₂
⊢ (Disjoint on extend e f ⊥) (e a₁) (e a₂)

case inl.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : PartialOrder γ
inst✝ : OrderBot γ
e : α → β
f : α → γ
hf : Pairwise (Disjoint on f)
he : FactorsThrough f e
b₂ : β
a₁ : α
hne : e a₁ ≠ b₂
hb₂ : ¬∃ a₂, e a₂ = b₂
⊢ (Disjoint on extend e f ⊥) (e a₁) b₂
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a b : α
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)

Tactic:
inf_comm,

Goal state after:
α : Type u_1
inst✝ : Lattice α
a b : α
⊢ Icc (a ⊓ b) (a ⊔ b) = Icc (a ⊓ b) (b ⊔ a)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: ι : Type u_4
s : Set ι
x✝ : ι
⊢ x✝ ∈ s → ∀ ⦃y : ι⦄, y ∈ s → x✝ ≠ y → (Disjoint on singleton) x✝ y

Tactic:
;

Goal state after:
ι : Type u_4
s : Set ι
x✝ : ι
⊢ x✝ ∈ s → ∀ ⦃y : ι⦄, y ∈ s → x✝ ≠ y → (Disjoint on singleton) x✝ y
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
⊢ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ioc a b ∪ Ι b c = Ι a c

Tactic:
uIoc_of_le h.2,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a✝ b c✝ a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ioc a b ∪ Ioc b c = Ι a c
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioo (min a b) (max a b) = Ioo (min b a) (max b a)

Tactic:
inf_comm,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ Ioo (min a b) (max a b) = Ioo (min a b) (max b a)
Module: Mathlib.Order.Interval.Set.OrdConnected

Goal state before:
pp: case inl
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s

pp: case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s

Tactic:
;

Goal state after:
case inl
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx hy : x ∈ s
hxy : x ≤ x
⊢ Icc x x ⊆ s

case inr
α : Type u_3
inst✝ : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
hxy' : x < y
⊢ Icc x y ⊆ s
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
⊢ f a * f b ≤ f a * f c

Tactic:
;

Goal state after:
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
⊢ f a * f b ≤ f a * f c
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
⊢ 0 ≤ f a

Tactic:
;

Goal state after:
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
⊢ 0 ≤ f a
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
⊢ f b * f a ≤ f c * f a

Tactic:
;

Goal state after:
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
⊢ f b * f a ≤ f c * f a
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 * f c ≤ f b * f c

Tactic:
;

Goal state after:
α : 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 * f c ≤ f b * f c
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
⊢ f a * f b < f a * f c

Tactic:
;

Goal state after:
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
⊢ f a * f b < f a * f c
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
⊢ 0 < f a

Tactic:
;

Goal state after:
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
⊢ 0 < f a
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
⊢ f b * f a < f c * f a

Tactic:
;

Goal state after:
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
⊢ f b * f a < f c * f a
Module: Mathlib.Algebra.Order.Nonneg.Lattice

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
⊢ (fun t ↦
        if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val '' t) ∈ Ici a then ⟨sSup (Subtype.val '' t), ⋯⟩
        else default)
      ∅ =
    ⊥

Tactic:
;

Goal state after:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrder α
a : α
⊢ (fun t ↦
        if ht : t.Nonempty ∧ BddAbove t ∧ sSup (Subtype.val '' t) ∈ Ici a then ⟨sSup (Subtype.val '' t), ⋯⟩
        else default)
      ∅ =
    ⊥
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ IsLUB ∅ ⟨a, ⋯⟩

Tactic:
;

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ IsLUB ∅ ⟨a, ⋯⟩
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ ⟨a, ⋯⟩ = ⊥

Tactic:
;

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ ⟨a, ⋯⟩ = ⊥
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ IsGLB ∅ ⟨b, ⋯⟩

Tactic:
;

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ IsGLB ∅ ⟨b, ⋯⟩
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ ⟨b, ⋯⟩ = ⊤

Tactic:
;

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
s : Set α
inst✝¹ : ConditionallyCompleteLattice α
a b : α
inst✝ : Fact (a ≤ b)
⊢ ⟨b, ⋯⟩ = ⊤
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ sSup (Subtype.val '' range fun i ↦ f i) = ⨆ i, ↑(f i)

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ sSup (Subtype.val '' range fun i ↦ f i) = ⨆ i, ↑(f i)
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i ↦ f i) = range fun i ↦ ↑(f i)

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i ↦ f i) = range fun i ↦ ↑(f i)
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i ↦ f i) ↔ x✝ ∈ range fun i ↦ ↑(f i)

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
x✝ : α
⊢ (x✝ ∈ Subtype.val '' range fun i ↦ f i) ↔ x✝ ∈ range fun i ↦ ↑(f i)
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ a ⊓ sInf (Subtype.val '' range fun i ↦ f i) = a ⊓ ⨅ i, ↑(f i)

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ a ⊓ sInf (Subtype.val '' range fun i ↦ f i) = a ⊓ ⨅ i, ↑(f i)
Module: Mathlib.Order.CompleteLatticeIntervals

Goal state before:
pp: case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i ↦ f i) = range fun i ↦ ↑(f i)

Tactic:
;

Goal state after:
case e_a
ι : Sort u_1
α : Type u_2
inst✝ : CompleteLattice α
a : α
f : ι → ↑(Iic a)
⊢ (Subtype.val '' range fun i ↦ f i) = range fun i ↦ ↑(f i)