Theorem: BunchImpl.Bunch.neq_right_semi (BunchImpl/Bunch.lean)

State before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
⊢ (b1 ;ᵇ b2) ≠ b2
Tactic:
intro h
State after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ;ᵇ b2) = b2
⊢ False

State before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ;ᵇ b2) = b2
⊢ False
Tactic:
have := congrArg sizeOf h
State after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ;ᵇ b2) = b2
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False

State before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ;ᵇ b2) = b2
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False
Tactic:
clear h
State after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False

State before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False
Tactic:
simp at this
State after:
no goals