awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
this : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
i : ↥(Finset.image f Finset.univ)
ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ i
a : α
⊢ (↑(φ a) : ι) = (↑i : ι) ↔ f a = (↑i : ι)

Tactic:
simp only [φ, Set.val_codRestrict_apply]

Premises used: Set.val_codRestrict_apply
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
suffices : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } =
    ∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!

Tactic:
suffices ∀ g : Perm α, f ∘ g = f ↔ φ ∘ g = φ by
    simp only [this, stabilizer_card]
    apply Finset.prod_bij (fun g _ => g.val)
    · exact fun g _ => Finset.coe_mem g
    · exact fun g _ g' _ => SetCoe.ext
    · simp
    · intro i _
      apply congr_arg
      apply Fintype.card_congr
      apply Equiv.subtypeEquiv (Equiv.refl α)
      intro a
      rw [refl_apply, ← Subtype.coe_inj]
      simp only [φ, Set.val_codRestrict_apply]
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
g : Perm α
simp : (∀ (x : α), (f ∘ (⇑g : (a : α) → α)) x = f x) ↔ ∀ (x : α), (φ ∘ (⇑g : (a : α) → α)) x = φ x
⊢ f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ

Tactic:
simp only [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
g : Perm α
h : ∀ (a : α), (f ∘ (⇑g : (a : α) → α)) a = f a ↔ (φ ∘ (⇑g : (a : α) → α)) a = φ a
⊢ (∀ (x : α), (f ∘ (⇑g : (a : α) → α)) x = f x) ↔ ∀ (x : α), (φ ∘ (⇑g : (a : α) → α)) x = φ x

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.GroupTheory.Perm.DomMulAct
Goal:
α : Type u_1
ι : Type u_2
f : α → ι
inst : Fintype α
inst_1 : DecidableEq α
inst_2 : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := Set.codRestrict f (↑(Finset.image f Finset.univ) : Set ι) ⋯
g : Perm α
a : α
⊢ (f ∘ (⇑g : (a : α) → α)) a = f a ↔ (φ ∘ (⇑g : (a : α) → α)) a = φ a

Tactic:
simp only [Function.comp_apply, φ, ← Subtype.coe_inj, Set.val_codRestrict_apply]

Premises used: Subtype.coe_inj, Function.comp_apply, Set.val_codRestrict_apply
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
p : Fin (n + 1)
⊢ (Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (p, Equiv.refl (Fin n)) = swap 0 p

Tactic:
simp [Equiv.Perm.decomposeFin, Equiv.permCongr_def, pull_end]

Premises used: Equiv.Perm.decomposeFin, Equiv.permCongr_def
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
p : Fin (n + 1)
⊢ (Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (p, 1) = swap 0 p

Tactic:
Equiv.Perm.decomposeFin_symm_of_refl p

Premises used: Equiv.Perm.decomposeFin_symm_of_refl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ (((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (p, e) : Perm (Fin n.succ)) :
        (a : Fin n.succ) → Fin n.succ)
      0 =
    p

Tactic:
simp [Equiv.Perm.decomposeFin]

Premises used: Equiv.Perm.decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ Eq (α := Fin n.succ)
    ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (p, e) : Perm (Fin n.succ)) :
          (a : Fin n.succ) → Fin n.succ)
        x.succ :
      Fin n.succ)
    ((swap 0 p : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))

Tactic:
Fin.cases ?_ ?_ p

Premises used: Fin.cases
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
refine_1 :
  Eq (α := Fin n.succ)
    ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (0, e) : Perm (Fin n.succ)) :
          (a : Fin n.succ) → Fin n.succ)
        x.succ :
      Fin n.succ)
    ((swap 0 0 : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))
refine_2 :
  ∀ (i : Fin n),
    Eq (α := Fin n.succ)
      ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, e) :
              Perm (Fin n.succ)) :
            (a : Fin n.succ) → Fin n.succ)
          x.succ :
        Fin n.succ)
      ((swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))
⊢ Eq (α := Fin n.succ)
    ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (p, e) : Perm (Fin n.succ)) :
          (a : Fin n.succ) → Fin n.succ)
        x.succ :
      Fin n.succ)
    ((swap 0 p : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))

Tactic:
refine Fin.cases ?_ ?_ p
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x : Fin n
⊢ Eq (α := Fin n.succ)
    ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (0, e) : Perm (Fin n.succ)) :
          (a : Fin n.succ) → Fin n.succ)
        x.succ :
      Fin n.succ)
    ((swap 0 0 : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))

