Theorem: BunchImpl.Bunch.semi_eq_semi (BunchImpl/Term/Bunch.lean)

State before:
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
⊢ (l1 ;ᵇ r1) = (l2 ;ᵇ r2) ↔ l1 = l2 ∧ r1 = r2
Tactic:
constructor
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)

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
State after:
case mp
P✝ : Sort u_1
l1 r1 l2 r2 : Bunch P✝
h : (l1 ;ᵇ r1) = (l2 ;ᵇ r2)
⊢ l1 = l2 ∧ r1 = r2

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

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
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

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
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

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
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

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

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⟩
State after:
case mpr.intro
P✝ : Sort u_1
l1 r1 : Bunch P✝
⊢ (l1 ;ᵇ r1) = (l1 ;ᵇ r1)

State before:
case mpr.intro
P✝ : Sort u_1
l1 r1 : Bunch P✝
⊢ (l1 ;ᵇ r1) = (l1 ;ᵇ r1)
Tactic:
rfl
State after:
no goals