awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x_1 : P
I : Ideal P
inst_1 : I.IsPrime
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ (↑J : Set P)
hyI : y ∉ (↑I : Set P)
suffices : x ⊓ y ⊔ x ⊓ yᶜ ∈ J
⊢ x ∈ (↑J : Set P)

Tactic:
suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J by rwa [sup_inf_inf_compl] at ass
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x_1 : P
I : Ideal P
inst_1 : I.IsPrime
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ (↑J : Set P)
hyI : y ∉ (↑I : Set P)
⊢ x ⊓ y ⊔ x ⊓ yᶜ ∈ J

Tactic:
sup_mem (J.lower inf_le_right hyJ)
      (hIJ.le <| I.lower inf_le_right <| IsPrime.compl_mem_of_notMem ‹_› hyI)

Premises used: Order.Ideal.lower, Order.Ideal.IsPrime.compl_mem_of_notMem, Set.Mem, inf_le_right, LT.lt.le, Order.Ideal.sup_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x_1 : P
I : Ideal P
inst_1 : I.IsPrime
J : Ideal P
hIJ : I < J
x y : P
hyJ : y ∈ (↑J : Set P)
hyI : y ∉ (↑I : Set P)
⊢ x ⊓ y ⊔ x ⊓ yᶜ ∈ J

Tactic:
exact
    sup_mem (J.lower inf_le_right hyJ)
      (hIJ.le <| I.lower inf_le_right <| IsPrime.compl_mem_of_notMem ‹_› hyI)

Premises used: Order.Ideal.lower, Order.Ideal.IsPrime.compl_mem_of_notMem, inf_le_right, LT.lt.le, Order.Ideal.sup_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : Ideal.PrimePair P
rw : IsIdeal (↑IF.I : Set P)
⊢ IsIdeal (↑IF.F : Set P)ᶜ

Tactic:
rw [IF.compl_F_eq_I]

Premises used: Order.Ideal.PrimePair.compl_F_eq_I
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal (↑IF.I : Set P)

Tactic:
IF.I.isIdeal

Premises used: Order.Ideal.isIdeal, Order.Ideal.PrimePair.I
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal (↑IF.I : Set P)

Tactic:
exact IF.I.isIdeal

Premises used: Order.Ideal.isIdeal, Order.Ideal.PrimePair.I
-- Module: Mathlib.Order.PrimeSeparator
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : α
J : Ideal α
⊢ b ∈ J ⊔ principal a ↔ ∃ j ∈ J, b ≤ j ⊔ a

Tactic:
⟨fun ⟨j, ⟨jJ, _, ha', bja'⟩⟩ => ⟨j, jJ, le_trans bja' (sup_le_sup_left ha' j)⟩,
    fun ⟨j, hj, hbja⟩ => ⟨j, hj, a, le_refl a, hbja⟩⟩

Premises used: sup_le_sup_left, le_refl, Membership.mem, Exists, _private.0.DistribLattice.mem_ideal_sup_principal.match_1, LE.le, And, _private.0.DistribLattice.mem_ideal_sup_principal.match_2, Max.max, And.intro, Iff.intro, Exists.intro, Order.Ideal.principal, 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}
left : (↑I : Set α) ≤ (↑I : Set α)
right : Disjoint (↑F : Set α) (↑I : Set α)
left₁ : (↑I : Set α) ≤ (↑I : Set α)
right₁ : Disjoint (↑F : Set α) (↑I : Set α)
left₂ : (↑I : Set α) ≤ (↑I : Set α)
right₂ : Disjoint (↑F : Set α) (↑I : Set α)
left₃ : (↑I : Set α) ≤ (↑I : Set α)
right₃ : Disjoint (↑F : Set α) (↑I : Set α)
⊢ (↑I : Set α) ≤ (↑I : Set α) ∧ Disjoint (↑F : Set α) (↑I : Set α)

Tactic:
trivial
-- 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}
⊢ (↑I : Set α) ∈ S

Tactic:
refine ⟨Order.Ideal.isIdeal I, by trivial⟩
-- 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}
⊢ (↑I : Set α) ∈ S

Tactic:
have IinS : ↑I ∈ S := by
    refine ⟨Order.Ideal.isIdeal I, by trivial⟩
-- 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
h : ⋃₀ c ∈ S ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
⊢ ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub

Tactic:
use sUnion c

Premises used: Set.sUnion
-- 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ ⋃₀ c ∈ S ∧ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
⟨?_, fun s hs ↦ le_sSup hs⟩

Premises used: And.intro, le_sSup
-- 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
h : ⋃₀ c ∈ S
⊢ ⋃₀ c ∈ S ∧ ∀ s ∈ c, s ⊆ ⋃₀ c

Tactic:
refine ⟨?_, fun s hs ↦ le_sSup hs⟩
-- 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
h : IsIdeal (⋃₀ c) ∧ (↑I : Set α) ⊆ ⋃₀ c ∧ ∀ t ∈ c, Disjoint (↑F : Set α) t
⊢ ⋃₀ c ∈ S

Tactic:
simp only [le_eq_subset, mem_setOf_eq, disjoint_sUnion_right, S]

Premises used: Set.le_eq_subset, Set.mem_setOf_eq, Set.disjoint_sUnion_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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
h : ∀ (J : Set α) (hJ : J ∈ c), IsIdeal (⋃₀ c) ∧ (↑I : Set α) ⊆ ⋃₀ c ∧ ∀ t ∈ c, Disjoint (↑F : Set α) t
⊢ IsIdeal (⋃₀ c) ∧ (↑I : Set α) ⊆ ⋃₀ c ∧ ∀ t ∈ c, Disjoint (↑F : Set α) t

