awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
⊢ s.Infinite
have inhabit : ∀ (inhabited_h : Inhabited α), s.Infinite
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Nonempty α
h : ∀ (a : α), ∃ b ∈ s, a < b
inhabited_h : Inhabited α
f : (n : ℕ) → α :=
  fun (n : ℕ) ↦
    Nat.recOn (motive := fun (x : ℕ) ↦ α) n (Exists.choose (p := fun (b : α) ↦ b ∈ s ∧ default < b) ⋯)
      fun (x : ℕ) (a : α) ↦ ⋯.choose (p := fun (b : α) ↦ b ∈ s ∧ a < b)
⊢ s.Infinite
have hf : ∀ (n : ℕ), f n ∈ s
Tactic: have hf : ∀ n, f n ∈ s := by rintro (_ | _) <;> exact (h _).choose_spec.1
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
t : Set β
f : α → β
inst_1 : Infinite α
hf : ∀ (a : α), f a ∈ t
ht : t.Finite
⊢ ∃ (a : α) (b : α), a < b ∧ f a = f b
have hf₁ : MapsTo f univ t
Tactic: rw [← mapsTo_univ_iff] at hf
Cleared hypotheses: hf, ht
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
t : Set β
f : α → β
inst_1 : Infinite α
hf : MapsTo f univ t
ht : t.Finite
⊢ ∃ (a : α) (b : α), a < b ∧ f a = f b
have obtain : ∀ (a b : α) (h : a < b ∧ f a = f b), ∃ (a : α) (b : α), a < b ∧ f a = f b
Tactic: obtain ⟨a, -, b, -, h⟩ := infinite_univ.exists_lt_map_eq_of_mapsTo hf ht
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
have inl : ∀ (hs : Set.Finite.{u_2} (α := α) ∅) (hs' : IsCofinal.{u_2} (α := α) ∅), ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
Tactic: obtain rfl | hn := s.eq_empty_or_nonempty
Cleared hypotheses: s, hs, hs'
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
inl :
  ∀ (hs : Set.Finite.{u_2} (α := α) ∅) (hs' : IsCofinal.{u_2} (α := α) ∅), ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
have inr : ∀ (hn : s.Nonempty), ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
Tactic: obtain rfl | hn := s.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : LinearOrder α
hs : Set.Finite.{u_2} (α := α) ∅
hs' : IsCofinal.{u_2} (α := α) ∅
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
have h : Set.Subsingleton.{u_2} (α := α) ∅ ∧ IsCofinal.{u_2} (α := α) ∅
Tactic: use ∅
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
have inr : ∀ (a : α) (ha : Maximal (fun (x : α) ↦ x ∈ s) a), ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
Tactic: obtain ⟨a, ha⟩ := hs.exists_maximal hn
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun (x : α) ↦ x ∈ s) a
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
have h : Set.Subsingleton (α := α) {a} ∧ IsCofinal (α := α) {a}
Tactic: use {a}
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun (x : α) ↦ x ∈ s) a
⊢ Set.Subsingleton (α := α) {a} ∧ IsCofinal (α := α) {a}
have h : IsTop a
Tactic: suffices IsTop a by simpa [IsCofinal]
-- Lean 4 proof step from Mathlib.Order.Preorder.Finite (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
a : α
ha : Maximal (fun (x : α) ↦ x ∈ s) a
b : α
⊢ b ≤ a
have h : ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c), b ≤ a
Tactic: obtain ⟨c, hc, hbc⟩ := hs' b
-- Lean 4 proof step from Mathlib.Order.Preorder.Finsupp (goal)
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : Lattice M
f g : ι →₀ M
inst_2 : DecidableEq ι
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support) : Set ι)ᶜ = (↑(f.support ∪ g.support) : Set ι)ᶜ
have h : ∀ (x : ι), x ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support) : Set ι)ᶜ ↔ x ∈ (↑(f.support ∪ g.support) : Set ι)ᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
⊢ IF.I.IsProper
have obtain : ∀ (w : P) (h : w ∈ (↑IF.F : Set P)), IF.I.IsProper
Tactic: obtain ⟨w, h⟩ := IF.F.nonempty
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
w : P
h : w ∈ (↑IF.F : Set P)
⊢ IF.I.IsProper
have apply : w ∉ IF.I
Tactic: apply isProper_of_notMem (_ : w ∉ IF.I)
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
w : P
h : w ∈ (↑IF.F : Set P)
⊢ w ∉ IF.I
have rwa : ∀ (h : w ∈ (↑IF.I : Set P)ᶜ), w ∉ IF.I
Tactic: rwa [← IF.compl_I_eq_F] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
⊢ IsPFilter (↑IF.I : Set P)ᶜ
have rw : IsPFilter (↑IF.F : Set P)
Tactic: rw [IF.compl_I_eq_F]
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
have contrapose! : x ∉ I ∧ y ∉ I → x ⊓ y ∉ I
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
F : PFilter P := IsPFilter.toPFilter (F := (↑I : Set P)ᶜ) ⋯
⊢ x ∉ I ∧ y ∉ I → x ⊓ y ∉ I
have change : x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
Tactic: change x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
inst_1 : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ I.IsPrime
have rw : I.IsProper ∧ IsPFilter (↑I : Set P)ᶜ
Tactic: rw [isPrime_iff]
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
inst_1 : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ I.IsProper ∧ IsPFilter (↑I : Set P)ᶜ
have right : IsPFilter (↑I : Set P)ᶜ
Tactic: use ‹_›
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
inst_1 : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ IsPFilter (↑I : Set P)ᶜ
have right : (↑I : Set P)ᶜ.Nonempty
Tactic: refine .of_def ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
inst_1 : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
right : (↑I : Set P)ᶜ.Nonempty
⊢ IsPFilter (↑I : Set P)ᶜ
have right₁ : DirectedOn (fun (x1 x2 : P) ↦ x1 ≥ x2) (↑I : Set P)ᶜ
Tactic: refine .of_def ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
inst_1 : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
right : (↑I : Set P)ᶜ.Nonempty
right₁ : DirectedOn (fun (x1 x2 : P) ↦ x1 ≥ x2) (↑I : Set P)ᶜ
⊢ IsPFilter (↑I : Set P)ᶜ
have right₂ : ∀ {x y : P}, x ≤ y → x ∈ (↑I : Set P)ᶜ → y ∈ (↑I : Set P)ᶜ
Tactic: refine .of_def ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
⊢ I.IsPrime
have rw : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
Tactic: rw [isPrime_iff_mem_or_mem]
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
have contrapose! : x ∉ I ∧ y ∉ I → x ⊓ y ∉ I
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
⊢ False
have apply : y ∈ I
Tactic: apply hynI
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (hypothesis)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
⊢ y ∈ I
have hJuniv : (↑J : Set P) = Set.univ
Tactic: have hJuniv : (J : Set P) = Set.univ :=
    IsMaximal.maximal_proper (lt_sup_principal_of_notMem ‹_›)
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (hypothesis)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : (↑J : Set P) = Set.univ
⊢ y ∈ I
have hyJ : y ∈ (↑J : Set P)
Tactic: have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (hypothesis)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : (↑J : Set P) = Set.univ
hyJ : y ∈ (↑J : Set P)
⊢ y ∈ I
have hyJ₁ : Membership.mem (γ := Set P) {x_1 : P | ∃ i ∈ I, ∃ (j : P), Membership.mem (γ := Ideal P) (principal x) j ∧ x_1 = i ⊔ j}
  y
