awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)) → (↑(↑a : Set α) : Type u)
⊢ LE.le.{u} (α := α) (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))
    (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))
have refine : LE.le.{u} (α := α) (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))
  (⨅ (i : ι),
    f i
      ((fun (a : ι) ↦
          (Classical.choose (p := fun (x : κ a) ↦
              f a x =
                (↑(g
                      (Subtype.mk (p := fun (x : Set α) ↦
                        Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                        ((fun (x : ι) ↦ range (f x)) a) sorry)) :
                  α))
              sorry :
            κ a))
        i))
Tactic: refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)) → (↑(↑a : Set α) : Type u)
⊢ LE.le.{u} (α := α) (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), (↑(g a) : α))
    (⨅ (i : ι),
      f i
        ((fun (a : ι) ↦
            (Classical.choose (p := fun (x : κ a) ↦
                f a x =
                  (↑(g
                        (Subtype.mk (p := fun (x : Set α) ↦
                          Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                          ((fun (x : ι) ↦ range (f x)) a) ⋯)) :
                    α))
                ⋯ :
              κ a))
          i))
have refine : ∀ (a : ι),
  (↑(g
          (Subtype.mk (p := fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
            (range (f a)) sorry)) :
      α) ≤
    f a
      ((fun (a : ι) ↦
          (Classical.choose (p := fun (x : κ a) ↦
              f a x =
                (↑(g
                      (Subtype.mk (p := fun (x : Set α) ↦
                        Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                        ((fun (x : ι) ↦ range (f x)) a) sorry)) :
                  α))
              sorry :
            κ a))
        a)
Tactic: refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)) → (↑(↑a : Set α) : Type u)
a : ι
⊢ (↑(g
          (Subtype.mk (p := fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
            (range (f a)) ⋯)) :
      α) ≤
    f a
      ((fun (a : ι) ↦
          (Classical.choose (p := fun (x : κ a) ↦
              f a x =
                (↑(g
                      (Subtype.mk (p := fun (x : Set α) ↦
                        Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                        ((fun (x : ι) ↦ range (f x)) a) ⋯)) :
                  α))
              ⋯ :
            κ a))
        a)
have rw : f a
    (Classical.choose (p := fun (x : κ a) ↦
      f a x =
        (↑(g
              (Subtype.mk (p := fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                ((fun (x : ι) ↦ range (f x)) a) sorry)) :
          α))
      sorry) ≤
  f a
    (Classical.choose (p := fun (x : κ a) ↦
      f a x =
        (↑(g
              (Subtype.mk (p := fun (x : Set α) ↦ Membership.mem (γ := Set (Set α)) (range fun (x : ι) ↦ range (f x)) x)
                ((fun (x : ι) ↦ range (f x)) a) sorry)) :
          α))
      sorry)
Tactic: rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ LE.le.{u} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))
have _ : Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
  (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), ⨆ (b : (↑(↑a : Set α) : Type u)), (↑b : α))
Tactic: calc
    _ = ⨅ a : range (range <| f ·), ⨆ b : a.1, b.1 := by
      simp_rw [iInf_subtype, iInf_range, iSup_subtype, iSup_range]
    _ = _ := minAx.iInf_iSup_eq _
    _ ≤ _ := iSup_le fun g => by
      refine le_trans ?_ <| le_iSup _ fun a => Classical.choose (g ⟨_, a, rfl⟩).2
      refine le_iInf fun a => le_trans (iInf_le _ ⟨range (f a), a, rfl⟩) ?_
      rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ let x := minAx.toCompleteLattice;
  Eq.{u + 1} (α := α) (⨆ (i : ι), ⨅ (j : κ i), f i j) (⨅ (g : (i : ι) → κ i), ⨆ (i : ι), f i (g i))
have refine : LE.le.{u} (α := α) (⨅ (g : (i : ι) → κ i), ⨆ (i : ι), f i (g i)) (⨆ (i : ι), ⨅ (j : κ i), f i j)
Tactic: refine le_antisymm iSup_iInf_le ?_
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ LE.le.{u} (α := α) (⨅ (g : (i : ι) → κ i), ⨆ (i : ι), f i (g i)) (⨆ (i : ι), ⨅ (j : κ i), f i j)
have rw : LE.le.{u} (α := α) (⨆ (g : (i : (i : ι) → κ i) → ι), ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)))
  (⨆ (i : ι), ⨅ (j : κ i), f i j)
Tactic: rw [minAx.iInf_iSup_eq']
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ LE.le.{u} (α := α) (⨆ (g : (i : (i : ι) → κ i) → ι), ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)))
    (⨆ (i : ι), ⨅ (j : κ i), f i j)
