awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
p : α → Prop
inst_2 : DecidablePred p
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
l : { l : List (Perm { x : α // p x }) // l.prod = f.subtypePerm (p := p) h₁ ∧ ∀ g ∈ l, g.IsSwap } :=
  Trunc.out (f.subtypePerm (p := p) h₁).truncSwapFactors
hl' :
  ∀ (g' : Perm α),
    Membership.mem (γ := List (Perm α))
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))
        g' →
      g'.IsSwap
hl'₂ :
  List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f
rw :
  HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length =
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
      (List.prod
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x }))))
rw₁ :
  HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length =
    HPow.hPow (α := ℤˣ) (-1)
      (List.length (α := Perm α)
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x }))))
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ)
        (↑l : List (Perm { x : α // p x })).prod :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (List.prod
          (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
            (↑l : List (Perm { x : α // p x })))) :
      ℤˣ)
have rw₂ : HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length =
  HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length
Tactic: rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]
-- 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 β
f : Perm α
g : Perm β
e : α ≃ β
h :
  ∀ (x : α),
    Eq.{v + 1} (α := β) ((e : (a : α) → β) ((f : (a : α) → α) x : α) : β)
      ((g : (a : β) → β) ((e : (a : α) → β) x : β) : β)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) g : ℤˣ)
have hg : g = (e.symm.trans f).trans e
Tactic: have hg : g = (e.symm.trans f).trans e := Equiv.ext <| by simp [h]
-- 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 β
f : Perm α
g : Perm β
e : α ≃ β
h :
  ∀ (x : α),
    Eq.{v + 1} (α := β) ((e : (a : α) → β) ((f : (a : α) → α) x : α) : β)
      ((g : (a : β) → β) ((e : (a : α) → β) x : β) : β)
hg : g = (e.symm.trans f).trans e
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) g : ℤˣ)
have rw : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
  (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) ((e.symm.trans f).trans e) : ℤˣ)
Tactic: rw [hg, sign_symm_trans_trans]
-- 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 β
f : Perm α
g : Perm β
e : α ≃ β
h :
  ∀ (x : α),
    Eq.{v + 1} (α := β) ((e : (a : α) → β) ((f : (a : α) → α) x : α) : β)
      ((g : (a : β) → β) ((e : (a : α) → β) x : β) : β)
hg : g = (e.symm.trans f).trans e
rw :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) ((e.symm.trans f).trans e) : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) g : ℤˣ)
have rw₁ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: rw [hg, sign_symm_trans_trans]
-- 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 β
f : Perm α
g : Perm β
i : (x : α) → (f : (a : α) → α) x ≠ x → β
h :
  ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x)
    (hx' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)),
    i ((f : (a : α) → α) x) hx' = (g : (a : β) → β) (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : (f : (a : α) → α) x₁ ≠ x₁) (hx₂ : (f : (a : α) → α) x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), (g : (a : β) → β) y ≠ y → ∃ (x : α) (hx : (f : (a : α) → α) x ≠ x), i x hx = y
x : { x : α // (f : (a : α) → α) x ≠ x }
⊢ (g : (a : β) → β) (i (↑x : α) ⋯) ≠ i (↑x : α) ⋯
have this : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) (↑x : α) : α) : α) ((f : (a : α) → α) (↑x : α) : α)
Tactic: have : f (f x) ≠ f x := mt (fun h => f.injective h) x.2
-- 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 β
f : Perm α
g : Perm β
i : (x : α) → (f : (a : α) → α) x ≠ x → β
h :
  ∀ (x : α) (hx : (f : (a : α) → α) x ≠ x)
    (hx' : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α)),
    i ((f : (a : α) → α) x) hx' = (g : (a : β) → β) (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : (f : (a : α) → α) x₁ ≠ x₁) (hx₂ : (f : (a : α) → α) x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), (g : (a : β) → β) y ≠ y → ∃ (x : α) (hx : (f : (a : α) → α) x ≠ x), i x hx = y
x : { x : α // (f : (a : α) → α) x ≠ x }
this : Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) (↑x : α) : α) : α) ((f : (a : α) → α) (↑x : α) : α)
⊢ (g : (a : β) → β) (i (↑x : α) ⋯) ≠ i (↑x : α) ⋯
have rw : i ((f : (a : α) → α) (↑x : α)) this ≠ i (↑x : α) sorry
Tactic: rw [← h _ x.2 this]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
⊢ List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) = prodCongrRight σ
have H : ∀ (a : α) (b : β),
  Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
Tactic: ext ⟨a, b⟩ : 1
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  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)
⊢ Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
have left : a ∈ l
Tactic: obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  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)
left : a ∈ l
⊢ Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
have prod_eq : Eq (α := α × β) ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
  ((a, (σ a : (a : β) → β) b) : α × β)
