awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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
⊢ J.IsPrime
have h : ∀ {x y : α}, x ⊓ y ∈ J → x ∈ J ∨ y ∈ J
Tactic: rw [isPrime_iff_mem_or_mem]
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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₂ : α
⊢ a₁ ⊓ a₂ ∈ J → a₁ ∈ J ∨ a₂ ∈ J
have h : a₁ ∉ J ∧ a₂ ∉ J → a₁ ⊓ a₂ ∉ J
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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₁ ⊓ a₂ ∉ J
have a₁J₁ : a₁ ∈ J₁
Tactic: have a₁J₁ : a₁ ∈ J₁ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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₁ ⊓ a₂ ∉ J
have a₂J₂ : a₂ ∈ J₂
Tactic: have a₂J₂ : a₂ ∈ J₂ := mem_of_subset_of_mem (le_sup_right : _ ≤ J ⊔ _) mem_principal_self
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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₂
⊢ a₁ ⊓ a₂ ∉ J
have J₁J : (↑J₁ : Set α) ≠ Jset
Tactic: have J₁J : ↑J₁ ≠ Jset := ne_of_mem_of_not_mem' a₁J₁ ha₁
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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
⊢ a₁ ⊓ a₂ ∉ J
have J₂J : (↑J₂ : Set α) ≠ Jset
Tactic: have J₂J : ↑J₂ ≠ Jset := ne_of_mem_of_not_mem' a₂J₂ ha₂
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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
⊢ a₁ ⊓ a₂ ∉ J
have J₁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
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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
⊢ a₁ ⊓ a₂ ∉ J
have J₂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
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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 α)
⊢ False
have apply : (↑J₁ : Set α) ∈ S
Tactic: apply J₁S
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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 α)
⊢ (↑J₁ : Set α) ∈ S
have simp : IsIdeal (↑J₁ : Set α) ∧ I ≤ J₁ ∧ Disjoint (↑F : Set α) (↑J₁ : Set α)
Tactic: simp only [le_eq_subset, mem_setOf_eq, SetLike.coe_subset_coe, S]
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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
⊢ a₁ ⊓ a₂ ∉ J
have J₁F : ¬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⟩
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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 α)
⊢ False
have apply : (↑J₂ : Set α) ∈ S
Tactic: apply J₂S
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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 α)
⊢ (↑J₂ : Set α) ∈ S
have simp : IsIdeal (↑J₂ : Set α) ∧ I ≤ J₂ ∧ Disjoint (↑F : Set α) (↑J₂ : Set α)
Tactic: simp only [le_eq_subset, mem_setOf_eq, SetLike.coe_subset_coe, S]
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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 α)
⊢ a₁ ⊓ a₂ ∉ J
have J₂F : ¬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⟩
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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 α)
⊢ a₁ ⊓ a₂ ∉ J
have h : ∀ (c₁ : α) (c₁F : c₁ ∈ (↑F : Set α)) (c₁J₁ : c₁ ∈ (↑J₁ : Set α)), a₁ ⊓ a₂ ∉ J
Tactic: let ⟨c₁, ⟨c₁F, c₁J₁⟩⟩ := Set.not_disjoint_iff.1 J₁F
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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 α)
⊢ a₁ ⊓ a₂ ∉ J
have h : ∀ (c₂ : α) (c₂F : c₂ ∈ (↑F : Set α)) (c₂J₂ : c₂ ∈ (↑J₂ : Set α)), a₁ ⊓ a₂ ∉ J
Tactic: let ⟨c₂, ⟨c₂F, c₂J₂⟩⟩ := Set.not_disjoint_iff.1 J₂F
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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 α)
⊢ a₁ ⊓ a₂ ∉ J
have h : ∀ (b₁ : α) (b₁J : b₁ ∈ J) (cba₁ : c₁ ≤ b₁ ⊔ a₁), a₁ ⊓ a₂ ∉ J
Tactic: let ⟨b₁, ⟨b₁J, cba₁⟩⟩ := (mem_ideal_sup_principal a₁ c₁ J).1 c₁J₁
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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₁
⊢ a₁ ⊓ a₂ ∉ J
have h : ∀ (b₂ : α) (b₂J : b₂ ∈ J) (cba₂ : c₂ ≤ b₂ ⊔ a₂), a₁ ⊓ a₂ ∉ J
Tactic: let ⟨b₂, ⟨b₂J, cba₂⟩⟩ := (mem_ideal_sup_principal a₂ c₂ J).1 c₂J₂
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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₂
⊢ a₁ ⊓ a₂ ∉ J
have bJ : b ∈ J
Tactic: have bJ : b ∈ J := sup_mem b₁J b₂J
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂)
have h₁ : b₁ ≤ b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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
⊢ (b₁ ⊔ a₁) ⊓ (b₂ ⊔ a₂) ≤ (b ⊔ a₁) ⊓ (b ⊔ a₂)
have h₂ : b₂ ≤ b
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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
⊢ a₁ ⊓ a₂ ∉ J
have ineq : 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
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (hypothesis)
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₂
⊢ a₁ ⊓ a₂ ∉ J
have ba₁a₂F : 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)
-- Lean 4 proof step from Mathlib.Order.PrimeSeparator (goal)
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
⊢ a₁ ⊓ a₂ ∉ J
have h : ∀ (ha₁a₂ : a₁ ⊓ a₂ ∈ J), ¬Disjoint (↑F : Set α) Jset
Tactic: contrapose JF with ha₁a₂
Cleared hypotheses: JF