Tactic:
let ⟨J, hJ⟩ := hcNe
-- 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
J : Set α
hJ : J ∈ c
⊢ IsIdeal (⋃₀ c) ∧ (↑I : Set α) ⊆ ⋃₀ c ∧ ∀ t ∈ c, Disjoint (↑F : Set α) t

Tactic:
⟨Order.isIdeal_sUnion_of_isChain (fun _ hJ ↦ (hcS hJ).1) hcC hcNe,
            ⟨le_trans (hcS hJ).2.1 (le_sSup hJ), fun J hJ ↦ (hcS hJ).2.2⟩⟩

Premises used: And.right, And.left, And.intro, Order.isIdeal_sUnion_of_isChain, le_sSup, 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
J : Set α
hJ : J ∈ c
⊢ IsIdeal (⋃₀ c) ∧ (↑I : Set α) ⊆ ⋃₀ c ∧ ∀ t ∈ c, Disjoint (↑F : Set α) t

Tactic:
refine ⟨Order.isIdeal_sUnion_of_isChain (fun _ hJ ↦ (hcS hJ).1) hcC hcNe,
            ⟨le_trans (hcS hJ).2.1 (le_sSup hJ), fun J hJ ↦ (hcS hJ).2.2⟩⟩
-- 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}
IinS : (↑I : Set α) ∈ S
⊢ ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub

Tactic:
have chainub : ∀ c ⊆ S, IsChain (· ⊆ ·) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub := by
    intro c hcS hcC hcNe
    use sUnion c
    refine ⟨?_, fun s hs ↦ le_sSup hs⟩
    simp only [le_eq_subset, mem_setOf_eq, disjoint_sUnion_right, S]
    let ⟨J, hJ⟩ := hcNe
    refine ⟨Order.isIdeal_sUnion_of_isChain (fun _ hJ ↦ (hcS hJ).1) hcC hcNe,
            ⟨le_trans (hcS hJ).2.1 (le_sSup hJ), fun J hJ ↦ (hcS hJ).2.2⟩⟩
-- 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}
IinS : (↑I : Set α) ∈ S
chainub : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
obtain :
  ∀ (Jset : Set α),
    (↑I : Set α) ⊆ Jset →
      ∀ (hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset),
        ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)

Tactic:
obtain ⟨Jset, _, hmax⟩ := zorn_subset_nonempty S chainub I IinS

Premises used: SetLike.coe, zorn_subset_nonempty
-- 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}
IinS : (↑I : Set α) ∈ S
chainub : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
⊢ IsIdeal Jset

Tactic:
obtain ⟨Jidl, IJ, JF⟩ := hmax.prop

Premises used: Maximal.prop
-- 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}
IinS : (↑I : Set α) ∈ S
chainub : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
⊢ (↑I : Set α) ≤ Jset

Tactic:
obtain ⟨Jidl, IJ, JF⟩ := hmax.prop

Premises used: Maximal.prop
-- 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}
IinS : (↑I : Set α) ∈ S
chainub : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
Jset : Set α
left : (↑I : Set α) ⊆ Jset
hmax : Maximal (fun (x : Set α) ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : (↑I : Set α) ≤ Jset
⊢ Disjoint (↑F : Set α) Jset

Tactic:
obtain ⟨Jidl, IJ, JF⟩ := hmax.prop

Premises used: Maximal.prop
-- 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}
IinS : (↑I : Set α) ∈ S
chainub : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
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)
h : J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)

Tactic:
use 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}
IinS : (↑I : Set α) ∈ S
chainub : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
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)
⊢ I ≤ J

Tactic:
have IJ' : I ≤ J := IJ
-- 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
⊢ J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)

Tactic:
⟨?_, ⟨IJ, JF⟩⟩

Premises used: And.intro
-- 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
h : J.IsPrime
⊢ J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)

Tactic:
refine ⟨?_, ⟨IJ, JF⟩⟩
-- 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
⊢ J.IsProper

Tactic:
have Jpr : IsProper J := isProper_of_notMem (Set.disjoint_left.1 JF F.top_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
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
h : ∀ {x y : α}, x ⊓ y ∈ J → x ∈ J ∨ y ∈ J
⊢ J.IsPrime

Tactic:
rw [isPrime_iff_mem_or_mem]

Premises used: Order.Ideal.isPrime_iff_mem_or_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
JF : Disjoint (↑F : Set α) Jset
J : Ideal α := Jidl.toIdeal (I := Jset)
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
h : a₁ ∉ J ∧ a₂ ∉ J → a₁ ⊓ a₂ ∉ J
⊢ a₁ ⊓ a₂ ∈ J → a₁ ∈ J ∨ a₂ ∈ J

Tactic:
contrapose!
-- 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₁

Tactic:
have a₁J₁ : a₁ ∈ J₁ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self
-- 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₂

Tactic:
have a₂J₂ : a₂ ∈ J₂ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self
-- 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₁ : Set α) ≠ Jset

Tactic:
have J₁J : ↑J₁ ≠ Jset := ne_of_mem_of_not_mem' a₁J₁ ha₁
-- 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₂ : Set α) ≠ Jset

Tactic:
have J₂J : ↑J₂ ≠ Jset := ne_of_mem_of_not_mem' a₂J₂ ha₂
-- 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₁ : Set α) ∉ S

Tactic:
have J₁S : ↑J₁ ∉ S := fun h => J₁J (hmax.eq_of_le h (le_sup_left : J ≤ J₁)).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₂ : Set α) ∉ S

Tactic:
have J₂S : ↑J₂ ∉ S := fun h => J₂J (hmax.eq_of_le h (le_sup_left : J ≤ J₂)).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
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
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
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
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⟩