internlm/Lean-Github huggingface dataset:
Theorem: Fin.list_length_le_of_nodup
Proof state before:
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l : List (Fin (Nat.succ n))
nodup : List.Nodup l
hn : ¬last n ∈ l
l' : List (Fin n)
hl' : l = List.map castSucc l'
⊢ List.length l ≤ Nat.succ n
Tactic:
cases hl'
Proof state after:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.length (List.map castSucc l') ≤ Nat.succ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.length (List.map castSucc l') ≤ Nat.succ n
Tactic:
rewrite [List.length_map]
Proof state after:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.length l' ≤ Nat.succ n
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.length l' ≤ Nat.succ n
Tactic:
refine trans (IH ?_) (n.le_succ)
Proof state after:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.Nodup l'
Theorem: Fin.list_length_le_of_nodup
Proof state before:
case refl
m n✝ n : Nat
IH : ∀ {l : List (Fin n)}, List.Nodup l → List.length l ≤ n
l' : List (Fin n)
nodup : List.Nodup (List.map castSucc l')
hn : ¬last n ∈ List.map castSucc l'
⊢ List.Nodup l'
Tactic:
exact List.nodup_of_nodup_map nodup
Proof state after:
no goals
Theorem: Fin.rlexProd_val_div
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(rlexProd i j) / m = ↑j
Tactic:
dsimp [rlexProd]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ (↑i + m * ↑j) / m = ↑j
Theorem: Fin.rlexProd_val_div
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ (↑i + m * ↑j) / m = ↑j
Tactic:
rewrite [Nat.add_mul_div_left _ _ i.pos, Nat.div_eq_of_lt i.2]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ 0 + ↑j = ↑j
Theorem: Fin.rlexProd_val_div
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ 0 + ↑j = ↑j
Tactic:
exact j.1.zero_add
Proof state after:
no goals
Theorem: Fin.rlexProd_val_mod
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ ↑(rlexProd i j) % m = ↑i
Tactic:
dsimp [rlexProd]
Proof state after:
m n : Nat
i : Fin m
j : Fin n
⊢ (↑i + m * ↑j) % m = ↑i
Theorem: Fin.rlexProd_val_mod
Proof state before:
m n : Nat
i : Fin m
j : Fin n
⊢ (↑i + m * ↑j) % m = ↑i
Tactic:
rw [Nat.add_mul_mod_self_left, Nat.mod_eq_of_lt i.2]
Proof state after:
no goals
Theorem: Fin.rlexProd_inj
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ i₁ = i₂ ∧ j₁ = j₂
Tactic:
constructor <;> ext
Proof state after:
case left.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑i₁ = ↑i₂

case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂
Theorem: Fin.rlexProd_inj
Proof state before:
case left.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑i₁ = ↑i₂

case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂
Tactic:
. rw [← rlexProd_val_mod (i:=i₁) (j:=j₁), ← rlexProd_val_mod (i:=i₂) (j:= j₂), h]
Proof state after:
case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂
Theorem: Fin.rlexProd_inj
Proof state before:
case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂
Tactic:
. rw [← rlexProd_val_div (i:=i₁) (j:=j₁), ← rlexProd_val_div (i:=i₂) (j:= j₂), h]
Proof state after:
no goals
Theorem: Fin.rlexProd_inj
Proof state before:
case left.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑i₁ = ↑i₂
Tactic:
rw [← rlexProd_val_mod (i:=i₁) (j:=j₁), ← rlexProd_val_mod (i:=i₂) (j:= j₂), h]
Proof state after:
no goals
Theorem: Fin.rlexProd_inj
Proof state before:
case right.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : rlexProd i₁ j₁ = rlexProd i₂ j₂
⊢ ↑j₁ = ↑j₂
Tactic:
rw [← rlexProd_val_div (i:=i₁) (j:=j₁), ← rlexProd_val_div (i:=i₂) (j:= j₂), h]
Proof state after:
no goals
Theorem: Fin.rlexProd_lt_of_snd
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ rlexProd i₁ j₁ < rlexProd i₂ j₂
Tactic:
calc i₁.1 + m * j₁.1
  _ < m + m * j₁.1 := Nat.add_lt_add_right i₁.2 _
  _ = m * (j₁.1 + 1) := by rewrite [Nat.add_comm m]; rfl
  _ ≤ m * j₂.1 := Nat.mul_le_mul_left m h
  _ ≤ i₂.1 + m * j₂.1 := Nat.le_add_left ..
Proof state after:
no goals
Theorem: Fin.rlexProd_lt_of_snd
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ m + m * ↑j₁ = m * (↑j₁ + 1)
Tactic:
rewrite [Nat.add_comm m]
Proof state after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ m * ↑j₁ + m = m * (↑j₁ + 1)
Theorem: Fin.rlexProd_lt_of_snd
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
h : j₁ < j₂
⊢ m * ↑j₁ + m = m * (↑j₁ + 1)
Tactic:
rfl
Proof state after:
no goals
Theorem: Fin.rlexProd_lt_iff
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ rlexProd i₁ j₁ < rlexProd i₂ j₂ ↔ j₁ < j₂ ∨ j₁ = j₂ ∧ i₁ < i₂
Tactic:
dsimp [rlexProd]
Proof state after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ { val := ↑i₁ + m * ↑j₁, isLt := (_ : ↑i₁ + m * ↑j₁ < m * n) } <
      { val := ↑i₂ + m * ↑j₂, isLt := (_ : ↑i₂ + m * ↑j₂ < m * n) } ↔
    j₁ < j₂ ∨ j₁ = j₂ ∧ i₁ < i₂
Theorem: Fin.rlexProd_lt_iff
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ { val := ↑i₁ + m * ↑j₁, isLt := (_ : ↑i₁ + m * ↑j₁ < m * n) } <
      { val := ↑i₂ + m * ↑j₂, isLt := (_ : ↑i₂ + m * ↑j₂ < m * n) } ↔
    j₁ < j₂ ∨ j₁ = j₂ ∧ i₁ < i₂
Tactic:
simp only [Fin.lt_def]
Proof state after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Theorem: Fin.rlexProd_lt_iff
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
if hj : j₁.1 < j₂.1 then
  simp only [hj, true_or, iff_true]
  exact rlexProd_lt_of_snd i₁ i₂ hj
else
  simp only [hj, false_or]
  rewrite [Nat.not_lt] at hj
  cases Nat.eq_or_lt_of_le hj with
  | inl heq =>
    cases Fin.eq_of_val_eq heq
    simp only [true_and]
    exact Nat.add_lt_add_iff_right _ i₁.1 i₂.1
  | inr hlt =>
    have : j₁ ≠ j₂ := fun h =>
      Nat.lt_irrefl _ (h ▸ hlt)
    simp only [this, false_and, iff_false, Nat.not_lt]
    apply Nat.le_of_lt
    exact rlexProd_lt_of_snd i₂ i₁ hlt
Proof state after:
no goals
Theorem: Fin.rlexProd_lt_iff
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
simp only [hj, true_or, iff_true]
Proof state after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂
Theorem: Fin.rlexProd_lt_iff
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂
Tactic:
exact rlexProd_lt_of_snd i₁ i₂ hj
Proof state after:
no goals
Theorem: Fin.rlexProd_lt_iff
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ¬↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ ↑j₁ < ↑j₂ ∨ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
simp only [hj, false_or]
Proof state after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ¬↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Theorem: Fin.rlexProd_lt_iff
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ¬↑j₁ < ↑j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
rewrite [Nat.not_lt] at hj
Proof state after:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Theorem: Fin.rlexProd_lt_iff
Proof state before:
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
cases Nat.eq_or_lt_of_le hj with
| inl heq =>
  cases Fin.eq_of_val_eq heq
  simp only [true_and]
  exact Nat.add_lt_add_iff_right _ i₁.1 i₂.1
| inr hlt =>
  have : j₁ ≠ j₂ := fun h =>
    Nat.lt_irrefl _ (h ▸ hlt)
  simp only [this, false_and, iff_false, Nat.not_lt]
  apply Nat.le_of_lt
  exact rlexProd_lt_of_snd i₂ i₁ hlt
Proof state after:
no goals
Theorem: Fin.rlexProd_lt_iff
Proof state before:
case inl
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
heq : ↑j₂ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
cases Fin.eq_of_val_eq heq
Proof state after:
case inl.refl
m n : Nat
i₁ i₂ : Fin m
j₁ : Fin n
hj : ↑j₁ ≤ ↑j₁
heq : ↑j₁ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₁ ↔ j₁ = j₁ ∧ ↑i₁ < ↑i₂
Theorem: Fin.rlexProd_lt_iff
Proof state before:
case inl.refl
m n : Nat
i₁ i₂ : Fin m
j₁ : Fin n
hj : ↑j₁ ≤ ↑j₁
heq : ↑j₁ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₁ ↔ j₁ = j₁ ∧ ↑i₁ < ↑i₂
Tactic:
simp only [true_and]
Proof state after:
case inl.refl
m n : Nat
i₁ i₂ : Fin m
j₁ : Fin n
hj : ↑j₁ ≤ ↑j₁
heq : ↑j₁ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₁ ↔ ↑i₁ < ↑i₂
Theorem: Fin.rlexProd_lt_iff
Proof state before:
case inl.refl
m n : Nat
i₁ i₂ : Fin m
j₁ : Fin n
hj : ↑j₁ ≤ ↑j₁
heq : ↑j₁ = ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₁ ↔ ↑i₁ < ↑i₂
Tactic:
exact Nat.add_lt_add_iff_right _ i₁.1 i₂.1
Proof state after:
no goals
Theorem: Fin.rlexProd_lt_iff
Proof state before:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
have : j₁ ≠ j₂ := fun h =>
  Nat.lt_irrefl _ (h ▸ hlt)
Proof state after:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Theorem: Fin.rlexProd_lt_iff
Proof state before:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₁ + m * ↑j₁ < ↑i₂ + m * ↑j₂ ↔ j₁ = j₂ ∧ ↑i₁ < ↑i₂
Tactic:
simp only [this, false_and, iff_false, Nat.not_lt]
Proof state after:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₂ + m * ↑j₂ ≤ ↑i₁ + m * ↑j₁
Theorem: Fin.rlexProd_lt_iff
Proof state before:
case inr
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₂ + m * ↑j₂ ≤ ↑i₁ + m * ↑j₁
Tactic:
apply Nat.le_of_lt
Proof state after:
case inr.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₂ + m * ↑j₂ < ↑i₁ + m * ↑j₁
Theorem: Fin.rlexProd_lt_iff
Proof state before:
case inr.h
m n : Nat
i₁ i₂ : Fin m
j₁ j₂ : Fin n
hj : ↑j₂ ≤ ↑j₁
hlt : ↑j₂ < ↑j₁
this : j₁ ≠ j₂
⊢ ↑i₂ + m * ↑j₂ < ↑i₁ + m * ↑j₁
Tactic:
exact rlexProd_lt_of_snd i₂ i₁ hlt
Proof state after:
no goals
Theorem: Fin.OrbitChain.nodup
Proof state before:
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
h : OrbitChain f i l j
⊢ List.Nodup (i :: l)
Tactic:
induction h with
| single => exact .cons (fun _ h => nomatch h) .nil
| cons hnotmem _ IH =>
  refine .cons ?_ IH
  intro _ hfa h; cases h
  exact hnotmem hfa
Proof state after:
no goals
Theorem: Fin.OrbitChain.nodup
Proof state before:
case single
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ : Fin n
⊢ List.Nodup [i✝]
Tactic:
exact .cons (fun _ h => nomatch h) .nil
Proof state after:
no goals
Theorem: Fin.OrbitChain.nodup
Proof state before:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
⊢ List.Nodup (f i✝ :: i✝ :: l✝)
Tactic:
refine .cons ?_ IH
Proof state after:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
⊢ ∀ (a' : Fin n), a' ∈ i✝ :: l✝ → f i✝ ≠ a'
Theorem: Fin.OrbitChain.nodup
Proof state before:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
⊢ ∀ (a' : Fin n), a' ∈ i✝ :: l✝ → f i✝ ≠ a'
Tactic:
intro _ hfa h
Proof state after:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
a'✝ : Fin n
hfa : a'✝ ∈ i✝ :: l✝
h : f i✝ = a'✝
⊢ False
Theorem: Fin.OrbitChain.nodup
Proof state before:
case cons
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
a'✝ : Fin n
hfa : a'✝ ∈ i✝ :: l✝
h : f i✝ = a'✝
⊢ False
Tactic:
cases h
Proof state after:
case cons.refl
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
hfa : f i✝ ∈ i✝ :: l✝
⊢ False
Theorem: Fin.OrbitChain.nodup
Proof state before:
case cons.refl
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
i✝ j✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j✝
IH : List.Nodup (i✝ :: l✝)
hfa : f i✝ ∈ i✝ :: l✝
⊢ False
Tactic:
exact hnotmem hfa
Proof state after:
no goals
Theorem: Fin.OrbitChain.not_mem
Proof state before:
m n : Nat
f : Fin n → Fin n
i j : Fin n
l : List (Fin n)
h : OrbitChain f i l j
⊢ ¬i ∈ l
Tactic:
cases h with
| single => exact List.not_mem_nil _
| cons hnotmem _ => exact hnotmem
Proof state after:
no goals
Theorem: Fin.OrbitChain.not_mem
Proof state before:
case single
m n : Nat
f : Fin n → Fin n
i : Fin n
⊢ ¬i ∈ []
Tactic:
exact List.not_mem_nil _
Proof state after:
no goals
Theorem: Fin.OrbitChain.not_mem
Proof state before:
case cons
m n : Nat
f : Fin n → Fin n
j i✝ : Fin n
l✝ : List (Fin n)
hnotmem : ¬f i✝ ∈ i✝ :: l✝
a✝ : OrbitChain f i✝ l✝ j
⊢ ¬f i✝ ∈ i✝ :: l✝
Tactic:
exact hnotmem
Proof state after:
no goals
Theorem: Fin.OrbitChain.cycle
Proof state before:
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
i j : Fin n
l : List (Fin n)
h : OrbitChain f i l j
k : Fin n
hk : ¬k ∈ l
hfk : f k ∈ i :: l
⊢ f k = j
Tactic:
induction l generalizing i with
| nil => cases h; exact List.mem_singleton.mp hfk
| cons k' l IH =>
  cases h with | cons hfk' htail =>
  specialize IH htail (List.not_mem_of_not_mem_cons hk)
  rewrite [List.mem_cons] at hfk
  rewrite [List.mem_cons, not_or] at hk
  cases hfk with
  | inl hfkk' => exact absurd (f_inj _ _ hfkk') hk.1
  | inr h => exact IH h
Proof state after:
no goals
Theorem: Fin.OrbitChain.cycle
Proof state before:
case nil
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k i : Fin n
h : OrbitChain f i [] j
hk : ¬k ∈ []
hfk : f k ∈ [i]
⊢ f k = j
Tactic:
cases h
Proof state after:
case nil.single
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k : Fin n
hk : ¬k ∈ []
hfk : f k ∈ [j]
⊢ f k = j
Theorem: Fin.OrbitChain.cycle
Proof state before:
case nil.single
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k : Fin n
hk : ¬k ∈ []
hfk : f k ∈ [j]
⊢ f k = j
Tactic:
exact List.mem_singleton.mp hfk
Proof state after:
no goals
Theorem: Fin.OrbitChain.cycle
Proof state before:
case cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
IH : ∀ {i : Fin n}, OrbitChain f i l j → ¬k ∈ l → f k ∈ i :: l → f k = j
i : Fin n
h : OrbitChain f i (k' :: l) j
hk : ¬k ∈ k' :: l
hfk : f k ∈ i :: k' :: l
⊢ f k = j
Tactic:
cases h with | cons hfk' htail =>
specialize IH htail (List.not_mem_of_not_mem_cons hk)
rewrite [List.mem_cons] at hfk
rewrite [List.mem_cons, not_or] at hk
cases hfk with
| inl hfkk' => exact absurd (f_inj _ _ hfkk') hk.1
| inr h => exact IH h
Proof state after:
no goals
Theorem: Fin.OrbitChain.cycle
Proof state before:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
IH : ∀ {i : Fin n}, OrbitChain f i l j → ¬k ∈ l → f k ∈ i :: l → f k = j
hk : ¬k ∈ k' :: l
hfk : f k ∈ f k' :: k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
⊢ f k = j
Tactic:
specialize IH htail (List.not_mem_of_not_mem_cons hk)
Proof state after:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k ∈ k' :: l
hfk : f k ∈ f k' :: k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Theorem: Fin.OrbitChain.cycle
Proof state before:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k ∈ k' :: l
hfk : f k ∈ f k' :: k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Tactic:
rewrite [List.mem_cons] at hfk
Proof state after:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k ∈ k' :: l
hfk : f k = f k' ∨ f k ∈ k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Theorem: Fin.OrbitChain.cycle
Proof state before:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k ∈ k' :: l
hfk : f k = f k' ∨ f k ∈ k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Tactic:
rewrite [List.mem_cons, not_or] at hk
Proof state after:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k = k' ∧ ¬k ∈ l
hfk : f k = f k' ∨ f k ∈ k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Theorem: Fin.OrbitChain.cycle
Proof state before:
case cons.cons
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k = k' ∧ ¬k ∈ l
hfk : f k = f k' ∨ f k ∈ k' :: l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
⊢ f k = j
Tactic:
cases hfk with
| inl hfkk' => exact absurd (f_inj _ _ hfkk') hk.1
| inr h => exact IH h
Proof state after:
no goals
Theorem: Fin.OrbitChain.cycle
Proof state before:
case cons.cons.inl
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k = k' ∧ ¬k ∈ l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
hfkk' : f k = f k'
⊢ f k = j
Tactic:
exact absurd (f_inj _ _ hfkk') hk.1
Proof state after:
no goals
Theorem: Fin.OrbitChain.cycle
Proof state before:
case cons.cons.inr
m n : Nat
f : Fin n → Fin n
f_inj : ∀ (i j : Fin n), f i = f j → i = j
j k k' : Fin n
l : List (Fin n)
hk : ¬k = k' ∧ ¬k ∈ l
hfk' : ¬f k' ∈ k' :: l
htail : OrbitChain f k' l j
IH : f k ∈ k' :: l → f k = j
h : f k ∈ k' :: l
⊢ f k = j
Tactic:
exact IH h
Proof state after:
no goals
Theorem: Nat.decreasing_induction
Proof state before:
motive : Nat → Prop
succ : ∀ (n : Nat), motive (n + 1) → motive n
m n : Nat
beg : motive n
h : m ≤ n
⊢ motive m
Tactic:
induction h with
| refl => exact beg
| @step n _ IH => exact IH <| succ _ beg
Proof state after:
no goals
Theorem: Nat.decreasing_induction
Proof state before:
case refl
motive : Nat → Prop
succ : ∀ (n : Nat), motive (n + 1) → motive n
m n : Nat
beg : motive m
⊢ motive m
Tactic:
exact beg
Proof state after:
no goals
Theorem: Nat.decreasing_induction
Proof state before:
case step
motive : Nat → Prop
succ : ∀ (n : Nat), motive (n + 1) → motive n
m n✝ n : Nat
a✝ : Nat.le m n
IH : motive n → motive m
beg : motive (Nat.succ n)
⊢ motive m
Tactic:
exact IH <| succ _ beg
Proof state after:
no goals
Theorem: Nat.dfold_congr
Proof state before:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
⊢ HEq (dfold f n a) (dfold g n b)
Tactic:
have : α = β := funext fun n => by
  suffices ∃ (a : α n) (b : β n), HEq a b
  from let ⟨_,_,hab⟩ := this; type_eq_of_heq hab
  induction n with
  | zero => exact ⟨a,b,hab⟩
  | succ n IH =>
    let ⟨a,b,hab⟩ := IH
    exact ⟨f n a, g n b, hfg n a b hab⟩
Proof state after:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
this : α = β
⊢ HEq (dfold f n a) (dfold g n b)
Theorem: Nat.dfold_congr
Proof state before:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
this : α = β
⊢ HEq (dfold f n a) (dfold g n b)
Tactic:
cases this
Proof state after:
case refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), HEq a b → HEq (f n a) (g n b)
b : α 0
hab : HEq a b
⊢ HEq (dfold f n a) (dfold g n b)
Theorem: Nat.dfold_congr
Proof state before:
case refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), HEq a b → HEq (f n a) (g n b)
b : α 0
hab : HEq a b
⊢ HEq (dfold f n a) (dfold g n b)
Tactic:
cases hab
Proof state after:
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), HEq a b → HEq (f n a) (g n b)
⊢ HEq (dfold f n a) (dfold g n a)
Theorem: Nat.dfold_congr
Proof state before:
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), HEq a b → HEq (f n a) (g n b)
⊢ HEq (dfold f n a) (dfold g n a)
Tactic:
simp only [heq_iff_eq] at hfg ⊢
Proof state after:
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
⊢ dfold f n a = dfold g n a
Theorem: Nat.dfold_congr
Proof state before:
case refl.refl
α : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
n : Nat
a : α 0
g : (n : Nat) → α n → α (n + 1)
hfg : ∀ (n : Nat) (a b : α n), a = b → f n a = g n b
⊢ dfold f n a = dfold g n a
Tactic:
induction n with
| zero => rfl
| succ n IH => dsimp [dfold]; exact hfg n _ _ IH
Proof state after:
no goals
Theorem: Nat.dfold_congr
Proof state before:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a : α 0
b : β 0
hab : HEq a b
n : Nat
⊢ α n = β n
Tactic:
suffices ∃ (a : α n) (b : β n), HEq a b
from let ⟨_,_,hab⟩ := this; type_eq_of_heq hab
Proof state after:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a : α 0
b : β 0
hab : HEq a b
n : Nat
⊢ ∃ a b, HEq a b
Theorem: Nat.dfold_congr
Proof state before:
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n✝ : Nat
a : α 0
b : β 0
hab : HEq a b
n : Nat
⊢ ∃ a b, HEq a b
Tactic:
induction n with
| zero => exact ⟨a,b,hab⟩
| succ n IH =>
  let ⟨a,b,hab⟩ := IH
  exact ⟨f n a, g n b, hfg n a b hab⟩
Proof state after:
no goals
Theorem: Nat.dfold_congr
Proof state before:
case zero
α β : Nat → Sort u
f : (n : Nat) → α n → α (n + 1)
g : (n : Nat) → β n → β (n + 1)
hfg : ∀ (n : Nat) (a : α n) (b : β n), HEq a b → HEq (f n a) (g n b)
n : Nat
a : α 0
b : β 0
hab : HEq a b
⊢ ∃ a b, HEq a b
Tactic:
exact ⟨a,b,hab⟩
Proof state after:
no goals