internlm/Lean-Github huggingface dataset:
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof 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
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof state before:
case mpr
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ Γ = hole → subst b Γ = b
Tactic:
rintro rfl
Proof state after:
case mpr
P✝ : Sort u_1
b : Bunch P✝
⊢ subst b hole = b
Theorem: BunchImpl.BunchWithHole.subst_idem
Proof state before:
case mpr
P✝ : Sort u_1
b : Bunch P✝
⊢ subst b hole = b
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.idem_subst
Proof state before:
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ b = subst b Γ ↔ Γ = hole
Tactic:
rw [eq_comm]
Proof state after:
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b ↔ Γ = hole
Theorem: BunchImpl.BunchWithHole.idem_subst
Proof state before:
P✝ : Sort u_1
b : Bunch P✝
Γ : BunchWithHole P✝
⊢ subst b Γ = b ↔ Γ = hole
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.comp_hole
Proof state before:
P : Sort u_1
Γ : BunchWithHole P
⊢ Γ.comp hole = Γ
Tactic:
induction Γ <;> simp_all
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.comp_def
Proof state before:
P : Sort u_1
h1 h2 : BunchWithHole P
b : Bunch P
⊢ ↑(h1.comp h2) b = ↑h1 (↑h2 b)
Tactic:
induction h1 <;> simp_all [comp, FunLike.coe, subst]
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_prop
Proof state before:
P : Sort u_1
b : Bunch P
φ : Typ P
Γ : BunchWithHole P
⊢ ↑Γ b = prop φ ↔ Γ = hole ∧ b = prop φ
Tactic:
cases Γ <;> simp [FunLike.coe, subst]
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.prop_eq
Proof state before:
P : Sort u_1
φ : Typ P
b : Bunch P
Γ : BunchWithHole P
⊢ prop φ = ↑Γ b ↔ Γ = hole ∧ b = prop φ
Tactic:
rw [show (prop φ = _ ↔ _ = prop φ) from ⟨Eq.symm, Eq.symm⟩]
Proof state after:
P : Sort u_1
φ : Typ P
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = prop φ ↔ Γ = hole ∧ b = prop φ
Theorem: BunchImpl.BunchWithHole.prop_eq
Proof state before:
P : Sort u_1
φ : Typ P
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = prop φ ↔ Γ = hole ∧ b = prop φ
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_cunit
Proof state before:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = cunit ↔ Γ = hole ∧ b = cunit
Tactic:
cases Γ <;> simp [FunLike.coe, subst]
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.cunit_eq
Proof state before:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ cunit = ↑Γ b ↔ Γ = hole ∧ b = cunit
Tactic:
rw [show (_ = _ ↔ _ = _) from ⟨Eq.symm, Eq.symm⟩]
Proof state after:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = cunit ↔ Γ = hole ∧ b = cunit
Theorem: BunchImpl.BunchWithHole.cunit_eq
Proof state before:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = cunit ↔ Γ = hole ∧ b = cunit
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_sunit
Proof state before:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = sunit ↔ Γ = hole ∧ b = sunit
Tactic:
cases Γ <;> simp [FunLike.coe, subst]
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.sunit_eq
Proof state before:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ sunit = ↑Γ b ↔ Γ = hole ∧ b = sunit
Tactic:
rw [show (_ = _ ↔ _ = _) from ⟨Eq.symm, Eq.symm⟩]
Proof state after:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = sunit ↔ Γ = hole ∧ b = sunit
Theorem: BunchImpl.BunchWithHole.sunit_eq
Proof state before:
P : Sort u_1
b : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = sunit ↔ Γ = hole ∧ b = sunit
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_comma
Proof state before:
P : Sort u_1
b Δ₁ Δ₂ : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = (Δ₁ ,ᵇ Δ₂) ↔
    Γ = hole ∧ b = (Δ₁ ,ᵇ Δ₂) ∨ (∃ Γ', Γ = commaL Γ' Δ₂ ∧ ↑Γ' b = Δ₁) ∨ ∃ Γ', Γ = commaR Δ₁ Γ' ∧ ↑Γ' b = Δ₂
Tactic:
cases Γ <;> aesop
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_semi
Proof state before:
P : Sort u_1
b Δ₁ Δ₂ : Bunch P
Γ : BunchWithHole P
⊢ ↑Γ b = (Δ₁ ;ᵇ Δ₂) ↔
    Γ = hole ∧ b = (Δ₁ ;ᵇ Δ₂) ∨ (∃ Γ', Γ = semiL Γ' Δ₂ ∧ ↑Γ' b = Δ₁) ∨ ∃ Γ', Γ = semiR Δ₁ Γ' ∧ ↑Γ' b = Δ₂
Tactic:
cases Γ <;> aesop
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
⊢ ↑Γ φ = ↑Γ' φ' →
    (∃ Δ, φ = ↑Δ φ' ∧ Γ.comp Δ = Γ') ∨
      (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = Γ) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
intro h
Proof state after:
P : Sort u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
h : ↑Γ φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ Γ.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = Γ) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
h : ↑Γ φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ Γ.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = Γ) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
induction Γ generalizing Γ'
Proof state after:
case hole
P : Sort u_1
φ φ' : Bunch P
Γ' : BunchWithHole P
h : ↑hole φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ hole.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = hole) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = hole ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

