Theorem: BunchImpl.BunchWithHole.substX_idem (BunchImpl/Term/Bunch.lean)

State before:
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b ↔ Γ = hole
Tactic:
constructor
State after:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b → Γ = hole

case mpr
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ Γ = hole → substX b Γ = b

State before:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b → Γ = hole
Tactic:
intro h
State after:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
⊢ Γ = hole

State before:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
⊢ Γ = hole
Tactic:
have := sizeOf_substX b Γ
State after:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
this : sizeOf (substX b Γ) = sizeOf b + sizeOf Γ - 1
⊢ Γ = hole

State before:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
this : sizeOf (substX b Γ) = sizeOf b + sizeOf Γ - 1
⊢ Γ = hole
Tactic:
rw [h] at this
State after:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
this : sizeOf b = sizeOf b + sizeOf Γ - 1
⊢ Γ = hole

State before:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
this : sizeOf b = sizeOf b + sizeOf Γ - 1
⊢ Γ = hole
Tactic:
rw [Nat.add_sub_assoc (sizeOf_pos _)] at this
State after:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
this : sizeOf b = sizeOf b + (sizeOf Γ - Nat.succ 0)
⊢ Γ = hole

State before:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
this : sizeOf b = sizeOf b + (sizeOf Γ - Nat.succ 0)
⊢ Γ = hole
Tactic:
simp at this
State after:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
this : sizeOf Γ ≤ Nat.succ 0
⊢ Γ = hole

State before:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
this : sizeOf Γ ≤ Nat.succ 0
⊢ Γ = hole
Tactic:
cases Γ <;> simp at * <;> (
  apply Nat.pos_iff_ne_zero.mp (sizeOf_pos _) this
)
State after:
no goals

State before:
case mp.semiR
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
l✝ : Bunch P✝
r✝ : X P✝ V✝
h : X.semi (l✝ V✝) (substX b r✝) = b
this : sizeOf r✝ = 0
⊢ False
Tactic:
apply Nat.pos_iff_ne_zero.mp (sizeOf_pos _) this
State after:
no goals

State before:
case mpr
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ Γ = hole → substX b Γ = b
Tactic:
rintro rfl
State after:
case mpr
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
⊢ substX b hole = b

State before:
case mpr
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
⊢ substX b hole = b
Tactic:
rfl
State after:
no goals