awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLinearOrder α
f : ι → α
rw : ⊤ ≤ iSup f ↔ ∀ b < ⊤, ∃ (i : ι), b < f i
rw₁ rw₂ : (∀ b < ⊤, ∃ (i : ι), b < f i) ↔ ∀ b < ⊤, ∃ (i : ι), b < f i
⊢ iSup f = ⊤ ↔ ∀ b < ⊤, ∃ (i : ι), b < f i

Tactic:
rw [eq_top_iff, le_iSup_iff_forall_lt]

Premises used: le_iSup_iff_forall_lt, eq_top_iff
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLinearOrder α
a : α
s : Set β
f : β → α
⊢ a < ⨆ i ∈ s, f i ↔ ∃ i ∈ s, a < f i

Tactic:
simp [lt_iSup_iff]

Premises used: lt_iSup_iff
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : SupSet β
s : Set α
⊢ sSup s = (e.symm : (a : β) → α) (⨆ a ∈ s, (e : (a : α) → β) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : InfSet β
s : Set α
⊢ sInf s = (e.symm : (a : β) → α) (⨅ a ∈ s, (e : (a : α) → β) a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : ι → α
⊢ ⨆ (i : ι), u i * v i ≤ HMul.hMul (α := α) (⨆ (i : ι), u i) (⨆ (i : ι), v i)

Tactic:
iSup_le fun _ ↦ mul_le_mul' (le_iSup ..) (le_iSup ..)

Premises used: le_iSup, iSup_le, mul_le_mul'
-- Module: Mathlib.Order.CompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : ι → α
⊢ HMul.hMul (α := α) (⨅ (i : ι), u i) (⨅ (i : ι), v i) ≤ ⨅ (i : ι), u i * v i

Tactic:
iSup_mul_le (α := αᵒᵈ) ..

Premises used: iInf, OrderDual, iSup_mul_le
-- Module: Mathlib.Order.CompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : (i : ι) → κ i → α
⊢ ⨆ (i : ι), ⨆ (j : κ i), u i j * v i j ≤
    HMul.hMul (α := α) (⨆ (i : ι), ⨆ (j : κ i), u i j) (⨆ (i : ι), ⨆ (j : κ i), v i j)

Tactic:
le_trans ?_ (iSup_mul_le ..)

Premises used: iSup_mul_le, le_trans
-- Module: Mathlib.Order.CompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : (i : ι) → κ i → α
refine :
  LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), u i j * v i j)
    (⨆ (i : ι), HMul.hMul (α := α) (⨆ (j : κ i), u i j) (⨆ (j : κ i), v i j))
⊢ ⨆ (i : ι), ⨆ (j : κ i), u i j * v i j ≤
    HMul.hMul (α := α) (⨆ (i : ι), ⨆ (j : κ i), u i j) (⨆ (i : ι), ⨆ (j : κ i), v i j)

Tactic:
refine le_trans ?_ (iSup_mul_le ..)

Premises used: iSup_mul_le, le_trans
-- Module: Mathlib.Order.CompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : (i : ι) → κ i → α
h : ∀ (i : ι), ⨆ (j : κ i), u i j * v i j ≤ HMul.hMul (α := α) (⨆ (j : κ i), u i j) (⨆ (j : κ i), v i j)
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), ⨆ (j : κ i), u i j * v i j)
    (⨆ (i : ι), HMul.hMul (α := α) (⨆ (j : κ i), u i j) (⨆ (j : κ i), v i j))

Tactic:
gcongr
-- Module: Mathlib.Order.CompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : (i : ι) → κ i → α
i : ι
⊢ ⨆ (j : κ i), u i j * v i j ≤ HMul.hMul (α := α) (⨆ (j : κ i), u i j) (⨆ (j : κ i), v i j)

Tactic:
iSup_mul_le ..

Premises used: iSup_mul_le
-- Module: Mathlib.Order.CompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : (i : ι) → κ i → α
i : ι
⊢ ⨆ (j : κ i), u i j * v i j ≤ HMul.hMul (α := α) (⨆ (j : κ i), u i j) (⨆ (j : κ i), v i j)

Tactic:
exact iSup_mul_le ..

