awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑∅ : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑∅ : Type u_5)), g (f (↑i : ι)))
inl :
  Eq.{u_1 + 1} (α := α) (⨆ (i : ι'), ⨆ (_ : Membership.mem (γ := Set ι') ∅ i), g i)
    (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
inl₁ : Eq.{u_1 + 1} (α := α) (sSup ∅) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' ∅, g i) (⨆ (x : ι), ⨆ (_ : Membership.mem (γ := Set ι) ∅ x), g (f x))
have inl₂ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [Set.image_empty, cbiSup_empty, cbiSup_empty]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
have hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
Tactic: have hg : BddAbove (Set.range fun i : f '' s ↦ g i) := by
    simpa [bddAbove_def] using hf
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
⊢ LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
have refine : LE.le.{u_1} (α := α) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι))) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
Tactic: refine hg'.trans ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
⊢ LE.le.{u_1} (α := α) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι))) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
have this : Nonempty.{u_5 + 1} (↑s : Type u_5)
Tactic: have : Nonempty s := Set.Nonempty.to_subtype hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
⊢ LE.le.{u_1} (α := α) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι))) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
have refine : ∀ (x : (↑s : Type u_5)), g (f (↑x : ι)) ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
Tactic: refine ciSup_le ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
⊢ ∃ (t : (↑(f '' s) : Type u_6)), g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))
have this₁ : f i ∈ f '' s
Tactic: have : f i ∈ f '' s := Set.mem_image_of_mem _ h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
⊢ g (f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι)) ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
have obtain : ∀ (t : (↑(f '' s) : Type u_6)) (ht : g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))),
  g (f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι)) ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
Tactic: obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
      have : f i ∈ f '' s := Set.mem_image_of_mem _ h
      exact ⟨⟨f i, this⟩, by simp⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
t : (↑(f '' s) : Type u_6)
ht : g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))
⊢ g (f (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) : ι)) ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
have rw : g (↑t : ι') ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
Tactic: rw [← ht]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
this : Nonempty.{u_5 + 1} (↑s : Type u_5)
i : ι
h : i ∈ s
t : (↑(f '' s) : Type u_6)
ht : g (↑t : ι') = g (f (↑(Subtype.mk (p := Membership.mem s) i h) : ι))
⊢ g (↑t : ι') ≤ ⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι')
have refine : BddAbove (g '' f '' s)
Tactic: refine le_ciSup_set ?_ t.prop
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
have hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
Tactic: have hf' : sSup ∅ ≤ ⨆ i : f '' s, g i := by
    refine hg'.trans ?_
    have : Nonempty s := Set.Nonempty.to_subtype hs
    refine ciSup_le ?_
    intro ⟨i, h⟩
    obtain ⟨t, ht⟩ : ∃ t : f '' s, g t = g (f (Subtype.mk i h)) := by
      have : f i ∈ f '' s := Set.mem_image_of_mem _ h
      exact ⟨⟨f i, this⟩, by simp⟩
    rw [← ht]
    refine le_ciSup_set ?_ t.prop
    simpa [bddAbove_def] using hf
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
have inr : sSup (g '' f '' s) = ⨆ x ∈ s, g (f x)
Tactic: rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
inr : sSup (g '' f '' s) = ⨆ x ∈ s, g (f x)
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
have inr₁ : sSup (g '' f '' s) = sSup ((fun (x : ι) ↦ g (f x)) '' s)
Tactic: rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
inr : sSup (g '' f '' s) = ⨆ x ∈ s, g (f x)
inr₁ : sSup (g '' f '' s) = sSup ((fun (x : ι) ↦ g (f x)) '' s)
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
have inr₂ : sSup (g ∘ f '' s) = sSup ((fun (x : ι) ↦ g (f x)) '' s)
Tactic: rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove.{u_1} (α := α) (range fun (i : (↑s : Type u_5)) ↦ g (f (↑i : ι)))
hg' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑s : Type u_5)), g (f (↑i : ι)))
hs : s.Nonempty
hg : BddAbove.{u_1} (α := α) (range fun (i : (↑(f '' s) : Type u_6)) ↦ g (↑i : ι'))
hf' : LE.le.{u_1} (α := α) (sSup ∅) (⨆ (i : (↑(f '' s) : Type u_6)), g (↑i : ι'))
inr : sSup (g '' f '' s) = ⨆ x ∈ s, g (f x)
inr₁ : sSup (g '' f '' s) = sSup ((fun (x : ι) ↦ g (f x)) '' s)
inr₂ : sSup (g ∘ f '' s) = sSup ((fun (x : ι) ↦ g (f x)) '' s)
⊢ Eq.{u_1 + 1} (α := α) (⨆ i ∈ f '' s, g i) (⨆ x ∈ s, g (f x))
have inr₃ : Eq.{u_1 + 1} (α := α) (sSup ((fun (x : ι) ↦ g (f x)) '' s)) (sSup ((fun (x : ι) ↦ g (f x)) '' s))
Tactic: rw [← csSup_image hg hf', ← csSup_image hf hg', ← Set.image_comp, comp_def]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
have pos : ∀ (h : Exists p), LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f sorry)
Tactic: by_cases! h : Exists p
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
pos : ∀ (h : Exists p), LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
have neg : ∀ (h : ∀ (x : ι), ¬p x), LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f sorry)
Tactic: by_cases! h : Exists p
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (hypothesis)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
have this : Nonempty (Exists p)
Tactic: have : Nonempty <| Exists p := ⟨h⟩
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : Exists p
this : Nonempty (Exists p)
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
have pos : Exists p →
  ∀ (i : ι) (hi : p i),
    Membership.mem (γ := Set α) (upperBounds (⋃ (i_1 : ι), range (ι := p i_1) ((fun (x : ι) (x_1 : p x) ↦ f sorry) i_1)))
      (f sorry)
