awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_2
inst : SemilatticeSup P
inst_1 : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
s : Finset ι
empty : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s → (s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t) → ((Insert.insert a s).sup f ∈ t ↔ ∀ i ∈ Insert.insert a s, f i ∈ t)
⊢ s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t

Tactic:
induction s using Finset.induction_on
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_2
inst : SemilatticeSup P
inst_1 : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
⊢ Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t

Tactic:
simp [*]
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_2
inst : SemilatticeSup P
inst_1 : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
a : ι
s : Finset ι
h : a ∉ s
h_1 : s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t
⊢ (insert a s).sup f ∈ t ↔ ∀ i ∈ insert a s, f i ∈ t

Tactic:
simp [*]
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_2
inst : SemilatticeSup P
inst_1 : OrderBot P
t : Ideal P
ι : Type u_3
f : ι → P
s : Finset ι
empty : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
insert :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s → (s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t) → ((Insert.insert a s).sup f ∈ t ↔ ∀ i ∈ Insert.insert a s, f i ∈ t)
empty₁ : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
insert₁ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s → (s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t) → ((Insert.insert a s).sup f ∈ t ↔ ∀ i ∈ Insert.insert a s, f i ∈ t)
empty₂ : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
insert₂ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s → (s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t) → ((Insert.insert a s).sup f ∈ t ↔ ∀ i ∈ Insert.insert a s, f i ∈ t)
empty₃ : Finset.sup ∅ f ∈ t ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ∈ t
insert₃ :
  ∀ (a : ι) (s : Finset ι),
    a ∉ s → (s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t) → ((Insert.insert a s).sup f ∈ t ↔ ∀ i ∈ Insert.insert a s, f i ∈ t)
⊢ s.sup f ∈ t ↔ ∀ i ∈ s, f i ∈ t

Tactic:
classical
  induction s using Finset.induction_on <;> simp [*]
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
x_1 : P
I_1 J_1 s t I J : Ideal P
x : P
hx : x ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
y : P
hy : y ∈ (I.toLowerSet ⊓ J.toLowerSet).carrier
⊢ (fun (x1 x2 : P) ↦ x1 ≤ x2) x (x ⊔ y) ∧ (fun (x1 x2 : P) ↦ x1 ≤ x2) y (x ⊔ y)

Tactic:
simp
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
x : P
I_1 J_1 s t I J : Ideal P
obtain :
  ∀ (w : P) (h : w ∈ (↑I : Set P) ∩ (↑J : Set P)), Set.Nonempty.{u_1} (α := P) {x : P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}
⊢ Set.Nonempty.{u_1} (α := P) {x : P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}

Tactic:
obtain ⟨w, h⟩ := inter_nonempty I J

Premises used: Order.Ideal.inter_nonempty
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
x : P
I_1 J_1 s t I J : Ideal P
w : P
h : w ∈ (↑I : Set P) ∩ (↑J : Set P)
⊢ Set.Nonempty.{u_1} (α := P) {x : P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}

Tactic:
⟨w, w, h.1, w, h.2, le_sup_left⟩

Premises used: le_sup_left, Set.Nonempty, And.right, And.left, And.intro, Exists.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
x : P
I_1 J_1 s t I J : Ideal P
w : P
h : w ∈ (↑I : Set P) ∩ (↑J : Set P)
⊢ Set.Nonempty.{u_1} (α := P) {x : P | ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j}

Tactic:
exact ⟨w, w, h.1, w, h.2, le_sup_left⟩
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
s t : Ideal P
⊢ (↑(s ⊔ t) : Set P) = {x : P | ∃ a ∈ s, ∃ b ∈ t, x ≤ a ⊔ b}

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
s t : Ideal P
⊢ (↑(s ⊓ t) : Set P) = (↑s : Set P) ∩ (↑t : Set P)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.inter, rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
x : P
I J : Ideal P
⊢ x ∈ I ⊓ J ↔ x ∈ I ∧ x ∈ J

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
x : P
I J : Ideal P
⊢ x ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, x ≤ i ⊔ j

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : IsCodirectedOrder P
x : P
I : Ideal P
hx : x ∉ I
h : I = I ⊔ principal x
⊢ x ∈ I

Tactic:
simpa only [left_eq_sup, principal_le_iff] using h

