internlm/Lean-Github huggingface dataset:
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑((fun x => semiR l✝ (Δ' x)) ψ') ψ
Tactic:
intro ψ ψ'
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)) ψ') ψ
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
ψ ψ' : Bunch P
⊢ ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑((fun x => semiR l✝ (Δ' x)) ψ') ψ
Tactic:
simp [h3]
Proof state after:
no goals
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ 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,?_⟩
)
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)) ψ') ψ
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ 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,?_⟩
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)) ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
Proof 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✝) ψ') ψ
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ x, x φ' = commaR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => commaR l✝ (Δ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
refine ⟨(fun x => commaR _ _),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 => commaR l✝ (Δ x)) ψ) ψ' = ↑((fun x => commaR l✝ (Δ' x)) ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
Proof 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✝) ψ') ψ
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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
⊢ ∃ x, x φ' = semiR l✝ (Δ' φ') ∧ ∀ (ψ ψ' : Bunch P), ↑((fun x => semiR l✝ (Δ x)) ψ) ψ' = ↑(x ψ') ψ
Tactic:
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)) ψ') ψ
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✝
⊢ (∃ Δ, φ = ↑Δ φ' ∧ (semiR l✝ r✝).comp Δ = semiL Γ'' (↑r✝ φ)) ∨
    (∃ Δ, φ' = ↑Δ φ ∧ (semiL Γ'' (↑r✝ φ)).comp Δ = semiR l✝ r✝) ∨
      ∃ Δ Δ', Δ φ = semiL Γ'' (↑r✝ φ) ∧ Δ' φ' = semiR l✝ r✝ ∧ ∀ (ψ ψ' : Bunch P), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Tactic:
cases h
Proof 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), ↑(Δ ψ) ψ' = ↑(Δ' ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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
Proof 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 ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
)
Proof 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✝) ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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 ψ ψ'
Proof 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✝) ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
)
Proof 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✝) ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
Proof 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✝) ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
Proof 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 ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
Proof 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✝) ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
Proof 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 ψ') ψ
Theorem: BunchImpl.BunchWithHole.eq_inv
Proof 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,?_⟩
Proof 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✝) ψ') ψ
Theorem: BunchImpl.BunchWithHole.idem
Proof state before:
P : Sort u_1
Γ : BunchWithHole P
b : Bunch P
⊢ ↑Γ b = b ↔ Γ = hole
Tactic:
simp [FunLike.coe]
Proof state after:
no goals
Theorem: BunchImpl.BunchWithHole.idem'
Proof state before:
P : Sort u_1
Γ : BunchWithHole P
b : Bunch P
⊢ b = ↑Γ b ↔ Γ = hole
Tactic:
simp [FunLike.coe]
Proof state after:
no goals