awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin (n + 1)) (succ (rev 0)) ⊤
rw₁ : Eq (α := Fin (n + 1)) (succ (rev 0)) (rev 0)
rw₂ : Eq (α := Fin (n + 1)) (rev (castSucc 0)) (rev 0)
rw₃ rw₄ : Eq (α := Fin (n + 1)) (rev 0) (rev 0)
⊢ Eq (α := Fin (n + 1)) (succ ⊤) ⊤

Tactic:
rw [← rev_zero_eq_top, ← rev_zero_eq_top, ← rev_castSucc, castSucc_zero']

Premises used: Fin.castSucc_zero', Fin.rev_zero_eq_top, Fin.rev_castSucc
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ (↑⊤ : ℕ) = n - 1

Tactic:
rfl

Premises used: Nat.mod, rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
rw : Eq (α := Fin n) ⊥ ⊤ ↔ n = 1
rw₁ : Subsingleton (Fin n) ↔ n = 1
rw₂ : n ≤ 1 ↔ n = 1
rw₃ : n = 0 ∨ n = 1 ↔ n = 1
rw₄ rw₅ : n = 1 ↔ n = 1
⊢ Eq (α := Fin n) 0 ⊤ ↔ n = 1

Tactic:
rw [← bot_eq_zero, subsingleton_iff_bot_eq_top, subsingleton_iff_le_one,
    le_one_iff_eq_zero_or_eq_one, or_iff_right (NeZero.ne n)]

Premises used: Nat.le_one_iff_eq_zero_or_eq_one, Fin.subsingleton_iff_le_one, or_iff_right, subsingleton_iff_bot_eq_top, bot_eq_zero, NeZero.ne
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) ⊤ 0 ↔ n = 1

Tactic:
eq_comm.trans zero_eq_top

Premises used: eq_comm, Iff.trans, Fin.zero_eq_top
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
inst : NeZero m
inst_1 : NeZero n
h : m = n
⊢ Fin.cast h ⊤ = ⊤

Tactic:
simp [← val_inj, h]

Premises used: Fin.val_inj
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
α : Type u_1
inst : Preorder α
f : α → Fin (n + 1)
hf : ∀ (a : α), f a ≠ 0
hf₂ : StrictMono f
⊢ StrictMono (β := Fin n) fun (a : α) ↦ (f a).pred ⋯

Tactic:
fun _ _ h => pred_lt_pred_iff.2 (hf₂ h)

Premises used: Iff.mpr, StrictMono, Fin.pred_lt_pred_iff
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
α : Type u_1
inst : Preorder α
f : α → Fin (n + 1)
hf : ∀ (a : α), f a ≠ 0
hf₂ : Monotone f
⊢ Monotone (β := Fin n) fun (a : α) ↦ (f a).pred ⋯

Tactic:
fun _ _ h => pred_le_pred_iff.2 (hf₂ h)

Premises used: Iff.mpr, Monotone, Fin.pred_le_pred_iff
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
α : Type u_1
inst : Preorder α
f : α → Fin (n + 1)
hf : ∀ (a : α), f a ≠ last n
hf₂ : StrictMono f
⊢ StrictMono (β := Fin n) fun (a : α) ↦ (f a).castPred ⋯

Tactic:
fun _ _ h => castPred_lt_castPred_iff.2 (hf₂ h)

Premises used: Iff.mpr, StrictMono, Fin.castPred_lt_castPred_iff
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
α : Type u_1
inst : Preorder α
f : α → Fin (n + 1)
hf : ∀ (a : α), f a ≠ last n
hf₂ : Monotone f
⊢ Monotone (β := Fin n) fun (a : α) ↦ (f a).castPred ⋯

Tactic:
fun _ _ h => castPred_le_castPred_iff.2 (hf₂ h)

Premises used: Iff.mpr, Monotone, Fin.castPred_le_castPred_iff
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
α : Type u_1
inst : Preorder α
f : Fin (n + 1) → α
⊢ StrictMono f ↔ ∀ (i : Fin n), f i.castSucc < f i.succ

Tactic:
liftFun_iff_succ (· < ·)

Premises used: Fin.liftFun_iff_succ, StrictMono, LT.lt
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
α : Type u_1
inst : Preorder α
f : Fin (n + 1) → α
⊢ Monotone f ↔ ∀ (i : Fin n), f i.castSucc ≤ f i.succ

