awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ (b ⊔ c) = a ⊔ c ⊔ b
rw₁ : a ⊔ (b ⊔ c) = a ⊔ (c ⊔ b)
rw₂ rw₃ : a ⊔ (c ⊔ b) = a ⊔ (c ⊔ b)
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ b

Tactic:
rw [sup_assoc, sup_assoc, sup_comm b]

Premises used: sup_assoc, sup_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c d : α
rw : a ⊔ (b ⊔ (c ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)
rw₁ : a ⊔ (c ⊔ (b ⊔ d)) = a ⊔ c ⊔ (b ⊔ d)
rw₂ rw₃ : a ⊔ c ⊔ (b ⊔ d) = a ⊔ c ⊔ (b ⊔ d)
⊢ a ⊔ b ⊔ (c ⊔ d) = a ⊔ c ⊔ (b ⊔ d)

Tactic:
rw [sup_assoc, sup_left_comm b, ← sup_assoc]

Premises used: sup_assoc, sup_left_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ (b ⊔ c) = b ⊔ c ⊔ a
rw₁ rw₂ : b ⊔ c ⊔ a = b ⊔ c ⊔ a
⊢ a ⊔ b ⊔ c = b ⊔ c ⊔ a

Tactic:
rw [sup_assoc, sup_comm]

Premises used: sup_assoc, sup_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : b ⊔ c ⊔ a = b ⊔ (c ⊔ a)
rw₁ rw₂ : b ⊔ (c ⊔ a) = b ⊔ (c ⊔ a)
⊢ a ⊔ (b ⊔ c) = b ⊔ (c ⊔ a)

Tactic:
rw [sup_comm, sup_assoc]

Premises used: sup_assoc, sup_comm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ (b ⊔ c) = a ⊔ a ⊔ (b ⊔ c)
rw₁ rw₂ : a ⊔ (b ⊔ c) = a ⊔ (b ⊔ c)
⊢ a ⊔ (b ⊔ c) = a ⊔ b ⊔ (a ⊔ c)

Tactic:
rw [sup_sup_sup_comm, sup_idem]

Premises used: sup_sup_sup_comm, sup_idem
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
rw : a ⊔ b ⊔ c = a ⊔ b ⊔ (c ⊔ c)
rw₁ rw₂ : a ⊔ b ⊔ c = a ⊔ b ⊔ c
⊢ a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)

Tactic:
rw [sup_sup_sup_comm, sup_idem]

Premises used: sup_sup_sup_comm, sup_idem
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
hb : b ≤ a ⊔ c
hc : c ≤ a ⊔ b
⊢ a ⊔ b = a ⊔ c

Tactic:
(sup_le le_sup_left hb).antisymm <| sup_le le_sup_left hc

Premises used: le_sup_left, LE.le.antisymm, sup_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
ha : a ≤ b ⊔ c
hb : b ≤ a ⊔ c
⊢ a ⊔ c = b ⊔ c

Tactic:
(sup_le ha le_sup_right).antisymm <| sup_le hb le_sup_right

Premises used: LE.le.antisymm, le_sup_right, sup_le
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ b = a ⊔ c ↔ b ≤ a ⊔ c ∧ c ≤ a ⊔ b

Tactic:
⟨fun h => ⟨h ▸ le_sup_right, h.symm ▸ le_sup_right⟩, fun h => sup_congr_left h.1 h.2⟩

Premises used: Eq.rec, le_sup_right, sup_congr_left, And.right, And.left, And.intro, Iff.intro, Eq.symm
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b c : α
⊢ a ⊔ c = b ⊔ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c

Tactic:
⟨fun h => ⟨h ▸ le_sup_left, h.symm ▸ le_sup_left⟩, fun h => sup_congr_right h.1 h.2⟩

Premises used: le_sup_left, Eq.rec, And.right, And.left, And.intro, Iff.intro, Eq.symm, sup_congr_right
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
hab : a ≠ b
⊢ a < a ⊔ b ∨ b < a ⊔ b

Tactic:
hab.symm.not_le_or_not_ge.imp left_lt_sup.2 right_lt_sup.2

Premises used: Iff.mpr, right_lt_sup, Ne.symm, left_lt_sup, Ne.not_le_or_not_ge, Or.imp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : SemilatticeSup α
a b : α
P : Prop
inst_1 : Decidable P
⊢ (if P then a else b) ≤ a ⊔ b

