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

Goal state before:
pp: case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))

Tactic:
·

Goal state after:
case neg.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ ↑(sInf ((fun a ↦ ↑a) ⁻¹' s))
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty

pp: case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ b ∈ (fun a ↦ ↑a) ⁻¹' s, a ≤ b

Tactic:
·

Goal state after:
case neg.some.refine_1
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ((fun a ↦ ↑a) ⁻¹' s).Nonempty
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha✝ : Option.some a ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
ha : none ∈ s
⊢ none ∈ {⊤}

pp: case neg.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a✝ : β
ha✝ : Option.some a✝ ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
a : β
ha : Option.some a ∈ s
⊢ Option.some a ∈ {⊤}

Tactic:
·

Goal state after:
case neg.some.refine_1.none
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a : β
ha✝ : Option.some a ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
ha : none ∈ s
⊢ none ∈ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a✝ : β
ha✝ : Option.some a✝ ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
a : β
ha : Option.some a ∈ s
⊢ Option.some a ∈ {⊤}

Tactic:
·

Goal state after:
case neg.some.refine_1.some
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
a✝ : β
ha✝ : Option.some a✝ ∈ lowerBounds s
h : (fun a ↦ ↑a) ⁻¹' s = ∅
a : β
ha : Option.some a ∈ s
⊢ Option.some a ∈ {⊤}
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ b ∈ (fun a ↦ ↑a) ⁻¹' s, a ≤ b

Tactic:
·

Goal state after:
case neg.some.refine_2
β : Type u_5
inst✝ : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ ∀ b ∈ (fun a ↦ ↑a) ⁻¹' s, a ≤ b
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)

pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
·

Goal state after:
case pos
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : BddBelow s
⊢ IsGLB s (sInf s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)

Tactic:
·

Goal state after:
case neg
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
hs : ¬BddBelow s
⊢ IsGLB s (sInf s)
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

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

pp: case inr
α : 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
⊢ sInf (f '' s) = sInf (f '' t)

Tactic:
·

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

Goal state before:
pp: case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False

pp: case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False

Tactic:
·

Goal state after:
case left
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ≤ f a → b' ∈ lowerBounds (f '' Icc a b)

pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ≤ f a → b' ∈ lowerBounds (f '' Icc a b)
Module: Mathlib.Order.Interval.Set.LinearOrder

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False

Tactic:
·

Goal state after:
case right
α : Type u_1
inst✝¹ : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst✝ : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
b' : β
⊢ b' ∈ lowerBounds (f '' Icc a b) → b' ≤ f a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S = ∅
⊢ sSup S ≤ a

pp: case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S.Nonempty
⊢ sSup S ≤ a

Tactic:
·

Goal state after:
case inl
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S = ∅
⊢ sSup S ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S.Nonempty
⊢ sSup S ≤ a

Tactic:
·

Goal state after:
case inr
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
ha : a ∈ upperBounds S
h : S.Nonempty
⊢ sSup S ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : S ⊆ {⊤}
⊢ ⊤ ≤ a

pp: case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : ¬S ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ a

Tactic:
·

Goal state after:
case pos
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : S ⊆ {⊤}
⊢ ⊤ ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case pos.top
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ ⊤ ≤ ⊤

pp: case pos.coe
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ ⊤ ≤ ↑a✝

Tactic:
·

Goal state after:
case pos.top
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ ⊤ ≤ ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : ¬S ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ a

Tactic:
·

Goal state after:
case neg
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
a : WithTop (WithBot α)
haS : a ∈ S
h₁ : ¬S ⊆ {⊤}
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ a
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.top
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ ⊤

pp: case neg.coe
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ ↑a✝

Tactic:
·

Goal state after:
case neg.top
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
haS : ⊤ ∈ S
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ ⊤
Module: Mathlib.Order.ConditionallyCompleteLattice.Basic

Goal state before:
pp: case neg.coe
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ ↑a✝

Tactic:
·

Goal state after:
case neg.coe
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : Type u_5
inst✝ : ConditionallyCompleteLattice α
S : Set (WithTop (WithBot α))
h₁ : ¬S ⊆ {⊤}
a✝ : WithBot α
haS : ↑a✝ ∈ S
⊢ ↑(sInf ((fun a ↦ ↑a) ⁻¹' S)) ≤ ↑a✝
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₂

pp: case 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₁ b₂ : β
hne : b₁ ≠ b₂
hb₁ : ¬∃ a₁, e a₁ = b₁
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
·

Goal state after:
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₂
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: 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₂)

pp: 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₂

Tactic:
·

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₂)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: 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₂

Tactic:
·

Goal state after:
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.Data.Set.Pairwise.Basic

Goal state before:
pp: case 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₁ b₂ : β
hne : b₁ ≠ b₂
hb₁ : ¬∃ a₁, e a₁ = b₁
⊢ (Disjoint on extend e f ⊥) b₁ b₂

Tactic:
·

Goal state after:
case 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₁ b₂ : β
hne : b₁ ≠ b₂
hb₁ : ¬∃ a₁, e a₁ = b₁
⊢ (Disjoint on extend e f ⊥) b₁ b₂
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case mp
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z

pp: case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)

Tactic:
·

Goal state after:
case mp
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ s.Pairwise (r on f) → ∃ z, ∀ (x : ι), x ∈ s → r (f x) z
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case mp.inl
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
H : s.Pairwise (r on f)
x : ι
hx hy : x ∈ s
⊢ r (f x) (f x)

pp: case mp.inr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)

