-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_balLeft (l : RBNode α) (v : α) (r : RBNode α) :
    (balLeft l v r).reverse = balRight r.reverse v l.reverse

Proof state:
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ (match r with
      | node black a y b => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r).reverse =
    match r.reverse with
    | node black a x b => (node red a x b).balance1 v l.reverse
    | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v l.reverse)
    | l_1 => node red l_1 v l.reverse

Tactic:
split <;> simp

Result:
case h_2.h_3
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝² : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (y : α) (b : RBNode α), r = node black a y b → False
x✝ : ∀ (a : RBNode α) (y : α) (b : RBNode α) (z : α) (c : RBNode α), r = node red (node black a y b) z c → False
⊢ node red r.reverse v l.reverse =
    match r.reverse with
    | node black a x b => (node red a x b).balance1 v l.reverse
    | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v l.reverse)
    | l_1 => node red l_1 v l.reverse

Proof state:
case h_1
α : Type u_1
v : α
r l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
⊢ (node red (node black a✝ x✝ b✝) v r).reverse =
    match (node red a✝ x✝ b✝).reverse with
    | node red b y c => node red r.reverse v (node black b y c)
    | r_1 =>
      match r.reverse with
      | node black a x b => (node red a x b).balance1 v r_1
      | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r_1)
      | l => node red l v r_1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ ∀ (a : RBNode α) (x : α) (b : RBNode α), l.reverse = node red a x b → False

Tactic:
simp [reverse_eq_iff]

Result:
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ ∀ (a : RBNode α) (x : α) (b : RBNode α), ¬l = node red b.reverse x a.reverse

Proof state:
case h_2.h_3.x
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝² : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (y : α) (b : RBNode α), r = node black a y b → False
x✝ : ∀ (a : RBNode α) (y : α) (b : RBNode α) (z : α) (c : RBNode α), r = node red (node black a y b) z c → False
⊢ ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), r.reverse = node red a x (node black b y c) → False

Tactic:
simp [reverse_eq_iff]

Result:
case h_2.h_3.x
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝² : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (y : α) (b : RBNode α), r = node black a y b → False
x✝ : ∀ (a : RBNode α) (y : α) (b : RBNode α) (z : α) (c : RBNode α), r = node red (node black a y b) z c → False
⊢ ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α),
    ¬r = node red (node black c.reverse y b.reverse) x a.reverse

Proof state:
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ (match r with
      | node black a y b => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r).reverse =
    match l.reverse with
    | node red b y c => node red r.reverse v (node black b y c)
    | r_1 =>
      match r.reverse with
      | node black a x b => (node red a x b).balance1 v r_1
      | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r_1)
      | l => node red l v r_1

Tactic:
rw [balLeft.match_2.eq_2 _ _ _ _ (by simp [reverse_eq_iff]; intros; solve_by_elim)]

Result:
case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ (match r with
      | node black a y b => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r).reverse =
    match r.reverse with
    | node black a x b => (node red a x b).balance1 v l.reverse
    | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v l.reverse)
    | l_1 => node red l_1 v l.reverse

Proof state:
case h_2.h_3
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝² : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
r✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (y : α) (b : RBNode α), r = node black a y b → False
x✝ : ∀ (a : RBNode α) (y : α) (b : RBNode α) (z : α) (c : RBNode α), r = node red (node black a y b) z c → False
⊢ node red r.reverse v l.reverse =
    match r.reverse with
    | node black a x b => (node red a x b).balance1 v l.reverse
    | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v l.reverse)
    | l_1 => node red l_1 v l.reverse

Tactic:
rw [balRight.match_1.eq_3] <;> (simp [reverse_eq_iff]; intros; solve_by_elim)

Result:
no goals

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l with
      | node red a x b => node red (node black a x b) v r
      | l =>
        match r with
        | node black a y b => l.balance2 v (node red a y b)
        | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
        | r => node red l v r).reverse =
    match l.reverse with
    | node red b y c => node red r.reverse v (node black b y c)
    | r_1 =>
      match r.reverse with
      | node black a x b => (node red a x b).balance1 v r_1
      | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r_1)
      | l => node red l v r_1

Tactic:
split

Result:
case h_1
α : Type u_1
v : α
r l✝ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
⊢ (node red (node black a✝ x✝ b✝) v r).reverse =
    match (node red a✝ x✝ b✝).reverse with
    | node red b y c => node red r.reverse v (node black b y c)
    | r_1 =>
      match r.reverse with
      | node black a x b => (node red a x b).balance1 v r_1
      | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r_1)
      | l => node red l v r_1

case h_2
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
⊢ (match r with
      | node black a y b => l.balance2 v (node red a y b)
      | node red (node black a y b) z c => node red (node black l v a) y (b.balance2 z c.setRed)
      | r => node red l v r).reverse =
    match l.reverse with
    | node red b y c => node red r.reverse v (node black b y c)
    | r_1 =>
      match r.reverse with
      | node black a x b => (node red a x b).balance1 v r_1
      | node red a x (node black b y c) => node red (a.setRed.balance1 x b) y (node black c v r_1)
      | l => node red l v r_1

Proof state:
α : Type u_1
l : RBNode α
v : α
r l✝ : RBNode α
x✝¹ : ∀ (a : RBNode α) (x : α) (b : RBNode α), l = node red a x b → False
a✝ : RBNode α
x✝ : α
b✝ : RBNode α
⊢ ¬l = node red b✝.reverse x✝ a✝.reverse

Tactic:
solve_by_elim

Result:
no goals