awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih : a.castSucc.rev = a.rev.fs
⊢ a.fs.castSucc.rev = a.fs.rev.fs

Tactic:
simp_all [rev, castSucc, last]

Premises used: Fin2.castSucc, Fin2.rev, Fin2.last
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
i : Fin2 n
fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1)) (rev (rev Fin2.fz)) Fin2.fz
fs : ∀ {n : ℕ} (a : Fin2 n), a.rev.rev = a → a.fs.rev.rev = a.fs
⊢ i.rev.rev = i

Tactic:
induction i
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n n_1 : ℕ
⊢ Eq (α := Fin2 (n_1 + 1)) (rev (rev fz)) fz

Tactic:
simp_all [rev]

Premises used: Fin2.rev
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n n_1 : ℕ
a : Fin2 n_1
a_ih : a.rev.rev = a
⊢ a.fs.rev.rev = a.fs

Tactic:
simp_all [rev]

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

Tactic:
rev_rev

Premises used: Function.Involutive, Fin2.rev_rev
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ fz ∉ Finset.map { toFun := fs, inj' := ⋯ : Fin2 n ↪ Fin2 (n + 1) } elems

Tactic:
simp
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
⊢ fz ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ : Fin2 n ↪ Fin2 (n + 1) } elems) ⋯

Tactic:
simp [compl]
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
elems : Finset (Fin2 n)
compl : ∀ (x : Fin2 n), x ∈ elems
i : Fin2 n
⊢ i.fs ∈ Finset.cons fz (Finset.map { toFun := fs, inj' := ⋯ : Fin2 n ↪ Fin2 (n + 1) } elems) ⋯

Tactic:
simp [compl]
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1)) (toFin fz) 0

Tactic:
rfl

Premises used: Fin2.toFin, rfl
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
i : Fin2 n
⊢ i.fs.toFin = i.toFin.succ

Tactic:
rfl

Premises used: Fin2.toFin, rfl
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
⊢ Eq (α := Fin2 (n + 1)) (ofFin 0) fz

Tactic:
rfl

Premises used: Eq.mpr, Fin2.ofFin, Fin.succRec, rfl
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
i : Fin n
⊢ ofFin i.succ = (ofFin i).fs

Tactic:
rfl

Premises used: Fin2.ofFin, Fin.succRec, rfl
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
i : Fin n
⊢ (ofFin i).toFin = i

Tactic:
i.succRec (fun _ => rfl) (fun _ _ ih => congrArg Fin.succ ih)

Premises used: Fin.succRec
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n n_1 : ℕ
⊢ Eq (α := Fin2 (n_1 + 1)) (ofFin (toFin fz)) fz

Tactic:
rfl
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n n_1 : ℕ
a : Fin2 n_1
ih : ofFin a.toFin = a
⊢ ofFin a.fs.toFin = a.fs

Tactic:
congrArg fs ih

Premises used: congrArg, Fin2.ofFin, Fin2.fs, Fin.succRec
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n n_1 : ℕ
a : Fin2 n_1
ih : ofFin a.toFin = a
⊢ ofFin a.fs.toFin = a.fs

Tactic:
exact congrArg fs ih

Premises used: congrArg, Fin2.fs
-- Module: Mathlib.Data.Fin.Fin2
Goal:
n : ℕ
i : Fin2 n
fz : ∀ {n : ℕ}, Eq (α := Fin2 (n + 1)) (ofFin (toFin Fin2.fz)) Fin2.fz
fs : ∀ {n : ℕ} (a : Fin2 n) (ih : ofFin a.toFin = a), ofFin a.fs.toFin = a.fs
⊢ ofFin i.toFin = i

Tactic:
induction i with
  | fz => rfl
  | fs _ ih => exact congrArg fs ih

Premises used: Fin2.fz, Fin2.fs
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
⊢ Monotone f

Tactic:
have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovBy k).1
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
⊢ IsMaxChain (fun (x1 x2 : α) ↦ x1 ≤ x2) (range f)

Tactic:
⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩

Premises used: IsMaxChain, Monotone.isChain_range, HasSubset.Subset.antisymm, And.intro
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
refine :
  ∀ (t : Set α) (htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t) (hbt : range f ⊆ t) (x : α) (hx : x ∈ t), x ∈ range f
