awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a b : α
h : a ≠ b
inl : ∀ (h : ⊥ ≠ b), Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤
have inr : ∀ (h : ⊤ ≠ b), Ne.{u_2 + 1} (α := α) ⊥ ⊤
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
b : α
h : ⊥ ≠ b
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤
have inl : ∀ (h : Ne.{u_2 + 1} (α := α) ⊥ ⊥), Ne.{u_2 + 1} (α := α) ⊥ ⊤
Tactic: rcases eq_bot_or_eq_top b with (rfl | rfl)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
b : α
h : ⊥ ≠ b
inl : ∀ (h : Ne.{u_2 + 1} (α := α) ⊥ ⊥), Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤
have inl₁ : ∀ (h : Ne.{u_2 + 1} (α := α) ⊥ ⊤), Ne.{u_2 + 1} (α := α) ⊥ ⊤
Tactic: rcases eq_bot_or_eq_top b with (rfl | rfl)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
b : α
h : ⊤ ≠ b
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤
have inr : ∀ (h : Ne.{u_2 + 1} (α := α) ⊤ ⊥), Ne.{u_2 + 1} (α := α) ⊥ ⊤
Tactic: rcases eq_bot_or_eq_top b with (rfl | rfl)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
b : α
h : ⊤ ≠ b
inr : ∀ (h : Ne.{u_2 + 1} (α := α) ⊤ ⊥), Ne.{u_2 + 1} (α := α) ⊥ ⊤
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤
have inr₁ : ∀ (h : Ne.{u_2 + 1} (α := α) ⊤ ⊤), Ne.{u_2 + 1} (α := α) ⊥ ⊤
Tactic: rcases eq_bot_or_eq_top b with (rfl | rfl)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
a : α
⊢ a ≤ a
have inl : LE.le.{u_4} (α := α) ⊥ ⊥
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
a : α
inl : LE.le.{u_4} (α := α) ⊥ ⊥
⊢ a ≤ a
have inr : LE.le.{u_4} (α := α) ⊤ ⊤
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
a b c : α
⊢ a ≤ b → b ≤ c → a ≤ c
have inl : ⊥ ≤ b → b ≤ c → ⊥ ≤ c
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
a b c : α
inl : ⊥ ≤ b → b ≤ c → ⊥ ≤ c
⊢ a ≤ b → b ≤ c → a ≤ c
have inr : ⊤ ≤ b → b ≤ c → ⊤ ≤ c
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
b c : α
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c
have inr : LE.le.{u_4} (α := α) ⊤ ⊥ → ⊥ ≤ c → ⊤ ≤ c
Tactic: rcases eq_bot_or_eq_top b with (rfl | rfl)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
b c : α
inr : LE.le.{u_4} (α := α) ⊤ ⊥ → ⊥ ≤ c → ⊤ ≤ c
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c
have inr₁ : LE.le.{u_4} (α := α) ⊤ ⊤ → ⊤ ≤ c → ⊤ ≤ c
Tactic: rcases eq_bot_or_eq_top b with (rfl | rfl)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
c : α
⊢ LE.le.{u_4} (α := α) ⊤ ⊥ → ⊥ ≤ c → ⊤ ≤ c
have inr : LE.le.{u_4} (α := α) ⊤ ⊥ → LE.le.{u_4} (α := α) ⊥ ⊥ → LE.le.{u_4} (α := α) ⊤ ⊥
Tactic: rcases eq_bot_or_eq_top c with (rfl | rfl)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
inst_1 : BoundedOrder α_1
inst_2 : IsSimpleOrder α_1
α : Type u_4
inst_3 : LE α
inst_4 : BoundedOrder α
inst_5 : IsSimpleOrder α
c : α
inr : LE.le.{u_4} (α := α) ⊤ ⊥ → LE.le.{u_4} (α := α) ⊥ ⊥ → LE.le.{u_4} (α := α) ⊤ ⊥
⊢ LE.le.{u_4} (α := α) ⊤ ⊥ → ⊥ ≤ c → ⊤ ≤ c
have inr₁ : LE.le.{u_4} (α := α) ⊤ ⊥ → LE.le.{u_4} (α := α) ⊥ ⊤ → LE.le.{u_4} (α := α) ⊤ ⊤
Tactic: rcases eq_bot_or_eq_top c with (rfl | rfl)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
a b : α
⊢ a ≤ b ∨ b ≤ a
have inl : ⊥ ≤ b ∨ b ≤ ⊥
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
a b : α
inl : ⊥ ≤ b ∨ b ≤ ⊥
⊢ a ≤ b ∨ b ≤ a
have inr : ⊤ ≤ b ∨ b ≤ ⊤
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
x y z : α
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
have inl : (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
x y z : α
inl : (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
have inr : (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : LE α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
⊢ (fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) x) = x
have inl : Eq.{u_4 + 1} (α := α)
  ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) ⊥)) ⊥
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : LE α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
inl :
  Eq.{u_4 + 1} (α := α)
    ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) ⊥)) ⊥
