awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteLattice.PiLex (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : LinearOrder ι
inst_1 : (i : ι) → CompleteLinearOrder (α i)
inst_2 : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun (i : ι) ↦ α i) i))
e : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)
h : e ∈ upperBounds s
a : ι
ha :
  (∀ (j : ι), (fun (x1 x2 : ι) ↦ x1 < x2) j a → e j = sSup s j) ∧
    (fun {i : ι} (x1 x2 : (fun (i : ι) ↦ ((fun (i : ι) ↦ α i) i : Type u_2)) i) ↦ x1 < x2) (e a) (sSup s a)
⊢ False
have refine_2 : ∀ (f : Lex ((i : ι) → (fun (i : ι) ↦ α i) i)) (hf : f ∈ s) (hf' : ∀ j < a, f j = sSup s j), ∀ j < a, f j = e j
Tactic: refine ha.2.not_ge <| sSup_apply_le fun f hf hf' ↦ apply_le_of_toLex (h hf) ?_
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddAbove t
⊢ IsLUB ((fun {y : (↑s : Type u_2)} ↦ (↑y : α)) '' t) (↑(sSup t) : α)
have rw : IsLUB ((fun {y : (↑s : Type u_2)} ↦ (↑y : α)) '' t) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))
Tactic: rw [← subset_sSup_of_within s ht h_bdd (h_Sup ht h_bdd)]
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLinearOrder α
inst_1 : Inhabited (↑s : Type u_2)
h_Sup :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddAbove t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
h_Inf :
  ∀ {t : Set (↑s : Type u_2)},
    t.Nonempty → ∀ (_h_bdd : BddBelow t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddBelow t
⊢ IsGLB ((fun {x : (↑s : Type u_2)} ↦ (↑x : α)) '' t) (↑(sInf t) : α)
have rw : IsGLB ((fun {x : (↑s : Type u_2)} ↦ (↑x : α)) '' t) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t))
Tactic: rw [← subset_sInf_of_within s ht h_bdd (h_Inf ht h_bdd)]
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddAbove t
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
have obtain : ∀ (c : (↑s : Type u_2)) (hct : c ∈ t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
Tactic: obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
h_bdd : BddAbove t
c : (↑s : Type u_2)
hct : c ∈ t
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
have obtain : ∀ (B : (↑s : Type u_2)) (hB : B ∈ upperBounds t), sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
Tactic: obtain ⟨B, hB⟩ : ∃ B, B ∈ upperBounds t := h_bdd
Cleared hypotheses: h_bdd
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ upperBounds t
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
have refine_1 : (↑c : α) ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
Tactic: refine hs.out c.2 B.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ upperBounds t
refine_1 : (↑c : α) ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
have refine_2 : sSup (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ≤ (↑B : α)
Tactic: refine hs.out c.2 B.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
ht : t.Nonempty
h_bdd : BddBelow t
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
have obtain : ∀ (c : (↑s : Type u_2)) (hct : c ∈ t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
Tactic: obtain ⟨c, hct⟩ : ∃ c, c ∈ t := ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
h_bdd : BddBelow t
c : (↑s : Type u_2)
hct : c ∈ t
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
have obtain : ∀ (B : (↑s : Type u_2)) (hB : B ∈ lowerBounds t), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
Tactic: obtain ⟨B, hB⟩ : ∃ B, B ∈ lowerBounds t := h_bdd
Cleared hypotheses: h_bdd
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ lowerBounds t
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
have refine_1 : (↑B : α) ≤ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
Tactic: refine hs.out B.2 c.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrder α
s : Set α
hs : s.OrdConnected
t : Set (↑s : Type u_2)
c : (↑s : Type u_2)
hct : c ∈ t
B : (↑s : Type u_2)
hB : B ∈ lowerBounds t
refine_1 : (↑B : α) ≤ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t)
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ∈ s
have refine_2 : sInf (Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t) ≤ (↑c : α)
Tactic: refine hs.out B.2 c.2 ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : ¬S = ∅
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ∈ Icc a b
have hS₁ : S.Nonempty
Tactic: rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ∈ Icc a b
have refine : a ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)
Tactic: refine ⟨?_, csSup_le (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.2)⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
⊢ a ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)
have obtain : ∀ (c : (↑(Icc a b) : Type u_2)) (hc : c ∈ S), a ≤ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)
Tactic: obtain ⟨c, hc⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
⊢ IsLUB S
    (if hS : S = ∅ then Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯
    else Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)
