awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
s : Set α
t : Set β
f : α → β
hs : s.Infinite
hf : MapsTo f s t
ht : t.Finite
⊢ ∃ x ∈ s, ∃ y ∈ s, x < y ∧ f x = f y

Tactic:
let ⟨x, hx, y, hy, hxy, hf⟩ := hs.exists_ne_map_eq_of_mapsTo hf ht
  hxy.lt_or_gt.elim (fun hxy => ⟨x, hx, y, hy, hxy, hf⟩) fun hyx => ⟨y, hy, x, hx, hyx, hf.symm⟩

Premises used: _private.0.Set.Infinite.exists_lt_map_eq_of_mapsTo.match_1, Membership.mem, Exists, And, And.intro, LT.lt, Exists.intro, Or.elim, Eq.symm, Set.Infinite.exists_ne_map_eq_of_mapsTo, Eq, Ne.lt_or_gt
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
t : Set β
f : α → β
inst_1 : Infinite α
hf : ∀ (a : α), f a ∈ t
ht : t.Finite
⊢ MapsTo f univ t

Tactic:
rw [← mapsTo_univ_iff] at hf

Premises used: Set.mapsTo_univ_iff
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
t : Set β
f : α → β
inst_1 : Infinite α
hf : ∀ (a : α), f a ∈ t
ht : t.Finite
hf₁ : MapsTo f univ t
⊢ t.Finite

Tactic:
rw [← mapsTo_univ_iff] at hf

Premises used: Set.mapsTo_univ_iff
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
β : Type u_3
inst : LinearOrder α
t : Set β
f : α → β
inst_1 : Infinite α
hf : MapsTo f univ t
ht : t.Finite
obtain : ∀ (a b : α) (h : a < b ∧ f a = f b), ∃ (a : α) (b : α), 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

Premises used: Set.Infinite.exists_lt_map_eq_of_mapsTo, Set.infinite_univ
-- Module: Mathlib.Order.Preorder.Finite
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 : α
h : a < b ∧ f a = f b
⊢ ∃ (a : α) (b : α), a < b ∧ f a = f b

Tactic:
⟨a, b, h⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.Preorder.Finite
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 : α
h : a < b ∧ f a = f b
⊢ ∃ (a : α) (b : α), a < b ∧ f a = f b

Tactic:
exact ⟨a, b, h⟩
-- Module: Mathlib.Order.Preorder.Finite
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
inr : ∀ (hn : s.Nonempty), ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t

Tactic:
obtain rfl | hn := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : LinearOrder α
hs : Set.Finite.{u_2} (α := α) ∅
hs' : IsCofinal.{u_2} (α := α) ∅
h : Set.Subsingleton.{u_2} (α := α) ∅ ∧ IsCofinal.{u_2} (α := α) ∅
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t

Tactic:
use ∅
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : LinearOrder α
hs : Set.Finite.{u_2} (α := α) ∅
hs' : IsCofinal.{u_2} (α := α) ∅
⊢ Set.Subsingleton.{u_2} (α := α) ∅ ∧ IsCofinal.{u_2} (α := α) ∅

Tactic:
simpa
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
hs : s.Finite
hs' : IsCofinal s
hn : s.Nonempty
inr : ∀ (a : α) (ha : Maximal (fun (x : α) ↦ x ∈ s) a), ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t

Tactic:
obtain ⟨a, ha⟩ := hs.exists_maximal hn

Premises used: Set.Finite.exists_maximal
-- Module: Mathlib.Order.Preorder.Finite
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
h : Set.Subsingleton (α := α) {a} ∧ IsCofinal (α := α) {a}
⊢ ∃ (t : Set α), t.Subsingleton ∧ IsCofinal t

Tactic:
use {a}
-- Module: Mathlib.Order.Preorder.Finite
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
this : IsTop a
⊢ Set.Subsingleton (α := α) {a} ∧ IsCofinal (α := α) {a}

Tactic:
simpa [IsCofinal]

Premises used: IsCofinal
-- Module: Mathlib.Order.Preorder.Finite
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
h : IsTop a
⊢ Set.Subsingleton (α := α) {a} ∧ IsCofinal (α := α) {a}

Tactic:
suffices IsTop a by simpa [IsCofinal]
-- Module: Mathlib.Order.Preorder.Finite
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 : α
h : ∀ (c : α) (hc : c ∈ s) (hbc : b ≤ c), b ≤ a
⊢ b ≤ a

