internlm/Lean-Github huggingface dataset:
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
case mpr
P✝ : Sort u_1
B : Bunch P✝
A : Typ P✝
⊢ B = (cunit ,ᵇ prop A) ∨ B = (prop A ,ᵇ cunit) ∨ B = (sunit ;ᵇ prop A) ∨ B = (prop A ;ᵇ sunit) → PreEquiv B (prop A)
Tactic:
rintro (rfl|rfl|rfl|rfl)
Proof state after:
case mpr.inl
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (cunit ,ᵇ prop A) (prop A)

case mpr.inr.inl
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (prop A ,ᵇ cunit) (prop A)

case mpr.inr.inr.inl
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (sunit ;ᵇ prop A) (prop A)

case mpr.inr.inr.inr
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (prop A ;ᵇ sunit) (prop A)
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
case mpr.inl
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (cunit ,ᵇ prop A) (prop A)
Tactic:
exact cunitL
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
case mpr.inr.inl
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (prop A ,ᵇ cunit) (prop A)
Tactic:
exact cunitR
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
case mpr.inr.inr.inl
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (sunit ;ᵇ prop A) (prop A)
Tactic:
exact sunitL
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.prop_right
Proof state before:
case mpr.inr.inr.inr
P✝ : Sort u_1
A : Typ P✝
⊢ PreEquiv (prop A ;ᵇ sunit) (prop A)
Tactic:
exact sunitR
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B sunit ↔ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)
Tactic:
constructor
Proof state after:
case mp
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B sunit → B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)

case mpr
P✝ : Sort u_1
B : Bunch P✝
⊢ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit) → PreEquiv B sunit
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
case mp
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B sunit → B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)
Tactic:
intro h
Proof state after:
case mp
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv B sunit
⊢ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
case mp
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv B sunit
⊢ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit)
Tactic:
generalize hA' : sunit = A' at h
Proof state after:
case mp
P✝ : Sort u_1
B A' : Bunch P✝
hA' : sunit = A'
h : PreEquiv B A'
⊢ B = (cunit ,ᵇ A') ∨ B = (A' ,ᵇ cunit) ∨ B = (A' ;ᵇ A') ∨ B = (A' ;ᵇ A')
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
case mp
P✝ : Sort u_1
B A' : Bunch P✝
hA' : sunit = A'
h : PreEquiv B A'
⊢ B = (cunit ,ᵇ A') ∨ B = (A' ,ᵇ cunit) ∨ B = (A' ;ᵇ A') ∨ B = (A' ;ᵇ A')
Tactic:
induction h <;> simp_all
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
case mpr
P✝ : Sort u_1
B : Bunch P✝
⊢ B = (cunit ,ᵇ sunit) ∨ B = (sunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ sunit) ∨ B = (sunit ;ᵇ sunit) → PreEquiv B sunit
Tactic:
rintro (rfl|rfl|rfl|rfl)
Proof state after:
case mpr.inl
P✝ : Sort u_1
⊢ PreEquiv (cunit ,ᵇ sunit) sunit

case mpr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ,ᵇ cunit) sunit

case mpr.inr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ sunit) sunit

case mpr.inr.inr.inr
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ sunit) sunit
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
case mpr.inl
P✝ : Sort u_1
⊢ PreEquiv (cunit ,ᵇ sunit) sunit
Tactic:
exact cunitL
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
case mpr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ,ᵇ cunit) sunit
Tactic:
exact cunitR
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
case mpr.inr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ sunit) sunit
Tactic:
exact sunitL
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.sunit_right
Proof state before:
case mpr.inr.inr.inr
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ sunit) sunit
Tactic:
exact sunitR
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B cunit ↔ B = (cunit ,ᵇ cunit) ∨ B = (cunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ cunit) ∨ B = (cunit ;ᵇ sunit)
Tactic:
constructor
Proof state after:
case mp
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B cunit → B = (cunit ,ᵇ cunit) ∨ B = (cunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ cunit) ∨ B = (cunit ;ᵇ sunit)

