Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case hi
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case hj
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case left_neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case right_neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

pp: case h
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
<;>

Goal state after:
case hi
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case hj
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case left_neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case right_neg
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

case h
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : Semiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a b : α
a✝ : a ≤ b
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)