-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_union_of_disjoint [DecidableEq α] {s t : Finset α} (h : Disjoint s t)
    (f : α → β) (comm : { x | x ∈ s ∪ t }.Pairwise (Commute on f)) :
    noncommProd (s ∪ t) f comm =
      noncommProd s f (comm.mono <| coe_subset.2 subset_union_left) *
        noncommProd t f (comm.mono <| coe_subset.2 subset_union_right)

Proof state:
case h.e'_2
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ ↑{ val := ↑(sl ++ tl), nodup := ⋯ } = {x | x ∈ sl.toFinset ∪ tl.toFinset}

Tactic:
simp [Set.ext_iff]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ sl.toFinset ∪ tl.toFinset = { val := ↑(sl ++ tl), nodup := ⋯ }

Tactic:
ext

Result:
case h
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
a✝ : α
⊢ a✝ ∈ sl.toFinset ∪ tl.toFinset ↔ a✝ ∈ { val := ↑(sl ++ tl), nodup := ⋯ }

Proof state:
case intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
t : Finset α
f : α → β
sl : List α
sl' : sl.Nodup
h : Disjoint sl.toFinset t
comm : {x | x ∈ sl.toFinset ∪ t}.Pairwise (Commute on f)
⊢ (sl.toFinset ∪ t).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * t.noncommProd f ⋯

Tactic:
obtain ⟨tl, tl', rfl⟩ := exists_list_nodup_eq t

Result:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : Disjoint sl.toFinset tl.toFinset
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ (sl.toFinset ∪ tl.toFinset).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * tl.toFinset.noncommProd f ⋯

Proof state:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ (sl.toFinset ∪ tl.toFinset).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * tl.toFinset.noncommProd f ⋯

Tactic:
calc noncommProd (List.toFinset sl ∪ List.toFinset tl) f comm
   = noncommProd ⟨↑(sl ++ tl), Multiset.coe_nodup.2 (sl'.append tl' h)⟩ f
       (by convert comm; simp [Set.ext_iff]) := noncommProd_congr (by ext; simp) (by simp) _
 _ = noncommProd (List.toFinset sl) f (comm.mono <| coe_subset.2 subset_union_left) *
       noncommProd (List.toFinset tl) f (comm.mono <| coe_subset.2 subset_union_right) := by
  simp [noncommProd, List.dedup_eq_self.2 sl', List.dedup_eq_self.2 tl', h]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ { val := ↑(sl ++ tl), nodup := ⋯ }.noncommProd f ⋯ = sl.toFinset.noncommProd f ⋯ * tl.toFinset.noncommProd f ⋯

Tactic:
simp [noncommProd, List.dedup_eq_self.2 sl', List.dedup_eq_self.2 tl', h]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ (↑{ val := ↑(sl ++ tl), nodup := ⋯ }).Pairwise (Commute on f)

Tactic:
convert comm

Result:
case h.e'_2
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ ↑{ val := ↑(sl ++ tl), nodup := ⋯ } = {x | x ∈ sl.toFinset ∪ tl.toFinset}

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s t : Finset α
h : Disjoint s t
f : α → β
comm : {x | x ∈ s ∪ t}.Pairwise (Commute on f)
⊢ (s ∪ t).noncommProd f comm = s.noncommProd f ⋯ * t.noncommProd f ⋯

Tactic:
obtain ⟨sl, sl', rfl⟩ := exists_list_nodup_eq s

Result:
case intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
t : Finset α
f : α → β
sl : List α
sl' : sl.Nodup
h : Disjoint sl.toFinset t
comm : {x | x ∈ sl.toFinset ∪ t}.Pairwise (Commute on f)
⊢ (sl.toFinset ∪ t).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * t.noncommProd f ⋯

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ ∀ x ∈ { val := ↑(sl ++ tl), nodup := ⋯ }, f x = f x

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : Disjoint sl.toFinset tl.toFinset
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ (sl.toFinset ∪ tl.toFinset).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * tl.toFinset.noncommProd f ⋯

Tactic:
rw [List.disjoint_toFinset_iff_disjoint] at h

Result:
case intro.intro.intro.intro
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
⊢ (sl.toFinset ∪ tl.toFinset).noncommProd f comm = sl.toFinset.noncommProd f ⋯ * tl.toFinset.noncommProd f ⋯

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
f : α → β
sl : List α
sl' : sl.Nodup
tl : List α
tl' : tl.Nodup
h : sl.Disjoint tl
comm : {x | x ∈ sl.toFinset ∪ tl.toFinset}.Pairwise (Commute on f)
a✝ : α
⊢ a✝ ∈ sl.toFinset ∪ tl.toFinset ↔ a✝ ∈ { val := ↑(sl ++ tl), nodup := ⋯ }

Tactic:
simp

Result:
no goals