Tactic: refine ciSup_le fun ⟨i, hi⟩ ↦ le_ciSup₂ (f := fun _ _ ↦ _) ⟨f ⟨i, hi⟩, ?_⟩ i hi
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
have neg : IsEmpty ι → LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f sorry)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLattice α
p : ι → Prop
f : Exists p → α
h : ∀ (x : ι), ¬p x
neg : IsEmpty ι → LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
⊢ LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f ⋯)
have neg₁ : Nonempty ι → LE.le.{u_1} (α := α) (⨆ (ih : Exists p), f ih) (⨆ (i : ι), ⨆ (h : p i), f sorry)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
have pos : ∀ (hp : p), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f sorry)
Tactic: by_cases hp : p
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
pos : ∀ (hp : p), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
have neg : ∀ (hp : ¬p), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f sorry)
Tactic: by_cases hp : p
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
have pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f sorry)
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : p
pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
have neg : ∀ (hq : ¬q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f sorry)
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
have pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f sorry)
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
p q : Prop
f : p ∧ q → α
hp : ¬p
pos : ∀ (hq : q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f ⋯)
have neg : ∀ (hq : ¬q), Eq.{u_1 + 1} (α := α) (⨆ (ih : p ∧ q), f ih) (⨆ (h₁ : p), ⨆ (h₂ : q), f sorry)
Tactic: by_cases hq : q
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
have pos : ∀ (hf : ¬BddAbove (range f)), LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
Tactic: by_cases! hf : ¬BddAbove (range f)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
pos :
  ∀ (hf : ¬BddAbove (range f)),
    LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
have neg : ∀ (hf : BddAbove (range f)), LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
Tactic: by_cases! hf : ¬BddAbove (range f)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : ¬BddAbove (range f)
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
have pos : LE.le.{u_1} (α := α) (sSup ∅) (max (sSup ∅) (⨆ (x : ι), g x))
Tactic: rw [ciSup_of_not_bddAbove hf, ciSup_of_not_bddAbove <| mt bbdAbove_range_left_of_sup hf]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
have pos : ∀ (hg : ¬BddAbove (range g)), LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
Tactic: by_cases! hg : ¬BddAbove (range g)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
pos :
  ∀ (hg : ¬BddAbove (range g)),
    LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
have neg : ∀ (hg : BddAbove (range g)), LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
Tactic: by_cases! hg : ¬BddAbove (range g)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
f g : ι → α
hf : BddAbove (range f)
hg : ¬BddAbove (range g)
⊢ LE.le.{u_1} (α := α) (⨆ (x : ι), max (f x) (g x)) (max (⨆ (x : ι), f x) (⨆ (x : ι), g x))
have pos : LE.le.{u_1} (α := α) (sSup ∅) (max (⨆ (x : ι), f x) (sSup ∅))
Tactic: rw [ciSup_of_not_bddAbove hg, ciSup_of_not_bddAbove <| mt bbdAbove_range_right_of_sup hg]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
have inl : ∀ (le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f),
  ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
Tactic: rcases le_or_gt (sSup ∅) (iSup f) with le | gt
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
inl :
  ∀ (le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f),
    ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
have inr : ∀ (gt : iSup.{u_1, max 1 u_4} f < sSup ∅),
  ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
Tactic: rcases le_or_gt (sSup ∅) (iSup f) with le | gt
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
have inl : ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
Tactic: rw [max_eq_left le]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
have pos : ∀ (bdd : BddAbove (range.{u_1, max 1 u_4} f)),
  ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
Tactic: by_cases bdd : BddAbove (range f)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
pos :
  ∀ (bdd : BddAbove (range.{u_1, max 1 u_4} f)),
    ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
have neg : ∀ (bdd : ¬BddAbove (range.{u_1, max 1 u_4} f)),
  ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
Tactic: by_cases bdd : BddAbove (range f)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
bdd : BddAbove (range.{u_1, max 1 u_4} f)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
have pos : iSup.{u_1, max 1 u_4} f = iSup.{u_1, max 1 u_4} f
Tactic: rw [← ciSup_subtype bdd le]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
bdd : ¬BddAbove (range.{u_1, max 1 u_4} f)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
have neg : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)
Tactic: rw [ciSup_of_not_bddAbove bdd, cbiSup_of_not_bddAbove bdd]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup.{u_1, max 1 u_4} f
bdd : ¬BddAbove (range.{u_1, max 1 u_4} f)
neg : Eq.{u_1 + 1} (α := α) (⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h)) (sSup ∅)
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = iSup.{u_1, max 1 u_4} f
have neg₁ : Eq.{u_1 + 1} (α := α) (sSup ∅) (sSup ∅)
Tactic: rw [ciSup_of_not_bddAbove bdd, cbiSup_of_not_bddAbove bdd]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Indexed (goal)
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
gt : iSup.{u_1, max 1 u_4} f < sSup ∅
⊢ ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
have inr : ∀ (i : ι) (hi : ¬p i), ⨆ (i : ι), ⨆ (h : p i), f (Subtype.mk (p := p) i h) = max (iSup.{u_1, max 1 u_4} f) (sSup ∅)
Tactic: have ⟨i, hi⟩ := not_forall.mp hp