Premises used: iSup_mul_le
-- Module: Mathlib.Order.CompleteLattice.Group
Goal:
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst : CompleteLattice α
inst_1 : Mul α
inst_2 : MulLeftMono α
inst_3 : MulRightMono α
u v : (i : ι) → κ i → α
⊢ HMul.hMul (α := α) (⨅ (i : ι), ⨅ (j : κ i), u i j) (⨅ (i : ι), ⨅ (j : κ i), v i j) ≤
    ⨅ (i : ι), ⨅ (j : κ i), u i j * v i j

Tactic:
iSup₂_mul_le (α := αᵒᵈ) ..

Premises used: iInf, OrderDual, iSup₂_mul_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : Bool → α
rw : sSup (range fun (b : Bool) ↦ f b) = f true ⊔ f false
rw₁ : sSup {f false, f true} = f true ⊔ f false
rw₂ : f false ⊔ f true = f true ⊔ f false
rw₃ rw₄ : f true ⊔ f false = f true ⊔ f false
⊢ ⨆ (b : Bool), f b = f true ⊔ f false

Tactic:
rw [iSup, Bool.range_eq, sSup_pair, sup_comm]

Premises used: iSup, Bool.range_eq, sup_comm, sSup_pair
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : Bool → α
⊢ ⨅ (b : Bool), f b = f true ⊓ f false

Tactic:
@iSup_bool_eq αᵒᵈ _ _

Premises used: iSup_bool_eq, iInf, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
x y : α
rw : x ⊔ y = (bif true then x else y) ⊔ bif false then x else y
rw₁ : x ⊔ y = x ⊔ bif false then x else y
rw₂ rw₃ : x ⊔ y = x ⊔ y
⊢ x ⊔ y = ⨆ (b : Bool), bif b then x else y

Tactic:
rw [iSup_bool_eq, Bool.cond_true, Bool.cond_false]

Premises used: iSup_bool_eq, Bool.cond_true, Bool.cond_false
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
x y : α
⊢ x ⊓ y = ⨅ (b : Bool), bif b then x else y

Tactic:
@sup_eq_iSup αᵒᵈ _ _ _

Premises used: iInf, sup_eq_iSup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
a : LE.le.{u_1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i) (⨆ (i : ℕ), u (i + n))
a₁ : LE.le.{u_1} (α := α) (⨆ (i : ℕ), u (i + n)) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i) (⨆ (i : ℕ), u (i + n))

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
a : ∀ (i : ℕ) (i_1 : i ≥ n), u i ≤ ⨆ (i : ℕ), u (i + n)
⊢ LE.le.{u_1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i) (⨆ (i : ℕ), u (i + n))

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
a : ∀ (i : ℕ), u (i + n) ≤ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i
⊢ LE.le.{u_1} (α := α) (⨆ (i : ℕ), u (i + n)) (⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i)

Tactic:
simp only [iSup_le_iff]

Premises used: iSup_le_iff
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ) (i_1 : i ≥ n), u i ≤ ⨆ (i : ℕ), u (i + n)

Tactic:
fun i hi => le_sSup ⟨i - n, ?_⟩

Premises used: iSup, HSub.hSub, Exists.intro, le_sSup
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
a : ∀ (i : ℕ) (hi : i ≥ n), (fun (i : ℕ) ↦ u (i + n)) (i - n) = u i
⊢ ∀ (i : ℕ) (i_1 : i ≥ n), u i ≤ ⨆ (i : ℕ), u (i + n)

Tactic:
refine fun i hi => le_sSup ⟨i - n, ?_⟩
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
a : u (i - n + n) = u i
⊢ (fun (i : ℕ) ↦ u (i + n)) (i - n) = u i

Tactic:
dsimp only
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n i : ℕ
hi : i ≥ n
a a₁ : u i = u i
⊢ u (i - n + n) = u i

Tactic:
rw [Nat.sub_add_cancel hi]

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i

Tactic:
fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩

Premises used: iSup, Nat.le_add_left, iSup_pos, HAdd.hAdd, Exists.intro, le_sSup
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ ∀ (i : ℕ), u (i + n) ≤ ⨆ (i : ℕ), ⨆ (_ : i ≥ n), u i

Tactic:
exact fun i => le_sSup ⟨i + n, iSup_pos (Nat.le_add_left _ _)⟩
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
n : ℕ
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨅ (_ : i ≥ n), u i) (⨅ (i : ℕ), u (i + n))

