Theorem: BunchImpl.Bunch.neq_self_left_semi (BunchImpl/Term/Bunch.lean)

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

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

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

State before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = sizeOf (b1 ;ᵇ b2)
⊢ False
Tactic:
simp [instSizeOfBunch, semi] at this
State after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 PUnit.{u_1}) = 1 + sizeOf (b1 PUnit.{u_1}) + sizeOf (b2 PUnit.{u_1})
⊢ False

State before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 PUnit.{u_1}) = 1 + sizeOf (b1 PUnit.{u_1}) + sizeOf (b2 PUnit.{u_1})
⊢ False
Tactic:
linarith
State after:
no goals