Premises used: Order.Ideal.principal_le_iff, left_eq_sup
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
rw : ∀ (i : Ideal P) (j : i ∈ S), ⊥ ∈ (↑i.toLowerSet : Set P)
⊢ Membership.mem (γ := Set P) (LowerSet.carrier (⨅ s ∈ S, s.toLowerSet)) ⊥

Tactic:
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂]

Premises used: Set.mem_iInter₂, LowerSet.coe_iInf₂, LowerSet.carrier_eq_coe
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
⊢ ∀ (i : Ideal P) (j : i ∈ S), ⊥ ∈ (↑i.toLowerSet : Set P)

Tactic:
fun s _ ↦ s.bot_mem

Premises used: Set.Mem, Order.Ideal.bot_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
⊢ ∀ (i : Ideal P) (j : i ∈ S), ⊥ ∈ (↑i.toLowerSet : Set P)

Tactic:
exact fun s _ ↦ s.bot_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : Membership.mem (γ := Set P) (LowerSet.carrier (⨅ s ∈ S, s.toLowerSet)) a
b : P
hb : Membership.mem (γ := Set P) (LowerSet.carrier (⨅ s ∈ S, s.toLowerSet)) b
rw :
  ∀ (ha : ∀ (i : Ideal P) (j : i ∈ S), a ∈ (↑i.toLowerSet : Set P)) (b : P)
    (hb : ∀ (i : Ideal P) (j : i ∈ S), b ∈ (↑i.toLowerSet : Set P)) (i : Ideal P) (j : i ∈ S),
    a ⊔ b ∈ (↑i.toLowerSet : Set P)
⊢ Membership.mem (γ := Set P) (LowerSet.carrier (⨅ s ∈ S, s.toLowerSet)) (a ⊔ b)

Tactic:
rw [LowerSet.carrier_eq_coe, LowerSet.coe_iInf₂, Set.mem_iInter₂] at ha hb ⊢

Premises used: Set.mem_iInter₂, LowerSet.coe_iInf₂, LowerSet.carrier_eq_coe
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : ∀ (i : Ideal P) (j : i ∈ S), a ∈ (↑i.toLowerSet : Set P)
b : P
hb : ∀ (i : Ideal P) (j : i ∈ S), b ∈ (↑i.toLowerSet : Set P)
⊢ ∀ (i : Ideal P) (j : i ∈ S), a ⊔ b ∈ (↑i.toLowerSet : Set P)

Tactic:
fun s hs ↦ sup_mem (ha _ hs) (hb _ hs)

Premises used: Set.Mem, Order.Ideal.sup_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
a : P
ha : ∀ (i : Ideal P) (j : i ∈ S), a ∈ (↑i.toLowerSet : Set P)
b : P
hb : ∀ (i : Ideal P) (j : i ∈ S), b ∈ (↑i.toLowerSet : Set P)
⊢ ∀ (i : Ideal P) (j : i ∈ S), a ⊔ b ∈ (↑i.toLowerSet : Set P)

Tactic:
exact fun s hs ↦ sup_mem (ha _ hs) (hb _ hs)

Premises used: Order.Ideal.sup_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
S : Set (Ideal P)
⊢ (↑(sInf S) : Set P) = ⋂ s ∈ S, (↑s : Set P)

Tactic:
LowerSet.coe_iInf₂ _

Premises used: LowerSet.coe_iInf₂
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S : Set (Ideal P)
simp_rw : x ∈ (↑(sInf S) : Set P) ↔ ∀ s ∈ S, x ∈ (↑s : Set P)
simp_rw₁ : Membership.mem (γ := Set P) (⋂ s ∈ S, (↑s : Set P)) x ↔ ∀ s ∈ S, x ∈ (↑s : Set P)
⊢ x ∈ sInf S ↔ ∀ s ∈ S, x ∈ s

Tactic:
simp_rw [← SetLike.mem_coe, coe_sInf, mem_iInter₂]

Premises used: Set.mem_iInter₂, SetLike.mem_coe, Order.Ideal.coe_sInf
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
s : Ideal P
hs : s ∈ lowerBounds S
rwa : (↑s : Set P) ⊆ (↑(sInf S) : Set P)
rwa₁ : (↑s : Set P) ⊆ ⋂ s ∈ S, (↑s : Set P)
rwa₂ rwa₃ rwa₄ rwa₅ : ∀ (i : Ideal P) (j : i ∈ S), (↑s : Set P) ⊆ (↑i : Set P)
⊢ s ≤ sInf S

