awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
⊢ ¬Disjoint (↑F : Set α) (↑J₁ : Set α)

Tactic:
have J₁F : ¬ (Disjoint (F : Set α) J₁) := by
    intro hdis
    apply J₁S
    simp only [le_eq_subset, mem_setOf_eq, SetLike.coe_subset_coe, S]
    exact ⟨J₁.isIdeal, le_trans IJ' le_sup_left, hdis⟩
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
hdis : Disjoint (↑F : Set α) (↑J₂ : Set α)
apply : (↑J₂ : Set α) ∈ S
⊢ False

Tactic:
apply J₂S
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
hdis : Disjoint (↑F : Set α) (↑J₂ : Set α)
simp : IsIdeal (↑J₂ : Set α) ∧ I ≤ J₂ ∧ Disjoint (↑F : Set α) (↑J₂ : Set α)
⊢ (↑J₂ : Set α) ∈ S

Tactic:
simp only [le_eq_subset, mem_setOf_eq, SetLike.coe_subset_coe, S]

Premises used: Set.le_eq_subset, Set.mem_setOf_eq, SetLike.coe_subset_coe
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
hdis : Disjoint (↑F : Set α) (↑J₂ : Set α)
⊢ IsIdeal (↑J₂ : Set α) ∧ I ≤ J₂ ∧ Disjoint (↑F : Set α) (↑J₂ : Set α)

Tactic:
⟨J₂.isIdeal, le_trans IJ' le_sup_left, hdis⟩

Premises used: le_sup_left, And.intro, Order.Ideal.isIdeal, le_trans
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
hdis : Disjoint (↑F : Set α) (↑J₂ : Set α)
⊢ IsIdeal (↑J₂ : Set α) ∧ I ≤ J₂ ∧ Disjoint (↑F : Set α) (↑J₂ : Set α)

Tactic:
exact ⟨J₂.isIdeal, le_trans IJ' le_sup_left, hdis⟩
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
⊢ ¬Disjoint (↑F : Set α) (↑J₂ : Set α)

Tactic:
have J₂F : ¬ (Disjoint (F : Set α) J₂) := by
    intro hdis
    apply J₂S
    simp only [le_eq_subset, mem_setOf_eq, SetLike.coe_subset_coe, S]
    exact ⟨J₂.isIdeal, le_trans IJ' le_sup_left, hdis⟩
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
h : ∀ (c₁ : α) (c₁F : c₁ ∈ (↑F : Set α)) (c₁J₁ : c₁ ∈ (↑J₁ : Set α)), a₁ ⊓ a₂ ∉ J
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
let ⟨c₁, ⟨c₁F, c₁J₁⟩⟩ := Set.not_disjoint_iff.1 J₁F
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
h : ∀ (c₂ : α) (c₂F : c₂ ∈ (↑F : Set α)) (c₂J₂ : c₂ ∈ (↑J₂ : Set α)), a₁ ⊓ a₂ ∉ J
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
let ⟨c₂, ⟨c₂F, c₂J₂⟩⟩ := Set.not_disjoint_iff.1 J₂F
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
h : ∀ (b₁ : α) (b₁J : b₁ ∈ J) (cba₁ : c₁ ≤ b₁ ⊔ a₁), a₁ ⊓ a₂ ∉ J
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
let ⟨b₁, ⟨b₁J, cba₁⟩⟩ := (mem_ideal_sup_principal a₁ c₁ J).1 c₁J₁
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
h : ∀ (b₂ : α) (b₂J : b₂ ∈ J) (cba₂ : c₂ ≤ b₂ ⊔ a₂), a₁ ⊓ a₂ ∉ J
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
let ⟨b₂, ⟨b₂J, cba₂⟩⟩ := (mem_ideal_sup_principal a₂ c₂ J).1 c₂J₂
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
⊢ b ∈ J

Tactic:
have bJ : b ∈ J := sup_mem b₁J b₂J
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
h₁ : b₁ ≤ b
h₂ : b₂ ≤ b
⊢ (b₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂)