Tactic:
@iSup_ge_eq_iSup_nat_add αᵒᵈ _ _ _

Premises used: iInf, OrderDual, iSup_ge_eq_iSup_nat_add
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
hf : Monotone f
k : ℕ
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), f (n + k)) (⨆ (n : ℕ), f n)

Tactic:
le_antisymm (iSup_le fun i => le_iSup _ (i + k)) <| iSup_mono fun i => hf <| Nat.le_add_right i k

Premises used: Nat.le_add_right, le_iSup, le_antisymm, HAdd.hAdd, iSup_le, iSup_mono
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
hf : Antitone f
k : ℕ
⊢ Eq.{u_1 + 1} (α := α) (⨅ (n : ℕ), f (n + k)) (⨅ (n : ℕ), f n)

Tactic:
hf.dual_right.iSup_nat_add k

Premises used: iInf, Antitone.dual_right, OrderDual, Monotone.iSup_nat_add
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
k : ℕ
⊢ Monotone.{0, u_1} (β := α) fun (n : ℕ) ↦ ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i

Tactic:
have hf : Monotone fun n => ⨅ i ≥ n, f i := fun n m h => biInf_mono fun i => h.trans
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone.{0, u_1} (β := α) fun (n : ℕ) ↦ ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i
rw :
  Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f (i + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n + k), f i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f (i + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i)

Tactic:
rw [← Monotone.iSup_nat_add hf k]

Premises used: Monotone.iSup_nat_add
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
k : ℕ
hf : Monotone.{0, u_1} (β := α) fun (n : ℕ) ↦ ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f i
simp_rw : Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), f (i + n + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), f (i + (n + k)))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n), f (i + k)) (⨆ (n : ℕ), ⨅ (i : ℕ), ⨅ (_ : i ≥ n + k), f i)

Tactic:
simp_rw [iInf_ge_eq_iInf_nat_add, ← Nat.add_assoc]

Premises used: Nat.add_assoc, iInf_ge_eq_iInf_nat_add
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ ∀ (f : ℕ → α) (k : ℕ),
    Eq.{u_1 + 1} (α := α) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f (i + k)) (⨅ (n : ℕ), ⨆ (i : ℕ), ⨆ (_ : i ≥ n), f i)

Tactic:
@iSup_iInf_ge_nat_add αᵒᵈ _

Premises used: iInf, iSup, OrderDual, iSup_iInf_ge_nat_add
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
rw :
  u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) {0} x), u x) ⊔ ⨆ x ∈ range Nat.succ, u x
rw₁ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ x ∈ range Nat.succ, u x
rw₂ rw₃ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ (i : ℕ), u i.succ
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x

Tactic:
rw [iSup_union, iSup_singleton, iSup_range]

Premises used: iSup_range, iSup_singleton, iSup_union
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
rw :
  u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) {0} x), u x) ⊔ ⨆ x ∈ range Nat.succ, u x
rw₁ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ x ∈ range Nat.succ, u x
rw₂ rw₃ : u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = u 0 ⊔ ⨆ (i : ℕ), u i.succ
⊢ u 0 ⊔ ⨆ (i : ℕ), u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x

Tactic:
{ rw [iSup_union, iSup_singleton, iSup_range] }

Premises used: iSup_range, iSup_singleton, iSup_union
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
rw : Eq.{u_1 + 1} (α := α) (⨆ (x : ℕ), ⨆ (_ : Membership.mem (γ := Set ℕ) univ x), u x) (⨆ (i : ℕ), u i)
rw₁ rw₂ : Eq.{u_1 + 1} (α := α) (⨆ (x : ℕ), u x) (⨆ (i : ℕ), u i)
⊢ Eq.{u_1 + 1} (α := α) (⨆ x ∈ {0} ∪ range Nat.succ, u x) (⨆ (i : ℕ), u i)

Tactic:
rw [Nat.zero_union_range_succ, iSup_univ]

Premises used: Nat.zero_union_range_succ, iSup_univ
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊓ ⨅ (i : ℕ), u (i + 1) = ⨅ (i : ℕ), u i

Tactic:
@sup_iSup_nat_succ αᵒᵈ _ u