⊢ (fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) x) = x
have inr : Eq.{u_4 + 1} (α := α)
  ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) ((fun (x : α) ↦ decide (x = ⊤)) ⊤)) ⊤
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : LE α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : Bool
⊢ (fun (x : α) ↦ decide (x = ⊤)) ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) x) = x
have false : (fun (x : α) ↦ decide (x = ⊤)) ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) false) =
  false
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : LE α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : Bool
false :
  (fun (x : α) ↦ decide (x = ⊤))
      ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) Bool.false) =
    Bool.false
⊢ (fun (x : α) ↦ decide (x = ⊤)) ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) x) = x
have true : (fun (x : α) ↦ decide (x = ⊤)) ((fun (x : Bool) ↦ (Bool.casesOn (motive := fun (x : Bool) ↦ α) x ⊥ ⊤ : α)) true) = true
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : PartialOrder α
inst_2 : BoundedOrder α
inst_3 : IsSimpleOrder α
a b : α
⊢ LE.le (α := Bool) ((equivBool : (a : α) → Bool) a : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ a ≤ b
have inl : LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊥ : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ ⊥ ≤ b
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : PartialOrder α
inst_2 : BoundedOrder α
inst_3 : IsSimpleOrder α
a b : α
inl : LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊥ : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ ⊥ ≤ b
⊢ LE.le (α := Bool) ((equivBool : (a : α) → Bool) a : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ a ≤ b
have inr : LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ ⊤ ≤ b
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : PartialOrder α
inst_2 : BoundedOrder α
inst_3 : IsSimpleOrder α
b : α
⊢ LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ ⊤ ≤ b
have inr : LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) ⊥ : Bool) ↔
  LE.le.{u_2} (α := α) ⊤ ⊥
Tactic: rcases eq_bot_or_eq_top b with (rfl | rfl)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : DecidableEq α
inst_1 : PartialOrder α
inst_2 : BoundedOrder α
inst_3 : IsSimpleOrder α
b : α
inr :
  LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) ⊥ : Bool) ↔
    LE.le.{u_2} (α := α) ⊤ ⊥
