awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
by_contra! :
  ∀
    (h :
      Fintype.card α ≤
        s.length (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})),
    False
⊢ s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α

Tactic:
by_contra! h
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
rw :
  Fintype.card α <
    s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1
⊢ Fintype.card α <
    Fintype.card
      (Fin
        (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1))

Tactic:
rw [Fintype.card_fin]

Premises used: Fintype.card_fin
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
⊢ Fintype.card α <
    s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
obtain :
  ∀
    (i j :
      Fin
        (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1))
    (hn : i ≠ j)
    (he :
      s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i =
        s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          j),
    False
⊢ False

Tactic:
obtain ⟨i, j, hn, he⟩ := Fintype.exists_ne_map_eq_of_card_lt s (by rw [Fintype.card_fin]; lia)

Premises used: Fintype.exists_ne_map_eq_of_card_lt, RelSeries.toFun
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
i j :
  Fin
    (s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
hn : i ≠ j
he :
  s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      j
inr :
  ∀
    (this :
      ∀
        (i j :
          Fin
            (s.length (r :=
                {x : α × α |
                  match (motive := α × α → Prop) x with
                  | (a, b) => a < b}) +
              1))
        (hn : i ≠ j)
        (he :
          s.toFun (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              i =
            s.toFun (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              j)
        (hl : i < j), False)
    (hl : ¬i < j), False
wlog :
  ∀
    (i j :
      Fin
        (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1))
    (hn : i ≠ j)
    (he :
      s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i =
        s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          j)
    (hl : i < j), False
⊢ False

Tactic:
wlog hl : i < j generalizing i j
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
i j :
  Fin
    (s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
hn : i ≠ j
he :
  s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      j
this :
  ∀
    (i j :
      Fin
        (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1))
    (hn : i ≠ j)
    (he :
      s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i =
        s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          j)
    (hl : i < j), False
hl : ¬i < j
⊢ j < i

Tactic:
lia
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
i j :
  Fin
    (s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
hn : i ≠ j
he :
  s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      j
this :
  ∀
    (i j :
      Fin
        (s.length (r :=
            {x : α × α |
              match (motive := α × α → Prop) x with
              | (a, b) => a < b}) +
          1))
    (hn : i ≠ j)
    (he :
      s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          i =
        s.toFun (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          j)
    (hl : i < j), False
hl : ¬i < j
⊢ False

Tactic:
exact this j i hn.symm he.symm (by lia)

Premises used: Ne.symm, Eq.symm
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
i j :
  Fin
    (s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
hn : i ≠ j
he :
  s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      j
hl : i < j
⊢ False

Tactic:
absurd he (s.strictMono hl).ne

Premises used: LTSeries.strictMono, absurd, LT.lt.ne
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Fintype α
s : LTSeries α
h :
  Fintype.card α ≤
    s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
i j :
  Fin
    (s.length (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b}) +
      1)
hn : i ≠ j
he :
  s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      i =
    s.toFun (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      j
hl : i < j
⊢ False

Tactic:
exact absurd he (s.strictMono hl).ne

Premises used: LTSeries.strictMono, absurd, LT.lt.ne
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
s : LTSeries α
⊢ s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α

Tactic:
have bl := s.length_lt_card
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s_1 : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
s : LTSeries α
bl :
  s.length (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α
obtain :
  ∀ (l : ℕ) (f : Fin (l + 1) → α)
    (mf :
      ∀ (i : Fin l),
        Membership.mem (γ := SetRel α α)
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}
          (f i.castSucc, f i.succ))
    (bl :
      (RelSeries.mk (r :=
              {x : α × α |
                match (motive := α × α → Prop) x with
                | (a, b) => a < b})
              l f mf).length
          (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b}) <
        Fintype.card α),
    Membership.mem (γ := Finset (LTSeries α))
      (Finset.map (α :=
        { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) //
          StrictMono (f.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)) })
        (injStrictMono (Fintype.card α)) Finset.univ)
      (RelSeries.mk (r :=
        {x : α × α |
          match (motive := α × α → Prop) x with
          | (a, b) => a < b})
        l f mf)
⊢ Membership.mem (γ := Finset (LTSeries α))
    (Finset.map (α :=
      { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) //
        StrictMono (f.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)) })
      (injStrictMono (Fintype.card α)) Finset.univ)
    s

Tactic:
obtain ⟨l, f, mf⟩ := s
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf :
  ∀ (i : Fin l),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (f i.castSucc, f i.succ)
bl :
  (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          l f mf).length
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α
simp_rw :
  ∃ (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) (b :
    StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α))),
    (injStrictMono (Fintype.card α) :
          (a : { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono f.snd }) → LTSeries α)
        (Subtype.mk (p := fun (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) ↦
          StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α))) a b) =
      RelSeries.mk (r := {x : α × α | x.1 < x.2}) l f mf