Premises used: iInf, sup_iSup_nat_succ, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
rw :
  Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨅ (_ : i > 0), f i)
    (⨅ (b : ℕ), ⨅ (_ : Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} b), f b)
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨅ (_ : i > 0), f i) (⨅ (i : ℕ), f (i + 1))

Tactic:
rw [← iInf_range, Nat.range_succ]

Premises used: Nat.range_succ, iInf_range
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
⊢ Eq.{u_1 + 1} (α := α) (⨅ (i : ℕ), ⨅ (_ : i > 0), f i)
    (⨅ (b : ℕ), ⨅ (_ : Membership.mem (γ := Set ℕ) {i : ℕ | 0 < i} b), f b)

Tactic:
simp
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
f : ℕ → α
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), ⨆ (_ : i > 0), f i) (⨆ (i : ℕ), f (i + 1))

Tactic:
@iInf_nat_gt_zero_eq αᵒᵈ _ f

Premises used: iSup, iInf_nat_gt_zero_eq, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
a : α
s : Set α
⊢ a ⊔ sInf s ≤ ⨅ b ∈ s, a ⊔ b

Tactic:
le_iInf₂ fun _ h => sup_le_sup_left (sInf_le h) _

Premises used: sup_le_sup_left, le_iInf₂, sInf_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
a : α
s : Set α
⊢ ⨆ b ∈ s, a ⊓ b ≤ a ⊓ sSup s

Tactic:
@sup_sInf_le_iInf_sup αᵒᵈ _ _ _

Premises used: Set.Mem, iSup, sup_sInf_le_iInf_sup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
a : α
s : Set α
⊢ sInf s ⊔ a ≤ ⨅ b ∈ s, b ⊔ a

Tactic:
le_iInf₂ fun _ h => sup_le_sup_right (sInf_le h) _

Premises used: sup_le_sup_right, le_iInf₂, sInf_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
a : α
s : Set α
⊢ ⨆ b ∈ s, b ⊓ a ≤ sSup s ⊓ a

Tactic:
@sInf_sup_le_iInf_sup αᵒᵈ _ _ _

Premises used: sInf_sup_le_iInf_sup, Set.Mem, iSup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
a : α
⊢ (⨅ (i : ι), f i) ⊔ a ≤ ⨅ (i : ι), f i ⊔ a

Tactic:
le_iInf fun i ↦ sup_le_sup_right (iInf_le f i) a

Premises used: sup_le_sup_right, le_iInf, iInf_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
a : α
⊢ a ⊔ ⨅ (i : ι), f i ≤ ⨅ (i : ι), a ⊔ f i

Tactic:
le_iInf fun i ↦ sup_le_sup_left (iInf_le f i) a

Premises used: sup_le_sup_left, le_iInf, iInf_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
a : α
⊢ ⨆ (i : ι), f i ⊓ a ≤ (⨆ (i : ι), f i) ⊓ a

Tactic:
@iInf_sup_le_iInf_sup αᵒᵈ ι _ f a

Premises used: iSup, iInf_sup_le_iInf_sup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f : ι → α
a : α
⊢ ⨆ (i : ι), a ⊓ f i ≤ a ⊓ ⨆ (i : ι), f i

Tactic:
@sup_iInf_le_iInf_sup αᵒᵈ ι _ f a

Premises used: iSup, sup_iInf_le_iInf_sup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s : Set β
a : α
⊢ (⨅ i ∈ s, f i) ⊔ a ≤ ⨅ i ∈ s, f i ⊔ a

Tactic:
le_iInf₂ fun _ hi ↦ sup_le_sup_right (biInf_le f hi) a

Premises used: sup_le_sup_right, le_iInf₂, biInf_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s : Set β
a : α
⊢ a ⊔ ⨅ i ∈ s, f i ≤ ⨅ i ∈ s, a ⊔ f i

Tactic:
le_iInf₂ fun _ hi ↦ sup_le_sup_left (biInf_le f hi) a

Premises used: sup_le_sup_left, le_iInf₂, biInf_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s : Set β
a : α
⊢ ⨆ i ∈ s, f i ⊓ a ≤ (⨆ i ∈ s, f i) ⊓ a

Tactic:
@biInf_sup_le_biInf_sup αᵒᵈ β _ f s a

Premises used: iSup, biInf_sup_le_biInf_sup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
f : β → α
s : Set β
a : α
⊢ ⨆ i ∈ s, a ⊓ f i ≤ a ⊓ ⨆ i ∈ s, f i