Tactic:
if h : P then (if_pos h).trans_le le_sup_left else (if_neg h).trans_le le_sup_right

Premises used: le_sup_left, le_sup_right, Eq.trans_le, if_pos, dite, if_neg
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
simp : x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
⊢ x ⊔ y ≤ c ↔ x ⊔ y ≤ c

Tactic:
simp only [sup_le_iff]

Premises used: sup_le_iff
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
rw : x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c
rw₁ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
rw₂ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
rw₃ rw₄ : x ≤ c ∧ y ≤ c ↔ x ≤ c ∧ y ≤ c
⊢ x ⊔ y ≤ c ↔ x ≤ c ∧ y ≤ c

Tactic:
rw [← H, @sup_le_iff α A, H, H]

Premises used: sup_le_iff
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk :
  ∀ [toPartialOrder : PartialOrder α] (sup : α → α → α) (le_sup_left : ∀ (a b : α), a ≤ sup a b)
    (le_sup_right : ∀ (a b : α), b ≤ sup a b) (sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c)
    (H : ∀ (x y : α), x ≤ y ↔ x ≤ y),
    { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
        sup_le := sup_le : SemilatticeSup α } =
      B
⊢ A = B

Tactic:
cases A
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
B : SemilatticeSup α
toPartialOrder : PartialOrder α
sup : α → α → α
le_sup_left : ∀ (a b : α), a ≤ sup a b
le_sup_right : ∀ (a b : α), b ≤ sup a b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk :
  ∀ [toPartialOrder_1 : PartialOrder α] (sup_1 : α → α → α) (le_sup_left_1 : ∀ (a b : α), a ≤ sup_1 a b)
    (le_sup_right_1 : ∀ (a b : α), b ≤ sup_1 a b) (sup_le_1 : ∀ (a b c : α), a ≤ c → b ≤ c → sup_1 a b ≤ c)
    (H : ∀ (x y : α), x ≤ y ↔ x ≤ y),
    { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
        sup_le := sup_le : SemilatticeSup α } =
      { toPartialOrder := toPartialOrder_1, sup := sup_1, le_sup_left := le_sup_left_1, le_sup_right := le_sup_right_1,
        sup_le := sup_le_1 }
⊢ { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
      sup_le := sup_le : SemilatticeSup α } =
    B

Tactic:
cases B
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
toPartialOrder : PartialOrder α
sup : α → α → α
le_sup_left : ∀ (a b : α), a ≤ sup a b
le_sup_right : ∀ (a b : α), b ≤ sup a b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c
toPartialOrder_1 : PartialOrder α
sup_1 : α → α → α
le_sup_left_1 : ∀ (a b : α), a ≤ sup_1 a b
le_sup_right_1 : ∀ (a b : α), b ≤ sup_1 a b
sup_le_1 : ∀ (a b c : α), a ≤ c → b ≤ c → sup_1 a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk :
  ∀ (le_sup_left_2 : ∀ (a b : α), a ≤ sup_1 a b) (le_sup_right_2 : ∀ (a b : α), b ≤ sup_1 a b)
    (sup_le_2 : ∀ (a b c : α), a ≤ c → b ≤ c → sup_1 a b ≤ c) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y),
    { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
        sup_le := sup_le : SemilatticeSup α } =
      {
        toPartialOrder :=
          { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
              sup_le := sup_le }.toPartialOrder,
        sup := sup_1, le_sup_left := le_sup_left_2, le_sup_right := le_sup_right_2, sup_le := sup_le_2 }
⊢ { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
      sup_le := sup_le : SemilatticeSup α } =
    { toPartialOrder := toPartialOrder_1, sup := sup_1, le_sup_left := le_sup_left_1, le_sup_right := le_sup_right_1,
      sup_le := sup_le_1 }

Tactic:
cases PartialOrder.ext H

Premises used: PartialOrder.ext
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
toPartialOrder : PartialOrder α
sup : α → α → α
le_sup_left : ∀ (a b : α), a ≤ sup a b
le_sup_right : ∀ (a b : α), b ≤ sup a b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c
sup_1 : α → α → α
le_sup_left_1 : ∀ (a b : α), a ≤ sup_1 a b
le_sup_right_1 : ∀ (a b : α), b ≤ sup_1 a b
sup_le_1 : ∀ (a b c : α), a ≤ c → b ≤ c → sup_1 a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk : sup = sup_1
⊢ { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
      sup_le := sup_le : SemilatticeSup α } =
    {
      toPartialOrder :=
        { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
            sup_le := sup_le }.toPartialOrder,
      sup := sup_1, le_sup_left := le_sup_left_1, le_sup_right := le_sup_right_1, sup_le := sup_le_1 }

