awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.FlagRange (hypothesis)
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
⊢ IsMaxChain (fun (x1 x2 : α) ↦ x1 ≤ x2) (range f)
have hmono : Monotone f
Tactic: have hmono : Monotone f := Fin.monotone_iff_le_succ.2 fun k ↦ (hcovBy k).1
-- Lean 4 proof step from Mathlib.Data.Fin.FlagRange (goal)
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)
have refine : ∀ (t : Set α) (htc : IsChain (fun (x1 x2 : α) ↦ x1 ≤ x2) t) (hbt : range f ⊆ t) (x : α) (hx : x ∈ t), x ∈ range f
Tactic: refine ⟨hmono.isChain_range, fun t htc hbt ↦ hbt.antisymm fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Fin.FlagRange (goal)
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
⊢ ∃ (y : Fin (n + 1)), f y = x
have by_contra! : ∀ (h : ∀ (y : Fin (n + 1)), f y ≠ x), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Data.Fin.FlagRange (goal)
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
⊢ False
have suffices : ∀ (k : Fin (n + 1)), f k < x
Tactic: suffices ∀ k, f k < x by simpa [hlast] using this (.last _)
-- Lean 4 proof step from Mathlib.Data.Fin.FlagRange (goal)
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
⊢ f k.succ < x
have 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
Tactic: rw [range_subset_iff] at hbt
Cleared hypotheses: hbt, x, hx, h, k, ihk
-- Lean 4 proof step from Mathlib.Data.Fin.FlagRange (goal)
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)
⊢ f k < x
have zero : f 0 < 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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Fin.FlagRange (goal)
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
⊢ f k < x
have succ : ∀ (k : Fin n) (ihk : f k.castSucc < x), f k.succ < 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)
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
have inl : ∀ (hji : j.castSucc < i), Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
Tactic: rcases lt_or_ge j.castSucc i with hji | hij
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
inl : ∀ (hji : j.castSucc < i), Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
have inr : ∀ (hij : i ≤ j.castSucc), Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
Tactic: rcases lt_or_ge j.castSucc i with hji | hij
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (hypothesis)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
hji : j.castSucc < i
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
have this : 1 ≤ (↑i : ℕ)
Tactic: have : 1 ≤ (i : ℕ) := (Nat.zero_le j).trans_lt hji
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
R : Type u_1
inst : Monoid R
inst_1 : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
⊢ HPow.hPow (α := R) (-1) ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) =
    -HPow.hPow (α := R) (-1) ((↑i : ℕ) + (↑j : ℕ))
