awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u_1
A B : SemilatticeSup α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
have 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
Tactic: cases A
Cleared hypotheses: A, H
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ { toPartialOrder := toPartialOrder, sup := sup, le_sup_left := le_sup_left, le_sup_right := le_sup_right,
      sup_le := sup_le : SemilatticeSup α } =
    B
have 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 }
Tactic: cases B
Cleared hypotheses: B, H
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ { 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 }
have 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 }
Tactic: cases PartialOrder.ext H
Cleared hypotheses: toPartialOrder_1, le_sup_left_1, le_sup_right_1, sup_le_1, H
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ { 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 }
have mk : sup = sup_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ sup = sup_1
have mk : ∀ (x x_1 : α), sup x x_1 = sup_1 x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ b ⊓ a = a
have rw : (a ⊔ b) ⊓ a = a
Tactic: rw [← h, inf_comm, inf_sup_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ b ⊓ a = a
have rw₁ : a ⊓ (a ⊔ b) = a
Tactic: rw [← h, inf_comm, inf_sup_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ b ⊓ a = a
have rw₂ : a = a
Tactic: rw [← h, inf_comm, inf_sup_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ a ⊔ b = b
have rw : b ⊓ a ⊔ b = b
Tactic: rw [← h, sup_comm, sup_inf_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ a ⊔ b = b
have rw₁ : b ⊔ b ⊓ a = b
Tactic: rw [← h, sup_comm, sup_inf_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ a ⊔ b = b
have rw₂ : b = b
Tactic: rw [← h, sup_comm, sup_inf_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : α
⊢ b ⊔ b = b ⊔ b ⊓ (b ⊔ b)
have rw : b ⊔ b = b ⊔ b
Tactic: rw [inf_sup_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : α
⊢ b ⊔ b ⊓ (b ⊔ b) = b
have rw : b = b
Tactic: rw [sup_inf_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : α
⊢ b ⊓ b = b ⊓ (b ⊔ b ⊓ b)
have rw : b ⊓ b = b ⊓ b
Tactic: rw [sup_inf_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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 : α
⊢ b ⊓ (b ⊔ b ⊓ b) = b
have rw : b = b
Tactic: rw [inf_sup_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
have rw : SemilatticeInf.inf a b ≤ a
Tactic: rw [partial_order_eq]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
have rw : SemilatticeInf.inf a b ≤ b
Tactic: rw [partial_order_eq]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
have rw : a ≤ b → a ≤ c → a ≤ SemilatticeInf.inf b c
Tactic: rw [partial_order_eq]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b : α
⊢ a ⊓ b = a ⊔ b ↔ a = b
have rw : a ⊔ b ≤ a ⊓ b ↔ a = b
Tactic: rw [← inf_le_sup.ge_iff_eq, sup_le_inf]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b : α
rw : a ⊔ b ≤ a ⊓ b ↔ a = b
⊢ a ⊓ b = a ⊔ b ↔ a = b
have rw₁ : a = b ↔ a = b
Tactic: rw [← inf_le_sup.ge_iff_eq, sup_le_inf]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b : α
⊢ a ⊓ b < a ⊔ b ↔ a ≠ b
have rw : a ⊓ b ≠ a ⊔ b ↔ a ≠ b
Tactic: rw [inf_le_sup.lt_iff_ne, Ne, inf_eq_sup]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b : α
rw : a ⊓ b ≠ a ⊔ b ↔ a ≠ b
⊢ a ⊓ b < a ⊔ b ↔ a ≠ b
have rw₁ : ¬a ⊓ b = a ⊔ b ↔ a ≠ b
Tactic: rw [inf_le_sup.lt_iff_ne, Ne, inf_eq_sup]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b : α
rw : a ⊓ b ≠ a ⊔ b ↔ a ≠ b
rw₁ : ¬a ⊓ b = a ⊔ b ↔ a ≠ b
⊢ a ⊓ b < a ⊔ b ↔ a ≠ b
have rw₂ : ¬a = b ↔ a ≠ b
Tactic: rw [inf_le_sup.lt_iff_ne, Ne, inf_eq_sup]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b c : α
⊢ a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c
have refine_1 : ∀ (h : a ⊓ b = c ∧ a ⊔ b = c), a = c ∧ b = c
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b c : α
refine_1 : ∀ (h : a ⊓ b = c ∧ a ⊔ b = c), a = c ∧ b = c
⊢ a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c
have refine_2 : a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b c : α
h : a ⊓ b = c ∧ a ⊔ b = c
⊢ a = c ∧ b = c
have refine_1 : ∀ (h : a ⊓ a = c ∧ a ⊔ a = c), a = c ∧ a = c
Tactic: obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b : α
⊢ a ⊔ b = b ↔ a ⊓ b = a
have rw : a ≤ b ↔ a ⊓ b = a
Tactic: rw [sup_eq_right, ← inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : Lattice α
a b : α
rw : a ≤ b ↔ a ⊓ b = a
⊢ a ⊔ b = b ↔ a ⊓ b = a
have rw₁ : a ⊓ b = a ↔ a ⊓ b = a
Tactic: rw [sup_eq_right, ← inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u_1
A B : Lattice α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ A = B
have 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
Tactic: cases A
Cleared hypotheses: A, H
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
      le_inf := le_inf : Lattice α } =
    B
have 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 }
Tactic: cases B
Cleared hypotheses: B, H
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
⊢ { 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 }
have 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 }
Tactic: cases SemilatticeSup.ext H
Cleared hypotheses: toSemilatticeSup_1, inf_le_left_1, inf_le_right_1, le_inf_1, H
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
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
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 := 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_1, inf_le_right := inf_le_right_1, le_inf := le_inf_1 }
have mk : ∀ (inf_le_left_2 : ∀ (a b : α), inf a b ≤ a) (inf_le_right_2 : ∀ (a b : α), inf a b ≤ b)
  (le_inf_2 : ∀ (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 α } =
    {
      toSemilatticeSup :=
        { toSemilatticeSup := toSemilatticeSup, inf := inf, inf_le_left := inf_le_left, inf_le_right := inf_le_right,
            le_inf := le_inf }.toSemilatticeSup,
      inf := inf, inf_le_left := inf_le_left_2, inf_le_right := inf_le_right_2, le_inf := le_inf_2 }
Tactic: cases SemilatticeInf.ext H
Cleared hypotheses: inf_1, inf_le_left_1, inf_le_right_1, le_inf_1, H
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : DistribLattice α
a b c : α
⊢ a ⊓ (b ⊔ c) = a ⊓ (a ⊔ c) ⊓ (b ⊔ c)
have rw : a ⊓ (b ⊔ c) = a ⊓ (b ⊔ c)
Tactic: rw [inf_sup_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : DistribLattice α
a b c : α
⊢ a ⊓ (a ⊓ b ⊔ c) = (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c)
have rw : a ⊓ (a ⊓ b ⊔ c) = a ⊓ (a ⊓ b ⊔ c)
Tactic: rw [sup_inf_self]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : DistribLattice α
a b c : α
⊢ (a ⊔ a ⊓ b) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)
have rw : (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)
Tactic: rw [sup_comm]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : DistribLattice α
a b c : α
⊢ (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = a ⊓ b ⊔ a ⊓ c
have rw : (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c) = (a ⊓ b ⊔ a) ⊓ (a ⊓ b ⊔ c)
Tactic: rw [sup_inf_left]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : DistribLattice α
x y z : α
⊢ x ⊓ (y ⊔ z) ≤ x ⊓ y ⊔ x ⊓ z
have rw : x ⊓ y ⊔ x ⊓ z ≤ x ⊓ y ⊔ x ⊓ z
Tactic: rw [inf_sup_left]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)
have rw : (y ⊔ x) ⊓ (z ⊔ x) = (y ⊔ x) ⊓ (x ⊔ z)
Tactic: rw [sup_inf_right, sup_comm x]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
rw : (y ⊔ x) ⊓ (z ⊔ x) = (y ⊔ x) ⊓ (x ⊔ z)
⊢ y ⊓ z ⊔ x = (y ⊔ x) ⊓ (x ⊔ z)
have rw₁ : (y ⊔ x) ⊓ (z ⊔ x) = (y ⊔ x) ⊓ (z ⊔ x)
Tactic: rw [sup_inf_right, sup_comm x]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : DistribLattice α
x y z : α
h₁ : x ⊓ z ≤ y ⊓ z
h₂ : x ⊔ z ≤ y ⊔ z
⊢ (y ⊔ x) ⊓ (y ⊔ z) = y ⊔ x ⊓ z
have rw : y ⊔ x ⊓ z = y ⊔ x ⊓ z
Tactic: rw [← sup_inf_left]
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ Eq.{u + 1} (α := α → α → α) (fun (x1 x2 : α) ↦ x1 ⊔ x2) maxDefault
have h : ∀ (x y : α), x ⊔ y = maxDefault x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
⊢ x ⊔ y = if x ≤ y then y else x
have pos : ∀ (h' : x ≤ y), x ⊔ y = y
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeSup α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
pos : ∀ (h' : x ≤ y), x ⊔ y = y
⊢ x ⊔ y = if x ≤ y then y else x
have neg : ∀ (h' : ¬x ≤ y), x ⊔ y = x
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
⊢ Eq.{u + 1} (α := α → α → α) (fun (x1 x2 : α) ↦ x1 ⊓ x2) minDefault
have h : ∀ (x y : α), x ⊓ y = minDefault x y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
⊢ x ⊓ y = if x ≤ y then x else y
have pos : ∀ (h' : x ≤ y), x ⊓ y = x
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
inst : SemilatticeInf α
inst_1 : DecidableLE α
inst_2 : Std.Total fun (x1 x2 : α) ↦ x1 ≤ x2
x y : α
pos : ∀ (h' : x ≤ y), x ⊓ y = x
⊢ x ⊓ y = if x ≤ y then x else y
have neg : ∀ (h' : ¬x ≤ y), x ⊓ y = y
Tactic: split_ifs with h'
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
⊢ update (β := π) f i (a ⊔ b) j = (update (β := π) f i a ⊔ update (β := π) f i b) j
have inl : ∀ (a b : π j), update (β := π) f j (a ⊔ b) j = (update (β := π) f j a ⊔ update (β := π) f j b) j
Tactic: obtain rfl | hji := eq_or_ne j i
Cleared hypotheses: i, a, b
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
ι : Type u_1
π : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → SemilatticeSup (π i)
f : (i : ι) → π i
i : ι
a b : π i
j : ι
inl : ∀ (a b : π j), update (β := π) f j (a ⊔ b) j = (update (β := π) f j a ⊔ update (β := π) f j b) j
⊢ update (β := π) f i (a ⊔ b) j = (update (β := π) f i a ⊔ update (β := π) f i b) j
have inr : ∀ (hji : j ≠ i), update (β := π) f i (a ⊔ b) j = (update (β := π) f i a ⊔ update (β := π) f i b) j
Tactic: obtain rfl | hji := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Order.Lattice (goal)
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : Preorder β
f : α → β
h : ∀ (x y : α), f x ≤ f (x ⊔ y)
x y : α
hxy : x ≤ y
⊢ f x ≤ f y
have rw : f x ≤ f (x ⊔ y)
Tactic: rw [← sup_eq_right.2 hxy]