awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s t : Set β
⊢ s ⊆ t → LE.le.{u_1} (α := α) (⨆ x ∈ s, f x) (⨆ x ∈ t, f x)

Tactic:
biSup_mono

Premises used: biSup_mono, Set.Subset
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s : Set β
b : β
⊢ ⨆ x ∈ insert b s, f x = f b ⊔ ⨆ x ∈ s, f x

Tactic:
simp [iSup_or, iSup_sup_eq]

Premises used: iSup_sup_eq, iSup_or
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
b : β
⊢ ⨆ (x : β), ⨆ (_ : Membership.mem (γ := Set β) {b} x), f x = f b

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
a b : β
rw : f a ⊔ ⨆ (x : β), ⨆ (_ : Membership.mem (γ := Set β) {b} x), f x = f a ⊔ f b
rw₁ rw₂ : f a ⊔ f b = f a ⊔ f b
⊢ ⨆ (x : β), ⨆ (_ : Membership.mem (γ := Set β) {a, b} x), f x = f a ⊔ f b

Tactic:
rw [iSup_insert, iSup_singleton]

Premises used: iSup_insert, iSup_singleton
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
rw : sSup (g '' f '' t) = ⨆ b ∈ t, g (f b)
rw₁ : sSup (g '' f '' t) = sSup ((fun (b : β) ↦ g (f b)) '' t)
rw₂ : sSup (g ∘ f '' t) = sSup ((fun (b : β) ↦ g (f b)) '' t)
rw₃ rw₄ : Eq.{u_1 + 1} (α := α) (sSup ((fun (x : β) ↦ g (f x)) '' t)) (sSup ((fun (b : β) ↦ g (f b)) '' t))
⊢ Eq.{u_1 + 1} (α := α) (⨆ c ∈ f '' t, g c) (⨆ b ∈ t, g (f b))

Tactic:
rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]

Premises used: Function.comp_def, sSup_image, Set.image_comp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
rw :
  Eq.{u_1 + 1} (α := α)
    ((⨆ (i : β), ⨆ (_ : ∃ (i_1 : ι), e i_1 = i), extend e f ⊥ i) ⊔
      ⨆ (i : β), ⨆ (_ : ¬∃ (i_1 : ι), e i_1 = i), extend e f ⊥ i)
    (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (j : β), extend e f ⊥ j) (⨆ (i : ι), f i)

Tactic:
rw [iSup_split _ fun j => ∃ i, e i = j]

Premises used: iSup_split, Exists, Eq
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ Eq.{u_1 + 1} (α := α)
    ((⨆ (i : β), ⨆ (_ : ∃ (i_1 : ι), e i_1 = i), extend e f ⊥ i) ⊔
      ⨆ (i : β), ⨆ (_ : ¬∃ (i_1 : ι), e i_1 = i), extend e f ⊥ i)
    (⨆ (i : ι), f i)

Tactic:
simp +contextual [he.extend_apply, extend_apply', @iSup_comm _ β ι]

Premises used: iSup_comm, Function.Injective.extend_apply, Function.extend_apply'
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
s : Set β
t : Set γ
f : β → γ
g : γ → α
hf : BijOn f s t
rw : Eq.{u_1 + 1} (α := α) (⨆ x ∈ s, g (f x)) (⨆ y ∈ f '' s, g y)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (⨆ x ∈ s, g (f x)) (⨆ b ∈ s, g (f b))
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s, g (f x)) (⨆ y ∈ t, g y)

Tactic:
rw [← hf.image_eq, iSup_image]

Premises used: iSup_image, Set.BijOn.image_eq
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
s : Set β
t : Set γ
f : β → α
g : γ → α
h : β → γ
h1 : BijOn h s t
h2 : ∀ (x : β), g (h x) = f x
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s, f x) (⨆ y ∈ t, g y)

Tactic:
simpa only [h2] using h1.iSup_comp g

