awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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 : ι
rw 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)
                  ⋯)) :
            α))
        ⋯) ≤
    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)
                  ⋯)) :
            α))
        ⋯)
⊢ (↑(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)

Tactic:
rw [← Classical.choose_spec (g ⟨_, a, rfl⟩).2]

Premises used: Subtype.mk, Classical.choose_spec, Exists.intro, rfl, Subtype.property
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (a : ι) → κ a → α
x : CompleteLattice α := minAx.toCompleteLattice
_ :
  Eq.{u + 1} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j)
    (⨅ (a : (↑(range fun (x : ι) ↦ range (f x)) : Type u)), ⨆ (b : (↑(↑a : Set α) : Type u)), (↑b : α))
⊢ LE.le.{u} (α := α) (⨅ (i : ι), ⨆ (j : κ i), f i j) (⨆ (g : (i : ι) → κ i), ⨅ (i : ι), f i (g i))

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]

Premises used: CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq, iSup_le, Set.range
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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))

Tactic:
le_antisymm iSup_iInf_le ?_

Premises used: le_antisymm, iSup_iInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
refine : LE.le.{u} (α := α) (⨅ (g : (i : ι) → κ i), ⨆ (i : ι), f i (g i)) (⨆ (i : ι), ⨅ (j : κ i), f i j)
⊢ let x := minAx.toCompleteLattice;
  Eq.{u + 1} (α := α) (⨆ (i : ι), ⨅ (j : κ i), f i j) (⨅ (g : (i : ι) → κ i), ⨆ (i : ι), f i (g i))

Tactic:
refine le_antisymm iSup_iInf_le ?_

Premises used: le_antisymm, iSup_iInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
rw :
  LE.le.{u} (α := α) (⨆ (g : (i : (i : ι) → κ i) → ι), ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)))
    (⨆ (i : ι), ⨅ (j : κ i), f i j)
⊢ LE.le.{u} (α := α) (⨅ (g : (i : ι) → κ i), ⨆ (i : ι), f i (g i)) (⨆ (i : ι), ⨅ (j : κ i), f i j)

Tactic:
rw [minAx.iInf_iSup_eq']

Premises used: CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq'
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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)

Tactic:
iSup_le fun g => ?_

Premises used: iSup_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
refine :
  ∀ (g : (i : (i : ι) → κ i) → ι),
    LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨆ (i : ι), ⨅ (j : κ i), f i j)
⊢ LE.le.{u} (α := α) (⨆ (g : (i : (i : ι) → κ i) → ι), ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)))
    (⨆ (i : ι), ⨅ (j : κ i), f i j)

Tactic:
refine iSup_le fun g => ?_

Premises used: iSup_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
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
⊢ ∃ (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))

Tactic:
by_contra! h
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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))
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
⊢ False

Tactic:
choose h hh using h
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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))
⊢ Ne.{w'} (α := κ (g h)) (Eq.rec (motive := fun (x : ι) (h : g h = x) ↦ κ x) (h (g h)) ⋯ : κ (g h)) (h (g h) : κ (g h))

Tactic:
have := hh _ h rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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))
this :
  Ne.{w'} (α := κ (g h)) (Eq.rec (motive := fun (x : ι) (h : g h = x) ↦ κ x) (h (g h)) ⋯ : κ (g h)) (h (g h) : κ (g h))
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
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)
⊢ 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
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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)

Tactic:
le_trans ?_ (le_iSup _ a)

Premises used: le_iSup, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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))
refine : LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨅ (j : κ a), f a j)
⊢ LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨆ (i : ι), ⨅ (j : κ i), f i j)

Tactic:
refine le_trans ?_ (le_iSup _ a)

Premises used: le_iSup, le_trans
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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)

Tactic:
le_iInf fun b => ?_

Premises used: le_iInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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))
refine : ∀ (b : κ a), ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)) ≤ f a b
⊢ LE.le.{u} (α := α) (⨅ (i : (i : ι) → κ i), f (g i) (i (g i))) (⨅ (j : κ a), f a j)

Tactic:
refine le_iInf fun b => ?_

Premises used: le_iInf
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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
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))
⊢ ⨅ (i : (i : ι) → κ i), f (g i) (i (g i)) ≤ f a b

Tactic:
obtain ⟨h, rfl, rfl⟩ := ha b