Tactic:
·

Goal state after:
case mp.inl
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
H : s.Pairwise (r on f)
x : ι
hx hy : x ∈ s
⊢ r (f x) (f x)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case mp.inr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)

Tactic:
·

Goal state after:
case mp.inr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
y : ι
hy : y ∈ s
H : s.Pairwise (r on f)
x : ι
hx : x ∈ s
hne : x ≠ y
⊢ r (f x) (f y)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)

Tactic:
·

Goal state after:
case mpr
α : Type u_1
ι : Type u_4
r : α → α → Prop
f : ι → α
inst✝ : IsEquiv α r
s : Set ι
hs : s.Nonempty
⊢ (∃ z, ∀ (x : ι), x ∈ s → r (f x) z) → s.Pairwise (r on f)
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ ∅.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ ∅ → r (f x) z

pp: case inr
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z

Tactic:
·

Goal state after:
case inl
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
⊢ ∅.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ ∅ → r (f x) z
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z

Tactic:
·

Goal state after:
case inr
α : Type u_1
ι : Type u_4
inst✝¹ : Nonempty ι
s : Set α
f : α → ι
r : ι → ι → Prop
inst✝ : IsEquiv ι r
hne : s.Nonempty
⊢ s.Pairwise (r on f) ↔ ∃ z, ∀ (x : α), x ∈ s → r (f x) z
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (Disjoint on fun a ↦ f a '' t) x y

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : s.PairwiseDisjoint fun a ↦ f a '' t
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]

pp: case mpr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ (∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f

Tactic:
·

Goal state after:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
⊢ Monotone f ∨ Antitone f → ∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (Disjoint on fun a ↦ f a '' t) x y

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (a : α), a ∈ s → Injective (f a)
hs : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
h : x ≠ y
⊢ (Disjoint on fun a ↦ f a '' t) x y
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b ↦ (fun a ↦ f a b) '' s) x y

Tactic:
·

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : t.PairwiseDisjoint fun b ↦ (fun a ↦ f a b) '' s
x : α × β
hx : x ∈ s ×ˢ t
y : α × β
hy : y ∈ s ×ˢ t
h : f x.1 x.2 = (fun p ↦ f p.1 p.2) y
⊢ x = y
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mpr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

pp: case mpr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
·

Goal state after:
case mpr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfab : f a < f b
hfcb : f c < f b
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
Module: Mathlib.Order.Interval.Set.UnorderedInterval

Goal state before:
pp: case mpr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]

Tactic:
·

Goal state after:
case mpr.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
a b c : α
hab : a ≤ b
hbc : b ≤ c
hfba : f b < f a
hfbc : f b < f c
⊢ ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b ↦ (fun a ↦ f a b) '' s) x y

Tactic:
·

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
s : Set α
t : Set β
hf : ∀ (b : β), b ∈ t → Injective fun a ↦ f a b
ht : InjOn (fun p ↦ f p.1 p.2) (s ×ˢ t)
x : β
hx : x ∈ t
y : β
hy : y ∈ t
h : x ≠ y
⊢ (Disjoint on fun b ↦ (fun a ↦ f a b) '' s) x y
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : i < j
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

pp: case inr
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
·

Goal state after:
case inl
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : i < j
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j
Module: Mathlib.Data.Set.Pairwise.Basic

Goal state before:
pp: case inr
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
·

Goal state after:
case inr
α : Type u_1
ι : Type u_4
s : Set ι
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬s.PairwiseDisjoint f
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hne : i ≠ j
x : α
hx₁ : x ∈ f i
hx₂ : x ∈ f j
h_lt : j < i
⊢ ∃ i, i ∈ s ∧ ∃ j, j ∈ s ∧ i < j ∧ ∃ x, x ∈ f i ∩ f j