internlm/Lean-Github huggingface dataset:
Theorem: BunchImpl.Bunch.neq_right_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ;ᵇ b2) = b2
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False
Tactic:
clear h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False
Theorem: BunchImpl.Bunch.neq_right_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False
Tactic:
simp [instSizeOfBunch, semi] at this
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_self_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
⊢ b1 ≠ (b1 ;ᵇ b2)
Tactic:
intro h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : b1 = (b1 ;ᵇ b2)
⊢ False
Theorem: BunchImpl.Bunch.neq_self_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : b1 = (b1 ;ᵇ b2)
⊢ False
Tactic:
have := congrArg sizeOf h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : b1 = (b1 ;ᵇ b2)
this : sizeOf b1 = sizeOf (b1 ;ᵇ b2)
⊢ False
Theorem: BunchImpl.Bunch.neq_self_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : b1 = (b1 ;ᵇ b2)
this : sizeOf b1 = sizeOf (b1 ;ᵇ b2)
⊢ False
Tactic:
clear h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = sizeOf (b1 ;ᵇ b2)
⊢ False
Theorem: BunchImpl.Bunch.neq_self_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = sizeOf (b1 ;ᵇ b2)
⊢ False
Tactic:
simp [instSizeOfBunch, semi] at this
Proof 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
Theorem: BunchImpl.Bunch.neq_self_left_semi
Proof 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
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_self_right_semi
Proof state before:
P✝ : Sort u_1
b2 b1 : Bunch P✝
⊢ b2 ≠ (b1 ;ᵇ b2)
Tactic:
intro h
Proof state after:
P✝ : Sort u_1
b2 b1 : Bunch P✝
h : b2 = (b1 ;ᵇ b2)
⊢ False
Theorem: BunchImpl.Bunch.neq_self_right_semi
Proof state before:
P✝ : Sort u_1
b2 b1 : Bunch P✝
h : b2 = (b1 ;ᵇ b2)
⊢ False
Tactic:
have := congrArg sizeOf h
Proof state after:
P✝ : Sort u_1
b2 b1 : Bunch P✝
h : b2 = (b1 ;ᵇ b2)
this : sizeOf b2 = sizeOf (b1 ;ᵇ b2)
⊢ False
Theorem: BunchImpl.Bunch.neq_self_right_semi
Proof state before:
P✝ : Sort u_1
b2 b1 : Bunch P✝
h : b2 = (b1 ;ᵇ b2)
this : sizeOf b2 = sizeOf (b1 ;ᵇ b2)
⊢ False
Tactic:
clear h
Proof state after:
P✝ : Sort u_1
b2 b1 : Bunch P✝
this : sizeOf b2 = sizeOf (b1 ;ᵇ b2)
⊢ False
Theorem: BunchImpl.Bunch.neq_self_right_semi
Proof state before:
P✝ : Sort u_1
b2 b1 : Bunch P✝
this : sizeOf b2 = sizeOf (b1 ;ᵇ b2)
⊢ False
Tactic:
simp [instSizeOfBunch, semi] at this
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.sizeOf_pos
Proof state before:
P : Sort u_1
V : Sort u_2
h : X P V
⊢ sizeOf h > 0
Tactic:
induction h <;> simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.sizeOf_substX
Proof state before:
P V : Sort u_1
b : Bunch.X P V
h : X P V
⊢ sizeOf (substX b h) = sizeOf b + sizeOf h - 1
Tactic:
induction h <;> simp [subst, substX, comma, semi, instSizeOfBunch] at * <;>
  simp [*] <;> sorry
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof state before:
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b ↔ Γ = hole
Tactic:
constructor
Proof 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
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof state before:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b → Γ = hole
Tactic:
intro h
Proof state after:
case mp
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
h : substX b Γ = b
⊢ Γ = hole
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof 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 Γ
Proof 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
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof 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
Proof 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
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof 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
Proof 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
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof 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
Proof 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
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof 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
)
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof 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
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof state before:
case mpr
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ Γ = hole → substX b Γ = b
Tactic:
rintro rfl
Proof state after:
case mpr
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
⊢ substX b hole = b
Theorem: BunchImpl.BunchWithHole.substX_idem
Proof state before:
case mpr
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
⊢ substX b hole = b
Tactic:
rfl
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.idem_substX
Proof state before:
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ b = substX b Γ ↔ Γ = hole
Tactic:
rw [eq_comm]
Proof state after:
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b ↔ Γ = hole
Theorem: BunchImpl.BunchWithHole.idem_substX
Proof state before:
P✝ V✝ : Sort u_1
b : Bunch.X P✝ V✝
Γ : X P✝ V✝
⊢ substX b Γ = b ↔ Γ = hole
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.prop_eq
Proof state before:
P b : Type u_1
V : Bunch.X P b
Γ : BunchWithHole P
⊢ sorryAx ((fun x => Bunch.X P b) V) true = ↑(Γ b) V ↔
    sorryAx Prop true ∧ sorryAx (?m.4408005 Γ) true = sorryAx (?m.4408005 Γ) true