Tactic:
simp [Equiv.Perm.decomposeFin]

Premises used: Equiv.Perm.decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
pos :
  ∀ (h : i = (e : (a : Fin n) → Fin n) x),
    Eq (α := Fin n.succ)
      ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, e) :
              Perm (Fin n.succ)) :
            (a : Fin n.succ) → Fin n.succ)
          x.succ :
        Fin n.succ)
      ((swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))
neg :
  ∀ (h : ¬i = (e : (a : Fin n) → Fin n) x),
    Eq (α := Fin n.succ)
      ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, e) :
              Perm (Fin n.succ)) :
            (a : Fin n.succ) → Fin n.succ)
          x.succ :
        Fin n.succ)
      ((swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))
⊢ Eq (α := Fin n.succ)
    ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, e) :
            Perm (Fin n.succ)) :
          (a : Fin n.succ) → Fin n.succ)
        x.succ :
      Fin n.succ)
    ((swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))

Tactic:
by_cases h : i = e x

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : i = (e : (a : Fin n) → Fin n) x
⊢ Eq (α := Fin n.succ)
    ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, e) :
            Perm (Fin n.succ)) :
          (a : Fin n.succ) → Fin n.succ)
        x.succ :
      Fin n.succ)
    ((swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))

Tactic:
simp [h, Equiv.Perm.decomposeFin]

Premises used: Equiv.Perm.decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x i : Fin n
h : ¬i = (e : (a : Fin n) → Fin n) x
⊢ Eq (α := Fin n.succ)
    ((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, e) :
            Perm (Fin n.succ)) :
          (a : Fin n.succ) → Fin n.succ)
        x.succ :
      Fin n.succ)
    ((swap 0 i.succ : (a : Fin (n + 1)) → Fin (n + 1)) (Fin.succ ((e : (a : Fin n) → Fin n) x)) : Fin (n + 1))

Tactic:
simp [Equiv.Perm.decomposeFin, swap_apply_def, Ne.symm h]

Premises used: Equiv.swap_apply_def, Ne.symm, Equiv.Perm.decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
e : Perm (Fin (n + 1))
p : Fin (n + 2)
rw :
  Eq (α := Fin (n + 1).succ)
    ((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ)) (p, e) :
            Perm (Fin (n + 1).succ)) :
          (a : Fin (n + 1).succ) → Fin (n + 1).succ)
        (Fin.succ 0) :
      Fin (n + 1).succ)
    ((swap 0 p : (a : Fin (n + 2)) → Fin (n + 2)) (Fin.succ ((e : (a : Fin (n + 1)) → Fin (n + 1)) 0)) : Fin (n + 2))
rw₁ rw₂ :
  Eq (α := Fin (n + 1).succ)
    ((swap 0 p : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1)) (Fin.succ ((e : (a : Fin (n + 1)) → Fin (n + 1)) 0)) :
      Fin (n + 1 + 1))
    ((swap 0 p : (a : Fin (n + 2)) → Fin (n + 2)) (Fin.succ ((e : (a : Fin (n + 1)) → Fin (n + 1)) 0)) : Fin (n + 2))
⊢ Eq (α := Fin (n + 1).succ)
    ((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ)) (p, e) :
            Perm (Fin (n + 1).succ)) :
          (a : Fin (n + 1).succ) → Fin (n + 1).succ)
        1 :
      Fin (n + 1).succ)
    ((swap 0 p : (a : Fin (n + 2)) → Fin (n + 2)) (Fin.succ ((e : (a : Fin (n + 1)) → Fin (n + 1)) 0)) : Fin (n + 2))

Tactic:
rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]

Premises used: Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ, OfNat.ofNat
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ (sign : (a : Perm (Fin n.succ)) → ℤˣ)
      ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (p, e)) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (if p = 0 then 1 else -1 : ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) e : ℤˣ)

Tactic:
Fin.cases ?_ ?_ p

Premises used: Fin.cases
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
refine_1 :
  (sign : (a : Perm (Fin n.succ)) → ℤˣ)
      ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (0, e)) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (if Eq (α := Fin (n + 1)) 0 0 then 1 else -1 : ℤˣ)
      ((sign : (a : Perm (Fin n)) → ℤˣ) e : ℤˣ)
refine_2 :
  ∀ (i : Fin n),
    (sign : (a : Perm (Fin n.succ)) → ℤˣ)
        ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, e)) =
      HMul.hMul (α := ℤˣ) (β := ℤˣ) (if i.succ = 0 then 1 else -1 : ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) e : ℤˣ)