have refine : ∀ (g : (i : (i : ι) → κ i) → ι),
  LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨆ (i : ι), ⨅ (j : κ i), f i j)
Tactic: refine iSup_le fun g => ?_
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
⊢ ∃ (a : ι),
    ∀ (b : κ a),
      ∃ (f : (i : ι) → κ i) (h : a = g f),
        Eq.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) b h : κ (g f)) (f (g f) : κ (g f))
have by_contra! : ∀
  (h :
    ∀ (a : ι),
      ∃ (b : κ a),
        ∀ (f : (i : ι) → κ i) (h : a = g f),
          Ne.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) b h : κ (g f)) (f (g f) : κ (g f))),
  False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
h :
  ∀ (a : ι),
    ∃ (b : κ a),
      ∀ (f : (i : ι) → κ i) (h : a = g f),
        Ne.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) b h : κ (g f)) (f (g f) : κ (g f))
⊢ False
have choose : ∀ (h : (a : ι) → κ a)
  (hh :
    ∀ (a : ι) (f : (i : ι) → κ i) (h_1 : a = g f),
      Ne.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) (h a) h_1 : κ (g f))
        (f (g f) : κ (g f))),
  False
Tactic: choose h hh using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (hypothesis)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
h : (a : ι) → κ a
hh :
  ∀ (a : ι) (f : (i : ι) → κ i) (h_1 : a = g f),
    Ne.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) (h a) h_1 : κ (g f)) (f (g f) : κ (g f))
⊢ False
have this : Ne.{w'} (α := κ (g h)) (Eq.rec (motive := fun (x : ι) (h : g h = x) ↦ κ x) (h (g h)) sorry : κ (g h)) (h (g h) : κ (g h))
Tactic: have := hh _ h rfl
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
⊢ LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨆ (i : ι), ⨅ (j : κ i), f i j)
have have : ∀ (a : ι)
  (ha :
    ∀ (b : κ a),
      ∃ (f : (i : ι) → κ i) (h : a = g f),
        Eq.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) b h : κ (g f)) (f (g f) : κ (g f))),
  LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨆ (i : ι), ⨅ (j : κ i), f i j)
Tactic: have ⟨a, ha⟩ : ∃ a, ∀ b, ∃ f, ∃ h : a = g f, h ▸ b = f (g f) := by
    by_contra! h
    choose h hh using h
    have := hh _ h rfl
    contradiction
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
a : ι
ha :
  ∀ (b : κ a),
    ∃ (f : (i : ι) → κ i) (h : a = g f),
      Eq.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) b h : κ (g f)) (f (g f) : κ (g f))
⊢ LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨆ (i : ι), ⨅ (j : κ i), f i j)
have refine : LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨅ (j : κ a), f a j)
Tactic: refine le_trans ?_ (le_iSup _ a)
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
a : ι
ha :
  ∀ (b : κ a),
    ∃ (f : (i : ι) → κ i) (h : a = g f),
      Eq.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) b h : κ (g f)) (f (g f) : κ (g f))
⊢ LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨅ (j : κ a), f a j)
have refine : ∀ (b : κ a), ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)) ≤ f a b
Tactic: refine le_iInf fun b => ?_
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
a : ι
ha :
  ∀ (b : κ a),
    ∃ (f : (i : ι) → κ i) (h : a = g f),
      Eq.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : a = x) ↦ κ x) b h : κ (g f)) (f (g f) : κ (g f))
b : κ a
⊢ ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)) ≤ f a b
have obtain : ∀ (h : (i : ι) → κ i)
  (ha :
    ∀ (b : κ (g h)),
      ∃ (f : (i : ι) → κ i) (h_1 : g h = g f),
        Eq.{w'} (α := κ (g f)) (Eq.rec (motive := fun (x : ι) (h : g h = x) ↦ κ x) b h_1 : κ (g f))
          (f (g f) : κ (g f))),
  ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)) ≤ f (g h) (h (g h))
Tactic: obtain ⟨h, rfl, rfl⟩ := ha b
Cleared hypotheses: a, ha, b
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ LE.le.{u} (α := α)
    (⨅ (i : ULift Bool),
      ⨆ (j :
        match (motive := ULift Bool → Type u) i with
        | { down := true } => PUnit
        | { down := false } => (↑s : Type u)),
        match (motive :=
          (i : ULift Bool) →
            (j :
                match (motive := ULift Bool → Type u) i with
                | { down := true } => PUnit
                | { down := false } => (↑s : Type u)) →
              α)
          i, j with
        | { down := true }, j => a
        | { down := false }, j => (↑j : α))
    (⨆ b ∈ s, a ⊓ b)
