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

State before:
P : Sort u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
⊢ ↑Γ φ = ↑Γ' φ' →
    (∃ Δ, φ = ↑Δ φ' ∧ Γ.comp Δ = Γ') ∨
      (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = Γ) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
intro h
State after:
P : Sort u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
h : ↑Γ φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ Γ.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = Γ) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

State before:
P : Sort u_1
Γ Γ' : BunchWithHole P
φ φ' : Bunch P
h : ↑Γ φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ Γ.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = Γ) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = Γ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
induction Γ generalizing Γ'
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

State before:
P : Sort u_1
φ φ' : Bunch P
Γ' : BunchWithHole P
h : ↑hole φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ hole.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = hole) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = hole ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
case hole => simp_all
State after:
no goals

State before:
P : Sort u_1
φ φ' : Bunch P
Γ' : BunchWithHole P
h : ↑hole φ = ↑Γ' φ'
⊢ (∃ Δ, φ = ↑Δ φ' ∧ hole.comp Δ = Γ') ∨
    (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = hole) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = hole ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
simp_all
State after:
no goals

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
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

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
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

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
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

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⟩)
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

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
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

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
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

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
State after:
no goals

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
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 ψ') ψ

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
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 ψ') ψ

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
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 ψ') ψ

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]
State after:
no goals

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]
State after:
no goals

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
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 ψ') ψ

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
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 ψ') ψ

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,?_⟩
)
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)) ψ') ψ

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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑((fun x => semiR l✝ (Δ' x)) ψ') ψ
Tactic:
intro ψ ψ'
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)) ψ') ψ

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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
ψ ψ' : Bunch P
⊢ ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑((fun x => semiR l✝ (Δ' x)) ψ') ψ
Tactic:
simp [h3]
State after:
no goals

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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
(
first | refine ⟨(fun x => commaL _ _),rfl,?_⟩
| refine ⟨(fun x => commaR _ _),rfl,?_⟩
| refine ⟨(fun x => semiL _ _),rfl,?_⟩
| refine ⟨(fun x => semiR _ _),rfl,?_⟩
)
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)) ψ') ψ

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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
first | refine ⟨(fun x => commaL _ _),rfl,?_⟩
      | refine ⟨(fun x => commaR _ _),rfl,?_⟩
      | refine ⟨(fun x => semiL _ _),rfl,?_⟩
      | refine ⟨(fun x => semiR _ _),rfl,?_⟩
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)) ψ') ψ

State before:
case inr.inr.intro.intro.intro.intro.h.h
P : Sort u_1
φ φ' r✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ x, x φ' = commaL (Δ' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => commaL (Δ x) r✝) ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => commaL _ _),rfl,?_⟩
State after:
case inr.inr.intro.intro.intro.intro.h.h
P : Sort u_1
φ φ' r✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => commaL (Δ x) r✝) ψ) ψ' = ↑((fun x => commaL (Δ' x) r✝) ψ') ψ

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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ x, x φ' = commaR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => commaR l✝ (Δ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => commaR _ _),rfl,?_⟩
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 => commaR l✝ (Δ x)) ψ) ψ' = ↑((fun x => commaR l✝ (Δ' x)) ψ') ψ