⊢ (sign : (a : Perm (Fin n.succ)) → ℤˣ)
      ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (p, e)) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (if p = 0 then 1 else -1 : ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) e : ℤˣ)

Tactic:
refine Fin.cases ?_ ?_ p
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ (sign : (a : Perm (Fin n.succ)) → ℤˣ)
      ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (0, e)) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (if Eq (α := Fin (n + 1)) 0 0 then 1 else -1 : ℤˣ)
      ((sign : (a : Perm (Fin n)) → ℤˣ) e : ℤˣ)

Tactic:
simp [Equiv.Perm.decomposeFin]

Premises used: Equiv.Perm.decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ ∀ (i : Fin n),
    (sign : (a : Perm (Fin n.succ)) → ℤˣ)
        ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (i.succ, e)) =
      HMul.hMul (α := ℤˣ) (β := ℤˣ) (if i.succ = 0 then 1 else -1 : ℤˣ) ((sign : (a : Perm (Fin n)) → ℤˣ) e : ℤˣ)

Tactic:
simp [Equiv.Perm.decomposeFin]

Premises used: Equiv.Perm.decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
⊢ Eq (α := Finset (Perm (Fin n.succ))) univ (map (Equiv.toEmbedding (Equiv.symm Perm.decomposeFin)) univ)

Tactic:
(Finset.univ_map_equiv_to_embedding _).symm

Premises used: Finset.univ_map_equiv_to_embedding, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
H :
  ∀ (i : Fin n.succ),
    (↑((finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i) : ℕ) =
      (↑((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (1, finRotate n) :
                Perm (Fin n.succ)) :
              (a : Fin n.succ) → Fin n.succ)
            i) :
        ℕ)
⊢ Eq (α := Perm (Fin n.succ)) (finRotate n.succ)
    ((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (1, finRotate n))

Tactic:
ext i
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin n.succ
H :
  ∀ (i : Fin (Nat.succ 0)),
    (↑((finRotate (Nat.succ 0) : (a : Fin (Nat.succ 0)) → Fin (Nat.succ 0)) i) : ℕ) =
      (↑((((Equiv.symm decomposeFin : (a : Fin (Nat.succ 0) × Perm (Fin 0)) → Perm (Fin (Nat.succ 0)))
                  (1, finRotate 0) :
                Perm (Fin (Nat.succ 0))) :
              (a : Fin (Nat.succ 0)) → Fin (Nat.succ 0))
            i) :
        ℕ)
H₁ :
  ∀ (n : ℕ) (i : Fin (n + 1).succ),
    (↑((finRotate (n + 1).succ : (a : Fin (n + 1).succ) → Fin (n + 1).succ) i) : ℕ) =
      (↑((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
                  (1, finRotate (n + 1)) :
                Perm (Fin (n + 1).succ)) :
              (a : Fin (n + 1).succ) → Fin (n + 1).succ)
            i) :
        ℕ)
⊢ (↑((finRotate n.succ : (a : Fin n.succ) → Fin n.succ) i) : ℕ) =
    (↑((((Equiv.symm decomposeFin : (a : Fin n.succ × Perm (Fin n)) → Perm (Fin n.succ)) (1, finRotate n) :
              Perm (Fin n.succ)) :
            (a : Fin n.succ) → Fin n.succ)
          i) :
      ℕ)

Tactic:
cases n
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
i : Fin (Nat.succ 0)
⊢ (↑((finRotate (Nat.succ 0) : (a : Fin (Nat.succ 0)) → Fin (Nat.succ 0)) i) : ℕ) =
    (↑((((Equiv.symm decomposeFin : (a : Fin (Nat.succ 0) × Perm (Fin 0)) → Perm (Fin (Nat.succ 0))) (1, finRotate 0) :
              Perm (Fin (Nat.succ 0))) :
            (a : Fin (Nat.succ 0)) → Fin (Nat.succ 0))
          i) :
      ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin (n + 1).succ
⊢ (↑((finRotate (n + 1).succ : (a : Fin (n + 1).succ) → Fin (n + 1).succ) i) : ℕ) =
    (↑((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
                (1, finRotate (n + 1)) :
              Perm (Fin (n + 1).succ)) :
            (a : Fin (n + 1).succ) → Fin (n + 1).succ)
          i) :
      ℕ)

Tactic:
Fin.cases ?_ (fun i => ?_) i

