awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.DirectedInverseSystem (goal)
Goal:
ι : Type u_6
F : ι → Type u_7
X : ι → Type u_8
inst : LinearOrder ι
f : ⦃i j : ι⦄ → i ≤ j → F j → F i
inst_1 : WellFoundedLT ι
inst_2 : SuccOrder ι
inst_3 : InverseSystem (F := F) f
equivSucc :
  (i : ι) →
    ¬IsMax i → { e : F i⁺ ≃ Prod.{u_7, u_8} (F i) (X i) // ∀ (x : F i⁺), ((e : (a : F i⁺) → F i × X i) x).1 = f ⋯ x }
equivLim :
  (i : ι) →
    IsSuccPrelimit i →
      { e : F i ≃ (↑(limit (F := F) f i) : Type (max u_6 u_7)) //
        ∀ (x : F i) (l : (↑(Iio i) : Type u_6)),
          (↑((e : (a : F i) → (↑(limit f i) : Type (max u_6 u_7))) x) : (l : (↑(Iio i) : Type u_6)) → F (↑l : ι)) l =
            f ⋯ x }
i j : ι
h : i ≤ j
x : F j
⊢ Eq (α := piLT X i) ((globalEquiv (F := F) (X := X) equivSucc equivLim i : (a : F i) → piLT X i) (f h x) : piLT X i)
    (piLTProj (X := X) h ((globalEquiv (F := F) (X := X) equivSucc equivLim j : (a : F j) → piLT X j) x) : piLT X i)
have refine : globalEquiv (F := F) (X := X) equivSucc equivLim i =
  (globalEquivAux (F := F) (X := X) equivSucc equivLim j).equiv (F := F) (X := X) (s := Iic j)
    (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic j) i h)
