awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Pigeonhole
Goal:
m n : ℕ
f : Fin m ↪ Fin n
⊢ m ≤ n

Tactic:
simpa using Fintype.card_le_of_embedding f

Premises used: Fintype.card_le_of_embedding
-- Module: Mathlib.Data.Fin.Pigeonhole
Goal:
m n : ℕ
f : Fin m → Fin n
hf : Function.Injective f
b : Fin n
hb : b ∉ Set.range f
⊢ m < n

Tactic:
simpa using Fintype.card_lt_of_injective_of_notMem f hf hb

Premises used: Fintype.card_lt_of_injective_of_notMem
-- Module: Mathlib.Data.Fin.Pigeonhole
Goal:
m n : ℕ
f : Fin m → Fin n
hf : Function.Surjective f
⊢ n ≤ m

Tactic:
simpa using Fintype.card_le_of_surjective f hf

Premises used: Fintype.card_le_of_surjective
-- Module: Mathlib.Data.Fin.Pigeonhole
Goal:
m : ℕ
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
f : Fin m → α
⊢ Fintype.card.{u_1} (↑(Set.range f) : Type u_1) ≤ m

Tactic:
simpa using Fintype.card_range_le f

Premises used: Fintype.card_range_le
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
⊢ Involutive (α := Fin n) rev

Tactic:
rev_rev

Premises used: Function.Involutive, Fin.rev_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
⊢ Injective (α := Fin n) rev

Tactic:
rev_involutive.injective

Premises used: Fin.rev_involutive, Function.Involutive.injective
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
⊢ Surjective (α := Fin n) rev

Tactic:
rev_involutive.surjective

Premises used: Fin.rev_involutive, Function.Involutive.surjective
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
⊢ Bijective (α := Fin n) rev

Tactic:
rev_involutive.bijective

Premises used: Fin.rev_involutive, Function.Involutive.bijective
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
⊢ Eq (α := Fin n ≃ Fin n) (Equiv.symm revPerm) revPerm

Tactic:
rfl

Premises used: Function.Involutive.toPerm, Equiv.symm, Fin.revPerm, rfl
-- Module: Mathlib.Data.Fin.Rev
Goal:
n m : ℕ
i : Fin n
h : n = m
subst : Fin.cast ⋯ i.rev = (Fin.cast ⋯ i).rev
⊢ Fin.cast h i.rev = (Fin.cast h i).rev

Tactic:
subst h
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i : Fin n
⊢ Fin.cast ⋯ i.rev = (Fin.cast ⋯ i).rev

Tactic:
simp
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i j : Fin n
rw : i.rev.rev = j.rev ↔ i = j.rev
rw₁ rw₂ : i = j.rev ↔ i = j.rev
⊢ i.rev = j ↔ i = j.rev

Tactic:
rw [← rev_inj, rev_rev]

Premises used: Fin.rev_rev, Fin.rev_inj
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i j : Fin n
⊢ i.rev ≠ j ↔ i ≠ j.rev

Tactic:
rev_eq_iff.not

Premises used: Iff.not, Fin.rev_eq_iff
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i j : Fin n
rw : j.rev < i.rev.rev ↔ j.rev < i
rw₁ rw₂ : j.rev < i ↔ j.rev < i
⊢ i.rev < j ↔ j.rev < i

Tactic:
rw [← rev_lt_rev, rev_rev]

Premises used: Fin.rev_rev, Fin.rev_lt_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i j : Fin n
rw : j.rev ≤ i.rev.rev ↔ j.rev ≤ i
rw₁ rw₂ : j.rev ≤ i ↔ j.rev ≤ i
⊢ i.rev ≤ j ↔ j.rev ≤ i

Tactic:
rw [← rev_le_rev, rev_rev]

Premises used: Fin.rev_le_rev, Fin.rev_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i j : Fin n
rw : j.rev.rev < i.rev ↔ j < i.rev
rw₁ rw₂ : j < i.rev ↔ j < i.rev
⊢ i < j.rev ↔ j < i.rev