Premises used: Fin.cases
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin (n + 1).succ
H :
  (↑((finRotate (n + 1).succ : (a : Fin (n + 1).succ) → Fin (n + 1).succ) 0) : ℕ) =
    (↑((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
                (1, finRotate (n + 1)) :
              Perm (Fin (n + 1).succ)) :
            (a : Fin (n + 1).succ) → Fin (n + 1).succ)
          0) :
      ℕ)
H₁ :
  ∀ (i : Fin (n + 1)),
    (↑((finRotate (n + 1).succ : (a : Fin (n + 1).succ) → Fin (n + 1).succ) i.succ) : ℕ) =
      (↑((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
                  (1, finRotate (n + 1)) :
                Perm (Fin (n + 1).succ)) :
              (a : Fin (n + 1).succ) → Fin (n + 1).succ)
            i.succ) :
        ℕ)
⊢ (↑((finRotate (n + 1).succ : (a : Fin (n + 1).succ) → Fin (n + 1).succ) i) : ℕ) =
    (↑((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
                (1, finRotate (n + 1)) :
              Perm (Fin (n + 1).succ)) :
            (a : Fin (n + 1).succ) → Fin (n + 1).succ)
          i) :
      ℕ)

Tactic:
refine Fin.cases ?_ (fun i => ?_) i
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i : Fin (n + 1).succ
⊢ (↑((finRotate (n + 1).succ : (a : Fin (n + 1).succ) → Fin (n + 1).succ) 0) : ℕ) =
    (↑((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
                (1, finRotate (n + 1)) :
              Perm (Fin (n + 1).succ)) :
            (a : Fin (n + 1).succ) → Fin (n + 1).succ)
          0) :
      ℕ)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
H :
  (if i = Fin.last n then 0 else (↑i.succ : ℕ) + 1) =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
⊢ (↑((finRotate (n + 1).succ : (a : Fin (n + 1).succ) → Fin (n + 1).succ) i.succ) : ℕ) =
    (↑((((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
                (1, finRotate (n + 1)) :
              Perm (Fin (n + 1).succ)) :
            (a : Fin (n + 1).succ) → Fin (n + 1).succ)
          i.succ) :
      ℕ)

Tactic:
rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]

Premises used: if_congr, coe_finRotate, Equiv.Perm.decomposeFin_symm_apply_succ, Fin.succ_eq_last_succ, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
pos :
  ∀ (h : i = Fin.last n),
    0 =
      (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
            (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
        ℕ)
neg :
  ∀ (h : ¬i = Fin.last n),
    (↑i.succ : ℕ) + 1 =
      (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
            (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
        ℕ)
⊢ (if i = Fin.last n then 0 else (↑i.succ : ℕ) + 1) =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : i = Fin.last n
⊢ 0 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
h : ¬i = Fin.last n
neg :
  (↑i : ℕ) + 1 + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)
neg₁ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) (↑(Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i)) : ℕ)
neg₂ :
  (↑i : ℕ) + 1 + 1 =
    (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i) : ℕ) + 1)
