awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : Ne.{u_2 + 1} (α := β) ((φ : (a : α) → β) a : β) ((φ : (a : α) → β) a' : β)
h₂ : r' ((φ : (a : α) → β) a) ((φ : (a : α) → β) a')
haa' : a = a'
⊢ Eq.{u_2 + 1} (α := β) ((φ : (a : α) → β) a : β) ((φ : (a : α) → β) a' : β)
have rw : Eq.{u_2 + 1} (α := β) ((φ : (a : α) → β) a' : β) ((φ : (a : α) → β) a' : β)
Tactic: rw [haa']
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
have rw : (s ∪ t).Pairwise rᶜ ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
Tactic: rw [IsAntichain, IsAntichain, IsAntichain, pairwise_union]
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
rw : (s ∪ t).Pairwise rᶜ ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
⊢ IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
have rw₁ : (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
Tactic: rw [IsAntichain, IsAntichain, IsAntichain, pairwise_union]
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
rw : (s ∪ t).Pairwise rᶜ ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
rw₁ : (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
⊢ IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
have rw₂ : (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
Tactic: rw [IsAntichain, IsAntichain, IsAntichain, pairwise_union]
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s t : Set α
rw : (s ∪ t).Pairwise rᶜ ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
rw₁ : (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
rw₂ : (s ∪ t).Pairwise rᶜ ↔ s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
⊢ IsAntichain r (s ∪ t) ↔ IsAntichain r s ∧ IsAntichain r t ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
have rw₃ : (s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a) ↔
  s.Pairwise rᶜ ∧ t.Pairwise rᶜ ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → rᶜ a b ∧ rᶜ b a
Tactic: rw [IsAntichain, IsAntichain, IsAntichain, pairwise_union]
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ x = y
have by_contra! : ∀ (hne : x ≠ y), False
Tactic: by_contra! hne
-- Lean 4 proof step from Mathlib.Order.Antichain (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
hs : IsChain r s
ht : IsAntichain r s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hne : x ≠ y
⊢ False
have x₁ : r x y ∨ r y x
Tactic: cases hs hx hy hne with
  | inl h => exact ht hx hy hne h
  | inr h => exact ht hy hx hne.symm h
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
ht : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun (x : α) ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun (x : α) ↦ x ∈ s) b
⊢ {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} = t
have refine : ∀ (x : α) (hx : x ∈ t), Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} x
Tactic: refine Set.ext fun x ↦ ⟨h _, fun hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
ht : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun (x : α) ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun (x : α) ↦ x ∈ s) b
x : α
hx : x ∈ t
⊢ Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} x
have obtain : ∀ (y : α) (hyx : y ≤ x) (hy : Maximal (fun (x : α) ↦ x ∈ s) y),
  Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} x
Tactic: obtain ⟨y, hyx, hy⟩ := hs x hx
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
s t : Set α
inst : Preorder α
ht : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
h : ∀ (x : α), Maximal (fun (x : α) ↦ x ∈ s) x → x ∈ t
hs : ∀ a ∈ t, ∃ b ≤ a, Maximal (fun (x : α) ↦ x ∈ s) b
x : α
hx : x ∈ t
y : α
hyx : y ≤ x
hy : Maximal (fun (x : α) ↦ x ∈ s) y
⊢ Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} x
have rwa : Membership.mem (γ := Set α) {x : α | Maximal (fun (x : α) ↦ x ∈ s) x} y
Tactic: rwa [← ht.eq (h y hy) hx hyx]
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : β
⊢ ¬r' (f a) c ∨ ¬r' (f b) c
have obtain : ∀ (c : α), ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)
Tactic: obtain ⟨c, rfl⟩ := hf c
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
e : r ≃r s
c : Set α
hc : IsMaxAntichain r c
t : Set β
ht : IsAntichain s t
hf : (⇑e : (a : α) → β) '' c ⊆ t
⊢ (⇑e : (a : α) → β) '' c = t
have rw : c = (⇑e.toEquiv (r := r) (s := s).symm : (a : β) → α) '' t
Tactic: rw [← e.coe_fn_toEquiv, ← e.toEquiv.eq_preimage_iff_image_eq, ← Equiv.image_symm_eq_preimage]
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
⊢ IsEmpty α ↔ s = ∅
have refine : ∀ (h' : s = ∅), IsEmpty α
Tactic: refine ⟨fun _ ↦ s.eq_empty_of_isEmpty, fun h' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.Antichain (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
h' : s = ∅
⊢ IsEmpty α
have false : ∀ (a : α), False
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Antichain (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
h : IsMaxAntichain r s
h' : s = ∅
x : α
⊢ False
have h₁ : ∀ ⦃t : Set α⦄, IsAntichain r t → ∅ = t
Tactic: simp only [IsMaxAntichain, h', IsAntichain.empty, empty_subset, forall_const, true_and] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
⊢ a ≤ b ↔ a < b ∨ AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
have rw : a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
Tactic: rw [lt_iff_le_not_ge, AntisymmRel]
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
mp₁ mp₂ : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mp₃ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → a ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
mp₁ mp₂ : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mp₃ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → a ≤ b
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mp₄ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
mp₁ mp₂ : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mp₃ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → a ≤ b
mp₄ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → b ≤ a
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mpr₁ : a ≤ b → ¬b ≤ a → a ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
mp₁ mp₂ : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mp₃ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → a ≤ b
mp₄ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → a ≤ b
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mpr₂ : a ≤ b → b ≤ a → a ≤ b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
mp₁ mp₂ : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mp₃ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → a ≤ b
mp₄ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₂ : a ≤ b → b ≤ a → a ≤ b
mpr₃ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₄ : a ≤ b → b ≤ a → a ≤ b
mpr₅ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₆ : a ≤ b → b ≤ a → a ≤ b
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mp₅ : a ≤ b → ¬a ≤ b → b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
mp₁ mp₂ : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mp₃ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → a ≤ b
mp₄ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₂ : a ≤ b → b ≤ a → a ≤ b
mpr₃ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₄ : a ≤ b → b ≤ a → a ≤ b
mpr₅ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₆ : a ≤ b → b ≤ a → a ≤ b
mp₅ : a ≤ b → ¬a ≤ b → b ≤ a
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mp₆ : a ≤ b → ¬¬b ≤ a → b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b : α
inst : Preorder α
mp : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mpr : a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a → a ≤ b
mp₁ mp₂ : a ≤ b → a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
mp₃ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → a ≤ b
mp₄ : a ≤ b → ¬(a ≤ b ∧ ¬b ≤ a) → b ≤ a
mpr₁ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₂ : a ≤ b → b ≤ a → a ≤ b
mpr₃ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₄ : a ≤ b → b ≤ a → a ≤ b
mpr₅ : a ≤ b → ¬b ≤ a → a ≤ b
mpr₆ : a ≤ b → b ≤ a → a ≤ b
mp₅ : a ≤ b → ¬a ≤ b → b ≤ a
mp₆ mp₇ mp₈ : a ≤ b → ¬¬b ≤ a → b ≤ a
⊢ a ≤ b ↔ a ≤ b ∧ ¬b ≤ a ∨ a ≤ b ∧ b ≤ a
have mp₉ : a ≤ b → b ≤ a → b ≤ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ WellFoundedLT.{u_1} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↔ WellFoundedLT α
have simp_rw : (WellFounded fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↦ x1 < x2) ↔
  WellFounded fun (x1 x2 : α) ↦ x1 < x2
Tactic: simp_rw [isWellFounded_iff, wellFounded_antisymmetrization_iff]
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ WellFoundedGT.{u_1} (Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↔ WellFoundedGT α
have simp_rw : (WellFounded fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↦ x2 < x1) ↔
  WellFounded fun (x1 x2 : α) ↦ x2 < x1
Tactic: simp_rw [isWellFounded_iff]
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ (WellFounded fun (x1 x2 : Antisymmetrization α fun (x1 x2 : α) ↦ x1 ≤ x2) ↦ x2 < x1) ↔
    WellFounded fun (x1 x2 : α) ↦ x2 < x1
have convert_4 : ∀ (a₁ a₂ b₁ b₂ : α),
  (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2 : α → α → Prop) a₁ b₁ →
    (AntisymmRel.setoid α fun (x1 x2 : α) ↦ x1 ≤ x2 : α → α → Prop) a₂ b₂ → (a₂ < a₁) = (b₂ < b₁)
Tactic: convert! wellFounded_liftOn₂'_iff with ⟨_⟩ ⟨_⟩
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c
have inl : ∀ (h : a ≤ b), SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c
Tactic: obtain (h | h) := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.Antisymmetrization (goal)
Goal:
α : Type u_1
a b c : α
inst : Preorder α
h₁ : SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a b
h₂ : AntisymmRel (fun (x1 x2 : α) ↦ x1 ≤ x2) b c
inl : ∀ (h : a ≤ b), SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c
⊢ SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c
have inr : ∀ (h : b ≤ a), SymmGen (fun (x1 x2 : α) ↦ x1 ≤ x2) a c
Tactic: obtain (h | h) := h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (goal)
Goal:
α : Type u_1
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
inst_3 : DecidableEq α
⊢ Eq (α := Finset α) Finset.univ {⊤, ⊥}
have h : ∀ (a : α), Membership.mem (γ := Finset α) Finset.univ a ↔ Membership.mem (γ := Finset α) {⊤, ⊥} a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
a : Bool
⊢ a = ⊥ ∨ a = ⊤
have rw : Membership.mem (γ := Finset Bool) Finset.univ a
Tactic: rw [← Finset.mem_singleton, Or.comm, ← Finset.mem_insert, top_eq_true, bot_eq_false, ←
      Fintype.univ_bool]
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have obtain : ∀ (x : α) (hx : x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b)
  (hxmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b) y → y ≤ x → x ≤ y),
  ∃ (x : α), a ⋖ x ∧ x ≤ b
Tactic: obtain ⟨x, hx, hxmin⟩ := (LocallyFiniteOrder.finsetIoc a b).exists_minimal
      ⟨b, by simpa [LocallyFiniteOrder.finset_mem_Ioc]⟩
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b
hxmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b) y → y ≤ x → x ≤ y
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have hx₁ : a < x ∧ x ≤ b
Tactic: simp only [LocallyFiniteOrder.finset_mem_Ioc] at hx hxmin
Cleared hypotheses: hx, hxmin
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b
hxmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b) y → y ≤ x → x ≤ y
hx₁ : a < x ∧ x ≤ b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have hxmin₁ : ∀ ⦃y : α⦄, a < y ∧ y ≤ b → y ≤ x → x ≤ y
Tactic: simp only [LocallyFiniteOrder.finset_mem_Ioc] at hx hxmin
Cleared hypotheses: hx, hxmin
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ IsStronglyCoatomic α
have rw : IsStronglyAtomic.{u_1} αᵒᵈ
Tactic: rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
⊢ ∃ (b : α), a ⋖ b ∧ (Set.Ici b).Infinite
have by_contra! : ∀ (h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite
⊢ False
have refine : ∀ (b : α) (hb : b ∈ Set.Ici a \ {a}),
  Membership.mem (γ := Set α) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) {x : α | a ⋖ x} i), Set.Ici i) b
