awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
j : ℕ
hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
⊢ (e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩ < (⟨i, hi⟩ : Fin n)

Tactic:
have := e.symm.lt_symm_apply.1 (mk_lt_of_lt_val hj)
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
j : ℕ
hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
this : (e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩ < (⟨i, hi⟩ : Fin n)
⊢ (↑((e : (a : Fin n) → Fin m) (⟨(↑((e.symm : (a : Fin m) → Fin n) (⟨j, ⋯⟩ : Fin m)) : ℕ), ⋯⟩ : Fin n)) : ℕ) =
    (↑((e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩) : ℕ)

Tactic:
specialize h _ this (e.symm _).is_lt

Premises used: Fin.is_lt, OrderIso.symm, DFunLike.coe
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
j : ℕ
hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
this : (e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩ < (⟨i, hi⟩ : Fin n)
h :
  (↑((e : (a : Fin n) → Fin m) (⟨(↑((e.symm : (a : Fin m) → Fin n) (⟨j, ⋯⟩ : Fin m)) : ℕ), ⋯⟩ : Fin n)) : ℕ) =
    (↑((e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩) : ℕ)
⊢ j = (↑((e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩) : ℕ)

Tactic:
simp only [Fin.eta, OrderIso.apply_symm_apply] at h

Premises used: OrderIso.apply_symm_apply, Fin.eta
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
j : ℕ
hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
this : (e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩ < (⟨i, hi⟩ : Fin n)
h : j = (↑((e.symm : (a : Fin m) → Fin n) ⟨j, ⋯⟩) : ℕ)
h₁ h₂ h₃ h₄ : (↑((e.symm : (a : Fin m) → Fin n) (⟨j, ⋯⟩ : Fin m)) : ℕ) < i
⊢ j < i

Tactic:
rwa [h]
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
h : ∀ (m_1 : ℕ), m_1 < i → ∀ (hi : m_1 < n), (↑((e : (a : Fin n) → Fin m) (⟨m_1, hi⟩ : Fin n)) : ℕ) = m_1
hi : i < n
j : ℕ
hj : j < i
h₁ : (↑((e : (a : Fin n) → Fin m) (⟨j, ⋯⟩ : Fin n)) : ℕ) < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
h₂ : LT.lt (α := Fin m) ((e : (a : Fin n) → Fin m) ⟨j, ⋯⟩ : Fin m) ((e : (a : Fin n) → Fin m) ⟨i, hi⟩ : Fin m)
h₃ h₄ h₅ h₆ : (⟨j, ⋯⟩ : Fin n) < ⟨i, hi⟩
⊢ j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)

Tactic:
rwa [← h j hj (hj.trans hi), ← lt_def, e.lt_iff_lt]

Premises used: OrderIso.lt_iff_lt, Fin.lt_def, LT.lt.trans
-- Module: Mathlib.Order.Fin.Clamp
Goal:
m a b : ℕ
h : a ≤ b
⊢ (↑((fun (n : ℕ) ↦ clamp n m) a) : ℕ) ≤ (↑((fun (n : ℕ) ↦ clamp n m) b) : ℕ)

Tactic:
min_le_min_right m h

Premises used: min_le_min_right
-- Module: Mathlib.Order.Fin.Clamp
Goal:
m a b : ℕ
h : a ≤ b
⊢ (↑((fun (n : ℕ) ↦ clamp n m) a) : ℕ) ≤ (↑((fun (n : ℕ) ↦ clamp n m) b) : ℕ)

Tactic:
exact min_le_min_right m h

Premises used: min_le_min_right
-- Module: Mathlib.Order.Fin.Clamp
Goal:
n m : ℕ
hmn : m ≤ n
h : (↑(clamp n m) : ℕ) = (↑(last m) : ℕ)
⊢ clamp n m = last m

Tactic:
ext
-- Module: Mathlib.Order.Fin.Clamp
Goal:
n m : ℕ
hmn : m ≤ n
⊢ (↑(clamp n m) : ℕ) = (↑(last m) : ℕ)

Tactic:
simpa
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
a : α
i : Fin 1
⊢ (↑((orderIsoSingleton a : (a_1 : Fin 1) → ↥{a}) i) : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
⊢ Membership.mem (γ := Finset α) {a, b} a

Tactic:
simp
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
⊢ Membership.mem (γ := Finset α) {a, b} b

Tactic:
simp
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
x_1 : ↥{a, b}
x : α
hx : Membership.mem (γ := Finset α) {a, b} x
⊢ x = a ∨ x = b

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
x_1 : ↥{a, b}
x : α
hx_1 : Membership.mem (γ := Finset α) {a, b} x
hx : x = a ∨ x = b
inl :
  ∀ (hab : x < b) (x_2 : ↥{x, b}) (hx : Membership.mem (γ := Finset α) {x, b} x),
    ∃ (a : Fin 2),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) x ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) b ⋯]
          a =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_3) x hx
inr :
  ∀ (hab : a < x) (x_2 : ↥{a, x}) (hx : Membership.mem (γ := Finset α) {a, x} x),
    ∃ (a_1 : Fin 2),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_3) a ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_3) x ⋯]
          a_1 =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_3) x hx
