-- Mathlib/Data/Multiset/Powerset.lean
theorem revzip_powersetAux_lemma {α : Type*} [DecidableEq α] (l : List α) {l' : List (Multiset α)}
    (H : ∀ ⦃x : _ × _⦄, x ∈ revzip l' → x.1 + x.2 = ↑l) :
    revzip l' = l'.map fun x => (x, (l : Multiset α) - x)

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ l'.revzip = List.map (fun x => (x, ↑l - x)) l'

Tactic:
have :
  Forall₂ (fun (p : Multiset α × Multiset α) (s : Multiset α) => p = (s, ↑l - s)) (revzip l')
    ((revzip l').map Prod.fst) := by
  rw [forall₂_map_right_iff, forall₂_same]
  rintro ⟨s, t⟩ h
  dsimp
  rw [← H h, add_tsub_cancel_left]

Result:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ l'.revzip = List.map (fun x => (x, ↑l - x)) l'

Proof state:
case mk
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = (s, ↑l - s)

Tactic:
rw [← H h, add_tsub_cancel_left]

Result:
no goals

Proof state:
case mk
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = ((s, t).1, ↑l - (s, t).1)

Tactic:
dsimp

Result:
case mk
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = (s, ↑l - s)

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ Forall₂ (fun p s => p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)

Tactic:
rw [forall₂_map_right_iff, forall₂_same]

Result:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ ∀ x ∈ l'.revzip, x = (x.1, ↑l - x.1)

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ Forall₂ (fun a c => a = (c, ↑l - c)) l'.revzip l'

Tactic:
simpa using this

Result:
no goals

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ l'.revzip = List.map (fun x => (x, ↑l - x)) l'

Tactic:
rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]

Result:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) l'.revzip (List.map Prod.fst l'.revzip)
⊢ Forall₂ (fun a c => a = (c, ↑l - c)) l'.revzip l'

Proof state:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ ∀ x ∈ l'.revzip, x = (x.1, ↑l - x.1)

Tactic:
rintro ⟨s, t⟩ h

Result:
case mk
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
s t : Multiset α
h : (s, t) ∈ l'.revzip
⊢ (s, t) = ((s, t).1, ↑l - (s, t).1)