Premises used: Set.BijOn.iSup_comp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : PartialOrder ι
f : ι → α
i : ι
rw : (⨆ (_ : i ≤ i), f i) ⊔ ⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≤ i), f i_1 = (⨆ (j : ι), ⨆ (_ : j < i), f j) ⊔ f i
⊢ ⨆ (j : ι), ⨆ (_ : j ≤ i), f j = (⨆ (j : ι), ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
rw [iSup_split_single _ i]

Premises used: iSup_split_single
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≤ i), f i) ⊔ ⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≤ i), f i_1 = (⨆ (j : ι), ⨆ (_ : j < i), f j) ⊔ f i

Tactic:
simp only [le_refl, iSup_pos, iSup_and', lt_iff_le_and_ne, and_comm, sup_comm]

Premises used: lt_iff_le_and_ne, le_refl, iSup_and', iSup_pos, and_comm, sup_comm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : PartialOrder ι
f : ι → α
i : ι
rw : (⨆ (_ : i ≥ i), f i) ⊔ ⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≥ i), f i_1 = f i ⊔ ⨆ (j : ι), ⨆ (_ : j > i), f j
⊢ ⨆ (j : ι), ⨆ (_ : j ≥ i), f j = f i ⊔ ⨆ (j : ι), ⨆ (_ : j > i), f j

Tactic:
rw [iSup_split_single _ i]

Premises used: iSup_split_single
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≥ i), f i) ⊔ ⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≥ i), f i_1 = f i ⊔ ⨆ (j : ι), ⨆ (_ : j > i), f j

Tactic:
simp only [ge_iff_le, le_refl, iSup_pos, ne_comm, iSup_and', gt_iff_lt, lt_iff_le_and_ne,
    and_comm]

Premises used: lt_iff_le_and_ne, le_refl, iSup_and', ge_iff_le, iSup_pos, and_comm, gt_iff_lt, ne_comm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
ι : Sort u_9
inst : SupSet α
inst_1 : IsEmpty ι
f : ι → α
⊢ iSup f = sSup ∅

Tactic:
congr_arg sSup (range_eq_empty f)

Premises used: iSup, congr_arg, Set.range_eq_empty, SupSet.sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
inst_1 : IsEmpty ι
f : ι → α
⊢ iSup f = ⊥

Tactic:
(iSup_of_empty' f).trans sSup_empty

Premises used: sSup_empty, iSup_of_empty', Eq.trans
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
s : Set β
f : β → α
⊢ IsLUB (f '' s) (⨆ x ∈ s, f x)

Tactic:
simpa only [range_comp, Subtype.range_coe, iSup_subtype'] using
    @isLUB_iSup α s _ (f ∘ fun x => (x : β))

Premises used: Set.range_comp, isLUB_iSup, iSup_subtype', Subtype.range_coe
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
p : β → Type u_8
f : Sigma p → α
c : α
⊢ ⨆ (x : Sigma p), f x ≤ c ↔ ⨆ (i : β), ⨆ (j : p i), f (Sigma.mk (β := p) i j) ≤ c

Tactic:
simp only [iSup_le_iff, Sigma.forall]

Premises used: Sigma.forall, iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
κ : β → Type u_8
f : (i : β) → κ i → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : β), ⨆ (j : κ i), f i j)
    (⨆ (x : (i : β) × κ i), f (x.fst (β := fun (i : β) ↦ κ i)) (x.snd (β := fun (i : β) ↦ κ i)))

Tactic:
(iSup_sigma (f := fun x ↦ f x.1 x.2)).symm

Premises used: iSup_sigma, Eq.symm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_8
κ : ι → Sort u_9
f : (i : ι) ×' κ i → α
c : α
⊢ ⨆ (ij : (i : ι) ×' κ i), f ij ≤ c ↔ ⨆ (i : ι), ⨆ (j : κ i), f (PSigma.mk (β := fun (i : ι) ↦ κ i) i j) ≤ c

Tactic:
simp only [iSup_le_iff, PSigma.forall]

Premises used: PSigma.forall, iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Sort u_8
κ : ι → Sort u_9
f : (i : ι) → κ i → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), f i j)
    (⨆ (ij : (i : ι) ×' κ i), f (ij.fst (β := fun (i : ι) ↦ κ i)) (ij.snd (β := fun (i : ι) ↦ κ i)))

Tactic:
(iSup_psigma fun x ↦ f x.1 x.2).symm

Premises used: PSigma.snd, iSup_psigma, PSigma.fst, Eq.symm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β × γ → α
c : α
⊢ ⨆ (x : β × γ), f x ≤ c ↔ ⨆ (i : β), ⨆ (j : γ), f (i, j) ≤ c

Tactic:
simp only [iSup_le_iff, Prod.forall]

Premises used: Prod.forall, iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β → γ → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : β), ⨆ (j : γ), f i j) (⨆ (x : β × γ), f x.1 x.2)