have simp : ∀
  (i :
    (a : ULift Bool) →
      match (motive := ULift Bool → Type u) a with
      | { down := true } => PUnit
      | { down := false } => (↑s : Type u)),
  a ⊓ (↑(i { down := false : ULift Bool }) : α) ≤ ⨆ b ∈ s, a ⊓ b
Tactic: simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
have _ : a ⊓ sSup s =
  ⨅ (i : ULift Bool),
    ⨆ (j :
      match (motive := ULift Bool → Type u) i with
      | { down := true } => PUnit
      | { down := false } => (↑s : Type u)),
      match (motive :=
        (i : ULift Bool) →
          (j :
              match (motive := ULift Bool → Type u) i with
              | { down := true } => PUnit
              | { down := false } => (↑s : Type u)) →
            α)
        i, j with
      | { down := true }, j => a
      | { down := false }, j => (↑j : α)
Tactic: calc
      _ = ⨅ i : ULift.{u} Bool, ⨆ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]
      _ ≤ _ := by
        simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
        exact fun x ↦ le_biSup _ (x (.up false)).2
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
_ :
  a ⊓ sSup s =
    ⨅ (i : ULift Bool),
      ⨆ (j :
        match (motive := ULift Bool → Type u) i with
        | { down := true } => PUnit
        | { down := false } => (↑s : Type u)),
        match (motive :=
          (i : ULift Bool) →
            (j :
                match (motive := ULift Bool → Type u) i with
                | { down := true } => PUnit
                | { down := false } => (↑s : Type u)) →
              α)
          i, j with
        | { down := true }, j => a
        | { down := false }, j => (↑j : α)
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
have _₁ : LE.le.{u} (α := α)
  (⨅ (i : ULift Bool),
    ⨆ (j :
      match (motive := ULift Bool → Type u) i with
      | { down := true } => PUnit
      | { down := false } => (↑s : Type u)),
      match (motive :=
        (i : ULift Bool) →
          (j :
              match (motive := ULift Bool → Type u) i with
              | { down := true } => PUnit
              | { down := false } => (↑s : Type u)) →
            α)
        i, j with
      | { down := true }, j => a
      | { down := false }, j => (↑j : α))
  (⨆ b ∈ s, a ⊓ b)
Tactic: calc
      _ = ⨅ i : ULift.{u} Bool, ⨆ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]
      _ ≤ _ := by
        simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]
        exact fun x ↦ le_biSup _ (x (.up false)).2
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ LE.le.{u} (α := α) (⨅ b ∈ s, a ⊔ b)
    (⨆ (i : ULift Bool),
      ⨅ (j :
        match (motive := ULift Bool → Type u) i with
        | { down := true } => PUnit
        | { down := false } => (↑s : Type u)),
        match (motive :=
          (i : ULift Bool) →
            (j :
                match (motive := ULift Bool → Type u) i with
                | { down := true } => PUnit
                | { down := false } => (↑s : Type u)) →
              α)
          i, j with
        | { down := true }, j => a
        | { down := false }, j => (↑j : α))
have simp : ∀
  (i :
    (i : ULift Bool) →
      match (motive := ULift Bool → Type u) i with
      | { down := true } => PUnit
      | { down := false } => (↑s : Type u)),
  ⨅ b ∈ s, a ⊔ b ≤ a ⊔ (↑(i { down := false : ULift Bool }) : α)
Tactic: simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
have _ : LE.le.{u} (α := α) (⨅ b ∈ s, a ⊔ b)
  (⨆ (i : ULift Bool),
    ⨅ (j :
      match (motive := ULift Bool → Type u) i with
      | { down := true } => PUnit
      | { down := false } => (↑s : Type u)),
      match (motive :=
        (i : ULift Bool) →
          (j :
              match (motive := ULift Bool → Type u) i with
              | { down := true } => PUnit
              | { down := false } => (↑s : Type u)) →
            α)
        i, j with
      | { down := true }, j => a
      | { down := false }, j => (↑j : α))
Tactic: calc
      _ ≤ ⨆ i : ULift.{u} Bool, ⨅ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by
        simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
        exact fun x ↦ biInf_le _ (x (.up false)).2
      _ = _ := by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
_ :
  LE.le.{u} (α := α) (⨅ b ∈ s, a ⊔ b)
    (⨆ (i : ULift Bool),
      ⨅ (j :
        match (motive := ULift Bool → Type u) i with
        | { down := true } => PUnit
        | { down := false } => (↑s : Type u)),
        match (motive :=
          (i : ULift Bool) →
            (j :
                match (motive := ULift Bool → Type u) i with
                | { down := true } => PUnit
                | { down := false } => (↑s : Type u)) →
              α)
          i, j with
        | { down := true }, j => a
        | { down := false }, j => (↑j : α))