Tactic: rw [coe_sup_eq] at hyJ
Cleared hypotheses: hyJ
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : (↑J : Set P) = Set.univ
hyJ :
  Membership.mem (γ := Set P)
    {x_1 : P | ∃ i ∈ I, ∃ (j : P), Membership.mem (γ := Ideal P) (principal x) j ∧ x_1 = i ⊔ j} y
⊢ y ∈ I
have rcases : ∀ (a : P) (ha : a ∈ I) (b : P) (hb : Membership.mem (γ := Ideal P) (principal x) b) (hy : y = a ⊔ b), y ∈ I
Tactic: rcases hyJ with ⟨a, ha, b, hb, hy⟩
Cleared hypotheses: hyJ
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : (↑J : Set P) = Set.univ
a : P
ha : a ∈ I
b : P
hb : Membership.mem (γ := Ideal P) (principal x) b
hy : y = a ⊔ b
⊢ y ∈ I
have rw : a ⊔ b ∈ I
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : (↑J : Set P) = Set.univ
a : P
ha : a ∈ I
b : P
hb : Membership.mem (γ := Ideal P) (principal x) b
hy : y = a ⊔ b
⊢ a ⊔ b ∈ I
have refine : b ≤ y
Tactic: refine sup_mem ha (I.lower (le_inf hb ?_) hxy)
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : (↑J : Set P) = Set.univ
a : P
ha : a ∈ I
b : P
hb : Membership.mem (γ := Ideal P) (principal x) b
hy : y = a ⊔ b
⊢ b ≤ y
have rw : b ≤ a ⊔ b
Tactic: rw [hy]
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ x ∈ I ∨ xᶜ ∈ I
have apply : x ⊓ xᶜ ∈ I
Tactic: apply hI.mem_or_mem
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ x ⊓ xᶜ ∈ I
have rw : ⊥ ∈ I
Tactic: rw [inf_compl_eq_bot]
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
I : Ideal P
inst_1 : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ I.IsPrime
have simp : ∀ {x y : P}, x ⊓ y ∈ I → x ∉ I → y ∈ I
Tactic: simp only [isPrime_iff_mem_or_mem, or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (hypothesis)
Goal:
P : Type u_1
inst : BooleanAlgebra P
I : Ideal P
inst_1 : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
⊢ y ∈ I
have hxcI : xᶜ ∈ I
Tactic: have hxcI : xᶜ ∈ I := h.resolve_left hxI
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (hypothesis)
Goal:
P : Type u_1
inst : BooleanAlgebra P
I : Ideal P
inst_1 : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
⊢ y ∈ I
have ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
Tactic: have ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I := sup_mem hxy (I.lower inf_le_right hxcI)
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
I : Ideal P
inst_1 : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
⊢ y ∈ I
have rwa : ∀ (ass : y ⊓ x ⊔ y ⊓ xᶜ ∈ I), y ∈ I
Tactic: rwa [inf_comm, sup_inf_inf_compl] at ass
Cleared hypotheses: ass
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
I : Ideal P
inst_1 : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
hxcI : xᶜ ∈ I
ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I
rwa : ∀ (ass : y ⊓ x ⊔ y ⊓ xᶜ ∈ I), y ∈ I
⊢ y ∈ I
have rwa₁ : ∀ (ass : y ∈ I), y ∈ I
Tactic: rwa [inf_comm, sup_inf_inf_compl] at ass
Cleared hypotheses: ass
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
inst_1 : I.IsPrime
⊢ I.IsMaximal
have simp : ∀ ⦃J : Ideal P⦄, I < J → ∀ (x : P), x ∈ (↑J : Set P)
Tactic: simp only [isMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
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 : P
⊢ x ∈ (↑J : Set P)
have rcases : ∀ (y : P) (hyJ : y ∈ (↑J : Set P)) (hyI : y ∉ (↑I : Set P)), x ∈ (↑J : Set P)
Tactic: rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
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)
ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J
⊢ x ∈ (↑J : Set P)
have rwa : ∀ (ass : x ∈ J), x ∈ (↑J : Set P)
Tactic: rwa [sup_inf_inf_compl] at ass
Cleared hypotheses: ass
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
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 ∈ (↑J : Set P)
have suffices : x ⊓ y ⊔ x ⊓ yᶜ ∈ J
Tactic: suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J by rwa [sup_inf_inf_compl] at ass
-- Lean 4 proof step from Mathlib.Order.PrimeIdeal (goal)
Goal:
P : Type u_1
inst : Preorder P
IF : Ideal.PrimePair P
⊢ IsIdeal (↑IF.F : Set P)ᶜ
have rw : IsIdeal (↑IF.I : Set P)
Tactic: rw [IF.compl_F_eq_I]
-- 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}
⊢ (↑I : Set α) ≤ (↑I : Set α) ∧ Disjoint (↑F : Set α) (↑I : Set α)
have left : (↑I : Set α) ≤ (↑I : Set α)
Tactic: trivial
-- 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}
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have IinS : (↑I : Set α) ∈ S
Tactic: have IinS : ↑I ∈ S := by
    refine ⟨Order.Ideal.isIdeal I, by trivial⟩
