-- Mathlib/GroupTheory/Perm/Sign.lean
theorem prod_prodExtendRight {α : Type*} [DecidableEq α] (σ : α → Perm β) {l : List α}
    (hl : l.Nodup) (mem_l : ∀ a, a ∈ l) :
    (l.map fun a => prodExtendRight a (σ a)).prod = prodCongrRight σ

Proof state:
case H.mk.cons
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
⊢ a ∈ a' :: l ∧ (List.map (fun a => prodExtendRight a (σ a)) (a' :: l)).prod (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (List.map (fun a => prodExtendRight a (σ a)) (a' :: l)).prod (a, b) = (a, b)

Tactic:
rw [List.map_cons, List.prod_cons, mul_apply]

Result:
case H.mk.cons
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
⊢ a ∈ a' :: l ∧
      (prodExtendRight a' (σ a')) ((List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b)) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) ((List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b)) = (a, b)

Proof state:
case H.mk.nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ a ∈ [] ∧ (List.map (fun a => prodExtendRight a (σ a)) []).prod (a, b) = (a, (σ a) b) ∨
    a ∉ [] ∧ (List.map (fun a => prodExtendRight a (σ a)) []).prod (a, b) = (a, b)

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

Result:
case H.mk.nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ (List.map (fun a => prodExtendRight a (σ a)) []).prod (a, b) = (a, b)

Proof state:
case neg
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
not_mem_l : a ∉ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : ¬a = a'
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Tactic:
refine Or.inr ⟨fun h => not_or_intro ha' not_mem_l ((List.mem_cons).mp h), ?_⟩

Result:
case neg
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
not_mem_l : a ∉ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : ¬a = a'
⊢ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Proof state:
case H.mk.cons.inr.intro
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
not_mem_l : a ∉ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Tactic:
by_cases ha' : a = a'

Result:
case pos
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
not_mem_l : a ∉ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : a = a'
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)

case neg
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
not_mem_l : a ∉ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : ¬a = a'
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Proof state:
case H.mk.nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ (List.map (fun a => prodExtendRight a (σ a)) []).prod (a, b) = (a, b)

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

Result:
no goals

Proof state:
case H.mk
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
a : α
b : β
⊢ a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
    a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)

Tactic:
induction' l with a' l ih

Result:
case H.mk.nil
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
hl : [].Nodup
⊢ a ∈ [] ∧ (List.map (fun a => prodExtendRight a (σ a)) []).prod (a, b) = (a, (σ a) b) ∨
    a ∉ [] ∧ (List.map (fun a => prodExtendRight a (σ a)) []).prod (a, b) = (a, b)

case H.mk.cons
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
⊢ a ∈ a' :: l ∧ (List.map (fun a => prodExtendRight a (σ a)) (a' :: l)).prod (a, b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (List.map (fun a => prodExtendRight a (σ a)) (a' :: l)).prod (a, b) = (a, b)

Proof state:
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
⊢ (List.map (fun a => prodExtendRight a (σ a)) l).prod = prodCongrRight σ

Tactic:
ext ⟨a, b⟩ : 1

Result:
case H.mk
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
⊢ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (prodCongrRight σ) (a, b)

Proof state:
case H.mk
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
⊢ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (prodCongrRight σ) (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]

Result:
case H.mk
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
⊢ a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
    a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)

Proof state:
case intro
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
    a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
left✝ : a ∈ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (prodCongrRight σ) (a, b)

Tactic:
rw [prod_eq, prodCongrRight_apply]

Result:
no goals