awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
d : α
rd : rα d a
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(d, b)

Tactic:
exact iha d rd ⟨b, hb⟩

Premises used: Acc.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c b
intro :
  Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(a, c)
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(c, a)

Tactic:
rw [Sym2.eq_swap]

Premises used: Sym2.eq_swap
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c b
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(a, c)

Tactic:
ihb c rc

Premises used: Sym2.GameAdd
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
a_1 a : α
h : ∀ (y : α), rα y a → Acc rα y
iha : ∀ (y : α), rα y a → ∀ {b : α} (hb : Acc rα b), Acc (Sym2.GameAdd rα) s(y, b)
b_1 b : α
hb : ∀ (y : α), rα y b → Acc rα y
ihb : ∀ (y : α), rα y b → Acc (Sym2.GameAdd rα) s(a, y)
c : α
rc : rα c b
⊢ Acc
    ((Sym2.lift₂ :
        (a :
            { f : α → α → α → α → Prop //
              ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁ }) →
          Sym2 α → Sym2 α → Prop)
      (Subtype.mk (p := fun (f : α → α → α → α → Prop) ↦
        ∀ (a₁ a₂ b₁ b₂ : α), f a₁ a₂ b₁ b₂ = f a₂ a₁ b₁ b₂ ∧ f a₁ a₂ b₁ b₂ = f a₁ a₂ b₂ b₁)
        (fun (a₁ b₁ a₂ b₂ : α) ↦ Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) ∨ Prod.GameAdd rα rα (b₁, a₁) (a₂, b₂)) ⋯))
    s(a, c)

Tactic:
exact ihb c rc
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
h : WellFounded rα
⊢ WellFounded (Sym2.GameAdd rα)

Tactic:
⟨fun i => Sym2.inductionOn i fun x y => (h.apply x).sym2_gameAdd (h.apply y)⟩

Premises used: Sym2.inductionOn, WellFounded.intro
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
β : Type u_2
rα : α → α → Prop
rβ : β → β → Prop
a_1 : α
b_1 : β
C : α → α → Sort u_3
hr : WellFounded rα
IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁
a b : α
⊢ WellFounded fun (x y : α × α) ↦ Prod.GameAdd rα rα x y ∨ Prod.GameAdd rα rα x.swap y

Tactic:
simpa [← Sym2.gameAdd_iff] using hr.sym2_gameAdd.onFun

