awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
have pos : ∀ (ha' : a = a'),
  a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: by_cases ha' : a = a'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
pos :
  ∀ (ha' : a = a'),
    a ∈ a' :: l ∧
        Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
have neg : ∀ (ha' : ¬a = a'),
  a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: by_cases ha' : a = a'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : a = a'
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
have pos : ∀
  (ih :
    ∀ (hl : l.Nodup),
      a ∈ l ∧
          Eq (α := α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
            ((a, (σ a : (a : β) → β) b) : α × β) ∨
        a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b))
  (hl : (a' :: l).Nodup) (notMem_l : a ∉ l)
  (prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b))
  (ha' : a = a),
  a ∈ a :: l ∧
      Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a :: l ∧ (prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: rw [← ha'] at *
Cleared hypotheses: ih, hl, notMem_l, prod_eq, ha'
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : a = a
⊢ a ∈ a :: l ∧
      Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a :: l ∧ (prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) = (a, b)
have pos : Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)
Tactic: refine Or.inl ⟨l.mem_cons_self, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : a = a
⊢ Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)
have pos : Eq (α := α × β) ((a, (σ a : (a : β) → β) b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)
Tactic: rw [prodExtendRight_apply_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : ¬a = a'
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
have neg : (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: refine Or.inr ⟨fun h => not_or_intro ha' notMem_l ((List.mem_cons).mp h), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : ¬a = a'
⊢ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
have neg : (a, b) = (a, b)
Tactic: rw [prodExtendRight_apply_ne _ ha']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
a : α
b : β
⊢ a ∈ l ∧
      Eq (α := α × β)
        ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
have H : ∀ (hl : List.Nodup.{u_1} (α := α) []),
  Membership.mem (γ := List α) [] a ∧
      Eq (α := α × β)
        ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ [] ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: induction l with
  | nil =>
    refine Or.inr ⟨List.not_mem_nil, ?_⟩
    rw [List.map_nil, List.prod_nil, one_apply]
  | cons a' l ih =>
    rw [List.map_cons, List.prod_cons, mul_apply]
    rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨notMem_l, prod_eq⟩) <;>
      rw [prod_eq]
    · refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩
      rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]
    by_cases ha' : a = a'
    · rw [← ha'] at *
      refine Or.inl ⟨l.mem_cons_self, ?_⟩
      rw [prodExtendRight_apply_eq]
    · refine Or.inr ⟨fun h => not_or_intro ha' notMem_l ((List.mem_cons).mp h), ?_⟩
      rw [prodExtendRight_apply_ne _ ha']
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
a : α
b : β
H :
  ∀ (hl : List.Nodup.{u_1} (α := α) []),
    Membership.mem (γ := List α) [] a ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ [] ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)
⊢ a ∈ l ∧
      Eq (α := α × β)
        ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
have H₁ : ∀ (a' : α) (l : List α)
  (ih :
    ∀ (hl : l.Nodup),
      a ∈ l ∧
          Eq (α := α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
            ((a, (σ a : (a : β) → β) b) : α × β) ∨
        a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b))
  (hl : (a' :: l).Nodup),
  a ∈ a' :: l ∧
      Eq (α := α × β)
        ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) (a' :: l)) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧
      (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) (a' :: l)) : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: induction l with
  | nil =>
    refine Or.inr ⟨List.not_mem_nil, ?_⟩
    rw [List.map_nil, List.prod_nil, one_apply]
  | cons a' l ih =>
    rw [List.map_cons, List.prod_cons, mul_apply]
    rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨notMem_l, prod_eq⟩) <;>
      rw [prod_eq]
    · refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩
      rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]
    by_cases ha' : a = a'
    · rw [← ha'] at *
      refine Or.inl ⟨l.mem_cons_self, ?_⟩
      rw [prodExtendRight_apply_eq]
    · refine Or.inr ⟨fun h => not_or_intro ha' notMem_l ((List.mem_cons).mp h), ?_⟩
      rw [prodExtendRight_apply_ne _ ha']
Cleared hypotheses: l, hl
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
⊢ Eq (α := ℤˣ) (((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodCongrRight σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)
have obtain : ∀ (l : List α) (hl : l.Nodup) (mem_l : ∀ (x : α), x ∈ l),
  Eq (α := ℤˣ) (((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodCongrRight σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)
Tactic: obtain ⟨l, hl, mem_l⟩ := Finite.exists_univ_list α
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
⊢ l.toFinset = univ
have apply : ⊤ ≤ l.toFinset
Tactic: apply eq_top_iff.mpr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
⊢ Eq (α := ℤˣ) (((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodCongrRight σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)
have l_to_finset : l.toFinset = univ
Tactic: have l_to_finset : l.toFinset = Finset.univ := by
    apply eq_top_iff.mpr
    intro b _
    exact List.mem_toFinset.mpr (mem_l b)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
l_to_finset : l.toFinset = univ
⊢ Eq (α := ℤˣ) (((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodCongrRight σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)
have rw : Eq (α := ℤˣ)
  (List.prod
    (List.map (comp (β := Perm (α × β)) (⇑sign : (a : Perm (α × β)) → ℤˣ) fun (a : α) ↦ prodExtendRight a (σ a)) l))
  (List.prod (List.map (fun (k : α) ↦ ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k)) l))
Tactic: rw [← prod_prodExtendRight σ hl mem_l, map_list_prod sign, List.map_map, ← l_to_finset,
    List.prod_toFinset _ hl]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
l_to_finset : l.toFinset = univ
⊢ Eq (α := ℤˣ)
    (List.prod
      (List.map (comp (β := Perm (α × β)) (⇑sign : (a : Perm (α × β)) → ℤˣ) fun (a : α) ↦ prodExtendRight a (σ a)) l))
    (List.prod (List.map (fun (k : α) ↦ ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k)) l))
have simp_rw : Eq (α := ℤˣ)
  (List.prod
    (List.map (comp (β := Perm (α × β)) (⇑sign : (a : Perm (α × β)) → ℤˣ) fun (a : α) ↦ prodExtendRight a (σ a)) l))
  (List.prod
    (List.map (fun (k : α) ↦ ((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodExtendRight k (σ k))) l))
Tactic: simp_rw [← fun a => sign_prodExtendRight a (σ a), Function.comp_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
⊢ Eq (α := ℤˣ) (((sign : Perm (β × α) →* ℤˣ) : (a : Perm (β × α)) → ℤˣ) (prodCongrLeft σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)
have refine : ∀ (x : β × α),
  Eq (α := α × β) ((prodComm β α : (a : β × α) → α × β) ((prodCongrLeft σ : (a : β × α) → β × α) x) : α × β)
    ((prodCongrRight σ : (a : α × β) → α × β) ((prodComm β α : (a : β × α) → α × β) x) : α × β)
Tactic: refine (sign_eq_sign_of_equiv _ _ (prodComm β α) ?_).trans (sign_prodCongrRight σ)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
this :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have rw : ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
Tactic: rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
this :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have rw₁ : ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
Tactic: rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
this :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw₁ :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have rw₂ : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
  (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1 * sumCongr 1 σb) : ℤˣ)
Tactic: rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
this :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw₁ :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
rw₂ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1 * sumCongr 1 σb) : ℤˣ)
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have rw₃ : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
  (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((σa * 1).sumCongr (1 * σb)) : ℤˣ)
Tactic: rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σa : Perm α
σb : Perm β
this :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ) ∧
    Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
rw₁ :
  ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1) : ℤˣ)
      (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (sumCongr 1 σb) : ℤˣ)
rw₂ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr 1 * sumCongr 1 σb) : ℤˣ)
rw₃ :
  Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
    (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((σa * 1).sumCongr (1 * σb)) : ℤˣ)
⊢ ((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) σa : ℤˣ)
      (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) σb : ℤˣ)
have rw₄ : Eq (α := ℤˣ) (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) (σa.sumCongr σb) : ℤˣ)
  (((sign : Perm (α ⊕ β) →* ℤˣ) : (a : Perm (α ⊕ β)) → ℤˣ) ((σa * 1).sumCongr σb) : ℤˣ)
Tactic: rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]