awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
h : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩

Premises used: And.right, And.left, And.intro, Or.inr
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
h : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
mb : b ∈ s ∪ t
inl : ∀ (h : b ∈ s), P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t
inr : ∀ (h : b ∈ t), P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
h : b ∈ s
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩

Premises used: And.right, And.left, And.intro, Or.inl
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
h : b ∈ s
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
h : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩

Premises used: And.right, And.left, And.intro, Or.inr
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
h : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
mb : b ∈ s ∪ t
inl : ∀ (h : b ∈ s), P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t
inr : ∀ (h : b ∈ t), P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
h : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
simp_all :
  ∀ (hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s)
    (ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ t),
    b ∈ s ∩ t → ∀ (bs : b ∈ s) (bt : b ∈ t) ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t

Tactic:
simp_all only [IsRelUpperSet, true_and]

Premises used: IsRelUpperSet, true_and
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
b : α
hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s
ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ t
h : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t

Tactic:
fun _ x y ↦ ⟨(hs bs).2 x y, (ht bt).2 x y⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
b : α
hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s
ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ t
h : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t

Tactic:
exact fun _ x y ↦ ⟨(hs bs).2 x y, (ht bt).2 x y⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
h : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
simp_all :
  ∀ (hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ s)
    (ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ t),
    b ∈ s ∩ t → ∀ (bs : b ∈ s) (bt : b ∈ t) ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∩ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∩ t

Tactic:
simp_all only [IsRelLowerSet, true_and]

Premises used: IsRelLowerSet, true_and
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
b : α
hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ s
ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ t
h : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∩ t

Tactic:
fun _ x y ↦ ⟨(hs bs).2 x y, (ht bt).2 x y⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
s t : Set α
P : α → Prop
inst : LE α
b : α
hs : ∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ s
ht : ∀ ⦃a : α⦄, a ∈ t → P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ t
h : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∩ t

Tactic:
exact fun _ x y ↦ ⟨(hs bs).2 x y, (ht bt).2 x y⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hS : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
⊢ IsRelUpperSet (⋃₀ S) P

Tactic:
fun _ ⟨s, ms, mb⟩ ↦
  ⟨(hS s ms mb).1, fun _ x y ↦ ⟨s, ms, (hS s ms mb).2 x y⟩⟩

Premises used: IsRelUpperSet, _private.0.IsRelUpperSet.sUnion.match_1, And, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hS : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
⊢ IsRelLowerSet (⋃₀ S) P

Tactic:
fun _ ⟨s, ms, mb⟩ ↦
  ⟨(hS s ms mb).1, fun _ x y ↦ ⟨s, ms, (hS s ms mb).2 x y⟩⟩

Premises used: IsRelLowerSet, _private.0.IsRelUpperSet.sUnion.match_1, And, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
P : α → Prop
inst : LE α
f : ι → Set α
hf : ∀ (i : ι), IsRelUpperSet (f i) P
⊢ IsRelUpperSet (⋃ (i : ι), f i) P

Tactic:
.sUnion (forall_mem_range.2 hf)

Premises used: Iff.mpr, Set.forall_mem_range, iSup, IsRelUpperSet.sUnion, Set.iUnion
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
P : α → Prop
inst : LE α
f : ι → Set α
hf : ∀ (i : ι), IsRelLowerSet (f i) P
⊢ IsRelLowerSet (⋃ (i : ι), f i) P

Tactic:
.sUnion (forall_mem_range.2 hf)

Premises used: Iff.mpr, Set.forall_mem_range, iSup, IsRelLowerSet.sUnion, Set.iUnion
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
P : α → Prop
inst : LE α
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsRelUpperSet (f i j) P
⊢ IsRelUpperSet (⋃ (i : ι), ⋃ (j : κ i), f i j) P

Tactic:
.iUnion fun i ↦ .iUnion (hf i)

Premises used: IsRelUpperSet.iUnion
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
P : α → Prop
inst : LE α
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsRelLowerSet (f i j) P
⊢ IsRelLowerSet (⋃ (i : ι), ⋃ (j : κ i), f i j) P

Tactic:
.iUnion fun i ↦ .iUnion (hf i)