Tactic: refine (DFunLike.congr_fun ?_ _).trans ((globalEquivAux equivSucc equivLim j).nat le_rfl h h x)
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
ha : a ≠ ⊥
hab : Disjoint a b
h : a = b
⊢ Disjoint a a
have rwa : ∀ (hab : Disjoint a a) (h : a = b), Disjoint a a
Tactic: rwa [← h] at hab
Cleared hypotheses: hab, h
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
inst_1 : OrderBot α
pr : α → Prop
Pinf : ∀ ⦃s t : α⦄, pr s → pr t → pr (s ⊓ t)
hbot : pr ⊥
a b : Subtype pr
this_1 : SemilatticeInf (Subtype pr) := Subtype.semilatticeInf (P := pr) Pinf
this : OrderBot (Subtype pr) := Subtype.orderBot (p := pr) hbot
⊢ Disjoint a b ↔ Disjoint (↑a : α) (↑b : α)
have rw : a ⊓ b = ⊥ ↔ (↑(a ⊓ b) : α) = (↑⊥ : α)
Tactic: rw [disjoint_iff, disjoint_iff, ← Subtype.coe_inf Pinf, ← Subtype.coe_bot hbot]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b c : α
hab : Disjoint a b
hbc : Codisjoint b c
⊢ a ≤ c
have rw : a ⊓ (b ⊔ c) ≤ (a ⊔ c) ⊓ (b ⊔ c)
Tactic: rw [← @inf_top_eq _ _ _ a, ← @bot_sup_eq _ _ _ c, ← hab.eq_bot, ← hbc.eq_top, sup_inf_right]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b x y : α
h : IsCompl x y
hle : a ≤ b ⊔ y
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x
have rw : b ⊓ x ⊔ ⊥ = b ⊓ x
Tactic: rw [h.symm.inf_eq_bot, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
⊢ b ⊓ x ⊔ y ⊓ x = b ⊓ x
have rw₁ : b ⊓ x = b ⊓ x
Tactic: rw [h.symm.inf_eq_bot, sup_bot_eq]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z
have rw : x ⊓ y ≤ ⊥ ↔ x ≤ z
Tactic: rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
rw : x ⊓ y ≤ ⊥ ↔ x ≤ z
⊢ x ⊓ y = ⊥ ↔ x ≤ z
have rw₁ : x ≤ ⊥ ⊔ z ↔ x ≤ z
Tactic: rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
⊢ x ⊓ y = ⊥ ↔ x ≤ z
have rw₂ : x ≤ z ↔ x ≤ z
Tactic: rw [← le_bot_iff, ← h.le_sup_right_iff_inf_left_le, bot_sup_eq]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ Disjoint x y ↔ x ≤ z
have rw : x ⊓ y = ⊥ ↔ x ≤ z
Tactic: rw [disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
have rw : x ⊓ (y ⊓ y') ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊥
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
have rw₁ : x ⊓ y ⊓ y' ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊥
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
have rw₂ : ⊥ ⊓ y' ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊥
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
have rw₃ : ⊥ ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊥
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
have rw₄ : 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊥
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
have rw₅ : y ⊓ (x' ⊓ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊥
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
have rw₆ : 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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 ⊓ ⊥ = ⊥
⊢ (x ⊔ x') ⊓ (y ⊓ y') = ⊥
have rw₇ : Eq.{u_1 + 1} (α := α) ⊥ ⊥
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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
x y x' y' : α
h : IsCompl x y
h' : IsCompl x' y'
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw : (x ⊔ x' ⊔ y) ⊓ (x ⊔ x' ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₁ : (x' ⊔ x ⊔ y) ⊓ (x' ⊔ x ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₂ : (x' ⊔ (x ⊔ y)) ⊓ (x' ⊔ x ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₃ : (x' ⊔ ⊤) ⊓ (x' ⊔ x ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₄ : ⊤ ⊓ (x' ⊔ x ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₅ : x' ⊔ x ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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' = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₆ : x' ⊔ (x ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₇ : x ⊔ (x' ⊔ 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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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') = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₈ : x ⊔ ⊤ = ⊤
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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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 ⊔ ⊤ = ⊤
⊢ x ⊔ x' ⊔ y ⊓ y' = ⊤
have rw₉ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
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]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
x y : α × β
⊢ Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
have mp : Disjoint x y → Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
⊢ Disjoint x y ↔ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
have mpr : Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd → Disjoint x y
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
have mp : ∀ (a : α) (hx : a ≤ x.fst) (hy : a ≤ y.fst), snd (a, ⊥) ≤ x.snd
Tactic: refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
have mp₁ : ∀ (a : α) (hx : a ≤ x.fst) (hy : a ≤ y.fst), snd (a, ⊥) ≤ y.snd
Tactic: refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
have mp₂ : ∀ (b : β) (hx : b ≤ x.snd) (hy : b ≤ y.snd), fst (⊥, b) ≤ x.fst
Tactic: refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
⊢ Disjoint x.fst y.fst ∧ Disjoint x.snd y.snd
have mp₃ : ∀ (b : β) (hx : b ≤ x.snd) (hy : b ≤ y.snd), fst (⊥, b) ≤ y.fst
Tactic: refine ⟨fun a hx hy ↦ (@h (a, ⊥) ⟨hx, ?_⟩ ⟨hy, ?_⟩).1,
      fun b hx hy ↦ (@h (⊥, b) ⟨?_, hx⟩ ⟨?_, hy⟩).2⟩
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
x y : α × β
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd
have 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
Tactic: simp_rw [isCompl_iff, Prod.disjoint_iff, Prod.codisjoint_iff, and_and_and_comm]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd
have 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
Tactic: simp_rw [isCompl_iff, Prod.disjoint_iff, Prod.codisjoint_iff, and_and_and_comm]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
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
⊢ IsCompl x y ↔ IsCompl x.fst y.fst ∧ IsCompl x.snd y.snd
have 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
Tactic: simp_rw [isCompl_iff, Prod.disjoint_iff, Prod.codisjoint_iff, and_and_and_comm]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x : α
h : IsCompl x ⊥
⊢ x = ⊤
have rw : x ⊔ ⊥ = ⊤
Tactic: rw [← sup_bot_eq x, h.sup_eq_top]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
x : α
h : IsCompl x ⊥
rw : x ⊔ ⊥ = ⊤
⊢ x = ⊤
have rw₁ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: rw [← sup_bot_eq x, h.sup_eq_top]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Subsingleton α
⊢ ComplementedLattice α
have refine : ∀ (a : α), Codisjoint a ⊥
Tactic: refine ⟨fun a ↦ ⟨⊥, disjoint_bot_right, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : Subsingleton α
a : α
⊢ Codisjoint a ⊥
have rw : Codisjoint a ⊤
Tactic: rw [Subsingleton.elim ⊥ ⊤]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ Disjoint (↑a : α) (↑b : α) ↔ Disjoint a b
have rw : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ Disjoint a b
Tactic: rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ Disjoint a b
⊢ Disjoint (↑a : α) (↑b : α) ↔ Disjoint a b
have rw₁ : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ a ⊓ b = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ Disjoint a b
rw₁ : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ a ⊓ b = ⊥
⊢ Disjoint (↑a : α) (↑b : α) ↔ Disjoint a b
have rw₂ : (↑(a ⊓ b) : α) = ⊥ ↔ a ⊓ b = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ Disjoint a b
rw₁ : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ a ⊓ b = ⊥
rw₂ : (↑(a ⊓ b) : α) = ⊥ ↔ a ⊓ b = ⊥
⊢ Disjoint (↑a : α) (↑b : α) ↔ Disjoint a b
have rw₃ : (↑(a ⊓ b) : α) = (↑⊥ : α) ↔ a ⊓ b = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ Disjoint a b
rw₁ : (↑a : α) ⊓ (↑b : α) = ⊥ ↔ a ⊓ b = ⊥
rw₂ : (↑(a ⊓ b) : α) = ⊥ ↔ a ⊓ b = ⊥
rw₃ : (↑(a ⊓ b) : α) = (↑⊥ : α) ↔ a ⊓ b = ⊥
⊢ Disjoint (↑a : α) (↑b : α) ↔ Disjoint a b
have rw₄ : a ⊓ b = ⊥ ↔ a ⊓ b = ⊥
Tactic: rw [disjoint_iff, disjoint_iff, ← coe_inf, ← coe_bot, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ Codisjoint (↑a : α) (↑b : α) ↔ Codisjoint a b
have rw : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ Codisjoint a b
Tactic: rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ Codisjoint a b
⊢ Codisjoint (↑a : α) (↑b : α) ↔ Codisjoint a b
have rw₁ : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ a ⊔ b = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ Codisjoint a b
rw₁ : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ a ⊔ b = ⊤
⊢ Codisjoint (↑a : α) (↑b : α) ↔ Codisjoint a b
have rw₂ : (↑(a ⊔ b) : α) = ⊤ ↔ a ⊔ b = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ Codisjoint a b
rw₁ : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ a ⊔ b = ⊤
rw₂ : (↑(a ⊔ b) : α) = ⊤ ↔ a ⊔ b = ⊤
⊢ Codisjoint (↑a : α) (↑b : α) ↔ Codisjoint a b
have rw₃ : (↑(a ⊔ b) : α) = (↑⊤ : α) ↔ a ⊔ b = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
rw : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ Codisjoint a b
rw₁ : (↑a : α) ⊔ (↑b : α) = ⊤ ↔ a ⊔ b = ⊤
rw₂ : (↑(a ⊔ b) : α) = ⊤ ↔ a ⊔ b = ⊤
rw₃ : (↑(a ⊔ b) : α) = (↑⊤ : α) ↔ a ⊔ b = ⊤
⊢ Codisjoint (↑a : α) (↑b : α) ↔ Codisjoint a b
have rw₄ : a ⊔ b = ⊤ ↔ a ⊔ b = ⊤
Tactic: rw [codisjoint_iff, codisjoint_iff, ← coe_sup, ← coe_top, coe_inj]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
⊢ IsCompl (↑a : α) (↑b : α) ↔ IsCompl a b
have simp_rw : Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α) ↔ Disjoint a b ∧ Codisjoint a b
Tactic: simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]
-- Lean 4 proof step from Mathlib.Order.Disjoint (goal)
Goal:
α : Type u_1
inst : DistribLattice α
inst_1 : BoundedOrder α
a b : Complementeds α
simp_rw : Disjoint (↑a : α) (↑b : α) ∧ Codisjoint (↑a : α) (↑b : α) ↔ Disjoint a b ∧ Codisjoint a b
⊢ IsCompl (↑a : α) (↑b : α) ↔ IsCompl a b
have simp_rw₁ : Disjoint a b ∧ Codisjoint (↑a : α) (↑b : α) ↔ Disjoint a b ∧ Codisjoint a b
Tactic: simp_rw [isCompl_iff, disjoint_coe, codisjoint_coe]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
⊢ Iio i = ∅
have rwa : (↑(Iio i) : Set ι) = ∅
Tactic: rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Disjointed (goal)
Goal:
α : Type u_1
ι : Type u_2
inst : GeneralizedBooleanAlgebra α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hn : IsMin i
rwa : (↑(Iio i) : Set ι) = ∅
⊢ Iio i = ∅
have rwa₁ : Set.Iio i = ∅
Tactic: rwa [← Finset.coe_eq_empty, coe_Iio, Set.Iio_eq_empty_iff]