awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderTop α
a b c : α
ha : Codisjoint a c
hb : Codisjoint b c
⊢ Codisjoint (a ⊓ b) c

Tactic:
codisjoint_inf_left.2 ⟨ha, hb⟩

Premises used: Iff.mpr, And.intro, codisjoint_inf_left
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderTop α
a b c : α
hb : Codisjoint a b
hc : Codisjoint a c
⊢ Codisjoint a (b ⊓ c)

Tactic:
codisjoint_inf_right.2 ⟨hb, hc⟩

Premises used: Iff.mpr, codisjoint_inf_right, And.intro
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderTop α
a b c : α
h : a ⊓ b ≤ c
hd : Codisjoint b c
⊢ a ≤ c

Tactic:
@Disjoint.left_le_of_le_sup_right αᵒᵈ _ _ _ _ _ h hd.symm

Premises used: Disjoint.left_le_of_le_sup_right, Codisjoint.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : OrderTop α
a b c : α
h : b ⊓ a ≤ c
hd : Codisjoint b c
rwa rwa₁ rwa₂ rwa₃ : b ⊓ a ≤ c
⊢ a ⊓ b ≤ c

Tactic:
rwa [inf_comm]

Premises used: inf_comm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
⊢ Disjoint a b → Codisjoint (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ)

Tactic:
id

Premises used: Codisjoint, id, OrderDual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderTop α
a b : α
⊢ Disjoint (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ Codisjoint a b

Tactic:
Iff.rfl

Premises used: Codisjoint, Iff.rfl, OrderDual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : αᵒᵈ
⊢ Disjoint (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ Codisjoint a b

Tactic:
Iff.rfl

Premises used: Codisjoint, Iff.rfl, OrderDual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
rw : a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)
⊢ a ≤ c

Tactic:
rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]

Premises used: inf_top_eq, bot_sup_eq, sup_inf_right, Disjoint.eq_bot, Codisjoint.eq_top
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
inf_le_inf_right _ le_sup_left

Premises used: le_sup_left, inf_le_inf_right
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)

Tactic:
exact inf_le_inf_right _ le_sup_left

Premises used: inf_le_inf_right
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
a b : α
⊢ IsCompl a b ↔ Disjoint a b ∧ Codisjoint a b

Tactic:
⟨fun h ↦ ⟨h.1, h.2⟩, fun h ↦ ⟨h.1, h.2⟩⟩

Premises used: And.right, And.left, And.intro, Iff.intro, IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
x y : α
h : IsCompl x y
⊢ IsCompl y x

Tactic:
⟨h.1.symm, h.2.symm⟩

Premises used: Disjoint.symm, IsCompl.mk, Codisjoint.symm, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
x y : α
⊢ IsCompl x y ↔ IsCompl y x

Tactic:
⟨IsCompl.symm, IsCompl.symm⟩

Premises used: Iff.intro, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
x y : α
h : IsCompl x y
⊢ IsCompl (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) y : αᵒᵈ)

Tactic:
⟨h.2, h.1⟩

Premises used: IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
a b : αᵒᵈ
h : IsCompl a b
⊢ IsCompl (α := α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) a : α) ((OrderDual.ofDual : (a : αᵒᵈ) → α) b : α)

Tactic:
⟨h.2, h.1⟩

Premises used: IsCompl.mk, IsCompl.codisjoint, IsCompl.disjoint
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x y : α
h₁ : x ⊓ y ≤ ⊥
h₂ : ⊤ ≤ x ⊔ y
⊢ Disjoint x y

Tactic:
grind [disjoint_iff_inf_le]

Premises used: disjoint_iff_inf_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x y : α
h₁ : x ⊓ y ≤ ⊥
h₂ : ⊤ ≤ x ⊔ y
⊢ Codisjoint x y

Tactic:
grind [codisjoint_iff_le_sup]

Premises used: codisjoint_iff_le_sup
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x y : α
h₁ : x ⊓ y = ⊥
h₂ : x ⊔ y = ⊤
⊢ IsCompl x y

Tactic:
⟨disjoint_iff.mpr h₁, codisjoint_iff.mpr h₂⟩