⊢ Membership.mem (γ := Finset (LTSeries α))
    (Finset.map (α :=
      { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) //
        StrictMono (f.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)) })
      (injStrictMono (Fintype.card α)) Finset.univ)
    (RelSeries.mk (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b})
      l f mf)

Tactic:
simp_rw [Finset.mem_map, Finset.mem_univ, true_and, Subtype.exists]

Premises used: Finset.mem_univ, Subtype.exists, Finset.mem_map, true_and
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf :
  ∀ (i : Fin l),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (f i.castSucc, f i.succ)
bl :
  (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          l f mf).length
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α
h :
  (injStrictMono (Fintype.card α) :
        (a : { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono f.snd }) → LTSeries α)
      (Subtype.mk (p := fun (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) ↦
        StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)))
        (Sigma.mk (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α) ⟨l, bl⟩ f) ⋯) =
    RelSeries.mk (r := {x : α × α | x.1 < x.2}) l f mf
⊢ ∃ (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) (b :
    StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α))),
    (injStrictMono (Fintype.card α) :
          (a : { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono f.snd }) → LTSeries α)
        (Subtype.mk (p := fun (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) ↦
          StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α))) a b) =
      RelSeries.mk (r := {x : α × α | x.1 < x.2}) l f mf

Tactic:
use ⟨⟨l, bl⟩, f⟩, Fin.strictMono_iff_lt_succ.mpr mf

Premises used: Iff.mpr, Fin.strictMono_iff_lt_succ
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
r : SetRel α α
β : Type u_2
s : SetRel β β
inst : Preorder α
inst_1 : Preorder β
inst_2 : Fintype α
inst_3 : DecidableLT α
l : ℕ
f : Fin (l + 1) → α
mf :
  ∀ (i : Fin l),
    Membership.mem (γ := SetRel α α)
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}
      (f i.castSucc, f i.succ)
bl :
  (RelSeries.mk (r :=
          {x : α × α |
            match (motive := α × α → Prop) x with
            | (a, b) => a < b})
          l f mf).length
      (r :=
      {x : α × α |
        match (motive := α × α → Prop) x with
        | (a, b) => a < b}) <
    Fintype.card α
⊢ (injStrictMono (Fintype.card α) :
        (a : { f : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α) // StrictMono f.snd }) → LTSeries α)
      (Subtype.mk (p := fun (a : (l : Fin (Fintype.card α)) × (Fin ((↑l : ℕ) + 1) → α)) ↦
        StrictMono (a.snd (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α)))
        (Sigma.mk (β := fun (l : Fin (Fintype.card α)) ↦ Fin ((↑l : ℕ) + 1) → α) ⟨l, bl⟩ f) ⋯) =
    RelSeries.mk (r := {x : α × α | x.1 < x.2}) l f mf

Tactic:
rfl
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ¬FiniteDimensionalOrder α ↔ InfiniteDimensionalOrder α

Tactic:
SetRel.not_finiteDimensional_iff

Premises used: SetRel.not_finiteDimensional_iff
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ ¬InfiniteDimensionalOrder α ↔ FiniteDimensionalOrder α

Tactic:
SetRel.not_infiniteDimensional_iff

Premises used: SetRel.not_infiniteDimensional_iff
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
⊢ FiniteDimensionalOrder α ∨ InfiniteDimensionalOrder α

Tactic:
SetRel.finiteDimensional_or_infiniteDimensional _

Premises used: SetRel.finiteDimensional_or_infiniteDimensional
-- Module: Mathlib.Order.RelSeries
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : StrictMono f
inst_2 : InfiniteDimensionalOrder α
⊢ InfiniteDimensionalOrder β

Tactic:
⟨fun n ↦ ⟨(LTSeries.withLength _ n).map f hf, LTSeries.length_withLength α n⟩⟩

Premises used: SetRel.InfiniteDimensional.mk, LTSeries.length_withLength, LTSeries.withLength, Exists.intro, LTSeries.map
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
a : α
f : (a : α) → π a
i : (↑(Iic a) : Type u_1)
⊢ restrictLe (π := π) a f i = f (↑i : α)

Tactic:
rfl

Premises used: Preorder.restrictLe, Set.restrict, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
a b : α
hab : a ≤ b
f : (i : (↑(Iic b) : Type u_1)) → π (↑i : α)
i : (↑(Iic a) : Type u_1)
⊢ restrictLe₂ (π := π) hab f i = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (↑i : α) ⋯)

Tactic:
rfl

Premises used: Preorder.restrictLe₂, Set.restrict₂, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
a b : α
hab : a ≤ b
⊢ Eq (α := ((a : α) → π a) → (a_2 : (↑(Iic a) : Type u_1)) → π (↑a_2 : α))
    (restrictLe₂ (π := π) hab ∘ restrictLe (π := π) b) (restrictLe (π := π) a)

Tactic:
rfl

Premises used: Preorder.restrictLe₂, Preorder.restrictLe, Set.restrict₂, Set.restrict, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Eq (α := ((a : (↑(Iic c) : Type u_1)) → π (↑a : α)) → (a_2 : (↑(Iic a) : Type u_1)) → π (↑a_2 : α))
    (restrictLe₂ (π := π) hab ∘ restrictLe₂ (π := π) hbc) (restrictLe₂ (π := π) ⋯)

Tactic:
rfl

Premises used: Preorder.restrictLe₂, Set.restrict₂, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
a : α
⊢ DependsOn (α := π) (β := (a_1 : (↑(Iic a) : Type u_1)) → π (↑a_1 : α)) (restrictLe (π := π) a) (Iic a)

Tactic:
(Iic a).dependsOn_restrict

Premises used: Set.dependsOn_restrict, Preorder.restrictLe, Set.Iic
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
a : α
f : (a : α) → π a
i : ↥(Iic a)
⊢ frestrictLe (π := π) a f i = f (↑i : α)

Tactic:
rfl

Premises used: Finset.restrict, Preorder.frestrictLe, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
a b : α
hab : a ≤ b
f : (i : ↥(Iic b)) → π (↑i : α)
i : ↥(Iic a)
⊢ frestrictLe₂ (π := π) hab f i = f (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) (↑i : α) ⋯)

