α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) (revzip l') (List.map Prod.fst (revzip l'))
⊢ revzip l' = List.map (fun x => (x, ↑l - x)) l'
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
⊢ revzip l' = List.map (fun x => (x, ↑l - x)) l'
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]
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) (revzip l') (List.map Prod.fst (revzip l'))
⊢ Forall₂ (fun a c => a = (c, ↑l - c)) (revzip l') l'
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) (revzip l') (List.map Prod.fst (revzip l'))
⊢ revzip l' = List.map (fun x => (x, ↑l - x)) l'
rw [← forall₂_eq_eq_eq, forall₂_map_right_iff]
no goals
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
this : Forall₂ (fun p s => p = (s, ↑l - s)) (revzip l') (List.map Prod.fst (revzip l'))
⊢ Forall₂ (fun a c => a = (c, ↑l - c)) (revzip l') l'
simpa using this
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
⊢ ∀ (x : Multiset α × Multiset α), x ∈ revzip l' → x = (x.fst, ↑l - x.fst)
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
⊢ Forall₂ (fun p s => p = (s, ↑l - s)) (revzip l') (List.map Prod.fst (revzip l'))
rw [forall₂_map_right_iff, forall₂_same]
case mk
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
s t : Multiset α
h : (s, t) ∈ revzip l'
⊢ (s, t) = ((s, t).fst, ↑l - (s, t).fst)
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
⊢ ∀ (x : Multiset α × Multiset α), x ∈ revzip l' → x = (x.fst, ↑l - x.fst)
rintro ⟨s, t⟩ h
case mk
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
s t : Multiset α
h : (s, t) ∈ revzip l'
⊢ (s, t) = (s, ↑l - s)
case mk
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
s t : Multiset α
h : (s, t) ∈ revzip l'
⊢ (s, t) = ((s, t).fst, ↑l - (s, t).fst)
dsimp
no goals
case mk
α✝ : Type ?u.31102
α : Type u
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ revzip l' → x.fst + x.snd = ↑l
s t : Multiset α
h : (s, t) ∈ revzip l'
⊢ (s, t) = (s, ↑l - s)
rw [← H h, add_tsub_cancel_left]