State before:
case inr.inr.intro.intro.intro.intro.h.h
P : Sort u_1
φ φ' r✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ x, x φ' = semiL (Δ' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL (Δ x) r✝) ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => semiL _ _),rfl,?_⟩
State after:
case inr.inr.intro.intro.intro.intro.h.h
P : Sort u_1
φ φ' r✝ : Bunch P
Δ Δ' : Bunch P → BunchWithHole P
h3 : ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL (Δ x) r✝) ψ) ψ' = ↑((fun x => semiL (Δ' x) r✝) ψ') ψ

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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => semiR _ _),rfl,?_⟩
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)) ψ') ψ

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✝
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = semiL Γ'' (↑r✝ φ)) ∨
    (∃ Δ, φ' = ↑Δ φ ∧ (semiL Γ'' (↑r✝ φ)).comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = semiL Γ'' (↑r✝ φ) ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
cases h
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR (↑Γ'' φ') r✝).comp Δ = semiL Γ'' (↑r✝ φ)) ∨
    (∃ Δ, φ' = ↑Δ φ ∧ (semiL Γ'' (↑r✝ φ)).comp Δ = semiR (↑Γ'' φ') r✝) ∨
      ∃ Δ Δ', Δ φ = semiL Γ'' (↑r✝ φ) ∧ Δ' φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR (↑Γ'' φ') r✝).comp Δ = semiL Γ'' (↑r✝ φ)) ∨
    (∃ Δ, φ' = ↑Δ φ ∧ (semiL Γ'' (↑r✝ φ)).comp Δ = semiR (↑Γ'' φ') r✝) ∨
      ∃ Δ Δ', Δ φ = semiL Γ'' (↑r✝ φ) ∧ Δ' φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
simp
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ Δ, Δ φ = semiL Γ'' (↑r✝ φ) ∧ ∃ x, x φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ Δ, Δ φ = semiL Γ'' (↑r✝ φ) ∧ ∃ x, x φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(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,?_⟩
)
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑((fun x => semiR (↑Γ'' x) r✝) ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑((fun x => semiR (↑Γ'' x) r✝) ψ') ψ
Tactic:
intro ψ ψ'
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
ψ ψ' : Bunch P
⊢ ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑((fun x => semiR (↑Γ'' x) r✝) ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
ψ ψ' : Bunch P
⊢ ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑((fun x => semiR (↑Γ'' x) r✝) ψ') ψ
Tactic:
simp
State after:
no goals

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ x, x φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
(
first | refine ⟨(fun x => commaL _ _),rfl,?_⟩
| refine ⟨(fun x => commaR _ _),rfl,?_⟩
| refine ⟨(fun x => semiL _ _),rfl,?_⟩
| refine ⟨(fun x => semiR _ _),rfl,?_⟩
)
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑((fun x => semiR (↑Γ'' x) r✝) ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ x, x φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
first | refine ⟨(fun x => commaL _ _),rfl,?_⟩
      | refine ⟨(fun x => commaR _ _),rfl,?_⟩
      | refine ⟨(fun x => semiL _ _),rfl,?_⟩
      | refine ⟨(fun x => semiR _ _),rfl,?_⟩
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑((fun x => semiR (↑Γ'' x) r✝) ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ Δ, Δ φ = commaL Γ'' (↑r✝ φ) ∧ ∃ x, x φ' = commaR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => commaL _ _),rfl,?_⟩
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ x, x φ' = commaR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => commaL Γ'' (↑r✝ x)) ψ) ψ' = ↑(x ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ x, x φ' = commaR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => commaL Γ'' (↑r✝ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => commaR _ _),rfl,?_⟩
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => commaL Γ'' (↑r✝ x)) ψ) ψ' = ↑((fun x => commaR (↑Γ'' x) r✝) ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ Δ, Δ φ = semiL Γ'' (↑r✝ φ) ∧ ∃ x, x φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => semiL _ _),rfl,?_⟩
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ x, x φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑(x ψ') ψ

State before:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∃ x, x φ' = semiR (↑Γ'' φ') r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => semiR _ _),rfl,?_⟩
State after:
case refl
P : Sort u_1
φ φ' : Bunch P
r✝ : BunchWithHole P
ih :
  ∀ {Γ' : BunchWithHole P},
    ↑r✝ φ = ↑Γ' φ' →
      (∃ Δ, φ = ↑Δ φ' ∧ r✝.comp Δ = Γ') ∨
        (∃ Δ, φ' = ↑Δ φ ∧ Γ'.comp Δ = r✝) ∨ ∃ Δ Δ', Δ φ = Γ' ∧ Δ' φ' = r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Γ'' : BunchWithHole P
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiL Γ'' (↑r✝ x)) ψ) ψ' = ↑((fun x => semiR (↑Γ'' x) r✝) ψ') ψ