Tactic:
obtain ⟨c, hc, hbc⟩ := hs' b
-- Module: Mathlib.Order.Preorder.Finite
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 c : α
hc : c ∈ s
hbc : b ≤ c
⊢ b ≤ a

Tactic:
hbc.trans (ha.le hc)

Premises used: Maximal.le, LE.le.trans
-- Module: Mathlib.Order.Preorder.Finite
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 c : α
hc : c ∈ s
hbc : b ≤ c
⊢ b ≤ a

Tactic:
exact hbc.trans (ha.le hc)

Premises used: Maximal.le, LE.le.trans
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Finite α
p : α → Prop
a : α
h : p a
⊢ ∃ (b : α), a ≤ b ∧ Maximal p b

Tactic:
{x | p x}.toFinite.exists_le_maximal h

Premises used: Set.Mem, setOf, Set.Finite.exists_le_maximal, Set.toFinite
-- Module: Mathlib.Order.Preorder.Finite
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Finite α
p : α → Prop
a : α
h : p a
⊢ ∃ b ≤ a, Minimal p b

Tactic:
{x | p x}.toFinite.exists_le_minimal h

Premises used: Set.Mem, setOf, Set.toFinite, Set.Finite.exists_le_minimal
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : LE M
f g : ι →₀ M
⊢ f ≤ g ↔ ∀ (i : ι), LE.le.{u_2} (α := M) ((f : (a : ι) → M) i : M) ((g : (a : ι) → M) i : M)

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : LE M
f g : ι →₀ M
⊢ LE.le (α := (a : ι) → M) (⇑f : (a : ι) → M) (⇑g : (a : ι) → M) ↔ f ≤ g

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : Preorder M
f g : ι →₀ M
⊢ f < g ↔ f ≤ g ∧ ∃ (i : ι), LT.lt.{u_2} (α := M) ((f : (a : ι) → M) i : M) ((g : (a : ι) → M) i : M)

Tactic:
Pi.lt_def

Premises used: Pi.lt_def
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : Preorder M
f g : ι →₀ M
⊢ LT.lt (α := (a : ι) → M) (⇑f : (a : ι) → M) (⇑g : (a : ι) → M) ↔ f < g

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : Preorder M
⊢ Monotone (α := ι →₀ M) toFun

Tactic:
fun _ _ ↦ id

Premises used: Monotone, id
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : SemilatticeInf M
f g : ι →₀ M
i : ι
⊢ Eq.{u_2 + 1} (α := M) ((f ⊓ g : (a : ι) → M) i : M) ((f : (a : ι) → M) i ⊓ (g : (a : ι) → M) i : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : SemilatticeSup M
f g : ι →₀ M
i : ι
⊢ Eq.{u_2 + 1} (α := M) ((f ⊔ g : (a : ι) → M) i : M) ((f : (a : ι) → M) i ⊔ (g : (a : ι) → M) i : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : Lattice M
f g : ι →₀ M
inst_2 : DecidableEq ι
h : ∀ (x : ι), x ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support) : Set ι)ᶜ ↔ x ∈ (↑(f.support ∪ g.support) : Set ι)ᶜ
⊢ (↑((f ⊓ g).support ∪ (f ⊔ g).support) : Set ι)ᶜ = (↑(f.support ∪ g.support) : Set ι)ᶜ

Tactic:
ext
-- Module: Mathlib.Order.Preorder.Finsupp
Goal:
ι : Type u_1
M : Type u_2
inst : Zero M
inst_1 : Lattice M
f g : ι →₀ M
inst_2 : DecidableEq ι
x : ι
⊢ x ∈ (↑((f ⊓ g).support ∪ (f ⊔ g).support) : Set ι)ᶜ ↔ x ∈ (↑(f.support ∪ g.support) : Set ι)ᶜ

Tactic:
simp [inf_eq_and_sup_eq_iff]

Premises used: inf_eq_and_sup_eq_iff
-- Module: Mathlib.Order.Preorder.Finsupp
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 = f.support ∪ g.support

Tactic:
(union_comm _ _).trans <| support_inf_union_support_sup _ _

Premises used: Finset.union_comm, Finsupp.support_inf_union_support_sup, Eq.trans
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
⊢ (↑IF.I : Set P)ᶜ = (↑IF.F : Set P)

Tactic:
IF.isCompl_I_F.compl_eq

Premises used: Order.Ideal.PrimePair.isCompl_I_F, IsCompl.compl_eq
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
⊢ (↑IF.F : Set P)ᶜ = (↑IF.I : Set P)