⊢ IsMaxChain (fun (x1 x2 : α) ↦ x1 ≤ x2) (range f)

Tactic:
refine ⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
by_contra! : ∀ (h : ∀ (y : Fin (n + 1)), f y ≠ x), False
⊢ ∃ (y : Fin (n + 1)), f y = x

Tactic:
by_contra! h
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
this : ∀ (k : Fin (n + 1)), f k < x
⊢ False

Tactic:
simpa [hlast] using this (.last _)

Premises used: Fin.last
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
suffices : ∀ (k : Fin (n + 1)), f k < x
⊢ False

Tactic:
suffices ∀ k, f k < x by simpa [hlast] using this (.last _)
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
⊢ f 0 < x

Tactic:
simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm

Premises used: bot_lt_iff_ne_bot, Ne.symm, OfNat.ofNat
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
k : Fin n
ihk : f k.castSucc < x
succ :
  ∀ (hbt : ∀ (y : Fin (n + 1)), f y ∈ t) (x : α) (hx : x ∈ t) (h : ∀ (y : Fin (n + 1)), f y ≠ x) (k : Fin n)
    (ihk : f k.castSucc < x), f k.succ < x
⊢ f k.succ < x

Tactic:
rw [range_subset_iff] at hbt

Premises used: Set.range_subset_iff
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hbt : ∀ (y : Fin (n + 1)), f y ∈ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
k : Fin n
ihk : f k.castSucc < x
⊢ f k.succ < x

Tactic:
(htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)

Premises used: Fin.succ, IsChain.lt_of_le, And.right, Or.resolve_right
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hbt : ∀ (y : Fin (n + 1)), f y ∈ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
k : Fin n
ihk : f k.castSucc < x
⊢ f k.succ < x

Tactic:
exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)

Premises used: Fin.succ, IsChain.lt_of_le, And.right, Or.resolve_right
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
hmono : Monotone f
t : Set α
htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hbt : range f ⊆ t
x : α
hx : x ∈ t
h : ∀ (y : Fin (n + 1)), f y ≠ x
k : Fin (n + 1)
zero : f 0 < x
succ : ∀ (k : Fin n) (ihk : f k.castSucc < x), f k.succ < x
⊢ f k < x

Tactic:
induction k using Fin.induction with
  | zero => simpa [h0, bot_lt_iff_ne_bot] using (h 0).symm
  | succ k ihk =>
    rw [range_subset_iff] at hbt
    exact (htc.lt_of_le (hbt k.succ) hx (h _)).resolve_right ((hcovBy k).2 ihk)

Premises used: bot_lt_iff_ne_bot, Ne.symm, Set.range_subset_iff, OfNat.ofNat
-- Module: Mathlib.Data.Fin.FlagRange
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : BoundedOrder α
n : ℕ
f : Fin (n + 1) → α
x : α
h0 : f 0 = ⊥
hlast : f (Fin.last n) = ⊤
hcovBy : ∀ (k : Fin n), f k.castSucc ⩿ f k.succ
⊢ x ∈ rangeFin f h0 hlast hcovBy ↔ ∃ (k : Fin (n + 1)), f k = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.range
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
inl : ∀ (hji : j.castSucc < i), Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
inr : ∀ (hij : i ≤ j.castSucc), Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))

Tactic:
rcases lt_or_ge j.castSucc i with hji | hij

Premises used: lt_or_ge, Fin.castSucc
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
⊢ 1 ≤ (↑i : ℕ)

Tactic:
have : 1 ≤ (i : ℕ) := (Nat.zero_le j).trans_lt hji
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
this : 1 ≤ (↑i : ℕ)
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))

Tactic:
simp [succAbove_of_castSucc_lt _ _ hji, predAbove_of_castSucc_lt _ _ hji, this, iff_comm,
      parity_simps]

Premises used: Fin.predAbove_of_castSucc_lt, iff_comm, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
hij : i ≤ j.castSucc
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))

Tactic:
simp [succAbove_of_le_castSucc _ _ hij, predAbove_of_le_castSucc _ _ hij,
      ← Nat.not_even_iff_odd, not_iff, not_iff_comm, parity_simps]

Premises used: Fin.succAbove_of_le_castSucc, Nat.not_even_iff_odd, not_iff, Fin.predAbove_of_le_castSucc, not_iff_comm
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
R : Type u_1
inst : Monoid R
inst_1 : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
rw : Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Even ((↑i : ℕ) + (↑j : ℕ) + 1)
⊢ HPow.hPow (α := R) (-1) ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) =
    -HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ))