Premises used: Iff.mpr, codisjoint_iff, disjoint_iff, IsCompl.mk
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x y : α
h : IsCompl x y
⊢ x ⊓ y = ⊥

Tactic:
h.disjoint.eq_bot

Premises used: IsCompl.disjoint, Disjoint.eq_bot
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
rw : b ⊓ x ⊔ ⊥ = b ⊓ x
rw₁ rw₂ : b ⊓ x = b ⊓ x
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x

Tactic:
rw [h.symm.inf_eq_bot, sup_bot_eq]

Premises used: sup_bot_eq, IsCompl.inf_eq_bot, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y a b : α
h : IsCompl x y
⊢ a ≤ b ⊔ y ↔ a ⊓ x ≤ b

Tactic:
⟨h.inf_left_le_of_le_sup_right, h.symm.dual.inf_left_le_of_le_sup_right⟩

Premises used: IsCompl.inf_left_le_of_le_sup_right, Iff.intro, IsCompl.dual, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
rw : x ⊓ y ≤ ⊥ ↔ x ≤ z
rw₁ : x ≤ ⊥ ⊔ z ↔ x ≤ z
rw₂ rw₃ : x ≤ z ↔ x ≤ z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]

Premises used: le_bot_iff, IsCompl.le_sup_right_iff_inf_left_le, bot_sup_eq
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ z = ⊥ ↔ x ≤ y

Tactic:
h.symm.inf_left_eq_bot_iff

Premises used: IsCompl.inf_left_eq_bot_iff, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
rw : x ⊓ y = ⊥ ↔ x ≤ z
⊢ Disjoint x y ↔ x ≤ z

Tactic:
rw [disjoint_iff]

Premises used: disjoint_iff
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
h.inf_left_eq_bot_iff

Premises used: IsCompl.inf_left_eq_bot_iff
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
exact h.inf_left_eq_bot_iff

Premises used: IsCompl.inf_left_eq_bot_iff
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ Disjoint x z ↔ x ≤ y

Tactic:
h.symm.disjoint_left_iff

Premises used: IsCompl.disjoint_left_iff, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl x y
⊢ z ≤ x ↔ Disjoint z y

Tactic:
h.disjoint_right_iff.symm

Premises used: Iff.symm, IsCompl.disjoint_right_iff
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl x y
⊢ z ≤ y ↔ Disjoint z x

Tactic:
h.symm.le_left_iff

Premises used: IsCompl.le_left_iff, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl x y
⊢ x ≤ z ↔ Codisjoint z y

Tactic:
h.dual.le_left_iff

Premises used: Codisjoint, OrderDual, IsCompl.dual, IsCompl.le_left_iff
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl x y
⊢ y ≤ z ↔ Codisjoint z x

Tactic:
h.symm.left_le_iff

Premises used: IsCompl.left_le_iff, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
hx : x ≤ x'
⊢ y' ≤ y

Tactic:
h'.right_le_iff.2 <| h.symm.codisjoint.mono_right hx

Premises used: Iff.mpr, IsCompl.right_le_iff, Codisjoint.mono_right, IsCompl.codisjoint, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
hxy : IsCompl x y
hxz : IsCompl x z
⊢ y = z

Tactic:
le_antisymm (hxz.Antitone hxy <| le_refl x) (hxy.Antitone hxz <| le_refl x)

Premises used: le_refl, le_antisymm, IsCompl.Antitone
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
hxz : IsCompl x z
hyz : IsCompl y z
⊢ x = y

Tactic:
hxz.symm.right_unique hyz.symm