Tactic:
@sup_biInf_le_biInf_sup αᵒᵈ β _ f s a

Premises used: sup_biInf_le_biInf_sup, iSup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f g : ι → α
⊢ LE.le.{u_1} (α := α) (⨆ (i : ι), f i ⊓ g i) ((⨆ (i : ι), f i) ⊓ ⨆ (i : ι), g i)

Tactic:
le_inf (iSup_mono fun _ => inf_le_left) (iSup_mono fun _ => inf_le_right)

Premises used: inf_le_right, le_inf, inf_le_left, iSup_mono
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : CompleteLattice α
f g : ι → α
⊢ LE.le.{u_1} (α := α) ((⨅ (i : ι), f i) ⊔ ⨅ (i : ι), g i) (⨅ (i : ι), f i ⊔ g i)

Tactic:
@le_iSup_inf_iSup αᵒᵈ ι _ f g

Premises used: iInf, le_iSup_inf_iSup, OrderDual
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
a : Set α
b : α
d : Disjoint (sSup a) b
i : α
hi : i ∈ a
⊢ Disjoint i b

Tactic:
disjoint_iff_inf_le.mpr (iSup₂_le_iff.1 (iSup_inf_le_sSup_inf.trans d.le_bot) i hi :)

Premises used: Iff.mpr, Disjoint.le_bot, iSup_inf_le_sSup_inf, iSup₂_le_iff, Iff.mp, LE.le.trans, disjoint_iff_inf_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
a : Set α
b : α
d : Disjoint b (sSup a)
i : α
hi : i ∈ a
⊢ Disjoint b i

Tactic:
disjoint_iff_inf_le.mpr (iSup₂_le_iff.mp (iSup_inf_le_inf_sSup.trans d.le_bot) i hi :)

Premises used: Iff.mpr, Disjoint.le_bot, iSup_inf_le_inf_sSup, iSup₂_le_iff, Iff.mp, LE.le.trans, disjoint_iff_inf_le
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
a b : α
c d : Set α
hs : ∀ e ∈ c, e ≤ a
ht : ∀ e ∈ d, e ≤ b
hd : Disjoint a b
he : ⊥ ∉ c ∨ ⊥ ∉ d
⊢ Disjoint c d

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : CompleteLattice α
a b : Set α
hd : Disjoint (sSup a) (sSup b)
he : ⊥ ∉ a ∨ ⊥ ∉ b
⊢ Disjoint a b

Tactic:
disjoint_of_sSup_disjoint_of_le_of_le (fun _ hc ↦ le_sSup hc) (fun _ hc ↦ le_sSup hc) hd he

Premises used: disjoint_of_sSup_disjoint_of_le_of_le, le_sSup
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : SupSet α
s : Set (ULift.{v, u_1} α)
⊢ down.{v, u_1} (sSup s) = sSup (up ⁻¹' s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : SupSet α
s : Set α
⊢ { down := sSup s : ULift.{u_8, u_1} α } = sSup (down ⁻¹' s)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : InfSet α
s : Set (ULift.{v, u_1} α)
⊢ down.{v, u_1} (sInf s) = sInf (up ⁻¹' s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
inst : InfSet α
s : Set α
⊢ { down := sInf s : ULift.{u_8, u_1} α } = sInf (down ⁻¹' s)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
f : ι → ULift.{v, u_1} α
⊢ Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨆ (i : ι), f i)) (⨆ (i : ι), down.{v, u_1} (f i))

Tactic:
congr_arg sSup <| (preimage_eq_iff_eq_image ULift.up_bijective).mpr <|
    Eq.symm (range_comp _ _).symm

Premises used: Iff.mpr, Set.range_comp, ULift.up_bijective, iSup, Set.preimage_eq_iff_eq_image, congr_arg, Eq.symm, SupSet.sSup
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : SupSet α
f : ι → α
⊢ Eq (α := ULift.{u_8, u_1} α) { down := ⨆ (i : ι), f i } (⨆ (i : ι), { down := f i })

Tactic:
congr_arg ULift.up <| (down_iSup _).symm

Premises used: iSup, congr_arg, ULift.down_iSup, ULift.up, Eq.symm
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : InfSet α
f : ι → ULift.{v, u_1} α
⊢ Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨅ (i : ι), f i)) (⨅ (i : ι), down.{v, u_1} (f i))