Tactic:
congr
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
toPartialOrder : PartialOrder α
sup : α → α → α
le_sup_left : ∀ (a b : α), a ≤ sup a b
le_sup_right : ∀ (a b : α), b ≤ sup a b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c
sup_1 : α → α → α
le_sup_left_1 : ∀ (a b : α), a ≤ sup_1 a b
le_sup_right_1 : ∀ (a b : α), b ≤ sup_1 a b
sup_le_1 : ∀ (a b c : α), a ≤ c → b ≤ c → sup_1 a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk : ∀ (x x_1 : α), sup x x_1 = sup_1 x x_1
⊢ sup = sup_1

Tactic:
ext
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
toPartialOrder : PartialOrder α
sup : α → α → α
le_sup_left : ∀ (a b : α), a ≤ sup a b
le_sup_right : ∀ (a b : α), b ≤ sup a b
sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → sup a b ≤ c
sup_1 : α → α → α
le_sup_left_1 : ∀ (a b : α), a ≤ sup_1 a b
le_sup_right_1 : ∀ (a b : α), b ≤ sup_1 a b
sup_le_1 : ∀ (a b c : α), a ≤ c → b ≤ c → sup_1 a b ≤ c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x x_1 : α
⊢ sup x x_1 = sup_1 x x_1

Tactic:
apply SemilatticeSup.ext_sup H

Premises used: SemilatticeSup.ext_sup
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
H : SemilatticeSup α
⊢ OrderDual.instSemilatticeSup αᵒᵈ = H

Tactic:
SemilatticeSup.ext fun _ _ => Iff.rfl

Premises used: SemilatticeSup.ext, Iff.rfl
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : a ⊔ b = b
rw : (a ⊔ b) ⊓ a = a
rw₁ : a ⊓ (a ⊔ b) = a
rw₂ rw₃ : a = a
⊢ b ⊓ a = a

Tactic:
rw [← h, inf_comm, inf_sup_self]
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
sup_idem : ∀ (a : α), a ⊔ a = a
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
inf_idem : ∀ (a : α), a ⊓ a = a
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
a b : α
h : b ⊓ a = a
rw : b ⊓ a ⊔ b = b
rw₁ : b ⊔ b ⊓ a = b
rw₂ rw₃ : b = b
⊢ a ⊔ b = b

Tactic:
rw [← h, sup_comm, sup_inf_self]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
rw rw₁ : b ⊔ b = b ⊔ b
⊢ b ⊔ b = b ⊔ b ⊓ (b ⊔ b)

Tactic:
rw [inf_sup_self]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
b : α
rw rw₁ : b = b
⊢ b ⊔ b ⊓ (b ⊔ b) = b

Tactic:
rw [sup_inf_self]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
rw rw₁ : b ⊓ b = b ⊓ b
⊢ b ⊓ b = b ⊓ (b ⊔ b ⊓ b)

Tactic:
rw [sup_inf_self]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
b : α
rw rw₁ : b = b
⊢ b ⊓ (b ⊔ b ⊓ b) = b

Tactic:
rw [inf_sup_self]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : Eq.{u_1 + 1} (α := PartialOrder α) SemilatticeSup.toPartialOrder SemilatticeInf.toPartialOrder
a b : α
rw : SemilatticeInf.inf a b ≤ a
⊢ SemilatticeInf.inf a b ≤ a

Tactic:
rw [partial_order_eq]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : Eq.{u_1 + 1} (α := PartialOrder α) SemilatticeSup.toPartialOrder SemilatticeInf.toPartialOrder
a b : α
⊢ SemilatticeInf.inf a b ≤ a

Tactic:
apply inf_le_left

Premises used: inf_le_left
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : Eq.{u_1 + 1} (α := PartialOrder α) SemilatticeSup.toPartialOrder SemilatticeInf.toPartialOrder
a b : α
rw : SemilatticeInf.inf a b ≤ b
⊢ SemilatticeInf.inf a b ≤ b