Tactic:
(iSup_prod (f := fun x ↦ f x.1 x.2)).symm

Premises used: Eq.symm, iSup_prod
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
simp_rw :
  Eq.{u_1 + 1} (α := α) (⨆ (i : β), ⨆ (j : γ), ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j)) (⨆ a ∈ s, ⨆ b ∈ t, f (a, b))
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s ×ˢ t, f x) (⨆ a ∈ s, ⨆ b ∈ t, f (a, b))

Tactic:
simp_rw [iSup_prod, mem_prod, iSup_and]

Premises used: Set.mem_prod, iSup_and, iSup_prod
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : β), ⨆ (j : γ), ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j)) (⨆ a ∈ s, ⨆ b ∈ t, f (a, b))

Tactic:
iSup_congr fun _ => iSup_comm

Premises used: iSup_comm, iSup_congr
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : β), ⨆ (j : γ), ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j)) (⨆ a ∈ s, ⨆ b ∈ t, f (a, b))

Tactic:
exact iSup_congr fun _ => iSup_comm

Premises used: iSup_comm, iSup_congr
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β → γ → α
s : Set β
t : Set γ
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s ×ˢ t, f x.1 x.2) (⨆ a ∈ s, ⨆ b ∈ t, f a b)

Tactic:
biSup_prod

Premises used: biSup_prod
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
γ : Type u_8
δ : Type u_9
f : β → γ → δ
s : Set β
t : Set γ
g : δ → α
rw :
  Eq.{u_1 + 1} (α := α)
    (⨆ (d : δ), ⨆ (_ : Membership.mem (γ := Set δ) ((fun (x : β × γ) ↦ f x.1 x.2) '' s ×ˢ t) d), g d)
    (⨆ b ∈ s, ⨆ c ∈ t, g (f b c))
rw₁ : Eq.{u_1 + 1} (α := α) (⨆ b ∈ s ×ˢ t, g (f b.1 b.2)) (⨆ b ∈ s, ⨆ c ∈ t, g (f b c))
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨆ a ∈ s, ⨆ b ∈ t, g (f (a, b).1 (a, b).2)) (⨆ b ∈ s, ⨆ c ∈ t, g (f b c))
⊢ Eq.{u_1 + 1} (α := α) (⨆ d ∈ image2 f s t, g d) (⨆ b ∈ s, ⨆ c ∈ t, g (f b c))

Tactic:
rw [← image_prod, iSup_image, biSup_prod]

Premises used: iSup_image, Set.image_prod, biSup_prod
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β ⊕ γ → α
c : α
⊢ ⨆ (x : β ⊕ γ), f x ≤ c ↔ (⨆ (i : β), f (Sum.inl i)) ⊔ ⨆ (j : γ), f (Sum.inr j) ≤ c

Tactic:
simp only [sup_le_iff, iSup_le_iff, Sum.forall]

Premises used: sup_le_iff, iSup_le_iff, Sum.forall
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : Option β → α
c : α
⊢ ⨆ (o : Option β), f o ≤ c ↔ f none ⊔ ⨆ (b : β), f (some b) ≤ c

Tactic:
simp only [iSup_le_iff, sup_le_iff, Option.forall]

Premises used: Option.forall, sup_le_iff, iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
a : α
f : β → α
⊢ ⨆ (o : Option β), o.elim a f = a ⊔ ⨆ (b : β), f b