Premises used: IsRelLowerSet.iUnion
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
b : α
mb : b ∈ ⋂₀ S
obtain : ∀ (s₀ : Set α) (ms₀ : s₀ ∈ S), P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
obtain ⟨s₀, ms₀⟩ := hS
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
b : α
mb : b ∈ ⋂₀ S
s₀ : Set α
ms₀ : s₀ ∈ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
⟨(hf s₀ ms₀ (mb s₀ ms₀)).1, fun _ x y s ms ↦ (hf s ms (mb s ms)).2 x y⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
b : α
mb : b ∈ ⋂₀ S
s₀ : Set α
ms₀ : s₀ ∈ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
refine ⟨(hf s₀ ms₀ (mb s₀ ms₀)).1, fun _ x y s ms ↦ (hf s ms (mb s ms)).2 x y⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
b : α
mb : b ∈ ⋂₀ S
obtain : ∀ (s₀ : Set α) (ms₀ : s₀ ∈ S), P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
obtain ⟨s₀, ms₀⟩ := hS
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
b : α
mb : b ∈ ⋂₀ S
s₀ : Set α
ms₀ : s₀ ∈ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
⟨(hf s₀ ms₀ (mb s₀ ms₀)).1, fun _ x y s ms ↦ (hf s ms (mb s ms)).2 x y⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
S : Set (Set α)
hf : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
b : α
mb : b ∈ ⋂₀ S
s₀ : Set α
ms₀ : s₀ ∈ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
refine ⟨(hf s₀ ms₀ (mb s₀ ms₀)).1, fun _ x y s ms ↦ (hf s ms (mb s ms)).2 x y⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
P : α → Prop
inst : LE α
inst_1 : Nonempty ι
f : ι → Set α
hf : ∀ (i : ι), IsRelUpperSet (f i) P
⊢ IsRelUpperSet (⋂ (i : ι), f i) P

Tactic:
.sInter (range_nonempty f) (forall_mem_range.2 hf)

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, IsRelUpperSet.sInter, Set.range_nonempty
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
P : α → Prop
inst : LE α
inst_1 : Nonempty ι
f : ι → Set α
hf : ∀ (i : ι), IsRelLowerSet (f i) P
⊢ IsRelLowerSet (⋂ (i : ι), f i) P

Tactic:
.sInter (range_nonempty f) (forall_mem_range.2 hf)

Premises used: Iff.mpr, iInf, Set.forall_mem_range, Set.iInter, IsRelLowerSet.sInter, Set.range_nonempty
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
P : α → Prop
inst : LE α
inst_1 : Nonempty ι
inst_2 : ∀ (i : ι), Nonempty.{u_3} (κ i)
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsRelUpperSet (f i j) P
⊢ IsRelUpperSet (⋂ (i : ι), ⋂ (j : κ i), f i j) P

Tactic:
.iInter fun i ↦ .iInter (hf i)

Premises used: IsRelUpperSet.iInter
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
P : α → Prop
inst : LE α
inst_1 : Nonempty ι
inst_2 : ∀ (i : ι), Nonempty.{u_3} (κ i)
f : (i : ι) → κ i → Set α
hf : ∀ (i : ι) (j : κ i), IsRelLowerSet (f i j) P
⊢ IsRelLowerSet (⋂ (i : ι), ⋂ (j : κ i), f i j) P

Tactic:
.iInter fun i ↦ .iInter (hf i)

Premises used: IsRelLowerSet.iInter
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
⊢ IsUpperSet s ↔ IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P

Tactic:
⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
refine_1 :
  ∀ (h : IsUpperSet s) (a : α) (x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s),
    P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