Tactic:
rw [partial_order_eq]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : Eq.{u_1 + 1} (α := PartialOrder α) SemilatticeSup.toPartialOrder SemilatticeInf.toPartialOrder
a b : α
⊢ SemilatticeInf.inf a b ≤ b

Tactic:
apply inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : Eq.{u_1 + 1} (α := PartialOrder α) SemilatticeSup.toPartialOrder SemilatticeInf.toPartialOrder
a b c : α
rw : a ≤ b → a ≤ c → a ≤ SemilatticeInf.inf b c
⊢ a ≤ b → a ≤ c → a ≤ SemilatticeInf.inf b c

Tactic:
rw [partial_order_eq]
-- Module: Mathlib.Order.Lattice
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : Max α
inst_1 : Min α
sup_comm : ∀ (a b : α), a ⊔ b = b ⊔ a
sup_assoc : ∀ (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
inf_comm : ∀ (a b : α), a ⊓ b = b ⊓ a
inf_assoc : ∀ (a b c : α), a ⊓ b ⊓ c = a ⊓ (b ⊓ c)
sup_inf_self : ∀ (a b : α), a ⊔ a ⊓ b = a
inf_sup_self : ∀ (a b : α), a ⊓ (a ⊔ b) = a
sup_idem : ∀ (b : α), b ⊔ b = b
inf_idem : ∀ (b : α), b ⊓ b = b
semilatt_inf_inst : SemilatticeInf α := SemilatticeInf.mk' inf_comm inf_assoc inf_idem
semilatt_sup_inst : SemilatticeSup α := SemilatticeSup.mk' sup_comm sup_assoc sup_idem
partial_order_eq : Eq.{u_1 + 1} (α := PartialOrder α) SemilatticeSup.toPartialOrder SemilatticeInf.toPartialOrder
a b c : α
⊢ a ≤ b → a ≤ c → a ≤ SemilatticeInf.inf b c

Tactic:
apply le_inf

Premises used: le_inf
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b : α
⊢ a ⊓ b ≤ a ⊔ b

Tactic:
inf_le_left.trans le_sup_left

Premises used: le_sup_left, inf_le_left, LE.le.trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b : α
⊢ a ⊔ b ≤ a ⊓ b ↔ a = b

Tactic:
simp [le_antisymm_iff, and_comm]

Premises used: and_comm, le_antisymm_iff
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b : α
rw : a ⊔ b ≤ a ⊓ b ↔ a = b
rw₁ rw₂ : a = b ↔ a = b
⊢ a ⊓ b = a ⊔ b ↔ a = b

Tactic:
rw [← inf_le_sup.ge_iff_eq, sup_le_inf]

Premises used: sup_le_inf, inf_le_sup, LE.le.ge_iff_eq
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b : α
rw : a ⊓ b ≠ a ⊔ b ↔ a ≠ b
rw₁ : ¬a ⊓ b = a ⊔ b ↔ a ≠ b
rw₂ rw₃ : ¬a = b ↔ a ≠ b
⊢ a ⊓ b < a ⊔ b ↔ a ≠ b

Tactic:
rw [inf_le_sup.lt_iff_ne, Ne, inf_eq_sup]

Premises used: inf_eq_sup, inf_le_sup, Ne, LE.le.lt_iff_ne
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b c : α
⊢ a ⊓ b ≤ b ⊔ c

Tactic:
le_trans inf_le_right le_sup_left

Premises used: le_sup_left, inf_le_right, le_trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b c : α
⊢ b ⊓ a ≤ b ⊔ c

Tactic:
le_trans inf_le_left le_sup_left

Premises used: le_sup_left, inf_le_left, le_trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b c : α
⊢ a ⊓ b ≤ c ⊔ b

Tactic:
le_trans inf_le_right le_sup_right

Premises used: inf_le_right, le_sup_right, le_trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b c : α
⊢ a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c

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

Premises used: Iff.intro
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b c : α
refine_1 : ∀ (h : a ⊓ b = c ∧ a ⊔ b = c), a = c ∧ b = c
refine_2 : a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c
⊢ a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b c : α
h : a ⊓ b = c ∧ a ⊔ b = c
refine_1 : ∀ (h : a ⊓ a = c ∧ a ⊔ a = c), a = c ∧ a = c
⊢ a = c ∧ b = c

Tactic:
obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)