Tactic:
rfl

Premises used: Preorder.frestrictLe₂, Finset.restrict₂, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
a b : α
hab : a ≤ b
⊢ Eq (α := ((i : α) → π i) → (i : ↥(Iic a)) → π (↑i : α)) (frestrictLe₂ (π := π) hab ∘ frestrictLe (π := π) b)
    (frestrictLe (π := π) a)

Tactic:
rfl

Premises used: Finset.restrict, Preorder.frestrictLe₂, Finset.restrict₂, Preorder.frestrictLe, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Eq (α := ((i : ↥(Iic c)) → π (↑i : α)) → (i : ↥(Iic a)) → π (↑i : α))
    (frestrictLe₂ (π := π) hab ∘ frestrictLe₂ (π := π) hbc) (frestrictLe₂ (π := π) ⋯)

Tactic:
rfl

Premises used: Preorder.frestrictLe₂, Finset.restrict₂, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
a : α
⊢ Eq (α := ((a : α) → π a) → (b : ↥(Iic a)) → π (↑b : α))
    (Function.comp (β :=
      (a_1 : (↑(Set.Iic a) : Type u_1)) →
        π (↑((Equiv.symm (Equiv.IicFinsetSet a) : (a_2 : (↑(Set.Iic a) : Type u_1)) → ↥(Iic a)) a_1) : α))
      (⇑(Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(Iic a)) ↦ π (↑i : α))
              (Equiv.symm (Equiv.IicFinsetSet a)) :
            ((a_1 : (↑(Set.Iic a) : Type u_1)) →
                π (↑((Equiv.symm (Equiv.IicFinsetSet a) : (a_2 : (↑(Set.Iic a) : Type u_1)) → ↥(Iic a)) a_1) : α)) ≃
              ((b : ↥(Iic a)) → π (↑b : α))) :
        (a_1 :
            (a_1 : (↑(Set.Iic a) : Type u_1)) →
              π (↑(((Equiv.IicFinsetSet a).symm : (a_2 : (↑(Set.Iic a) : Type u_1)) → ↥(Iic a)) a_1) : α)) →
          (b : ↥(Iic a)) → π (↑b : α))
      (restrictLe (π := π) a))
    (frestrictLe (π := π) a)

Tactic:
rfl