case mpr
P✝ : Sort u_1
B : Bunch P✝
⊢ B = (cunit ,ᵇ cunit) ∨ B = (cunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ cunit) ∨ B = (cunit ;ᵇ sunit) → PreEquiv B cunit
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
case mp
P✝ : Sort u_1
B : Bunch P✝
⊢ PreEquiv B cunit → B = (cunit ,ᵇ cunit) ∨ B = (cunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ cunit) ∨ B = (cunit ;ᵇ sunit)
Tactic:
intro h
Proof state after:
case mp
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv B cunit
⊢ B = (cunit ,ᵇ cunit) ∨ B = (cunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ cunit) ∨ B = (cunit ;ᵇ sunit)
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
case mp
P✝ : Sort u_1
B : Bunch P✝
h : PreEquiv B cunit
⊢ B = (cunit ,ᵇ cunit) ∨ B = (cunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ cunit) ∨ B = (cunit ;ᵇ sunit)
Tactic:
generalize hA' : cunit = A' at h
Proof state after:
case mp
P✝ : Sort u_1
B A' : Bunch P✝
hA' : cunit = A'
h : PreEquiv B A'
⊢ B = (A' ,ᵇ A') ∨ B = (A' ,ᵇ A') ∨ B = (sunit ;ᵇ A') ∨ B = (A' ;ᵇ sunit)
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
case mp
P✝ : Sort u_1
B A' : Bunch P✝
hA' : cunit = A'
h : PreEquiv B A'
⊢ B = (A' ,ᵇ A') ∨ B = (A' ,ᵇ A') ∨ B = (sunit ;ᵇ A') ∨ B = (A' ;ᵇ sunit)
Tactic:
induction h <;> simp_all
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
case mpr
P✝ : Sort u_1
B : Bunch P✝
⊢ B = (cunit ,ᵇ cunit) ∨ B = (cunit ,ᵇ cunit) ∨ B = (sunit ;ᵇ cunit) ∨ B = (cunit ;ᵇ sunit) → PreEquiv B cunit
Tactic:
rintro (rfl|rfl|rfl|rfl)
Proof state after:
case mpr.inl
P✝ : Sort u_1
⊢ PreEquiv (cunit ,ᵇ cunit) cunit

case mpr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (cunit ,ᵇ cunit) cunit

case mpr.inr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ cunit) cunit

case mpr.inr.inr.inr
P✝ : Sort u_1
⊢ PreEquiv (cunit ;ᵇ sunit) cunit
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
case mpr.inl
P✝ : Sort u_1
⊢ PreEquiv (cunit ,ᵇ cunit) cunit
Tactic:
exact cunitL
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
case mpr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (cunit ,ᵇ cunit) cunit
Tactic:
exact cunitR
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
case mpr.inr.inr.inl
P✝ : Sort u_1
⊢ PreEquiv (sunit ;ᵇ cunit) cunit
Tactic:
exact sunitL
Proof state after:
no goals
Theorem: BunchImpl.PreEquiv.cunit_right
Proof state before:
case mpr.inr.inr.inr
P✝ : Sort u_1
⊢ PreEquiv (cunit ;ᵇ sunit) cunit
Tactic:
exact sunitR
Proof state after:
no goals
Theorem: BunchImpl.Equiv.subbunch
Proof state before:
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
⊢ b1 ≈ b2 → ↑h b1 ≈ ↑h b2
Tactic:
intro e
Proof state after:
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
e : b1 ≈ b2
⊢ ↑h b1 ≈ ↑h b2
Theorem: BunchImpl.Equiv.subbunch
Proof state before:
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
e : b1 ≈ b2
⊢ ↑h b1 ≈ ↑h b2
Tactic:
induction e with
| rel _ _ h =>
  apply EqvGen.rel
  apply PreEquiv.subbunch
  exact h
| refl =>
  exact refl
| symm _ _ _ ih =>
  exact symm ih
| trans _ _ _ _ _ ih1 ih2 =>
  exact trans ih1 ih2