Tactic: refine ((hfin.biUnion (t := Set.Ici) (by simpa using h)).subset (fun b hb ↦ ?_)).not_infinite
    (ha.diff (Set.finite_singleton a))
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite
b : α
hb : b ∈ Set.Ici a \ {a}
⊢ Membership.mem (γ := Set α) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) {x : α | a ⋖ x} i), Set.Ici i) b
have obtain : ∀ (x : α) (hax : a ⋖ x) (hxb : x ≤ b),
  Membership.mem (γ := Set α) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) {x : α | a ⋖ x} i), Set.Ici i) b
Tactic: obtain ⟨x, hax, hxb⟩ := ((show a ≤ b from hb.1).lt_of_ne (Ne.symm hb.2)).exists_covby_le
-- Lean 4 proof step from Mathlib.Order.Atoms.Finite (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | x ⋖ a}
⊢ ∃ (b : α), b ⋖ a ∧ (Set.Iic b).Infinite
have simp_rw : ∀
  (hfin :
    Set.Finite.{u_1} (α := α)
      {x : α |
        CovBy (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) x : αᵒᵈ)}),
  ∃ (b : α),
    CovBy (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ∧
      (Set.Iic b).Infinite
Tactic: simp_rw [← toDual_covBy_toDual_iff (α := α)] at hfin ⊢
Cleared hypotheses: hfin
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a x : α
h : IsAtom a
⊢ x ≤ a ↔ x = ⊥ ∨ x = a
have rw : x < a ∨ x = a ↔ x = ⊥ ∨ x = a
Tactic: rw [le_iff_lt_or_eq, h.lt_iff]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a x : α
h : IsAtom a
rw : x < a ∨ x = a ↔ x = ⊥ ∨ x = a
⊢ x ≤ a ↔ x = ⊥ ∨ x = a
have rw₁ : x = ⊥ ∨ x = a ↔ x = ⊥ ∨ x = a
Tactic: rw [le_iff_lt_or_eq, h.lt_iff]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
⊢ a ≤ iSup f ↔ ∃ (i : ι), a ≤ f i
have refine : a ≤ iSup f → ∃ (i : ι), a ≤ f i
Tactic: refine ⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
⊢ a ≤ ⨆ (i : ι), f i → ∃ (i : ι), a ≤ f i
have refine : ∀ (h : a ≤ ⨆ (i : ι), f i) (ha' : ¬∃ (i : ι), a ≤ f i), False
Tactic: refine fun h => of_not_not fun ha' => ?_
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ¬∃ (i : ι), a ≤ f i
⊢ False
have ha'₁ : ∀ (i : ι), ¬a ≤ f i
Tactic: push Not at ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
⊢ False
have ha'' : Disjoint a (⨆ (i : ι), f i)
Tactic: have ha'' : Disjoint a (⨆ i, f i) :=
    disjoint_iSup_iff.2 fun i => fun x hxa hxf => le_bot_iff.2 <| of_not_not fun hx =>
      have hxa : x < a := (le_iff_eq_or_lt.1 hxa).resolve_left (by rintro rfl; exact ha' _ hxf)
      hx (ha.2 _ hxa)
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
⊢ False
have ha₁ : IsAtom.{u_2} (α := α) ⊥
Tactic: obtain rfl := le_bot_iff.1 (ha'' le_rfl h)
Cleared hypotheses: a, ha, h, ha', ha''
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
ha₁ : IsAtom.{u_2} (α := α) ⊥
⊢ False
have h₁ : LE.le.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
Tactic: obtain rfl := le_bot_iff.1 (ha'' le_rfl h)
Cleared hypotheses: a, ha, h, ha', ha''
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
ha₁ : IsAtom.{u_2} (α := α) ⊥
h₁ : LE.le.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
⊢ False
have ha'₁ : ∀ (i : ι), ¬⊥ ≤ f i
Tactic: obtain rfl := le_bot_iff.1 (ha'' le_rfl h)
Cleared hypotheses: a, ha, h, ha', ha''
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
ha₁ : IsAtom.{u_2} (α := α) ⊥
h₁ : LE.le.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
ha'₁ : ∀ (i : ι), ¬⊥ ≤ f i
⊢ False
have ha''₁ : Disjoint.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
Tactic: obtain rfl := le_bot_iff.1 (ha'' le_rfl h)
Cleared hypotheses: a, ha, h, ha', ha''
-- 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
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
have simp_rw : (K ≠ ⊥ ∧ ∀ 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 = ⊥
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
have simp_rw₁ : (K ≠ ⊥ ∧ ∀ (b : A), b ≤ K ∧ ¬K ≤ b → 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 = ⊥
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
have simp_rw₂ : (K ≠ ⊥ ∧ ∀ (b : A), (b ≤ K ∧ ∃ x ∈ K, x ∉ b) → 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 = ⊥
⊢ 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]