refine_2 :
  ∀ (h : IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P) (a b : { x : α // P x }) (x : a ≤ b) (y : a ∈ s),
    b ∈ s
⊢ IsUpperSet s ↔ IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P

Tactic:
refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsUpperSet s
a : α
x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
refine_1 :
  ∀ (a : { x : α // P x }) (ma : a ∈ s),
    P (↑a : α) ∧ ∀ ⦃b : α⦄, (↑a : α) ≤ b → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
⊢ P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
obtain ⟨a, ma, rfl⟩ := x

Premises used: rfl
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsUpperSet s
a : { x : α // P x }
ma : a ∈ s
b : α
x : (↑a : α) ≤ b
y : P b
⊢ a ≤ Subtype.mk (p := fun (x : α) ↦ P x) b y

Tactic:
x
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsUpperSet s
a : { x : α // P x }
ma : a ∈ s
b : α
x : (↑a : α) ≤ b
y : P b
⊢ a ≤ Subtype.mk (p := fun (x : α) ↦ P x) b y

Tactic:
exact x
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsUpperSet s
a : { x : α // P x }
ma : a ∈ s
b : α
x : (↑a : α) ≤ b
y : P b
⊢ b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
simpa [h (show a ≤ ⟨b, y⟩ by exact x) ma]
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsUpperSet s
a : { x : α // P x }
ma : a ∈ s
⊢ P (↑a : α) ∧ ∀ ⦃b : α⦄, (↑a : α) ≤ b → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
exact ⟨a.2, fun b x y ↦ by simpa [h (show a ≤ ⟨b, y⟩ by exact x) ma]⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
a b : { x : α // P x }
x : a ≤ b
y : a ∈ s
⊢ (↑a : α) ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
simp [a.2, y]

Premises used: Subtype.property
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
a b : { x : α // P x }
x : a ≤ b
y : a ∈ s
⊢ (↑a : α) ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
have ma : a.1 ∈ Subtype.val '' s := by simp [a.2, y]
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsRelUpperSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
a b : { x : α // P x }
x : a ≤ b
y : a ∈ s
ma : (↑a : α) ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
⊢ b ∈ s

Tactic:
simpa only [mem_image, Subtype.coe_inj, exists_eq_right] using (h ma).2 x b.2

Premises used: Subtype.coe_inj, Set.mem_image, exists_eq_right, And.right, Subtype.property
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
⊢ IsLowerSet s ↔ IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P

Tactic:
⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
refine_1 :
  ∀ (h : IsLowerSet s) (a : α) (x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s),
    P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
refine_2 :
  ∀ (h : IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P) (a b : { x : α // P x }) (x : b ≤ a) (y : a ∈ s),
    b ∈ s
⊢ IsLowerSet s ↔ IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P

Tactic:
refine ⟨fun h a x ↦ ?_, fun h a b x y ↦ ?_⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsLowerSet s
a : α
x : a ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
refine_1 :
  ∀ (a : { x : α // P x }) (ma : a ∈ s),
    P (↑a : α) ∧ ∀ ⦃b : α⦄, b ≤ (↑a : α) → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
⊢ P a ∧ ∀ ⦃b : α⦄, b ≤ a → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
obtain ⟨a, ma, rfl⟩ := x

Premises used: rfl
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsLowerSet s
a : { x : α // P x }
ma : a ∈ s
b : α
x : b ≤ (↑a : α)
y : P b
⊢ Subtype.mk (p := fun (x : α) ↦ P x) b y ≤ a

Tactic:
x
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsLowerSet s
a : { x : α // P x }
ma : a ∈ s
b : α
x : b ≤ (↑a : α)
y : P b
⊢ Subtype.mk (p := fun (x : α) ↦ P x) b y ≤ a

Tactic:
exact x
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsLowerSet s
a : { x : α // P x }
ma : a ∈ s
b : α
x : b ≤ (↑a : α)
y : P b
⊢ b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
simpa [h (show ⟨b, y⟩ ≤ a by exact x) ma]
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsLowerSet s
a : { x : α // P x }
ma : a ∈ s
⊢ P (↑a : α) ∧ ∀ ⦃b : α⦄, b ≤ (↑a : α) → P b → b ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
exact ⟨a.2, fun b x y ↦ by simpa [h (show ⟨b, y⟩ ≤ a by exact x) ma]⟩
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
a b : { x : α // P x }
x : b ≤ a
y : a ∈ s
⊢ (↑a : α) ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
simp [a.2, y]

Premises used: Subtype.property
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
a b : { x : α // P x }
x : b ≤ a
y : a ∈ s
⊢ (↑a : α) ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s

Tactic:
have ma : a.1 ∈ Subtype.val '' s := by simp [a.2, y]
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
s : Set { x : α // P x }
h : IsRelLowerSet (Subtype.val (p := fun (x : α) ↦ P x) '' s) P
a b : { x : α // P x }
x : b ≤ a
y : a ∈ s
ma : (↑a : α) ∈ Subtype.val (p := fun (x : α) ↦ P x) '' s
⊢ b ∈ s

Tactic:
simpa only [mem_image, Subtype.coe_inj, exists_eq_right] using (h ma).2 x b.2

Premises used: Subtype.coe_inj, Set.mem_image, exists_eq_right, And.right, Subtype.property
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s_1 t_1 : Set α
a b : α
P : α → Prop
inst : LE α
s t : RelUpperSet P
h : s.carrier (P := P) = t.carrier (P := P)
mk :
  ∀ (carrier : Set α) (isRelUpperSet' : IsRelUpperSet carrier P)
    (h : (RelUpperSet.mk (P := P) carrier isRelUpperSet').carrier (P := P) = t.carrier (P := P)),
    RelUpperSet.mk (P := P) carrier isRelUpperSet' = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t_1 : Set α
a b : α
P : α → Prop
inst : LE α
t : RelUpperSet P
carrier : Set α
isRelUpperSet' : IsRelUpperSet carrier P
h : (RelUpperSet.mk (P := P) carrier isRelUpperSet').carrier (P := P) = t.carrier (P := P)
mk :
  ∀ (carrier_1 : Set α) (isRelUpperSet'_1 : IsRelUpperSet carrier_1 P)
    (h :
      (RelUpperSet.mk (P := P) carrier isRelUpperSet').carrier (P := P) =
        (RelUpperSet.mk (P := P) carrier_1 isRelUpperSet'_1).carrier (P := P)),
    RelUpperSet.mk (P := P) carrier isRelUpperSet' = RelUpperSet.mk (P := P) carrier_1 isRelUpperSet'_1
⊢ RelUpperSet.mk (P := P) carrier isRelUpperSet' = t

Tactic:
cases t
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst : LE α
carrier : Set α
isRelUpperSet' : IsRelUpperSet carrier P
carrier_1 : Set α
isRelUpperSet'_1 : IsRelUpperSet carrier_1 P
h :
  (RelUpperSet.mk (P := P) carrier isRelUpperSet').carrier (P := P) =
    (RelUpperSet.mk (P := P) carrier_1 isRelUpperSet'_1).carrier (P := P)
⊢ RelUpperSet.mk (P := P) carrier isRelUpperSet' = RelUpperSet.mk (P := P) carrier_1 isRelUpperSet'_1

Tactic:
congr
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s_1 t_1 : Set α
a b : α
P : α → Prop
inst : LE α
s t : RelLowerSet P
h : s.carrier (P := P) = t.carrier (P := P)
mk :
  ∀ (carrier : Set α) (isRelLowerSet' : IsRelLowerSet carrier P)
    (h : (RelLowerSet.mk (P := P) carrier isRelLowerSet').carrier (P := P) = t.carrier (P := P)),
    RelLowerSet.mk (P := P) carrier isRelLowerSet' = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t_1 : Set α
a b : α
P : α → Prop
inst : LE α
t : RelLowerSet P
carrier : Set α
isRelLowerSet' : IsRelLowerSet carrier P
h : (RelLowerSet.mk (P := P) carrier isRelLowerSet').carrier (P := P) = t.carrier (P := P)
mk :
  ∀ (carrier_1 : Set α) (isRelLowerSet'_1 : IsRelLowerSet carrier_1 P)
    (h :
      (RelLowerSet.mk (P := P) carrier isRelLowerSet').carrier (P := P) =
        (RelLowerSet.mk (P := P) carrier_1 isRelLowerSet'_1).carrier (P := P)),
    RelLowerSet.mk (P := P) carrier isRelLowerSet' = RelLowerSet.mk (P := P) carrier_1 isRelLowerSet'_1
⊢ RelLowerSet.mk (P := P) carrier isRelLowerSet' = t

Tactic:
cases t
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst : LE α
carrier : Set α
isRelLowerSet' : IsRelLowerSet carrier P
carrier_1 : Set α
isRelLowerSet'_1 : IsRelLowerSet carrier_1 P
h :
  (RelLowerSet.mk (P := P) carrier isRelLowerSet').carrier (P := P) =
    (RelLowerSet.mk (P := P) carrier_1 isRelLowerSet'_1).carrier (P := P)
⊢ RelLowerSet.mk (P := P) carrier isRelLowerSet' = RelLowerSet.mk (P := P) carrier_1 isRelLowerSet'_1

Tactic:
congr
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
u : RelUpperSet P
⊢ IsRelUpperSet (↑u : Set α) P

Tactic:
u.isRelUpperSet'

Premises used: RelUpperSet.isRelUpperSet'
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
P : α → Prop
inst : LE α
l : RelLowerSet P
⊢ IsRelLowerSet (↑l : Set α) P

Tactic:
l.isRelLowerSet'

Premises used: RelLowerSet.isRelLowerSet'
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
a : α
inst : Preorder α
c x : α
b : x ∈ Icc a c
simp_all : ∀ (b : a ≤ x ∧ x ≤ c) ⦃b : α⦄, x ≤ b → b ≤ c → a ≤ b
⊢ (fun (x : α) ↦ x ≤ c) x ∧ ∀ ⦃b : α⦄, x ≤ b → (fun (x : α) ↦ x ≤ c) b → b ∈ Icc a c

Tactic:
simp_all only [mem_Icc, and_true, true_and]

Premises used: and_true, Set.mem_Icc, true_and
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
a : α
inst : Preorder α
c x : α
b : a ≤ x ∧ x ≤ c
⊢ ∀ ⦃b : α⦄, x ≤ b → b ≤ c → a ≤ b

Tactic:
fun _ x _ ↦ b.1.trans x

Premises used: And.left, LE.le.trans
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
a : α
inst : Preorder α
c x : α
b : a ≤ x ∧ x ≤ c
⊢ ∀ ⦃b : α⦄, x ≤ b → b ≤ c → a ≤ b

Tactic:
exact fun _ x _ ↦ b.1.trans x

Premises used: And.left, LE.le.trans
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
a : α
inst : Preorder α
c x : α
b : x ∈ Icc c a
simp_all : ∀ (b : c ≤ x ∧ x ≤ a) ⦃b : α⦄, b ≤ x → c ≤ b → b ≤ a
⊢ (fun (x : α) ↦ c ≤ x) x ∧ ∀ ⦃b : α⦄, b ≤ x → (fun (x : α) ↦ c ≤ x) b → b ∈ Icc c a

Tactic:
simp_all only [mem_Icc, true_and]

Premises used: Set.mem_Icc, true_and
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
a : α
inst : Preorder α
c x : α
b : c ≤ x ∧ x ≤ a
⊢ ∀ ⦃b : α⦄, b ≤ x → c ≤ b → b ≤ a

Tactic:
fun _ x _ ↦ x.trans b.2

Premises used: And.right, LE.le.trans
-- Module: Mathlib.Order.UpperLower.Relative
Goal:
α : Type u_1
a : α
inst : Preorder α
c x : α
b : c ≤ x ∧ x ≤ a
⊢ ∀ ⦃b : α⦄, b ≤ x → c ≤ b → b ≤ a

Tactic:
exact fun _ x _ ↦ x.trans b.2
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_1
a : α
r : α → α → Prop
h : ¬Acc r a
⊢ ¬∀ (b : α), r b a → Acc r b

Tactic:
rw [acc_def] at h

Premises used: acc_def
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_1
a : α
r : α → α → Prop
h : ¬∀ (b : α), r b a → Acc r b
⊢ ∃ (b : α), r b a ∧ ¬Acc r b

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.Order.WellFounded
Goal:
α : Sort u_1
a : α
r : α → α → Prop
h : ∃ (b : α), r b a ∧ ¬Acc r b
⊢ ∃ (b : α), ¬Acc r b ∧ r b a

Tactic:
simpa only [and_comm]

Premises used: and_comm