Tactic:
monotone_iff_forall_lt.trans <| liftFun_iff_succ (· ≤ ·)

Premises used: Fin.liftFun_iff_succ, LE.le, Iff.trans, monotone_iff_forall_lt
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
α : Type u_1
inst : Preorder α
f : Fin (n + 1) → α
⊢ StrictAnti f ↔ ∀ (i : Fin n), f i.succ < f i.castSucc

Tactic:
liftFun_iff_succ (· > ·)

Premises used: Fin.liftFun_iff_succ, GT.gt, StrictAnti
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
α : Type u_1
inst : Preorder α
f : Fin (n + 1) → α
⊢ Antitone f ↔ ∀ (i : Fin n), f i.succ ≤ f i.castSucc

Tactic:
antitone_iff_forall_lt.trans <| liftFun_iff_succ (· ≥ ·)

Premises used: Fin.liftFun_iff_succ, GE.ge, Iff.trans, antitone_iff_forall_lt
-- Module: Mathlib.Order.Fin.Basic
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
mp :
  Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α) →
    ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
mpr :
  (∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)) →
    Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α)
⊢ Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α) ↔
    ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)

Tactic:
constructor
-- Module: Mathlib.Order.Fin.Basic
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α)
i : Fin n
hi : Eq (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
⊢ i.castSucc = i.succ

Tactic:
have := hf hi
-- Module: Mathlib.Order.Fin.Basic
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α)
i : Fin n
hi : Eq (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
this : i.castSucc = i.succ
⊢ False

Tactic:
simp [Fin.ext_iff] at this

Premises used: Fin.ext_iff
-- Module: Mathlib.Order.Fin.Basic
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
⊢ Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α)

Tactic:
(strictMono_iff_lt_succ (f := f).2 fun i ↦ ?_).injective