Tactic:
congr_arg sInf <| (preimage_eq_iff_eq_image ULift.up_bijective).mpr <|
    Eq.symm (range_comp _ _).symm

Premises used: Iff.mpr, Set.range_comp, ULift.up_bijective, iInf, Set.preimage_eq_iff_eq_image, congr_arg, Eq.symm, InfSet.sInf
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
ι : Sort u_4
inst : InfSet α
f : ι → α
⊢ Eq (α := ULift.{u_8, u_1} α) { down := ⨅ (i : ι), f i } (⨅ (i : ι), { down := f i })

Tactic:
congr_arg ULift.up <| (down_iInf _).symm

Premises used: iInf, congr_arg, ULift.down_iInf, ULift.up, Eq.symm
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
s : Set (ULift.{v, u_1} α)
rw : Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨆ (a : (↑s : Type (max u_1 v))), (↑a : ULift α))) (⨆ a ∈ s, a.down)
rw₁ : Eq.{u_1 + 1} (α := α) (⨆ (i : (↑s : Type (max u_1 v))), down.{v, u_1} (↑i : ULift α)) (⨆ a ∈ s, a.down)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨆ t ∈ s, t.down) (⨆ a ∈ s, a.down)
⊢ down.{v, u_1} (sSup s) = ⨆ a ∈ s, a.down

Tactic:
rw [sSup_eq_iSup', down_iSup, iSup_subtype'']

Premises used: iSup_subtype'', ULift.down_iSup, sSup_eq_iSup'
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
inst : CompleteLattice α
s : Set (ULift.{v, u_1} α)
rw : Eq.{u_1 + 1} (α := α) (down.{v, u_1} (⨅ (a : (↑s : Type (max u_1 v))), (↑a : ULift α))) (⨅ a ∈ s, a.down)
rw₁ : Eq.{u_1 + 1} (α := α) (⨅ (i : (↑s : Type (max u_1 v))), down.{v, u_1} (↑i : ULift α)) (⨅ a ∈ s, a.down)
rw₂ rw₃ : Eq.{u_1 + 1} (α := α) (⨅ t ∈ s, t.down) (⨅ a ∈ s, a.down)
⊢ down.{v, u_1} (sInf s) = ⨅ a ∈ s, a.down

Tactic:
rw [sInf_eq_iInf', down_iInf, iInf_subtype'']

Premises used: iInf_subtype'', sInf_eq_iInf', ULift.down_iInf
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a b c : PUnit
⊢ a ≤ b ⇨ c ↔ min a b ≤ c

Tactic:
trivial
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a : PUnit
⊢ a ⇨ ⊥ = aᶜ

Tactic:
trivial
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a b c : PUnit
⊢ a \ b ≤ c ↔ a ≤ max b c

Tactic:
trivial
-- Module: Mathlib.Order.CompleteLattice.Lemmas
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
ι' : Sort u_5
κ : ι → Sort u_6
κ' : ι' → Sort u_7
a : PUnit
⊢ ⊤ \ a = ￢a

Tactic:
trivial
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
x₁ x₂ x₃ x₄ : T
inst : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₁ ≤ x₂

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
x₁ x₂ x₃ x₄ : T
inst : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₁ ≤ x₃

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
x₁ x₂ x₃ x₄ : T
inst : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₂ ≤ x₄

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
x₁ x₂ x₃ x₄ : T
inst : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ x₃ ≤ x₄

Tactic:
grind
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
x₁ x₂ x₃ x₄ : T
inst : Lattice T
sq : BicartSq x₁ x₂ x₃ x₄
⊢ CommSq (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯) (homOfLE ⋯)

Tactic:
⟨rfl⟩

Premises used: CategoryTheory.CommSq.mk, rfl
-- Module: Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
Goal:
T : Type u
inst : CompleteLattice T
ι : Type u_1
x : T
u : ι → T
v : ι → ι → T
d : MulticoequalizerDiagram x u v
x_1 : (MultispanShape.prod ι).L
⊢ (match (motive := (MultispanShape.prod ι).L → T) x_1 with
    | (i, j) => v i j) ≤
    u ((MultispanShape.prod ι).fst x_1)

Tactic:
grind