Tactic:
IF.isCompl_I_F.eq_compl.symm

Premises used: Order.Ideal.PrimePair.isCompl_I_F, Eq.symm, IsCompl.eq_compl
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
obtain : ∀ (w : P) (h : w ∈ (↑IF.F : Set P)), IF.I.IsProper
⊢ IF.I.IsProper

Tactic:
obtain ⟨w, h⟩ := IF.F.nonempty

Premises used: Order.PFilter.nonempty, Order.Ideal.PrimePair.F
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
w : P
h : w ∈ (↑IF.F : Set P)
apply : w ∉ IF.I
⊢ IF.I.IsProper

Tactic:
apply isProper_of_notMem (_ : w ∉ IF.I)

Premises used: Order.Ideal.isProper_of_notMem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
w : P
h : w ∈ (↑IF.F : Set P)
rwa rwa₁ rwa₂ rwa₃ : ∀ (h : w ∈ (↑IF.I : Set P)ᶜ), w ∉ IF.I
⊢ w ∉ IF.I

Tactic:
rwa [← IF.compl_I_eq_F] at h

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

Tactic:
IF.isCompl_I_F.disjoint

Premises used: Order.Ideal.PrimePair.isCompl_I_F, IsCompl.disjoint
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
⊢ (↑IF.I : Set P) ∪ (↑IF.F : Set P) = Set.univ

Tactic:
IF.isCompl_I_F.sup_eq_top

Premises used: IsCompl.sup_eq_top, Order.Ideal.PrimePair.isCompl_I_F
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
⊢ (↑IF.F : Set P) ∪ (↑IF.I : Set P) = Set.univ

Tactic:
IF.isCompl_I_F.symm.sup_eq_top

Premises used: IsCompl.sup_eq_top, Order.Ideal.PrimePair.isCompl_I_F, IsCompl.symm
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
rw : IsPFilter (↑IF.F : Set P)
⊢ IsPFilter (↑IF.I : Set P)ᶜ

Tactic:
rw [IF.compl_I_eq_F]

Premises used: Order.Ideal.PrimePair.compl_I_eq_F
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
⊢ IsPFilter (↑IF.F : Set P)

Tactic:
IF.F.isPFilter

Premises used: Order.Ideal.PrimePair.F, Order.PFilter.isPFilter
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : Preorder P
IF : PrimePair P
⊢ IsPFilter (↑IF.F : Set P)

Tactic:
exact IF.F.isPFilter

Premises used: Order.Ideal.PrimePair.F, Order.PFilter.isPFilter
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
hI : I.IsPrime
x y : P
contrapose! : x ∉ I ∧ y ∉ I → x ⊓ y ∉ I
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
contrapose!
-- Module: Mathlib.Order.PrimeIdeal
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)ᶜ) ⋯
change : x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
⊢ x ∉ I ∧ y ∉ I → x ⊓ y ∉ I

Tactic:
change x ∈ F ∧ y ∈ F → x ⊓ y ∈ F
-- Module: Mathlib.Order.PrimeIdeal
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 ∈ F ∧ y ∈ F → x ⊓ y ∈ F

Tactic:
fun h => inf_mem h.1 h.2

Premises used: Order.PFilter.inf_mem, And.right, And.left
-- Module: Mathlib.Order.PrimeIdeal
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 ∈ F ∧ y ∈ F → x ⊓ y ∈ F

Tactic:
exact fun h => inf_mem h.1 h.2

Premises used: Order.PFilter.inf_mem
-- Module: Mathlib.Order.PrimeIdeal
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
rw : I.IsProper ∧ IsPFilter (↑I : Set P)ᶜ
⊢ I.IsPrime

Tactic:
rw [isPrime_iff]

Premises used: Order.Ideal.isPrime_iff
-- Module: Mathlib.Order.PrimeIdeal
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 : IsPFilter (↑I : Set P)ᶜ
⊢ I.IsProper ∧ IsPFilter (↑I : Set P)ᶜ

Tactic:
use ‹_›
-- Module: Mathlib.Order.PrimeIdeal
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)ᶜ

Tactic:
.of_def ?_ ?_ ?_

Premises used: Order.IsPFilter.of_def
-- Module: Mathlib.Order.PrimeIdeal
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)ᶜ
right₂ : ∀ {x y : P}, x ≤ y → x ∈ (↑I : Set P)ᶜ → y ∈ (↑I : Set P)ᶜ
⊢ IsPFilter (↑I : Set P)ᶜ