Premises used: WellFounded.sym2_gameAdd, WellFounded.onFun, Sym2.gameAdd_iff
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα : α → α → Prop
C : α → α → Sort u_3
hr : WellFounded rα
IH : (a₁ b₁ : α) → ((a₂ b₂ : α) → GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁
a b : α
⊢ recursion (rα := rα) (C := fun (x x_1 : α) ↦ C x x_1) hr IH a b =
    IH a b fun (a' b' : α) (x : GameAdd rα s(a', b') s(a, b)) ↦
      recursion (rα := rα) (C := fun (x x_1 : α) ↦ C x x_1) hr IH a' b'

Tactic:
WellFounded.fix_eq ..

Premises used: Sym2.GameAdd, Sym2.GameAdd.recursion, WellFounded.fix_eq, Prod.swap
-- Module: Mathlib.Order.GameAdd
Goal:
α : Type u_1
rα C : α → α → Prop
⊢ WellFounded rα →
    (∀ (a₁ b₁ : α), (∀ (a₂ b₂ : α), GameAdd rα s(a₂, b₂) s(a₁, b₁) → C a₂ b₂) → C a₁ b₁) → ∀ (a b : α), C a b

Tactic:
GameAdd.recursion

Premises used: Sym2.GameAdd.recursion
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeOrder 𝕆 α
a b : α
h : a ⋖ b
⊢ grade 𝕆 a ⋖ grade 𝕆 b

Tactic:
GradeOrder.covBy_grade h

Premises used: GradeOrder.covBy_grade, grade
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeOrder 𝕆 α
⊢ StrictMono.{u_3, u_1} (α := α) (grade 𝕆)

Tactic:
GradeOrder.grade_strictMono

Premises used: GradeOrder.grade_strictMono, grade
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeOrder 𝕆 α
a b : α
⊢ a ⋖ b ↔ a < b ∧ grade 𝕆 a ⋖ grade 𝕆 b

Tactic:
⟨fun h => ⟨h.1, h.grade _⟩,
    And.imp_right fun h _ ha hb => h.2 (grade_strictMono ha) <| grade_strictMono hb⟩

Premises used: grade_strictMono, And.right, And.left, And.intro, Iff.intro, CovBy.grade, And.imp_right
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeMinOrder 𝕆 α
a : α
h : IsMin a
⊢ IsMin (grade 𝕆 a)

Tactic:
GradeMinOrder.isMin_grade h

Premises used: GradeMinOrder.isMin_grade, grade
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeMinOrder 𝕆 α
a : α
⊢ IsMin (grade 𝕆 a) ↔ IsMin a

Tactic:
⟨grade_strictMono.isMin_of_apply, IsMin.grade _⟩

Premises used: StrictMono.isMin_of_apply, grade_strictMono, IsMin.grade, Iff.intro
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeMaxOrder 𝕆 α
a : α
h : IsMax a
⊢ IsMax (grade 𝕆 a)

Tactic:
GradeMaxOrder.isMax_grade h

Premises used: grade, GradeMaxOrder.isMax_grade
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeMaxOrder 𝕆 α
a : α
⊢ IsMax (grade 𝕆 a) ↔ IsMax a

Tactic:
⟨grade_strictMono.isMax_of_apply, IsMax.grade _⟩

Premises used: grade_strictMono, StrictMono.isMax_of_apply, IsMax.grade, Iff.intro
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : PartialOrder α
inst_2 : GradeOrder 𝕆 α
⊢ Monotone.{u_3, u_1} (α := α) (grade 𝕆)

Tactic:
grade_strictMono.monotone

Premises used: grade_strictMono, StrictMono.monotone
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : LinearOrder α
inst_2 : GradeOrder 𝕆 α
⊢ Function.Injective.{u_3 + 1, u_1 + 1} (α := α) (grade 𝕆)

Tactic:
grade_strictMono.injective

Premises used: grade_strictMono, StrictMono.injective
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : LinearOrder α
inst_2 : GradeOrder 𝕆 α
a b : α
⊢ grade 𝕆 a ≤ grade 𝕆 b ↔ a ≤ b

Tactic:
grade_strictMono.le_iff_le

Premises used: grade_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : LinearOrder α
inst_2 : GradeOrder 𝕆 α
a b : α
⊢ grade 𝕆 a < grade 𝕆 b ↔ a < b

Tactic:
grade_strictMono.lt_iff_lt

Premises used: grade_strictMono, StrictMono.lt_iff_lt
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : LinearOrder α
inst_2 : GradeOrder 𝕆 α
a b : α
⊢ grade 𝕆 a = grade 𝕆 b ↔ a = b

Tactic:
grade_injective.eq_iff

Premises used: Function.Injective.eq_iff, grade_injective
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : LinearOrder α
inst_2 : GradeOrder 𝕆 α
a b : α
⊢ grade 𝕆 a ≠ grade 𝕆 b ↔ a ≠ b

Tactic:
grade_injective.ne_iff

Premises used: Function.Injective.ne_iff, grade_injective
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : LinearOrder α
inst_2 : GradeOrder 𝕆 α
a b : α
⊢ grade 𝕆 a ⋖ grade 𝕆 b ↔ a ⋖ b

Tactic:
(covBy_iff_lt_covBy_grade.trans <| and_iff_right_of_imp fun h => grade_lt_grade_iff.1 h.1).symm

Premises used: covBy_iff_lt_covBy_grade, grade_lt_grade_iff, And.left, Iff.mp, Iff.trans, and_iff_right_of_imp, Iff.symm
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : PartialOrder 𝕆
inst_1 : Preorder α
inst_2 : OrderBot 𝕆
inst_3 : OrderBot α
inst_4 : GradeMinOrder 𝕆 α
⊢ grade.{u_1, u_3} 𝕆 (α := α) ⊥ = ⊥

Tactic:
(isMin_bot.grade _).eq_bot

Premises used: IsMin.grade, IsMin.eq_bot, isMin_bot
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : PartialOrder 𝕆
inst_1 : Preorder α
inst_2 : OrderTop 𝕆
inst_3 : OrderTop α
inst_4 : GradeMaxOrder 𝕆 α
⊢ grade.{u_1, u_3} 𝕆 (α := α) ⊤ = ⊤

Tactic:
(isMax_top.grade _).eq_top

Premises used: isMax_top, IsMax.eq_top, IsMax.grade
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : Preorder α
a : α
⊢ grade α a = a

Tactic:
rfl

Premises used: grade, rfl
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeOrder 𝕆 α
a : α
⊢ Eq (α := 𝕆ᵒᵈ) (grade 𝕆ᵒᵈ (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) : 𝕆ᵒᵈ)
    ((toDual : (a : 𝕆) → 𝕆ᵒᵈ) (grade 𝕆 a) : 𝕆ᵒᵈ)

Tactic:
rfl

Premises used: grade, rfl
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : Preorder 𝕆
inst_1 : Preorder α
inst_2 : GradeOrder 𝕆 α
a : αᵒᵈ
⊢ grade 𝕆 (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) = (ofDual : (a : 𝕆ᵒᵈ) → 𝕆) (grade 𝕆ᵒᵈ a)

Tactic:
rfl

Premises used: grade, rfl
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
n : ℕ
inst_4 : GradeMinOrder (Fin n) α
a : Fin n
h : IsMin a
zero : ∀ [GradeMinOrder (Fin 0) α] (a : Fin 0) (h : IsMin a), IsMin (↑a : ℕ)
succ : ∀ (n : ℕ) [GradeMinOrder (Fin (n + 1)) α] (a : Fin (n + 1)) (h : IsMin a), IsMin (↑a : ℕ)
⊢ IsMin (↑a : ℕ)

Tactic:
cases n
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
inst_4 : GradeMinOrder (Fin 0) α
a : Fin 0
h : IsMin a
⊢ IsMin (↑a : ℕ)

Tactic:
a.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
inst_4 : GradeMinOrder (Fin 0) α
a : Fin 0
h : IsMin a
⊢ IsMin (↑a : ℕ)

Tactic:
exact a.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
n : ℕ
inst_4 : GradeMinOrder (Fin (n + 1)) α
a : Fin (n + 1)
h : IsMin a
succ : IsMin (↑0 : ℕ)
⊢ IsMin (↑a : ℕ)

Tactic:
rw [h.eq_bot, bot_eq_zero]

Premises used: IsMin.eq_bot, bot_eq_zero
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
n : ℕ
inst_4 : GradeMinOrder (Fin (n + 1)) α
a : Fin (n + 1)
h : IsMin a
⊢ IsMin (↑0 : ℕ)

Tactic:
isMin_bot

Premises used: Nat.mod, isMin_bot
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
n : ℕ
inst_4 : GradeMinOrder (Fin (n + 1)) α
a : Fin (n + 1)
h : IsMin a
⊢ IsMin (↑0 : ℕ)

Tactic:
exact isMin_bot

Premises used: isMin_bot
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : Preorder α
𝕆 : Type u_5
inst_1 : Preorder 𝕆
inst_2 : GradeOrder 𝕆 α
inst_3 : WellFoundedLT 𝕆
⊢ WellFoundedLT α

Tactic:
(grade_strictMono (𝕆 := 𝕆)).wellFoundedLT

Premises used: StrictMono.wellFoundedLT, GradeOrder.grade_strictMono
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : Preorder α
𝕆 : Type u_5
inst_1 : Preorder 𝕆
inst_2 : GradeOrder 𝕆 α
inst_3 : WellFoundedGT 𝕆
⊢ WellFoundedGT α

Tactic:
(grade_strictMono (𝕆 := 𝕆)).wellFoundedGT

Premises used: StrictMono.wellFoundedGT, GradeOrder.grade_strictMono
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
inst_4 : GradeOrder ℕ α
⊢ WellFoundedLT α

Tactic:
GradeOrder.wellFoundedLT ℕ

Premises used: GradeOrder.wellFoundedLT, Nat
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
ℙ : Type u_2
α : Type u_3
β : Type u_4
inst : Preorder 𝕆
inst_1 : Preorder ℙ
inst_2 : Preorder α
inst_3 : Preorder β
inst_4 : GradeOrder ℕᵒᵈ α
⊢ WellFoundedGT α

Tactic:
GradeOrder.wellFoundedGT ℕᵒᵈ

Premises used: Nat, OrderDual, GradeOrder.wellFoundedGT
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
⊢ (↑a : α) ⩿ (↑b : α) ↔ a ⩿ b

Tactic:
and_congr_right' ⟨fun h c hac ↦ h hac, fun h c hac hcb ↦
    @h ⟨c, mem_iff_forall_le_or_ge.2 fun d hd ↦ ?_⟩ hac hcb⟩

Premises used: and_congr_right', WCovBy, Iff.intro
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
refine :
  ∀ (h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b) (c : α) (hac : (↑a : α) < c) (hcb : c < (↑b : α)) (d : α) (hd : d ∈ s),
    c ≤ d ∨ d ≤ c
⊢ (↑a : α) ⩿ (↑b : α) ↔ a ⩿ b

Tactic:
refine and_congr_right' ⟨fun h c hac ↦ h hac, fun h c hac hcb ↦
    @h ⟨c, mem_iff_forall_le_or_ge.2 fun d hd ↦ ?_⟩ hac hcb⟩

Premises used: and_congr_right', Iff.intro
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
inl : ∀ (hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a), c ≤ d ∨ d ≤ c
inr : ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
⊢ c ≤ d ∨ d ≤ c

Tactic:
obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a

Premises used: Subtype.mk, le_or_gt
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a
⊢ c ≤ d ∨ d ≤ c

Tactic:
.inr ((Subtype.coe_le_coe.2 hda).trans hac.le)

Premises used: Iff.mpr, Subtype.coe_le_coe, LT.lt.le, LE.le.trans, Or.inr
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a
⊢ c ≤ d ∨ d ≤ c

Tactic:
exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
inr : ∀ (hbd : b ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
inr₁ : ∀ (hdb : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd < b), c ≤ d ∨ d ≤ c
⊢ c ≤ d ∨ d ≤ c

Tactic:
obtain hbd | hdb := le_or_gt b ⟨d, hd⟩

Premises used: Subtype.mk, le_or_gt
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
hbd : b ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
⊢ c ≤ d ∨ d ≤ c

Tactic:
.inl (hcb.le.trans hbd)

Premises used: LT.lt.le, Or.inl, LE.le.trans
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
hbd : b ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
⊢ c ≤ d ∨ d ≤ c

Tactic:
exact .inl (hcb.le.trans hbd)
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
hdb : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd < b
⊢ c ≤ d ∨ d ≤ c

Tactic:
cases h had hdb
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
h : ∀ ⦃c : ↥s⦄, a < c → ¬c < b
c : α
hac : (↑a : α) < c
hcb : c < (↑b : α)
d : α
hd : d ∈ s
inl : ∀ (hda : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd ≤ a), c ≤ d ∨ d ≤ c
inr inr₁ : ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd), c ≤ d ∨ d ≤ c
inr₂ :
  ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd) (hbd : b ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd),
    c ≤ d ∨ d ≤ c
