awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ s : Set α
h_1 : ChainClosure r s
ih : ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ s), s = c₁ ∨ SuccChain r c₁ ⊆ s
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s
h₁ : c₁ ⊆ s
succ : ∀ (hc₁ : ChainClosure r s) (h : s ⊆ SuccChain r s) (h₁ : s ⊆ s), SuccChain r s ⊆ SuccChain r s
succ₁ : ∀ (h₂ : SuccChain r c₁ ⊆ s), SuccChain r c₁ ⊆ SuccChain r s
⊢ SuccChain r c₁ ⊆ SuccChain r s

Tactic:
obtain rfl | h₂ := ih hc₁ h₁

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ s : Set α
h_1 : ChainClosure r s
ih : ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ s), s = c₁ ∨ SuccChain r c₁ ⊆ s
hc₁ : ChainClosure r s
h : s ⊆ SuccChain r s
h₁ : s ⊆ s
⊢ SuccChain r s ⊆ SuccChain r s

Tactic:
Subset.rfl

Premises used: Set.Subset.rfl
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ s : Set α
h_1 : ChainClosure r s
ih : ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ s), s = c₁ ∨ SuccChain r c₁ ⊆ s
hc₁ : ChainClosure r s
h : s ⊆ SuccChain r s
h₁ : s ⊆ s
⊢ SuccChain r s ⊆ SuccChain r s

Tactic:
exact Subset.rfl

Premises used: Set.Subset.rfl
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ s : Set α
h_1 : ChainClosure r s
ih : ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ s), s = c₁ ∨ SuccChain r c₁ ⊆ s
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s
h₁ : c₁ ⊆ s
h₂ : SuccChain r c₁ ⊆ s
⊢ SuccChain r c₁ ⊆ SuccChain r s

Tactic:
h₂.trans subset_succChain

Premises used: HasSubset.Subset.trans, subset_succChain
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ s : Set α
h_1 : ChainClosure r s
ih : ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ s), s = c₁ ∨ SuccChain r c₁ ⊆ s
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s
h₁ : c₁ ⊆ s
h₂ : SuccChain r c₁ ⊆ s
⊢ SuccChain r c₁ ⊆ SuccChain r s

Tactic:
exact h₂.trans subset_succChain

Premises used: HasSubset.Subset.trans, subset_succChain
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
union : ⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
⊢ ⋃₀ s = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s

Tactic:
apply Or.imp_left h.antisymm'

Premises used: Or.imp_left, HasSubset.Subset.antisymm'
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
union : ¬(⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s) → False
⊢ ⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s

Tactic:
apply by_contradiction

Premises used: by_contradiction
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
union : ∀ x ∈ s, ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s → False
⊢ ¬(⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s) → False

Tactic:
simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]

Premises used: and_imp, forall_exists_index, exists_prop, Set.sUnion_subset_iff, not_or, Classical.not_forall
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
union : ∀ (h : SuccChain r c₃ ⊆ c₁), False
union₁ : ∀ (h : c₁ ⊆ c₃), False
⊢ False

Tactic:
obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃

Premises used: _private.0.chainClosure_succ_total_aux
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h_2 : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : SuccChain r c₃ ⊆ c₁
⊢ False

Tactic:
h₁ (subset_succChain.trans h)

Premises used: HasSubset.Subset.trans, subset_succChain
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h_2 : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : SuccChain r c₃ ⊆ c₁
⊢ False

Tactic:
exact h₁ (subset_succChain.trans h)