Tactic:
rw [← rev_lt_rev, rev_rev]

Premises used: Fin.rev_rev, Fin.rev_lt_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i j : Fin n
rw : j.rev.rev ≤ i.rev ↔ j ≤ i.rev
rw₁ rw₂ : j ≤ i.rev ↔ j ≤ i.rev
⊢ i ≤ j.rev ↔ j ≤ i.rev

Tactic:
rw [← rev_le_rev, rev_rev]

Premises used: Fin.rev_le_rev, Fin.rev_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
inst : NeZero n
⊢ (↑(rev 0) : ℕ) = n.pred

Tactic:
rfl

Premises used: Nat.pred, rfl
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
rw : (i.pred h).rev.castSucc = (i.rev.castPred h').castSucc
rw₁ : (i.pred h).rev.castSucc = i.rev
rw₂ : (i.pred h).succ.rev = i.rev
rw₃ rw₄ : i.rev = i.rev
⊢ (i.pred h).rev = i.rev.castPred h'

Tactic:
rw [← castSucc_inj, castSucc_castPred, ← rev_succ, succ_pred]

Premises used: Fin.castSucc_castPred, Fin.castSucc_inj, Fin.rev_succ, Fin.succ_pred
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
rw : (i.castPred h).rev.succ = (i.rev.pred h').succ
rw₁ : (i.castPred h).rev.succ = i.rev
rw₂ : (i.castPred h).castSucc.rev = i.rev
rw₃ rw₄ : i.rev = i.rev
⊢ (i.castPred h).rev = i.rev.pred h'

Tactic:
rw [← succ_inj, succ_pred, ← rev_castSucc, castSucc_castPred]

Premises used: Fin.succ_inj, Fin.castSucc_castPred, Fin.rev_castSucc, Fin.succ_pred
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
inl : ∀ (h : i.succ ≤ p.rev), p.rev.succAbove i = (p.succAbove i.rev).rev
inr : ∀ (h : p.rev ≤ i.castSucc), p.rev.succAbove i = (p.succAbove i.rev).rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
obtain h | h := (rev p).succ_le_or_le_castSucc i

Premises used: Fin.rev, Fin.succ_le_or_le_castSucc
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
inl : i.castSucc = (p.succAbove i.rev).rev
inl₁ : i.castSucc = i.rev.succ.rev
inl₂ : i.castSucc = i.rev.rev.castSucc
inl₃ inl₄ : i.castSucc = i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
rw [succAbove_of_succ_le _ _ h,
      succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]

Premises used: Fin.succAbove_of_le_castSucc, Fin.succAbove_of_succ_le, Fin.rev_rev, Fin.rev_succ
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
inr : i.succ = (p.succAbove i.rev).rev
inr₁ : i.succ = i.rev.castSucc.rev
inr₂ : i.succ = i.rev.rev.succ
inr₃ inr₄ : i.succ = i.succ
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev

Tactic:
rw [succAbove_of_le_castSucc _ _ h,
      succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc, rev_rev]

Premises used: Fin.succAbove_of_le_castSucc, Fin.succAbove_of_succ_le, Fin.rev_castSucc, Fin.rev_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : p.succAbove i.rev = (p.succAbove i.rev).rev.rev
rw₁ rw₂ : p.succAbove i.rev = p.succAbove i.rev
⊢ p.succAbove i.rev = (p.rev.succAbove i).rev

Tactic:
rw [succAbove_rev_left, rev_rev]

Premises used: Fin.succAbove_rev_left, Fin.rev_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : (p.succAbove i).rev = (p.succAbove i.rev.rev).rev
rw₁ rw₂ : (p.succAbove i).rev = (p.succAbove i).rev
⊢ (p.succAbove i).rev = p.rev.succAbove i.rev

Tactic:
rw [succAbove_rev_left, rev_rev]

Premises used: Fin.succAbove_rev_left, Fin.rev_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
inl : ∀ (h : p.succ ≤ i.rev), p.rev.predAbove i = (p.predAbove i.rev).rev
inr : ∀ (h : i.rev ≤ p.castSucc), p.rev.predAbove i = (p.predAbove i.rev).rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
obtain h | h := (rev i).succ_le_or_le_castSucc p

Premises used: Fin.rev, Fin.succ_le_or_le_castSucc
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
inl : p.rev.predAbove i = (i.rev.pred ⋯).rev
inl₁ : p.rev.predAbove i = i.rev.rev.castPred ⋯
inl₂ : i.castPred ⋯ = i.rev.rev.castPred ⋯
inl₃ : i = i.rev.rev
inl₄ inl₅ : i = i
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
rw [predAbove_of_succ_le _ _ h, rev_pred,
      predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]

Premises used: Iff.mpr, Fin.castPred_inj, Eq.rec, Fin.rev_pred, Fin.predAbove_of_succ_le, Fin.predAbove_of_le_castSucc, Fin.rev_rev, Fin.rev_last, Eq.symm, Fin.rev_ne_iff
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
inr : p.rev.predAbove i = (i.rev.castPred ⋯).rev
inr₁ : p.rev.predAbove i = i.rev.rev.pred ⋯
inr₂ : i.pred ⋯ = i.rev.rev.pred ⋯
inr₃ : i = i.rev.rev
inr₄ inr₅ : i = i
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev

Tactic:
rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]

Premises used: Iff.mpr, Fin.pred_inj, Eq.rec, Fin.predAbove_of_succ_le, Fin.rev_castPred, Fin.predAbove_of_le_castSucc, Fin.rev_rev, Eq.symm, Fin.rev_zero, Fin.rev_ne_iff
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
rw : p.predAbove i.rev = (p.predAbove i.rev).rev.rev
rw₁ rw₂ : p.predAbove i.rev = p.predAbove i.rev
⊢ p.predAbove i.rev = (p.rev.predAbove i).rev

Tactic:
rw [predAbove_rev_left, rev_rev]

Premises used: Fin.predAbove_rev_left, Fin.rev_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
rw : (p.predAbove i).rev = (p.predAbove i.rev.rev).rev
rw₁ rw₂ : (p.predAbove i).rev = (p.predAbove i).rev
⊢ (p.predAbove i).rev = p.rev.predAbove i.rev

Tactic:
rw [predAbove_rev_left, rev_rev]

Premises used: Fin.predAbove_rev_left, Fin.rev_rev
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
j : Fin (n + 1)
obtain : ∀ (j : ℕ) (hj : j < n + 1), (↑(⟨j, hj⟩ : Fin (n + 1)) : ℕ) + (↑(⟨j, hj⟩ : Fin (n + 1)).rev : ℕ) = n
⊢ (↑j : ℕ) + (↑j.rev : ℕ) = n

Tactic:
obtain ⟨j, hj⟩ := j
-- Module: Mathlib.Data.Fin.Rev
Goal:
n j : ℕ
hj : j < n + 1
⊢ (↑(⟨j, hj⟩ : Fin (n + 1)) : ℕ) + (↑(⟨j, hj⟩ : Fin (n + 1)).rev : ℕ) = n

Tactic:
simp [Nat.add_sub_cancel' <| le_of_lt_succ hj]

Premises used: Nat.le_of_lt_succ, Nat.add_sub_cancel'
-- Module: Mathlib.Data.Fin.Rev
Goal:
n : ℕ
j : Fin (n + 1)
rw : (↑j : ℕ) + (↑j.rev : ℕ) = n
rw₁ rw₂ : n = n
⊢ (↑j.rev : ℕ) + (↑j : ℕ) = n

Tactic:
rw [Nat.add_comm, j.add_rev_cast]

Premises used: Fin.add_rev_cast, Nat.add_comm
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin n
⊢ a.succ = b.succ → a = b

Tactic:
simp [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x : Fin (n + 1)
⊢ (∃ (y : Fin n), y.succ = x) ↔ x ≠ 0

Tactic:
⟨fun ⟨_, hy⟩ => hy ▸ succ_ne_zero _, x.cases (fun h => h.irrefl.elim) (fun _ _ => ⟨_, rfl⟩)⟩

Premises used: Eq.rec, Ne, Iff.intro, Fin.succ_ne_zero, _private.0.Fin.exists_succ_eq.match_1, Fin.cases, OfNat.ofNat
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x : Fin (n + 1)
h : x ≠ 0
⊢ ∃ (y : Fin n), y.succ = x

Tactic:
exists_succ_eq.mpr h

Premises used: Iff.mpr, Fin.exists_succ_eq
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
zero : ∀ [inst : NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (Fin.succ 0) 1
succ : ∀ (n : ℕ) [inst : NeZero (n + 1)], Eq (α := Fin (n + 1 + 1)) (Fin.succ 0) 1
⊢ Eq (α := Fin (n + 1)) (Fin.succ 0) 1

Tactic:
cases n
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
inst : NeZero (R := ℕ) 0
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (succ 0) 1

Tactic:
(NeZero.ne 0 rfl).elim

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
inst : NeZero (R := ℕ) 0
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (succ 0) 1

Tactic:
exact (NeZero.ne 0 rfl).elim

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero (n + 1)
⊢ Eq (α := Fin (n + 1 + 1)) (succ 0) 1

Tactic:
rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
⊢ LT.lt (α := Fin (n + 1)) 0 1

Tactic:
succ_zero_eq_one' (n := n) ▸ succ_pos _

Premises used: Fin.succ_zero_eq_one', Eq.rec, Fin.succ_pos
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
⊢ Ne (α := Fin (n + 1)) 0 1

Tactic:
Fin.ne_of_lt one_pos'

Premises used: Fin.ne_of_lt, Fin.one_pos'
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
zero : ∀ [NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1 + 1)) (Fin.succ 1) 2
succ : ∀ (n : ℕ) [NeZero (n + 1)], Eq (α := Fin (n + 1 + 1 + 1)) (Fin.succ 1) 2
⊢ Eq (α := Fin (n + 1 + 1)) (Fin.succ 1) 2

Tactic:
cases n
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
inst : NeZero (R := ℕ) 0
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1 + 1)) (succ 1) 2

Tactic:
(NeZero.ne 0 rfl).elim

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
inst : NeZero (R := ℕ) 0
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1 + 1)) (succ 1) 2