⊢ LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) b : Bool) ↔ ⊤ ≤ b
have inr₁ : LE.le (α := Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ((equivBool : (a : α) → Bool) ⊤ : Bool) ↔
  LE.le.{u_2} (α := α) ⊤ ⊤
Tactic: rcases eq_bot_or_eq_top b with (rfl | rfl)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
⊢ (x ⊓ if x = ⊥ then ⊤ else ⊥) ≤ ⊥
have inl : LE.le.{u_4} (α := α) (⊥ ⊓ if Eq.{u_4 + 1} (α := α) ⊥ ⊥ then ⊤ else ⊥) ⊥
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
inl : LE.le.{u_4} (α := α) (⊥ ⊓ if Eq.{u_4 + 1} (α := α) ⊥ ⊥ then ⊤ else ⊥) ⊥
⊢ (x ⊓ if x = ⊥ then ⊤ else ⊥) ≤ ⊥
have inr : LE.le.{u_4} (α := α) (⊤ ⊓ if Eq.{u_4 + 1} (α := α) ⊤ ⊥ then ⊤ else ⊥) ⊥
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
⊢ ⊤ ≤ x ⊔ if x = ⊥ then ⊤ else ⊥
have inl : LE.le.{u_4} (α := α) ⊤ (⊥ ⊔ if Eq.{u_4 + 1} (α := α) ⊥ ⊥ then ⊤ else ⊥)
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x : α
inl : LE.le.{u_4} (α := α) ⊤ (⊥ ⊔ if Eq.{u_4 + 1} (α := α) ⊥ ⊥ then ⊤ else ⊥)
⊢ ⊤ ≤ x ⊔ if x = ⊥ then ⊤ else ⊥
have inr : LE.le.{u_4} (α := α) ⊤ (⊤ ⊔ if Eq.{u_4 + 1} (α := α) ⊤ ⊥ then ⊤ else ⊥)
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x y : α
⊢ (if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = x ⊓ if y = ⊥ then ⊤ else ⊥
have inl : Eq.{u_4 + 1} (α := α) (if Eq.{u_4 + 1} (α := α) ⊥ ⊤ ∧ y = ⊥ then ⊤ else ⊥) (⊥ ⊓ if y = ⊥ then ⊤ else ⊥)
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : DecidableEq α_1
inst_1 : PartialOrder α_1
inst_2 : BoundedOrder α_1
inst_3 : IsSimpleOrder α_1
α : Type u_4
inst_4 : DecidableEq α
inst_5 : Lattice α
inst_6 : BoundedOrder α
inst_7 : IsSimpleOrder α
x y : α
inl : Eq.{u_4 + 1} (α := α) (if Eq.{u_4 + 1} (α := α) ⊥ ⊤ ∧ y = ⊥ then ⊤ else ⊥) (⊥ ⊓ if y = ⊥ then ⊤ else ⊥)
⊢ (if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = x ⊓ if y = ⊥ then ⊤ else ⊥
have inr : Eq.{u_4 + 1} (α := α) (if Eq.{u_4 + 1} (α := α) ⊤ ⊤ ∧ y = ⊥ then ⊤ else ⊥) (⊤ ⊓ if y = ⊥ then ⊤ else ⊥)
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
⊢ IsLUB s (if ⊤ ∈ s then ⊤ else ⊥)
have refine_1 : ∀ (x : α) (h : x ∈ s), x ≤ if ⊤ ∈ s then ⊤ else ⊥
Tactic: refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
refine_1 : ∀ (x : α) (h : x ∈ s), x ≤ if ⊤ ∈ s then ⊤ else ⊥
⊢ IsLUB s (if ⊤ ∈ s then ⊤ else ⊥)
have refine_2 : ∀ (x : α) (h : x ∈ upperBounds s), (if ⊤ ∈ s then ⊤ else ⊥) ≤ x
Tactic: refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ x ≤ if ⊤ ∈ s then ⊤ else ⊥
have refine_1 : ∀ (h : ⊥ ∈ s), LE.le.{u_2} (α := α) ⊥ (if ⊤ ∈ s then ⊤ else ⊥)
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
refine_1 : ∀ (h : ⊥ ∈ s), LE.le.{u_2} (α := α) ⊥ (if ⊤ ∈ s then ⊤ else ⊥)
⊢ x ≤ if ⊤ ∈ s then ⊤ else ⊥
have refine_1₁ : ∀ (h : ⊤ ∈ s), LE.le.{u_2} (α := α) ⊤ (if ⊤ ∈ s then ⊤ else ⊥)
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ LE.le.{u_2} (α := α) ⊤ (if ⊤ ∈ s then ⊤ else ⊥)
have refine_1 : LE.le.{u_2} (α := α) ⊤ ⊤
Tactic: rw [if_pos h]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ x
have refine_2 : ∀ (h : ⊥ ∈ upperBounds s), LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊥
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
refine_2 : ∀ (h : ⊥ ∈ upperBounds s), LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊥
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ x
have refine_2₁ : ∀ (h : ⊤ ∈ upperBounds s), LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊤
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊥ ∈ upperBounds s
⊢ LE.le.{u_2} (α := α) (if ⊤ ∈ s then ⊤ else ⊥) ⊥
have refine_2 : ⊤ ∉ s
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
⊢ IsGLB s (if ⊥ ∈ s then ⊥ else ⊤)
have refine_1 : ∀ (x : α) (h : x ∈ s), (if ⊥ ∈ s then ⊥ else ⊤) ≤ x
Tactic: refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
refine_1 : ∀ (x : α) (h : x ∈ s), (if ⊥ ∈ s then ⊥ else ⊤) ≤ x
⊢ IsGLB s (if ⊥ ∈ s then ⊥ else ⊤)
have refine_2 : ∀ (x : α) (h : x ∈ lowerBounds s), x ≤ if ⊥ ∈ s then ⊥ else ⊤
Tactic: refine ⟨fun x h ↦ ?_, fun x h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ x
have refine_1 : ∀ (h : ⊥ ∈ s), LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊥
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
refine_1 : ∀ (h : ⊥ ∈ s), LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊥
⊢ (if ⊥ ∈ s then ⊥ else ⊤) ≤ x
have refine_1₁ : ∀ (h : ⊤ ∈ s), LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊤
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊥ ∈ s
⊢ LE.le.{u_2} (α := α) (if ⊥ ∈ s then ⊥ else ⊤) ⊥
have refine_1 : LE.le.{u_2} (α := α) ⊥ ⊥
Tactic: rw [if_pos h]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ lowerBounds s
⊢ x ≤ if ⊥ ∈ s then ⊥ else ⊤
have refine_2 : ∀ (h : ⊥ ∈ lowerBounds s), LE.le.{u_2} (α := α) ⊥ (if ⊥ ∈ s then ⊥ else ⊤)
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
x : α
h : x ∈ lowerBounds s
refine_2 : ∀ (h : ⊥ ∈ lowerBounds s), LE.le.{u_2} (α := α) ⊥ (if ⊥ ∈ s then ⊥ else ⊤)
⊢ x ≤ if ⊥ ∈ s then ⊥ else ⊤
have refine_2₁ : ∀ (h : ⊤ ∈ lowerBounds s), LE.le.{u_2} (α := α) ⊤ (if ⊥ ∈ s then ⊥ else ⊤)
Tactic: rcases eq_bot_or_eq_top x with (rfl | rfl)
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
s : Set α
h : ⊤ ∈ lowerBounds s
⊢ LE.le.{u_2} (α := α) ⊤ (if ⊥ ∈ s then ⊥ else ⊤)
have refine_2 : ⊥ ∉ s
Tactic: rw [if_neg]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
f : β ↪o α
hbot : Eq.{u_2 + 1} (α := α) ((f : (a : β) → α) ⊥ : α) (⊥ : α)
b : β
hb : IsAtom.{u_2} (α := α) ((f : (a : β) → α) b : α)
⊢ IsAtom b
have simp : ∀ (hb : CovBy.{u_2} (α := α) (⊥ : α) ((f : (a : β) → α) b : α)), ⊥ ⋖ b
Tactic: simp only [← bot_covBy_iff] at hb ⊢
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
⊢ IsAtom (l a) ↔ IsAtom a
have refine : ∀ (hla : IsAtom (l a)), IsAtom a
Tactic: refine ⟨fun hla => ?_, fun ha => gi.isAtom_of_u_bot hbot ((h_atom a ha).symm ▸ ha)⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
⊢ IsAtom a
have obtain : ∀ (a' : α) (ha' : IsAtom a') (hab' : a' ≤ u (l a)), IsAtom a
Tactic: obtain ⟨a', ha', hab'⟩ :=
    (eq_bot_or_exists_atom_le (u (l a))).resolve_left (hbot ▸ fun h => hla.1 (gi.u_injective h))
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
⊢ IsAtom a
have this : l a' = l a
Tactic: have :=
    (hla.le_iff.mp <| (gi.l_u_eq (l a) ▸ gi.gc.monotone_l hab' : l a' ≤ l a)).resolve_left fun h =>
      ha'.1 (hbot ▸ h_atom a' ha' ▸ congr_arg u h)
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
this : l a' = l a
⊢ IsAtom a
have haa' : a = a'
Tactic: have haa' : a = a' :=
    (ha'.le_iff.mp <|
          (gi.gc.le_u_l a).trans_eq (h_atom a' ha' ▸ congr_arg u this.symm)).resolve_left
      (mt (congr_arg l) (gi.gc.l_bot.symm ▸ hla.1))
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
⊢ IsAtom (u b) ↔ IsAtom b
have rw : IsAtom (l (u b)) ↔ IsAtom b
Tactic: rw [← gi.isAtom_iff hbot h_atom, gi.l_u_eq]