Tactic:
simp [iSup_option]

Premises used: iSup_option
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
pos : ∀ (htriv : ∀ (i : ι), f i = ⊥), Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)
neg : ∀ (htriv : ∃ (i : ι), f i ≠ ⊥), Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)

Tactic:
by_cases! htriv : ∀ i, f i = ⊥
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∀ (i : ι), f i = ⊥
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)

Tactic:
simp only [iSup_bot, (funext htriv : f = _)]

Premises used: funext, iSup_bot
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)

Tactic:
(iSup_comp_le f _).antisymm (iSup_mono' fun i => ?_)

Premises used: iSup_mono', LE.le.antisymm, iSup_comp_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
neg : ∀ (i : ι), ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)

Tactic:
refine (iSup_comp_le f _).antisymm (iSup_mono' fun i => ?_)

Premises used: iSup_mono', LE.le.antisymm, iSup_comp_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
i : ι
pos : ∀ (hi : f i = ⊥), ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)
neg : ∀ (hi : ¬f i = ⊥), ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)

Tactic:
by_cases hi : f i = ⊥
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
i : ι
hi : f i = ⊥
pos : ∃ (i' : { i : ι // f i ≠ ⊥ }), ⊥ ≤ f (↑i' : ι)
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)

Tactic:
rw [hi]
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
i : ι
hi : f i = ⊥
pos : ∀ (i₀ : ι) (hi₀ : f i₀ ≠ ⊥), ∃ (i' : { i : ι // f i ≠ ⊥ }), ⊥ ≤ f (↑i' : ι)
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), ⊥ ≤ f (↑i' : ι)

Tactic:
obtain ⟨i₀, hi₀⟩ := htriv
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : f i₀ ≠ ⊥
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), ⊥ ≤ f (↑i' : ι)

Tactic:
⟨⟨i₀, hi₀⟩, bot_le⟩

Premises used: Subtype.mk, Exists.intro, bot_le
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
i : ι
hi : f i = ⊥
i₀ : ι
hi₀ : f i₀ ≠ ⊥
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), ⊥ ≤ f (↑i' : ι)

Tactic:
exact ⟨⟨i₀, hi₀⟩, bot_le⟩
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)

Tactic:
⟨⟨i, hi⟩, rfl.le⟩

Premises used: Eq.le, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
i : ι
hi : ¬f i = ⊥
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)

