awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Sign
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
simp_rw :
  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 })))) :
      ℤˣ)
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ)
        (↑l : List (Perm { x : α // p x })).prod :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
simp_rw [← hl'₂]
-- Module: Mathlib.GroupTheory.Perm.Sign
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 }))))
rw₂ rw₃ :
  HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length =
    HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length
⊢ 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 })))) :
      ℤˣ)

Tactic:
rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]

Premises used: And.right, List.length_map, Equiv.Perm.sign_prod_list_swap, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Sign
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 : β) : β)
⊢ ∀ (x : β), Eq (α := β) ((g : (a : β) → β) x : β) (((e.symm.trans f).trans e : (a : β) → β) x : β)

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Perm.Sign
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 : β) : β)
⊢ g = (e.symm.trans f).trans e

Tactic:
have hg : g = (e.symm.trans f).trans e := Equiv.ext <| by simp [h]
-- Module: Mathlib.GroupTheory.Perm.Sign
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) : ℤˣ)
rw₁ rw₂ :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) g : ℤˣ)

Tactic:
rw [hg, sign_symm_trans_trans]

Premises used: Equiv.Perm.sign_symm_trans_trans
-- Module: Mathlib.GroupTheory.Perm.Sign
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 : α),
    Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) x : α) : α) ((f : (a : α) → α) x : α) ↔ (f : (a : α) → α) x ≠ x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
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 : β),
    Ne (α := β) ((g : (a : β) → β) ((g : (a : β) → β) x : β) : β) ((g : (a : β) → β) x : β) ↔ (g : (a : β) → β) x ≠ x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
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 }
⊢ Ne (α := α) ((f : (a : α) → α) ((f : (a : α) → α) (↑x : α) : α) : α) ((f : (a : α) → α) (↑x : α) : α)

Tactic:
have : f (f x) ≠ f x := mt (fun h => f.injective h) x.2
-- Module: Mathlib.GroupTheory.Perm.Sign
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 : α) : α)
rw : i ((f : (a : α) → α) (↑x : α)) this ≠ i (↑x : α) ⋯
⊢ (g : (a : β) → β) (i (↑x : α) ⋯) ≠ i (↑x : α) ⋯

Tactic:
rw [← h _ x.2 this]

Premises used: Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Sign
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 : α) : α)
⊢ i ((f : (a : α) → α) (↑x : α)) this ≠ i (↑x : α) ⋯

Tactic:
mt (hi _ _ this x.2) x.2

Premises used: mt, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Sign
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 : α) : α)
⊢ i ((f : (a : α) → α) (↑x : α)) this ≠ i (↑x : α) ⋯

Tactic:
exact mt (hi _ _ this x.2) x.2

Premises used: mt, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
H :
  ∀ (a : α) (b : β),
    Eq (α := α × β)
      ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
      ((prodCongrRight σ : (a : α × β) → α × β) (a, b) : α × β)
⊢ List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) = prodCongrRight σ

Tactic:
ext ⟨a, b⟩ : 1
-- Module: Mathlib.GroupTheory.Perm.Sign
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)
⊢ a ∈ l

Tactic:
obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))

Premises used: Iff.mpr, Or.resolve_right, not_and
-- Module: Mathlib.GroupTheory.Perm.Sign
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) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)

Tactic:
obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))

Premises used: Iff.mpr, Or.resolve_right, not_and
-- Module: Mathlib.GroupTheory.Perm.Sign
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) : α × β)
rw₁ rw₂ : Eq (α := α × β) ((a, (σ 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) : α × β)

Tactic:
rw [prod_eq, prodCongrRight_apply]

Premises used: Equiv.prodCongrRight_apply
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
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)
⊢ Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((prodCongrRight σ : (a : α × β) → α × β) (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]
-- Module: Mathlib.GroupTheory.Perm.Sign
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)

Tactic:
Or.inr ⟨List.not_mem_nil, ?_⟩

Premises used: And.intro, List.not_mem_nil, Or.inr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : List.Nodup.{u_1} (α := α) []
H : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)
⊢ 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:
refine Or.inr ⟨List.not_mem_nil, ?_⟩

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.Perm.Sign
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)
H₂ H₃ : (a, b) = (a, b)
⊢ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
rw [List.map_nil, List.prod_nil, one_apply]

Premises used: List.prod_nil, Equiv.Perm.one_apply, List.map_nil
-- Module: Mathlib.GroupTheory.Perm.Sign
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 :
  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 (α := α × β)
        ((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:
rw [List.map_cons, List.prod_cons, mul_apply]

Premises used: List.map_cons, Equiv.Perm.mul_apply, List.prod_cons
-- Module: Mathlib.GroupTheory.Perm.Sign
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)
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)
⊢ 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⟩)

Premises used: List.nodup_cons, And.right, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Sign
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) : α × β)
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)
⊢ 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 [prod_eq]
-- Module: Mathlib.GroupTheory.Perm.Sign
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)
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)
⊢ 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 [prod_eq]
-- Module: Mathlib.GroupTheory.Perm.Sign
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)

Tactic:
Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩

Premises used: List.mem_cons_of_mem, And.intro, Or.inl