awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = if k = j then i else k + 1
have this : (Equiv.symm
        (Function.Embedding.toEquivRange
          (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr sorry)))) :
      (a :
          (↑(Set.range
                (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr sorry).toEmbedding) :
                  (a : Fin (n - (↑i : ℕ))) → Fin n)) :
            Type)) →
        Fin (n - (↑i : ℕ)))
    (Subtype.mk (p := fun (x : Fin n) ↦
      Membership.mem (γ := Set (Fin n))
        (Set.range (ι := Fin (n - (↑i : ℕ)))
          (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr sorry))) :
            (a : Fin (n - (↑i : ℕ))) → Fin n))
        x)
      k kin) =
  subNat (↑i : ℕ) (Fin.cast sorry k) sorry
Tactic: have : (((addNatEmb (n - (n - i.1))).trans (finCongr _).toEmbedding).toEquivRange.symm ⟨k, kin⟩)
      = subNat i.1 (k.cast (by lia)) (by simp; lia) := by
    simpa [symm_apply_eq] using eq_of_val_eq (by simp; lia)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ (i.cycleIcc j : (a : Fin n) → Fin n) k = if k = j then i else k + 1
have simp : Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) sorry
    (addNat
      ((((j - i).castLT sorry).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
        (subNat (↑i : ℕ) (Fin.cast sorry k) sorry))
      (n - (n - (↑i : ℕ)))) =
  if k = j then i else k + 1
Tactic: simp only [cycleIcc_to_cycleRange hij kin, natAdd_castLEEmb, this, Function.Embedding.trans_apply,
    addNatEmb_apply, coe_toEmbedding, finCongr_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
      (addNat
        ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
          (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
        (n - (n - (↑i : ℕ)))) =
    if k = j then i else k + 1
have refine : (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) sorry
        (addNat
          ((((j - i).castLT sorry).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
            (subNat (↑i : ℕ) (Fin.cast sorry k) sorry))
          (n - (n - (↑i : ℕ))))) :
    ℕ) =
  (↑(if k = j then i else k + 1) : ℕ)
Tactic: refine eq_of_val_eq ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
⊢ (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
          (addNat
            ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
              (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑(if k = j then i else k + 1) : ℕ)
have pos : ∀ (ch : k = j),
  (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) sorry
          (addNat
            ((((j - i).castLT sorry).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
              (subNat (↑i : ℕ) (Fin.cast sorry k) sorry))
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑i : ℕ)
Tactic: split_ifs with ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
pos :
  ∀ (ch : k = j),
    (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
            (addNat
              ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
                (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
              (n - (n - (↑i : ℕ))))) :
        ℕ) =
      (↑i : ℕ)
⊢ (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
          (addNat
            ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
              (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑(if k = j then i else k + 1) : ℕ)
have neg : ∀ (ch : ¬k = j),
  (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) sorry
          (addNat
            ((((j - i).castLT sorry).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
              (subNat (↑i : ℕ) (Fin.cast sorry k) sorry))
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑(k + 1) : ℕ)
Tactic: split_ifs with ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
ch : k = j
⊢ (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
          (addNat
            ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
              (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑i : ℕ)
have this₁ : subNat (↑i : ℕ) (Fin.cast sorry j) sorry = (j - i).castLT sorry
Tactic: have : subNat i.1 (j.cast (by lia)) (by simp [hij]) = (j - i).castLT (sub_val_lt_sub hij) :=
      eq_of_val_eq (by simp [sub_val_of_le hij])
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this_1 :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
ch : k = j
this : subNat (↑i : ℕ) (Fin.cast ⋯ j) ⋯ = (j - i).castLT ⋯
⊢ (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
          (addNat
            ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
              (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑i : ℕ)
have pos : n - (n - (↑i : ℕ)) = (↑i : ℕ)
Tactic: simp [ch, cycleRange_of_eq this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
⊢ subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
have simp : (↑k : ℕ) - (↑i : ℕ) < (↑j : ℕ) - (↑i : ℕ)
Tactic: simp [lt_def, sub_val_of_le hij]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (hypothesis)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
⊢ (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
          (addNat
            ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
              (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑(k + 1) : ℕ)
have this₁ : subNat (↑i : ℕ) (Fin.cast sorry k) sorry < (j - i).castLT sorry
Tactic: have : subNat i.1 (k.cast (by lia)) (by simp [hik]) < (j - i).castLT (sub_val_lt_sub hij) := by
      simp [lt_def, sub_val_of_le hij]; lia
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this_1 :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
this : subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ (↑(Fin.cast (n := n - (↑i : ℕ) + (n - (n - (↑i : ℕ)))) ⋯
          (addNat
            ((((j - i).castLT ⋯).cycleRange : (a : Fin (n - (↑i : ℕ))) → Fin (n - (↑i : ℕ)))
              (subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯))
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑(k + 1) : ℕ)
have neg : (↑(Fin.cast sorry
        ((HAdd.hAdd (α := Fin (n - (↑i : ℕ))) (⟨(↑(Fin.cast sorry k) : ℕ) - (↑i : ℕ), sorry⟩ : Fin (n - (↑i : ℕ))) 1).addNat
          (n - (n - (↑i : ℕ))))) :
    ℕ) =
  (↑(k + 1) : ℕ)
Tactic: rw [cycleRange_of_lt this, subNat]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this_1 :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
this : subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ (↑(Fin.cast ⋯
          ((HAdd.hAdd (α := Fin (n - (↑i : ℕ))) (⟨(↑(Fin.cast ⋯ k) : ℕ) - (↑i : ℕ), ⋯⟩ : Fin (n - (↑i : ℕ))) 1).addNat
            (n - (n - (↑i : ℕ))))) :
      ℕ) =
    (↑(k + 1) : ℕ)
have neg : ((↑k : ℕ) - (↑i : ℕ) + 1) % (n - (↑i : ℕ)) + (n - (n - (↑i : ℕ))) = ((↑k : ℕ) + 1) % n
Tactic: simp only [val_cast, add_def, val_one', Nat.add_mod_mod, addNat_mk, cast_mk]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j k : Fin n
hik : i ≤ k
hkj : k ≤ j
inst : NeZero n
hij : i ≤ j
kin :
  Membership.mem (γ := Set (Fin n))
    (Set.range (ι := Fin (n - (↑i : ℕ))) (⇑(natAdd_castLEEmb ⋯) : (a : Fin (n - (↑i : ℕ))) → Fin n)) k
this_1 :
  (Equiv.symm
          (Function.Embedding.toEquivRange
            (Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯)))) :
        (a :
            (↑(Set.range
                  (⇑((addNatEmb (n - (n - (↑i : ℕ)))).trans (finCongr ⋯).toEmbedding) :
                    (a : Fin (n - (↑i : ℕ))) → Fin n)) :
              Type)) →
          Fin (n - (↑i : ℕ)))
      (Subtype.mk (p := fun (x : Fin n) ↦
        Membership.mem (γ := Set (Fin n))
          (Set.range (ι := Fin (n - (↑i : ℕ)))
            (⇑(Function.Embedding.trans (addNatEmb (n - (n - (↑i : ℕ)))) (Equiv.toEmbedding (finCongr ⋯))) :
              (a : Fin (n - (↑i : ℕ))) → Fin n))
          x)
        k kin) =
    subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯
ch : ¬k = j
this : subNat (↑i : ℕ) (Fin.cast ⋯ k) ⋯ < (j - i).castLT ⋯
⊢ ((↑k : ℕ) - (↑i : ℕ) + 1) % (n - (↑i : ℕ)) + (n - (n - (↑i : ℕ))) = ((↑k : ℕ) + 1) % n
have neg : (↑k : ℕ) - (↑i : ℕ) + 1 + (n - (n - (↑i : ℕ))) = (↑k : ℕ) + 1
Tactic: rw [Nat.mod_eq_of_lt (by lia), Nat.mod_eq_of_lt (by lia)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
⊢ i.cycleIcc i = 1
have H : ∀ (k : Fin n), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑((1 : (a : Fin n) → Fin n) k) : ℕ)
Tactic: ext k
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑((1 : (a : Fin n) → Fin n) k) : ℕ)
have H : (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
Tactic: simp only [Perm.coe_one, id_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
have H : ∀ (ch : k < i), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
Tactic: rcases lt_trichotomy k i with ch | ch | ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
H : ∀ (ch : k < i), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
have H₁ : ∀ (ch : k = i), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
Tactic: rcases lt_trichotomy k i with ch | ch | ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
k : Fin n
H : ∀ (ch : k < i), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
H₁ : ∀ (ch : k = i), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
⊢ (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
have H₂ : ∀ (ch : i < k), (↑((i.cycleIcc i : (a : Fin n) → Fin n) k) : ℕ) = (↑k : ℕ)
Tactic: rcases lt_trichotomy k i with ch | ch | ch
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
inst : NeZero n
⊢ j.cycleIcc i = 1
have inl : ∀ (hij : i < j), j.cycleIcc i = 1
Tactic: rcases Fin.lt_or_eq_of_le hij with hij | hij
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
inst : NeZero n
inl : ∀ (hij : i < j), j.cycleIcc i = 1
⊢ j.cycleIcc i = 1
have inr : ∀ (hij : i = j), j.cycleIcc i = 1
Tactic: rcases Fin.lt_or_eq_of_le hij with hij | hij
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
hij_1 : i ≤ j
inst : NeZero n
hij : i = j
⊢ j.cycleIcc i = 1
have inr : j.cycleIcc j = 1
Tactic: rw [hij, ← cycleIcc_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
hij_1 : i ≤ j
inst : NeZero n
hij : i = j
inr : j.cycleIcc j = 1
⊢ j.cycleIcc i = 1
have inr₁ : j.cycleIcc j = j.cycleIcc j
Tactic: rw [hij, ← cycleIcc_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (i.cycleIcc i) : ℤˣ) (1 : ℤˣ)
have rw : HPow.hPow (α := ℤˣ) (-1) ((↑i : ℕ) - (↑i : ℕ)) = 1
Tactic: rw [sign_cycleIcc_of_le (Fin.ge_of_eq rfl), tsub_self, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
rw : HPow.hPow (α := ℤˣ) (-1) ((↑i : ℕ) - (↑i : ℕ)) = 1
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (i.cycleIcc i) : ℤˣ) (1 : ℤˣ)
have rw₁ : HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 0 = 1
Tactic: rw [sign_cycleIcc_of_le (Fin.ge_of_eq rfl), tsub_self, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
rw : HPow.hPow (α := ℤˣ) (-1) ((↑i : ℕ) - (↑i : ℕ)) = 1
rw₁ : HPow.hPow (α := ℤˣ) (β := ℕ) (-1) 0 = 1
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (i.cycleIcc i) : ℤˣ) (1 : ℤˣ)
have rw₂ : Eq (α := ℤˣ) 1 1
Tactic: rw [sign_cycleIcc_of_le (Fin.ge_of_eq rfl), tsub_self, pow_zero]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
have inl : ∀ (hij : i < j), Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
Tactic: rcases Fin.lt_or_eq_of_le hij with hij | hij
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
hij : i ≤ j
inl : ∀ (hij : i < j), Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
have inr : ∀ (hij : i = j), Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
Tactic: rcases Fin.lt_or_eq_of_le hij with hij | hij
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
hij_1 : i ≤ j
hij : i = j
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
have inr : Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc j) : ℤˣ) (1 : ℤˣ)
Tactic: rw [hij, sign_cycleIcc_of_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i j : Fin n
hij_1 : i ≤ j
hij : i = j
inr : Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc j) : ℤˣ) (1 : ℤˣ)
⊢ Eq (α := ℤˣ) ((Perm.sign : (a : Perm (Fin n)) → ℤˣ) (j.cycleIcc i) : ℤˣ) (1 : ℤˣ)
have inr₁ : Eq (α := ℤˣ) 1 1
Tactic: rw [hij, sign_cycleIcc_of_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i : Fin n
inst : NeZero n
⊢ cycleIcc 0 i = i.cycleRange
have H : ∀ (x : Fin n), (↑((cycleIcc 0 i : (a : Fin n) → Fin n) x) : ℕ) = (↑((i.cycleRange : (a : Fin n) → Fin n) x) : ℕ)
Tactic: ext x