inr₃ inr₄ :
  ∀ (had : a < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd) (hdb : Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd < b),
    c ≤ d ∨ d ≤ c
⊢ c ≤ d ∨ d ≤ c

Tactic:
classical
  obtain hda | had := le_or_gt (⟨d, hd⟩ : s) a
  · exact .inr ((Subtype.coe_le_coe.2 hda).trans hac.le)
  obtain hbd | hdb := le_or_gt b ⟨d, hd⟩
  · exact .inl (hcb.le.trans hbd)
  · cases h had hdb
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a b : ↥s
⊢ (↑a : α) ⋖ (↑b : α) ↔ a ⋖ b

Tactic:
simp [covBy_iff_wcovBy_and_not_le]

Premises used: covBy_iff_wcovBy_and_not_le
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMax a
b : α
hab : (↑a : α) ≤ b
⊢ b ≤ (↑a : α)

Tactic:
@h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hab
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMax a
b : α
hab : (↑a : α) ≤ b
refine : ∀ (c : α) (hc : c ∈ s), b ≤ c ∨ c ≤ b
⊢ b ≤ (↑a : α)

Tactic:
refine @h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hab
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMax a
b : α
hab : (↑a : α) ≤ b
c : α
hc : c ∈ s
⊢ b ≤ c ∨ c ≤ b