have pos : ∀ (hS : S = ∅), IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a sorry)
Tactic: split_ifs with hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
pos : ∀ (hS : S = ∅), IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)
⊢ IsLUB S
    (if hS : S = ∅ then Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯
    else Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)
have neg : ∀ (hS : ¬S = ∅),
  IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) sorry)
Tactic: split_ifs with hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S = ∅
⊢ IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)
have pos : IsLUB (α := (↑(Icc a b) : Type u_2)) ∅ (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a sorry)
Tactic: subst hS
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
⊢ IsLUB (α := (↑(Icc a b) : Type u_2)) ∅ (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a ⋯)
have pos : Eq (α := (↑(Icc a b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) a sorry) ⊥
Tactic: simp only [isLUB_empty_iff, isBot_iff_eq_bot]
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (hypothesis)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : ¬S = ∅
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ∈ Icc a b
have hS₁ : S.Nonempty
Tactic: rw [← Set.not_nonempty_iff_eq_empty, not_not] at hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ∈ Icc a b
have refine : sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ≤ b
Tactic: refine ⟨le_csInf (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.1), ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ≤ b
have obtain : ∀ (c : (↑(Icc a b) : Type u_2)) (hc : c ∈ S), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ≤ b
Tactic: obtain ⟨c, hc⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
⊢ IsGLB S
    (if hS : S = ∅ then Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯
    else Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)
have pos : ∀ (hS : S = ∅), IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b sorry)
Tactic: split_ifs with hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
pos : ∀ (hS : S = ∅), IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)
⊢ IsGLB S
    (if hS : S = ∅ then Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯
    else Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)
have neg : ∀ (hS : ¬S = ∅),
  IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) sorry)
Tactic: split_ifs with hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S = ∅
⊢ IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)
have pos : IsGLB (α := (↑(Icc a b) : Type u_2)) ∅ (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b sorry)
Tactic: subst hS
Cleared hypotheses: S, hS
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
⊢ IsGLB (α := (↑(Icc a b) : Type u_2)) ∅ (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)
have pos : Eq (α := (↑(Icc a b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b sorry) ⊤
Tactic: simp only [isGLB_empty_iff, isTop_iff_eq_top]
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
⊢ Eq.{u_2 + 1} (α := α) (↑(⨆ (i : ι), f i) : α) (⨆ (i : ι), (↑(f i) : α))
have rw : Eq.{u_2 + 1} (α := α)
  (sSup (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)))
  (⨆ (i : ι), (↑(f i) : α))
Tactic: rw [iSup, coe_sSup]
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
⊢ Eq.{u_2 + 1} (α := α)
    (sSup (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)))
    (⨆ (i : ι), (↑(f i) : α))
have e_a : Eq.{u_2 + 1} (α := Set α)
  (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i))
  (range fun (i : ι) ↦ (↑(f i) : α))
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
⊢ Eq.{u_2 + 1} (α := Set α)
    (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i))
    (range fun (i : ι) ↦ (↑(f i) : α))
have e_a : ∀ (x : α),
  Membership.mem (γ := Set α)
      (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)) x ↔
    Membership.mem (γ := Set α) (range fun (i : ι) ↦ (↑(f i) : α)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
⊢ (↑(⨅ (i : ι), f i) : α) = a ⊓ ⨅ (i : ι), (↑(f i) : α)
have rw : a ⊓ sInf (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)) =
  a ⊓ ⨅ (i : ι), (↑(f i) : α)
Tactic: rw [iInf, coe_sInf]
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
⊢ a ⊓ sInf (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)) =
    a ⊓ ⨅ (i : ι), (↑(f i) : α)