Tactic:
rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]

Premises used: Set.subset_iInter₂_iff, Order.Ideal.coe_subset_coe, Order.Ideal.coe_sInf
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
refine : ∀ (s : Ideal P) (hs : s ∈ S), sInf S ≤ s
⊢ IsGLB S (sInf S)

Tactic:
refine ⟨fun s hs ↦ ?_, fun s hs ↦ by rwa [← coe_subset_coe, coe_sInf, subset_iInter₂_iff]⟩
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
rw : ⋂ s ∈ S, (↑s : Set P) ⊆ (↑s : Set P)
⊢ sInf S ≤ s

Tactic:
rw [← coe_subset_coe, coe_sInf]

Premises used: Order.Ideal.coe_subset_coe, Order.Ideal.coe_sInf
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
⊢ ⋂ s ∈ S, (↑s : Set P) ⊆ (↑s : Set P)

Tactic:
biInter_subset_of_mem hs

Premises used: Set.biInter_subset_of_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
inst_1 : OrderBot P
x : P
S_1 S : Set (Ideal P)
s : Ideal P
hs : s ∈ S
⊢ ⋂ s ∈ S, (↑s : Set P) ⊆ (↑s : Set P)

Tactic:
exact biInter_subset_of_mem hs

Premises used: Set.biInter_subset_of_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'

Tactic:
⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, ?_⟩

Premises used: Order.Ideal.lower, inf_le_right, And.intro, Exists.intro, Min.min
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
refine : x = x ⊓ i ⊔ x ⊓ j
⊢ ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'

Tactic:
refine ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, ?_⟩
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ (i ⊔ j)

Tactic:
left_eq_inf.mpr hx

Premises used: Iff.mpr, left_eq_inf
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x ⊓ (i ⊔ j) = x ⊓ i ⊔ x ⊓ j

Tactic:
inf_sup_left _ _ _

Premises used: inf_sup_left
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ i ⊔ x ⊓ j

Tactic:
calc
    x = x ⊓ (i ⊔ j) := left_eq_inf.mpr hx
    _ = x ⊓ i ⊔ x ⊓ j := inf_sup_left _ _ _

Premises used: Iff.mpr, inf_sup_left, Max.max, left_eq_inf
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : DistribLattice P
I J : Ideal P
⊢ (↑(I ⊔ J) : Set P) = {x : P | ∃ i ∈ I, ∃ j ∈ J, x = i ⊔ j}

Tactic:
Set.ext fun _ ↦
    ⟨fun ⟨_, _, _, _, _⟩ ↦ eq_sup_of_le_sup ‹_› ‹_› ‹_›, fun ⟨i, _, j, _, _⟩ ↦
      ⟨i, ‹_›, j, ‹_›, le_of_eq ‹_›⟩⟩

Premises used: Set.ext, setOf, Membership.mem, Exists, Order.Ideal.eq_sup_of_le_sup, And, SetLike.coe, Max.max, And.intro, Iff.intro, Exists.intro, _private.0.Order.Ideal.coe_sup_eq.match_1, le_of_eq, Eq, _private.0.Order.Ideal.coe_sup_eq.match_2
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
apply : ⊤ ∈ I
⊢ False

Tactic:
apply hI.top_notMem

Premises used: Order.Ideal.IsProper.top_notMem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
⊢ x ⊔ xᶜ ∈ I

Tactic:
have ht : x ⊔ xᶜ ∈ I := sup_mem ‹_› ‹_›
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
hxc : xᶜ ∈ I
hx : x ∈ I
ht : x ⊔ xᶜ ∈ I
rwa rwa₁ rwa₂ rwa₃ : ∀ (ht : ⊤ ∈ I), ⊤ ∈ I
⊢ ⊤ ∈ I

Tactic:
rwa [sup_compl_eq_top] at ht

Premises used: sup_compl_eq_top
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
⊢ xᶜ ∈ I → x ∉ I