Tactic:
exact (NeZero.ne 0 rfl).elim

Premises used: False.elim, OfNat.ofNat, rfl, NeZero.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero (n + 1)
⊢ Eq (α := Fin (n + 1 + 1 + 1)) (succ 1) 2

Tactic:
rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
k : Fin n
h : k ≤ 0
rw : 0 = (↑0 : ℕ)
⊢ (↑k : ℕ) = (↑0 : ℕ)

Tactic:
rw [Nat.eq_zero_of_le_zero h]

Premises used: Nat.eq_zero_of_le_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
k : Fin n
h : k ≤ 0
⊢ 0 = (↑0 : ℕ)

Tactic:
rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
⊢ LE.le (α := Fin n) 0 0

Tactic:
Nat.le_refl _

Premises used: Nat.le_refl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
⊢ LE.le (α := Fin n) 0 0

Tactic:
exact Nat.le_refl _

Premises used: Nat.le_refl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
hmn : m ≤ n
a b : Fin m
⊢ castLE hmn a = castLE hmn b ↔ a = b

Tactic:
simp [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
a b : Fin m
⊢ castAdd n a = castAdd n b ↔ a = b

Tactic:
simp [Fin.ext_iff]

Premises used: Fin.ext_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
hmn : m ≤ n
⊢ Injective (castLE hmn)

Tactic:
fun _ _ hab ↦ Fin.ext (congr_arg val hab :)

Premises used: Fin.ext, Fin.val, congr_arg, Function.Injective
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
m n : ℕ
⊢ Injective (α := Fin m) (castAdd n)

Tactic:
castLE_injective _

Premises used: Fin.castLE_injective
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
⊢ Injective (α := Fin n) castSucc

Tactic:
castAdd_injective _ _

Premises used: Fin.castAdd_injective
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i : Fin n
h : n + 1 ≤ m
⊢ castLE h i.castSucc = castLE ⋯ i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
h : n + 1 ≤ m
⊢ castLE h ∘ castSucc = castLE ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
⊢ castLE ⋯ = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n k : ℕ
h : n ≤ k
⊢ Set.range (castLE h) = {i : Fin k | (↑i : ℕ) < n}

Tactic:
Set.ext fun x => ⟨fun ⟨y, hy⟩ => hy ▸ y.2, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩

Premises used: Set.ext, setOf, Fin.isLt, Membership.mem, Eq.rec, Fin.mk, Fin.val, LT.lt, Iff.intro, Exists.intro, _private.0.Fin.range_castLE.match_1, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
rw :
  (↑(castLE h
          (((Equiv.ofInjective (castLE h) ⋯).symm : (a : (↑(Set.range (castLE h)) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin k) ↦ x ∈ Set.range (castLE h)) i hi))) :
      ℕ) =
    (↑i : ℕ)
⊢ (↑(((Equiv.ofInjective (castLE h) ⋯).symm : (a : (↑(Set.range (castLE h)) : Type)) → Fin n)
          (Subtype.mk (p := fun (x : Fin k) ↦ x ∈ Set.range (castLE h)) i hi)) :
      ℕ) =
    (↑i : ℕ)

Tactic:
rw [← val_castLE h]

Premises used: Fin.val_castLE
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ (↑(castLE h
          (((Equiv.ofInjective (castLE h) ⋯).symm : (a : (↑(Set.range (castLE h)) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin k) ↦ x ∈ Set.range (castLE h)) i hi))) :
      ℕ) =
    (↑i : ℕ)

Tactic:
congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _)