⊢ ⨅ b ∈ s, a ⊔ b ≤ a ⊔ sInf s
have _₁ : (⨆ (i : ULift Bool),
    ⨅ (j :
      match (motive := ULift Bool → Type u) i with
      | { down := true } => PUnit
      | { down := false } => (↑s : Type u)),
      match (motive :=
        (i : ULift Bool) →
          (j :
              match (motive := ULift Bool → Type u) i with
              | { down := true } => PUnit
              | { down := false } => (↑s : Type u)) →
            α)
        i, j with
      | { down := true }, j => a
      | { down := false }, j => (↑j : α)) =
  a ⊔ sInf s
Tactic: calc
      _ ≤ ⨆ i : ULift.{u} Bool, ⨅ j : match i with | .up true => PUnit.{u + 1} | .up false => s,
          match i with
          | .up true => a
          | .up false => j := by
        simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]
        exact fun x ↦ biInf_le _ (x (.up false)).2
      _ = _ := by simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
hκ : Nonempty κ
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) (⋂ (j : κ), s j) i), f i)
    (⨅ (j : κ), ⨆ i ∈ s j, f i)
have rcases : ∀ (j : κ),
  Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) (⋂ (j : κ), s j) i), f i)
    (⨅ (j : κ), ⨆ i ∈ s j, f i)
Tactic: rcases hκ with ⟨j⟩
Cleared hypotheses: hκ
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) (⋂ (j : κ), s j) i), f i)
    (⨅ (j : κ), ⨆ i ∈ s j, f i)
have simp_rw : Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
  (⨆ (g : (a : κ) → ι), ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ (a : κ), f (g a))
Tactic: simp_rw [iInf_iSup_eq, mem_iInter]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
    (⨆ (g : (a : κ) → ι), ⨆ (_ : ∀ (a : κ), g a ∈ s a), ⨅ (a : κ), f (g a))
have refine : ∀ (I : (a : κ) → ι) (hI : ∀ (a : κ), I a ∈ s a),
  LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
Tactic: refine le_antisymm
    (iSup₂_le fun i hi ↦ le_iSup₂_of_le (fun _ ↦ i) hi (le_iInf fun _ ↦ le_rfl))
    (iSup₂_le fun I hI ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
⊢ LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
have pos : ∀ (H : ∀ (k : κ), I k = I j), LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
Tactic: by_cases! H : ∀ k, I k = I j
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
pos :
  ∀ (H : ∀ (k : κ), I k = I j), LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
⊢ LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
have neg : ∀ (H : ∃ (k : κ), I k ≠ I j), LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
Tactic: by_cases! H : ∀ k, I k = I j
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
I : (a : κ) → ι
hI : ∀ (a : κ), I a ∈ s a
H : ∃ (k : κ), I k ≠ I j
⊢ LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
have neg : ∀ (k : κ) (hk : I k ≠ I j), LE.le.{u} (α := α) (⨅ (a : κ), f (I a)) (⨆ (i : ι), ⨆ (_ : ∀ (i_1 : κ), i ∈ s i_1), f i)
Tactic: rcases H with ⟨k, hk⟩
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
⊢ Eq.{u + 1} (α := α_1) (⨅ (a : α), ⨆ (b : β a), g a b) (⨆ (g_1 : (a : α) → β a), ⨅ (a : α), g a (g_1 a))
have suffices : lhs ≤ rhs
Tactic: suffices lhs ≤ rhs from le_antisymm this le_iInf_iSup
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
h : ∃ (x : α_1), rhs < x ∧ x < lhs
⊢ lhs ≤ rhs
have rcases : ∀ (x : α_1) (hr : rhs < x) (hl : x < lhs), lhs ≤ rhs
Tactic: rcases h with ⟨x, hr, hl⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α_1 : Type u
β_1 : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompleteLinearOrder α_1
α : Type u
β : α → Type u
g : (a : α) → β a → α_1
lhs : α_1 := ⨅ (a : α), ⨆ (b : β a), g a b
rhs : α_1 := ⨆ (h : (a : α) → β a), ⨅ (a : α), g a (h a)
x : α_1
hr : rhs < x
hl : x < lhs
⊢ lhs ≤ rhs
have suffices : rhs ≥ x
Tactic: suffices rhs ≥ x from nomatch not_lt.2 this hr