awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMinOrder α
x : α × β
a : α
b : β
c : α
h : c < a
⊢ ∃ (b_1 : α × β), b_1 < (a, b)

Tactic:
⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩

Premises used: Iff.mpr, Prod.mk, Exists.intro, Prod.mk_lt_mk_iff_left
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMinOrder α
x : α × β
a : α
b : β
c : α
h : c < a
⊢ ∃ (b_1 : α × β), b_1 < (a, b)

Tactic:
exact ⟨(c, b), Prod.mk_lt_mk_iff_left.2 h⟩
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMinOrder β
x : α × β
a : α
b : β
obtain : ∀ (c : β) (h : c < b), ∃ (b_1 : α × β), b_1 < (a, b)
⊢ ∃ (b_1 : α × β), b_1 < (a, b)

Tactic:
obtain ⟨c, h⟩ := exists_lt b

Premises used: NoMinOrder.exists_lt
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMinOrder β
x : α × β
a : α
b c : β
h : c < b
⊢ ∃ (b_1 : α × β), b_1 < (a, b)

Tactic:
⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩

Premises used: Iff.mpr, Prod.mk, Prod.mk_lt_mk_iff_right, Exists.intro
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
inst_2 : NoMinOrder β
x : α × β
a : α
b c : β
h : c < b
⊢ ∃ (b_1 : α × β), b_1 < (a, b)

Tactic:
exact ⟨(a, c), Prod.mk_lt_mk_iff_right.2 h⟩
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst : Nonempty ι
inst_1 : (i : ι) → Preorder (π i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_3} (π i)
a : (i : ι) → π i
obtain : ∀ (b : π (Classical.arbitrary ι)) (hb : b < a (Classical.arbitrary ι)), ∃ (b : (i : ι) → π i), b < a
⊢ ∃ (b : (i : ι) → π i), b < a

Tactic:
obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)

Premises used: Classical.arbitrary, NoMinOrder.exists_lt
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst : Nonempty ι
inst_1 : (i : ι) → Preorder (π i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_3} (π i)
a : (i : ι) → π i
b : π (Classical.arbitrary ι)
hb : b < a (Classical.arbitrary ι)
⊢ ∃ (b : (i : ι) → π i), b < a

Tactic:
⟨_, update_lt_self_iff.2 hb⟩

Premises used: Iff.mpr, Exists.intro, update_lt_self_iff
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst : Nonempty ι
inst_1 : (i : ι) → Preorder (π i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_3} (π i)
a : (i : ι) → π i
b : π (Classical.arbitrary ι)
hb : b < a (Classical.arbitrary ι)
⊢ ∃ (b : (i : ι) → π i), b < a

Tactic:
exact ⟨_, update_lt_self_iff.2 hb⟩
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
ι : Type u
π : ι → Type u_3
inst : Nonempty ι
inst_1 : (i : ι) → Preorder (π i)
inst_2 : ∀ (i : ι), NoMinOrder.{u_3} (π i)
a : (i : ι) → π i
obtain : ∀ (b : π (Classical.arbitrary ι)) (hb : b < a (Classical.arbitrary ι)), ∃ (b : (i : ι) → π i), b < a
⊢ ∃ (b : (i : ι) → π i), b < a

Tactic:
classical
    obtain ⟨b, hb⟩ := exists_lt (a <| Classical.arbitrary _)
    exact ⟨_, update_lt_self_iff.2 hb⟩

Premises used: Classical.arbitrary, NoMinOrder.exists_lt
-- Module: Mathlib.Order.Max
Goal:
α : Type u_3
inst : LinearOrder α
inst_1 : NoBotOrder α
a : α
⊢ ∃ (b : α), b < a

Tactic:
simpa [not_le] using exists_not_ge a

Premises used: not_le, NoBotOrder.exists_not_ge
-- Module: Mathlib.Order.Max
Goal:
α : Type u_3
inst : LinearOrder α
⊢ NoBotOrder α ↔ NoMinOrder α

Tactic:
⟨fun _ => NoBotOrder.to_noMinOrder α, fun _ => inferInstance⟩