Premises used: IsCompl.right_unique, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
rw : x ⊓ (y ⊓ y') ⊔ x' ⊓ (y ⊓ y') = ⊥
rw₁ : x ⊓ y ⊓ y' ⊔ x' ⊓ (y ⊓ y') = ⊥
rw₂ : ⊥ ⊓ y' ⊔ x' ⊓ (y ⊓ y') = ⊥
rw₃ : ⊥ ⊔ x' ⊓ (y ⊓ y') = ⊥
rw₄ : x' ⊓ (y ⊓ y') = ⊥
rw₅ : y ⊓ (x' ⊓ y') = ⊥
rw₆ : y ⊓ ⊥ = ⊥
rw₇ rw₈ : Eq.{u_1 + 1} (α := α) ⊥ ⊥
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥

Tactic:
rw [inf_sup_right, ← inf_assoc, h.inf_eq_bot, bot_inf_eq, bot_sup_eq, inf_left_comm,
      h'.inf_eq_bot, inf_bot_eq]

Premises used: bot_sup_eq, inf_sup_right, IsCompl.inf_eq_bot, inf_bot_eq, inf_assoc, bot_inf_eq, inf_left_comm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
rw : (x ⊔ x' ⊔ y) ⊓ (x ⊔ x' ⊔ y') = ⊤
rw₁ : (x' ⊔ x ⊔ y) ⊓ (x' ⊔ x ⊔ y') = ⊤
rw₂ : (x' ⊔ (x ⊔ y)) ⊓ (x' ⊔ x ⊔ y') = ⊤
rw₃ : (x' ⊔ ⊤) ⊓ (x' ⊔ x ⊔ y') = ⊤
rw₄ : ⊤ ⊓ (x' ⊔ x ⊔ y') = ⊤
rw₅ : x' ⊔ x ⊔ y' = ⊤
rw₆ : x' ⊔ (x ⊔ y') = ⊤
rw₇ : x ⊔ (x' ⊔ y') = ⊤
rw₈ : x ⊔ ⊤ = ⊤
rw₉ rw₁₀ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤

Tactic:
rw [sup_inf_left, sup_comm x, sup_assoc, h.sup_eq_top, sup_top_eq, top_inf_eq,
      sup_assoc, sup_left_comm, h'.sup_eq_top, sup_top_eq]

Premises used: IsCompl.sup_eq_top, sup_top_eq, top_inf_eq, sup_inf_left, sup_assoc, sup_comm, sup_left_comm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ IsCompl (x ⊓ x') (y ⊔ y')

Tactic:
(h.symm.sup_inf h'.symm).symm

Premises used: IsCompl.sup_inf, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
mp : Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
mpr : Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y
⊢ Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
constructor
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
mp : ∀ (a : α) (hx : a ≤ x.fst) (hy : a ≤ y.fst), snd (a, ⊥) ≤ x.snd
mp₁ : ∀ (a : α) (hx : a ≤ x.fst) (hy : a ≤ y.fst), snd (a, ⊥) ≤ y.snd
mp₂ : ∀ (b : β) (hx : b ≤ x.snd) (hy : b ≤ y.snd), fst (⊥, b) ≤ x.fst
mp₃ : ∀ (b : β) (hx : b ≤ x.snd) (hy : b ≤ y.snd), fst (⊥, b) ≤ y.fst
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd

Tactic:
refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ snd (a, ⊥) ≤ x.snd

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ snd (a, ⊥) ≤ x.snd

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ snd (a, ⊥) ≤ y.snd

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
a : α
hx : a ≤ x.fst
hy : a ≤ y.fst
⊢ snd (a, ⊥) ≤ y.snd

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ fst (⊥, b) ≤ x.fst

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ fst (⊥, b) ≤ x.fst

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ fst (⊥, b) ≤ y.fst

Tactic:
bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
h : Disjoint x y
b : β
hx : b ≤ x.snd
hy : b ≤ y.snd
⊢ fst (⊥, b) ≤ y.fst

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
ha : Disjoint x.fst y.fst
hb : Disjoint x.snd y.snd
z : α × β
hza : z ≤ x
hzb : z ≤ y
⊢ z ≤ ⊥

Tactic:
⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
ha : Disjoint x.fst y.fst
hb : Disjoint x.snd y.snd
z : α × β
hza : z ≤ x
hzb : z ≤ y
⊢ z ≤ ⊥

Tactic:
exact ⟨ha hza.1 hzb.1, hb hza.2 hzb.2⟩
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
x y : α × β
⊢ Codisjoint x y ↔ Codisjoint x.fst y.fst ∧ Codisjoint x.snd y.snd

Tactic:
@Prod.disjoint_iff αᵒᵈ βᵒᵈ _ _ _ _ _ _

Premises used: Codisjoint, Prod.disjoint_iff, OrderDual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
x y : α × β
simp_rw :
  Disjoint x y ∧ Codisjoint x y ↔
    (Disjoint x.fst y.fst ∧ Codisjoint x.fst y.fst) ∧ Disjoint x.snd y.snd ∧ Codisjoint x.snd y.snd
simp_rw₁ :
  (Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd) ∧ Codisjoint x y ↔
    (Disjoint x.fst y.fst ∧ Codisjoint x.fst y.fst) ∧ Disjoint x.snd y.snd ∧ Codisjoint x.snd y.snd
simp_rw₂ :
  (Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd) ∧ Codisjoint x.fst y.fst ∧ Codisjoint x.snd y.snd ↔
    (Disjoint x.fst y.fst ∧ Codisjoint x.fst y.fst) ∧ Disjoint x.snd y.snd ∧ Codisjoint x.snd y.snd
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd

Tactic:
simp_rw [isCompl_iff, Prod.disjoint_iff, Prod.codisjoint_iff, and_and_and_comm]

Premises used: Prod.codisjoint_iff, isCompl_iff, and_and_and_comm, Prod.disjoint_iff
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
a b : α
⊢ IsCompl (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ IsCompl a b

Tactic:
⟨IsCompl.ofDual, IsCompl.dual⟩

Premises used: IsCompl.ofDual, Iff.intro, IsCompl.dual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
a b : αᵒᵈ
⊢ IsCompl (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ IsCompl a b

Tactic:
⟨IsCompl.dual, IsCompl.ofDual⟩

Premises used: IsCompl.ofDual, Iff.intro, IsCompl.dual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ IsCompl.{u_1} (α := α) ⊥ ⊤

Tactic:
IsCompl.of_eq (bot_inf_eq _) (sup_top_eq _)

Premises used: sup_top_eq, IsCompl.of_eq, bot_inf_eq
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ IsCompl.{u_1} (α := α) ⊤ ⊥

Tactic:
IsCompl.of_eq (inf_bot_eq _) (top_sup_eq _)

Premises used: IsCompl.of_eq, top_sup_eq, inf_bot_eq
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x : α
h : IsCompl x ⊥
rw : x ⊔ ⊥ = ⊤
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
⊢ x = ⊤

Tactic:
rw [← sup_bot_eq x, h.sup_eq_top]

Premises used: IsCompl.sup_eq_top, sup_bot_eq
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x : α
h : IsCompl ⊥ x
⊢ x = ⊤

Tactic:
eq_top_of_isCompl_bot h.symm

Premises used: eq_top_of_isCompl_bot, IsCompl.symm
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x : α
h : IsCompl x ⊤
⊢ x = ⊥

Tactic:
eq_top_of_isCompl_bot h.dual

Premises used: OrderDual, eq_top_of_isCompl_bot, IsCompl.dual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x : α
h : IsCompl ⊤ x
⊢ x = ⊥

Tactic:
eq_top_of_bot_isCompl h.dual

Premises used: eq_top_of_bot_isCompl, OrderDual, IsCompl.dual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ IsComplemented.{u_1} (α := α) ⊥

Tactic:
⟨⊤, isCompl_bot_top⟩

Premises used: Exists.intro, isCompl_bot_top, Top.top, IsComplemented
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ IsComplemented.{u_1} (α := α) ⊤

Tactic:
⟨⊥, isCompl_top_bot⟩

Premises used: Bot.bot, Exists.intro, isCompl_top_bot, IsComplemented
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : α
⊢ IsComplemented a → IsComplemented b → IsComplemented (a ⊔ b)

Tactic:
fun ⟨a', ha⟩ ⟨b', hb⟩ => ⟨a' ⊓ b', ha.sup_inf hb⟩

Premises used: IsCompl.sup_inf, Max.max, Exists.intro, _private.0.IsComplemented.sup.match_1, Min.min, IsComplemented
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : α
⊢ IsComplemented a → IsComplemented b → IsComplemented (a ⊓ b)

Tactic:
fun ⟨a', ha⟩ ⟨b', hb⟩ => ⟨a' ⊔ b', ha.inf_sup hb⟩

Premises used: Max.max, Exists.intro, _private.0.IsComplemented.sup.match_1, IsCompl.inf_sup, Min.min, IsComplemented
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
⊢ ComplementedLattice α ↔ ∀ (a : α), ∃ (b : α), IsCompl a b

Tactic:
⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩

Premises used: ComplementedLattice.mk, _private.0.complementedLattice_iff.match_1, Iff.intro
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Subsingleton α
⊢ ComplementedLattice α

Tactic:
⟨fun a ↦ ⟨⊥, disjoint_bot_right, ?_⟩⟩

Premises used: ComplementedLattice.mk, disjoint_bot_right, Bot.bot, Exists.intro, IsCompl.mk
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Subsingleton α
refine : ∀ (a : α), Codisjoint a ⊥
⊢ ComplementedLattice α

Tactic:
refine ⟨fun a ↦ ⟨⊥, disjoint_bot_right, ?_⟩⟩
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Subsingleton α
a : α
rw : Codisjoint a ⊤
⊢ Codisjoint a ⊥

Tactic:
rw [Subsingleton.elim ⊥ ⊤]

Premises used: Bot.bot, Subsingleton.elim, Top.top
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Subsingleton α
a : α
⊢ Codisjoint a ⊤

Tactic:
codisjoint_top_right

Premises used: codisjoint_top_right
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Subsingleton α
a : α
⊢ Codisjoint a ⊤

Tactic:
exact codisjoint_top_right

Premises used: codisjoint_top_right
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : ComplementedLattice α
⊢ ComplementedLattice.{u_1} αᵒᵈ

Tactic:
⟨fun a ↦
    let ⟨b, hb⟩ := exists_isCompl (show α from a)
    ⟨b, hb.dual⟩⟩

Premises used: ComplementedLattice.mk, Exists, ComplementedLattice.exists_isCompl, _private.0.ComplementedLattice.instOrderDual.match_1, IsCompl, Exists.intro, IsCompl.dual
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ Injective.{u_1 + 1, u_1 + 1} (α := { a : α // IsComplemented a }) (Subtype.val (p := fun (a : α) ↦ IsComplemented a))

Tactic:
Subtype.coe_injective

Premises used: Subtype.coe_injective
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ (↑a : α) = (↑b : α) ↔ a = b

Tactic:
Subtype.coe_inj

Premises used: Subtype.coe_inj
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ (↑a : α) ≤ (↑b : α) ↔ a ≤ b

Tactic:
simp
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ (↑a : α) < (↑b : α) ↔ a < b

Tactic:
simp
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ Eq.{u_1 + 1} (α := α) (↑⊥ : α) ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ Eq.{u_1 + 1} (α := α) (↑⊤ : α) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ Eq.{u_1 + 1} (α := { a : α // IsComplemented a }) (Subtype.mk (p := fun (a : α) ↦ IsComplemented a) ⊥ ⋯) ⊥

Tactic:
simp
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
⊢ Eq.{u_1 + 1} (α := { a : α // IsComplemented a }) (Subtype.mk (p := fun (a : α) ↦ IsComplemented a) ⊤ ⋯) ⊤

Tactic:
simp
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ (↑(a ⊔ b) : α) = (↑a : α) ⊔ (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ (↑(a ⊓ b) : α) = (↑a : α) ⊓ (↑b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : α
ha : IsComplemented a
hb : IsComplemented b
⊢ Subtype.mk (p := fun (a : α) ↦ IsComplemented a) a ha ⊔ Subtype.mk (p := fun (a : α) ↦ IsComplemented a) b hb =
    Subtype.mk (p := fun (a : α) ↦ IsComplemented a) (a ⊔ b) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Disjoint
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : α
ha : IsComplemented a
hb : IsComplemented b
⊢ Subtype.mk (p := fun (a : α) ↦ IsComplemented a) a ha ⊓ Subtype.mk (p := fun (a : α) ↦ IsComplemented a) b hb =
    Subtype.mk (p := fun (a : α) ↦ IsComplemented a) (a ⊓ b) ⋯

Tactic:
rfl

Premises used: rfl