Tactic:
exact ⟨⟨i, hi⟩, rfl.le⟩
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β → γ → α
s : Set β
t : Set γ
rw : Eq.{u_1 + 1} (α := α) (sSup ((fun (x : β × γ) ↦ f x.1 x.2) '' s ×ˢ t)) (⨆ a ∈ s, ⨆ b ∈ t, f a b)
rw₁ : Eq.{u_1 + 1} (α := α) (⨆ a ∈ s ×ˢ t, f a.1 a.2) (⨆ a ∈ s, ⨆ b ∈ t, f a b)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨆ a ∈ s, ⨆ b ∈ t, f (a, b).1 (a, b).2) (⨆ a ∈ s, ⨆ b ∈ t, f a b)
⊢ sSup (image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b

Tactic:
rw [← image_prod, sSup_image, biSup_prod]

Premises used: Set.image_prod, biSup_prod, sSup_image
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLinearOrder α
f : (i : ι) → κ i → α
simp_rw :
  Eq.{u_1 + 1} (α := α) (⨆ (ij : (i : ι) ×' κ i), f (ij.fst (β := fun (i : ι) ↦ κ i)) (ij.snd (β := fun (i : ι) ↦ κ i)))
      ⊤ ↔
    ∀ b < ⊤, ∃ (i : ι) (j : κ i), b < f i j
simp_rw₁ :
  (∀ b < ⊤, ∃ (i : (i : ι) ×' κ i), b < f (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) ↔
    ∀ b < ⊤, ∃ (i : ι) (j : κ i), b < f i j
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), f i j) ⊤ ↔ ∀ b < ⊤, ∃ (i : ι) (j : κ i), b < f i j

Tactic:
simp_rw [iSup_psigma', iSup_eq_top, PSigma.exists]

Premises used: iSup_eq_top, PSigma.exists, iSup_psigma'
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
s : Set Prop
⊢ sSup s = ∃ p ∈ s, p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
s : Set Prop
⊢ sInf s = ∀ p ∈ s, p

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
ι : Sort u_4
p : ι → Prop
⊢ ⨆ (i : ι), p i = ∃ (i : ι), p i

Tactic:
le_antisymm (fun ⟨_, ⟨i, (eq : p i = _)⟩, hq⟩ => ⟨i, eq.symm ▸ hq⟩) fun ⟨i, hi⟩ =>
    ⟨p i, ⟨i, rfl⟩, hi⟩

Premises used: iSup, _private.0.biSup_sup.match_1, le_antisymm, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
ι : Sort u_4
p : ι → Prop
⊢ Eq (α := Prop) (⨅ (i : ι), p i) (∀ (i : ι), p i)

Tactic:
le_antisymm (fun h i => h _ ⟨i, rfl⟩) fun h _ ⟨i, Eq⟩ => Eq ▸ h i

Premises used: Eq.rec, _private.0.iInf_Prop_eq.match_1, le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
β : α → Type u_9
inst : (i : α) → SupSet (β i)
s : Set ((a : α) → β a)
a : α
⊢ sSup s a = ⨆ (f : (↑s : Type (max u_8 u_9))), (↑f : (a : α) → β a) a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
β : α → Type u_9
inst : (i : α) → SupSet (β i)
s : Set ((a : α) → β a)
a : α
⊢ sSup s a = sSup (eval (β := β) a '' s)

Tactic:
simp [sSup_apply, iSup, image_eq_range]

Premises used: iSup, Set.image_eq_range, sSup_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst : (i : α) → CompleteLattice (β i)
x : Set ((i : α) → β i)
x_1 : α
rw : IsLUB (eval (β := β) x_1 '' x) (sSup (eval (β := β) x_1 '' x))
⊢ IsLUB (eval (β := β) x_1 '' x) (sSup x x_1)

Tactic:
rw [sSup_apply_eq_sSup_image]

Premises used: sSup_apply_eq_sSup_image
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst : (i : α) → CompleteLattice (β i)
x : Set ((i : α) → β i)
x_1 : α
⊢ IsLUB (eval (β := β) x_1 '' x) (sSup (eval (β := β) x_1 '' x))

Tactic:
isLUB_sSup _

Premises used: isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst : (i : α) → CompleteLattice (β i)
x : Set ((i : α) → β i)
x_1 : α
⊢ IsLUB (eval (β := β) x_1 '' x) (sSup (eval (β := β) x_1 '' x))

Tactic:
exact isLUB_sSup _

Premises used: isLUB_sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst : (i : α) → CompleteLattice (β i)
x : Set ((i : α) → β i)
x_1 : α
rw : IsGLB (eval (β := β) x_1 '' x) (sInf (eval (β := β) x_1 '' x))
⊢ IsGLB (eval (β := β) x_1 '' x) (sInf x x_1)

Tactic:
rw [sInf_apply_eq_sInf_image]

Premises used: sInf_apply_eq_sInf_image
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst : (i : α) → CompleteLattice (β i)
x : Set ((i : α) → β i)
x_1 : α
⊢ IsGLB (eval (β := β) x_1 '' x) (sInf (eval (β := β) x_1 '' x))

Tactic:
isGLB_sInf _

Premises used: isGLB_sInf
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
α : Type u_8
β : α → Type u_9
inst : (i : α) → CompleteLattice (β i)
x : Set ((i : α) → β i)
x_1 : α
⊢ IsGLB (eval (β := β) x_1 '' x) (sInf (eval (β := β) x_1 '' x))

Tactic:
exact isGLB_sInf _

Premises used: isGLB_sInf
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
rw : Eq.{u_9 + 1} (α := β a) (sSup (range ((fun (f : (i : α) → β i) ↦ f a) ∘ f))) (sSup (range fun (i : ι) ↦ f i a))
⊢ Eq.{u_9 + 1} (α := β a) ((⨆ (i : ι), f i) a) (⨆ (i : ι), f i a)

Tactic:
rw [iSup, sSup_apply, iSup, iSup, ← image_eq_range (fun f : ∀ i, β i => f a) (range f), ←
    range_comp]

Premises used: Set.range_comp, iSup, Set.image_eq_range, Set.range, sSup_apply
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ Eq.{u_9 + 1} (α := β a) (sSup (range ((fun (f : (i : α) → β i) ↦ f a) ∘ f))) (sSup (range fun (i : ι) ↦ f i a))

Tactic:
rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
s : Set (α → Prop)
a : α
⊢ sSup s a ↔ ∃ r ∈ s, r a

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
s : Set (α → Prop)
a : α
⊢ sInf s a ↔ ∀ r ∈ s, r a

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ sSup s a b ↔ ∃ r ∈ s, r a b

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ sInf s a b ↔ ∀ r ∈ s, r a b

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, Monotone f
⊢ Monotone (sSup s)

Tactic:
fun _ _ h ↦ iSup_mono fun f ↦ hs f f.2 h

Premises used: Monotone, Subtype.val, Subtype.property, iSup_mono
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, Antitone f
⊢ Antitone (sSup s)

Tactic:
fun _ _ h ↦ iSup_mono fun f ↦ hs f f.2 h

Premises used: Antitone, Subtype.val, Subtype.property, iSup_mono
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Preorder α
inst_1 : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Monotone (f i)
⊢ ∀ (f_1 : α → β), Membership.mem (γ := Set (α → β)) (range fun (i : ι) ↦ f i) f_1 → Monotone f_1

Tactic:
simpa
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : Preorder α
inst_1 : CompleteLattice β
f : ι → α → β
hf : ∀ (i : ι), Antitone (f i)
⊢ ∀ (f_1 : α → β), Membership.mem (γ := Set (α → β)) (range fun (i : ι) ↦ f i) f_1 → Antitone f_1

Tactic:
simpa
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : SupSet α
inst_1 : SupSet β
s : Set (α × β)
⊢ (sSup s).1 = sSup (fst '' s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : SupSet α
inst_1 : SupSet β
s : Set (α × β)
⊢ (sSup s).2 = sSup (snd '' s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
inst : SupSet α
inst_1 : SupSet β
s : Set (α × β)
⊢ (sSup s).swap = sSup (swap '' s)

Tactic:
Prod.ext (congr_arg sSup <| image_comp Prod.fst swap s)
    (congr_arg sSup <| image_comp Prod.snd swap s)

Premises used: Prod.fst, congr_arg, Prod.ext, Set.image_comp, Prod.swap, Prod.snd, SupSet.sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
inst_1 : SupSet β
f : ι → α × β
⊢ (iSup f).1 = ⨆ (i : ι), (f i).1

Tactic:
congr_arg sSup (range_comp _ _).symm

Premises used: Set.range_comp, iSup, congr_arg, Eq.symm, SupSet.sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
inst_1 : SupSet β
f : ι → α × β
⊢ (iSup f).2 = ⨆ (i : ι), (f i).2

Tactic:
congr_arg sSup (range_comp _ _).symm

Premises used: Set.range_comp, iSup, congr_arg, Eq.symm, SupSet.sSup
-- Module: Mathlib.Order.CompleteLattice.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
inst_1 : SupSet β
f : ι → α × β
simp_rw : (sSup (range f)).swap = sSup (range fun (i : ι) ↦ (f i).swap)
simp_rw₁ : sSup (swap '' range f) = sSup (range fun (i : ι) ↦ (f i).swap)
simp_rw₂ : sSup (range (swap ∘ f)) = sSup (range fun (i : ι) ↦ (f i).swap)
⊢ (iSup f).swap = ⨆ (i : ι), (f i).swap

Tactic:
simp_rw [iSup, swap_sSup, ← range_comp, comp_def]

Premises used: Set.range_comp, Prod.swap_sSup, iSup, Function.comp_def