awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
refine :
  ∀ (x : (↑s : Type u_2) × (↑s : Type u_2)) (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    x ∉ t →
      ∀
        (ih :
          ∀
            (hx :
              Membership.mem (γ := BooleanSubalgebra α) (closure s)
                (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
            p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx)
        (hxt :
          Membership.mem (γ := BooleanSubalgebra α) (closure s)
            ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
        p ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hxt
⊢ ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx

Tactic:
refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
x : (↑s : Type u_2) × (↑s : Type u_2)
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
h : x ∉ t
ih :
  ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
hxt :
  Membership.mem (γ := BooleanSubalgebra α) (closure s)
    ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
simp :
  ∀
    (hxt_1 :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) ⋯
⊢ p ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hxt

Tactic:
simp only [Finset.sup_insert] at hxt ⊢

Premises used: Finset.sup_insert
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
x : (↑s : Type u_2) × (↑s : Type u_2)
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
h : x ∉ t
ih :
  ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
hxt_1 :
  Membership.mem (γ := BooleanSubalgebra α) (closure s)
    ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
hxt :
  Membership.mem (γ := BooleanSubalgebra α) (closure s)
    ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
⊢ p ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) ⋯

Tactic:
sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
    (sdiff _ x.1.2 _ x.2.2) (ih _)

Premises used: Iff.mpr, BooleanSubalgebra.mem_closure_iff_sup_sdiff, Prod.fst, Exists.intro, Prod.snd, rfl, Subtype.property
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
x : (↑s : Type u_2) × (↑s : Type u_2)
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
h : x ∉ t
ih :
  ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
hxt_1 :
  Membership.mem (γ := BooleanSubalgebra α) (closure s)
    ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
hxt :
  Membership.mem (γ := BooleanSubalgebra α) (closure s)
    ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
⊢ p ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) ⋯

Tactic:
exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
    (sdiff _ x.1.2 _ x.2.2) (ih _)

Premises used: Iff.mpr, BooleanSubalgebra.mem_closure_iff_sup_sdiff, Prod.fst, Exists.intro, Prod.snd, rfl, Subtype.property
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
refine :
  ∀ (x : (↑s : Type u_2) × (↑s : Type u_2)) (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    x ∉ t →
      ∀
        (ih :
          ∀
            (hx :
              Membership.mem (γ := BooleanSubalgebra α) (closure s)
                (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
            p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx)
        (hxt :
          Membership.mem (γ := BooleanSubalgebra α) (closure s)
            ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
        p ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hxt
refine₁ :
  ∀ (x : (↑s : Type u_2) × (↑s : Type u_2)) (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    x ∉ t →
      ∀
        (ih :
          ∀
            (hx :
              Membership.mem (γ := BooleanSubalgebra α) (closure s)
                (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
            p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx)
        (hxt :
          Membership.mem (γ := BooleanSubalgebra α) (closure s)
            ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)))
        (hxt_1 :
          Membership.mem (γ := BooleanSubalgebra α) (closure s)
            ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
        p ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) ⋯
⊢ ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx

Tactic:
classical
  refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
  simp only [Finset.sup_insert] at hxt ⊢
  exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
    (sdiff _ x.1.2 _ x.2.2) (ih _)

Premises used: Finset.sup_insert
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteBooleanAlgebra α
L : BooleanSubalgebra α
f : ι → α
inst_1 : Finite ι
hf : ∀ (i : ι), f i ∈ L
⊢ ⨆ (i : ι), f i ∈ L

Tactic:
L.supClosed.iSup_mem bot_mem hf

Premises used: SupClosed.iSup_mem, BooleanSubalgebra.bot_mem, BooleanSubalgebra.supClosed
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteBooleanAlgebra α
L : BooleanSubalgebra α
f : ι → α
inst_1 : Finite ι
hf : ∀ (i : ι), f i ∈ L
⊢ ⨅ (i : ι), f i ∈ L

Tactic:
L.infClosed.iInf_mem top_mem hf

Premises used: BooleanSubalgebra.top_mem, BooleanSubalgebra.infClosed, InfClosed.iInf_mem
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : CompleteBooleanAlgebra α
L : BooleanSubalgebra α
s : Set α
hs : s.Finite
hsL : s ⊆ (↑L : Set α)
⊢ sSup s ∈ L

Tactic:
L.supClosed.sSup_mem hs bot_mem hsL

Premises used: SupClosed.sSup_mem, BooleanSubalgebra.bot_mem, BooleanSubalgebra.supClosed
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : CompleteBooleanAlgebra α
L : BooleanSubalgebra α
s : Set α
hs : s.Finite
hsL : s ⊆ (↑L : Set α)
⊢ sInf s ∈ L

Tactic:
L.infClosed.sInf_mem hs top_mem hsL

Premises used: BooleanSubalgebra.top_mem, BooleanSubalgebra.infClosed, InfClosed.sInf_mem
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : CompleteBooleanAlgebra α
L : BooleanSubalgebra α
ι : Type u_5
t : Set ι
f : ι → α
ht : t.Finite
hf : ∀ i ∈ t, f i ∈ L
⊢ ⨆ i ∈ t, f i ∈ L

Tactic:
L.supClosed.biSup_mem ht bot_mem hf

Premises used: SupClosed.biSup_mem, BooleanSubalgebra.bot_mem, BooleanSubalgebra.supClosed
-- Module: Mathlib.Order.BooleanSubalgebra
Goal:
α : Type u_2
inst : CompleteBooleanAlgebra α
L : BooleanSubalgebra α
ι : Type u_5
t : Set ι
f : ι → α
ht : t.Finite
hf : ∀ i ∈ t, f i ∈ L
⊢ ⨅ i ∈ t, f i ∈ L

Tactic:
L.infClosed.biInf_mem ht top_mem hf

Premises used: BooleanSubalgebra.top_mem, BooleanSubalgebra.infClosed, InfClosed.biInf_mem
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
a : α
⊢ (lift a)ᶜ = comp a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
a : α
⊢ (comp a)ᶜ = lift a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
h : a ≤ b
⊢ a ≤ b

Tactic:
assumption
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
h : b ≤ a
⊢ b ≤ a

Tactic:
assumption
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
h : Disjoint a b
⊢ Disjoint a b

Tactic:
assumption
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ ¬comp a ≤ lift b

Tactic:
fun h ↦ nomatch h

Premises used: _private.0.Booleanisation.not_comp_le_lift.match_1, False, Not
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
h : a < b
⊢ a < b

Tactic:
assumption
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
h : b < a
⊢ b < a

Tactic:
assumption
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ ¬comp a < lift b

Tactic:
fun h ↦ nomatch h

Premises used: False, _private.0.Booleanisation.not_comp_lt_lift.match_1, Not
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a ⊔ lift b = lift (a ⊔ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a ⊔ comp b = comp (b \ a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a ⊔ lift b = comp (a \ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a ⊔ comp b = comp (a ⊓ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a ⊓ lift b = lift (a ⊓ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a ⊓ comp b = lift (a \ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a ⊓ lift b = lift (b \ a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a ⊓ comp b = comp (a ⊔ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
⊢ Eq.{u_1 + 1} (α := Booleanisation α) (lift ⊥) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
⊢ Eq.{u_1 + 1} (α := Booleanisation α) (comp ⊥) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a \ lift b = lift (a \ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a \ comp b = lift (a ⊓ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a \ lift b = comp (a ⊔ b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a \ comp b = lift (b \ a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
⊢ lift a < lift b ↔ lift a ≤ lift b ∧ ¬lift b ≤ lift a

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
⊢ lift a < comp b ↔ lift a ≤ comp b ∧ ¬comp b ≤ lift a

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
⊢ comp a < lift b ↔ comp a ≤ lift b ∧ ¬lift b ≤ comp a

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
⊢ comp a < comp b ↔ comp a ≤ comp b ∧ ¬comp b ≤ comp a

Tactic:
simp [lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
hab : a ≤ b
hba : b ≤ a
rw rw₁ : lift b = lift b
⊢ lift a = lift b

Tactic:
rw [hab.antisymm hba]

Premises used: LE.le.antisymm
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
hab : b ≤ a
hba : a ≤ b
rw rw₁ : comp a = comp a
⊢ comp a = comp b

Tactic:
rw [hab.antisymm hba]

Premises used: LE.le.antisymm
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
⊢ (a ⊔ b) \ (c \ a) ≤ a ⊔ b \ c

Tactic:
simp [sup_comm, sup_assoc]

Premises used: sup_assoc, sup_comm
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
⊢ (a ⊔ c) \ (b \ a) ≤ a ⊔ c \ b

Tactic:
simp [sup_left_comm (a := b \ a), sup_comm (a := b \ a)]

Premises used: SDiff.sdiff, sup_comm, sup_left_comm
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
rw rw₁ : b \ a ⊔ c \ a ≤ b \ a ⊔ c \ a
⊢ (b ⊔ c) \ a ≤ b \ a ⊔ c \ a

Tactic:
rw [sup_sdiff]

Premises used: sup_sdiff
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
rw rw₁ : a \ b ⊔ a \ c ≤ a \ b ⊔ a \ c
⊢ a \ (b ⊓ c) ≤ a \ b ⊔ a \ c

Tactic:
rw [sdiff_inf]

Premises used: sdiff_inf
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
rw rw₁ : a \ b ⊔ a ⊓ c ≤ a \ b ⊔ a ⊓ c
⊢ a \ (b \ c) ≤ a \ b ⊔ a ⊓ c

Tactic:
rw [sdiff_sdiff_right']

Premises used: sdiff_sdiff_right'
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
rw : a \ c ⊔ a ⊓ b ≤ a ⊓ b ⊔ a \ c
rw₁ rw₂ : a ⊓ b ⊔ a \ c ≤ a ⊓ b ⊔ a \ c
⊢ a \ (c \ b) ≤ a ⊓ b ⊔ a \ c

Tactic:
rw [sdiff_sdiff_right', sup_comm]

Premises used: sup_comm, sdiff_sdiff_right'
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b a : α
⊢ lift a ⊓ (lift a)ᶜ ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b a : α
⊢ comp a ⊓ (comp a)ᶜ ≤ ⊥

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b a : α
⊢ ⊤ ≤ lift a ⊔ (lift a)ᶜ

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b a : α
⊢ ⊤ ≤ comp a ⊔ (comp a)ᶜ

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
⊢ lift a \ lift b = lift a ⊓ (lift b)ᶜ

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
⊢ lift a \ comp b = lift a ⊓ (comp b)ᶜ

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
⊢ comp a \ lift b = comp a ⊓ (lift b)ᶜ

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
⊢ comp a \ comp b = comp a ⊓ (comp b)ᶜ

Tactic:
simp
-- Module: Mathlib.Order.Booleanisation
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (β := Booleanisation α) (⇑liftLatticeHom : (a : α) → Booleanisation α)

Tactic:
Sum.inl_injective

Premises used: Booleanisation.lift, Sum.inl_injective, Booleanisation
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hst : s ⊆ t
hs : Bounded r t
⊢ Bounded r s

Tactic:
hs.imp fun _ ha b hb => ha b (hst hb)

Premises used: Set.Bounded, Exists.imp
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
hst : s ⊆ t
hs : Unbounded r s
⊢ Unbounded r t

Tactic:
fun a =>
  let ⟨b, hb, hb'⟩ := hs a
  ⟨b, hst hb, hb'⟩

Premises used: _private.0.Set.Unbounded.mono.match_1, Membership.mem, Exists, And, And.intro, Set.Unbounded, Exists.intro, Not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h : ∀ (a : α), ∃ (b : α), b ∈ s ∧ a < b
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
fun a =>
  let ⟨b, hb, hb'⟩ := h a
  ⟨b, hb, fun hba => hba.not_gt hb'⟩

Premises used: _private.0.Set.unbounded_le_of_forall_exists_lt.match_1, Membership.mem, Exists, LE.le, And, LE.le.not_gt, And.intro, Set.Unbounded, Exists.intro, Not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ ∀ (a : α), ∃ (b : α), b ∈ s ∧ a < b

Tactic:
simp only [Unbounded, not_le]

Premises used: not_le, Set.Unbounded
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h : ∀ (a : α), ∃ (b : α), b ∈ s ∧ a ≤ b
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
fun a =>
  let ⟨b, hb, hb'⟩ := h a
  ⟨b, hb, fun hba => hba.not_ge hb'⟩

Premises used: Membership.mem, Exists, And, _private.0.Set.unbounded_lt_of_forall_exists_le.match_1, And.intro, LT.lt, Set.Unbounded, Exists.intro, LT.lt.not_ge, Not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s ↔ ∀ (a : α), ∃ (b : α), b ∈ s ∧ a ≤ b

Tactic:
simp only [Unbounded, not_lt]

Premises used: not_lt, Set.Unbounded
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h : ∀ (a : α), ∃ (b : α), b ∈ s ∧ b < a
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s

Tactic:
@unbounded_le_of_forall_exists_lt αᵒᵈ _ _ h

Premises used: Set.unbounded_le_of_forall_exists_lt, OrderDual
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≥ x2) s ↔ ∀ (a : α), ∃ (b : α), b ∈ s ∧ b < a

Tactic:
⟨fun h a =>
    let ⟨b, hb, hba⟩ := h a
    ⟨b, hb, lt_of_not_ge hba⟩,
    unbounded_ge_of_forall_exists_gt⟩

Premises used: lt_of_not_ge, Membership.mem, Exists, And, And.intro, LT.lt, Iff.intro, Exists.intro, Set.unbounded_ge_of_forall_exists_gt, _private.0.Set.unbounded_ge_iff.match_1
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h : ∀ (a : α), ∃ (b : α), b ∈ s ∧ b ≤ a
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) s

Tactic:
fun a =>
  let ⟨b, hb, hb'⟩ := h a
  ⟨b, hb, fun hba => not_le_of_gt hba hb'⟩

Premises used: Membership.mem, Exists, GT.gt, And, _private.0.Set.unbounded_gt_of_forall_exists_ge.match_1, And.intro, Set.Unbounded, Exists.intro, not_le_of_gt, Not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 > x2) s ↔ ∀ (a : α), ∃ (b : α), b ∈ s ∧ b ≤ a

Tactic:
⟨fun h a =>
    let ⟨b, hb, hba⟩ := h a
    ⟨b, hb, le_of_not_gt hba⟩,
    unbounded_gt_of_forall_exists_ge⟩

Premises used: Membership.mem, Exists, le_of_not_gt, LE.le, _private.0.Set.unbounded_gt_iff.match_1, And, Set.unbounded_gt_of_forall_exists_ge, And.intro, Iff.intro, Exists.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
r' : α → α → Prop
h : Bounded r s
hrr' : r ≤ r'
⊢ Bounded r' s

Tactic:
let ⟨a, ha⟩ := h
  ⟨a, fun b hb => hrr' b a (ha b hb)⟩

Premises used: Set.Bounded, _private.0.Set.Bounded.rel_mono.match_1, Exists.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h : Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s

Tactic:
h.rel_mono fun _ _ => le_of_lt

Premises used: le_of_lt, Set.Bounded.rel_mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
r' : α → α → Prop
hr : r' ≤ r
h : Unbounded r s
⊢ Unbounded r' s

Tactic:
fun a =>
  let ⟨b, hb, hba⟩ := h a
  ⟨b, hb, fun hba' => hba (hr b a hba')⟩

Premises used: _private.0.Set.Unbounded.mono.match_1, Membership.mem, Exists, And, And.intro, Set.Unbounded, Exists.intro, Not
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
h : Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
h.rel_mono fun _ _ => le_of_lt

Premises used: le_of_lt, Set.Unbounded.rel_mono
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
⟨fun h => ?_, bounded_le_of_bounded_lt⟩

Premises used: Set.bounded_le_of_bounded_lt, Iff.intro
-- Module: Mathlib.Order.Bounded
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
refine : ∀ (h : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s), Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s

Tactic:
refine ⟨fun h => ?_, bounded_le_of_bounded_lt⟩