awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderBot A
K : A
simp_rw : (K ≠ ⊥ ∧ ∀ b < K, b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₁ : (K ≠ ⊥ ∧ ∀ (b : A), b ≤ K ∧ ¬K ≤ b → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₂ :
  (K ≠ ⊥ ∧ ∀ (b : A), (b ≤ K ∧ ∃ x ∈ K, x ∉ b) → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₃ :
  (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) ∧ b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
have simp_rw₄ : (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
Tactic: simp_rw [IsAtom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderBot A
K : A
simp_rw : (K ≠ ⊥ ∧ ∀ b < K, b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₁ : (K ≠ ⊥ ∧ ∀ (b : A), b ≤ K ∧ ¬K ≤ b → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₂ :
  (K ≠ ⊥ ∧ ∀ (b : A), (b ≤ K ∧ ∃ x ∈ K, x ∉ b) → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₃ :
  (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) ∧ b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₄ :
  (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
have simp_rw₅ : (K ≠ ⊥ ∧ ∀ (b : A) (x : B), x ∈ K ∧ x ∉ b → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
Tactic: simp_rw [IsAtom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderBot A
K : A
simp_rw : (K ≠ ⊥ ∧ ∀ b < K, b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₁ : (K ≠ ⊥ ∧ ∀ (b : A), b ≤ K ∧ ¬K ≤ b → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₂ :
  (K ≠ ⊥ ∧ ∀ (b : A), (b ≤ K ∧ ∃ x ∈ K, x ∉ b) → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₃ :
  (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) ∧ b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₄ :
  (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₅ :
  (K ≠ ⊥ ∧ ∀ (b : A) (x : B), x ∈ K ∧ x ∉ b → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
have simp_rw₆ : (K ≠ ⊥ ∧ ∀ (b : A) (x : B), (x ∈ K ∧ x ∉ b) ∧ b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K ∧ g ∉ H ∧ g ∈ K → H = ⊥
Tactic: simp_rw [IsAtom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderTop A
K : A
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
have simp_rw : (K ≠ ⊤ ∧ ∀ (b : A), K < b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic: simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderTop A
K : A
simp_rw : (K ≠ ⊤ ∧ ∀ (b : A), K < b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
have simp_rw₁ : (K ≠ ⊤ ∧ ∀ (b : A), K ≤ b ∧ ¬b ≤ K → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic: simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderTop A
K : A
simp_rw : (K ≠ ⊤ ∧ ∀ (b : A), K < b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₁ : (K ≠ ⊤ ∧ ∀ (b : A), K ≤ b ∧ ¬b ≤ K → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
have simp_rw₂ : (K ≠ ⊤ ∧ ∀ (b : A), (K ≤ b ∧ ∃ x ∈ b, x ∉ K) → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic: simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderTop A
K : A
simp_rw : (K ≠ ⊤ ∧ ∀ (b : A), K < b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₁ : (K ≠ ⊤ ∧ ∀ (b : A), K ≤ b ∧ ¬b ≤ K → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₂ :
  (K ≠ ⊤ ∧ ∀ (b : A), (K ≤ b ∧ ∃ x ∈ b, x ∉ K) → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
have simp_rw₃ : (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) ∧ K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic: simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderTop A
K : A
simp_rw : (K ≠ ⊤ ∧ ∀ (b : A), K < b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₁ : (K ≠ ⊤ ∧ ∀ (b : A), K ≤ b ∧ ¬b ≤ K → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₂ :
  (K ≠ ⊤ ∧ ∀ (b : A), (K ≤ b ∧ ∃ x ∈ b, x ∉ K) → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₃ :
  (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) ∧ K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
have simp_rw₄ : (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic: simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderTop A
K : A
simp_rw : (K ≠ ⊤ ∧ ∀ (b : A), K < b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₁ : (K ≠ ⊤ ∧ ∀ (b : A), K ≤ b ∧ ¬b ≤ K → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₂ :
  (K ≠ ⊤ ∧ ∀ (b : A), (K ≤ b ∧ ∃ x ∈ b, x ∉ K) → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₃ :
  (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) ∧ K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₄ :
  (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
have simp_rw₅ : (K ≠ ⊤ ∧ ∀ (b : A) (x : B), x ∈ b ∧ x ∉ K → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
Tactic: simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderTop A
K : A
simp_rw : (K ≠ ⊤ ∧ ∀ (b : A), K < b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₁ : (K ≠ ⊤ ∧ ∀ (b : A), K ≤ b ∧ ¬b ≤ K → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₂ :
  (K ≠ ⊤ ∧ ∀ (b : A), (K ≤ b ∧ ∃ x ∈ b, x ∉ K) → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₃ :
  (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) ∧ K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₄ :
  (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₅ :
  (K ≠ ⊤ ∧ ∀ (b : A) (x : B), x ∈ b ∧ x ∉ K → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
have simp_rw₆ : (K ≠ ⊤ ∧ ∀ (b : A) (x : B), (x ∈ b ∧ x ∉ K) ∧ K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H ∧ g ∉ K ∧ g ∈ H → H = ⊤
Tactic: simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L
have refine : K < L → ∀ (H : A), K < H → ¬H < L ↔ ∀ (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L
Tactic: refine and_congr_right fun _ ↦ forall_congr' fun H ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
⊢ K < H → ¬H < L ↔ ∀ (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L
have contrapose! : K < H ∧ H < L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
⊢ K < H ∧ H < L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
Tactic: rw [lt_iff_le_not_ge, lt_iff_le_and_ne, and_and_and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have simp_rw₁ : K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have simp_rw₂ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x ∉ K, x ∈ H ∧ H ≠ L)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₂ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x ∉ K, x ∈ H ∧ H ≠ L)
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have simp_rw₃ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ (x : B), (x ∉ K ∧ x ∈ H) ∧ H ≠ L)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₂ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x ∉ K, x ∈ H ∧ H ≠ L)
simp_rw₃ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ (x : B), (x ∉ K ∧ x ∈ H) ∧ H ≠ L)
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have simp_rw₄ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ ∃ (x : B), H ≠ L ∧ x ∉ K ∧ x ∈ H)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₂ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x ∉ K, x ∈ H ∧ H ≠ L)
simp_rw₃ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ (x : B), (x ∉ K ∧ x ∈ H) ∧ H ≠ L)
simp_rw₄ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ ∃ (x : B), H ≠ L ∧ x ∉ K ∧ x ∈ H)
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have simp_rw₅ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₂ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x ∉ K, x ∈ H ∧ H ≠ L)
simp_rw₃ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ (x : B), (x ∉ K ∧ x ∈ H) ∧ H ≠ L)
simp_rw₄ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ ∃ (x : B), H ≠ L ∧ x ∉ K ∧ x ∈ H)
simp_rw₅ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have simp_rw₆ : K ≤ H → H ≤ L → ((H ≠ L ∧ ∃ x ∈ H, x ∉ K) ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₂ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x ∉ K, x ∈ H ∧ H ≠ L)
simp_rw₃ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ (x : B), (x ∉ K ∧ x ∈ H) ∧ H ≠ L)
simp_rw₄ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ ∃ (x : B), H ≠ L ∧ x ∉ K ∧ x ∈ H)
simp_rw₅ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)
simp_rw₆ : K ≤ H → H ≤ L → ((H ≠ L ∧ ∃ x ∈ H, x ∉ K) ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
have simp_rw₇ : K ≤ H → H ≤ L → True
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K
have refine : K < L → ∀ (H : A), ¬(K < H → ¬H < L) ↔ ¬∀ (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K
Tactic: refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
⊢ ¬(K < H → ¬H < L) ↔ ¬∀ (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K
have push : K < H ∧ H < L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
Tactic: push Not
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
⊢ K < H ∧ H < L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
Tactic: rw [lt_iff_le_and_ne, lt_iff_le_not_ge, and_and_and_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have simp_rw₁ : K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have simp_rw₂ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x ∉ H, x ∈ L ∧ H ≠ K)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₂ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x ∉ H, x ∈ L ∧ H ≠ K)
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have simp_rw₃ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), (x ∉ H ∧ x ∈ L) ∧ H ≠ K)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₂ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x ∉ H, x ∈ L ∧ H ≠ K)
simp_rw₃ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), (x ∉ H ∧ x ∈ L) ∧ H ≠ K)
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have simp_rw₄ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), H ≠ K ∧ x ∈ L ∧ x ∉ H)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₂ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x ∉ H, x ∈ L ∧ H ≠ K)
simp_rw₃ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), (x ∉ H ∧ x ∈ L) ∧ H ≠ K)
simp_rw₄ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), H ≠ K ∧ x ∈ L ∧ x ∉ H)
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have simp_rw₅ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₂ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x ∉ H, x ∈ L ∧ H ≠ K)
simp_rw₃ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), (x ∉ H ∧ x ∈ L) ∧ H ≠ K)
simp_rw₄ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), H ≠ K ∧ x ∈ L ∧ x ∉ H)
simp_rw₅ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have simp_rw₆ : K ≤ H → H ≤ L → ((K ≠ H ∧ ∃ x ∈ L, x ∉ H) ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₂ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x ∉ H, x ∈ L ∧ H ≠ K)
simp_rw₃ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), (x ∉ H ∧ x ∈ L) ∧ H ≠ K)
simp_rw₄ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), H ≠ K ∧ x ∈ L ∧ x ∉ H)
simp_rw₅ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)
simp_rw₆ : K ≤ H → H ≤ L → ((K ≠ H ∧ ∃ x ∈ L, x ∉ H) ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
have simp_rw₇ : K ≤ H → H ≤ L → True
Tactic: simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
a : α
b : (↑(Ici a) : Type u_2)
⊢ IsAtom b ↔ a ⋖ (↑b : α)
have rw : ⊥ ⋖ b ↔ a ⋖ (↑b : α)
Tactic: rw [← bot_covBy_iff]