Tactic:
.inr <| hab.trans' <| h.isTop ⟨c, hc⟩

Premises used: IsMax.isTop, Subtype.mk, Or.inr, LE.le.trans'
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMax a
b : α
hab : (↑a : α) ≤ b
c : α
hc : c ∈ s
⊢ b ≤ c ∨ c ≤ b

Tactic:
exact .inr <| hab.trans' <| h.isTop ⟨c, hc⟩

Premises used: IsMax.isTop, Subtype.mk, LE.le.trans'
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMax a
b : α
hab : (↑a : α) ≤ b
c : α
hc : c ∈ s
⊢ b ≤ c ∨ c ≤ b

Tactic:
classical
    exact .inr <| hab.trans' <| h.isTop ⟨c, hc⟩

Premises used: LE.le.trans'
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMin a
b : α
hba : b ≤ (↑a : α)
⊢ (↑a : α) ≤ b

Tactic:
@h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hba
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMin a
b : α
hba : b ≤ (↑a : α)
refine : ∀ (c : α) (hc : c ∈ s), b ≤ c ∨ c ≤ b
⊢ (↑a : α) ≤ b

Tactic:
refine @h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hba
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMin a
b : α
hba : b ≤ (↑a : α)
c : α
hc : c ∈ s
⊢ b ≤ c ∨ c ≤ b