have rw : Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Even ((↑i : ℕ) + (↑j : ℕ) + 1)
Tactic: rw [← neg_one_mul (_ ^ _), ← pow_succ', neg_one_pow_congr]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
R : Type u_1
inst : Monoid R
inst_1 : HasDistribNeg R
i : Fin (n + 1)
j : Fin n
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Even ((↑i : ℕ) + (↑j : ℕ) + 1)
have rw : Odd ((↑i : ℕ) + (↑j : ℕ)) ↔ Even ((↑i : ℕ) + (↑j : ℕ) + 1)
Tactic: rw [even_succAbove_add_predAbove, Nat.even_add_one, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
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)
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Even ((↑i : ℕ) + (↑j : ℕ) + 1)
have rw₁ : Odd ((↑i : ℕ) + (↑j : ℕ)) ↔ ¬Even ((↑i : ℕ) + (↑j : ℕ))
Tactic: rw [even_succAbove_add_predAbove, Nat.even_add_one, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
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 : ℕ))
⊢ Even ((↑(i.succAbove j) : ℕ) + (↑(j.predAbove i) : ℕ)) ↔ Even ((↑i : ℕ) + (↑j : ℕ) + 1)
have rw₂ : Odd ((↑i : ℕ) + (↑j : ℕ)) ↔ Odd ((↑i : ℕ) + (↑j : ℕ))
Tactic: rw [even_succAbove_add_predAbove, Nat.even_add_one, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (hypothesis)
Goal:
n : ℕ
k : Fin n
h : Even (↑k : ℕ)
⊢ Even k
have this : NeZero n
Tactic: have : NeZero n := ⟨k.pos.ne'⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
h : Even (↑k : ℕ)
this : NeZero n
⊢ Even k
have rw : Even (α := Fin n) (↑(↑k : ℕ) : Fin n)
Tactic: rw [← Fin.cast_val_eq_self k]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
inst : NeZero n
h : Odd (↑k : ℕ)
⊢ Odd k
have rw : Odd (α := Fin n) (↑(↑k : ℕ) : Fin n)
Tactic: rw [← Fin.cast_val_eq_self k]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (hypothesis)
Goal:
n : ℕ
hn : Odd n
k : Fin n
⊢ Even k
have this : NeZero n
Tactic: have : NeZero n := ⟨k.pos.ne'⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
⊢ Even k
have inl : ∀ (hk : Even (↑k : ℕ)), Even k
Tactic: rcases k.val.even_or_odd with hk | hk
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
hn : Odd n
k : Fin n
this : NeZero n
inl : ∀ (hk : Even (↑k : ℕ)), Even k
⊢ Even k
have inr : ∀ (hk : Odd (↑k : ℕ)), Even k
Tactic: rcases k.val.even_or_odd with hk | hk
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
inst : NeZero n
hn : Odd n
k : Fin n
⊢ Odd k
have inl : ∀ (hk : Even (↑k : ℕ)), Odd k
Tactic: rcases k.val.even_or_odd with hk | hk
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
inst : NeZero n
hn : Odd n
k : Fin n
inl : ∀ (hk : Even (↑k : ℕ)), Odd k
⊢ Odd k
have inr : ∀ (hk : Odd (↑k : ℕ)), Odd k
Tactic: rcases k.val.even_or_odd with hk | hk
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
hn : Even n
⊢ Even k ↔ Even (↑k : ℕ)
have rcases : ∀ (n : ℕ) {k : Fin (n + n)}, Even k ↔ Even (↑k : ℕ)
Tactic: rcases hn with ⟨n, rfl⟩
Cleared hypotheses: n, k, hn
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin (n + n)
⊢ Even k ↔ Even (↑k : ℕ)
have refine : Even k → Even (↑k : ℕ)
Tactic: refine ⟨?_, even_of_val⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
l : Fin (n + n)
⊢ Even (↑(l + l) : ℕ)
have rw : Even (if n + n ≤ (↑l : ℕ) + (↑l : ℕ) then (↑l : ℕ) + (↑l : ℕ) - (n + n) else (↑l : ℕ) + (↑l : ℕ))
Tactic: rw [val_add_eq_ite]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
l : Fin (n + n)
⊢ Even (if n + n ≤ (↑l : ℕ) + (↑l : ℕ) then (↑l : ℕ) + (↑l : ℕ) - (n + n) else (↑l : ℕ) + (↑l : ℕ))
have pos : ∀ (h : n + n ≤ (↑l : ℕ) + (↑l : ℕ)), Even ((↑l : ℕ) + (↑l : ℕ) - (n + n))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
l : Fin (n + n)
pos : ∀ (h : n + n ≤ (↑l : ℕ) + (↑l : ℕ)), Even ((↑l : ℕ) + (↑l : ℕ) - (n + n))
⊢ Even (if n + n ≤ (↑l : ℕ) + (↑l : ℕ) then (↑l : ℕ) + (↑l : ℕ) - (n + n) else (↑l : ℕ) + (↑l : ℕ))
have neg : ∀ (h : ¬n + n ≤ (↑l : ℕ) + (↑l : ℕ)), Even ((↑l : ℕ) + (↑l : ℕ))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ Odd k ↔ Odd (↑k : ℕ)
have rcases : ∀ (n : ℕ) {k : Fin (n + n)} [inst : NeZero (n + n)], Odd k ↔ Odd (↑k : ℕ)
Tactic: rcases hn with ⟨n, rfl⟩
Cleared hypotheses: n, k, inst, hn
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin (n + n)
inst : NeZero (n + n)
⊢ Odd k ↔ Odd (↑k : ℕ)
have refine : Odd k → Odd (↑k : ℕ)
Tactic: refine ⟨?_, odd_of_val⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
inst : NeZero (n + n)
l : Fin (n + n)
⊢ Odd (↑(2 * l + 1) : ℕ)
have rw : Odd ((2 % (n + n) * (↑l : ℕ) % (n + n) + 1 % (n + n)) % (n + n))
Tactic: rw [val_add, val_mul, coe_ofNat_eq_mod, coe_ofNat_eq_mod]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
inst : NeZero (n + n)
l : Fin (n + n)
⊢ Odd ((2 % (n + n) * (↑l : ℕ) % (n + n) + 1 % (n + n)) % (n + n))
have simp : (2 * (↑l : ℕ) + 1) % (n + n) % 2 = 1
Tactic: simp only [Nat.mod_mul_mod, Nat.add_mod_mod, Nat.mod_add_mod, Nat.odd_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
inst : NeZero (n + n)
l : Fin (n + n)
⊢ (2 * (↑l : ℕ) + 1) % (n + n) % 2 = 1
have rw : Even (2 * (↑l : ℕ))
Tactic: rw [Nat.mod_mod_of_dvd _ ⟨n, (two_mul n).symm⟩, ← Nat.odd_iff, Nat.odd_add_one,
    Nat.not_odd_iff_even]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
⊢ Even k ↔ Odd n ∨ Even (↑k : ℕ)
have refine : ∀ (hk : Even k), Odd n ∨ Even (↑k : ℕ)
Tactic: refine ⟨fun hk ↦ ?_, or_imp.mpr ⟨(even_of_odd · k), even_of_val⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
hk : Even k
⊢ Odd n ∨ Even (↑k : ℕ)
have rw : Even n → Even (↑k : ℕ)
Tactic: rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
⊢ Even k ↔ Even n → Even (↑k : ℕ)
have rw : Even k ↔ Odd n ∨ Even (↑k : ℕ)
Tactic: rw [imp_iff_not_or, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
inst : NeZero n
⊢ Odd k ↔ Odd n ∨ Odd (↑k : ℕ)
have refine : ∀ (hk : Odd k), Odd n ∨ Odd (↑k : ℕ)
Tactic: refine ⟨fun hk ↦ ?_, or_imp.mpr ⟨(odd_of_odd · k), odd_of_val⟩⟩
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hk : Odd k
⊢ Odd n ∨ Odd (↑k : ℕ)
have rw : Even n → Odd (↑k : ℕ)
Tactic: rw [← Nat.not_even_iff_odd, ← imp_iff_not_or]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
inst : NeZero n
⊢ Odd k ↔ Even n → Odd (↑k : ℕ)
have rw : Odd k ↔ Odd n ∨ Odd (↑k : ℕ)
Tactic: rw [imp_iff_not_or, Nat.not_even_iff_odd]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
hn : Even n
⊢ Even k ↔ (↑k : ℕ) % 2 = 0
have rw : Even (↑k : ℕ) ↔ (↑k : ℕ) % 2 = 0
Tactic: rw [even_iff_of_even hn]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ Odd k ↔ (↑k : ℕ) % 2 = 1
have rw : Odd (↑k : ℕ) ↔ (↑k : ℕ) % 2 = 1
Tactic: rw [odd_iff_of_even hn]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ ¬Odd k ↔ Even k
have rw : ¬Odd (↑k : ℕ) ↔ Even (↑k : ℕ)
Tactic: rw [even_iff_of_even hn, odd_iff_of_even hn]
-- Lean 4 proof step from Mathlib.Data.Fin.Parity (goal)
Goal:
n : ℕ
k : Fin n
inst : NeZero n
hn : Even n
⊢ ¬Even k ↔ Odd k
have rw : ¬Even (↑k : ℕ) ↔ Odd (↑k : ℕ)
Tactic: rw [even_iff_of_even hn, odd_iff_of_even hn]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n m : ℕ
i : Fin n
h : n = m
⊢ Fin.cast h i.rev = (Fin.cast h i).rev
have subst : Fin.cast sorry i.rev = (Fin.cast sorry i).rev
Tactic: subst h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
⊢ i.rev = j ↔ i = j.rev
have rw : i.rev.rev = j.rev ↔ i = j.rev
Tactic: rw [← rev_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
rw : i.rev.rev = j.rev ↔ i = j.rev
⊢ i.rev = j ↔ i = j.rev
have rw₁ : i = j.rev ↔ i = j.rev
Tactic: rw [← rev_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
⊢ i.rev < j ↔ j.rev < i
have rw : j.rev < i.rev.rev ↔ j.rev < i
Tactic: rw [← rev_lt_rev, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
rw : j.rev < i.rev.rev ↔ j.rev < i
⊢ i.rev < j ↔ j.rev < i
have rw₁ : j.rev < i ↔ j.rev < i
Tactic: rw [← rev_lt_rev, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
⊢ i.rev ≤ j ↔ j.rev ≤ i
have rw : j.rev ≤ i.rev.rev ↔ j.rev ≤ i
Tactic: rw [← rev_le_rev, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
rw : j.rev ≤ i.rev.rev ↔ j.rev ≤ i
⊢ i.rev ≤ j ↔ j.rev ≤ i
have rw₁ : j.rev ≤ i ↔ j.rev ≤ i
Tactic: rw [← rev_le_rev, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
⊢ i < j.rev ↔ j < i.rev
have rw : j.rev.rev < i.rev ↔ j < i.rev
Tactic: rw [← rev_lt_rev, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
rw : j.rev.rev < i.rev ↔ j < i.rev
⊢ i < j.rev ↔ j < i.rev
have rw₁ : j < i.rev ↔ j < i.rev
Tactic: rw [← rev_lt_rev, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
⊢ i ≤ j.rev ↔ j ≤ i.rev
have rw : j.rev.rev ≤ i.rev ↔ j ≤ i.rev
Tactic: rw [← rev_le_rev, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i j : Fin n
rw : j.rev.rev ≤ i.rev ↔ j ≤ i.rev
⊢ i ≤ j.rev ↔ j ≤ i.rev
have rw₁ : j ≤ i.rev ↔ j ≤ i.rev
Tactic: rw [← rev_le_rev, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h : i ≠ 0
h' : i.rev ≠ last n
⊢ (i.pred h).rev = i.rev.castPred h'
have rw : (i.pred h).rev.castSucc = (i.rev.castPred h').castSucc
Tactic: rw [← castSucc_inj, castSucc_castPred, ← rev_succ, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ (i.pred h).rev = i.rev.castPred h'
have rw₁ : (i.pred h).rev.castSucc = i.rev
Tactic: rw [← castSucc_inj, castSucc_castPred, ← rev_succ, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ (i.pred h).rev = i.rev.castPred h'
have rw₂ : (i.pred h).succ.rev = i.rev
Tactic: rw [← castSucc_inj, castSucc_castPred, ← rev_succ, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ (i.pred h).rev = i.rev.castPred h'
have rw₃ : i.rev = i.rev
Tactic: rw [← castSucc_inj, castSucc_castPred, ← rev_succ, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
h' : i.rev ≠ 0
⊢ (i.castPred h).rev = i.rev.pred h'
have rw : (i.castPred h).rev.succ = (i.rev.pred h').succ
Tactic: rw [← succ_inj, succ_pred, ← rev_castSucc, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ (i.castPred h).rev = i.rev.pred h'
have rw₁ : (i.castPred h).rev.succ = i.rev
Tactic: rw [← succ_inj, succ_pred, ← rev_castSucc, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ (i.castPred h).rev = i.rev.pred h'
have rw₂ : (i.castPred h).castSucc.rev = i.rev
Tactic: rw [← succ_inj, succ_pred, ← rev_castSucc, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ (i.castPred h).rev = i.rev.pred h'
have rw₃ : i.rev = i.rev
Tactic: rw [← succ_inj, succ_pred, ← rev_castSucc, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inl : ∀ (h : i.succ ≤ p.rev), p.rev.succAbove i = (p.succAbove i.rev).rev
Tactic: obtain h | h := (rev p).succ_le_or_le_castSucc i
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
inl : ∀ (h : i.succ ≤ p.rev), p.rev.succAbove i = (p.succAbove i.rev).rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inr : ∀ (h : p.rev ≤ i.castSucc), p.rev.succAbove i = (p.succAbove i.rev).rev
Tactic: obtain h | h := (rev p).succ_le_or_le_castSucc i
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inl : i.castSucc = (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]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p.rev
inl : i.castSucc = (p.succAbove i.rev).rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inl₁ : i.castSucc = i.rev.succ.rev
Tactic: rw [succAbove_of_succ_le _ _ h,
      succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inl₂ : i.castSucc = i.rev.rev.castSucc
Tactic: rw [succAbove_of_succ_le _ _ h,
      succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inl₃ : i.castSucc = i.castSucc
Tactic: rw [succAbove_of_succ_le _ _ h,
      succAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), rev_succ, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inr : i.succ = (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]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p.rev ≤ i.castSucc
inr : i.succ = (p.succAbove i.rev).rev
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inr₁ : i.succ = i.rev.castSucc.rev
Tactic: rw [succAbove_of_le_castSucc _ _ h,
      succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inr₂ : i.succ = i.rev.rev.succ
Tactic: rw [succAbove_of_le_castSucc _ _ h,
      succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
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
⊢ p.rev.succAbove i = (p.succAbove i.rev).rev
have inr₃ : i.succ = i.succ
Tactic: rw [succAbove_of_le_castSucc _ _ h,
      succAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), rev_castSucc, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i.rev = (p.rev.succAbove i).rev
have rw : p.succAbove i.rev = (p.succAbove i.rev).rev.rev
Tactic: rw [succAbove_rev_left, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : p.succAbove i.rev = (p.succAbove i.rev).rev.rev
⊢ p.succAbove i.rev = (p.rev.succAbove i).rev
have rw₁ : p.succAbove i.rev = p.succAbove i.rev
Tactic: rw [succAbove_rev_left, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ (p.succAbove i).rev = p.rev.succAbove i.rev
have rw : (p.succAbove i).rev = (p.succAbove i.rev.rev).rev
Tactic: rw [succAbove_rev_left, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : (p.succAbove i).rev = (p.succAbove i.rev.rev).rev
⊢ (p.succAbove i).rev = p.rev.succAbove i.rev
have rw₁ : (p.succAbove i).rev = (p.succAbove i).rev
Tactic: rw [succAbove_rev_left, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inl : ∀ (h : p.succ ≤ i.rev), p.rev.predAbove i = (p.predAbove i.rev).rev
Tactic: obtain h | h := (rev i).succ_le_or_le_castSucc p
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
inl : ∀ (h : p.succ ≤ i.rev), p.rev.predAbove i = (p.predAbove i.rev).rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inr : ∀ (h : i.rev ≤ p.castSucc), p.rev.predAbove i = (p.predAbove i.rev).rev
Tactic: obtain h | h := (rev i).succ_le_or_le_castSucc p
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inl : p.rev.predAbove i = (i.rev.pred sorry).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]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
inl : p.rev.predAbove i = (i.rev.pred ⋯).rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inl₁ : p.rev.predAbove i = i.rev.rev.castPred sorry
Tactic: rw [predAbove_of_succ_le _ _ h, rev_pred,
      predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]