awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a b_1 : WithTop { a : α // a ≠ ⊤ }
b : α
h : b ≠ ⊤
⊢ LE.le (α := α)
      (({ toFun := fun (a : WithTop { a : α // a ≠ ⊤ }) ↦ untopD ⊤ (map (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) a),
              invFun := fun (a : α) ↦
                if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : WithTop { a : α // a ≠ ⊤ }) → α)
          ⊤ :
        α)
      (({ toFun := fun (a : WithTop { a : α // a ≠ ⊤ }) ↦ untopD ⊤ (map (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) a),
              invFun := fun (a : α) ↦
                if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : WithTop { a : α // a ≠ ⊤ }) → α)
          (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) b h) : WithTop { a : α // a ≠ ⊤ }) :
        α) ↔
    LE.le (α := WithTop { a : α // a ≠ ⊤ }) ⊤
      (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) b h) : WithTop { a : α // a ≠ ⊤ })

Tactic:
simp [h]
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a_1 b a : WithTop { a : α // a ≠ ⊤ }
⊢ LE.le (α := α)
      (({ toFun := fun (a : WithTop { a : α // a ≠ ⊤ }) ↦ untopD ⊤ (map (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) a),
              invFun := fun (a : α) ↦
                if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : WithTop { a : α // a ≠ ⊤ }) → α)
          a :
        α)
      (({ toFun := fun (a : WithTop { a : α // a ≠ ⊤ }) ↦ untopD ⊤ (map (Subtype.val (p := fun (a : α) ↦ a ≠ ⊤)) a),
              invFun := fun (a : α) ↦
                if h : a = ⊤ then ⊤ else (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }),
              left_inv := ⋯, right_inv := ⋯ } :
            (a : WithTop { a : α // a ≠ ⊤ }) → α)
          ⊤ :
        α) ↔
    a ≤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : { a : α // a ≠ ⊤ }
⊢ (subtypeOrderIso : (a : WithTop { a : α // a ≠ ⊤ }) → α) (↑a : WithTop { a : α // a ≠ ⊤ }) = (↑a : α)

Tactic:
rfl

Premises used: WithTop.untopD, WithTop.recTopCoe, rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
h : a ≠ ⊤
rw :
  a =
    (subtypeOrderIso : (a : WithTop { a : α // a ≠ ⊤ }) → α)
      (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ })
⊢ Eq (α := WithTop { a : α // a ≠ ⊤ })
    ((OrderIso.symm subtypeOrderIso : (a : α) → WithTop { a : α // a ≠ ⊤ }) a : WithTop { a : α // a ≠ ⊤ })
    ((↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ }) : WithTop { a : α // a ≠ ⊤ })

Tactic:
rw [OrderIso.symm_apply_eq]

Premises used: OrderIso.symm_apply_eq
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : DecidablePred fun (x : α) ↦ x = ⊤
a : α
h : a ≠ ⊤
⊢ a =
    (subtypeOrderIso : (a : WithTop { a : α // a ≠ ⊤ }) → α)
      (↑(Subtype.mk (p := fun (a : α) ↦ a ≠ ⊤) a h) : WithTop { a : α // a ≠ ⊤ })

Tactic:
rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq (α := WithTop α ≃o WithTop α) (withTopCongr (refl α)) (refl (WithTop α))

Tactic:
RelIso.toEquiv_injective Equiv.withTopCongr_refl

Premises used: RelIso.toEquiv_injective, Equiv.withTopCongr_refl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
e : α ≃o β
⊢ e.symm.withTopCongr = e.withTopCongr.symm

Tactic:
RelIso.toEquiv_injective e.toEquiv.withTopCongr_symm

Premises used: RelIso.toEquiv_injective, Equiv.withTopCongr_symm, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : PartialOrder γ
e₁ : α ≃o β
e₂ : β ≃o γ
⊢ (e₁.trans e₂).withTopCongr = e₁.withTopCongr.trans e₂.withTopCongr

Tactic:
RelIso.toEquiv_injective <| e₁.toEquiv.withTopCongr_trans e₂.toEquiv

Premises used: RelIso.toEquiv_injective, Equiv.withTopCongr_trans, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : PartialOrder α
⊢ Eq (α := WithBot α ≃o WithBot α) (withBotCongr (refl α)) (refl (WithBot α))

Tactic:
RelIso.toEquiv_injective Equiv.withBotCongr_refl

Premises used: RelIso.toEquiv_injective, Equiv.withBotCongr_refl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
e : α ≃o β
⊢ e.symm.withBotCongr = e.withBotCongr.symm

Tactic:
RelIso.toEquiv_injective e.toEquiv.withBotCongr_symm

Premises used: RelIso.toEquiv_injective, Equiv.withBotCongr_symm, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : PartialOrder γ
e₁ : α ≃o β
e₂ : β ≃o γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr

Tactic:
RelIso.toEquiv_injective <| e₁.toEquiv.withBotCongr_trans e₂.toEquiv

Premises used: RelIso.toEquiv_injective, Equiv.withBotCongr_trans, RelIso.toEquiv
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : SemilatticeSup α
⊢ Eq (α := SupHom (WithTop α) (WithTop α)) (SupHom.withTop (SupHom.id α)) (SupHom.id (WithTop α))

Tactic:
DFunLike.coe_injective WithTop.map_id

Premises used: WithTop.map_id, DFunLike.coe_injective
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : SemilatticeSup γ
f : SupHom β γ
g : SupHom α β
⊢ (f.comp g).withTop = f.withTop.comp g.withTop

Tactic:
DFunLike.coe_injective <| Eq.symm <| WithTop.map_comp_map _ _

Premises used: WithTop.map_comp_map, DFunLike.coe_injective, Eq.symm
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : SemilatticeSup α
⊢ Eq (α := SupBotHom (WithBot α) (WithBot α)) (SupHom.withBot (SupHom.id α)) (SupBotHom.id (WithBot α))

Tactic:
DFunLike.coe_injective WithBot.map_id

Premises used: DFunLike.coe_injective, WithBot.map_id
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
inst_2 : SemilatticeSup γ
f : SupHom β γ
g : SupHom α β
⊢ (f.comp g).withBot = f.withBot.comp g.withBot

Tactic:
DFunLike.coe_injective <| Eq.symm <| WithBot.map_comp_map _ _

Premises used: WithBot.map_comp_map, DFunLike.coe_injective, Eq.symm
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ Eq (α := (a : WithTop α) → WithTop β) (⇑f.withTop : (a : WithTop α) → WithTop β) (WithTop.map (⇑f : (a : α) → β))

Tactic:
rfl

Premises used: WithTop.map, rfl, WithTop
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
a : WithTop α
⊢ Eq.{u_2 + 1} (α := WithTop β) ((f.withTop : (a : WithTop α) → WithTop β) a : WithTop β)
    (WithTop.map (⇑f : (a : α) → β) a : WithTop β)

Tactic:
rfl

Premises used: WithTop.map, rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : Lattice α
⊢ Eq (α := LatticeHom (WithTop α) (WithTop α)) (LatticeHom.withTop (LatticeHom.id α)) (LatticeHom.id (WithTop α))

Tactic:
DFunLike.coe_injective WithTop.map_id

Premises used: WithTop.map_id, DFunLike.coe_injective
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
⊢ (f.comp g).withTop = f.withTop.comp g.withTop

Tactic:
DFunLike.coe_injective <| Eq.symm <| WithTop.map_comp_map _ _

Premises used: WithTop.map_comp_map, DFunLike.coe_injective, Eq.symm
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
⊢ Eq (α := (a : WithTop (WithBot α)) → WithTop (WithBot β))
    (⇑f.withTopWithBot : (a : WithTop (WithBot α)) → WithTop (WithBot β)) (WithTop.map (WithBot.map (⇑f : (a : α) → β)))

Tactic:
rfl

Premises used: WithTop.map, WithBot.map, rfl, WithTop
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Lattice β
f : LatticeHom α β
a : WithTop (WithBot α)
⊢ Eq.{u_2 + 1} (α := WithTop (WithBot β))
    ((f.withTopWithBot : (a : WithTop (WithBot α)) → WithTop (WithBot β)) a : WithTop (WithBot β))
    (WithTop.map (WithBot.map (⇑f : (a : α) → β)) a : WithTop (WithBot β))

Tactic:
rfl

Premises used: WithTop.map, WithBot.map, rfl
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
inst : Lattice α
⊢ Eq.{u_1 + 1} (α := (a : WithTop (WithBot α)) → WithTop (WithBot α))
    ((fun (f : BoundedLatticeHom (WithTop (WithBot α)) (WithTop (WithBot α))) ↦
        ((⇑f : (a : WithTop (WithBot α)) → WithTop (WithBot α)) : (a : WithTop (WithBot α)) → WithTop (WithBot α)))
      (withTopWithBot (LatticeHom.id α)))
    ((fun (f : BoundedLatticeHom (WithTop (WithBot α)) (WithTop (WithBot α))) ↦
        ((⇑f : (a : WithTop (WithBot α)) → WithTop (WithBot α)) : (a : WithTop (WithBot α)) → WithTop (WithBot α)))
      (BoundedLatticeHom.id (WithTop (WithBot α))))

Tactic:
simp [WithTop.map_id, WithBot.map_id]

Premises used: WithTop.map_id, WithBot.map_id
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
h :
  ∀ (a : WithTop (WithBot α)),
    Eq.{u_3 + 1} (α := WithTop (WithBot γ))
      (((f.comp g).withTopWithBot : (a : WithTop (WithBot α)) → WithTop (WithBot γ)) a : WithTop (WithBot γ))
      ((f.withTopWithBot.comp g.withTopWithBot : (a : WithTop (WithBot α)) → WithTop (WithBot γ)) a :
        WithTop (WithBot γ))
⊢ (f.comp g).withTopWithBot = f.withTopWithBot.comp g.withTopWithBot

Tactic:
ext
-- Module: Mathlib.Order.Hom.WithTopBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Lattice α
inst_1 : Lattice β
inst_2 : Lattice γ
f : LatticeHom β γ
g : LatticeHom α β
a : WithTop (WithBot α)
⊢ Eq.{u_3 + 1} (α := WithTop (WithBot γ))
    (((f.comp g).withTopWithBot : (a : WithTop (WithBot α)) → WithTop (WithBot γ)) a : WithTop (WithBot γ))
    ((f.withTopWithBot.comp g.withTopWithBot : (a : WithTop (WithBot α)) → WithTop (WithBot γ)) a : WithTop (WithBot γ))

Tactic:
simp
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s t : Ideal P
h : s.toLowerSet = t.toLowerSet
mk :
  ∀ (toLowerSet : LowerSet P) (nonempty' : toLowerSet.carrier.Nonempty)
    (directed' : DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) toLowerSet.carrier),
    { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P }.toLowerSet = t.toLowerSet →
      { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P } = t
⊢ s = t

Tactic:
cases s
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
t : Ideal P
toLowerSet : LowerSet P
nonempty' : toLowerSet.carrier.Nonempty
directed' : DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) toLowerSet.carrier
h : { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P }.toLowerSet = t.toLowerSet
mk :
  ∀ (toLowerSet_1 : LowerSet P) (nonempty'_1 : toLowerSet_1.carrier.Nonempty)
    (directed'_1 : DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) toLowerSet_1.carrier),
    { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P }.toLowerSet =
        { toLowerSet := toLowerSet_1, nonempty' := nonempty'_1, directed' := directed'_1 }.toLowerSet →
      { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P } =
        { toLowerSet := toLowerSet_1, nonempty' := nonempty'_1, directed' := directed'_1 }
⊢ { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P } = t

Tactic:
cases t
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
toLowerSet : LowerSet P
nonempty' : toLowerSet.carrier.Nonempty
directed' : DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) toLowerSet.carrier
toLowerSet_1 : LowerSet P
nonempty'_1 : toLowerSet_1.carrier.Nonempty
directed'_1 : DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) toLowerSet_1.carrier
h :
  { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P }.toLowerSet =
    { toLowerSet := toLowerSet_1, nonempty' := nonempty'_1, directed' := directed'_1 }.toLowerSet
⊢ { toLowerSet := toLowerSet, nonempty' := nonempty', directed' := directed' : Ideal P } =
    { toLowerSet := toLowerSet_1, nonempty' := nonempty'_1, directed' := directed'_1 }

Tactic:
congr
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s t : Ideal P
⊢ (↑s : Set P) = (↑t : Set P) → s = t

Tactic:
SetLike.ext'

Premises used: SetLike.ext'
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s : Ideal P
⊢ s.carrier = (↑s : Set P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s : Ideal P
⊢ (↑s.toLowerSet : Set P) = (↑s : Set P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s : Ideal P
⊢ IsLowerSet (↑s : Set P)

Tactic:
s.lower'

Premises used: Order.Ideal.toLowerSet, LowerSet.lower'
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s : Ideal P
⊢ (↑s : Set P).Nonempty

Tactic:
s.nonempty'

Premises used: Order.Ideal.nonempty'
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s : Ideal P
⊢ DirectedOn (fun (x1 x2 : P) ↦ x1 ≤ x2) (↑s : Set P)

Tactic:
s.directed'

Premises used: Order.Ideal.directed'
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s : Ideal P
⊢ IsIdeal (↑s : Set P)

Tactic:
⟨s.lower, s.nonempty, s.directed⟩

Premises used: Order.IsIdeal.mk, Order.Ideal.lower, Order.Ideal.directed, Order.Ideal.nonempty
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Ideal P
x y : P
⊢ x ≤ y → x ∈ (↑I : Set P)ᶜ → y ∈ (↑I : Set P)ᶜ

Tactic:
fun h ↦
  mt <| I.lower h

Premises used: Order.Ideal.lower, Set.Mem, setOf, mt, Not
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s t : Ideal P
⊢ (↑s : Set P) ⊆ (↑t : Set P) ↔ s ≤ t

Tactic:
Iff.rfl

Premises used: Iff.rfl, Set.Subset
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
s t : Ideal P
⊢ (↑s : Set P) ⊂ (↑t : Set P) ↔ s < t

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
x : P
I J : Ideal P
⊢ x ∈ I → I ≤ J → x ∈ J

Tactic:
@Set.mem_of_mem_of_subset P x I J

Premises used: Set.Subset, Set.mem_of_mem_of_subset
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Set P
h : IsIdeal I
a : P
⊢ a ∈ h.toIdeal (I := I) ↔ a ∈ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Set P
h : IsIdeal I
⊢ (↑(h.toIdeal (I := I)) : Set P) = I

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Set P
h : IsIdeal I
J : Ideal P
⊢ h.toIdeal (I := I) ≤ J ↔ I ⊆ (↑J : Set P)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Set.Subset
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Set P
h : IsIdeal I
J : Ideal P
⊢ J ≤ h.toIdeal (I := I) ↔ (↑J : Set P) ⊆ I

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, Set.Subset
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Ideal P
p : P
notMem : p ∉ I
hp : (↑I : Set P) = univ
⊢ Membership.mem (γ := Set P) univ p

Tactic:
have := mem_univ p
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Ideal P
p : P
notMem : p ∉ I
hp : (↑I : Set P) = univ
this : Membership.mem (γ := Set P) univ p
⊢ p ∈ (↑I : Set P)

Tactic:
rw [← hp] at this
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Ideal P
p : P
notMem : p ∉ I
hp : (↑I : Set P) = univ
this : p ∈ (↑I : Set P)
⊢ False

Tactic:
notMem this
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
I : Ideal P
p : P
notMem : p ∉ I
hp : (↑I : Set P) = univ
this : p ∈ (↑I : Set P)
⊢ False

Tactic:
exact notMem this
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsCodirectedOrder P
I J : Ideal P
obtain : ∀ (a : P) (ha : a ∈ (↑I : Set P)), ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
⊢ ((↑I : Set P) ∩ (↑J : Set P)).Nonempty

Tactic:
obtain ⟨a, ha⟩ := I.nonempty

Premises used: Order.Ideal.nonempty
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ (↑I : Set P)
obtain : ∀ (b : P) (hb : b ∈ (↑J : Set P)), ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
⊢ ((↑I : Set P) ∩ (↑J : Set P)).Nonempty

Tactic:
obtain ⟨b, hb⟩ := J.nonempty

Premises used: Order.Ideal.nonempty
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ (↑I : Set P)
b : P
hb : b ∈ (↑J : Set P)
obtain : ∀ (c : P) (hac : c ≤ a) (hbc : c ≤ b), ((↑I : Set P) ∩ (↑J : Set P)).Nonempty
⊢ ((↑I : Set P) ∩ (↑J : Set P)).Nonempty

Tactic:
obtain ⟨c, hac, hbc⟩ := exists_le_le a b

Premises used: exists_le_le
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ (↑I : Set P)
b : P
hb : b ∈ (↑J : Set P)
c : P
hac : c ≤ a
hbc : c ≤ b
⊢ ((↑I : Set P) ∩ (↑J : Set P)).Nonempty

Tactic:
⟨c, I.lower hac ha, J.lower hbc hb⟩

Premises used: Order.Ideal.lower, Set.Nonempty, And.intro, Exists.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ (↑I : Set P)
b : P
hb : b ∈ (↑J : Set P)
c : P
hac : c ≤ a
hbc : c ≤ b
⊢ ((↑I : Set P) ∩ (↑J : Set P)).Nonempty

Tactic:
exact ⟨c, I.lower hac ha, J.lower hbc hb⟩
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
⊢ Eq.{u_1 + 1} (α := LowerSet P) (toLowerSet ⊤) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
⊢ (↑⊤ : Set P) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
I : Ideal P
ne_top : I ≠ ⊤
⊢ I.IsProper

Tactic:
⟨fun h ↦ ne_top <| ext h⟩

Premises used: Order.Ideal.ext, Order.Ideal.IsProper.mk
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
I : Ideal P
h : I.IsProper
⊢ I ≠ ⊤

Tactic:
fun h ↦ IsProper.ne_univ <| congr_arg SetLike.coe h

Premises used: Order.Ideal.IsProper.ne_univ, congr_arg, SetLike.coe, Not
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
I : Ideal P
hI : IsCoatom I
⊢ I.IsProper

Tactic:
isProper_of_ne_top hI.1

Premises used: Order.Ideal.isProper_of_ne_top, And.left
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
I : Ideal P
⊢ I.IsProper ↔ I ≠ ⊤

Tactic:
⟨fun h ↦ h.ne_top, fun h ↦ isProper_of_ne_top h⟩

Premises used: Order.Ideal.isProper_of_ne_top, Order.Ideal.IsProper.ne_top, Iff.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
I : Ideal P
h : I.IsMaximal
⊢ IsCoatom I

Tactic:
⟨IsMaximal.toIsProper.ne_top, fun _ h ↦ ext <| IsMaximal.maximal_proper h⟩

Premises used: Order.Ideal.ext, Order.Ideal.IsMaximal.toIsProper, Order.Ideal.IsMaximal.maximal_proper, Order.Ideal.IsProper.ne_top, IsCoatom, And.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
I : Ideal P
inst_3 : I.IsMaximal
⊢ IsCoatom I

Tactic:
IsMaximal.isCoatom ‹_›

Premises used: Order.Ideal.IsMaximal.isCoatom
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
I : Ideal P
hI : IsCoatom I
x : Ideal P
hJ : I < x
⊢ (↑x : Set P) = univ

Tactic:
simp [hI.2 _ hJ]

Premises used: And.right
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : IsDirectedOrder P
inst_2 : Nonempty P
I : Ideal P
⊢ I.IsMaximal ↔ IsCoatom I

Tactic:
⟨fun h ↦ h.isCoatom, fun h ↦ IsCoatom.isMaximal h⟩

Premises used: Iff.intro, IsCoatom.isMaximal, Order.Ideal.IsMaximal.isCoatom
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderBot P
s : Ideal P
⊢ ⊥ ∈ s

Tactic:
s.lower bot_le s.nonempty'.some_mem

Premises used: Order.Ideal.lower, Order.Ideal.nonempty', Set.Nonempty.some_mem, bot_le
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
⊢ ⊤ ∈ I ↔ I = ⊤

Tactic:
⟨fun h => SetLike.ext fun _ => iff_of_true (I.lower le_top h) ⟨⟩, fun h => h ▸ mem_univ _⟩

Premises used: Order.Ideal.lower, Eq.rec, iff_of_true, le_top, Iff.intro, SetLike.ext, Set.mem_univ, Top.top, Eq.symm, True.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
⊢ ⊤ ∉ I ↔ I ≠ ⊤

Tactic:
top_mem_iff_eq_top.not

Premises used: Order.Ideal.top_mem_iff_eq_top, Iff.not
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : LE P
inst_1 : OrderTop P
I : Ideal P
rw : I ≠ ⊤ ↔ ⊤ ∉ I
rw₁ : ¬I = ⊤ ↔ ⊤ ∉ I
rw₂ rw₃ : ¬I = ⊤ ↔ ¬I = ⊤
⊢ I.IsProper ↔ ⊤ ∉ I

Tactic:
rw [isProper_iff_ne_top, ne_eq, top_mem_iff_eq_top]

Premises used: Order.Ideal.top_mem_iff_eq_top, Order.Ideal.isProper_iff_ne_top, ne_eq
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
I : Ideal P
x : P
⊢ principal x ≤ I ↔ x ∈ I

Tactic:
⟨fun h ↦ h le_rfl, fun hx _ hy ↦ I.lower hy hx⟩

Premises used: le_rfl, Order.Ideal.lower, Iff.intro
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
x y : P
⊢ Membership.mem (γ := Ideal P) (principal y) x ↔ x ≤ y

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Iic
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
x : P
⊢ Membership.mem (γ := Ideal P) (principal x) x

Tactic:
mem_principal.2 (le_refl x)

Premises used: Iff.mpr, le_refl, Order.Ideal.mem_principal
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
inst_1 : OrderBot P
⊢ ∀ (a : Ideal P), principal ⊥ ≤ a

Tactic:
simp
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
inst_1 : OrderBot P
⊢ Eq.{u_1 + 1} (α := Ideal P) (principal ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : Preorder P
inst_1 : OrderTop P
⊢ Eq.{u_1 + 1} (α := Ideal P) (principal ⊤) ⊤

Tactic:
toLowerSet_injective <| LowerSet.Iic_top

Premises used: LowerSet.Iic_top, Order.Ideal.toLowerSet_injective
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : PartialOrder P
inst_1 : OrderTop P
a : P
rw : ⊤ ∉ principal a ↔ a ≠ ⊤
rw₁ : ¬⊤ ≤ a ↔ a ≠ ⊤
rw₂ rw₃ : ¬a = ⊤ ↔ a ≠ ⊤
⊢ IsProper (principal a) ↔ a ≠ ⊤

Tactic:
rw [isProper_iff_top_notMem, mem_principal, top_le_iff]

Premises used: Order.Ideal.isProper_iff_top_notMem, Order.Ideal.mem_principal, top_le_iff
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
x y : P
s : Ideal P
hx : x ∈ s
hy : y ∈ s
⊢ x ⊔ y ∈ s

Tactic:
let ⟨_, hz, hx, hy⟩ := s.directed x hx y hy
  s.lower (sup_le hx hy) hz

Premises used: Order.Ideal.lower, Membership.mem, Order.Ideal.directed, Max.max, sup_le, _private.0.Order.Ideal.sup_mem.match_1
-- Module: Mathlib.Order.Ideal
Goal:
P : Type u_1
inst : SemilatticeSup P
x y : P
I : Ideal P
⊢ x ⊔ y ∈ I ↔ x ∈ I ∧ y ∈ I

Tactic:
⟨fun h ↦ ⟨I.lower le_sup_left h, I.lower le_sup_right h⟩, fun h ↦ sup_mem h.1 h.2⟩

Premises used: Order.Ideal.lower, le_sup_left, le_sup_right, And.right, And.left, And.intro, Iff.intro, Order.Ideal.sup_mem