neg₃ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((if i = Fin.last n then 0 else (↑i : ℕ) + 1) + 1)
neg₄ : (↑i : ℕ) + 1 + 1 = (swap (↑0 : ℕ) (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
neg₅ : (↑i : ℕ) + 1 + 1 = (swap 0 (↑1 : ℕ) : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
neg₆ : (↑i : ℕ) + 1 + 1 = (swap 0 1 : (a : ℕ) → ℕ) ((↑i : ℕ) + 1 + 1)
neg₇ neg₈ : (↑i : ℕ) + 1 + 1 = ((↑i : ℕ) + 1).succ
⊢ (↑i.succ : ℕ) + 1 =
    (↑((swap 0 1 : (a : Fin (n + 1 + 1)) → Fin (n + 1 + 1))
          (Fin.succ ((finRotate (n + 1) : (a : Fin (n + 1)) → Fin (n + 1)) i))) :
      ℕ)

Tactic:
rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]

Premises used: Function.Injective.map_swap, Fin.val_one, Fin.val_succ, coe_finRotate, Nat.succ_succ_ne_one, Equiv.swap_apply_of_ne_of_ne, Fin.val_injective, Nat.succ_ne_zero, Fin.val_zero, if_neg
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
⊢ (sign : (a : Perm (Fin 0)) → ℤˣ) (finRotate 0) = HPow.hPow (α := ℤˣ) (-1) (HSub.hSub (α := ℕ) 0 1)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
⊢ (sign : (a : Perm (Fin (0 + 1))) → ℤˣ) (finRotate (HAdd.hAdd (α := ℕ) 0 1)) =
    HPow.hPow (α := ℤˣ) (-1) (HAdd.hAdd (α := ℕ) 0 1 - 1)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
ih : (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)
succ :
  (sign : (a : Perm (Fin (n + 1 + 1))) → ℤˣ)
      ((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
        (1, finRotate (n + 1))) =
    HPow.hPow (α := ℤˣ) (-1) (n + 1 + 1 - 1)
⊢ (sign : (a : Perm (Fin (n + 1 + 1))) → ℤˣ) (finRotate (n + 1 + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 + 1 - 1)

Tactic:
rw [finRotate_succ_eq_decomposeFin]

Premises used: finRotate_succ_eq_decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
ih : (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)
⊢ (sign : (a : Perm (Fin (n + 1 + 1))) → ℤˣ)
      ((Equiv.symm decomposeFin : (a : Fin (n + 1).succ × Perm (Fin (n + 1))) → Perm (Fin (n + 1).succ))
        (1, finRotate (n + 1))) =
    HPow.hPow (α := ℤˣ) (-1) (n + 1 + 1 - 1)

Tactic:
simp [ih, pow_succ]

Premises used: pow_succ
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
succ :
  (sign : (a : Perm (Fin (0 + 1))) → ℤˣ) (finRotate (HAdd.hAdd (α := ℕ) 0 1)) =
    HPow.hPow (α := ℤˣ) (-1) (HAdd.hAdd (α := ℕ) 0 1 - 1)
succ₁ :
  ∀ (n : ℕ) (ih : (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)),
    (sign : (a : Perm (Fin (n + 1 + 1))) → ℤˣ) (finRotate (n + 1 + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 + 1 - 1)
⊢ (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)

Tactic:
induction n with
    | zero => simp
    | succ n ih =>
      rw [finRotate_succ_eq_decomposeFin]
      simp [ih, pow_succ]

Premises used: pow_succ, finRotate_succ_eq_decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
zero : (sign : (a : Perm (Fin 0)) → ℤˣ) (finRotate 0) = HPow.hPow (α := ℤˣ) (-1) (HSub.hSub (α := ℕ) 0 1)
succ : ∀ (n : ℕ), (sign : (a : Perm (Fin (n + 1))) → ℤˣ) (finRotate (n + 1)) = HPow.hPow (α := ℤˣ) (-1) (n + 1 - 1)
⊢ (sign : (a : Perm (Fin n)) → ℤˣ) (finRotate n) = HPow.hPow (α := ℤˣ) (-1) (n - 1)

Tactic:
cases n with
  | zero => simp
  | succ n =>
    induction n with
    | zero => simp
    | succ n ih =>
      rw [finRotate_succ_eq_decomposeFin]
      simp [ih, pow_succ]

Premises used: pow_succ, finRotate_succ_eq_decomposeFin
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
h :
  ∀ (a : Fin (n + 2)),
    Membership.mem (γ := Finset (Fin (n + 2))) (support (finRotate (n + 2))) a ↔
      Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ a
⊢ Eq (α := Finset (Fin (n + 2))) (support (finRotate (n + 2))) Finset.univ

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
a : Fin (n + 2)
⊢ Membership.mem (γ := Finset (Fin (n + 2))) (support (finRotate (n + 2))) a ↔
    Membership.mem (γ := Finset (Fin (n + 2))) Finset.univ a

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
h : 2 ≤ n
obtain : ∀ (m : ℕ) (h : 2 ≤ 2 + m), Eq (α := Finset (Fin (2 + m))) (support (finRotate (2 + m))) Finset.univ
⊢ (finRotate n).support = Finset.univ

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Premises used: ExistsAddOfLE.exists_add_of_le, rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
m : ℕ
h : 2 ≤ 2 + m
rw : Eq (α := Finset (Fin (m + 2))) (support (finRotate (m + 2))) Finset.univ
rw₁ rw₂ : Eq (α := Finset (Fin (m + 2))) Finset.univ Finset.univ
⊢ Eq (α := Finset (Fin (2 + m))) (support (finRotate (2 + m))) Finset.univ

Tactic:
rw [add_comm, support_finRotate]

Premises used: add_comm, support_finRotate
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
⊢ Ne (α := Fin (n + 2)) ((finRotate (n + 2) : (a : Fin (n + 2)) → Fin (n + 2)) 0) 0

Tactic:
simp