have e_a : Eq.{u_2 + 1} (α := Set α)
  (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i))
  (range fun (i : ι) ↦ (↑(f i) : α))
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
⊢ (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
have inl : IsEmpty ι → (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
inl : IsEmpty ι → (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
⊢ (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
have inr : Nonempty ι → (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
h : Nonempty ι
⊢ (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
have inr : a ⊓ ⨅ (i : ι), a ⊓ ⨅ (_ : p i), (↑(f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
Tactic: simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
h : Nonempty ι
inr : a ⊓ ⨅ (i : ι), a ⊓ ⨅ (_ : p i), (↑(f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
⊢ (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
have inr₁ : a ⊓ (a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α)) = a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α)
Tactic: simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Order.CompleteLatticeIntervals (goal)
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
h : Nonempty ι
inr : a ⊓ ⨅ (i : ι), a ⊓ ⨅ (_ : p i), (↑(f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
inr₁ : a ⊓ (a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α)) = a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α)
⊢ (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
have inr₂ : a ⊓ a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α) = a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α)
Tactic: simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]
-- Lean 4 proof step from Mathlib.Order.CompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CompletePartialOrder α
inst_1 : Preorder β
f : α → β
⊢ ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
have refine : ∀ (h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))) (d : Set α)
  (hne : d.Nonempty) (hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (a : α) (hda : IsLUB d a), IsLUB (f '' d) (f a)
Tactic: refine ⟨fun h d hd₁ hd₂ ↦ h hd₁ hd₂ hd₂.isLUB_sSup, fun h d hne hd a hda ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.CompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
inst : CompletePartialOrder α
inst_1 : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f a)
have rw : IsLUB (f '' d) (f (sSup d))
Tactic: rw [hda.unique hd.isLUB_sSup]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊔ y ∈ carrier
have suffices : x ⊔ y = sSup {x, y}
Tactic: suffices x ⊔ y = sSup {x, y} by exact this ▸ sSupClosed' (fun z hz ↦ by aesop)
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊓ y ∈ carrier
have suffices : x ⊓ y = sInf {x, y}
Tactic: suffices x ⊓ y = sInf {x, y} by exact this ▸ sInfClosed' (fun z hz ↦ by aesop)
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L M : CompleteSublattice α
h :
  Eq.{u_1 + 1} (α := Set α) ((fun (L : CompleteSublattice α) ↦ L.carrier) L)
    ((fun (L : CompleteSublattice α) ↦ L.carrier) M)
⊢ L = M
have mk : ∀ (toSublattice : Sublattice α) (sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier)
  (sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (L : CompleteSublattice α) ↦ L.carrier)
        { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
      ((fun (L : CompleteSublattice α) ↦ L.carrier) M)),
  { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' : CompleteSublattice α } = M
Tactic: cases L
Cleared hypotheses: L, h
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L M : CompleteSublattice α
toSublattice : Sublattice α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
    ((fun (L : CompleteSublattice α) ↦ L.carrier) M)
⊢ { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' : CompleteSublattice α } = M
have mk : ∀ (toSublattice_1 : Sublattice α)
  (sSupClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sSup s ∈ toSublattice_1.carrier)
  (sInfClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sInf s ∈ toSublattice_1.carrier)
  (h :
    Eq.{u_1 + 1} (α := Set α)
      ((fun (L : CompleteSublattice α) ↦ L.carrier)
        { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
      ((fun (L : CompleteSublattice α) ↦ L.carrier)
        { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 })),
  { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' : CompleteSublattice α } =
    { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 }
Tactic: cases M
Cleared hypotheses: M, h
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L : CompleteSublattice α
toSublattice : Sublattice α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier
toSublattice_1 : Sublattice α
sSupClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sSup s ∈ toSublattice_1.carrier
sInfClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sInf s ∈ toSublattice_1.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 })
⊢ { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' : CompleteSublattice α } =
    { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 }
have mk : toSublattice = toSublattice_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ (↑(sSup S) : α) = ⨆ N ∈ S, (↑N : α)
have rw : Eq.{u_1 + 1} (α := α) (sSup {x : α | ∃ s ∈ S, (↑s : α) = x}) (⨆ N ∈ S, (↑N : α))
Tactic: rw [coe_sSup, ← Set.image, sSup_image]
-- Lean 4 proof step from Mathlib.Order.CompleteSublattice (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
rw : Eq.{u_1 + 1} (α := α) (sSup {x : α | ∃ s ∈ S, (↑s : α) = x}) (⨆ N ∈ S, (↑N : α))
⊢ (↑(sSup S) : α) = ⨆ N ∈ S, (↑N : α)
have rw₁ : sSup (Subtype.val (p := fun (x : α) ↦ x ∈ L) '' S) = ⨆ N ∈ S, (↑N : α)
Tactic: rw [coe_sSup, ← Set.image, sSup_image]