-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem RedRed.balance1 {l : RBNode α} {v : α} {r : RBNode α}
    (hl : l.RedRed p n) (hr : r.Balanced c n) : ∃ c, (balance1 l v r).Balanced c (n + 1)

Proof state:
case h_1
α : Type u_1
p : Prop
n : Nat
c : RBColor
v : α
r : RBNode α
hr : r.Balanced c n
x✝³ : RBNode α
x✝² : α
x✝¹ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
hl : RedRed p (node red (node red a✝ x✝ b✝) y✝ c✝) n
⊢ ∃ c, (node red (node black a✝ x✝ b✝) y✝ (node black c✝ v r)).Balanced c (n + 1)

Tactic:
have .redred _ (.red ha hb) hc := hl

Result:
case h_1
α : Type u_1
p : Prop
n : Nat
c : RBColor
v : α
r : RBNode α
hr : r.Balanced c n
x✝³ : RBNode α
x✝² : α
x✝¹ a✝¹ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
hl : RedRed p (node red (node red a✝¹ x✝ b✝) y✝ c✝) n
c₂✝ : RBColor
a✝ : p
ha : a✝¹.Balanced black n
hb : b✝.Balanced black n
hc : c✝.Balanced c₂✝ n
⊢ ∃ c, (node red (node black a✝¹ x✝ b✝) y✝ (node black c✝ v r)).Balanced c (n + 1)

Proof state:
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
x✝³ : RBNode α
x✝² : α
x✝¹ a✝⁴ : RBNode α
c₁✝ : RBColor
l✝ : RBNode α
v✝ : α
r✝ : RBNode α
x✝ : α
a✝³ : p
a✝² : a✝⁴.Balanced c₁✝ n
a✝¹ : l✝.Balanced black n
a✝ : r✝.Balanced black n
H1 :
  ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α),
    node red a✝⁴ x✝ (node red l✝ v✝ r✝) = node red (node red a x b) y c → False
H2 :
  ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α),
    node red a✝⁴ x✝ (node red l✝ v✝ r✝) = node red a x (node red b y c) → False
⊢ ∃ c, (node black (node red a✝⁴ x✝ (node red l✝ v✝ r✝)) v r).Balanced c (n + 1)

Tactic:
cases H2 _ _ _ _ _ rfl

Result:
no goals

Proof state:
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
x✝³ : RBNode α
x✝² : α
x✝¹ a✝¹ b✝ : RBNode α
x✝ : α
a✝ : p
ha : a✝¹.Balanced black n
hb : b✝.Balanced black n
H1 :
  ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α),
    node red a✝¹ x✝ b✝ = node red (node red a x b) y c → False
H2 :
  ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α),
    node red a✝¹ x✝ b✝ = node red a x (node red b y c) → False
⊢ ∃ c, (node black (node red a✝¹ x✝ b✝) v r).Balanced c (n + 1)

Tactic:
exact ⟨_, .black (.red ha hb) hr⟩

Result:
no goals

Proof state:
case h_3
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
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
⊢ ∃ c, (node black l v r).Balanced c (n + 1)

Tactic:
next H1 H2 => match hl with
| .balanced hl => exact ⟨_, .black hl hr⟩
| .redred _ (c₁ := black) (c₂ := black) ha hb => exact ⟨_, .black (.red ha hb) hr⟩
| .redred _ (c₁ := red) (.red ..) _ => cases H1 _ _ _ _ _ rfl
| .redred _ (c₂ := red) _ (.red ..) => cases H2 _ _ _ _ _ rfl

Result:
no goals

Proof state:
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
⊢ ∃ c,
    (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).Balanced
      c (n + 1)

Tactic:
split

Result:
case h_1
α : Type u_1
p : Prop
n : Nat
c : RBColor
v : α
r : RBNode α
hr : r.Balanced c n
x✝³ : RBNode α
x✝² : α
x✝¹ a✝ : RBNode α
x✝ : α
b✝ : RBNode α
y✝ : α
c✝ : RBNode α
hl : RedRed p (node red (node red a✝ x✝ b✝) y✝ c✝) n
⊢ ∃ c, (node red (node black a✝ x✝ b✝) y✝ (node black c✝ v r)).Balanced c (n + 1)