Proof state after:
no goals
Theorem: BunchImpl.Equiv.subbunch
Proof state before:
case rel
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ ↑h✝ x✝ ≈ ↑h✝ y✝
Tactic:
apply EqvGen.rel
Proof state after:
case rel.a
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ PreEquiv (↑h✝ x✝) (↑h✝ y✝)
Theorem: BunchImpl.Equiv.subbunch
Proof state before:
case rel.a
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ PreEquiv (↑h✝ x✝) (↑h✝ y✝)
Tactic:
apply PreEquiv.subbunch
Proof state after:
case rel.a.a
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ PreEquiv x✝ y✝
Theorem: BunchImpl.Equiv.subbunch
Proof state before:
case rel.a.a
P : Type u_1
b1 b2 : Bunch P
h✝ : BunchWithHole P
x✝ y✝ : Bunch P
h : PreEquiv x✝ y✝
⊢ PreEquiv x✝ y✝
Tactic:
exact h
Proof state after:
no goals
Theorem: BunchImpl.Equiv.subbunch
Proof state before:
case refl
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
x✝ : Bunch P
⊢ ↑h x✝ ≈ ↑h x✝
Tactic:
exact refl
Proof state after:
no goals
Theorem: BunchImpl.Equiv.subbunch
Proof state before:
case symm
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
x✝ y✝ : Bunch P
a✝ : EqvGen PreEquiv x✝ y✝
ih : ↑h x✝ ≈ ↑h y✝
⊢ ↑h y✝ ≈ ↑h x✝
Tactic:
exact symm ih
Proof state after:
no goals
Theorem: BunchImpl.Equiv.subbunch
Proof state before:
case trans
P : Type u_1
b1 b2 : Bunch P
h : BunchWithHole P
x✝ y✝ z✝ : Bunch P
a✝¹ : EqvGen PreEquiv x✝ y✝
a✝ : EqvGen PreEquiv y✝ z✝
ih1 : ↑h x✝ ≈ ↑h y✝
ih2 : ↑h y✝ ≈ ↑h z✝
⊢ ↑h x✝ ≈ ↑h z✝
Tactic:
exact trans ih1 ih2
Proof state after:
no goals
Theorem: BunchImpl.Equiv.hole_prop_inv
Proof state before:
P : Type u_1
Γ : BunchWithHole P
A : Typ P
Δ : Bunch P
⊢ ↑Γ (prop A) ≈ Δ → ∃ Γ', Δ = ↑Γ' (prop A)
Tactic:
intro e
Proof state after:
P : Type u_1
Γ : BunchWithHole P
A : Typ P
Δ : Bunch P
e : ↑Γ (prop A) ≈ Δ
⊢ ∃ Γ', Δ = ↑Γ' (prop A)
Theorem: BunchImpl.Equiv.hole_prop_inv
Proof state before:
P : Type u_1
Γ : BunchWithHole P
A : Typ P
Δ : Bunch P
e : ↑Γ (prop A) ≈ Δ
⊢ ∃ Γ', Δ = ↑Γ' (prop A)
Tactic:
induction Δ
Proof state after:
case prop
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ ∃ Γ', prop a✝ = ↑Γ' (prop A)

case cunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ cunit
⊢ ∃ Γ', cunit = ↑Γ' (prop A)

case comma
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ,ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ,ᵇ a✝) = ↑Γ' (prop A)

case sunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ sunit
⊢ ∃ Γ', sunit = ↑Γ' (prop A)

case semi
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ;ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ;ᵇ a✝) = ↑Γ' (prop A)
Theorem: BunchImpl.Equiv.hole_prop_inv
Proof state before:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ ∃ Γ', prop a✝ = ↑Γ' (prop A)
Tactic:
case prop =>
  simp at e
  refine ⟨.hole,?_⟩; simp
Proof state after:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ a✝ = A
Theorem: BunchImpl.Equiv.hole_prop_inv
Proof state before:
case cunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ cunit
⊢ ∃ Γ', cunit = ↑Γ' (prop A)

case comma
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ,ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ,ᵇ a✝) = ↑Γ' (prop A)

case sunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ sunit
⊢ ∃ Γ', sunit = ↑Γ' (prop A)

case semi
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ;ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ;ᵇ a✝) = ↑Γ' (prop A)
Tactic:
sorry
Proof state after:
case comma
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ,ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ,ᵇ a✝) = ↑Γ' (prop A)

case sunit
P : Type u_1
Γ : BunchWithHole P
A : Typ P
e : ↑Γ (prop A) ≈ sunit
⊢ ∃ Γ', sunit = ↑Γ' (prop A)

case semi
P : Type u_1
Γ : BunchWithHole P
A : Typ P
a✝¹ a✝ : Bunch P
a_ih✝¹ : ↑Γ (prop A) ≈ a✝¹ → ∃ Γ', a✝¹ = ↑Γ' (prop A)
a_ih✝ : ↑Γ (prop A) ≈ a✝ → ∃ Γ', a✝ = ↑Γ' (prop A)
e : ↑Γ (prop A) ≈ (a✝¹ ;ᵇ a✝)
⊢ ∃ Γ', (a✝¹ ;ᵇ a✝) = ↑Γ' (prop A)
Theorem: BunchImpl.Equiv.hole_prop_inv
Proof state before:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ ∃ Γ', prop a✝ = ↑Γ' (prop A)
Tactic:
refine ⟨.hole,?_⟩
Proof state after:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ prop a✝ = ↑BunchWithHole.hole (prop A)
Theorem: BunchImpl.Equiv.hole_prop_inv
Proof state before:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ prop a✝ = ↑BunchWithHole.hole (prop A)
Tactic:
simp
Proof state after:
P : Type u_1
Γ : BunchWithHole P
A a✝ : Typ P
e : ↑Γ (prop A) ≈ prop a✝
⊢ a✝ = A
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ (l1 ,ᵇ r1) = (l2 ,ᵇ r2) ↔ l1 = l2 ∧ r1 = r2
Tactic:
constructor
Proof state after:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ (l1 ,ᵇ r1) = (l2 ,ᵇ r2) → l1 = l2 ∧ r1 = r2