Premises used: Iff.mpr, Fin.strictMono_iff_lt_succ, StrictMono.injective
-- Module: Mathlib.Order.Fin.Basic
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
mpr :
  ∀ (i : Fin n), LT.lt (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
⊢ Injective (α := Fin (n + 1)) (β := α) (⇑f : (a : Fin (n + 1)) → α)

Tactic:
refine (strictMono_iff_lt_succ (f := f).2 fun i ↦ ?_).injective

Premises used: Iff.mpr, Fin.strictMono_iff_lt_succ, StrictMono.injective
-- Module: Mathlib.Order.Fin.Basic
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
i : Fin n
⊢ LT.lt (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)

Tactic:
lt_of_le_of_ne (f.monotone (Fin.castSucc_le_succ i)) (hf i)

Premises used: Fin.castSucc_le_succ, OrderHom.monotone, lt_of_le_of_ne
-- Module: Mathlib.Order.Fin.Basic
Goal:
α : Type u_2
inst : PartialOrder α
n : ℕ
f : Fin (n + 1) →o α
hf : ∀ (i : Fin n), Ne (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)
i : Fin n
⊢ LT.lt (α := α) ((f : (a : Fin (n + 1)) → α) i.castSucc : α) ((f : (a : Fin (n + 1)) → α) i.succ : α)

Tactic:
exact lt_of_le_of_ne (f.monotone (Fin.castSucc_le_succ i)) (hf i)

Premises used: Fin.castSucc_le_succ, OrderHom.monotone, lt_of_le_of_ne
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ StrictMono (α := Fin n) val

Tactic:
fun _ _ ↦ id

Premises used: StrictMono, id
-- Module: Mathlib.Order.Fin.Basic
Goal:
k l : ℕ
h : k = l
⊢ StrictMono (Fin.cast h)

Tactic:
fun {_ _} h ↦ h

Premises used: StrictMono
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ StrictMono (α := Fin n) succ

Tactic:
fun _ _ ↦ succ_lt_succ

Premises used: StrictMono, Nat.succ_lt_succ
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
h : n ≤ m
⊢ StrictMono (castLE h)

Tactic:
fun _ _ ↦ id

Premises used: StrictMono, id
-- Module: Mathlib.Order.Fin.Basic
Goal:
n m : ℕ
⊢ StrictMono (α := Fin n) (castAdd m)

Tactic:
strictMono_castLE _

Premises used: Fin.strictMono_castLE
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ StrictMono (α := Fin n) castSucc

Tactic:
strictMono_castAdd _

Premises used: Fin.strictMono_castAdd
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
⊢ StrictMono (α := Fin m) (natAdd n)

Tactic:
fun i j h ↦ Nat.add_lt_add_left (show i.val < j.val from h) _

Premises used: StrictMono, Nat.add_lt_add_left
-- Module: Mathlib.Order.Fin.Basic
Goal:
n m : ℕ
⊢ StrictMono (β := Fin (n + m)) fun (x : Fin n) ↦ x.addNat m

Tactic:
fun i j h ↦ Nat.add_lt_add_right (show i.val < j.val from h) _

Premises used: StrictMono, Nat.add_lt_add_right
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin (n + 1)
⊢ StrictMono p.succAbove

Tactic:
strictMono_castSucc.ite strictMono_succ
    (fun _ _ hij hj => (castSucc_lt_castSucc_iff.mpr hij).trans hj) fun _ => castSucc_lt_succ.le

Premises used: Iff.mpr, Fin.succAbove, Fin.castSucc_lt_castSucc_iff, StrictMono.ite, Fin.castSucc_lt_succ, LT.lt.le, Fin.strictMono_succ, Fin.strictMono_castSucc, LT.lt.trans
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
⊢ p.succAbove i = p.succAbove j ↔ i = j

Tactic:
(strictMono_succAbove p).injective.eq_iff

Premises used: Fin.strictMono_succAbove, Function.Injective.eq_iff, StrictMono.injective
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
⊢ p.succAbove i ≤ p.succAbove j ↔ i ≤ j

Tactic:
(strictMono_succAbove p).le_iff_le

Premises used: Fin.strictMono_succAbove, StrictMono.le_iff_le
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
⊢ p.succAbove i < p.succAbove j ↔ i < j

Tactic:
(strictMono_succAbove p).lt_iff_lt

Premises used: Fin.strictMono_succAbove, StrictMono.lt_iff_lt
-- Module: Mathlib.Order.Fin.Basic
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m i = natAdd m j ↔ i = j

Tactic:
(strictMono_natAdd _).injective.eq_iff

Premises used: Function.Injective.eq_iff, StrictMono.injective, Fin.strictMono_natAdd
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
⊢ Injective (α := Fin m) (natAdd n)

Tactic:
(strictMono_natAdd _).injective

Premises used: StrictMono.injective, Fin.strictMono_natAdd
-- Module: Mathlib.Order.Fin.Basic
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m i ≤ natAdd m j ↔ i ≤ j

Tactic:
(strictMono_natAdd _).le_iff_le

Premises used: StrictMono.le_iff_le, Fin.strictMono_natAdd
-- Module: Mathlib.Order.Fin.Basic
Goal:
n m : ℕ
i j : Fin n
⊢ natAdd m i < natAdd m j ↔ i < j

Tactic:
(strictMono_natAdd _).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Fin.strictMono_natAdd
-- Module: Mathlib.Order.Fin.Basic
Goal:
n m : ℕ
i j : Fin n
⊢ i.addNat m = j.addNat m ↔ i = j

Tactic:
(strictMono_addNat _).injective.eq_iff

Premises used: Function.Injective.eq_iff, Fin.strictMono_addNat, StrictMono.injective
-- Module: Mathlib.Order.Fin.Basic
Goal:
n m : ℕ
i j : Fin n
⊢ i.addNat m ≤ j.addNat m ↔ i ≤ j

Tactic:
(strictMono_addNat _).le_iff_le

Premises used: Fin.strictMono_addNat, StrictMono.le_iff_le
-- Module: Mathlib.Order.Fin.Basic
Goal:
n m : ℕ
i j : Fin n
⊢ i.addNat m < j.addNat m ↔ i < j

Tactic:
(strictMono_addNat _).lt_iff_lt

Premises used: StrictMono.lt_iff_lt, Fin.strictMono_addNat
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
i j : Fin n
h : n ≤ m
⊢ castLE h i ≤ castLE h j ↔ i ≤ j

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
i j : Fin n
h : n ≤ m
⊢ castLE h i < castLE h j ↔ i < j

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
pos : ∀ (ha : p.castSucc < a) (hb : p.castSucc < b), a.pred ⋯ ≤ b.pred ⋯
neg : ∀ (ha : p.castSucc < a) (hb : ¬p.castSucc < b), a.pred ⋯ ≤ b.castPred ⋯
pos₁ : ∀ (ha : ¬p.castSucc < a) (hb : p.castSucc < b), a.castPred ⋯ ≤ b.pred ⋯
neg₁ : ∀ (ha : ¬p.castSucc < a) (hb : ¬p.castSucc < b), a.castPred ⋯ ≤ b.castPred ⋯
⊢ LE.le (α := Fin n) (if h : p.castSucc < a then a.pred ⋯ else a.castPred ⋯)
    (if h : p.castSucc < b then b.pred ⋯ else b.castPred ⋯)

Tactic:
split_ifs with ha hb hb
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ (↑a : ℕ) - 1 ≤ (↑b : ℕ) - 1

Tactic:
pred_le_pred H

Premises used: Nat.pred_le_pred, Nat.pred
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : p.castSucc < b
⊢ (↑a : ℕ) - 1 ≤ (↑b : ℕ) - 1

Tactic:
exact pred_le_pred H

Premises used: Nat.pred_le_pred
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ (↑a : ℕ).pred ≤ (↑a : ℕ)

Tactic:
Nat.pred_le _

Premises used: Nat.pred_le
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ (↑a : ℕ) ≤ (↑b : ℕ)

Tactic:
H
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : p.castSucc < a
hb : ¬p.castSucc < b
⊢ (↑a : ℕ) - 1 ≤ (↑(b.castPred ⋯) : ℕ)

Tactic:
calc
      _ ≤ _ := Nat.pred_le _
      _ ≤ _ := H

Premises used: Nat.pred_le
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ (↑(a.castPred ⋯) : ℕ) ≤ (↑b : ℕ) - 1

Tactic:
le_pred_of_lt ((not_lt.mp ha).trans_lt hb)

Premises used: Nat.le_pred_of_lt, not_lt, Iff.mp, LE.le.trans_lt, Nat.pred
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : p.castSucc < b
⊢ (↑(a.castPred ⋯) : ℕ) ≤ (↑b : ℕ) - 1

Tactic:
exact le_pred_of_lt ((not_lt.mp ha).trans_lt hb)

Premises used: Nat.le_pred_of_lt, not_lt, Iff.mp, LE.le.trans_lt
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ (↑(a.castPred ⋯) : ℕ) ≤ (↑(b.castPred ⋯) : ℕ)

Tactic:
H
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p : Fin n
a b : Fin (n + 1)
H : a ≤ b
ha : ¬p.castSucc < a
hb : ¬p.castSucc < b
⊢ (↑(a.castPred ⋯) : ℕ) ≤ (↑(b.castPred ⋯) : ℕ)

Tactic:
exact H
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
pos : ∀ (ha : a.castSucc < i) (hb : b.castSucc < i), i.pred ⋯ ≤ i.pred ⋯
neg : ∀ (ha : a.castSucc < i) (hb : ¬b.castSucc < i), i.pred ⋯ ≤ i.castPred ⋯
pos₁ : ∀ (ha : ¬a.castSucc < i) (hb : b.castSucc < i), i.castPred ⋯ ≤ i.pred ⋯
neg₁ : ∀ (ha : ¬a.castSucc < i) (hb : ¬b.castSucc < i), i.castPred ⋯ ≤ i.castPred ⋯
⊢ LE.le (α := Fin n) (if h : a.castSucc < i then i.pred ⋯ else i.castPred ⋯)
    (if h : b.castSucc < i then i.pred ⋯ else i.castPred ⋯)

Tactic:
split_ifs with ha hb hb
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : b.castSucc < i
⊢ i.pred ⋯ ≤ i.pred ⋯

Tactic:
rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

Tactic:
pred_le _

Premises used: Nat.pred_le, Nat.pred
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.pred ⋯ ≤ i.castPred ⋯

Tactic:
exact pred_le _

Premises used: Nat.pred_le
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
⊢ b < a

Tactic:
have : b < a := castSucc_lt_castSucc_iff.mpr (hb.trans_le (le_of_not_gt ha))
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
this : b < a
⊢ i.castPred ⋯ ≤ i.pred ⋯

Tactic:
absurd H this.not_ge

Premises used: absurd, LT.lt.not_ge
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : b.castSucc < i
this : b < a
⊢ i.castPred ⋯ ≤ i.pred ⋯

Tactic:
exact absurd H this.not_ge

Premises used: absurd, LT.lt.not_ge
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
a b : Fin n
H : a ≤ b
ha : ¬a.castSucc < i
hb : ¬b.castSucc < i
⊢ i.castPred ⋯ ≤ i.castPred ⋯

Tactic:
rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
p q : Fin n
hpq : p ≤ q
i j : Fin (n + 1)
hij : i ≤ j
⊢ p.predAbove i ≤ q.predAbove j

Tactic:
(predAbove_right_monotone p hij).trans (predAbove_left_monotone j hpq)

Premises used: Fin.predAbove_left_monotone, Fin.predAbove_right_monotone, LE.le.trans
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin n
hij : i.predAbove = j.predAbove
obtain : ∀ (n : ℕ) ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove), i = j
⊢ i = j

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_add_one_eq.2 i.size_positive