Tactic:
gcongr
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
⊢ b₁ ≤ b

Tactic:
le_sup_left

Premises used: le_sup_left
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
⊢ b₂ ≤ b

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
⊢ b₁ ≤ b

Tactic:
exacts [le_sup_left, le_sup_right]

Premises used: le_sup_left, le_sup_right
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
⊢ c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂

Tactic:
have ineq : c₁ ⊓ c₂ ≤ b ⊔ (a₁ ⊓ a₂) :=
  calc
    c₁ ⊓ c₂ ≤ (b₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) := inf_le_inf cba₁ cba₂
    _       ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂) := by gcongr; exacts [le_sup_left, le_sup_right]
    _       = b ⊔ (a₁ ⊓ a₂) := (sup_inf_left b a₁ a₂).symm
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
⊢ b ⊔ a₁ ⊓ a₂ ∈ F

Tactic:
have ba₁a₂F : b ⊔ (a₁ ⊓ a₂) ∈ F := PFilter.mem_of_le ineq (PFilter.inf_mem c₁F c₂F)
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
h : ∀ (ha₁a₂ : a₁ ⊓ a₂ ∈ J), ¬Disjoint (↑F : Set α) Jset
⊢ a₁ ⊓ a₂ ∉ J

Tactic:
contrapose JF with ha₁a₂
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
h : ∃ x ∈ (↑F : Set α), x ∈ Jset
⊢ ¬Disjoint (↑F : Set α) Jset

Tactic:
rw [Set.not_disjoint_iff]

Premises used: Set.not_disjoint_iff
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
h : b ⊔ a₁ ⊓ a₂ ∈ (↑F : Set α) ∧ b ⊔ a₁ ⊓ a₂ ∈ Jset
⊢ ∃ x ∈ (↑F : Set α), x ∈ Jset

Tactic:
use b ⊔ (a₁ ⊓ a₂)

Premises used: Min.min
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
⊢ b ⊔ a₁ ⊓ a₂ ∈ (↑F : Set α) ∧ b ⊔ a₁ ⊓ a₂ ∈ Jset

Tactic:
⟨ba₁a₂F, sup_mem bJ ha₁a₂⟩

Premises used: And.intro, Order.Ideal.sup_mem
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
F : PFilter α
I : Ideal α
hFI : Disjoint (↑F : Set α) (↑I : Set α)
S : Set (Set α) := {J : Set α | IsIdeal J ∧ (↑I : Set α) ≤ J ∧ Disjoint (↑F : Set α) J}
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := J ⊔ principal a₁
J₂ : Ideal α := J ⊔ principal a₂
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : (↑J₁ : Set α) ≠ Jset
J₂J : (↑J₂ : Set α) ≠ Jset
J₁S : (↑J₁ : Set α) ∉ S
J₂S : (↑J₂ : Set α) ∉ S
J₁F : ¬Disjoint (↑F : Set α) (↑J₁ : Set α)
J₂F : ¬Disjoint (↑F : Set α) (↑J₂ : Set α)
c₁ : α
c₁F : c₁ ∈ (↑F : Set α)
c₁J₁ : c₁ ∈ (↑J₁ : Set α)
c₂ : α
c₂F : c₂ ∈ (↑F : Set α)
c₂J₂ : c₂ ∈ (↑J₂ : Set α)
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := b₁ ⊔ b₂
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
⊢ b ⊔ a₁ ⊓ a₂ ∈ (↑F : Set α) ∧ b ⊔ a₁ ⊓ a₂ ∈ Jset

Tactic:
exact ⟨ba₁a₂F, sup_mem bJ ha₁a₂⟩
-- Module: Mathlib.Order.PropInstances
Goal:
⊢ ⊥ = False

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.PropInstances
Goal:
⊢ ⊤ = True

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.PropInstances
Goal:
p q : Prop
pos : ∀ (h : q), p ≤ q ∨ q ≤ p
neg : ∀ (h : ¬q), p ≤ q ∨ q ≤ p
⊢ p ≤ q ∨ q ≤ p

Tactic:
by_cases h : q