case h_2
α : Type u_1
p : Prop
n : Nat
c : RBColor
v : α
r : RBNode α
hr : r.Balanced c n
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
hl : RedRed p (node red a✝ x✝¹ (node red b✝ y✝ c✝)) n
⊢ ∃ c, (node red (node black a✝ x✝¹ b✝) y✝ (node black c✝ v r)).Balanced c (n + 1)

case h_3
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
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
⊢ ∃ c, (node black l v r).Balanced c (n + 1)

Proof state:
case h_2
α : Type u_1
p : Prop
n : Nat
c : RBColor
v : α
r : RBNode α
hr : r.Balanced c n
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
hl : RedRed p (node red a✝ x✝¹ (node red b✝ y✝ c✝)) n
⊢ ∃ c, (node red (node black a✝ x✝¹ b✝) y✝ (node black c✝ v r)).Balanced c (n + 1)

Tactic:
have .redred _ ha (.red hb hc) := hl

Result:
case h_2
α : Type u_1
p : Prop
n : Nat
c : RBColor
v : α
r : RBNode α
hr : r.Balanced c n
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
hl : RedRed p (node red a✝¹ x✝¹ (node red b✝ y✝ c✝)) n
c₁✝ : RBColor
a✝ : p
ha : a✝¹.Balanced c₁✝ n
hb : b✝.Balanced black n
hc : c✝.Balanced black n
⊢ ∃ c, (node red (node black a✝¹ x✝¹ b✝) y✝ (node black c✝ v r)).Balanced c (n + 1)

Proof state:
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
x✝³ : RBNode α
x✝² : α
x✝¹ l✝ : RBNode α
v✝ : α
r✝ b✝ : RBNode α
c₂✝ : RBColor
x✝ : α
a✝³ : p
a✝² : l✝.Balanced black n
a✝¹ : r✝.Balanced black n
a✝ : b✝.Balanced c₂✝ n
H1 :
  ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α),
    node red (node red l✝ v✝ r✝) x✝ b✝ = node red (node red a x b) y c → False
H2 :
  ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α),
    node red (node red l✝ v✝ r✝) x✝ b✝ = node red a x (node red b y c) → False
⊢ ∃ c, (node black (node red (node red l✝ v✝ r✝) x✝ b✝) v r).Balanced c (n + 1)

Tactic:
cases H1 _ _ _ _ _ rfl

Result:
no goals

Proof state:
α : Type u_1
p : Prop
n : Nat
c : RBColor
l : RBNode α
v : α
r : RBNode α
hl : RedRed p l n
hr : r.Balanced c n
x✝² : RBNode α
x✝¹ : α
x✝ : RBNode α
H1 : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red (node red a x b) y c → False
H2 : ∀ (a : RBNode α) (x : α) (b : RBNode α) (y : α) (c : RBNode α), l = node red a x (node red b y c) → False
⊢ ∃ c, (node black l v r).Balanced c (n + 1)

Tactic:
match hl with
| .balanced hl => exact ⟨_, .black hl hr⟩
| .redred _ (c₁ := black) (c₂ := black) ha hb => exact ⟨_, .black (.red ha hb) hr⟩
| .redred _ (c₁ := red) (.red ..) _ => cases H1 _ _ _ _ _ rfl
| .redred _ (c₂ := red) _ (.red ..) => cases H2 _ _ _ _ _ rfl

Result:
no goals

Proof state:
case h_2
α : Type u_1
p : Prop
n : Nat
c : RBColor
v : α
r : RBNode α
hr : r.Balanced c n
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
hl : RedRed p (node red a✝¹ x✝¹ (node red b✝ y✝ c✝)) n
c₁✝ : RBColor
a✝ : p
ha : a✝¹.Balanced c₁✝ n
hb : b✝.Balanced black n
hc : c✝.Balanced black n
⊢ ∃ c, (node red (node black a✝¹ x✝¹ b✝) y✝ (node black c✝ v r)).Balanced c (n + 1)

Tactic:
exact ⟨_, .red (.black ha hb) (.black hc hr)⟩

Result:
no goals