case mpr
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ l1 = l2 ∧ r1 = r2 → (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ (l1 ,ᵇ r1) = (l2 ,ᵇ r2) → l1 = l2 ∧ r1 = r2
Tactic:
intro h
Proof state after:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
⊢ l1 = l2 ∧ r1 = r2
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
⊢ l1 = l2 ∧ r1 = r2
Tactic:
constructor <;> (funext V; have := congrFun h V; simp at this; simp [*])
Proof state after:
no goals
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
case mp.right
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
⊢ r1 = r2
Tactic:
funext V
Proof state after:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
V : Sort u_1
⊢ r1 V = r2 V
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
V : Sort u_1
⊢ r1 V = r2 V
Tactic:
have := congrFun h V
Proof state after:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
V : Sort u_1
this : (l1 ,ᵇ r1) V = (l2 ,ᵇ r2) V
⊢ r1 V = r2 V
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
V : Sort u_1
this : (l1 ,ᵇ r1) V = (l2 ,ᵇ r2) V
⊢ r1 V = r2 V
Tactic:
simp at this
Proof state after:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
V : Sort u_1
this : l1 V = l2 V ∧ r1 V = r2 V
⊢ r1 V = r2 V
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
V : Sort u_1
this : l1 V = l2 V ∧ r1 V = r2 V
⊢ r1 V = r2 V
Tactic:
simp [*]
Proof state after:
no goals
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
case mpr
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ l1 = l2 ∧ r1 = r2 → (l1 ,ᵇ r1) = (l2 ,ᵇ r2)
Tactic:
rintro ⟨rfl,rfl⟩
Proof state after:
case mpr.intro
P✝ : Sort u_1
l1 r1 : Bunch P✝
⊢ (l1 ,ᵇ r1) = (l1 ,ᵇ r1)
Theorem: BunchImpl.Bunch.comma_eq_comma
Proof state before:
case mpr.intro
P✝ : Sort u_1
l1 r1 : Bunch P✝
⊢ (l1 ,ᵇ r1) = (l1 ,ᵇ r1)
Tactic:
rfl
Proof state after:
no goals
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ (l1 ;ᵇ r1) = (l2 ;ᵇ r2) ↔ l1 = l2 ∧ r1 = r2
Tactic:
constructor
Proof state after:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ (l1 ;ᵇ r1) = (l2 ;ᵇ r2) → l1 = l2 ∧ r1 = r2

case mpr
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ l1 = l2 ∧ r1 = r2 → (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ (l1 ;ᵇ r1) = (l2 ;ᵇ r2) → l1 = l2 ∧ r1 = r2
Tactic:
intro h
Proof state after:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
⊢ l1 = l2 ∧ r1 = r2
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
⊢ l1 = l2 ∧ r1 = r2
Tactic:
constructor <;> (funext V; have := congrFun h V; simp at this; simp [*])
Proof state after:
no goals
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
case mp.right
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
⊢ r1 = r2
Tactic:
funext V
Proof state after:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
V : Sort u_1
⊢ r1 V = r2 V
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
V : Sort u_1
⊢ r1 V = r2 V
Tactic:
have := congrFun h V
Proof state after:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
V : Sort u_1
this : (l1 ;ᵇ r1) V = (l2 ;ᵇ r2) V
⊢ r1 V = r2 V
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
V : Sort u_1
this : (l1 ;ᵇ r1) V = (l2 ;ᵇ r2) V
⊢ r1 V = r2 V
Tactic:
simp at this
Proof state after:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
V : Sort u_1
this : l1 V = l2 V ∧ r1 V = r2 V
⊢ r1 V = r2 V
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
case mp.right.h
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
V : Sort u_1
this : l1 V = l2 V ∧ r1 V = r2 V
⊢ r1 V = r2 V
Tactic:
simp [*]
Proof state after:
no goals
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
case mpr
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ l1 = l2 ∧ r1 = r2 → (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
Tactic:
rintro ⟨rfl,rfl⟩
Proof state after:
case mpr.intro
P✝ : Sort u_1
l1 r1 : Bunch P✝
⊢ (l1 ;ᵇ r1) = (l1 ;ᵇ r1)
Theorem: BunchImpl.Bunch.semi_eq_semi
Proof state before:
case mpr.intro
P✝ : Sort u_1
l1 r1 : Bunch P✝
⊢ (l1 ;ᵇ r1) = (l1 ;ᵇ r1)
Tactic:
rfl
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P : Sort u
b1 b2 : Bunch P
⊢ (b1 ,ᵇ b2) ≠ b1
Tactic:
intro h
Proof state after:
P : Sort u
b1 b2 : Bunch P
h : (b1 ,ᵇ b2) = b1
⊢ False
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P : Sort u
b1 b2 : Bunch P
h : (b1 ,ᵇ b2) = b1
⊢ False
Tactic:
have := congrArg sizeOf h
Proof state after:
P : Sort u
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
b1 b2 : Bunch P
h : (b1 ,ᵇ b2) = b1
this : sizeOf (b1 ,ᵇ b2) = sizeOf b1
⊢ False
Tactic:
clear h
Proof state after:
P : Sort u
b1 b2 : Bunch P
this : sizeOf (b1 ,ᵇ b2) = sizeOf b1
⊢ False
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P : Sort u
b1 b2 : Bunch P
this : sizeOf (b1 ,ᵇ b2) = sizeOf b1
⊢ False
Tactic:
simp [instSizeOfBunch, comma] at this
Proof state after:
P : Sort u
b1 b2 : Bunch P
this : 1 + sizeOf (b1 PUnit.{u}) + sizeOf (b2 PUnit.{u}) = sizeOf (b1 PUnit.{u})
⊢ False
Theorem: BunchImpl.Bunch.neq_left_comma
Proof state before:
P : Sort u
b1 b2 : Bunch P
this : 1 + sizeOf (b1 PUnit.{u}) + sizeOf (b2 PUnit.{u}) = sizeOf (b1 PUnit.{u})
⊢ 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✝
⊢ (b1 ,ᵇ b2) ≠ b2
Tactic:
intro h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ,ᵇ b2) = b2
⊢ False
Theorem: BunchImpl.Bunch.neq_right_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ,ᵇ b2) = b2
⊢ False
Tactic:
have := congrArg sizeOf h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ,ᵇ b2) = b2
this : sizeOf (b1 ,ᵇ b2) = sizeOf b2
⊢ False
Theorem: BunchImpl.Bunch.neq_right_comma
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_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ,ᵇ b2) = sizeOf b2
⊢ False
Tactic:
simp [instSizeOfBunch, comma] 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✝
⊢ 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_comma
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_comma
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_comma
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf b1 = sizeOf (b1 ,ᵇ b2)
⊢ False
Tactic:
simp [instSizeOfBunch, comma] 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_comma
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_comma
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_comma
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_comma
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_comma
Proof state before:
P✝ : Sort u_1
b2 b1 : Bunch P✝
this : sizeOf b2 = sizeOf (b1 ,ᵇ b2)
⊢ False
Tactic:
simp [instSizeOfBunch, comma] at this
Proof state after:
no goals
Theorem: BunchImpl.Bunch.neq_left_semi
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_semi
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_semi
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_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : sizeOf (b1 ;ᵇ b2) = sizeOf b1
⊢ False
Tactic:
simp [instSizeOfBunch, semi] at this
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : 1 + sizeOf (b1 PUnit.{u_1}) + sizeOf (b2 PUnit.{u_1}) = sizeOf (b1 PUnit.{u_1})
⊢ False
Theorem: BunchImpl.Bunch.neq_left_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
this : 1 + sizeOf (b1 PUnit.{u_1}) + sizeOf (b2 PUnit.{u_1}) = sizeOf (b1 PUnit.{u_1})
⊢ 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✝
⊢ (b1 ;ᵇ b2) ≠ b2
Tactic:
intro h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ;ᵇ b2) = b2
⊢ False
Theorem: BunchImpl.Bunch.neq_right_semi
Proof state before:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ;ᵇ b2) = b2
⊢ False
Tactic:
have := congrArg sizeOf h
Proof state after:
P✝ : Sort u_1
b1 b2 : Bunch P✝
h : (b1 ;ᵇ b2) = b2
this : sizeOf (b1 ;ᵇ b2) = sizeOf b2
⊢ False