Premises used: rfl
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
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:
iInf_le _ _

Premises used: iInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
f : (i : ι) → κ i → α
x : CompleteLattice α := minAx.toCompleteLattice
g : (i : (i : ι) → κ i) → ι
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:
exact iInf_le _ _

Premises used: iInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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 : α)

Tactic:
simp [sSup_eq_iSup', iSup_unique, iInf_bool_eq]

Premises used: iInf_bool_eq, iSup_unique, sSup_eq_iSup'
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
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
⊢ 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:
simp only [minAx.iInf_iSup_eq, iInf_ulift, iInf_bool_eq, iSup_le_iff]

Premises used: iInf_ulift, iInf_bool_eq, CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq, iSup_le_iff
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ ∀
    (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:
fun x ↦ le_biSup _ (x (.up false)).2

Premises used: le_biSup, ULift.up, Bool.false, Min.min, Subtype.property
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ ∀
    (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:
exact fun x ↦ le_biSup _ (x (.up false)).2

Premises used: le_biSup
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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 : α)
_₁ :
  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)
⊢ a ⊓ sSup s ≤ ⨆ 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
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
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 }) : α)
⊢ 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:
simp only [minAx.iSup_iInf_eq, iSup_ulift, iSup_bool_eq, le_iInf_iff]

Premises used: CompletelyDistribLattice.MinimalAxioms.iSup_iInf_eq, iSup_bool_eq, le_iInf_iff, iSup_ulift
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ ∀
    (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:
fun x ↦ biInf_le _ (x (.up false)).2

Premises used: Max.max, ULift.up, Bool.false, Subtype.property, biInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ ∀
    (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:
exact fun x ↦ biInf_le _ (x (.up false)).2

Premises used: biInf_le
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
minAx : MinimalAxioms α
a : α
s : Set α
x : CompleteLattice α := minAx.toCompleteLattice
⊢ (⨆ (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:
simp [sInf_eq_iInf', iInf_unique, iSup_bool_eq]

Premises used: iSup_bool_eq, sInf_eq_iInf', iInf_unique
-- Module: Mathlib.Order.CompleteBooleanAlgebra
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 : α))
_₁ :
  (⨆ (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
⊢ ⨅ b ∈ s, a ⊔ b ≤ 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]
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : CompletelyDistribLattice α
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨅ (a : ι), ⨆ (b : κ a), f a b) (⨆ (g : (a : ι) → κ a), ⨅ (a : ι), f a (g a))

Tactic:
CompletelyDistribLattice.MinimalAxioms.of.iInf_iSup_eq' _

Premises used: CompletelyDistribLattice.MinimalAxioms.of, CompletelyDistribLattice.MinimalAxioms.iInf_iSup_eq'
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst : CompletelyDistribLattice α
f : (a : ι) → κ a → α
⊢ Eq.{u + 1} (α := α) (⨆ (a : ι), ⨅ (b : κ a), f a b) (⨅ (g : (a : ι) → κ a), ⨆ (a : ι), f a (g a))

Tactic:
CompletelyDistribLattice.MinimalAxioms.of.iSup_iInf_eq _

Premises used: CompletelyDistribLattice.MinimalAxioms.iSup_iInf_eq, CompletelyDistribLattice.MinimalAxioms.of
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
hκ : Nonempty κ
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
rcases :
  ∀ (j : κ),
    Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) (⋂ (j : κ), s j) i), f i)
      (⨅ (j : κ), ⨆ i ∈ s j, f i)
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) (⋂ (j : κ), s j) i), f i)
    (⨅ (j : κ), ⨆ i ∈ s j, f i)

Tactic:
rcases hκ with ⟨j⟩
-- Module: Mathlib.Order.CompleteBooleanAlgebra
Goal:
α : Type u
inst : CompletelyDistribLattice α
ι : Type u_1
κ : Type u_2
f : ι → α
h : Pairwise (Disjoint on f)
s : κ → Set ι
j : κ
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))
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (_ : Membership.mem (γ := Set ι) (⋂ (j : κ), s j) i), f i)
    (⨅ (j : κ), ⨆ i ∈ s j, f i)

Tactic:
simp_rw [iInf_iSup_eq, mem_iInter]

Premises used: iInf_iSup_eq, Set.mem_iInter