awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMaxOrder ι
f : ι → α
j : ι
⊢ f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j
have a : ∀ (i : ι) (jlt : j < i), f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j < i), f j
Tactic: obtain ⟨i, jlt⟩ := exists_gt j
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j) (⨆ (i : ι), f i)
have a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j) (⨆ (i : ι), f i)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j) (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j) (⨆ (i : ι), f i)
have a₁ : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≤ i), f j)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j) (⨆ (i : ι), f i)
have a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j) (⨆ (i : ι), f i)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j) (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j) (⨆ (i : ι), f i)
have a₁ : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j)
have a : ∀ (j : ι), f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j
Tactic: refine iSup_le fun j ↦ ?_
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : LT ι
inst_2 : NoMinOrder ι
f : ι → α
j : ι
⊢ f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j
have a : ∀ (i : ι) (jlt : i < j), f j ≤ ⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j > i), f j
Tactic: obtain ⟨i, jlt⟩ := exists_lt j
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j) (⨆ (i : ι), f i)
have a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j) (⨆ (i : ι), f i)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : Preorder ι
f : ι → α
a : LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j) (⨆ (i : ι), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j) (⨆ (i : ι), f i)
have a₁ : LE.le.{u_1} (α := α) (⨆ (i : ι), f i) (⨆ (i : ι), ⨆ (j : ι), ⨆ (_ : j ≥ i), f j)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), if h : p i then f i h else g i h)
    ((⨆ (i : ι), ⨆ (h : p i), f i h) ⊔ ⨆ (i : ι), ⨆ (h : ¬p i), g i h)
have rw : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), if h : p i then f i h else g i h)
  (⨆ (x : ι), (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h)
Tactic: rw [← iSup_sup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), if h : p i then f i h else g i h)
    (⨆ (x : ι), (⨆ (h : p x), f x h) ⊔ ⨆ (h : ¬p x), g x h)
