awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (hypothesis)
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
⊢ rhs ≥ x
have this : ∀ (a : α), ∃ (b : β a), x < g a b
Tactic: have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) 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
this : ∀ (a : α), ∃ (b : β a), x < g a b
⊢ rhs ≥ x
have choose : ∀ (f : (a : α) → β a) (hf : ∀ (a : α), x < g a (f a)), rhs ≥ x
Tactic: choose f hf using this
Cleared hypotheses: this
-- 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
f : (a : α) → β a
hf : ∀ (a : α), x < g a (f a)
⊢ rhs ≥ x
have refine : x ≤ ⨅ (a : α), g a (f a)
Tactic: refine le_trans ?_ (le_iSup _ f)
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (hypothesis)
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 hrl : rhs < lhs
Tactic: refine le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (hypothesis)
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
hrl : rhs < lhs
⊢ lhs ≤ rhs
have h₁ : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
Tactic: replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (hypothesis)
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)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
⊢ lhs ≤ rhs
have this : ∀ (a : α), ∃ (b : β a), rhs < g a b
Tactic: have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
-- 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)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
this : ∀ (a : α), ∃ (b : β a), rhs < g a b
⊢ lhs ≤ rhs
have choose : ∀ (f : (a : α) → β a) (hf : ∀ (a : α), rhs < g a (f a)), lhs ≤ rhs
Tactic: choose f hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (hypothesis)
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)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
⊢ lhs ≤ rhs
have this : ∀ (a : α), lhs ≤ g a (f a)
Tactic: have : ∀ a, lhs ≤ g a (f a) := fun a =>
        (h (g a (f a))).resolve_left (by simpa using hf a)
-- 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)
hrl : rhs < lhs
h : ∀ (x : α_1), x ≤ rhs ∨ lhs ≤ x
f : (a : α) → β a
hf : ∀ (a : α), rhs < g a (f a)
this : ∀ (a : α), lhs ≤ g a (f a)
⊢ lhs ≤ rhs
have refine : lhs ≤ ⨅ (a : α), g a (f a)
Tactic: refine le_trans ?_ (le_iSup _ f)
-- 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)
⊢ lhs ≤ rhs
have if : ∀ (h : ∃ (x : α_1), rhs < x ∧ x < lhs), lhs ≤ rhs
Tactic: if h : ∃ x, rhs < x ∧ x < lhs then
      rcases h with ⟨x, hr, hl⟩
      suffices rhs ≥ x from nomatch not_lt.2 this hr
      have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
      choose f hf using this
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => le_of_lt (hf a)
    else
      refine le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_
      replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h
      have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
      choose f hf using this
      have : ∀ a, lhs ≤ g a (f a) := fun a =>
        (h (g a (f a))).resolve_left (by simpa using hf a)
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => this _
-- 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)
if : ∀ (h : ∃ (x : α_1), rhs < x ∧ x < lhs), lhs ≤ rhs
⊢ lhs ≤ rhs
have if₁ : ∀ (h : ¬∃ (x : α_1), rhs < x ∧ x < lhs), lhs ≤ rhs
Tactic: if h : ∃ x, rhs < x ∧ x < lhs then
      rcases h with ⟨x, hr, hl⟩
      suffices rhs ≥ x from nomatch not_lt.2 this hr
      have : ∀ a, ∃ b, x < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_not_ge fun h =>
            lt_irrefl x (lt_of_lt_of_le hl (le_trans (iInf_le _ a) h))
      choose f hf using this
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => le_of_lt (hf a)
    else
      refine le_of_not_gt fun hrl : rhs < lhs => not_le_of_gt hrl ?_
      replace h : ∀ x, x ≤ rhs ∨ lhs ≤ x := by
        simpa only [not_exists, not_and_or, not_or, not_lt] using h
      have : ∀ a, ∃ b, rhs < g a b := fun a =>
        lt_iSup_iff.1 <| lt_of_lt_of_le hrl (iInf_le _ a)
      choose f hf using this
      have : ∀ a, lhs ≤ g a (f a) := fun a =>
        (h (g a (f a))).resolve_left (by simpa using hf a)
      refine le_trans ?_ (le_iSup _ f)
      exact le_iInf fun a => this _
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
inst : Frame α
f : ι → α
a : α
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
Tactic: rw [iSup, sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
inst : Frame α
f : ι → α
a : α
rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw₁ : Eq.{u + 1} (α := α) (⨆ (a_1 : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) a_1), a_1 ⊓ a)
  (⨆ (i : ι), f i ⊓ a)