⊢ ∃ (a_1 : Fin 2),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) b ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b} x) x hx_1

Tactic:
obtain rfl | rfl := hx

Premises used: rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
b x : α
hab : x < b
x_1 : ↥{x, b}
hx : Membership.mem (γ := Finset α) {x, b} x
⊢ ∃ (a : Fin 2),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_2) x ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_2) b ⋯]
        a =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_2) x hx

Tactic:
⟨0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
b x : α
hab : x < b
x_1 : ↥{x, b}
hx : Membership.mem (γ := Finset α) {x, b} x
⊢ ∃ (a : Fin 2),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_2) x ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_2) b ⋯]
        a =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b} x_2) x hx

Tactic:
exact ⟨0, rfl⟩
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a x : α
hab : a < x
x_1 : ↥{a, x}
hx : Membership.mem (γ := Finset α) {a, x} x
⊢ ∃ (a_1 : Fin 2),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_2) a ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_2) x ⋯]
        a_1 =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_2) x hx

Tactic:
⟨1, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a x : α
hab : a < x
x_1 : ↥{a, x}
hx : Membership.mem (γ := Finset α) {a, x} x
⊢ ∃ (a_1 : Fin 2),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_2) a ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_2) x ⋯]
        a_1 =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x} x_2) x hx

Tactic:
exact ⟨1, rfl⟩
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
⊢ (↑((orderIsoPair a b hab : (a_1 : Fin 2) → ↥{a, b}) 0) : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
⊢ (↑((orderIsoPair a b hab : (a_1 : Fin 2) → ↥{a, b}) 1) : α) = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ Membership.mem (γ := Finset α) {a, b, c} a

Tactic:
simp
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ Membership.mem (γ := Finset α) {a, b, c} b

Tactic:
simp
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ Membership.mem (γ := Finset α) {a, b, c} c

Tactic:
simp
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x_1 : ↥{a, b, c}
x : α
hx : Membership.mem (γ := Finset α) {a, b, c} x
⊢ x = a ∨ x = b ∨ x = c

Tactic:
simp only [Finset.mem_insert, Finset.mem_singleton] at hx

Premises used: Finset.mem_singleton, Finset.mem_insert
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
x_1 : ↥{a, b, c}
x : α
hx_1 : Membership.mem (γ := Finset α) {a, b, c} x
hx : x = a ∨ x = b ∨ x = c
inl :
  ∀ (hab : x < b) (x_2 : ↥{x, b, c}) (hx : Membership.mem (γ := Finset α) {x, b, c} x),
    ∃ (a : Fin 3),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) x ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) b ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) c ⋯]
          a =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_3) x hx
inr :
  ∀ (hab : a < x) (hbc : x < c) (x_2 : ↥{a, x, c}) (hx : Membership.mem (γ := Finset α) {a, x, c} x),
    ∃ (a_1 : Fin 3),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) a ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) x ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) c ⋯]
          a_1 =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_3) x hx
inr₁ :
  ∀ (hbc : b < x) (x_2 : ↥{a, b, x}) (hx : Membership.mem (γ := Finset α) {a, b, x} x),
    ∃ (a_1 : Fin 3),
      ![Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_3) a ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_3) b ⋯,
            Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_3) x ⋯]
          a_1 =
        Subtype.mk (p := fun (x_3 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_3) x hx
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) a ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) b ⋯,
          Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) c ⋯]
        a_1 =
      Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := Finset α) {a, b, c} x) x hx_1

Tactic:
obtain rfl | rfl | rfl := hx

Premises used: rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
b c : α
hbc : b < c
x : α
hab : x < b
x_1 : ↥{x, b, c}
hx : Membership.mem (γ := Finset α) {x, b, c} x
⊢ ∃ (a : Fin 3),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_2) x ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_2) b ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_2) c ⋯]
        a =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_2) x hx

Tactic:
⟨0, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
b c : α
hbc : b < c
x : α
hab : x < b
x_1 : ↥{x, b, c}
hx : Membership.mem (γ := Finset α) {x, b, c} x
⊢ ∃ (a : Fin 3),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_2) x ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_2) b ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_2) c ⋯]
        a =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {x, b, c} x_2) x hx