Premises used: Fin.val, congr_arg, Equiv.apply_ofInjective_symm
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ (↑(castLE h
          (((Equiv.ofInjective (castLE h) ⋯).symm : (a : (↑(Set.range (castLE h)) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin k) ↦ x ∈ Set.range (castLE h)) i hi))) :
      ℕ) =
    (↑i : ℕ)

Tactic:
exact congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _)

Premises used: Fin.val, congr_arg, Equiv.apply_ofInjective_symm
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
eq : n = m
⊢ LeftInverse (Fin.cast ⋯) (Fin.cast eq)

Tactic:
fun _ => rfl

Premises used: Function.LeftInverse, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
eq : n = m
⊢ RightInverse (Fin.cast ⋯) (Fin.cast eq)

Tactic:
fun _ => rfl

Premises used: Function.LeftInverse, Function.RightInverse, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
eq : n = m
a b : Fin n
⊢ Fin.cast eq a = Fin.cast eq b ↔ a = b

Tactic:
simp [← val_inj]

Premises used: Fin.val_inj
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
eq : n = m
a b : Fin n
⊢ Fin.cast eq a < Fin.cast eq b ↔ a < b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
eq : n = m
a b : Fin n
⊢ Fin.cast eq a ≤ Fin.cast eq b ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
h : m = n
k : ℕ
hk : k < m
⊢ Eq (α := Fin n) ((finCongr h : (a : Fin m) → Fin n) ⟨k, hk⟩ : Fin n) (⟨k, ⋯⟩ : Fin n)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
h : n = n
H : ∀ (x : Fin n), (↑((finCongr h : (a : Fin n) → Fin n) x) : ℕ) = (↑((Equiv.refl (Fin n) : (a : Fin n) → Fin n) x) : ℕ)
⊢ finCongr h = Equiv.refl (Fin n)