Tactic:
have h : xᶜ ∈ I → x ∉ I := hI.notMem_of_compl_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
h : xᶜ ∈ I → x ∉ I
inl : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
inr : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
inl₁ : ∀ (h : xᶜ ∉ I), x ∉ I ∨ xᶜ ∉ I
inr₁ : ∀ (h : x ∉ I), x ∉ I ∨ xᶜ ∉ I
inl₂ : ∀ (h : xᶜ ∉ I), ¬x ∉ I → xᶜ ∉ I
inr₂ : ∀ (h : x ∉ I), ¬x ∉ I → xᶜ ∉ I
inr₃ : ∀ (h : x ∉ I), x ∈ I → xᶜ ∈ I → False
⊢ x ∉ I ∨ xᶜ ∉ I

Tactic:
tauto
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
⊢ ⨆ (i : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ i), f i ∈ I ↔ ∀ (i : α), Membership.mem (γ := Set α) ∅ i → f i ∈ I

Tactic:
simp [↓iSup_insert, sup_mem_iff, *]

Premises used: iSup_insert, Order.Ideal.sup_mem_iff
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
a : α
s_1 : Set α
h : a ∉ s_1
hs : s_1.Finite
h_1 : ⨆ i ∈ s_1, f i ∈ I ↔ ∀ i ∈ s_1, f i ∈ I
⊢ ⨆ i ∈ insert a s_1, f i ∈ I ↔ ∀ i ∈ insert a s_1, f i ∈ I

Tactic:
simp [↓iSup_insert, sup_mem_iff, *]

Premises used: iSup_insert, Order.Ideal.sup_mem_iff
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Set α
hs : s.Finite
empty :
  ⨆ (i : α), ⨆ (_ : Membership.mem (γ := Set α) ∅ i), f i ∈ I ↔ ∀ (i : α), Membership.mem (γ := Set α) ∅ i → f i ∈ I
insert :
  ∀ {a : α} {s : Set α},
    a ∉ s →
      s.Finite →
        (⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I) → (⨆ i ∈ Insert.insert a s, f i ∈ I ↔ ∀ i ∈ Insert.insert a s, f i ∈ I)
⊢ ⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I

Tactic:
induction s, hs using Finite.induction_on with simp [↓iSup_insert, sup_mem_iff, *]

Premises used: iSup_insert, Order.Ideal.sup_mem_iff
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : CompleteLattice P
I : Ideal P
α : Type u_2
f : α → P
s : Finset α
⊢ ⨆ i ∈ s, f i ∈ I ↔ ∀ i ∈ s, f i ∈ I

Tactic:
biSup_mem_iff s.finite_toSet

Premises used: Set.Mem, Finset.finite_toSet, Order.Ideal.biSup_mem_iff
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : CompleteLattice P
I : Ideal P
α : Sort u_2
inst_1 : Finite α
f : α → P
⊢ ⨆ (i : α), f i ∈ I ↔ ∀ (i : α), f i ∈ I

Tactic:
simpa [← Equiv.plift.symm.iSup_comp, Equiv.plift.forall_congr_left]
    using biSup_mem_iff (f := f ∘ PLift.down) Set.finite_univ

Premises used: Equiv.forall_congr_left, Equiv.iSup_comp, Set.finite_univ, Equiv.plift, Order.Ideal.biSup_mem_iff, Equiv.symm
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
D : Cofinal P
x : P
⊢ D.above x ∈ D

Tactic:
(Classical.choose_spec <| D.isCofinal x).1

Premises used: Set.Mem, Classical.choose_spec, And.left, Order.Cofinal.above, Order.Cofinal.isCofinal
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
D : Cofinal P
x : P
⊢ x ≤ D.above x

Tactic:
(Classical.choose_spec <| D.isCofinal x).2

Premises used: Classical.choose_spec, And.right, Order.Cofinal.above, Order.Cofinal.isCofinal
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
hf : ∀ (n : ℕ), sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)
⊢ Monotone (sequenceOfCofinals p 𝒟)

Tactic:
apply monotone_nat_of_le_succ

Premises used: monotone_nat_of_le_succ
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
hf :
  sequenceOfCofinals p 𝒟 n ≤
    match (motive := Option ι → P) Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)
⊢ sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 (n + 1)

Tactic:
dsimp only [sequenceOfCofinals, Nat.add]

