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

State before:
P : Sort u
b1 b2 : Bunch P
⊢ (b1 ,ᵇ b2) ≠ b1
Tactic:
intro h
State after:
P : Sort u
b1 b2 : Bunch P
h : (b1 ,ᵇ b2) = b1
⊢ False

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

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

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

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