Tactic:
rw [← neg_one_mul (_ ^ _), ← pow_succ', neg_one_pow_congr]

Premises used: neg_one_pow_congr, neg_one_mul, HPow.hPow, pow_succ'
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
R : Type u_1
inst : Monoid R
inst_1 : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
rw : Odd ((↑i : ℕ) + (↑j : ℕ)) ↔ Even ((↑i : ℕ) + (↑j : ℕ) + 1)
rw₁ : Odd ((↑i : ℕ) + (↑j : ℕ)) ↔ ¬Even ((↑i : ℕ) + (↑j : ℕ))
rw₂ rw₃ : Odd ((↑i : ℕ) + (↑j : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Even ((↑i : ℕ) + (↑j : ℕ) + 1)

Tactic:
rw [even_succAbove_add_predAbove, Nat.even_add_one, Nat.not_even_iff_odd]

Premises used: Nat.even_add_one, Nat.not_even_iff_odd, Fin.even_succAbove_add_predAbove
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
h : Even (↑k : ℕ)
⊢ NeZero n

Tactic:
have : NeZero n := ⟨k.pos.ne'⟩
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
h : Even (↑k : ℕ)
this : NeZero n
rw : Even (α := Fin n) (↑(↑k : ℕ) : Fin n)
⊢ Even k

Tactic:
rw [← Fin.cast_val_eq_self k]

Premises used: Fin.cast_val_eq_self
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
h : Even (↑k : ℕ)
this : NeZero n
⊢ Even (α := Fin n) (↑(↑k : ℕ) : Fin n)

Tactic:
h.natCast

Premises used: Even.natCast
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
h : Even (↑k : ℕ)
this : NeZero n
⊢ Even (α := Fin n) (↑(↑k : ℕ) : Fin n)

Tactic:
exact h.natCast

Premises used: Even.natCast
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
h : Odd (↑k : ℕ)
rw : Odd (α := Fin n) (↑(↑k : ℕ) : Fin n)
⊢ Odd k

Tactic:
rw [← Fin.cast_val_eq_self k]

Premises used: Fin.cast_val_eq_self
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
h : Odd (↑k : ℕ)
⊢ Odd (α := Fin n) (↑(↑k : ℕ) : Fin n)

Tactic:
h.natCast

Premises used: Odd.natCast
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
h : Odd (↑k : ℕ)
⊢ Odd (α := Fin n) (↑(↑k : ℕ) : Fin n)

Tactic:
exact h.natCast

Premises used: Odd.natCast
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
hn : Odd n
k : Fin n
⊢ NeZero n

Tactic:
have : NeZero n := ⟨k.pos.ne'⟩
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
inl : ∀ (hk : Even (↑k : ℕ)), Even k
inr : ∀ (hk : Odd (↑k : ℕ)), Even k
⊢ Even k

Tactic:
rcases k.val.even_or_odd with hk | hk

Premises used: Fin.val, Nat.even_or_odd
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Even (↑k : ℕ)
⊢ Even k

Tactic:
even_of_val hk

Premises used: Fin.even_of_val
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Even (↑k : ℕ)
⊢ Even k

Tactic:
exact even_of_val hk

Premises used: Fin.even_of_val
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
hk : Odd (↑k : ℕ)
⊢ Even k

Tactic:
simpa using (hk.add_odd hn).natCast (α := Fin n)

Premises used: Odd.add_odd, Even.natCast
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
inst : NeZero n
hn : Odd n
k : Fin n
inl : ∀ (hk : Even (↑k : ℕ)), Odd k
inr : ∀ (hk : Odd (↑k : ℕ)), Odd k
⊢ Odd k

Tactic:
rcases k.val.even_or_odd with hk | hk

Premises used: Fin.val, Nat.even_or_odd
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
inst : NeZero n
hn : Odd n
k : Fin n
hk : Even (↑k : ℕ)
⊢ Odd k

Tactic:
simpa using (Even.add_odd hk hn).natCast (R := Fin n)

Premises used: Even.add_odd, Odd.natCast
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
inst : NeZero n
hn : Odd n
k : Fin n
hk : Odd (↑k : ℕ)
⊢ Odd k

Tactic:
odd_of_val hk

Premises used: Fin.odd_of_val
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
inst : NeZero n
hn : Odd n
k : Fin n
hk : Odd (↑k : ℕ)
⊢ Odd k

Tactic:
exact odd_of_val hk

Premises used: Fin.odd_of_val
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
hn : Even n
rcases : ∀ (n : ℕ) {k : Fin (n + n)}, Even k ↔ Even (↑k : ℕ)
⊢ Even k ↔ Even (↑k : ℕ)

Tactic:
rcases hn with ⟨n, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin (n + n)
⊢ Even k ↔ Even (↑k : ℕ)

Tactic:
⟨?_, even_of_val⟩

Premises used: Fin.even_of_val, Iff.intro
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin (n + n)
refine : Even k → Even (↑k : ℕ)
⊢ Even k ↔ Even (↑k : ℕ)

Tactic:
refine ⟨?_, even_of_val⟩
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
l : Fin (n + n)
rw : Even (if n + n ≤ (↑l : ℕ) + (↑l : ℕ) then (↑l : ℕ) + (↑l : ℕ) - (n + n) else (↑l : ℕ) + (↑l : ℕ))
⊢ Even (↑(l + l) : ℕ)

Tactic:
rw [val_add_eq_ite]

Premises used: Fin.val_add_eq_ite
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
l : Fin (n + n)
pos : ∀ (h : n + n ≤ (↑l : ℕ) + (↑l : ℕ)), Even ((↑l : ℕ) + (↑l : ℕ) - (n + n))
neg : ∀ (h : ¬n + n ≤ (↑l : ℕ) + (↑l : ℕ)), Even ((↑l : ℕ) + (↑l : ℕ))
⊢ Even (if n + n ≤ (↑l : ℕ) + (↑l : ℕ) then (↑l : ℕ) + (↑l : ℕ) - (n + n) else (↑l : ℕ) + (↑l : ℕ))

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
l : Fin (n + n)
h : n + n ≤ (↑l : ℕ) + (↑l : ℕ)
⊢ Even ((↑l : ℕ) + (↑l : ℕ) - (n + n))

Tactic:
simp [Nat.even_sub, *]

Premises used: Nat.even_sub
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
l : Fin (n + n)
h : ¬n + n ≤ (↑l : ℕ) + (↑l : ℕ)
⊢ Even ((↑l : ℕ) + (↑l : ℕ))

Tactic:
simp [Nat.even_sub, *]

Premises used: Nat.even_sub
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
rcases : ∀ (n : ℕ) {k : Fin (n + n)} [inst : NeZero (n + n)], Odd k ↔ Odd (↑k : ℕ)
⊢ Odd k ↔ Odd (↑k : ℕ)

Tactic:
rcases hn with ⟨n, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin (n + n)
inst : NeZero (n + n)
⊢ Odd k ↔ Odd (↑k : ℕ)

Tactic:
⟨?_, odd_of_val⟩

Premises used: Fin.odd_of_val, Iff.intro
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin (n + n)
inst : NeZero (n + n)
refine : Odd k → Odd (↑k : ℕ)
⊢ Odd k ↔ Odd (↑k : ℕ)

Tactic:
refine ⟨?_, odd_of_val⟩
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
inst : NeZero (n + n)
l : Fin (n + n)
rw : Odd ((2 % (n + n) * (↑l : ℕ) % (n + n) + 1 % (n + n)) % (n + n))
⊢ Odd (↑(2 * l + 1) : ℕ)

Tactic:
rw [val_add, val_mul, coe_ofNat_eq_mod, coe_ofNat_eq_mod]

Premises used: Fin.val_add, Fin.val_mul, Fin.coe_ofNat_eq_mod
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
inst : NeZero (n + n)
l : Fin (n + n)
simp : (2 * (↑l : ℕ) + 1) % (n + n) % 2 = 1
⊢ Odd ((2 % (n + n) * (↑l : ℕ) % (n + n) + 1 % (n + n)) % (n + n))

Tactic:
simp only [Nat.mod_mul_mod, Nat.add_mod_mod, Nat.mod_add_mod, Nat.odd_iff]

Premises used: Nat.mod_mul_mod, Nat.add_mod_mod, Nat.mod_add_mod, Nat.odd_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
inst : NeZero (n + n)
l : Fin (n + n)
rw : Even (2 * (↑l : ℕ))
⊢ (2 * (↑l : ℕ) + 1) % (n + n) % 2 = 1

Tactic:
rw [Nat.mod_mod_of_dvd _ ⟨n, (two_mul n).symm⟩, ← Nat.odd_iff, Nat.odd_add_one,
    Nat.not_odd_iff_even]

Premises used: Nat.odd_add_one, two_mul, Nat.not_odd_iff_even, Nat.mod_mod_of_dvd, Exists.intro, Eq.symm, Nat.odd_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
inst : NeZero (n + n)
l : Fin (n + n)
⊢ Even (2 * (↑l : ℕ))

Tactic:
simp
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
⊢ Even k ↔ Odd n ∨ Even (↑k : ℕ)

Tactic:
⟨fun hk ↦ ?_, or_imp.mpr ⟨(even_of_odd · k), even_of_val⟩⟩

Premises used: Iff.mpr, Fin.even_of_odd, or_imp, Fin.even_of_val, And.intro, Iff.intro
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
refine : ∀ (hk : Even k), Odd n ∨ Even (↑k : ℕ)
⊢ Even k ↔ Odd n ∨ Even (↑k : ℕ)

Tactic:
refine ⟨fun hk ↦ ?_, or_imp.mpr ⟨(even_of_odd · k), even_of_val⟩⟩
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
hk : Even k
rw : Even n → Even (↑k : ℕ)
⊢ Odd n ∨ Even (↑k : ℕ)

Tactic:
rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]

Premises used: Nat.not_even_iff_odd, imp_iff_not_or
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
hk : Even k
⊢ Even n → Even (↑k : ℕ)

Tactic:
fun hn ↦ (even_iff_of_even hn).mp hk

Premises used: Iff.mp, Fin.even_iff_of_even
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
hk : Even k
⊢ Even n → Even (↑k : ℕ)

Tactic:
exact fun hn ↦ (even_iff_of_even hn).mp hk

Premises used: Iff.mp, Fin.even_iff_of_even
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
rw : Even k ↔ Odd n ∨ Even (↑k : ℕ)
⊢ Even k ↔ Even n → Even (↑k : ℕ)

Tactic:
rw [imp_iff_not_or, Nat.not_even_iff_odd]

Premises used: Nat.not_even_iff_odd, imp_iff_not_or
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
⊢ Even k ↔ Odd n ∨ Even (↑k : ℕ)

Tactic:
even_iff

Premises used: Fin.even_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
⊢ Even k ↔ Odd n ∨ Even (↑k : ℕ)

Tactic:
exact even_iff

Premises used: Fin.even_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
⊢ Odd k ↔ Odd n ∨ Odd (↑k : ℕ)

Tactic:
⟨fun hk ↦ ?_, or_imp.mpr ⟨(odd_of_odd · k), odd_of_val⟩⟩

Premises used: Iff.mpr, Fin.odd_of_val, or_imp, And.intro, Iff.intro, Fin.odd_of_odd
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
refine : ∀ (hk : Odd k), Odd n ∨ Odd (↑k : ℕ)
⊢ Odd k ↔ Odd n ∨ Odd (↑k : ℕ)

Tactic:
refine ⟨fun hk ↦ ?_, or_imp.mpr ⟨(odd_of_odd · k), odd_of_val⟩⟩
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hk : Odd k
rw : Even n → Odd (↑k : ℕ)
⊢ Odd n ∨ Odd (↑k : ℕ)

Tactic:
rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]

Premises used: Nat.not_even_iff_odd, imp_iff_not_or
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hk : Odd k
⊢ Even n → Odd (↑k : ℕ)

Tactic:
fun hn ↦ (odd_iff_of_even hn).mp hk

Premises used: Fin.odd_iff_of_even, Iff.mp
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hk : Odd k
⊢ Even n → Odd (↑k : ℕ)

Tactic:
exact fun hn ↦ (odd_iff_of_even hn).mp hk

Premises used: Fin.odd_iff_of_even, Iff.mp
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
rw : Odd k ↔ Odd n ∨ Odd (↑k : ℕ)
⊢ Odd k ↔ Even n → Odd (↑k : ℕ)

Tactic:
rw [imp_iff_not_or, Nat.not_even_iff_odd]

Premises used: Nat.not_even_iff_odd, imp_iff_not_or
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
⊢ Odd k ↔ Odd n ∨ Odd (↑k : ℕ)

Tactic:
odd_iff

Premises used: Fin.odd_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
⊢ Odd k ↔ Odd n ∨ Odd (↑k : ℕ)

Tactic:
exact odd_iff

Premises used: Fin.odd_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
hn : Even n
rw : Even (↑k : ℕ) ↔ (↑k : ℕ) % 2 = 0
⊢ Even k ↔ (↑k : ℕ) % 2 = 0

Tactic:
rw [even_iff_of_even hn]

Premises used: Fin.even_iff_of_even
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
hn : Even n
⊢ Even (↑k : ℕ) ↔ (↑k : ℕ) % 2 = 0

Tactic:
Nat.even_iff

Premises used: Nat.even_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
hn : Even n
⊢ Even (↑k : ℕ) ↔ (↑k : ℕ) % 2 = 0

Tactic:
exact Nat.even_iff

Premises used: Nat.even_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
rw : Odd (↑k : ℕ) ↔ (↑k : ℕ) % 2 = 1
⊢ Odd k ↔ (↑k : ℕ) % 2 = 1

Tactic:
rw [odd_iff_of_even hn]

Premises used: Fin.odd_iff_of_even
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ Odd (↑k : ℕ) ↔ (↑k : ℕ) % 2 = 1

Tactic:
Nat.odd_iff

Premises used: Nat.odd_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ Odd (↑k : ℕ) ↔ (↑k : ℕ) % 2 = 1

Tactic:
exact Nat.odd_iff

Premises used: Nat.odd_iff
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
rw : ¬Odd (↑k : ℕ) ↔ Even (↑k : ℕ)
⊢ ¬Odd k ↔ Even k

Tactic:
rw [even_iff_of_even hn, odd_iff_of_even hn]

Premises used: Fin.odd_iff_of_even, Fin.even_iff_of_even
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ ¬Odd (↑k : ℕ) ↔ Even (↑k : ℕ)

Tactic:
Nat.not_odd_iff_even

Premises used: Nat.not_odd_iff_even
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ ¬Odd (↑k : ℕ) ↔ Even (↑k : ℕ)

Tactic:
exact Nat.not_odd_iff_even

Premises used: Nat.not_odd_iff_even
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
rw : ¬Even (↑k : ℕ) ↔ Odd (↑k : ℕ)
⊢ ¬Even k ↔ Odd k

Tactic:
rw [even_iff_of_even hn, odd_iff_of_even hn]

Premises used: Fin.odd_iff_of_even, Fin.even_iff_of_even
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ ¬Even (↑k : ℕ) ↔ Odd (↑k : ℕ)

Tactic:
Nat.not_even_iff_odd

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ ¬Even (↑k : ℕ) ↔ Odd (↑k : ℕ)

Tactic:
exact Nat.not_even_iff_odd

Premises used: Nat.not_even_iff_odd
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
⊢ Odd (k + 1) ↔ Even k

Tactic:
⟨fun ⟨k, hk⟩ ↦ add_right_cancel hk ▸ even_two_mul k, Even.add_one⟩

Premises used: Even.add_one, _private.0.Fin.odd_add_one_iff_even.match_1, Eq.rec, add_right_cancel, even_two_mul, Even, Iff.intro, Eq.symm
-- Module: Mathlib.Data.Fin.Parity
Goal:
n : ℕ
k : Fin n
inst : NeZero n
⊢ Even (k + 1) ↔ Odd k

Tactic:
⟨fun ⟨k, hk⟩ ↦ eq_sub_iff_add_eq.mpr hk ▸ (Even.add_self k).sub_odd odd_one, Odd.add_one⟩

Premises used: Iff.mpr, Even.add_self, Odd, eq_sub_iff_add_eq, Even.sub_odd, Eq.rec, _private.0.Fin.even_add_one_iff_odd.match_1, odd_one, Iff.intro, Odd.add_one, Eq.symm
-- Module: Mathlib.Data.Fin.Pigeonhole
Goal:
m n : ℕ
f : Fin m → Fin n
hf : Function.Injective f
⊢ m ≤ n

Tactic:
simpa using Fintype.card_le_of_injective f hf

Premises used: Fintype.card_le_of_injective