-- 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
have h : ⋃₀ c ∈ S ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic: use sUnion c
-- 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}
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
have h : ⋃₀ c ∈ S
Tactic: refine ⟨?_, fun s hs ↦ le_sSup hs⟩
-- 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ ⋃₀ c ∈ S
have h : IsIdeal (⋃₀ c) ∧ (↑I : Set α) ⊆ ⋃₀ c ∧ ∀ t ∈ c, Disjoint (↑F : Set α) t
Tactic: simp only [le_eq_subset, mem_setOf_eq, disjoint_sUnion_right, 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}
IinS : (↑I : Set α) ∈ S
c : Set (Set α)
hcS : c ⊆ S
hcC : IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c
hcNe : c.Nonempty
⊢ IsIdeal (⋃₀ c) ∧ (↑I : Set α) ⊆ ⋃₀ c ∧ ∀ t ∈ c, Disjoint (↑F : Set α) t
have h : ∀ (J : Set α) (hJ : J ∈ c), IsIdeal (⋃₀ c) ∧ (↑I : Set α) ⊆ ⋃₀ c ∧ ∀ t ∈ c, Disjoint (↑F : Set α) t
Tactic: let ⟨J, hJ⟩ := hcNe
-- 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}
IinS : (↑I : Set α) ∈ S
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have chainub : ∀ 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⟩⟩
-- 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}
IinS : (↑I : Set α) ∈ S
chainub : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have 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 α)
Tactic: obtain ⟨Jset, _, hmax⟩ := zorn_subset_nonempty S chainub I IinS
-- 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}
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
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have Jidl : IsIdeal Jset
Tactic: obtain ⟨Jidl, IJ, JF⟩ := hmax.prop
-- 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}
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
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have IJ : (↑I : Set α) ≤ Jset
Tactic: obtain ⟨Jidl, IJ, JF⟩ := hmax.prop
-- 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}
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
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have JF : Disjoint (↑F : Set α) Jset
Tactic: obtain ⟨Jidl, IJ, JF⟩ := hmax.prop
-- 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}
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)
⊢ ∃ (J : Ideal α), J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have h : J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
Tactic: use 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}
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)
⊢ J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have IJ' : I ≤ J
Tactic: have IJ' : I ≤ J := IJ
-- 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
⊢ J.IsPrime ∧ I ≤ J ∧ Disjoint (↑F : Set α) (↑J : Set α)
have h : J.IsPrime
Tactic: refine ⟨?_, ⟨IJ, JF⟩⟩
-- 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
⊢ J.IsPrime
have Jpr : J.IsProper
Tactic: have Jpr : IsProper J := isProper_of_notMem (Set.disjoint_left.1 JF F.top_mem)