-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem reverse_balance1 (l : RBNode α) (v : α) (r : RBNode α) :
    (balance1 l v r).reverse = balance2 r.reverse v l.reverse

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

Tactic:
intros

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

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

Tactic:
solve_by_elim

Result:
no goals

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

Tactic:
split <;> simp

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

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

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

Tactic:
intros

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

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

Tactic:
solve_by_elim

Result:
no goals

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

Tactic:
simp [reverse_eq_iff]

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

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

Tactic:
simp [reverse_eq_iff]

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

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

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

Result:
no goals

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

Tactic:
rw [balance2.match_1.eq_2]

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