Tactic:
rw [eq_comm]
Proof state after:
P b : Type u_1
V : Bunch.X P b
Γ : BunchWithHole P
⊢ ↑(Γ b) V = sorryAx ((fun x => Bunch.X P b) V) true ↔
    sorryAx Prop true ∧ sorryAx (?m.4408005 Γ) true = sorryAx (?m.4408005 Γ) true


⊢ {P b : Type u_1} → {V : Bunch.X P b} → BunchWithHole P → Sort u_2
Theorem: BunchImpl.BunchWithHole.prop_eq
Proof state before:
P b : Type u_1
V : Bunch.X P b
Γ : BunchWithHole P
⊢ ↑(Γ b) V = sorryAx ((fun x => Bunch.X P b) V) true ↔
    sorryAx Prop true ∧ sorryAx (?m.4408005 Γ) true = sorryAx (?m.4408005 Γ) true


⊢ {P b : Type u_1} → {V : Bunch.X P b} → BunchWithHole P → Sort u_2
Tactic:
simp
Proof state after:
P b : Type u_1
V : Bunch.X P b
Γ : BunchWithHole P
⊢ ↑(Γ b) V = sorryAx (Bunch.X P b) true ↔ sorryAx Prop true


⊢ {P b : Type u_1} → {V : Bunch.X P b} → BunchWithHole P → Sort u_2
Theorem: BunchImpl.BunchWithHole.cunit_eq
Proof state before:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ sorryAx (X P b) true = Γ b ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true
Tactic:
rw [show (_ = _ ↔ _ = _) from ⟨Eq.symm, Eq.symm⟩]
Proof state after:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ Γ b = sorryAx (X P b) true ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true
Theorem: BunchImpl.BunchWithHole.cunit_eq
Proof state before:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ Γ b = sorryAx (X P b) true ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.sunit_eq
Proof state before:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ sorryAx (X P b) true = Γ b ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true
Tactic:
rw [show (_ = _ ↔ _ = _) from ⟨Eq.symm, Eq.symm⟩]
Proof state after:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ Γ b = sorryAx (X P b) true ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true
Theorem: BunchImpl.BunchWithHole.sunit_eq
Proof state before:
P : Type u_1
b : Sort u_2
Γ : BunchWithHole P
⊢ Γ b = sorryAx (X P b) true ↔ sorryAx Prop true ∧ b = sorryAx (Sort u_2) true
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Type u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
⊢ Γ (sorryAx (Sort u_2) true) = Γ' (sorryAx (Sort u_2) true) →
    (∃ Δ, φ = ?m.12180131 Δ ∧ Γ.comp Δ = Γ') ∨
      (∃ Δ, φ' = ?m.12180132 Δ ∧ Γ'.comp Δ = Γ) ∨
        ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ (Bunch P → Sort u_2 → sorryAx Prop true)
Tactic:
intro h
Proof state after:
P : Type u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
h : Γ (sorryAx (Sort u_2) true) = Γ' (sorryAx (Sort u_2) true)
⊢ (∃ Δ, φ = ?m.12180131 Δ ∧ Γ.comp Δ = Γ') ∨
    (∃ Δ, φ' = ?m.12180132 Δ ∧ Γ'.comp Δ = Γ) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ (Bunch P → Sort u_2 → sorryAx Prop true)
Theorem: BunchImpl.BunchWithHole.idem
Proof state before:
P : Type u_1
Γ : BunchWithHole P
b : Bunch P
⊢ sorryAx Prop true ↔ sorryAx Prop true
Tactic:
simp [FunLike.coe]
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.idem'
Proof state before:
P : Type u_1
Γ : BunchWithHole P
b : Bunch P
⊢ sorryAx Prop true ↔ sorryAx Prop true
Tactic:
simp [FunLike.coe]
Proof state after:
no goals
Theorem: BunchImpl.Subbunch.comma_inv
Proof state before:
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ,ᵇ BR) b ↔ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
Tactic:
constructor
Proof state after:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ,ᵇ BR) b → Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)