Tactic:
exact ⟨0, rfl⟩
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a c x : α
hab : a < x
hbc : x < c
x_1 : ↥{a, x, c}
hx : Membership.mem (γ := Finset α) {a, x, c} x
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_2) a ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_2) x ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_2) c ⋯]
        a_1 =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_2) x hx

Tactic:
⟨1, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a c x : α
hab : a < x
hbc : x < c
x_1 : ↥{a, x, c}
hx : Membership.mem (γ := Finset α) {a, x, c} x
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_2) a ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_2) x ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_2) c ⋯]
        a_1 =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, x, c} x_2) x hx

Tactic:
exact ⟨1, rfl⟩
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
x : α
hbc : b < x
x_1 : ↥{a, b, x}
hx : Membership.mem (γ := Finset α) {a, b, x} x
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_2) a ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_2) b ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_2) x ⋯]
        a_1 =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_2) x hx

Tactic:
⟨2, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b : α
hab : a < b
x : α
hbc : b < x
x_1 : ↥{a, b, x}
hx : Membership.mem (γ := Finset α) {a, b, x} x
⊢ ∃ (a_1 : Fin 3),
    ![Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_2) a ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_2) b ⋯,
          Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_2) x ⋯]
        a_1 =
      Subtype.mk (p := fun (x_2 : α) ↦ Membership.mem (γ := Finset α) {a, b, x} x_2) x hx

Tactic:
exact ⟨2, rfl⟩
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ (↑((orderIsoTriple a b c hab hbc : (a_1 : Fin 3) → ↥{a, b, c}) 0) : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ (↑((orderIsoTriple a b c hab hbc : (a_1 : Fin 3) → ↥{a, b, c}) 1) : α) = b

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Finset
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DecidableEq α
a b c : α
hab : a < b
hbc : b < c
⊢ (↑((orderIsoTriple a b c hab hbc : (a_1 : Fin 3) → ↥{a, b, c}) 2) : α) = c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
i : Fin (n + 2)
a : Fin (n + 1)
⊢ Membership.mem (α := Fin (n + 2)) (γ := Finset (Fin (n + 2))) {i}ᶜ
    ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a : Fin (n + 1 + 1))

Tactic:
simp
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
i : Fin (n + 2)
left :
  Function.Injective (β := ↥{i}ᶜ) fun (a : Fin (n + 1)) ↦
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
      ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯
right :
  Function.Surjective (β := ↥{i}ᶜ) fun (a : Fin (n + 1)) ↦
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
      ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯
⊢ Function.Bijective (β := ↥{i}ᶜ) fun (a : Fin (n + 1)) ↦
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
      ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯

Tactic:
constructor
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
h :
  Eq (α := ↥{i}ᶜ)
    ((fun (a : Fin (n + 1)) ↦
        (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
            ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
          ↥{i}ᶜ))
      a)
    ((fun (a : Fin (n + 1)) ↦
        (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
            ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
          ↥{i}ᶜ))
      b)
⊢ Eq (α := Fin (n + 1 + 1)) ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a : Fin (n + 1 + 1))
    ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) b : Fin (n + 1 + 1))

Tactic:
simpa using h
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
h :
  Eq (α := ↥{i}ᶜ)
    ((fun (a : Fin (n + 1)) ↦
        (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
            ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
          ↥{i}ᶜ))
      a)
    ((fun (a : Fin (n + 1)) ↦
        (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
            ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
          ↥{i}ᶜ))
      b)
⊢ a = b

Tactic:
exact (Fin.succAboveOrderEmb i).injective (by simpa using h)

Premises used: RelEmbedding.injective, Fin.succAboveOrderEmb
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
i j : Fin (n + 2)
hj : Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ j
⊢ ¬j = i

Tactic:
simp only [mem_compl, mem_singleton] at hj

Premises used: Finset.mem_singleton, Finset.mem_compl
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
i j : Fin (n + 2)
hj_1 : Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ j
hj : ¬j = i
right :
  ∀ (hj : Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ j) (hj_2 : ¬j = 0),
    ∃ (a : Fin (n + 1)),
      (fun (a : Fin (n + 1)) ↦
            (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x)
                ((succAboveOrderEmb 0 : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
              ↥{0}ᶜ))
          a =
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x) j hj
right₁ :
  ∀ (i : Fin (n + 1)) (hj : Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ j) (hj_2 : ¬j = i.succ),
    ∃ (a : Fin (n + 1)),
      (fun (a : Fin (n + 1)) ↦
            (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ x)
                ((i.succ.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
              ↥{i.succ}ᶜ))
          a =
        Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ x) j hj
⊢ ∃ (a : Fin (n + 1)),
    (fun (a : Fin (n + 1)) ↦
          (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
              ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
            ↥{i}ᶜ))
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x) j hj_1

Tactic:
obtain rfl | ⟨i, rfl⟩ := Fin.eq_zero_or_eq_succ i