Premises used: Iff.mpr, Fin.size_positive, Nat.exists_add_one_eq, rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
inr : ∀ (this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j) (h : j ≤ i), i = j
wlog! : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j
⊢ i = j

Tactic:
wlog! h : i < j generalizing i j
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j
h : j ≤ i
inr : ∀ (h : j < i), i = j
inr₁ : ∀ (hij : j.predAbove = j.predAbove) (h : j ≤ j), j = j
⊢ i = j

Tactic:
obtain h | rfl := h.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j
h_1 : j ≤ i
h : j < i
⊢ i = j

Tactic:
(this hij.symm h).symm

Premises used: Eq.symm
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j
h_1 : j ≤ i
h : j < i
⊢ i = j

Tactic:
exact (this hij.symm h).symm

Premises used: Eq.symm
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
j : Fin (n + 1)
this : ∀ ⦃i j : Fin (n + 1)⦄ (hij : i.predAbove = j.predAbove) (h : i < j), i = j
hij : j.predAbove = j.predAbove
h : j ≤ j
⊢ j = j

Tactic:
rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
hij : i.predAbove = j.predAbove
h : i < j
⊢ i.predAbove i.succ = j.predAbove i.succ

Tactic:
replace hij := congr_fun hij i.succ
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i = j.predAbove i.succ
⊢ i.succ ≤ j.castSucc

