Theorem: BunchImpl.BunchWithHole.eq_comma (BunchImpl/Bunch.lean)

State before:
P : Sort u_1
b Δ₁ Δ₂ : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = (Δ₁ ,ᵇ Δ₂) ↔
    Γ = hole ∧ b = (Δ₁ ,ᵇ Δ₂) ∨ (∃ Γ', Γ = commaL Γ' Δ₂ ∧ ↑Γ' b = Δ₁) ∨ ∃ Γ', Γ = commaR Δ₁ Γ' ∧ ↑Γ' b = Δ₂
Tactic:
cases Γ <;> aesop
State after:
no goals