awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 : α) → α) = φ
hi :
  ∀ (a : ↥(Finset.image f Finset.univ)) (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
    (↑a : ι) ∈ Finset.image f Finset.univ
⊢ Eq (α := ℕ) (∏ i : ↥(Finset.image f Finset.univ), (Fintype.card.{u_1} { a : α // φ a = i })!)
    (∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!)
have i_inj : ∀ (a₁ : ↥(Finset.image f Finset.univ)) (ha₁ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₁)
  (a₂ : ↥(Finset.image f Finset.univ))
  (ha₂ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₂), (↑a₁ : ι) = (↑a₂ : ι) → a₁ = a₂
Tactic: apply Finset.prod_bij (fun g _ => g.val)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 : α) → α) = φ
hi :
  ∀ (a : ↥(Finset.image f Finset.univ)) (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
    (↑a : ι) ∈ Finset.image f Finset.univ
i_inj :
  ∀ (a₁ : ↥(Finset.image f Finset.univ))
    (ha₁ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₁)
    (a₂ : ↥(Finset.image f Finset.univ))
    (ha₂ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₂), (↑a₁ : ι) = (↑a₂ : ι) → a₁ = a₂
⊢ Eq (α := ℕ) (∏ i : ↥(Finset.image f Finset.univ), (Fintype.card.{u_1} { a : α // φ a = i })!)
    (∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!)
have i_surj : ∀ b ∈ Finset.image f Finset.univ,
  ∃ (a : ↥(Finset.image f Finset.univ)) (_ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
    (↑a : ι) = b
Tactic: apply Finset.prod_bij (fun g _ => g.val)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 : α) → α) = φ
hi :
  ∀ (a : ↥(Finset.image f Finset.univ)) (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
    (↑a : ι) ∈ Finset.image f Finset.univ
i_inj :
  ∀ (a₁ : ↥(Finset.image f Finset.univ))
    (ha₁ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₁)
    (a₂ : ↥(Finset.image f Finset.univ))
    (ha₂ : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a₂), (↑a₁ : ι) = (↑a₂ : ι) → a₁ = a₂
i_surj :
  ∀ b ∈ Finset.image f Finset.univ,
    ∃ (a : ↥(Finset.image f Finset.univ)) (_ :
      Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a), (↑a : ι) = b
⊢ Eq (α := ℕ) (∏ i : ↥(Finset.image f Finset.univ), (Fintype.card.{u_1} { a : α // φ a = i })!)
    (∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!)
have h : ∀ (a : ↥(Finset.image f Finset.univ)) (ha : Membership.mem (γ := Finset ↥(Finset.image f Finset.univ)) Finset.univ a),
  (Fintype.card.{u_1} { a_1 : α // φ a_1 = a })! = (Fintype.card.{u_1} { a_1 : α // f a_1 = (↑a : ι) })!
Tactic: apply Finset.prod_bij (fun g _ => g.val)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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
⊢ (Fintype.card.{u_1} { a : α // φ a = i })! = (Fintype.card.{u_1} { a : α // f a = (↑i : ι) })!
have h : Fintype.card.{u_1} { a : α // φ a = i } = Fintype.card.{u_1} { a : α // f a = (↑i : ι) }
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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
⊢ Fintype.card.{u_1} { a : α // φ a = i } = Fintype.card.{u_1} { a : α // f a = (↑i : ι) }
have h : { a : α // φ a = i } ≃ { a : α // f a = (↑i : ι) }
Tactic: apply Fintype.card_congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 } ≃ { a : α // f a = (↑i : ι) }
have h : ∀ (a : α), φ a = i ↔ f ((Equiv.refl α : (a : α) → α) a) = (↑i : ι)
Tactic: apply Equiv.subtypeEquiv (Equiv.refl α)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 ((Equiv.refl α : (a : α) → α) a) = (↑i : ι)
have h : (↑(φ a) : ι) = (↑i : ι) ↔ f a = (↑i : ι)
Tactic: rw [refl_apply, ← Subtype.coe_inj]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 ι) ⋯
⊢ Fintype.card.{u_1} { g : Perm α // f ∘ (⇑g : (a : α) → α) = f } =
    ∏ i ∈ Finset.image f Finset.univ, (Fintype.card.{u_1} { a : α // f a = i })!
have suffices : ∀ (g : Perm α), f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 α
⊢ f ∘ (⇑g : (a : α) → α) = f ↔ φ ∘ (⇑g : (a : α) → α) = φ
have simp : (∀ (x : α), (f ∘ (⇑g : (a : α) → α)) x = f x) ↔ ∀ (x : α), (φ ∘ (⇑g : (a : α) → α)) x = φ x
Tactic: simp only [funext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.DomMulAct (goal)
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 α
⊢ (∀ (x : α), (f ∘ (⇑g : (a : α) → α)) x = f x) ↔ ∀ (x : α), (φ ∘ (⇑g : (a : α) → α)) x = φ x
have h : ∀ (a : α), (f ∘ (⇑g : (a : α) → α)) a = f a ↔ (φ ∘ (⇑g : (a : α) → α)) a = φ a
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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))
have 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))
Tactic: refine Fin.cases ?_ ?_ p
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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))
⊢ 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))
have 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))
Tactic: refine Fin.cases ?_ ?_ p
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
e : Perm (Fin n)
p : Fin (n + 1)
x 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))
have 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))
Tactic: by_cases h : i = e x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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))
⊢ 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))
have 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))
Tactic: by_cases h : i = e x
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
e : Perm (Fin (n + 1))
p : 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))
have 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))
Tactic: rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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))
⊢ 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))
have 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))
Tactic: rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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 : ℤˣ)
have 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 : ℤˣ)
Tactic: refine Fin.cases ?_ ?_ p
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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 : ℤˣ)
⊢ (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 : ℤˣ)
have 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 : ℤˣ)
Tactic: refine Fin.cases ?_ ?_ p
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
⊢ 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))
have 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) :
      ℕ)
Tactic: ext i
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
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) :
      ℕ)
have 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) :
      ℕ)
Tactic: cases n
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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) :
        ℕ)
⊢ (↑((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) :
      ℕ)
have 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) :
      ℕ)
Tactic: cases n
Cleared hypotheses: n, i
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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) :
      ℕ)
have 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) :
    ℕ)
Tactic: refine Fin.cases ?_ (fun i => ?_) i
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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) :
      ℕ)
⊢ (↑((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) :
      ℕ)
have 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) :
      ℕ)
Tactic: refine Fin.cases ?_ (fun i => ?_) i
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
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) :
      ℕ)
have 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))) :
    ℕ)
Tactic: rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
⊢ (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))) :
      ℕ)
have 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))) :
      ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
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))) :
        ℕ)
⊢ (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))) :
      ℕ)
have 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))) :
      ℕ)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Fin (goal)
Goal:
n : ℕ
i_1 : Fin (n + 1).succ
i : Fin (n + 1)
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))) :
      ℕ)
have 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))) :
    ℕ)
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 _)]