Premises used: inferInstance, NoBotOrder.to_noMinOrder, Iff.intro
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : LT α
inst_1 : NoMinOrder α
a : α
⊢ ¬Acc (fun (x1 x2 : α) ↦ x1 < x2) a

Tactic:
fun h =>
  Acc.recOn h fun x _ => (exists_lt x).recOn

Premises used: Acc.recOn, Not
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : LE α
simp_rw : (∀ (a : α), ∃ (b : α), ¬a ≤ b) ↔ ∀ (x : α), ¬IsBot x
simp_rw₁ : (∀ (a : α), ∃ (b : α), ¬a ≤ b) ↔ ∀ (x : α), ¬∀ (b : α), x ≤ b
⊢ NoBotOrder α ↔ ∀ (x : α), ¬IsBot x

Tactic:
simp_rw [noBotOrder_iff', IsBot, not_forall]

Premises used: IsBot, Classical.not_forall, noBotOrder_iff'
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : LE α
inst_1 : NoBotOrder α
a : α
⊢ ¬IsBot a

Tactic:
fun h =>
  let ⟨_, hb⟩ := exists_not_ge a
  hb <| h _

Premises used: _private.0.not_isBot.match_1, False, NoBotOrder.exists_not_ge, Not
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : LE α
a : α
h : IsBot a
⊢ IsMin a

Tactic:
fun b _ => h b

Premises used: IsMin
-- Module: Mathlib.Order.Max
Goal:
α : Type u_3
inst : PartialOrder α
i j : α
h : IsBot i
simp_rw : IsMin j ↔ j ≤ i
⊢ IsMin j ↔ j = i

Tactic:
simp_rw [le_antisymm_iff, h j, and_true]

Premises used: and_true, le_antisymm_iff
-- Module: Mathlib.Order.Max
Goal:
α : Type u_3
inst : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i

Tactic:
⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ le_trans a (h h')⟩

Premises used: Iff.intro, le_trans
-- Module: Mathlib.Order.Max
Goal:
α : Type u_3
inst : PartialOrder α
i j : α
h : IsBot i
⊢ IsMin j ↔ j ≤ i

Tactic:
exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ le_trans a (h h')⟩
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : LE α
a : α
⊢ IsBot (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsTop a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsTop, OrderDual
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : LE α
a : α
⊢ IsMin (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsMax a

Tactic:
Iff.rfl

Premises used: Iff.rfl, OrderDual, IsMax
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : LE α
a : αᵒᵈ
⊢ IsBot (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ IsTop a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsTop, OrderDual
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : LE α
a : αᵒᵈ
⊢ IsMin (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ↔ IsMax a

Tactic:
Iff.rfl

Premises used: Iff.rfl, OrderDual, IsMax
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
⊢ NoMinOrder α ↔ ∀ (x : α), ¬IsMin x

Tactic:
simp [noMinOrder_iff', IsMin, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, noMinOrder_iff', IsMin
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
a b : α
ha : IsBot a
h : b ≤ a
⊢ IsBot b

Tactic:
fun _ => h.trans <| ha _

Premises used: IsBot, LE.le.trans
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
a b : α
ha : IsMin a
h : b ≤ a
⊢ IsMin b

Tactic:
fun _ hc => h.trans <| ha <| hc.trans h

Premises used: LE.le.trans, IsMin
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : IsMin a
⊢ ¬b < a

Tactic:
fun hb => hb.not_ge <| h hb.le

Premises used: LT.lt.le, LT.lt.not_ge, Not
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : b < a
⊢ ¬IsMin a

Tactic:
fun ha => ha.not_lt h

Premises used: IsMin.not_lt, Not
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ IsMin a ↔ ∀ (b : α), ¬b < a

Tactic:
⟨fun h _ => h.not_lt, fun h _ hba => of_not_not fun hab => h _ <| hba.lt_of_not_ge hab⟩

Premises used: LE.le.lt_of_not_ge, IsMin.not_lt, Iff.intro, of_not_not
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ¬IsMin a ↔ ∃ (b : α), b < a

Tactic:
simp [lt_iff_le_not_ge, IsMin, not_forall]

Premises used: lt_iff_le_not_ge, Classical.not_forall, IsMin
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMinOrder α
a : α
⊢ ¬IsMin a

Tactic:
not_isMin_iff.2 <| exists_lt a

Premises used: not_isMin_iff, Iff.mpr, NoMinOrder.exists_lt
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Subsingleton α
a : α
⊢ IsBot a

Tactic:
fun _ => (Subsingleton.elim _ _).le

Premises used: IsBot, Eq.le, Subsingleton.elim
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Subsingleton α
a : α
⊢ IsMin a

Tactic:
(Subsingleton.isBot _).isMin

Premises used: IsBot.isMin, Subsingleton.isBot
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
ha : IsMin a
h : b ≤ a
⊢ b = a

Tactic:
h.antisymm <| ha h

Premises used: LE.le.antisymm
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
ha : IsMin a
h : b ≤ a
⊢ a = b

Tactic:
h.antisymm' <| ha h

Premises used: LE.le.antisymm'
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
ha : IsBot a
h : a ≠ b
⊢ a < b

Tactic:
(ha b).lt_of_ne h

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
ha : IsTop a
h : b ≠ a
⊢ b < a

Tactic:
(ha b).lt_of_ne h

Premises used: LE.le.lt_of_ne
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : Nontrivial α
ha : IsBot a
ha' : IsMax a
obtain : ∀ (b : α) (hb : b ≠ a), False
⊢ False

Tactic:
obtain ⟨b, hb⟩ := exists_ne a

Premises used: exists_ne
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : Nontrivial α
ha : IsBot a
ha' : IsMax a
b : α
hb : b ≠ a
⊢ False

Tactic:
hb <| ha'.eq_of_ge (ha.lt_of_ne hb.symm).le

Premises used: LT.lt.le, Ne.symm, IsMax.eq_of_ge, IsBot.lt_of_ne
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : Nontrivial α
ha : IsBot a
ha' : IsMax a
b : α
hb : b ≠ a
⊢ False

Tactic:
exact hb <| ha'.eq_of_ge (ha.lt_of_ne hb.symm).le

Premises used: LT.lt.le, Ne.symm, IsMax.eq_of_ge, IsBot.lt_of_ne
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : Nontrivial α
ha : IsBot a
⊢ ¬IsTop a

Tactic:
mt IsTop.isMax ha.not_isMax

Premises used: mt, IsBot.not_isMax, IsTop.isMax
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
ha : IsBot a
hb : IsBot b
⊢ IsBot (a, b)

Tactic:
fun _ => ⟨ha _, hb _⟩

Premises used: IsBot, Prod.fst, And.intro, Prod.snd
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
ha : IsMin a
hb : IsMin b
⊢ IsMin (a, b)

Tactic:
fun _ hc => ⟨ha hc.1, hb hc.2⟩

Premises used: And.right, And.left, And.intro, IsMin
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
hx : IsBot x
⊢ IsBot x.fst

Tactic:
fun c => (hx (c, x.2)).1

Premises used: IsBot, Prod.mk, And.left, Prod.snd
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
hx : IsBot x
⊢ IsBot x.snd

Tactic:
fun c => (hx (x.1, c)).2

Premises used: IsBot, Prod.mk, Prod.fst, And.right
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
hx : IsMin x
⊢ IsMin x.fst

Tactic:
fun c hc => (hx <| show (c, x.2) ≤ x from (and_iff_left le_rfl).2 hc).1

Premises used: Iff.mpr, le_rfl, and_iff_left, And.left, IsMin
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
hx : IsMin x
⊢ IsMin x.snd

Tactic:
fun c hc => (hx <| show (x.1, c) ≤ x from (and_iff_right le_rfl).2 hc).2

Premises used: Iff.mpr, le_rfl, and_iff_right, And.right, IsMin
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
⊢ IsBot x ↔ IsBot x.fst ∧ IsBot x.snd

Tactic:
⟨fun hx => ⟨hx.fst, hx.snd⟩, fun h => h.1.prodMk h.2⟩

Premises used: IsBot.snd, And.right, And.left, And.intro, Iff.intro, IsBot.fst, IsBot.prodMk
-- Module: Mathlib.Order.Max
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
x : α × β
⊢ IsMin x ↔ IsMin x.fst ∧ IsMin x.snd

Tactic:
⟨fun hx => ⟨hx.fst, hx.snd⟩, fun h => h.1.prodMk h.2⟩

Premises used: IsMin.snd, IsMin.prodMk, And.right, And.left, And.intro, IsMin.fst, Iff.intro
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ c ≤ min a b ↔ c ≤ a ∧ c ≤ b

Tactic:
le_inf_iff

Premises used: le_inf_iff
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ a ≤ max b c ↔ a ≤ b ∨ a ≤ c

Tactic:
le_sup_iff

Premises used: le_sup_iff
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ a < min b c ↔ a < b ∧ a < c

Tactic:
lt_inf_iff

Premises used: lt_inf_iff
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ a < max b c ↔ a < b ∨ a < c

Tactic:
lt_sup_iff

Premises used: lt_sup_iff
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c d : α
⊢ a ≤ c → b ≤ d → max a b ≤ max c d

Tactic:
sup_le_sup

Premises used: sup_le_sup
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
h : a ≤ b
⊢ max c a ≤ max c b

Tactic:
sup_le_sup_left h c

Premises used: sup_le_sup_left
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
h : a ≤ b
⊢ max a c ≤ max b c

Tactic:
sup_le_sup_right h c

Premises used: sup_le_sup_right
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ a ≤ b → a ≤ max b c

Tactic:
le_sup_of_le_left

Premises used: le_sup_of_le_left
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ a ≤ c → a ≤ max b c

Tactic:
le_sup_of_le_right

Premises used: le_sup_of_le_right
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
h : a < b
⊢ a < max b c

Tactic:
h.trans_le (le_max_left b c)

Premises used: LT.lt.trans_le, le_max_left
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
h : a < c
⊢ a < max b c

Tactic:
h.trans_le (le_max_right b c)

Premises used: le_max_right, LT.lt.trans_le
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ max a (min b c) = min (max a b) (max a c)

Tactic:
sup_inf_left _ _ _

Premises used: sup_inf_left
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ max (min a b) c = min (max a c) (max b c)

Tactic:
sup_inf_right _ _ _

Premises used: sup_inf_right
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b : α
⊢ min a b ≤ max a b

Tactic:
le_trans (min_le_left a b) (le_max_left a b)

Premises used: min_le_left, le_max_left, le_trans
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b : α
⊢ min a b = a ↔ a ≤ b

Tactic:
inf_eq_left

Premises used: inf_eq_left
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b : α
⊢ min a b = b ↔ b ≤ a

Tactic:
inf_eq_right

Premises used: inf_eq_right
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b : α
⊢ min a b = a ∧ a ≤ b ∨ min a b = b ∧ b < a

Tactic:
grind
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ min a b = c ↔ a = c ∧ a ≤ b ∨ b = c ∧ b ≤ a

Tactic:
grind
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ min a c < min b c ↔ a < b ∧ a < c

Tactic:
grind
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
⊢ min a b < min a c ↔ b < c ∧ b < a

Tactic:
grind
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
a b c d : α
⊢ ∀ (x : α), max x x = x

Tactic:
simp
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b : α
⊢ min a b < max a b ↔ a ≠ b

Tactic:
inf_lt_sup

Premises used: inf_lt_sup
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c d : α
h₁ : a < c
h₂ : b < d
⊢ max a b < max c d

Tactic:
max_lt (lt_max_of_lt_left h₁) (lt_max_of_lt_right h₂)

Premises used: lt_max_of_lt_left, lt_max_of_lt_right, max_lt
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
rw : min a (min b c) = min (min a c) b
rw₁ : min a (min c b) = min (min a c) b
rw₂ rw₃ : min (min a c) b = min (min a c) b
⊢ min (min a b) c = min (min a c) b

Tactic:
rw [min_assoc, min_comm b, ← min_assoc]

Premises used: min_comm, min_assoc
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
inl : ∀ (h : a ≤ b), f (max a b) = max (f a) (f b)
inr : ∀ (h : b ≤ a), f (max a b) = max (f a) (f b)
⊢ f (max a b) = max (f a) (f b)

Tactic:
rcases le_total a b with h | h

Premises used: le_total
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)

Tactic:
simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]

Premises used: max_eq_left, max_eq_right
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
a b : α
hf : MonotoneOn f s
ha : a ∈ s
hb : b ∈ s
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)

Tactic:
simp only [max_eq_right, max_eq_left, hf ha hb, hf hb ha, h]

Premises used: max_eq_left, max_eq_right
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
s : Set α
a b : α
hf : AntitoneOn f s
ha : a ∈ s
hb : b ∈ s
⊢ f (max a b) = min (f a) (f b)

Tactic:
hf.dual_right.map_max ha hb

Premises used: AntitoneOn.dual_right, MonotoneOn.map_max, OrderDual
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Monotone f
inl : ∀ (h : a ≤ b), f (max a b) = max (f a) (f b)
inr : ∀ (h : b ≤ a), f (max a b) = max (f a) (f b)
⊢ f (max a b) = max (f a) (f b)

Tactic:
rcases le_total a b with h | h

Premises used: le_total
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Monotone f
h : a ≤ b
⊢ f (max a b) = max (f a) (f b)

Tactic:
simp [h, hf h]
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Monotone f
h : b ≤ a
⊢ f (max a b) = max (f a) (f b)

Tactic:
simp [h, hf h]
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Antitone f
inl : ∀ (h : a ≤ b), f (max a b) = min (f a) (f b)
inr : ∀ (h : b ≤ a), f (max a b) = min (f a) (f b)
⊢ f (max a b) = min (f a) (f b)

Tactic:
rcases le_total a b with h | h

Premises used: le_total
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Antitone f
h : a ≤ b
⊢ f (max a b) = min (f a) (f b)

Tactic:
simp [h, hf h]
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
a b : α
hf : Antitone f
h : b ≤ a
⊢ f (max a b) = min (f a) (f b)

Tactic:
simp [h, hf h]
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b : α
inl : a ≤ b → min a b = a ∨ min a b = b
inr : b ≤ a → min a b = a ∨ min a b = b
⊢ min a b = a ∨ min a b = b

Tactic:
cases le_total a b

Premises used: le_total
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ min a b = a ∨ min a b = b

Tactic:
simp [*]
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b : α
h : b ≤ a
⊢ min a b = a ∨ min a b = b

Tactic:
simp [*]
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
h : max a b ≤ c
⊢ a ≤ c

Tactic:
le_trans (le_max_left _ _) h

Premises used: le_max_left, le_trans
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
a b c : α
h : max a b ≤ c
⊢ b ≤ c

Tactic:
le_trans (le_max_right _ _) h

Premises used: le_max_right, le_trans
-- Module: Mathlib.Order.MinMax
Goal:
α : Type u
inst : LinearOrder α
⊢ LeftCommutative.{u + 1, u + 1} (α := α) max

Tactic:
⟨max_left_comm⟩

Premises used: max_left_comm, LeftCommutative.mk
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
f : ι → α
i j : ι
⊢ MinimalFor (fun (x : ι) ↦ x = j) f i ↔ i = j

Tactic:
simp +contextual [MinimalFor]

Premises used: MinimalFor
-- Module: Mathlib.Order.Minimal
Goal:
ι : Type u_1
α : Type u_2
inst : LE α
P Q : ι → Prop
f : ι → α
i : ι
h : MinimalFor P f i
hle : Q ≤ P
hQ : Q i
⊢ MinimalFor Q f i

Tactic:
⟨hQ, (h.le_of_le <| hle · ·)⟩

Premises used: And.intro, MinimalFor, MinimalFor.le_of_le
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : LE α
⊢ MinimalFor P id x ↔ Minimal P x

Tactic:
.rfl

Premises used: Iff.rfl, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
x : α
inst : LE α
⊢ Minimal (α := αᵒᵈ) (fun (x : αᵒᵈ) ↦ P ((ofDual : (a : αᵒᵈ) → α) x)) ((toDual : (a : α) → αᵒᵈ) x : αᵒᵈ) ↔ Maximal P x

Tactic:
Iff.rfl

Premises used: Iff.rfl, Maximal, OrderDual
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
inst : LE α
⊢ ¬Minimal (fun (x : α) ↦ False) x

Tactic:
simp [Minimal]

Premises used: Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
x : α
inst : LE α
⊢ Minimal (fun (x : α) ↦ True) x ↔ IsMin x

Tactic:
simp [IsMin, Minimal]

Premises used: Minimal, IsMin
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : Subtype Q
obtain :
  ∀ (x : α) (hx : Q x),
    Minimal (fun (x : Subtype Q) ↦ P (↑x : α)) (Subtype.mk (p := Q) x hx) ↔
      Minimal (P ⊓ Q) (↑(Subtype.mk (p := Q) x hx) : α)
⊢ Minimal (fun (x : Subtype Q) ↦ P (↑x : α)) x ↔ Minimal (P ⊓ Q) (↑x : α)

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
simp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
⊢ Minimal (fun (x : Subtype Q) ↦ P (↑x : α)) (Subtype.mk (p := Q) x hx) ↔
    Minimal (P ⊓ Q) (↑(Subtype.mk (p := Q) x hx) : α)

Tactic:
simp only [Minimal, Subtype.forall, Subtype.mk_le_mk, Pi.inf_apply, inf_Prop_eq]

Premises used: Subtype.forall, inf_Prop_eq, Pi.inf_apply, Subtype.mk_le_mk, Minimal
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P Q : α → Prop
inst : LE α
x : α
hx : Q x
mp : (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr : ((P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₁ mp₂ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mp₃ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → P x
mp₄ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → Q x
mp₅ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr₁ mpr₂ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mpr₃ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → P x
mpr₄ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a
mp₆ mp₇ mp₈ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y
mpr₅ mpr₆ mpr₇ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → ∀ (a : α), Q a → P a → a ≤ x → x ≤ a
mp₉ mp₁₀ mp₁₁ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, y ≤ x → P y → Q y → x ≤ y
mpr₈ mpr₉ mpr₁₀ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → ∀ (a : α), Q a → P a → a ≤ x → x ≤ a
mp₁₂ mp₁₃ mp₁₄ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, y ≤ x → P y → Q y → x ≤ y
mpr₁₁ mpr₁₂ mpr₁₃ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → ∀ (a : α), Q a → P a → a ≤ x → x ≤ a
mp₁₅ mp₁₆ : P x → (∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) → ∀ ⦃y : α⦄, y ≤ x → P y → Q y → x ≤ y
mpr₁₄ mpr₁₅ : (∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y) → P x → Q x → ∀ (a : α), Q a → P a → a ≤ x → x ≤ a
⊢ (P x ∧ ∀ (a : α) (b : Q a), P a → a ≤ x → x ≤ a) ↔ (P x ∧ Q x) ∧ ∀ ⦃y : α⦄, P y ∧ Q y → y ≤ x → x ≤ y

Tactic:
tauto
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
inst : LE α
x : Subtype P
obtain :
  ∀ (x : α) (hx : P x),
    Minimal (fun (x : Subtype P) ↦ True) (Subtype.mk (p := P) x hx) ↔ Minimal P (↑(Subtype.mk (p := P) x hx) : α)
⊢ Minimal (fun (x : Subtype P) ↦ True) x ↔ Minimal P (↑x : α)

Tactic:
obtain ⟨x, hx⟩ := x
-- Module: Mathlib.Order.Minimal
Goal:
α : Type u_2
P : α → Prop
inst : LE α
x : α
hx : P x
⊢ Minimal (fun (x : Subtype P) ↦ True) (Subtype.mk (p := P) x hx) ↔ Minimal P (↑(Subtype.mk (p := P) x hx) : α)

Tactic:
simp [Minimal, hx]

Premises used: Minimal