Premises used: Nat.add, Order.sequenceOfCofinals
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
hf : sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 n
hf₁ :
  ∀ (val : ι),
    sequenceOfCofinals p 𝒟 n ≤
      match (motive := Option ι → P) some val with
      | none => sequenceOfCofinals p 𝒟 n
      | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)
⊢ sequenceOfCofinals p 𝒟 n ≤
    match (motive := Option ι → P) Encodable.decode n with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Tactic:
cases (Encodable.decode n : Option ι)

Premises used: Encodable.decode
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
⊢ sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 n

Tactic:
rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
n : ℕ
val : ι
⊢ sequenceOfCofinals p 𝒟 n ≤
    match (motive := Option ι → P) some val with
    | none => sequenceOfCofinals p 𝒟 n
    | some i => (𝒟 i).above (sequenceOfCofinals p 𝒟 n)

Tactic:
apply Cofinal.le_above

Premises used: Order.Cofinal.le_above
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
i : ι
dsimp :
  Membership.mem (α := P) (𝒟 i)
    (match (motive := Option ι → P) Encodable.decode (Encodable.encode i) with
      | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
      | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i)) :
      P)
⊢ sequenceOfCofinals p 𝒟 (Encodable.encode i + 1) ∈ 𝒟 i

Tactic:
dsimp only [sequenceOfCofinals, Nat.add]

Premises used: Nat.add, Order.sequenceOfCofinals
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
i : ι
rw :
  Membership.mem (α := P) (𝒟 i)
    (match (motive := Option ι → P) some i with
      | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
      | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i)) :
      P)
⊢ Membership.mem (α := P) (𝒟 i)
    (match (motive := Option ι → P) Encodable.decode (Encodable.encode i) with
      | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
      | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i)) :
      P)

Tactic:
rw [Encodable.encodek]

Premises used: Encodable.encodek
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ Membership.mem (α := P) (𝒟 i)
    (match (motive := Option ι → P) some i with
      | none => sequenceOfCofinals p 𝒟 (Encodable.encode i)
      | some i_1 => (𝒟 i_1).above (sequenceOfCofinals p 𝒟 (Encodable.encode i)) :
      P)

Tactic:
apply Cofinal.above_mem

Premises used: Order.Cofinal.above_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
⊢ p ∈ idealOfCofinals p 𝒟

Tactic:
⟨0, le_rfl⟩

Premises used: le_rfl, Set.Mem, setOf, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
p : P
ι : Type u_2
inst_1 : Encodable ι
𝒟 : ι → Cofinal P
i : ι
⊢ ∃ x ∈ 𝒟 i, x ∈ idealOfCofinals p 𝒟

Tactic:
⟨_, sequenceOfCofinals.encode_mem p 𝒟 i, _, le_rfl⟩

Premises used: le_rfl, And.intro, Exists.intro, Order.sequenceOfCofinals.encode_mem
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun (x1 x2 : Set P) ↦ x1 ⊆ x2) C
hNe : C.Nonempty
⊢ IsIdeal (⋃₀ C)

Tactic:
⟨isLowerSet_sUnion (fun I hI ↦ (hidl I hI).1), Set.nonempty_sUnion.2 ?_,
    directedOn_sUnion hD (fun J hJ => (hidl J hJ).3)⟩

Premises used: Order.IsIdeal.IsLowerSet, Order.IsIdeal.mk, Iff.mpr, Order.IsIdeal.Directed, Set.directedOn_sUnion, Set.nonempty_sUnion, isLowerSet_sUnion
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun (x1 x2 : Set P) ↦ x1 ⊆ x2) C
hNe : C.Nonempty
refine : ∃ s ∈ C, s.Nonempty
⊢ IsIdeal (⋃₀ C)

Tactic:
refine ⟨isLowerSet_sUnion (fun I hI ↦ (hidl I hI).1), Set.nonempty_sUnion.2 ?_,
    directedOn_sUnion hD (fun J hJ => (hidl J hJ).3)⟩
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun (x1 x2 : Set P) ↦ x1 ⊆ x2) C
hNe : C.Nonempty
let : ∀ (I : Set P) (hI : I ∈ C), ∃ s ∈ C, s.Nonempty
⊢ ∃ s ∈ C, s.Nonempty

