Theorem: BunchImpl.Subbunch.comma_inv (BunchImpl/Subbunch.lean)

State before:
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ,ᵇ BR) b ↔ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
Tactic:
constructor
State after:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ,ᵇ BR) b → Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)

case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR) → Subbunch (BL ,ᵇ BR) b

State before:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ,ᵇ BR) b → Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
Tactic:
intro h
State after:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch (BL ,ᵇ BR) b
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)

State before:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch (BL ,ᵇ BR) b
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
Tactic:
cases h <;> simp_all
State after:
no goals

State before:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR) → Subbunch (BL ,ᵇ BR) b
Tactic:
intro h
State after:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
⊢ Subbunch (BL ,ᵇ BR) b

State before:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
⊢ Subbunch (BL ,ᵇ BR) b
Tactic:
cases h <;> aesop
State after:
no goals