Premises used: And.right, And.left, sup_eq_inf, Iff.mp, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a c : α
h : a ⊓ a = c ∧ a ⊔ a = c
⊢ a = c ∧ a = c

Tactic:
simpa using h
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
b : α
⊢ b ⊓ b = b ∧ b ⊔ b = b

Tactic:
⟨inf_idem _, sup_idem _⟩

Premises used: sup_idem, And.intro, inf_idem
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
b : α
⊢ b ⊓ b = b ∧ b ⊔ b = b

Tactic:
exact ⟨inf_idem _, sup_idem _⟩
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b c : α
⊢ a ⊔ b ⊓ c ≤ (a ⊔ b) ⊓ (a ⊔ c)

Tactic:
le_inf (sup_le_sup_left inf_le_left _) (sup_le_sup_left inf_le_right _)

Premises used: sup_le_sup_left, le_inf
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b : α
⊢ a ⊓ (a ⊔ b) = a

Tactic:
simp
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u
inst : Lattice α
a b : α
rw : a ≤ b ↔ a ⊓ b = a
rw₁ rw₂ : a ⊓ b = a ↔ a ⊓ b = a
⊢ a ⊔ b = b ↔ a ⊓ b = a

Tactic:
rw [sup_eq_right, ← inf_eq_left]

Premises used: sup_eq_right, inf_eq_left
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
A B : Lattice α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk :
  ∀ [toSemilatticeSup : SemilatticeSup α] (inf : α → α → α) (inf_le_left : ∀ (a b : α), inf a b ≤ a)
    (inf_le_right : ∀ (a b : α), inf a b ≤ b) (le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c)
    (H : ∀ (x y : α), x ≤ y ↔ x ≤ y),
    { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
        le_inf := le_inf : Lattice α } =
      B
⊢ A = B

Tactic:
cases A
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
B : Lattice α
toSemilatticeSup : SemilatticeSup α
inf : α → α → α
inf_le_left : ∀ (a b : α), inf a b ≤ a
inf_le_right : ∀ (a b : α), inf a b ≤ b
le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk :
  ∀ [toSemilatticeSup_1 : SemilatticeSup α] (inf_1 : α → α → α) (inf_le_left_1 : ∀ (a b : α), inf_1 a b ≤ a)
    (inf_le_right_1 : ∀ (a b : α), inf_1 a b ≤ b) (le_inf_1 : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf_1 b c)
    (H : ∀ (x y : α), x ≤ y ↔ x ≤ y),
    { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
        le_inf := le_inf : Lattice α } =
      { toSemilatticeSup := toSemilatticeSup_1, inf := inf_1, inf_le_left := inf_le_left_1,
        inf_le_right := inf_le_right_1, le_inf := le_inf_1 }
⊢ { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
      le_inf := le_inf : Lattice α } =
    B

Tactic:
cases B
-- Module: Mathlib.Order.Lattice
Goal:
α : Type u_1
toSemilatticeSup : SemilatticeSup α
inf : α → α → α
inf_le_left : ∀ (a b : α), inf a b ≤ a
inf_le_right : ∀ (a b : α), inf a b ≤ b
le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf b c
toSemilatticeSup_1 : SemilatticeSup α
inf_1 : α → α → α
inf_le_left_1 : ∀ (a b : α), inf_1 a b ≤ a
inf_le_right_1 : ∀ (a b : α), inf_1 a b ≤ b
le_inf_1 : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf_1 b c
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
mk :
  ∀ (inf_le_left_2 : ∀ (a b : α), inf_1 a b ≤ a) (inf_le_right_2 : ∀ (a b : α), inf_1 a b ≤ b)
    (le_inf_2 : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ inf_1 b c) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y),
    { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
        le_inf := le_inf : Lattice α } =
      {
        toSemilatticeSup :=
          { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
              le_inf := le_inf }.toSemilatticeSup,
        inf := inf_1, inf_le_left := inf_le_left_2, inf_le_right := inf_le_right_2, le_inf := le_inf_2 }
⊢ { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
      le_inf := le_inf : Lattice α } =
    { toSemilatticeSup := toSemilatticeSup_1, inf := inf_1, inf_le_left := inf_le_left_1,
      inf_le_right := inf_le_right_1, le_inf := le_inf_1 }

Tactic:
cases SemilatticeSup.ext H

Premises used: SemilatticeSup.ext