Premises used: HasSubset.Subset.trans, subset_succChain
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h_2 : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
union : ∀ (h' : c₃ = c₁), False
union₁ : ∀ (h' : SuccChain r c₁ ⊆ c₃), False
⊢ False

Tactic:
obtain h' | h' := ih c₃ hc₃ hc₁ h
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h_2 : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False

Tactic:
h₁ h'.subset

Premises used: Eq.subset
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h_2 : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : c₃ = c₁
⊢ False

Tactic:
exact h₁ h'.subset

Premises used: Eq.subset
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h_2 : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False

Tactic:
h₂ (h'.trans <| subset_sUnion_of_mem hc₃)

Premises used: HasSubset.Subset.trans, Set.subset_sUnion_of_mem
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₂ : Set α
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h_2 : c₁ ⊆ ⋃₀ s
c₃ : Set α
hc₃ : c₃ ∈ s
h₁ : ¬c₃ ⊆ c₁
h₂ : ¬SuccChain r c₁ ⊆ ⋃₀ s
h : c₁ ⊆ c₃
h' : SuccChain r c₁ ⊆ c₃
⊢ False

Tactic:
exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)

Premises used: HasSubset.Subset.trans, Set.subset_sUnion_of_mem
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
h : c₁ ⊆ c₂
succ :
  ∀ {s : Set α},
    ChainClosure r s →
      ∀ (ih : ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ s), s = c₁ ∨ SuccChain r c₁ ⊆ s) {c₁ : Set α}
        (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ SuccChain r s), SuccChain r s = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r s
union :
  ∀ {s : Set (Set α)},
    (∀ a ∈ s, ChainClosure r a) →
      ∀ (ih : ∀ a ∈ s, ∀ {c₁ : Set α} (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ a), a = c₁ ∨ SuccChain r c₁ ⊆ a) {c₁ : Set α}
        (hc₁ : ChainClosure r c₁) (h : c₁ ⊆ ⋃₀ s), ⋃₀ s = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
⊢ c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂

Tactic:
induction hc₂ generalizing c₁ hc₁ with
  | succ _ ih =>
    refine ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => ?_
    obtain rfl | h₂ := ih hc₁ h₁
    · exact Subset.rfl
    · exact h₂.trans subset_succChain
  | union _ ih =>
    apply Or.imp_left h.antisymm'
    apply by_contradiction
    simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
    intro c₃ hc₃ h₁ h₂
    obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
    · exact h₁ (subset_succChain.trans h)
    obtain h' | h' := ih c₃ hc₃ hc₁ h
    · exact h₁ h'.subset
    · exact h₂ (h'.trans <| subset_sUnion_of_mem hc₃)

Premises used: Or.imp_left, and_imp, forall_exists_index, exists_prop, Set.sUnion_subset_iff, not_or, Set.Subset.rfl, by_contradiction, Classical.not_forall, HasSubset.Subset.antisymm', rfl
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
⊢ c₁ ⊆ c₂ ∨ c₂ ⊆ c₁

Tactic:
((chainClosure_succ_total_aux hc₂) fun _ hc₃ => chainClosure_succ_total hc₃ hc₁).imp_left
    subset_succChain.trans

Premises used: Or.imp_left, HasSubset.Subset.trans, _private.0.chainClosure_succ_total_aux, subset_succChain, _private.0.chainClosure_succ_total
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s : Set α
hc₁ : ChainClosure r s
h : s ⊆ c₂
⊢ SuccChain r s ⊆ c₂

Tactic:
(chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id

Premises used: Eq.rec, id, Eq.subset, _private.0.chainClosure_succ_total, Or.elim
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s : Set α
hc₁ : ChainClosure r s
h : s ⊆ c₂
⊢ SuccChain r s ⊆ c₂

Tactic:
exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id

Premises used: id, _private.0.chainClosure_succ_total, Or.elim
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s : Set (Set α)
h : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, a ⊆ c₂
⊢ ⋃₀ s ⊆ c₂

Tactic:
sUnion_subset ih

Premises used: Set.sUnion_subset
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
s : Set (Set α)
h : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, a ⊆ c₂
⊢ ⋃₀ s ⊆ c₂

Tactic:
exact sUnion_subset ih

Premises used: Set.sUnion_subset
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
succ : ∀ {s : Set α} (hc₁ : ChainClosure r s) (h : s ⊆ c₂), SuccChain r s ⊆ c₂
union : ∀ {s : Set (Set α)}, (∀ a ∈ s, ChainClosure r a) → ∀ (ih : ∀ a ∈ s, a ⊆ c₂), ⋃₀ s ⊆ c₂
⊢ c₁ ⊆ c₂

Tactic:
induction hc₁ with
  | succ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
  | union _ ih => exact sUnion_subset ih

Premises used: ChainClosure.union, ChainClosure.succ
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : ChainClosure r c
⊢ SuccChain r c = c ↔ c = maxChain r

Tactic:
⟨fun h => (subset_sUnion_of_mem hc).antisymm <| chainClosure_maxChain.succ_fixpoint hc h,
    fun h => subset_succChain.antisymm' <| (subset_sUnion_of_mem hc.succ).trans h.symm.subset⟩

Premises used: HasSubset.Subset.trans, subset_succChain, Eq.subset, ChainClosure.succ_fixpoint, HasSubset.Subset.antisymm, Iff.intro, Set.subset_sUnion_of_mem, Eq.symm, chainClosure_maxChain, HasSubset.Subset.antisymm', ChainClosure.succ
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c s : Set α
h_1 : ChainClosure r s
h : IsChain r s
⊢ IsChain r (SuccChain r s)

Tactic:
h.succ

Premises used: IsChain.succ
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c s : Set α
h_1 : ChainClosure r s
h : IsChain r s
⊢ IsChain r (SuccChain r s)

Tactic:
exact h.succ

Premises used: IsChain.succ
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
s : Set (Set α)
hs : ∀ a ∈ s, ChainClosure r a
h : ∀ a ∈ s, IsChain r a
⊢ IsChain r (⋃₀ s)

Tactic:
fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
      ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
        h t₁ ht₁ hc₁ (ht hc₂) hneq

Premises used: Set.Pairwise, IsChain, ChainClosure.total, Or, Or.elim, _private.0.ChainClosure.isChain.match_1
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
s : Set (Set α)
hs : ∀ a ∈ s, ChainClosure r a
h : ∀ a ∈ s, IsChain r a
⊢ IsChain r (⋃₀ s)

Tactic:
exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
      ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
        h t₁ ht₁ hc₁ (ht hc₂) hneq
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : ChainClosure r c
succ : ∀ {s : Set α}, ChainClosure r s → ∀ (h : IsChain r s), IsChain r (SuccChain r s)
union : ∀ {s : Set (Set α)} (hs : ∀ a ∈ s, ChainClosure r a) (h : ∀ a ∈ s, IsChain r a), IsChain r (⋃₀ s)
⊢ IsChain r c

Tactic:
induction hc with
  | succ _ h => exact h.succ
  | union hs h =>
    exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
      ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
        h t₁ ht₁ hc₁ (ht hc₂) hneq

Premises used: ChainClosure.union, ChainClosure.succ
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
⊢ IsMaxChain r (maxChain r)

Tactic:
by_contradiction fun h =>
    let ⟨_, H⟩ := chainClosure_maxChain.isChain.superChain_succChain h
    H.ne (chainClosure_maxChain.succ_fixpoint_iff.mpr rfl).symm

Premises used: Iff.mpr, False, ChainClosure.isChain, _private.0.maxChain_spec.match_1, IsChain.superChain_succChain, HasSSubset.SSubset.ne, by_contradiction, ChainClosure.succ_fixpoint_iff, Eq.symm, chainClosure_maxChain, rfl
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
⊢ IsLUB s (sSup s)

Tactic:
CompleteSemilatticeSup.isLUB_sSup _

Premises used: CompleteSemilatticeSup.isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
a : α
h : a ∈ s
⊢ a ≤ sSup s

Tactic:
(isLUB_sSup s).1 h

Premises used: And.left, isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
a : α
h : ∀ b ∈ s, b ≤ a
⊢ sSup s ≤ a

Tactic:
(isLUB_sSup s).2 h

Premises used: And.right, isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
⊢ IsLUB s (sSup s)

Tactic:
isLUB_sSup _

Premises used: isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
⊢ IsLUB s (sSup s)

Tactic:
exact isLUB_sSup _

Premises used: isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
⊢ sSup s ∈ upperBounds s

Tactic:
(isLUB_le_iff <| isLUB_sSup s).mp <| refl _

Premises used: isLUB_le_iff, Iff.mp, isLUB_sSup, refl
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
a b : α
hb : b ∈ s
h : a ≤ b
⊢ a ≤ sSup s

Tactic:
le_trans h (le_sSup hb)

Premises used: le_sSup, le_trans
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s t : Set α
h : s ⊆ t
⊢ sSup s ≤ sSup t

Tactic:
(isLUB_sSup s).mono (isLUB_sSup t) h

Premises used: IsLUB.mono, isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
a : α
⊢ sSup s ≤ a ↔ ∀ b ∈ s, b ≤ a

Tactic:
isLUB_le_iff (isLUB_sSup s)

Premises used: Set.Mem, setOf, upperBounds, isLUB_le_iff, isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteSemilatticeSup α
s : Set α
a : α
⊢ a ≤ sSup s ↔ ∀ b ∈ upperBounds s, a ≤ b

Tactic:
⟨fun h _ hb => le_trans h (sSup_le hb), fun hb => hb _ fun _ => le_sSup⟩

Premises used: Iff.intro, le_sSup, sSup_le, SupSet.sSup, le_trans
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteSemilatticeSup α
a : α
s : ι → α
⊢ a ≤ iSup s ↔ ∀ (b : α), (∀ (i : ι), s i ≤ b) → a ≤ b

Tactic:
simp [iSup, le_sSup_iff, upperBounds]

Premises used: iSup, upperBounds, le_sSup_iff
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteSemilatticeSup α
l : α
f : ι → α
⊢ iSup f < l ↔ ∃ b < l, ∀ (i : ι), f i ≤ b

Tactic:
sSup_lt_iff.trans <| exists_congr fun _ ↦ and_congr_right fun _ ↦ forall_mem_range

Premises used: Set.forall_mem_range, iSup, sSup_lt_iff, and_congr_right, exists_congr, Iff.trans
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ Membership.mem (γ := Set α) {x : α | a ≤ x ∧ b ≤ x} c

Tactic:
simp [*]
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hab : a ≤ b
hac : a ≤ c
a₁ : Membership.mem (γ := Set α) (lowerBounds {b, c}) a
⊢ a ≤ sInf {b, c}

Tactic:
apply (isGLB_sInf _).2

Premises used: And.right
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ Membership.mem (γ := Set α) (lowerBounds {b, c}) a

Tactic:
simp [*]
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : InfSet α
isGLB_sInf : ∀ (s : Set α), IsGLB s (sInf s)
a : α
⊢ Membership.mem (γ := Set α) (lowerBounds ∅) a

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
a b c : α
hac : a ≤ c
hbc : b ≤ c
⊢ Membership.mem (γ := Set α) (upperBounds {a, b}) c

Tactic:
simp [*]
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
a b c : α
hab : a ≤ b
hac : a ≤ c
⊢ Membership.mem (γ := Set α) {x : α | x ≤ b ∧ x ≤ c} a

Tactic:
simp [*]
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
H1 : PartialOrder α
H2 : SupSet α
isLUB_sSup : ∀ (s : Set α), IsLUB s (sSup s)
x : α
⊢ Membership.mem (γ := Set α) (upperBounds ∅) x

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
pos : ∀ (h : a ≤ b), min a b = a
neg : ∀ (h : ¬a ≤ b), min a b = b
⊢ min a b = if a ≤ b then a else b

Tactic:
split_ifs with h
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a

Tactic:
simp [h]
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b = b

Tactic:
simp [(CompleteLinearOrder.le_total a b).resolve_left h]

Premises used: Or.resolve_left, CompleteLinearOrder.le_total
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
pos : ∀ (h : a ≤ b), max a b = b
neg : ∀ (h : ¬a ≤ b), max a b = a
⊢ max a b = if a ≤ b then b else a

Tactic:
split_ifs with h
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : a ≤ b
⊢ max a b = b

Tactic:
simp [h]
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
i : CompleteLinearOrder α
a b : α
h : ¬a ≤ b
⊢ max a b = a

Tactic:
simp [(CompleteLinearOrder.le_total a b).resolve_left h]

Premises used: Or.resolve_left, CompleteLinearOrder.le_total
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : SupSet α
s : Set α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (sSup s) : αᵒᵈ) (sInf ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' s) : αᵒᵈ)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, OrderDual, rfl
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : InfSet α
s : Set αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) (sSup s) : α) (sInf ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' s) : α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, OrderDual, rfl
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
f : ι → α
⊢ Eq.{u_1 + 1} (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) (⨆ (i : ι), f i) : αᵒᵈ)
    (⨅ (i : ι), (toDual : (a : α) → αᵒᵈ) (f i) : αᵒᵈ)

Tactic:
rfl

Premises used: iInf, iSup, OrderDual, rfl
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
ι : Sort u_4
inst : InfSet α
f : ι → αᵒᵈ
⊢ Eq.{u_1 + 1} (α := α) ((ofDual : (a : αᵒᵈ) → α) (⨆ (i : ι), f i) : α) (⨅ (i : ι), (ofDual : (a : αᵒᵈ) → α) (f i) : α)

Tactic:
rfl

Premises used: iInf, iSup, OrderDual, rfl
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteLinearOrder α
s : Set α
b : α
⊢ b < sSup s ↔ ∃ a ∈ s, b < a

Tactic:
lt_isLUB_iff <| isLUB_sSup s

Premises used: lt_isLUB_iff, isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLinearOrder α
a : α
f : ι → α
⊢ a < iSup f ↔ ∃ (i : ι), a < f i

Tactic:
lt_sSup_iff.trans exists_range_iff

Premises used: iSup, Set.exists_range_iff, Iff.trans, lt_sSup_iff
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteLinearOrder α
s : Set α
l : α
⊢ l ≤ sSup s ↔ ∀ b < l, ∃ a ∈ s, b < a

Tactic:
grind [sSup_lt_iff, mem_upperBounds, not_le]

Premises used: not_le, sSup_lt_iff, mem_upperBounds
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLinearOrder α
l : α
f : ι → α
⊢ l ≤ iSup f ↔ ∀ b < l, ∃ (i : ι), b < f i

Tactic:
le_sSup_iff_forall_lt.trans <| forall₂_congr fun _ _ ↦ exists_range_iff

Premises used: iSup, le_sSup_iff_forall_lt, forall₂_congr, Set.exists_range_iff, Iff.trans
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
inst : CompleteLinearOrder α
s : Set α
rw : ⊤ ≤ sSup s ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
rw₁ rw₂ : (∀ b < ⊤, ∃ a ∈ s, b < a) ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
⊢ sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a

Tactic:
rw [eq_top_iff, le_sSup_iff_forall_lt]

Premises used: eq_top_iff, le_sSup_iff_forall_lt