Theorem: BunchImpl.BunchWithHole.subst_idem (BunchImpl/Bunch.lean)

State before:
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b ↔ Γ = hole
Tactic:
constructor
State after:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b → Γ = hole

case mpr
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ Γ = hole → subst b Γ = b

State before:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b → Γ = hole
Tactic:
intro h
State after:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst b Γ = b
⊢ Γ = hole

State before:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst b Γ = b
⊢ Γ = hole
Tactic:
have := sizeOf_subst b Γ
State after:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst b Γ = b
this : sizeOf (subst b Γ) = sizeOf b + sizeOf Γ - 1
⊢ Γ = hole

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

State before:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst 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✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst b Γ = b
this : sizeOf b = sizeOf b + (sizeOf Γ - Nat.succ 0)
⊢ Γ = hole

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

State before:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst b Γ = b
this : sizeOf Γ ≤ Nat.succ 0
⊢ Γ = hole
Tactic:
cases Γ <;> simp at * <;> (
  revert this
  suffices ¬ _ ≥ _ from this
  simp
  rw [Nat.add_assoc]
  apply Nat.lt_add_of_pos_right
  first | (apply Nat.add_pos_left; apply sizeOf_pos)
        | (apply Nat.add_pos_right; apply sizeOf_pos)
)
State after:
no goals

State before:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
this : 1 + sizeOf l✝ + sizeOf r✝ ≤ Nat.succ 0
⊢ False
Tactic:
revert this
State after:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 1 + sizeOf l✝ + sizeOf r✝ ≤ Nat.succ 0 → False

State before:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 1 + sizeOf l✝ + sizeOf r✝ ≤ Nat.succ 0 → False
Tactic:
suffices ¬ _ ≥ _ from this
State after:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ ¬Nat.succ 0 ≥ 1 + sizeOf l✝ + sizeOf r✝

State before:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ ¬Nat.succ 0 ≥ 1 + sizeOf l✝ + sizeOf r✝
Tactic:
simp
State after:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ Nat.succ 0 < 1 + sizeOf l✝ + sizeOf r✝

State before:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ Nat.succ 0 < 1 + sizeOf l✝ + sizeOf r✝
Tactic:
rw [Nat.add_assoc]
State after:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ Nat.succ 0 < 1 + (sizeOf l✝ + sizeOf r✝)

State before:
case mp.semiR
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ Nat.succ 0 < 1 + (sizeOf l✝ + sizeOf r✝)
Tactic:
apply Nat.lt_add_of_pos_right
State after:
case mp.semiR.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf l✝ + sizeOf r✝

State before:
case mp.semiR.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf l✝ + sizeOf r✝
Tactic:
first | (apply Nat.add_pos_left; apply sizeOf_pos)
      | (apply Nat.add_pos_right; apply sizeOf_pos)
State after:
no goals

State before:
case mp.semiR.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf l✝ + sizeOf r✝
Tactic:
(apply Nat.add_pos_left; apply sizeOf_pos)
State after:
case mp.semiR.h.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf l✝

State before:
case mp.semiR.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf l✝ + sizeOf r✝
Tactic:
apply Nat.add_pos_left
State after:
case mp.semiR.h.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf l✝

State before:
case mp.semiL.h.h
P✝ : Sort u_1
b : Bunch P✝
l✝ : BunchWithHole P✝
r✝ : Bunch P✝
h : (subst b l✝ ;ᵇ r✝) = b
⊢ 0 < sizeOf l✝
Tactic:
apply sizeOf_pos
State after:
no goals

State before:
case mp.semiR.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf l✝ + sizeOf r✝
Tactic:
(apply Nat.add_pos_right; apply sizeOf_pos)
State after:
no goals

State before:
case mp.semiR.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf l✝ + sizeOf r✝
Tactic:
apply Nat.add_pos_right
State after:
case mp.semiR.h.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf r✝

State before:
case mp.semiR.h.h
P✝ : Sort u_1
b l✝ : Bunch P✝
r✝ : BunchWithHole P✝
h : (l✝ ;ᵇ subst b r✝) = b
⊢ 0 < sizeOf r✝
Tactic:
apply sizeOf_pos
State after:
no goals

State before:
case mpr
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ Γ = hole → subst b Γ = b
Tactic:
rintro rfl
State after:
case mpr
P✝ : Sort u_1
b : Bunch P✝
⊢ subst b hole = b

State before:
case mpr
P✝ : Sort u_1
b : Bunch P✝
⊢ subst b hole = b
Tactic:
simp
State after:
no goals