Tactic: obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  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)
left : a ∈ l
prod_eq :
  Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
⊢ Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
have rw : Eq (α := α × β) ((a, (σ a : (a : β) → β) b) : α × β) ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
Tactic: rw [prod_eq, prodCongrRight_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  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)
left : a ∈ l
prod_eq :
  Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
rw : Eq (α := α × β) ((a, (σ a : (a : β) → β) b) : α × β) ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
⊢ Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
have rw₁ : Eq (α := α × β) ((a, (σ a : (a : β) → β) b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)
Tactic: rw [prod_eq, prodCongrRight_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
⊢ Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
have H : 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)
Tactic: suffices a ∈ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, σ a b) ∨
      a ∉ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, b) by
    obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))
    rw [prod_eq, prodCongrRight_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
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)
have H : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: refine Or.inr ⟨List.not_mem_nil, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : List.Nodup.{u_1} (α := α) []
⊢ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)
have H : (List.prod [] : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: rw [List.map_nil, List.prod_nil, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : List.Nodup.{u_1} (α := α) []
H : (List.prod [] : (a : α × β) → α × β) (a, b) = (a, b)
⊢ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)
have H₁ : (1 : (a : α × β) → α × β) (a, b) = (a, b)
Tactic: rw [List.map_nil, List.prod_nil, one_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : List.Nodup.{u_1} (α := α) []
H : (List.prod [] : (a : α × β) → α × β) (a, b) = (a, b)
H₁ : (1 : (a : α × β) → α × β) (a, b) = (a, b)
⊢ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)
have H₂ : (a, b) = (a, b)
Tactic: rw [List.map_nil, List.prod_nil, one_apply]
-- 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
⊢ 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)
have H : a ∈ a' :: l ∧
    Eq (α := α × β)
      ((prodExtendRight a' (σ a') : (a : α × β) → α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) :
        α × β)
      ((a, (σ a : (a : β) → β) b) : α × β) ∨
  a ∉ a' :: l ∧
    (prodExtendRight a' (σ a') : (a : α × β) → α × β)
        ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) =
      (a, b)
Tactic: rw [List.map_cons, List.prod_cons, mul_apply]
-- 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
⊢ a ∈ a' :: l ∧
      Eq (α := α × β)
        ((prodExtendRight a' (σ a') : (a : α × β) → α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) :
          α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧
      (prodExtendRight a' (σ a') : (a : α × β) → α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) =
        (a, b)
have H : ∀ (mem_l : a ∈ l)
  (prod_eq :
    Eq (α := α × β)
      ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
      ((a, (σ a : (a : β) → β) b) : α × β)),
  a ∈ a' :: l ∧
      Eq (α := α × β)
        ((prodExtendRight a' (σ a') : (a : α × β) → α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) :
          α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧
      (prodExtendRight a' (σ a') : (a : α × β) → α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) =
        (a, b)
Tactic: rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨notMem_l, prod_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
H :
  ∀ (mem_l : a ∈ l)
    (prod_eq :
      Eq (α := α × β)
        ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β)),
    a ∈ a' :: l ∧
        Eq (α := α × β)
          ((prodExtendRight a' (σ a') : (a : α × β) → α × β)
              ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) :
            α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ a' :: l ∧
        (prodExtendRight a' (σ a') : (a : α × β) → α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) =
          (a, b)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β)
        ((prodExtendRight a' (σ a') : (a : α × β) → α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) :
          α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧
      (prodExtendRight a' (σ a') : (a : α × β) → α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) =
        (a, b)
have H₁ : ∀ (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 : α × β) → α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) :
          α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧
      (prodExtendRight a' (σ a') : (a : α × β) → α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) =
        (a, b)
Tactic: rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨notMem_l, prod_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
mem_l : a ∈ l
prod_eq :
  Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β)
        ((prodExtendRight a' (σ a') : (a : α × β) → α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) :
          α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧
      (prodExtendRight a' (σ a') : (a : α × β) → α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) =
        (a, b)
have H : a ∈ a' :: l ∧
    Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) : α × β)
      ((a, (σ a : (a : β) → β) b) : α × β) ∨
  a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) = (a, b)
Tactic: rw [prod_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)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β)
        ((prodExtendRight a' (σ a') : (a : α × β) → α × β)
            ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) :
          α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧
      (prodExtendRight a' (σ a') : (a : α × β) → α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b)) =
        (a, b)
have H : 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 [prod_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
mem_l : a ∈ l
prod_eq :
  Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) = (a, b)
have H : Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) : α × β)
  ((a, (σ a : (a : β) → β) b) : α × β)
Tactic: refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩
-- 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
mem_l : a ∈ l
prod_eq :
  Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
⊢ Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
have H : Eq (α := α × β) ((a, (σ a : (a : β) → β) b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)
Tactic: rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]