awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
inst_1 : SupSet β
f : ι → α
g : ι → β
⊢ Eq (α := α × β) (⨆ (i : ι), (f i, g i)) (⨆ (i : ι), f i, ⨆ (i : ι), g i)

Tactic:
congr_arg₂ Prod.mk (fst_iSup _) (snd_iSup _)

Premises used: iSup, Prod.fst_iSup, Prod.mk, Prod.snd_iSup, congr_arg₂
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : SupSet α
inst_1 : SupSet β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup (s ×ˢ t) = (sSup s, sSup t)

Tactic:
congr_arg₂ Prod.mk (congr_arg sSup <| fst_image_prod _ ht) (congr_arg sSup <| snd_image_prod hs _)

Premises used: Set.fst_image_prod, Prod.mk, congr_arg, Set.snd_image_prod, SupSet.sSup, congr_arg₂
-- Module: Mathlib.Order.CompleteLattice.Basic
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 α
rw : IsLUB.{u_2} (α := β) ((fun {y : α} ↦ f y) '' x) (⨆ a ∈ x, f a)
⊢ IsLUB ((fun {y : α} ↦ f y) '' x) (f (sSup x))

Tactic:
rw [map_sSup]
-- Module: Mathlib.Order.CompleteLattice.Basic
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.{u_2} (α := β) ((fun {y : α} ↦ f y) '' x) (⨆ a ∈ x, f a)

Tactic:
isLUB_biSup

Premises used: isLUB_biSup
-- Module: Mathlib.Order.CompleteLattice.Basic
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.{u_2} (α := β) ((fun {y : α} ↦ f y) '' x) (⨆ a ∈ x, f a)

Tactic:
exact isLUB_biSup

Premises used: isLUB_biSup
-- Module: Mathlib.Order.CompleteLattice.Basic
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 α
rw : IsGLB.{u_2} (α := β) ((fun {x : α} ↦ f x) '' x) (⨅ a ∈ x, f a)
⊢ IsGLB ((fun {x : α} ↦ f x) '' x) (f (sInf x))

Tactic:
rw [map_sInf]
-- Module: Mathlib.Order.CompleteLattice.Basic
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.{u_2} (α := β) ((fun {x : α} ↦ f x) '' x) (⨅ a ∈ x, f a)

Tactic:
isGLB_biInf

Premises used: isGLB_biInf
-- Module: Mathlib.Order.CompleteLattice.Basic
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.{u_2} (α := β) ((fun {x : α} ↦ f x) '' x) (⨅ a ∈ x, f a)

Tactic:
exact isGLB_biInf

Premises used: isGLB_biInf
-- Module: Mathlib.Order.CompleteLattice.Basic
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 : α) → β) ⊤ : β) (⊤ : β)
map_bot : Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)
⊢ CompleteLattice α

Tactic:
apply e.injective.completeLattice

Premises used: Function.Injective.completeLattice, Equiv.injective
-- Module: Mathlib.Order.CompleteLattice.Basic
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
x y : α
⊢ LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
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
x y : α
⊢ LE.le.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x ≤ y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
x y : α
⊢ LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
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
x y : α
⊢ LT.lt.{u_2} (α := β) ((e : (a : α) → β) x : β) ((e : (a : α) → β) y : β) ↔ x < y

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
a b : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
a b : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
a b : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊔ b) : β) ((e : (a : α) → β) a ⊔ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
a b : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
a b : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
a b : α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (a ⊓ b) : β) ((e : (a : α) → β) a ⊓ (e : (a : α) → β) b : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
s : Set α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
s : Set α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
s : Set α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
s : Set α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
s : Set α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
s : Set α
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ a ∈ s, (e : (a : α) → β) a : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊤ : β) (⊤ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
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
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) ⊥ : β) (⊥ : β)

Tactic:
first | rfl | exact e.apply_symm_apply _

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
⊢ ChainClosure r (⋃₀ ∅)

Tactic:
have : ChainClosure r (⋃₀ ∅) := ChainClosure.union fun a h => (notMem_empty _ h).elim
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅

Tactic:
simpa using this
-- Module: Mathlib.Order.CompleteLattice.Chain
Goal:
α : Type u_1
r : α → α → Prop
⊢ ChainClosure r (maxChain r)

Tactic:
ChainClosure.union fun _ => id

Premises used: maxChain, id, ChainClosure.union
-- Module: Mathlib.Order.CompleteLattice.Chain
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₂
succ₁ : ∀ (ih : c₃ ⊆ c₂), SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
obtain ih | ih := ih
-- Module: Mathlib.Order.CompleteLattice.Chain
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₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
Or.inl (ih.trans subset_succChain)

Premises used: HasSubset.Subset.trans, subset_succChain, Or.inl
-- Module: Mathlib.Order.CompleteLattice.Chain
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₃
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
exact Or.inl (ih.trans subset_succChain)

Premises used: HasSubset.Subset.trans, subset_succChain, Or.inl
-- Module: Mathlib.Order.CompleteLattice.Chain
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 : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
(h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl

Premises used: Or.imp_left, Eq.rec, Set.Subset.rfl
-- Module: Mathlib.Order.CompleteLattice.Chain
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 : c₃ ⊆ c₂
⊢ SuccChain r c₂ ⊆ SuccChain r c₃ ∨ SuccChain r c₃ ⊆ c₂

Tactic:
exact (h hc₃ ih).imp_left fun (h : c₂ = c₃) => h ▸ Subset.rfl

Premises used: Or.imp_left
-- Module: Mathlib.Order.CompleteLattice.Chain
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₂

Tactic:
or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => ?_

Premises used: Iff.mpr, Set.sUnion_subset, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.CompleteLattice.Chain
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₂
union : ∀ (hn : ¬SuccChain r c₂ ⊆ ⋃₀ s) (a : Set α) (ha : a ∈ s), a ⊆ c₂
⊢ SuccChain r c₂ ⊆ ⋃₀ s ∨ ⋃₀ s ⊆ c₂

Tactic:
refine or_iff_not_imp_left.2 fun hn => sUnion_subset fun a ha => ?_

Premises used: Iff.mpr, Set.sUnion_subset, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.CompleteLattice.Chain
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₂
hn : ¬SuccChain r c₂ ⊆ ⋃₀ s
a : Set α
ha : a ∈ s
⊢ a ⊆ c₂

Tactic:
(ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha

Premises used: HasSubset.Subset.trans, Or.resolve_left, Set.subset_sUnion_of_mem
-- Module: Mathlib.Order.CompleteLattice.Chain
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₂
hn : ¬SuccChain r c₂ ⊆ ⋃₀ s
a : Set α
ha : a ∈ s
⊢ a ⊆ c₂

Tactic:
exact (ih a ha).resolve_left fun h => hn <| h.trans <| subset_sUnion_of_mem ha

Premises used: HasSubset.Subset.trans, Or.resolve_left, Set.subset_sUnion_of_mem
-- Module: Mathlib.Order.CompleteLattice.Chain
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₂
union :
  ∀ {s : Set (Set α)},
    (∀ a ∈ s, ChainClosure r a) → ∀ (ih : ∀ a ∈ s, SuccChain r c₂ ⊆ a ∨ a ⊆ c₂), SuccChain r c₂ ⊆ ⋃₀ s ∨ ⋃₀ s ⊆ c₂
⊢ SuccChain r c₂ ⊆ c₁ ∨ 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

Premises used: Iff.mpr, Set.sUnion_subset, Classical.or_iff_not_imp_left
-- 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
⊢ SuccChain r s = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r s

Tactic:
((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => ?_

Premises used: _private.0.chainClosure_succ_total_aux, Or.imp, HasSubset.Subset.antisymm'
-- 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
succ : ∀ (h₁ : c₁ ⊆ s), SuccChain r c₁ ⊆ SuccChain r s
⊢ SuccChain r s = c₁ ∨ SuccChain r c₁ ⊆ SuccChain r s

Tactic:
refine ((chainClosure_succ_total_aux hc₁) fun c₁ => ih).imp h.antisymm' fun h₁ => ?_

Premises used: _private.0.chainClosure_succ_total_aux, Or.imp, HasSubset.Subset.antisymm'