Tactic:
refine .of_def ?_ ?_ ?_
-- Module: Mathlib.Order.PrimeIdeal
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 : Set P)ᶜ.Nonempty

Tactic:
Set.nonempty_compl.2 (I.isProper_iff.1 ‹_›)

Premises used: Iff.mpr, Order.Ideal.isProper_iff, Iff.mp, Set.nonempty_compl
-- Module: Mathlib.Order.PrimeIdeal
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 : Set P)ᶜ.Nonempty

Tactic:
exact Set.nonempty_compl.2 (I.isProper_iff.1 ‹_›)

Premises used: Iff.mpr, Order.Ideal.isProper_iff, Iff.mp, Set.nonempty_compl
-- Module: Mathlib.Order.PrimeIdeal
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
x : P
hx : x ∈ (↑I : Set P)ᶜ
y : P
hy : y ∈ (↑I : Set P)ᶜ
⊢ ∃ z ∈ (↑I : Set P)ᶜ, (fun (x1 x2 : P) ↦ x1 ≥ x2) x z ∧ (fun (x1 x2 : P) ↦ x1 ≥ x2) y z

Tactic:
⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩

Premises used: inf_le_right, And.intro, Exists.intro, inf_le_left, Or.elim, Min.min
-- Module: Mathlib.Order.PrimeIdeal
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
x : P
hx : x ∈ (↑I : Set P)ᶜ
y : P
hy : y ∈ (↑I : Set P)ᶜ
⊢ ∃ z ∈ (↑I : Set P)ᶜ, (fun (x1 x2 : P) ↦ x1 ≥ x2) x z ∧ (fun (x1 x2 : P) ↦ x1 ≥ x2) y z

Tactic:
exact ⟨x ⊓ y, fun h => (hI h).elim hx hy, inf_le_left, inf_le_right⟩
-- Module: Mathlib.Order.PrimeIdeal
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
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I : Set P)ᶜ → y ∈ (↑I : Set P)ᶜ

Tactic:
@mem_compl_of_ge _ _ _

Premises used: Order.Ideal.mem_compl_of_ge
-- Module: Mathlib.Order.PrimeIdeal
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
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I : Set P)ᶜ → y ∈ (↑I : Set P)ᶜ

Tactic:
exact @mem_compl_of_ge _ _ _

Premises used: Order.Ideal.mem_compl_of_ge
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : SemilatticeInf P
I : Ideal P
inst_1 : I.IsProper
⊢ I.IsPrime ↔ ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
⟨IsPrime.mem_or_mem, IsPrime.of_mem_or_mem⟩

Premises used: Iff.intro, Order.Ideal.IsPrime.mem_or_mem, Order.Ideal.IsPrime.of_mem_or_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
rw : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ I.IsPrime

Tactic:
rw [isPrime_iff_mem_or_mem]

Premises used: Order.Ideal.isPrime_iff_mem_or_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : DistribLattice P
I : Ideal P
inst_1 : I.IsMaximal
x y : P
contrapose! : x ∉ I ∧ y ∉ I → x ⊓ y ∉ I
⊢ x ⊓ y ∈ I → x ∈ I ∨ y ∈ I

Tactic:
contrapose!
-- Module: Mathlib.Order.PrimeIdeal
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
apply : y ∈ I
⊢ False

Tactic:
apply hynI
-- Module: Mathlib.Order.PrimeIdeal
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
⊢ (↑J : Set P) = Set.univ

Tactic:
have hJuniv : (J : Set P) = Set.univ :=
    IsMaximal.maximal_proper (lt_sup_principal_of_notMem ‹_›)
-- Module: Mathlib.Order.PrimeIdeal
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 ∈ (↑J : Set P)

Tactic:
have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y
-- Module: Mathlib.Order.PrimeIdeal
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)
⊢ 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

Premises used: Order.Ideal.coe_sup_eq
-- Module: Mathlib.Order.PrimeIdeal
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
rcases : ∀ (a : P) (ha : a ∈ I) (b : P) (hb : Membership.mem (γ := Ideal P) (principal x) b) (hy : y = a ⊔ b), y ∈ I
⊢ y ∈ I

Tactic:
rcases hyJ with ⟨a, ha, b, hb, hy⟩
-- Module: Mathlib.Order.PrimeIdeal
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
rw : a ⊔ b ∈ I
⊢ y ∈ I

Tactic:
rw [hy]
-- Module: Mathlib.Order.PrimeIdeal
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

