awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x : Set α
⊢ IsLUB ((fun {y : α} ↦ f y) '' x) (f (sSup x))
have rw : IsLUB.{u_2} (α := β) ((fun {y : α} ↦ f y) '' x) (⨆ a ∈ x, f a)
Tactic: rw [map_sSup]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
inst_8 : CompleteLattice β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
x : Set α
⊢ IsGLB ((fun {x : α} ↦ f x) '' x) (f (sInf x))
have rw : IsGLB.{u_2} (α := β) ((fun {x : α} ↦ f x) '' x) (⨅ a ∈ x, f a)
Tactic: rw [map_sInf]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
⊢ CompleteLattice α
have le : ∀ {x y : α}, LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
Tactic: apply e.injective.completeLattice
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
le : ∀ {x y : α}, LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
⊢ CompleteLattice α
have lt : ∀ {x y : α}, LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
Tactic: apply e.injective.completeLattice
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
le : ∀ {x y : α}, LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
⊢ CompleteLattice α
have map_sup : ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeLattice
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
le : ∀ {x y : α}, LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
⊢ CompleteLattice α
have map_inf : ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
Tactic: apply e.injective.completeLattice
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
le : ∀ {x y : α}, LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
⊢ CompleteLattice α
have map_sSup : ∀ (s : Set α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.completeLattice
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
le : ∀ {x y : α}, LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
⊢ CompleteLattice α
have map_sInf : ∀ (s : Set α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
Tactic: apply e.injective.completeLattice
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
le : ∀ {x y : α}, LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
⊢ CompleteLattice α
have map_top : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
Tactic: apply e.injective.completeLattice
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
e : α ≃ β
inst : CompleteLattice β
top : Top α := e.top
bot : Bot α := e.bot
supSet : SupSet α := e.supSet
infSet : InfSet α := e.infSet
lattice : Lattice α := e.lattice
le : ∀ {x y : α}, LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y
lt : ∀ {x y : α}, LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y
map_sup :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)
map_inf :
  ∀ (a b : α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)
map_sSup : ∀ (s : Set α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)
map_sInf : ∀ (s : Set α), Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)
map_top : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)
⊢ CompleteLattice α
have map_bot : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
Tactic: apply e.injective.completeLattice
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (hypothesis)
Goal:
α : Type u_1
r : α → α → Prop
⊢ ChainClosure r ∅
have this : ChainClosure r (⋃₀ ∅)
Tactic: have : ChainClosure r (⋃₀ ∅) := ChainClosure.union fun a h => (notMem_empty _ h).elim
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
have succ : ∀ (ih : SuccChain r c₂ ⊆ c₃), SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
Tactic: obtain ih | ih := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
c₃ : Set α
hc₃ : ChainClosure r c₃
ih : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂
succ : ∀ (ih : SuccChain r c₂ ⊆ c₃), SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
have succ₁ : ∀ (ih : c₃ ⊆ c₂), SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
Tactic: obtain ih | ih := ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
s : Set (Set α)
h_1 : ∀ a ∈ s, ChainClosure r a
ih : ∀ a ∈ s, SuccChain r c₂ ⊆ a ∨ a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s ∨ ⋃₀ s ⊆ c₂
have union : ∀ (hn : ¬SuccChain r c₂ ⊆ ⋃₀ s) (a : Set α) (ha : a ∈ s), a ⊆ c₂
Tactic: refine or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => ?_
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂
have succ : ∀ {c₃ : Set α} (hc₃ : ChainClosure r c₃) (ih : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂),
  SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
Tactic: induction hc₁ with
  | @succ c₃ hc₃ ih =>
    obtain ih | ih := ih
    · exact Or.inl (ih.trans subset_succChain)
    · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
  | union _ ih =>
    refine or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => ?_
    exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha
Cleared hypotheses: hc₁
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
h : ∀ ⦃c₃ : Set α⦄, ChainClosure r c₃ → c₃ ⊆ c₂ → c₂ = c₃ ∨ SuccChain r c₃ ⊆ c₂
succ :
  ∀ {c₃ : Set α} (hc₃ : ChainClosure r c₃) (ih : SuccChain r c₂ ⊆ c₃ ∨ c₃ ⊆ c₂),
    SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ c₁ ∨ c₁ ⊆ c₂
have union : ∀ {s : Set (Set α)},
  (∀ a ∈ s, ChainClosure r a) → ∀ (ih : ∀ a ∈ s, SuccChain r c₂ ⊆ a ∨ a ⊆ c₂), SuccChain r c₂ ⊆ ⋃₀ s ∨ ⋃₀ s ⊆ c₂
Tactic: induction hc₁ with
  | @succ c₃ hc₃ ih =>
    obtain ih | ih := ih
    · exact Or.inl (ih.trans subset_succChain)
    · exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl
  | union _ ih =>
    refine or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => ?_
    exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha
Cleared hypotheses: hc₁
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ SuccChain r s = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r s
have succ : ∀ (h₁ : c₁ ⊆ s), SuccChain r c₁ ⊆ SuccChain r s
Tactic: refine ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => ?_
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ SuccChain r c₁ ⊆ SuccChain r s
have succ : ∀ (hc₁ : ChainClosure r s) (h : s ⊆ SuccChain r s) (h₁ : s ⊆ s), SuccChain r s ⊆ SuccChain r s
Tactic: obtain rfl | h₂ := ih hc₁ h₁
Cleared hypotheses: c₁, hc₁, h, h₁
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ SuccChain r c₁ ⊆ SuccChain r s
have succ₁ : ∀ (h₂ : SuccChain r c₁ ⊆ s), SuccChain r c₁ ⊆ SuccChain r s
Tactic: obtain rfl | h₂ := ih hc₁ h₁
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ ⋃₀ s = c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
have union : ⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
Tactic: apply Or.imp_left h.antisymm'
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ ⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s
have union : ¬(⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s) → False
Tactic: apply by_contradiction
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ ¬(⋃₀ s ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s) → False
have union : ∀ x ∈ s, ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s → False
Tactic: simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ False
have union : ∀ (h : SuccChain r c₃ ⊆ c₁), False
Tactic: obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ False
have union₁ : ∀ (h : c₁ ⊆ c₃), False
Tactic: obtain h | h := chainClosure_succ_total_aux hc₁ fun c₄ => ih _ hc₃
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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₃
⊢ False
have union : ∀ (h' : c₃ = c₁), False
Tactic: obtain h' | h' := ih c₃ hc₃ hc₁ h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ False
have union₁ : ∀ (h' : SuccChain r c₁ ⊆ c₃), False
Tactic: obtain h' | h' := ih c₃ hc₃ hc₁ h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
h : c₁ ⊆ c₂
⊢ c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
have 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
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₃)
Cleared hypotheses: c₁, hc₁, hc₂, h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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
⊢ c₂ = c₁ ∨ SuccChain r c₁ ⊆ c₂
have 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
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₃)
Cleared hypotheses: c₁, hc₁, hc₂, h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
c₁ c₂ : Set α
hc₁ : ChainClosure r c₁
hc₂ : ChainClosure r c₂
hc : SuccChain r c₂ = c₂
⊢ c₁ ⊆ c₂
have succ : ∀ {s : Set α} (hc₁ : ChainClosure r s) (h : s ⊆ c₂), SuccChain r s ⊆ 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
Cleared hypotheses: hc₁
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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₂
⊢ c₁ ⊆ c₂
have union : ∀ {s : Set (Set α)}, (∀ a ∈ s, ChainClosure r a) → ∀ (ih : ∀ a ∈ s, a ⊆ c₂), ⋃₀ s ⊆ 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
Cleared hypotheses: hc₁
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
Goal:
α : Type u_1
r : α → α → Prop
c : Set α
hc : ChainClosure r c
⊢ IsChain r c
have succ : ∀ {s : Set α}, ChainClosure r s → ∀ (h : IsChain r s), IsChain r (SuccChain r s)
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
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Chain (goal)
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)
⊢ IsChain r c
have union : ∀ {s : Set (Set α)} (hs : ∀ a ∈ s, ChainClosure r a) (h : ∀ a ∈ s, IsChain r a), IsChain r (⋃₀ s)
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
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
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 ≤ sInf {b, c}
have a₁ : Membership.mem (γ := Set α) (lowerBounds {b, c}) a
Tactic: apply (isGLB_sInf _).2
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
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 : α
⊢ min a b = if a ≤ b then a else b
have pos : ∀ (h : a ≤ b), min a b = a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
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
⊢ min a b = if a ≤ b then a else b
have neg : ∀ (h : ¬a ≤ b), min a b = b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
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 : α
⊢ max a b = if a ≤ b then b else a
have pos : ∀ (h : a ≤ b), max a b = b
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
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
⊢ max a b = if a ≤ b then b else a
have neg : ∀ (h : ¬a ≤ b), max a b = a
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
s : Set α
⊢ sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
have rw : ⊤ ≤ sSup s ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
Tactic: rw [eq_top_iff, le_sSup_iff_forall_lt]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Defs (goal)
Goal:
α : Type u_1
inst : CompleteLinearOrder α
s : Set α
rw : ⊤ ≤ sSup s ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
⊢ sSup s = ⊤ ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
have rw₁ : (∀ b < ⊤, ∃ a ∈ s, b < a) ↔ ∀ b < ⊤, ∃ a ∈ s, b < a
Tactic: rw [eq_top_iff, le_sSup_iff_forall_lt]