Theorem: LO.Propositional.Superintuitionistic.Formula.toW_ofW (Logic/Propositional/Superintuitionistic/Formula.lean)

State before:
α : Type u_1
a : α
f✝ : Edge α (Sum.inl a) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inl a) f✝)).toW = WType.mk (Sum.inl a) f✝
Tactic:
simp [ofW, toW, Empty.eq_elim]
State after:
no goals

State before:
α : Type u_1
f✝ : Edge α (Sum.inr (Sum.inl true)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inl true)) f✝)).toW = WType.mk (Sum.inr (Sum.inl true)) f✝
Tactic:
simp [ofW, toW, Empty.eq_elim]
State after:
no goals

State before:
α : Type u_1
f✝ : Edge α (Sum.inr (Sum.inl false)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inl false)) f✝)).toW = WType.mk (Sum.inr (Sum.inl false)) f✝
Tactic:
simp [ofW, toW, Empty.eq_elim]
State after:
no goals

State before:
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) w)).toW = WType.mk (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) w
Tactic:
simp [ofW, toW, toW_ofW (w false), toW_ofW (w true)]
State after:
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w

State before:
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
State after:
case h
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b

State before:
case h
α : Type u_1
isLt✝ : 0 < 3
w : Edge α (Sum.inr (Sum.inr ⟨0, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
State after:
no goals

State before:
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) w)).toW = WType.mk (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) w
Tactic:
simp [ofW, toW, toW_ofW (w false), toW_ofW (w true)]
State after:
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w

State before:
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
State after:
case h
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b

State before:
case h
α : Type u_1
isLt✝ : 1 < 3
w : Edge α (Sum.inr (Sum.inr ⟨1, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
State after:
no goals

State before:
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
⊢ (ofW (WType.mk (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) w)).toW = WType.mk (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) w
Tactic:
simp [ofW, toW, toW_ofW (w false), toW_ofW (w true)]
State after:
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w

State before:
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
⊢ (fun t => Bool.rec (w false) (w true) t) = w
Tactic:
ext b
State after:
case h
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b

State before:
case h
α : Type u_1
isLt✝ : 2 < 3
w : Edge α (Sum.inr (Sum.inr ⟨2, isLt✝⟩)) → WType (Edge α)
b : Bool
⊢ Bool.rec (w false) (w true) b = w b
Tactic:
cases b <;> simp
State after:
no goals