Tactic: rw [iSup, sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
inst : Frame α
f : ι → α
a : α
rw : sSup (range fun (i : ι) ↦ f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
rw₁ :
  Eq.{u + 1} (α := α) (⨆ (a_1 : α), ⨆ (_ : Membership.mem (γ := Set α) (range fun (i : ι) ↦ f i) a_1), a_1 ⊓ a)
    (⨆ (i : ι), f i ⊓ a)
⊢ (⨆ (i : ι), f i) ⊓ a = ⨆ (i : ι), f i ⊓ a
have rw₂ : Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ a) (⨆ (i : ι), f i ⊓ a)
Tactic: rw [iSup, sSup_inf_eq, iSup_range]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
⊢ Eq.{u + 1} (α := α) ((⨆ (i : ι), f i) ⊓ ⨆ (j : ι'), g j) (⨆ (i : ι × ι'), f i.1 ⊓ g i.2)
have simp_rw : Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ ⨆ (j : ι'), g j) (⨆ (i : ι × ι'), f i.1 ⊓ g i.2)
Tactic: simp_rw [iSup_inf_eq, inf_iSup_eq, iSup_prod]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
simp_rw : Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ ⨆ (j : ι'), g j) (⨆ (i : ι × ι'), f i.1 ⊓ g i.2)
⊢ Eq.{u + 1} (α := α) ((⨆ (i : ι), f i) ⊓ ⨆ (j : ι'), g j) (⨆ (i : ι × ι'), f i.1 ⊓ g i.2)
have simp_rw₁ : Eq.{u + 1} (α := α) (⨆ (i : ι), ⨆ (i_1 : ι'), f i ⊓ g i_1) (⨆ (i : ι × ι'), f i.1 ⊓ g i.2)
Tactic: simp_rw [iSup_inf_eq, inf_iSup_eq, iSup_prod]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
ι' : Type u_2
f : ι → α
g : ι' → α
s : Set ι
t : Set ι'
⊢ Eq.{u + 1} (α := α) ((⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j) (⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2)
have simp : Eq.{u + 1} (α := α)
  (⨆ (i : Prod.{u_1, u_2} (Subtype (Membership.mem s)) (Subtype (Membership.mem t))), f (↑i.1 : ι) ⊓ g (↑i.2 : ι'))
  (⨆ (x : Subtype (Membership.mem (s ×ˢ t))), f (↑x : ι × ι').1 ⊓ g (↑x : ι × ι').2)
Tactic: simp only [iSup_subtype', iSup_inf_iSup]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
⊢ Eq.{u + 1} (α := α) (⨆ i ∈ s ∩ t, f i) ((⨆ i ∈ s, f i) ⊓ ⨆ i ∈ t, f i)
have rw : Eq.{u + 1} (α := α) (⨆ i ∈ s ∩ t, f i) (⨆ p ∈ s ×ˢ t, f p.1 ⊓ f p.2)
Tactic: rw [biSup_inf_biSup]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
⊢ Eq.{u + 1} (α := α) (⨆ i ∈ s ∩ t, f i) (⨆ p ∈ s ×ˢ t, f p.1 ⊓ f p.2)
have refine : ∀ (x : ι × ι) (i j : ι),
  (i, j) ∈ s ×ˢ t → ∀ (his : (i, j).1 ∈ s) (hjs : (i, j).2 ∈ t), f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
Tactic: refine le_antisymm
    (iSup₂_le fun i ⟨his, hit⟩ ↦ le_iSup₂_of_le ⟨i, i⟩ ⟨his, hit⟩ (le_inf le_rfl le_rfl))
    (iSup₂_le fun ⟨i, j⟩ ⟨his, hjs⟩ ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x : ι × ι
i j : ι
h_1 : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
have pos : ∀ (hij : i = j), f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
f : ι → α
h : Pairwise (Disjoint on f)
s t : Set ι
x : ι × ι
i j : ι
h_1 : (i, j) ∈ s ×ˢ t
his : (i, j).1 ∈ s
hjs : (i, j).2 ∈ t
pos : ∀ (hij : i = j), f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
⊢ f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
have neg : ∀ (hij : ¬i = j), f (i, j).1 ⊓ f (i, j).2 ≤ ⨆ i ∈ s ∩ t, f i
Tactic: by_cases hij : i = j
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ Eq.{u + 1} (α := α) (⨆ (i : ι), f i ⊓ g i) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i)
have refine : LE.le.{u} (α := α) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i) (⨆ (i : ι), f i ⊓ g i)
Tactic: refine (le_iSup_inf_iSup f g).antisymm ?_
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ LE.le.{u} (α := α) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i) (⨆ (i : ι), f i ⊓ g i)
have rw : LE.le.{u} (α := α) (⨆ (i : ι × ι), f i.1 ⊓ g i.2) (⨆ (i : ι), f i ⊓ g i)
Tactic: rw [iSup_inf_iSup]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
⊢ LE.le.{u} (α := α) (⨆ (i : ι × ι), f i.1 ⊓ g i.2) (⨆ (i : ι), f i ⊓ g i)
have refine : ∀ (i : ι × ι), ∃ (i' : ι), f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'
Tactic: refine iSup_mono' fun i => ?_
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : Frame α
ι : Type u_1
inst_1 : Preorder ι
inst_2 : IsDirectedOrder ι
f g : ι → α
hf : Monotone f
hg : Monotone g
i : ι × ι
⊢ ∃ (i' : ι), f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'
have rcases : ∀ (j : ι) (h₁ : i.1 ≤ j) (h₂ : i.2 ≤ j), ∃ (i' : ι), f i.1 ⊓ g i.2 ≤ f i' ⊓ g i'
Tactic: rcases directed_of (· ≤ ·) i.1 i.2 with ⟨j, h₁, h₂⟩
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Frame α
s t : Set α
a_1 b_1 c_1 d a b c : α
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
have rw : a ⊓ sSup {b, c} ≤ a ⊓ b ⊔ a ⊓ c
Tactic: rw [← sSup_pair, ← sSup_pair, inf_sSup_eq, ← sSup_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Frame α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : a ⊓ sSup {b, c} ≤ a ⊓ b ⊔ a ⊓ c
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
have rw₁ : a ⊓ sSup {b, c} ≤ sSup {a ⊓ b, a ⊓ c}
Tactic: rw [← sSup_pair, ← sSup_pair, inf_sSup_eq, ← sSup_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Frame α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : a ⊓ sSup {b, c} ≤ a ⊓ b ⊔ a ⊓ c
rw₁ : a ⊓ sSup {b, c} ≤ sSup {a ⊓ b, a ⊓ c}
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
have rw₂ : LE.le (α := α) (⨆ (b_2 : α), ⨆ (_ : Membership.mem (γ := Set α) {b, c} b_2), a ⊓ b_2) (sSup {a ⊓ b, a ⊓ c})
Tactic: rw [← sSup_pair, ← sSup_pair, inf_sSup_eq, ← sSup_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Frame α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : a ⊓ sSup {b, c} ≤ a ⊓ b ⊔ a ⊓ c
rw₁ : a ⊓ sSup {b, c} ≤ sSup {a ⊓ b, a ⊓ c}
rw₂ : LE.le (α := α) (⨆ (b_2 : α), ⨆ (_ : Membership.mem (γ := Set α) {b, c} b_2), a ⊓ b_2) (sSup {a ⊓ b, a ⊓ c})
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
have rw₃ : sSup (min a '' {b, c}) ≤ sSup {a ⊓ b, a ⊓ c}
Tactic: rw [← sSup_pair, ← sSup_pair, inf_sSup_eq, ← sSup_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Frame α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : a ⊓ sSup {b, c} ≤ a ⊓ b ⊔ a ⊓ c
rw₁ : a ⊓ sSup {b, c} ≤ sSup {a ⊓ b, a ⊓ c}
rw₂ : LE.le (α := α) (⨆ (b_2 : α), ⨆ (_ : Membership.mem (γ := Set α) {b, c} b_2), a ⊓ b_2) (sSup {a ⊓ b, a ⊓ c})
rw₃ : sSup (min a '' {b, c}) ≤ sSup {a ⊓ b, a ⊓ c}
⊢ a ⊓ (b ⊔ c) ≤ a ⊓ b ⊔ a ⊓ c
have rw₄ : LE.le (α := α) (sSup {a ⊓ b, a ⊓ c}) (sSup {a ⊓ b, a ⊓ c})
Tactic: rw [← sSup_pair, ← sSup_pair, inf_sSup_eq, ← sSup_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Coframe α
s t : Set α
a_1 b_1 c_1 d a b c : α
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have rw : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ b ⊓ c
Tactic: rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Coframe α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ b ⊓ c
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have rw₁ : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ sInf {b, c}
Tactic: rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Coframe α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ b ⊓ c
rw₁ : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ sInf {b, c}
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have rw₂ : LE.le (α := α) (sInf {a ⊔ b, a ⊔ c}) (⨅ (b_2 : α), ⨅ (_ : Membership.mem (γ := Set α) {b, c} b_2), a ⊔ b_2)
Tactic: rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Coframe α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ b ⊓ c
rw₁ : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ sInf {b, c}
rw₂ : LE.le (α := α) (sInf {a ⊔ b, a ⊔ c}) (⨅ (b_2 : α), ⨅ (_ : Membership.mem (γ := Set α) {b, c} b_2), a ⊔ b_2)
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have rw₃ : sInf {a ⊔ b, a ⊔ c} ≤ sInf (max a '' {b, c})
Tactic: rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Coframe α
s t : Set α
a_1 b_1 c_1 d a b c : α
rw : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ b ⊓ c
rw₁ : sInf {a ⊔ b, a ⊔ c} ≤ a ⊔ sInf {b, c}
rw₂ : LE.le (α := α) (sInf {a ⊔ b, a ⊔ c}) (⨅ (b_2 : α), ⨅ (_ : Membership.mem (γ := Set α) {b, c} b_2), a ⊔ b_2)
rw₃ : sInf {a ⊔ b, a ⊔ c} ≤ sInf (max a '' {b, c})
⊢ (a ⊔ b) ⊓ (a ⊔ c) ≤ a ⊔ b ⊓ c
have rw₄ : LE.le (α := α) (sInf {a ⊔ b, a ⊔ c}) (sInf {a ⊔ b, a ⊔ c})
Tactic: rw [← sInf_pair, ← sInf_pair, sup_sInf_eq, ← sInf_image, image_pair]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompletelyDistribLattice α
inst_1 : CompletelyDistribLattice β
ι_1 : Type (max u v)
κ_1 : ι_1 → Type (max u v)
f : (a : ι_1) → κ_1 a → α × β
⊢ Eq (α := α × β) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b) (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a))
have fst : Eq.{u + 1} (α := α) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b).1 (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a)).1
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : CompletelyDistribLattice α
inst_1 : CompletelyDistribLattice β
ι_1 : Type (max u v)
κ_1 : ι_1 → Type (max u v)
f : (a : ι_1) → κ_1 a → α × β
fst : Eq.{u + 1} (α := α) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b).1 (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a)).1
⊢ Eq (α := α × β) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b) (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a))
have snd : Eq.{v + 1} (α := β) (⨅ (a : ι_1), ⨆ (b : κ_1 a), f a b).2 (⨆ (g : (a : ι_1) → κ_1 a), ⨅ (a : ι_1), f a (g a)).2
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι_1 : Sort w
κ : ι_1 → Sort w'
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → CompletelyDistribLattice (π i)
ι_2 : Type (max u_1 u_2)
κ_1 : ι_2 → Type (max u_1 u_2)
f : (a : ι_2) → κ_1 a → (i : ι) → π i
⊢ Eq (α := (i : ι) → π i) (⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) (⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a))
have h : ∀ (i : ι),
  Eq.{u_2 + 1} (α := π i) ((⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) i)
    ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
ι : Sort w
inst : CompleteBooleanAlgebra α
f g : ι → α
⊢ LE.le.{u} (α := α) ((⨆ (i : ι), f i) ∆ ⨆ (i : ι), g i) (⨆ (i : ι), f i ∆ g i)
have simp_rw : LE.le.{u} (α := α) (⨆ (i : ι), f i) (⨆ (x : ι), g x ⊔ f x ∆ g x) ∧
  LE.le.{u} (α := α) (⨆ (i : ι), g i) (⨆ (x : ι), f x ⊔ f x ∆ g x)
Tactic: simp_rw [symmDiff_le_iff, ← iSup_sup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ sSup s ∆ a ≤ sSup ((fun (x : α) ↦ x ∆ a) '' s)
have rw : (⨆ (a : (↑s : Type u)), (↑a : α)) ∆ a ≤ ⨆ (a_1 : (↑s : Type u)), (↑a_1 : α) ∆ a
Tactic: rw [sSup_image', sSup_eq_iSup']
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (hypothesis)
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s : Set α
hs : s.Nonempty
a : α
⊢ (⨆ (a : (↑s : Type u)), (↑a : α)) ∆ a ≤ ⨆ (a_1 : (↑s : Type u)), (↑a_1 : α) ∆ a
have this : Nonempty.{u + 1} (↑s : Type u)
Tactic: have : Nonempty s := Set.nonempty_coe_sort.mpr hs
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ sSup (image2 (fun (x1 x2 : α) ↦ x1 ∆ x2) s t)
have rw : sSup s ∆ sSup t ≤ ⨆ a ∈ s, ⨆ b ∈ t, a ∆ b
Tactic: rw [sSup_image2]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
inst : CompleteBooleanAlgebra α
s t : Set α
hs : s.Nonempty
ht : t.Nonempty
⊢ sSup s ∆ sSup t ≤ ⨆ a ∈ s, ⨆ b ∈ t, a ∆ b
have _ : sSup s ∆ sSup t ≤ ⨆ a ∈ s, a ∆ sSup t
Tactic: calc
  _ ≤ ⨆ a ∈ s, a ∆ sSup t := by simpa [sSup_image] using sSup_symmDiff_le hs
  _ ≤ _ := iSup_mono fun a ↦ iSup_mono fun _ ↦ by simpa [sSup_image] using symmDiff_sSup_le ht
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι_1 : Sort w
κ : ι_1 → Sort w'
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι_2 : Type (max u_1 u_2)
κ_1 : ι_2 → Type (max u_1 u_2)
f : (a : ι_2) → κ_1 a → (i : ι) → π i
⊢ Eq (α := (i : ι) → π i) (⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) (⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a))
have h : ∀ (x : ι),
  Eq.{u_2 + 1} (α := π x) ((⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) x)
    ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι_1 : Sort w
κ : ι_1 → Sort w'
ι : Type u_1
π : ι → Type u_2
inst : (i : ι) → CompleteAtomicBooleanAlgebra (π i)
ι_2 : Type (max u_1 u_2)
κ_1 : ι_2 → Type (max u_1 u_2)
f : (a : ι_2) → κ_1 a → (i : ι) → π i
x : ι
⊢ Eq.{u_2 + 1} (α := π x) ((⨅ (a : ι_2), ⨆ (b : κ_1 a), f a b) x)
    ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) x)