case commaL
P : Sort u_1
φ φ' : Bunch P
l✝ : BunchWithHole P
r✝ : Bunch P
l_ih✝ :
  ∀ {Γ' : BunchWithHole P},
    ↑l✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ l✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = l✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = l✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑(commaL l✝ r✝) φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (commaL l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = commaL l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = commaL l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

case commaR
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
r_ih✝ :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑(commaR l✝ r✝) φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (commaR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = commaR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = commaR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

case semiL
P : Sort u_1
φ φ' : Bunch P
l✝ : BunchWithHole P
r✝ : Bunch P
l_ih✝ :
  ∀ {Γ' : BunchWithHole P},
    ↑l✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ l✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = l✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = l✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑(semiL l✝ r✝) φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiL l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiL l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiL l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

case semiR
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
r_ih✝ :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑(semiR l✝ r✝) φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' : Bunch P
Γ' : BunchWithHole P
h : ↑hole φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ hole.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = hole) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = hole ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
case hole => simp_all
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' : Bunch P
Γ' : BunchWithHole P
h : ↑hole φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ hole.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = hole) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = hole ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
simp_all
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑(semiR l✝ r✝) φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
simp at h
Proof state after:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : (l✝ ;ᵇ ↑r✝ φ) = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : (l✝ ;ᵇ ↑r✝ φ) = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
rw [eq_comm] at h
Proof state after:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑Γ' φ' = (l✝ ;ᵇ ↑r✝ φ)
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑Γ' φ' = (l✝ ;ᵇ ↑r✝ φ)
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
first | rw [eq_comma] at h | rw [eq_semi] at h
Proof state after:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h :
  Γ' = hole ∧ φ' = (l✝ ;ᵇ ↑r✝ φ) ∨
    (∃ Γ'_1, Γ' = semiL Γ'_1 (↑r✝ φ) ∧ ↑Γ'_1 φ' = l✝) ∨ ∃ Γ'_1, Γ' = semiR l✝ Γ'_1 ∧ ↑Γ'_1 φ' = ↑r✝ φ
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h :
  Γ' = hole ∧ φ' = (l✝ ;ᵇ ↑r✝ φ) ∨
    (∃ Γ'_1, Γ' = semiL Γ'_1 (↑r✝ φ) ∧ ↑Γ'_1 φ' = l✝) ∨ ∃ Γ'_1, Γ' = semiR l✝ Γ'_1 ∧ ↑Γ'_1 φ' = ↑r✝ φ
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
rcases h with (⟨rfl,rfl⟩|⟨Γ'',rfl,h⟩|⟨Γ'',rfl,h⟩)
Proof state after:
case inl.intro
P : Sort u_1
φ l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' (l✝ ;ᵇ ↑r✝ φ) →
      (∃ Δ, φ = ↑Δ (l✝ ;ᵇ ↑r✝ φ) ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, (l✝ ;ᵇ ↑r✝ φ) = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨
          ∃ Δ Δ', Δ φ = Γ' ∧ Δ' (l✝ ;ᵇ ↑r✝ φ) = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ (∃ Δ, φ = ↑Δ (l✝ ;ᵇ ↑r✝ φ) ∧ (semiR l✝ r✝).comp Δ = hole) ∨
    (∃ Δ, (l✝ ;ᵇ ↑r✝ φ) = ↑Δ φ ∧ hole.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = hole ∧ Δ' (l✝ ;ᵇ ↑r✝ φ) = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

case inr.inl.intro.intro
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
h : ↑Γ'' φ' = l✝
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = semiL Γ'' (↑r✝ φ)) ∨
    (∃ Δ, φ' = ↑Δ φ ∧ (semiL Γ'' (↑r✝ φ)).comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = semiL Γ'' (↑r✝ φ) ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

case inr.inr.intro.intro
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
h : ↑Γ'' φ' = ↑r✝ φ
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = semiR l✝ Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ (semiR l✝ Γ'').comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = semiR l✝ Γ'' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑Γ' φ' = (l✝ ,ᵇ ↑r✝ φ)
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (commaR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = commaR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = commaR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
rw [eq_comma] at h
Proof state after:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h :
  Γ' = hole ∧ φ' = (l✝ ,ᵇ ↑r✝ φ) ∨
    (∃ Γ'_1, Γ' = commaL Γ'_1 (↑r✝ φ) ∧ ↑Γ'_1 φ' = l✝) ∨ ∃ Γ'_1, Γ' = commaR l✝ Γ'_1 ∧ ↑Γ'_1 φ' = ↑r✝ φ
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (commaR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = commaR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = commaR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h : ↑Γ' φ' = (l✝ ;ᵇ ↑r✝ φ)
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
rw [eq_semi] at h
Proof state after:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ' : BunchWithHole P
h :
  Γ' = hole ∧ φ' = (l✝ ;ᵇ ↑r✝ φ) ∨
    (∃ Γ'_1, Γ' = semiL Γ'_1 (↑r✝ φ) ∧ ↑Γ'_1 φ' = l✝) ∨ ∃ Γ'_1, Γ' = semiR l✝ Γ'_1 ∧ ↑Γ'_1 φ' = ↑r✝ φ
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
case inl.intro
P : Sort u_1
φ l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' (l✝ ;ᵇ ↑r✝ φ) →
      (∃ Δ, φ = ↑Δ (l✝ ;ᵇ ↑r✝ φ) ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, (l✝ ;ᵇ ↑r✝ φ) = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨
          ∃ Δ Δ', Δ φ = Γ' ∧ Δ' (l✝ ;ᵇ ↑r✝ φ) = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ (∃ Δ, φ = ↑Δ (l✝ ;ᵇ ↑r✝ φ) ∧ (semiR l✝ r✝).comp Δ = hole) ∨
    (∃ Δ, (l✝ ;ᵇ ↑r✝ φ) = ↑Δ φ ∧ hole.comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = hole ∧ Δ' (l✝ ;ᵇ ↑r✝ φ) = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
simp
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
h : ↑Γ'' φ' = ↑r✝ φ
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = semiR l✝ Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ (semiR l✝ Γ'').comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = semiR l✝ Γ'' ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
simp
Proof state after:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
h : ↑Γ'' φ' = ↑r✝ φ
⊢ (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝) ∨
      ∃ Δ, Δ φ = semiR l✝ Γ'' ∧ ∃ x, x φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
h : ↑Γ'' φ' = ↑r✝ φ
⊢ (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝) ∨
      ∃ Δ, Δ φ = semiR l✝ Γ'' ∧ ∃ x, x φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ
Tactic:
rw [eq_comm] at h
Proof state after:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
h : ↑r✝ φ = ↑Γ'' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝) ∨
      ∃ Δ, Δ φ = semiR l✝ Γ'' ∧ ∃ x, x φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
h : ↑r✝ φ = ↑Γ'' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝) ∨
      ∃ Δ, Δ φ = semiR l✝ Γ'' ∧ ∃ x, x φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ
Tactic:
rcases ih h with (h1|h2|⟨Δ,Δ',rfl,rfl,h3⟩)
  <;> clear ih h
Proof state after:
case inl
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ Γ'' : BunchWithHole P
h1 : ∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ''
⊢ (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝) ∨
      ∃ Δ, Δ φ = semiR l✝ Γ'' ∧ ∃ x, x φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ

case inr.inl
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ Γ'' : BunchWithHole P
h2 : ∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝
⊢ (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝) ∨
      ∃ Δ, Δ φ = semiR l✝ Γ'' ∧ ∃ x, x φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ

case inr.inr.intro.intro.intro.intro
P : Sort u_1
φ φ' l✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ (∃ Δ_1, φ = ↑Δ_1 φ' ∧ (Δ' φ').comp Δ_1 = Δ φ) ∨
    (∃ Δ_1, φ' = ↑Δ_1 φ ∧ (Δ φ).comp Δ_1 = Δ' φ') ∨
      ∃ Δ_1, Δ_1 φ = semiR l✝ (Δ φ) ∧ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ_1 ψ) ψ' = ↑(x ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
case inl
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ Γ'' : BunchWithHole P
h1 : ∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ''
⊢ (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝) ∨
      ∃ Δ, Δ φ = semiR l✝ Γ'' ∧ ∃ x, x φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ
Tactic:
simp [h1]
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
case inr.inl
P : Sort u_1
φ φ' l✝ : Bunch P
r✝ Γ'' : BunchWithHole P
h2 : ∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝
⊢ (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ'') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ''.comp Δ = r✝) ∨
      ∃ Δ, Δ φ = semiR l✝ Γ'' ∧ ∃ x, x φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ
Tactic:
simp [h2]
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
case inr.inr.intro.intro.intro.intro
P : Sort u_1
φ φ' l✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ (∃ Δ_1, φ = ↑Δ_1 φ' ∧ (Δ' φ').comp Δ_1 = Δ φ) ∨
    (∃ Δ_1, φ' = ↑Δ_1 φ ∧ (Δ φ).comp Δ_1 = Δ' φ') ∨
      ∃ Δ_1, Δ_1 φ = semiR l✝ (Δ φ) ∧ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ_1 ψ) ψ' = ↑(x ψ') ψ
Tactic:
apply Or.inr
Proof state after:
case inr.inr.intro.intro.intro.intro.h
P : Sort u_1
φ φ' l✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ (∃ Δ_1, φ' = ↑Δ_1 φ ∧ (Δ φ).comp Δ_1 = Δ' φ') ∨
    ∃ Δ_1, Δ_1 φ = semiR l✝ (Δ φ) ∧ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ_1 ψ) ψ' = ↑(x ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
case inr.inr.intro.intro.intro.intro.h
P : Sort u_1
φ φ' l✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ (∃ Δ_1, φ' = ↑Δ_1 φ ∧ (Δ φ).comp Δ_1 = Δ' φ') ∨
    ∃ Δ_1, Δ_1 φ = semiR l✝ (Δ φ) ∧ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ_1 ψ) ψ' = ↑(x ψ') ψ
Tactic:
apply Or.inr
Proof state after:
case inr.inr.intro.intro.intro.intro.h.h
P : Sort u_1
φ φ' l✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ Δ_1, Δ_1 φ = semiR l✝ (Δ φ) ∧ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ_1 ψ) ψ' = ↑(x ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof state before:
case inr.inr.intro.intro.intro.intro.h.h
P : Sort u_1
φ φ' l✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ Δ_1, Δ_1 φ = semiR l✝ (Δ φ) ∧ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ_1 ψ) ψ' = ↑(x ψ') ψ
Tactic:
iterate 2 (
  first | refine ⟨(fun x => commaL _ _),rfl,?_⟩
        | refine ⟨(fun x => commaR _ _),rfl,?_⟩
        | refine ⟨(fun x => semiL _ _),rfl,?_⟩
        | refine ⟨(fun x => semiR _ _),rfl,?_⟩
)
Proof state after:
case inr.inr.intro.intro.intro.intro.h.h
P : Sort u_1
φ φ' l✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑((fun x => semiR l✝ (Δ' x)) ψ') ψ