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

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

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

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

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

State before:
case mp
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
A' : Bunch P✝
hA' : prop A = A'
h : PreEquiv B A'
⊢ B = (cunit ,ᵇ A') ∨ B = (A' ,ᵇ cunit) ∨ 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✝
A : Typ P✝
⊢ B = (cunit ,ᵇ prop A) ∨ B = (prop A ,ᵇ cunit) ∨ B = (sunit ;ᵇ prop A) ∨ B = (prop A ;ᵇ sunit) → PreEquiv B (prop A)
Tactic:
rintro (rfl|rfl|rfl|rfl)
State after:
case mpr.inl
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (cunit ,ᵇ prop A) (prop A)

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

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

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

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

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

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

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