have e_s : ∀ (i : ι), Eq.{u_1 + 1} (α := α) (if h : p i then f i h else g i h) ((⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h)
Tactic: congr 1 with i
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
⊢ Eq.{u_1 + 1} (α := α) (if h : p i then f i h else g i h) ((⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h)
have pos : ∀ (h : p i), f i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
p : ι → Prop
inst_1 : DecidablePred p
f : (i : ι) → p i → α
g : (i : ι) → ¬p i → α
i : ι
pos : ∀ (h : p i), f i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
⊢ Eq.{u_1 + 1} (α := α) (if h : p i then f i h else g i h) ((⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h)
have neg : ∀ (h : ¬p i), g i h = (⨆ (h : p i), f i h) ⊔ ⨆ (h : ¬p i), g i h
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
g : β → α
f : ι → β
⊢ Eq.{u_1 + 1} (α := α) (⨆ b ∈ range f, g b) (⨆ (i : ι), g (f i))
have rw : Eq.{u_1 + 1} (α := α) (⨆ (i : (↑(range f) : Type u_2)), g (↑i : β)) (⨆ (i : ι), g (f i))
Tactic: rw [← iSup_subtype'', iSup_range']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
g : β → α
f : ι → β
rw : Eq.{u_1 + 1} (α := α) (⨆ (i : (↑(range f) : Type u_2)), g (↑i : β)) (⨆ (i : ι), g (f i))
⊢ Eq.{u_1 + 1} (α := α) (⨆ b ∈ range f, g b) (⨆ (i : ι), g (f i))
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), g (f i)) (⨆ (i : ι), g (f i))
Tactic: rw [← iSup_subtype'', iSup_range']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
s : Set β
f : β → α
⊢ sSup (f '' s) = ⨆ a ∈ s, f a
have rw : sSup (f '' s) = ⨆ (i : (↑s : Type u_2)), f (↑i : β)
Tactic: rw [← iSup_subtype'', sSup_image']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
s : Set β
f : β → α
rw : sSup (f '' s) = ⨆ (i : (↑s : Type u_2)), f (↑i : β)
⊢ sSup (f '' s) = ⨆ a ∈ s, f a
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (a : (↑s : Type u_2)), f (↑a : β)) (⨆ (i : (↑s : Type u_2)), f (↑i : β))
Tactic: rw [← iSup_subtype'', sSup_image']
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
s : Set α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (sSup s) : β) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s) : β)
have rw : Eq.{u_2 + 1} (α := β) (⨆ a ∈ s, (f : (a : α) → β) a) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
Tactic: rw [map_sSup, ← sSup_image, f.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
s : Set α
rw : Eq.{u_2 + 1} (α := β) (⨆ a ∈ s, (f : (a : α) → β) a) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (sSup s) : β) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s) : β)
have rw₁ : Eq.{u_2 + 1} (α := β) (sSup ((⇑f : (a : α) → β) '' s)) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
Tactic: rw [map_sSup, ← sSup_image, f.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α ≃o β
s : Set α
rw : Eq.{u_2 + 1} (α := β) (⨆ a ∈ s, (f : (a : α) → β) a) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
rw₁ : Eq.{u_2 + 1} (α := β) (sSup ((⇑f : (a : α) → β) '' s)) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (sSup s) : β) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s) : β)
have rw₂ : Eq.{u_2 + 1} (α := β) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s)) (sSup ((⇑f.symm : (a : β) → α) ⁻¹' s))
Tactic: rw [map_sSup, ← sSup_image, f.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s t : Set β
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s ∪ t, f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)
have simp_rw : Eq.{u_1 + 1} (α := α) (⨆ (x : β), ⨆ (_ : x ∈ s ∨ x ∈ t), f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)
Tactic: simp_rw [mem_union, iSup_or, iSup_sup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s t : Set β
simp_rw : Eq.{u_1 + 1} (α := α) (⨆ (x : β), ⨆ (_ : x ∈ s ∨ x ∈ t), f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s ∪ t, f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)
have simp_rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (x : β), (⨆ (_ : x ∈ s), f x) ⊔ ⨆ (_ : x ∈ t), f x) ((⨆ x ∈ s, f x) ⊔ ⨆ x ∈ t, f x)
Tactic: simp_rw [mem_union, iSup_or, iSup_sup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
i₀ : β
⊢ ⨆ (i : β), f i = f i₀ ⊔ ⨆ (i : β), ⨆ (_ : i ≠ i₀), f i
have h : f i₀ = ⨆ (i : β), ⨆ (_ : i = i₀), f i
Tactic: convert! iSup_split f (fun i => i = i₀)
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
a b : β
⊢ ⨆ (x : β), ⨆ (_ : Membership.mem (γ := Set β) {a, b} x), f x = f a ⊔ f b
have rw : f a ⊔ ⨆ (x : β), ⨆ (_ : Membership.mem (γ := Set β) {b} x), f x = f a ⊔ f b
Tactic: rw [iSup_insert, iSup_singleton]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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
⊢ ⨆ (x : β), ⨆ (_ : Membership.mem (γ := Set β) {a, b} x), f x = f a ⊔ f b
have rw₁ : f a ⊔ f b = f a ⊔ f b
Tactic: rw [iSup_insert, iSup_singleton]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
γ : Type u_8
f : β → γ
g : γ → α
t : Set β
⊢ Eq.{u_1 + 1} (α := α) (⨆ c ∈ f '' t, g c) (⨆ b ∈ t, g (f b))
have rw : sSup (g '' f '' t) = ⨆ b ∈ t, g (f b)
Tactic: rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := α) (⨆ c ∈ f '' t, g c) (⨆ b ∈ t, g (f b))
have rw₁ : sSup (g '' f '' t) = sSup ((fun (b : β) ↦ g (f b)) '' t)
Tactic: rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := α) (⨆ c ∈ f '' t, g c) (⨆ b ∈ t, g (f b))
have rw₂ : sSup (g ∘ f '' t) = sSup ((fun (b : β) ↦ g (f b)) '' t)
Tactic: rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := α) (⨆ c ∈ f '' t, g c) (⨆ b ∈ t, g (f b))
have rw₃ : Eq.{u_1 + 1} (α := α) (sSup ((fun (x : β) ↦ g (f x)) '' t)) (sSup ((fun (b : β) ↦ g (f b)) '' t))
Tactic: rw [← sSup_image, ← sSup_image, ← image_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : CompleteLattice α
e : ι → β
he : Injective e
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (j : β), extend e f ⊥ j) (⨆ (i : ι), f i)
have 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)
Tactic: rw [iSup_split _ fun j => ∃ i, e i = j]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
s : Set β
t : Set γ
f : β → γ
g : γ → α
hf : BijOn f s t
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s, g (f x)) (⨆ y ∈ t, g y)
have rw : Eq.{u_1 + 1} (α := α) (⨆ x ∈ s, g (f x)) (⨆ y ∈ f '' s, g y)
Tactic: rw [← hf.image_eq, iSup_image]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ s, g (f x)) (⨆ y ∈ t, g y)
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ x ∈ s, g (f x)) (⨆ b ∈ s, g (f b))
Tactic: rw [← hf.image_eq, iSup_image]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ (j : ι), ⨆ (_ : j ≤ i), f j = (⨆ (j : ι), ⨆ (_ : j < i), f j) ⊔ f i
have rw : (⨆ (_ : i ≤ i), f i) ⊔ ⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≤ i), f i_1 = (⨆ (j : ι), ⨆ (_ : j < i), f j) ⊔ f i
Tactic: rw [iSup_split_single _ i]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
ι : Type u_8
inst_1 : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ (j : ι), ⨆ (_ : j ≥ i), f j = f i ⊔ ⨆ (j : ι), ⨆ (_ : j > i), f j
have rw : (⨆ (_ : i ≥ i), f i) ⊔ ⨆ (i_1 : ι), ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≥ i), f i_1 = f i ⊔ ⨆ (j : ι), ⨆ (_ : j > i), f j
Tactic: rw [iSup_split_single _ i]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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) (⨆ a ∈ s, ⨆ b ∈ t, f (a, b))
have simp_rw : Eq.{u_1 + 1} (α := α) (⨆ (i : β), ⨆ (j : γ), ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j)) (⨆ a ∈ s, ⨆ b ∈ t, f (a, b))
Tactic: simp_rw [iSup_prod, mem_prod, iSup_and]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
γ : Type u_8
δ : Type u_9
f : β → γ → δ
s : Set β
t : Set γ
g : δ → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ d ∈ image2 f s t, g d) (⨆ b ∈ s, ⨆ c ∈ t, g (f b c))
have 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))
Tactic: rw [← image_prod, iSup_image, biSup_prod]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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))
⊢ Eq.{u_1 + 1} (α := α) (⨆ d ∈ image2 f s t, g d) (⨆ b ∈ s, ⨆ c ∈ t, g (f b c))
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ b ∈ s ×ˢ t, g (f b.1 b.2)) (⨆ b ∈ s, ⨆ c ∈ t, g (f b c))
Tactic: rw [← image_prod, iSup_image, biSup_prod]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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))
⊢ Eq.{u_1 + 1} (α := α) (⨆ d ∈ image2 f s t, g d) (⨆ b ∈ s, ⨆ c ∈ t, g (f b c))
have 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))
Tactic: rw [← image_prod, iSup_image, biSup_prod]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)
have pos : ∀ (htriv : ∀ (i : ι), f i = ⊥), Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)
Tactic: by_cases! htriv : ∀ i, f i = ⊥
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)
have neg : ∀ (htriv : ∃ (i : ι), f i ≠ ⊥), Eq.{u_1 + 1} (α := α) (⨆ (i : { i : ι // f i ≠ ⊥ }), f (↑i : ι)) (⨆ (i : ι), f i)
Tactic: by_cases! htriv : ∀ i, f i = ⊥
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
have neg : ∀ (i : ι), ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)
Tactic: refine (iSup_comp_le f _).antisymm (iSup_mono' fun i => ?_)
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
i : ι
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)
have pos : ∀ (hi : f i = ⊥), ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)
Tactic: by_cases hi : f i = ⊥
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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' : ι)
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)
have neg : ∀ (hi : ¬f i = ⊥), ∃ (i' : { i : ι // f i ≠ ⊥ }), f i ≤ f (↑i' : ι)
Tactic: by_cases hi : f i = ⊥
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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' : ι)
have pos : ∃ (i' : { i : ι // f i ≠ ⊥ }), ⊥ ≤ f (↑i' : ι)
Tactic: rw [hi]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
htriv : ∃ (i : ι), f i ≠ ⊥
i : ι
hi : f i = ⊥
⊢ ∃ (i' : { i : ι // f i ≠ ⊥ }), ⊥ ≤ f (↑i' : ι)
have pos : ∀ (i₀ : ι) (hi₀ : f i₀ ≠ ⊥), ∃ (i' : { i : ι // f i ≠ ⊥ }), ⊥ ≤ f (↑i' : ι)
Tactic: obtain ⟨i₀, hi₀⟩ := htriv
Cleared hypotheses: htriv
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : CompleteLattice α
f : β → γ → α
s : Set β
t : Set γ
⊢ sSup (image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b
have rw : Eq.{u_1 + 1} (α := α) (sSup ((fun (x : β × γ) ↦ f x.1 x.2) '' s ×ˢ t)) (⨆ a ∈ s, ⨆ b ∈ t, f a b)
Tactic: rw [← image_prod, sSup_image, biSup_prod]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ sSup (image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b
have rw₁ : Eq.{u_1 + 1} (α := α) (⨆ a ∈ s ×ˢ t, f a.1 a.2) (⨆ a ∈ s, ⨆ b ∈ t, f a b)
Tactic: rw [← image_prod, sSup_image, biSup_prod]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ sSup (image2 f s t) = ⨆ a ∈ s, ⨆ b ∈ t, f a b
have rw₂ : Eq.{u_1 + 1} (α := α) (⨆ a ∈ s, ⨆ b ∈ t, f (a, b).1 (a, b).2) (⨆ a ∈ s, ⨆ b ∈ t, f a b)
Tactic: rw [← image_prod, sSup_image, biSup_prod]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_6
inst : CompleteLinearOrder α
f : (i : ι) → κ i → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), f i j) ⊤ ↔ ∀ b < ⊤, ∃ (i : ι) (j : κ i), b < f i j
have 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
Tactic: simp_rw [iSup_psigma', iSup_eq_top, PSigma.exists]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), f i j) ⊤ ↔ ∀ b < ⊤, ∃ (i : ι) (j : κ i), b < f i j
have 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
Tactic: simp_rw [iSup_psigma', iSup_eq_top, PSigma.exists]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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 x x_1)
have rw : IsLUB (eval (β := β) x_1 '' x) (sSup (eval (β := β) x_1 '' x))
Tactic: rw [sSup_apply_eq_sSup_image]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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 x x_1)
have rw : IsGLB (eval (β := β) x_1 '' x) (sInf (eval (β := β) x_1 '' x))
Tactic: rw [sInf_apply_eq_sInf_image]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_8
β : α → Type u_9
ι : Sort u_10
inst : (i : α) → SupSet (β i)
f : ι → (a : α) → β a
a : α
⊢ Eq.{u_9 + 1} (α := β a) ((⨆ (i : ι), f i) a) (⨆ (i : ι), f i a)
have rw : Eq.{u_9 + 1} (α := β a) (sSup (range ((fun (f : (i : α) → β i) ↦ f a) ∘ f))) (sSup (range fun (i : ι) ↦ f i a))
Tactic: rw [iSup, sSup_apply, iSup, iSup, ← image_eq_range (fun f : ∀ i, β i => f a) (range f), ←
    range_comp]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : SupSet α
inst_1 : SupSet β
f : ι → α × β
⊢ (iSup f).swap = ⨆ (i : ι), (f i).swap
have simp_rw : (sSup (range f)).swap = sSup (range fun (i : ι) ↦ (f i).swap)
Tactic: simp_rw [iSup, swap_sSup, ← range_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ (iSup f).swap = ⨆ (i : ι), (f i).swap
have simp_rw₁ : sSup (swap '' range f) = sSup (range fun (i : ι) ↦ (f i).swap)
Tactic: simp_rw [iSup, swap_sSup, ← range_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.Basic (goal)
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)
⊢ (iSup f).swap = ⨆ (i : ι), (f i).swap
have simp_rw₂ : sSup (range (swap ∘ f)) = sSup (range fun (i : ι) ↦ (f i).swap)
Tactic: simp_rw [iSup, swap_sSup, ← range_comp, comp_def]