Tactic:
sup_mem ha (I.lower (le_inf hb ?_) hxy)

Premises used: Order.Ideal.lower, Set.Mem, le_inf, Order.Ideal.sup_mem
-- Module: Mathlib.Order.PrimeIdeal
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
refine : b ≤ y
⊢ a ⊔ b ∈ I

Tactic:
refine sup_mem ha (I.lower (le_inf hb ?_) hxy)

Premises used: Order.Ideal.lower, le_inf, Order.Ideal.sup_mem
-- Module: Mathlib.Order.PrimeIdeal
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
rw : b ≤ a ⊔ b
⊢ b ≤ y

Tactic:
rw [hy]
-- Module: Mathlib.Order.PrimeIdeal
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 ≤ a ⊔ b

Tactic:
le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Order.PrimeIdeal
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 ≤ a ⊔ b

Tactic:
exact le_sup_right

Premises used: le_sup_right
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
apply : x ⊓ xᶜ ∈ I
⊢ x ∈ I ∨ xᶜ ∈ I

Tactic:
apply hI.mem_or_mem

Premises used: Order.Ideal.IsPrime.mem_or_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
rw : ⊥ ∈ I
⊢ x ⊓ xᶜ ∈ I

Tactic:
rw [inf_compl_eq_bot]

Premises used: inf_compl_eq_bot
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ ⊥ ∈ I

Tactic:
I.bot_mem

Premises used: Set.Mem, Order.Ideal.bot_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ ⊥ ∈ I

Tactic:
exact I.bot_mem

Premises used: Order.Ideal.bot_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
hxnI : x ∉ I
⊢ xᶜ ∈ I

Tactic:
hI.mem_or_compl_mem.resolve_left hxnI

Premises used: Or.resolve_left, Order.Ideal.IsPrime.mem_or_compl_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
I : Ideal P
inst_1 : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
simp : ∀ {x y : P}, x ⊓ y ∈ I → x ∉ I → y ∈ I
⊢ I.IsPrime

Tactic:
simp only [isPrime_iff_mem_or_mem, or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left, Order.Ideal.isPrime_iff_mem_or_mem
-- Module: Mathlib.Order.PrimeIdeal
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
⊢ xᶜ ∈ I

Tactic:
have hxcI : xᶜ ∈ I := h.resolve_left hxI
-- Module: Mathlib.Order.PrimeIdeal
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
⊢ x ⊓ y ⊔ y ⊓ xᶜ ∈ I

Tactic:
have ass : x ⊓ y ⊔ y ⊓ xᶜ ∈ I := sup_mem hxy (I.lower inf_le_right hxcI)
-- Module: Mathlib.Order.PrimeIdeal
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (ass : y ∈ I), y ∈ I
⊢ y ∈ I

Tactic:
rwa [inf_comm, sup_inf_inf_compl] at ass

Premises used: sup_inf_inf_compl, inf_comm
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
I : Ideal P
inst_1 : I.IsProper
⊢ I.IsPrime ↔ ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I

Tactic:
⟨fun h _ => h.mem_or_compl_mem, isPrime_of_mem_or_compl_mem⟩

Premises used: Order.Ideal.isPrime_of_mem_or_compl_mem, Iff.intro, Order.Ideal.IsPrime.mem_or_compl_mem
-- Module: Mathlib.Order.PrimeIdeal
Goal:
P : Type u_1
inst : BooleanAlgebra P
x : P
I : Ideal P
inst_1 : I.IsPrime
simp : ∀ ⦃J : Ideal P⦄, I < J → ∀ (x : P), x ∈ (↑J : Set P)
⊢ I.IsMaximal

Tactic:
simp only [isMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]

Premises used: Order.Ideal.IsPrime.toIsProper, Set.eq_univ_iff_forall, Order.Ideal.isMaximal_iff, true_and
-- 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 : P
rcases : ∀ (y : P) (hyJ : y ∈ (↑J : Set P)) (hyI : y ∉ (↑I : Set P)), x ∈ (↑J : Set P)
⊢ x ∈ (↑J : Set P)

Tactic:
rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩

Premises used: Set.exists_of_ssubset
-- 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)
ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J
rwa rwa₁ rwa₂ rwa₃ : ∀ (ass : x ∈ J), x ∈ (↑J : Set P)
⊢ x ∈ (↑J : Set P)

Tactic:
rwa [sup_inf_inf_compl] at ass

Premises used: sup_inf_inf_compl