Tactic:
.inl <| hba.trans <| h.isBot ⟨c, hc⟩

Premises used: IsMin.isBot, Subtype.mk, Or.inl, LE.le.trans
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMin a
b : α
hba : b ≤ (↑a : α)
c : α
hc : c ∈ s
⊢ b ≤ c ∨ c ≤ b

Tactic:
exact .inl <| hba.trans <| h.isBot ⟨c, hc⟩

Premises used: IsMin.isBot, Subtype.mk, LE.le.trans
-- Module: Mathlib.Order.Grade
Goal:
α : Type u_3
inst : PartialOrder α
s : Flag α
a : ↥s
h : IsMin a
b : α
hba : b ≤ (↑a : α)
c : α
hc : c ∈ s
⊢ b ≤ c ∨ c ≤ b

Tactic:
classical
    exact .inl <| hba.trans <| h.isBot ⟨c, hc⟩

Premises used: LE.le.trans
-- Module: Mathlib.Order.Grade
Goal:
𝕆 : Type u_1
α : Type u_3
inst : PartialOrder α
s : Flag α
inst_1 : Preorder 𝕆
inst_2 : GradeOrder 𝕆 α
a : ↥s
⊢ grade 𝕆 (↑a : α) = grade 𝕆 a

Tactic:
rfl