Tactic:
let ⟨I, hI⟩ := hNe
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun (x1 x2 : Set P) ↦ x1 ⊆ x2) C
hNe : C.Nonempty
I : Set P
hI : I ∈ C
⊢ ∃ s ∈ C, s.Nonempty

Tactic:
⟨I, ⟨hI, (hidl I hI).2⟩⟩

Premises used: Order.IsIdeal.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hD : DirectedOn (fun (x1 x2 : Set P) ↦ x1 ⊆ x2) C
hNe : C.Nonempty
I : Set P
hI : I ∈ C
⊢ ∃ s ∈ C, s.Nonempty

Tactic:
exact ⟨I, ⟨hI, (hidl I hI).2⟩⟩
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
C : Set (Set P)
hidl : ∀ I ∈ C, IsIdeal I
hC : IsChain (fun (x1 x2 : Set P) ↦ x1 ⊆ x2) C
hNe : C.Nonempty
⊢ IsIdeal (⋃₀ C)

Tactic:
isIdeal_sUnion_of_directedOn hidl hC.directedOn hNe

Premises used: IsChain.directedOn, Order.isIdeal_sUnion_of_directedOn
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
h :
  ∀ (c : Set (Ideal P)),
    IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ (x : Ideal P), x ≠ ⊤ ∧ x ∈ upperBounds c
⊢ IsCoatomic.{u_1} (Ideal P)

Tactic:
apply IsCoatomic.of_isChain_bounded

Premises used: IsCoatomic.of_isChain_bounded
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∃ (x : Ideal P), x ≠ ⊤ ∧ x ∈ upperBounds S

Tactic:
⟨IsIdeal.toIdeal <| isIdeal_sUnion_of_isChain (C := SetLike.coe '' S) ?_
    (hS₁.image_of_map_rel _ _ _ ?_) (hS₂.image _), ?_, ?_⟩

Premises used: IsChain.image_of_map_rel, Set.Nonempty.image, And.intro, Exists.intro, Order.isIdeal_sUnion_of_isChain, Order.IsIdeal.toIdeal
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
h : ∀ I ∈ SetLike.coe '' S, IsIdeal I
h₁ : ∀ (x y : Ideal P), x ≤ y → (↑x : Set P) ⊆ (↑y : Set P)
h₂ : Ne (α := Ideal P) (IsIdeal.toIdeal (I := ⋃₀ (SetLike.coe '' S)) ⋯) ⊤
h₃ : IsIdeal.toIdeal (I := ⋃₀ (SetLike.coe '' S)) ⋯ ∈ upperBounds S
⊢ ∃ (x : Ideal P), x ≠ ⊤ ∧ x ∈ upperBounds S

Tactic:
refine ⟨IsIdeal.toIdeal <| isIdeal_sUnion_of_isChain (C := SetLike.coe '' S) ?_
    (hS₁.image_of_map_rel _ _ _ ?_) (hS₂.image _), ?_, ?_⟩
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ I ∈ SetLike.coe '' S, IsIdeal I

Tactic:
simp [Ideal.isIdeal]

Premises used: Order.Ideal.isIdeal
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ ∀ (x y : Ideal P), x ≤ y → (↑x : Set P) ⊆ (↑y : Set P)

Tactic:
simp
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
⊢ Ne (α := Ideal P) (IsIdeal.toIdeal (I := ⋃₀ (SetLike.coe '' S)) ⋯) ⊤

Tactic:
simpa [top_notMem_iff, lt_top_iff_ne_top, ← top_mem_iff_eq_top] using hS₃

Premises used: Order.Ideal.top_mem_iff_eq_top, lt_top_iff_ne_top, top_notMem_iff
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
S : Set (Ideal P)
hS₁ : IsChain (fun (x1 x2 : Ideal P) ↦ x1 ≤ x2) S
hS₂ : S.Nonempty
hS₃ : ⊤ ∉ S
J : Ideal P
hJ : J ∈ S
⊢ J ≤ IsIdeal.toIdeal (I := ⋃₀ (SetLike.coe '' S)) ⋯

Tactic:
simpa [le_toIdeal] using Set.subset_biUnion_of_mem hJ

Premises used: Order.Ideal.le_toIdeal, Set.subset_biUnion_of_mem