case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR) → Subbunch (BL ,ᵇ BR) b
Theorem: BunchImpl.Subbunch.comma_inv
Proof state before:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ,ᵇ BR) b → Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
Tactic:
intro h
Proof state after:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch (BL ,ᵇ BR) b
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
Theorem: BunchImpl.Subbunch.comma_inv
Proof state before:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch (BL ,ᵇ BR) b
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
Tactic:
cases h <;> simp_all
Proof state after:
no goals
Theorem: BunchImpl.Subbunch.comma_inv
Proof state before:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR) → Subbunch (BL ,ᵇ BR) b
Tactic:
intro h
Proof state after:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
⊢ Subbunch (BL ,ᵇ BR) b
Theorem: BunchImpl.Subbunch.comma_inv
Proof state before:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ,ᵇ BR)
⊢ Subbunch (BL ,ᵇ BR) b
Tactic:
cases h <;> aesop
Proof state after:
no goals
Theorem: BunchImpl.Subbunch.semi_inv
Proof state before:
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ;ᵇ BR) b ↔ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR)
Tactic:
constructor
Proof state after:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ;ᵇ BR) b → Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR)

case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR) → Subbunch (BL ;ᵇ BR) b
Theorem: BunchImpl.Subbunch.semi_inv
Proof state before:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch (BL ;ᵇ BR) b → Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR)
Tactic:
intro h
Proof state after:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch (BL ;ᵇ BR) b
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR)
Theorem: BunchImpl.Subbunch.semi_inv
Proof state before:
case mp
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch (BL ;ᵇ BR) b
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR)
Tactic:
cases h <;> simp_all
Proof state after:
no goals
Theorem: BunchImpl.Subbunch.semi_inv
Proof state before:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
⊢ Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR) → Subbunch (BL ;ᵇ BR) b
Tactic:
intro h
Proof state after:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR)
⊢ Subbunch (BL ;ᵇ BR) b
Theorem: BunchImpl.Subbunch.semi_inv
Proof state before:
case mpr
P✝ : Sort u_1
BL BR b : Bunch P✝
h : Subbunch BL b ∨ Subbunch BR b ∨ b = (BL ;ᵇ BR)
⊢ Subbunch (BL ;ᵇ BR) b
Tactic:
cases h <;> aesop
Proof state after:
no goals
Theorem: BunchImpl.Subbunch.trans
Proof state before:
P✝ : Sort u_1
b1 b2 b3 : Bunch P✝
⊢ Subbunch b1 b2 → Subbunch b2 b3 → Subbunch b1 b3
Tactic:
intro h1 h2
Proof state after:
P✝ : Sort u_1
b1 b2 b3 : Bunch P✝
h1 : Subbunch b1 b2
h2 : Subbunch b2 b3
⊢ Subbunch b1 b3
Theorem: BunchImpl.Subbunch.trans
Proof state before:
P✝ : Sort u_1
b1 b2 b3 : Bunch P✝
h1 : Subbunch b1 b2
h2 : Subbunch b2 b3
⊢ Subbunch b1 b3
Tactic:
induction h1 <;> cases h2 <;> simp_all
Proof state after:
no goals
Theorem: BunchImpl.Subbunch.size_lt
Proof state before:
P : Sort u_1
b1 B1 : Bunch P
⊢ Subbunch B1 b1 → sizeOf B1 ≥ sizeOf b1
Tactic:
intro h1
Proof state after:
P : Sort u_1
b1 B1 : Bunch P
h1 : Subbunch B1 b1
⊢ sizeOf B1 ≥ sizeOf b1
Theorem: BunchImpl.Subbunch.size_lt
Proof state before:
P : Sort u_1
b1 B1 : Bunch P
h1 : Subbunch B1 b1
⊢ sizeOf B1 ≥ sizeOf b1
Tactic:
induction h1 <;> simp <;> linarith
Proof state after:
no goals
Theorem: BunchImpl.Subbunch.subst_hole
Proof state before:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ Subbunch (↑Γ b) b
Tactic:
induction Γ <;> simp [*]
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
⊢ (b1 ,ᵇ b2) ≠ b1
Tactic:
intro h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ,ᵇ b2) = b1
⊢ False
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ,ᵇ b2) = b1
⊢ False
Tactic:
have := congrArg sizeOf h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ,ᵇ b2) = b1
this : sizeOf (b1 ,ᵇ b2) = sizeOf b1
⊢ False
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ,ᵇ b2) = b1
this : sizeOf (b1 ,ᵇ b2) = sizeOf b1
⊢ False
Tactic:
clear h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ,ᵇ b2) = sizeOf b1
⊢ False
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ,ᵇ b2) = sizeOf b1
⊢ False
Tactic:
simp at this
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : 1 + sizeOf b1 + sizeOf b2 = sizeOf b1
⊢ False
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : 1 + sizeOf b1 + sizeOf b2 = sizeOf b1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_right_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ,ᵇ b2) = sizeOf b2
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_self_left_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = sizeOf (b1 ,ᵇ b2)
⊢ False
Tactic:
simp at this
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = 1 + sizeOf b1 + sizeOf b2
⊢ False
Theorem: BunchImpl.Bunch.neq_self_left_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = 1 + sizeOf b1 + sizeOf b2
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_self_right_comma
Proof state before:
P✝ : Sort u_1
b2 b1 : Bunch P✝
this : sizeOf b2 = sizeOf (b1 ,ᵇ b2)
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ;ᵇ b2) = sizeOf b1
⊢ False
Tactic:
simp at this
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : 1 + sizeOf b1 + sizeOf b2 = sizeOf b1
⊢ False
Theorem: BunchImpl.Bunch.neq_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : 1 + sizeOf b1 + sizeOf b2 = sizeOf b1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_right_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_self_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = sizeOf (b1 ;ᵇ b2)
⊢ False
Tactic:
simp at this
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = 1 + sizeOf b1 + sizeOf b2
⊢ False
Theorem: BunchImpl.Bunch.neq_self_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = 1 + sizeOf b1 + sizeOf b2
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_self_right_semi
Proof state before:
P✝ : Sort u_1
b2 b1 : Bunch P✝
this : sizeOf b2 = sizeOf (b1 ;ᵇ b2)
⊢ False
Tactic:
simp at this
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.sizeOf_pos
Proof state before:
P : Sort u_1
h : BunchWithHole P
⊢ sizeOf h > 0
Tactic:
induction h <;> simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.sizeOf_subst
Proof state before:
P : Sort u_1
b : Bunch P
h : BunchWithHole P
⊢ sizeOf (subst b h) = sizeOf b + sizeOf h - 1
Tactic:
induction h <;> simp [subst, *] <;> sorry
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof state before:
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b ↔ Γ = hole
Tactic:
constructor
Proof 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
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof state before:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b → Γ = hole
Tactic:
intro h
Proof state after:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst b Γ = b
⊢ Γ = hole
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof state before:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst b Γ = b
⊢ Γ = hole
Tactic:
have := sizeOf_subst b Γ
Proof 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
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof 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
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof 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
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof state after:
case mp
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
h : subst b Γ = b
this : sizeOf Γ ≤ Nat.succ 0
⊢ Γ = hole
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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)
)
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof 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
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof 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✝
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof 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✝
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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]
Proof 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✝)
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof 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✝
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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)
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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)
Proof 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✝
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof 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✝
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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)
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof 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✝