Tactic:
simpa
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.predAbove i.succ = j.predAbove i.succ
⊢ i.castSucc = i.succ

Tactic:
rw [predAbove_succ_self, Fin.predAbove_of_le_castSucc _ _ (by simpa),
    ← Fin.castSucc_inj, castSucc_castPred] at hij

Premises used: Fin.castSucc_castPred, Fin.castSucc_inj, Fin.predAbove_of_le_castSucc, Fin.predAbove_succ_self
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.castSucc = i.succ
⊢ i = j

Tactic:
(i.castSucc_lt_succ.ne hij).elim

Premises used: False.elim, Fin.castSucc_lt_succ, LT.lt.ne
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i j : Fin (n + 1)
h : i < j
hij : i.castSucc = i.succ
⊢ i = j

Tactic:
exact (i.castSucc_lt_succ.ne hij).elim

Premises used: False.elim, Fin.castSucc_lt_succ, LT.lt.ne
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
x y : Fin n
⊢ x.predAbove = y.predAbove ↔ x = y

Tactic:
predAbove_left_injective.eq_iff

Premises used: Function.Injective.eq_iff, Fin.predAbove_left_injective
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
p : Fin (n + 1)
i j : Fin n
⊢ Monotone (α := Fin n) (β := { i : ℕ // i < n }) (⇑equivSubtype : (a : Fin n) → { i : ℕ // i < n })

Tactic:
simp [Monotone]

Premises used: Monotone
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
p : Fin (n + 1)
i j : Fin n
⊢ Monotone (α := { i : ℕ // i < n }) (β := Fin n) (⇑(Equiv.symm equivSubtype) : (a : { i : ℕ // i < n }) → Fin n)

Tactic:
simp [Monotone]

Premises used: Monotone
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
h : n = m
subst : (castOrderIso ⋯).symm = castOrderIso ⋯
⊢ (castOrderIso h).symm = castOrderIso ⋯

Tactic:
subst h
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ (castOrderIso ⋯).symm = castOrderIso ⋯

Tactic:
rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
h : n = n
h₁ :
  ∀ (x : Fin n),
    (↑((castOrderIso h : (a : Fin n) → Fin n) x) : ℕ) = (↑((OrderIso.refl (Fin n) : (a : Fin n) → Fin n) x) : ℕ)
⊢ castOrderIso h = OrderIso.refl (Fin n)

Tactic:
ext
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
h : n = n
x : Fin n
⊢ (↑((castOrderIso h : (a : Fin n) → Fin n) x) : ℕ) = (↑((OrderIso.refl (Fin n) : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
h : n = m
subst :
  (castOrderIso ⋯).toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) = Equiv.cast ⋯
⊢ (castOrderIso h).toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin m) ↦ x1 ≤ x2) = Equiv.cast ⋯

Tactic:
subst h
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ (castOrderIso ⋯).toEquiv (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) = Equiv.cast ⋯

Tactic:
rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin n
⊢ Eq (α := (Fin n)ᵒᵈ) ((OrderIso.symm revOrderIso : (a : Fin n) → (Fin n)ᵒᵈ) i : (Fin n)ᵒᵈ)
    ((OrderDual.toDual : (a : Fin n) → (Fin n)ᵒᵈ) i.rev : (Fin n)ᵒᵈ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ StrictAnti (α := Fin n) rev

Tactic:
fun _ _ ↦ rev_lt_rev.mpr

Premises used: Iff.mpr, StrictAnti, Fin.rev_lt_rev
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ Antitone (α := Fin n) rev

Tactic:
rev_strictAnti.antitone

Premises used: Fin.rev_strictAnti, StrictAnti.antitone
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n_1 : ℕ
p : Fin (n_1 + 1)
i j : Fin n_1
n : ℕ
⊢ IsWellOrder (Fin n) fun (x1 x2 : Fin n) ↦ x1 < x2

Tactic:
(valOrderEmb n).isWellOrder

Premises used: OrderEmbedding.isWellOrder, Fin.valOrderEmb
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ Eq (α := (a : Fin n) → Fin (n + 1)) (⇑(succOrderEmb n) : (a : Fin n) → Fin (n + 1)) succ

Tactic:
rfl

Premises used: Fin.succ, rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
⊢ (succOrderEmb n).toEmbedding (r := fun (x1 x2 : Fin n) ↦ x1 ≤ x2) (s := fun (x1 x2 : Fin (n + 1)) ↦ x1 ≤ x2) =
    succEmb n

Tactic:
rfl

Premises used: Fin.succEmb, rfl
-- Module: Mathlib.Order.Fin.Basic
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := Set (Fin (n + 1))) (range (ι := Fin n) (⇑i.succAboveOrderEmb : (a : Fin n) → Fin (n + 1))) {i}ᶜ

Tactic:
aesop
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : Fin n
rcases : ∀ (i : ℕ) (hi : i < n), (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = (↑(⟨i, hi⟩ : Fin n) : ℕ)
⊢ (↑((e : (a : Fin n) → Fin m) i) : ℕ) = (↑i : ℕ)

Tactic:
rcases i with ⟨i, hi⟩
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
dsimp : (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i
⊢ (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = (↑(⟨i, hi⟩ : Fin n) : ℕ)

Tactic:
dsimp only
-- Module: Mathlib.Order.Fin.Basic
Goal:
m n : ℕ
e : Fin n ≃o Fin m
i : ℕ
hi : i < n
h :
  ∀ (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), (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i
⊢ (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i

Tactic:
induction i using Nat.strong_induction_on with | _ i 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
⊢ (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i

Tactic:
le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)

Premises used: forall_lt_iff_le, le_antisymm, Iff.mp
-- 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
h₁ : ∀ (j : ℕ) (hj : j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)), j < i
h₂ : ∀ (j : ℕ) (hj : j < i), j < (↑((e : (a : Fin n) → Fin m) ⟨i, hi⟩) : ℕ)
⊢ (↑((e : (a : Fin n) → Fin m) (⟨i, hi⟩ : Fin n)) : ℕ) = i

Tactic:
refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_)

Premises used: forall_lt_iff_le, le_antisymm, Iff.mp