have h : Eq.{u_2 + 1} (α := π x) ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) x)
  ((⨆ (g : (a : ι_2) → κ_1 a), ⨅ (a : ι_2), f a (g a)) x)
Tactic: rw [iInf_iSup_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Frame.MinimalAxioms β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
⊢ a ⊓ sSup s ≤ ⨆ b ∈ s, a ⊓ b
have rw : ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))
Tactic: rw [← le, ← sSup_image, map_inf, map_sSup s, minAx.inf_iSup₂_eq]
-- Lean 4 proof step from Mathlib.Order.CompleteBooleanAlgebra (goal)
Goal:
α : Type u
β : Type v
ι : Sort w
κ : ι → Sort w'
inst : Max α
inst_1 : Min α
inst_2 : LE α
inst_3 : LT α
inst_4 : SupSet α
inst_5 : InfSet α
inst_6 : Top α
inst_7 : Bot α
minAx : Frame.MinimalAxioms β
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
map_sSup : ∀ (s : Set α), f (sSup s) = ⨆ a ∈ s, f a
map_sInf : ∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a
map_top : f ⊤ = ⊤
map_bot : f ⊥ = ⊥
a : α
s : Set α
⊢ ⨆ i ∈ s, f a ⊓ f i ≤ f (sSup (min a '' s))
have simp_rw : ⨆ i ∈ s, f (a ⊓ i) ≤ f (sSup (min a '' s))
Tactic: simp_rw [← map_inf]