Theorem: BunchImpl.PreEquiv.sunit_right (BunchImpl/Equiv.lean)

State before:
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B sunit ↔ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)
Tactic:
constructor
State after:
case mp
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B sunit → B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)

case mpr
P✝ : Sort u_1
B : Bunch P✝
⊢ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit) → PreEquiv B sunit

State before:
case mp
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B sunit → B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)
Tactic:
intro h
State after:
case mp
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv B sunit
⊢ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)

State before:
case mp
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv B sunit
⊢ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)
Tactic:
generalize hA' : sunit = A' at h
State after:
case mp
P✝ : Sort u_1
B A' : Bunch P✝
hA' : sunit = A'
h : PreEquiv B A'
⊢ B = (cunit ,ᵇ A') ∨ B = (A' ,ᵇ cunit) ∨ B = (A' ;ᵇ A') ∨ B = (A' ;ᵇ A')

State before:
case mp
P✝ : Sort u_1
B A' : Bunch P✝
hA' : sunit = A'
h : PreEquiv B A'
⊢ B = (cunit ,ᵇ A') ∨ B = (A' ,ᵇ cunit) ∨ B = (A' ;ᵇ A') ∨ B = (A' ;ᵇ A')
Tactic:
induction h <;> simp_all
State after:
no goals

State before:
case mpr
P✝ : Sort u_1
B : Bunch P✝
⊢ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit) → PreEquiv B sunit
Tactic:
rintro (rfl|rfl|rfl|rfl)
State after:
case mpr.inl
P✝ : Sort u_1
⊢ PreEquiv (cunit ,ᵇ sunit) sunit

case mpr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ,ᵇ cunit) sunit

case mpr.inr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ sunit) sunit

case mpr.inr.inr.inr
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ sunit) sunit

State before:
case mpr.inl
P✝ : Sort u_1
⊢ PreEquiv (cunit ,ᵇ sunit) sunit
Tactic:
exact cunitL
State after:
no goals

State before:
case mpr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ,ᵇ cunit) sunit
Tactic:
exact cunitR
State after:
no goals

State before:
case mpr.inr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ sunit) sunit
Tactic:
exact sunitL
State after:
no goals

State before:
case mpr.inr.inr.inr
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ sunit) sunit
Tactic:
exact sunitR
State after:
no goals