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

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

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

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

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

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

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

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

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

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

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

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

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

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