Premises used: Set.Mem, setOf, Finset.restrict, Multiset.Mem, Preorder.restrictLe, Set.Iic, Preorder.frestrictLe, Set.restrict, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
a : α
⊢ Eq (α := ((i : α) → π i) → (b : (↑(Set.Iic a) : Type u_1)) → π (↑b : α))
    (Function.comp (β :=
      (a_1 : ↥(Iic a)) → π (↑((Equiv.IicFinsetSet a : (a_2 : ↥(Iic a)) → (↑(Set.Iic a) : Type u_1)) a_1) : α))
      (⇑(Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (α := ↥(Iic a))
              (fun (i : (↑(Set.Iic a) : Type u_1)) ↦ π (↑i : α)) (Equiv.IicFinsetSet a) :
            ((a_1 : ↥(Iic a)) → π (↑((Equiv.IicFinsetSet a : (a_2 : ↥(Iic a)) → (↑(Set.Iic a) : Type u_1)) a_1) : α)) ≃
              ((b : (↑(Set.Iic a) : Type u_1)) → π (↑b : α))) :
        (a_1 :
            (a_1 : ↥(Iic a)) → π (↑((Equiv.IicFinsetSet a : (a_2 : ↥(Iic a)) → (↑(Set.Iic a) : Type u_1)) a_1) : α)) →
          (b : (↑(Set.Iic a) : Type u_1)) → π (↑b : α))
      (frestrictLe (π := π) a))
    (restrictLe (π := π) a)

Tactic:
rfl

Premises used: Set.Mem, setOf, Finset.restrict, Multiset.Mem, Preorder.restrictLe, Set.Iic, Preorder.frestrictLe, Set.restrict, rfl
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
a b : α
hab : a ≤ b
x : (c : α) → π c
y : (c : ↥(Iic b)) → π (↑c : α)
⊢ frestrictLe (π := π) a (updateFinset (π := π) x (Iic b) y) = frestrictLe₂ (π := π) hab y

Tactic:
restrict_updateFinset_of_subset (Iic_subset_Iic.2 hab) ..

Premises used: Iff.mpr, Finset.Iic_subset_Iic, Function.restrict_updateFinset_of_subset, Preorder.frestrictLe₂, Preorder.frestrictLe
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
a : α
x : (a : α) → π a
y : (b : ↥(Iic a)) → π (↑b : α)
⊢ frestrictLe (π := π) a (updateFinset (π := π) x (Iic a) y) = y

Tactic:
restrict_updateFinset ..

Premises used: Function.restrict_updateFinset, Preorder.frestrictLe
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
a : α
x : (a : α) → π a
⊢ updateFinset (π := π) x (Iic a) (frestrictLe (π := π) a x) = x

Tactic:
simp [frestrictLe]

Premises used: Preorder.frestrictLe
-- Module: Mathlib.Order.Restriction
Goal:
α : Type u_1
inst : Preorder α
π : α → Type u_2
inst_1 : LocallyFiniteOrderBot α
a : α
⊢ DependsOn (α := π) (β := (i : ↥(Iic a)) → π (↑i : α)) (frestrictLe (π := π) a) (Set.Iic a)

Tactic:
coe_Iic a ▸ (Finset.Iic a).dependsOn_restrict

Premises used: Finset.coe_Iic, Eq.rec, Finset.dependsOn_restrict, Finset.Iic
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
rw : ∀ (i : F) (j : i ∈ Y), LE.le.{u_3} (α := β) (⨅ x ∈ X, f x i) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)
⊢ LE.le.{u_3} (α := β) (⨆ y ∈ Y, ⨅ x ∈ X, f x y) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)

Tactic:
rw [iSup₂_le_iff]

Premises used: iSup₂_le_iff
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
y : F
hy : y ∈ Y
rw : ∀ (i : E) (j : i ∈ X), LE.le.{u_3} (α := β) (⨅ x ∈ X, f x y) (⨆ y ∈ Y, f i y)
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, f x y) (⨅ x ∈ X, ⨆ y ∈ Y, f x y)

Tactic:
rw [le_iInf₂_iff]

Premises used: le_iInf₂_iff
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, f x y) (⨆ y ∈ Y, f x y)

Tactic:
iInf₂_le_of_le x hx (le_iSup₂_of_le y hy (le_refl _))

Premises used: le_refl, iInf₂_le_of_le, le_iSup₂_of_le
-- Module: Mathlib.Order.SaddlePoint
Goal:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst : CompleteLinearOrder β
y : F
hy : y ∈ Y
x : E
hx : x ∈ X
⊢ LE.le.{u_3} (α := β) (⨅ x ∈ X, f x y) (⨆ y ∈ Y, f x y)

Tactic:
exact iInf₂_le_of_le x hx (le_iSup₂_of_le y hy (le_refl _))

Premises used: iInf₂_le_of_le, le_iSup₂_of_le