Premises used: grade, rfl
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = ⨆ (t : { t : Set α // t ⊆ s ∧ IsChain r t }), (↑t : Set α).encard

Tactic:
rfl

Premises used: Set.chainHeight, rfl
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r ≤ s.encard

Tactic:
simp_all [chainHeight, encard_le_encard]

Premises used: Set.chainHeight, Set.encard_le_encard
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.Finite
⊢ s.chainHeight r ≠ ⊤

Tactic:
LT.lt.ne_top <| lt_of_le_of_lt (chainHeight_le_encard s r) <| lt_top_iff_ne_top.mpr <|
    encard_ne_top_iff.mpr h

Premises used: Iff.mpr, lt_of_le_of_lt, Set.chainHeight_le_encard, LT.lt.ne_top, lt_top_iff_ne_top, Set.encard_ne_top_iff
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
pos : ∀ (h' : n = 0), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
neg : ∀ (h' : ¬n = 0), ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t

Tactic:
by_cases h' : n = 0
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : n = 0
⊢ ∅ ⊆ s ∧ encard.{u_1} (α := α) ∅ = (↑n : ℕ∞) ∧ IsChain r ∅

Tactic:
simp [h']
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : n = 0
⊢ ∃ t ⊆ s, t.encard = (↑n : ℕ∞) ∧ IsChain r t

Tactic:
exact ⟨∅, by simp [h']⟩
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h : (↑n : ℕ∞) ≤ s.chainHeight r
h' : ¬n = 0
contrapose! : ∀ (h : ∀ (t : Set α) (_ : t ⊆ s) (_ : IsChain r t), t.encard < (↑n : ℕ∞)), s.chainHeight r < (↑n : ℕ∞)
⊢ ∃ t ⊆ s, IsChain r t ∧ (↑n : ℕ∞) ≤ t.encard

Tactic:
contrapose! h
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h' : ¬n = 0
h : ∀ (t : Set α) (_ : t ⊆ s) (_ : IsChain r t), t.encard < (↑n : ℕ∞)
⊢ s.chainHeight r < (↑n : ℕ∞)

Tactic:
iSup_lt_iff.mpr ⟨n - 1, ?_, fun m ↦ ENat.le_sub_one_of_lt <| h m.1 m.2.1 m.2.2⟩

Premises used: Set.chainHeight, Iff.mpr, HSub.hSub, Nat.cast, And.right, And.left, ENat.le_sub_one_of_lt, And.intro, Exists.intro, OfNat.ofNat, Subtype.val, iSup_lt_iff, Subtype.property
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h' : ¬n = 0
h : ∀ (t : Set α) (_ : t ⊆ s) (_ : IsChain r t), t.encard < (↑n : ℕ∞)
refine : HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 < (↑n : ℕ∞)
⊢ s.chainHeight r < (↑n : ℕ∞)

Tactic:
refine iSup_lt_iff.mpr ⟨n - 1, ?_, fun m ↦ ENat.le_sub_one_of_lt <| h m.1 m.2.1 m.2.2⟩

Premises used: Iff.mpr, HSub.hSub, And.intro, Exists.intro, OfNat.ofNat, iSup_lt_iff
-- Module: Mathlib.Order.Height
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
n : ℕ
h' : ¬n = 0
h : ∀ (t : Set α) (_ : t ⊆ s) (_ : IsChain r t), t.encard < (↑n : ℕ∞)
⊢ HSub.hSub (α := ℕ∞) (↑n : ℕ∞) 1 < (↑n : ℕ∞)

Tactic:
exact_mod_cast Nat.sub_one_lt h'

Premises used: Nat.sub_one_lt