Premises used: Fin.eq_zero_or_eq_succ, rfl
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
j : Fin (n + 2)
hj_1 : Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ j
hj : ¬j = 0
⊢ (fun (a : Fin (n + 1)) ↦
        (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x)
            ((succAboveOrderEmb 0 : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
          ↥{0}ᶜ))
      (j.pred hj) =
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x) j hj_1

Tactic:
simp
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
j : Fin (n + 2)
hj_1 : Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ j
hj : ¬j = 0
⊢ ∃ (a : Fin (n + 1)),
    (fun (a : Fin (n + 1)) ↦
          (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x)
              ((succAboveOrderEmb 0 : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
            ↥{0}ᶜ))
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {0}ᶜ x) j hj_1

Tactic:
exact ⟨j.pred hj, by simp⟩
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj_1 : Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ j
hj : ¬j = i.succ
⊢ (fun (a : Fin (n + 1)) ↦
        (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ x)
            ((i.succ.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
          ↥{i.succ}ᶜ))
      (i.predAbove j) =
    Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ x) j hj_1

Tactic:
aesop
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj_1 : Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ j
hj : ¬j = i.succ
⊢ ∃ (a : Fin (n + 1)),
    (fun (a : Fin (n + 1)) ↦
          (Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ x)
              ((i.succ.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯ :
            ↥{i.succ}ᶜ))
        a =
      Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i.succ}ᶜ x) j hj_1

Tactic:
exact ⟨i.predAbove j, by aesop⟩
-- Module: Mathlib.Order.Fin.SuccAboveOrderIso
Goal:
n : ℕ
i : Fin (n + 2)
a b : Fin (n + 1)
⊢ LE.le (α := ↥{i}ᶜ)
      ((Equiv.ofBijective
              (fun (a : Fin (n + 1)) ↦
                Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
                  ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯)
              ⋯ :
            (a : Fin (n + 1)) → ↥{i}ᶜ)
          a :
        ↥{i}ᶜ)
      ((Equiv.ofBijective
              (fun (a : Fin (n + 1)) ↦
                Subtype.mk (p := fun (x : Fin (n + 2)) ↦ Membership.mem (γ := Finset (Fin (n + 2))) {i}ᶜ x)
                  ((i.succAboveOrderEmb : (a : Fin (n + 1)) → Fin (n + 1 + 1)) a) ⋯)
              ⋯ :
            (a : Fin (n + 1)) → ↥{i}ᶜ)
          b :
        ↥{i}ᶜ) ↔
    a ≤ b

Tactic:
simp only [Equiv.ofBijective_apply, Subtype.mk_le_mk, OrderEmbedding.le_iff_le]

Premises used: Equiv.ofBijective_apply, OrderEmbedding.le_iff_le, Subtype.mk_le_mk
-- Module: Mathlib.Order.Fin.Tuple
Goal:
n : ℕ
α : Fin (n + 1) → Type u_1
x₀ y₀ : α 0
x y : (i : Fin n) → α i.succ
s : {i : Fin n.succ} → α i → α i → Prop
simp_rw :
  (((LT.lt (α := Fin n.succ) 0 0 → Eq (α := α 0) (cons (α := α) x₀ x 0) (cons (α := α) y₀ y 0)) ∧
          ∀ (i : Fin n), i.succ < 0 → Eq (α := α i.succ) (cons (α := α) x₀ x i.succ) (cons (α := α) y₀ y i.succ)) ∧
        s x₀ y₀ ∨
      ∃ (i : Fin n),
        ((0 < i.succ → Eq (α := α 0) (cons (α := α) x₀ x 0) (cons (α := α) y₀ y 0)) ∧
            ∀ (i_1 : Fin n),
              i_1.succ < i.succ → Eq (α := α i_1.succ) (cons (α := α) x₀ x i_1.succ) (cons (α := α) y₀ y i_1.succ)) ∧
          s (x i) (y i)) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ ∃ (i : Fin n), (∀ (j : Fin n), j < i → x j = y j) ∧ s (x i) (y i)
⊢ Pi.Lex (β := α) (fun (x1 x2 : Fin n.succ) ↦ x1 < x2) (@s) (cons (α := α) x₀ x) (cons (α := α) y₀ y) ↔
    s x₀ y₀ ∨
      x₀ = y₀ ∧ Pi.Lex (β := fun (i : Fin n) ↦ α i.succ) (fun (x1 x2 : Fin n) ↦ x1 < x2) (fun (i : Fin n) ↦ s) x y

Tactic:
simp_rw [Pi.Lex, Fin.exists_fin_succ, Fin.cons_succ, Fin.cons_zero, Fin.forall_iff_succ]

Premises used: Fin.cons_succ, Pi.Lex, Fin.forall_iff_succ, Fin.exists_fin_succ, Fin.cons_zero