Tactic:
ext
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
h : n = n
x : Fin n
⊢ (↑((finCongr h : (a : Fin n) → Fin n) x) : ℕ) = (↑((Equiv.refl (Fin n) : (a : Fin n) → Fin n) x) : ℕ)

Tactic:
simp
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
h : m = n
⊢ (finCongr h).symm = finCongr ⋯

Tactic:
rfl

Premises used: finCongr, Equiv.symm, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
h : m = n
k : Fin m
⊢ (↑((finCongr h : (a : Fin m) → Fin n) k) : ℕ) = (↑k : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
h : m = n
k : Fin n
⊢ (↑(((finCongr h).symm : (a : Fin n) → Fin m) k) : ℕ) = (↑k : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
h : n = m
subst : finCongr ⋯ = Equiv.cast ⋯
⊢ finCongr h = Equiv.cast ⋯

Tactic:
subst h
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
⊢ finCongr ⋯ = Equiv.cast ⋯

Tactic:
simp
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
h : n = m
⊢ Fin.cast h = cast ⋯

Tactic:
grind
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n
⊢ i.castSucc ≤ i.succ

Tactic:
Nat.le_succ i

Premises used: Nat.le_succ, Fin.val
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin n
⊢ a.castSucc ≤ b.castSucc ↔ a ≤ b

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin n
rw : a.succ < b.succ ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ a.succ ≤ b.castSucc ↔ a < b

Tactic:
rw [le_castSucc_iff, succ_lt_succ_iff]

Premises used: Fin.succ_lt_succ_iff, Fin.le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin n
rw : a.succ ≤ b.succ ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a.castSucc < b.succ ↔ a ≤ b

Tactic:
rw [castSucc_lt_iff_succ_le, succ_le_succ_iff]

Premises used: Fin.succ_le_succ_iff, Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : i.castSucc < a
hu : b < i.succ
⊢ (↑i : ℕ) < (↑a : ℕ)

Tactic:
simp [Fin.lt_def, -val_fin_lt] at *

Premises used: Fin.val_fin_lt, Fin.lt_def
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : i.castSucc < a
hu : b < i.succ
hl₁ : (↑i : ℕ) < (↑a : ℕ)
⊢ (↑b : ℕ) < (↑i : ℕ) + 1

Tactic:
simp [Fin.lt_def, -val_fin_lt] at *

Premises used: Fin.val_fin_lt, Fin.lt_def
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : (↑i : ℕ) < (↑a : ℕ)
hu : (↑b : ℕ) < (↑i : ℕ) + 1
⊢ (↑b : ℕ) < (↑a : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
simp : (↑i : ℕ) < (↑p : ℕ) ∨ (↑p : ℕ) < (↑i : ℕ) + 1
⊢ i.castSucc < p ∨ p < i.succ

Tactic:
simp [Fin.lt_def, -val_fin_lt]

Premises used: Fin.val_fin_lt, Fin.lt_def
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (↑i : ℕ) < (↑p : ℕ) ∨ (↑p : ℕ) < (↑i : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : i.castSucc < p ∨ p < i.succ
⊢ i.succ ≤ p ∨ p ≤ i.castSucc

Tactic:
rw [le_castSucc_iff, ← castSucc_lt_iff_succ_le]

Premises used: Fin.le_castSucc_iff, Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ

Tactic:
p.castSucc_lt_or_lt_succ i

Premises used: Fin.castSucc_lt_or_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ

Tactic:
exact p.castSucc_lt_or_lt_succ i

Premises used: Fin.castSucc_lt_or_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x : Fin (n + 1)
h : x ≠ last n
⊢ ∃ (y : Fin n), y.castSucc = x

Tactic:
exists_castSucc_eq.mpr h

Premises used: Iff.mpr, Fin.exists_castSucc_eq
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
P : Fin (n + 1) → Prop
⊢ (∀ (i : Fin (n + 1)), P i) ↔ (∀ (i : Fin n), P i.castSucc) ∧ P (last n)

Tactic:
⟨fun H => ⟨fun _ => H _, H _⟩, fun ⟨H0, H1⟩ i => Fin.lastCases H1 H0 i⟩

Premises used: Fin.lastCases, Fin.last, And.intro, Iff.intro, _private.0.Fin.forall_fin_succ'.match_1, Fin.castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (∃ (j : Fin n), i = j.castSucc) ∨ i = last n

Tactic:
i.lastCases (Or.inr rfl) (Or.inl ⟨·, rfl⟩)

Premises used: Fin.lastCases
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n
⊢ i.castSucc ≠ last n

Tactic:
Fin.ne_of_lt i.castSucc_lt_last

Premises used: Fin.ne_of_lt, Fin.castSucc_lt_last
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
P : Fin (n + 1) → Prop
⊢ (∃ (i : Fin (n + 1)), P i) ↔ (∃ (i : Fin n), P i.castSucc) ∨ P (last n)

Tactic:
⟨fun ⟨i, h⟩ => Fin.lastCases Or.inr (fun i hi => Or.inl ⟨i, hi⟩) i h,
   fun h => h.elim (fun ⟨i, hi⟩ => ⟨i.castSucc, hi⟩) (fun h => ⟨.last _, h⟩)⟩

Premises used: Exists, Fin.lastCases, _private.0.Fin.exists_fin_succ'.match_2, _private.0.Fin.exists_fin_succ'.match_1, Fin.last, Iff.intro, Exists.intro, Or, Fin.castSucc, Or.elim
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin (n + 1)) (castSucc 0) 0

Tactic:
rfl

Premises used: Fin.ofNat, Nat.mod, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ 0 < i.castSucc ↔ 0 < i

Tactic:
simp [← val_pos_iff]

Premises used: Fin.val_pos_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : p < i
zero : ∀ {p i : Fin 0} (h : p < i), i.castSucc ≠ 0
succ : ∀ (n : ℕ) {p i : Fin (n + 1)} (h : p < i), i.castSucc ≠ 0
⊢ i.castSucc ≠ 0

Tactic:
cases n
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
p i : Fin 0
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
p i : Fin 0
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ i.castSucc ≠ 0

Tactic:
grind [castSucc_ne_zero_iff]

Premises used: Fin.castSucc_ne_zero_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
⊢ a.succ ≠ last (n + 1) ↔ a ≠ last n

Tactic:
not_iff_not.mpr <| succ_eq_last_succ

Premises used: not_iff_not, Iff.mpr, Fin.succ_eq_last_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : i < p
⊢ i.succ ≠ last n

Tactic:
grind
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
h : (↑(↑(↑a : ℕ) : Fin (n + 1)) : ℕ) = (↑a.castSucc : ℕ)
⊢ (↑(↑a : ℕ) : Fin (n + 1)) = a.castSucc

Tactic:
ext
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
⊢ (↑(↑(↑a : ℕ) : Fin (n + 1)) : ℕ) = (↑a.castSucc : ℕ)

Tactic:
val_cast_of_lt (Nat.lt_succ_of_lt a.is_lt)

Premises used: Fin.is_lt, Fin.val_cast_of_lt, Nat.lt_succ_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
⊢ (↑(↑(↑a : ℕ) : Fin (n + 1)) : ℕ) = (↑a.castSucc : ℕ)

Tactic:
exact val_cast_of_lt (Nat.lt_succ_of_lt a.is_lt)

Premises used: Fin.is_lt, Fin.val_cast_of_lt, Nat.lt_succ_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j k : Fin n
⊢ LT.lt (α := Fin (n + 1)) (↑(↑j : ℕ) : Fin (n + 1)) (↑(↑k : ℕ) : Fin (n + 1)) ↔ j < k

Tactic:
simp only [coe_eq_castSucc, castSucc_lt_castSucc_iff]

Premises used: Fin.castSucc_lt_castSucc_iff, Fin.coe_eq_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
⊢ n ≤ n + 1

Tactic:
lia