tests/lean/1027.lean - third_party/github.com/leanprover/lean4 - Git at Google


            
            example (h : x ≠ 0) : Unit := by

            
              simp_all

            
              trace_state

            
              sorry