Paper-Proof/paperproof

Parser.lean - parse tactic combinators

lakesare opened this issue · 1 comments

lakesare commented

Deal with backtracking tactic combinators issue

There is also a similar issue for repeat, can be checked for this proof. Again - can be fixed in the Converter, but better fixed in the Parser if possible.

import Mathlib.Tactic
import Mathlib.Data.Real.Basic

variable (a b c d : ℝ)

example : min a b = min b a := by
  apply le_antisymm
  repeat
    apply le_min
    apply min_le_right
    apply min_le_left
image
lakesare commented

Anton fixed this (by just taking the last subtree)

image