009.lean.leanInk.expected

[{"contents":
  [{"typeinfo":
    {"type": "∀ (p q r : Prop), p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r",
     "name": "example",
     "_type": "typeinfo"},
    "semanticType": "Keyword",
    "raw": "example",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " (",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "p", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "p",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "q", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "q",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "r", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "r",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " : ",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Type", "name": "Prop", "_type": "typeinfo"},
    "semanticType": null,
    "raw": "Prop",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": ") : ",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "p", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "p",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ∧ (",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "q", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "q",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ∨ ",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "r", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "r",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": ") ↔ (",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "p", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "p",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ∧ ",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "q", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "q",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": ") ∨ (",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "p", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "p",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ∧ ",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": {"type": "Prop", "name": "r", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "r",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": ") := ",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "text"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "by",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": "\n  ",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)",
     "name": "Iff.intro",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "Iff.intro",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n  ",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "intro",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ (q ∨ r)", "name": "h", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "h",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n    ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "q → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c",
     "name": "Or.elim",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "Or.elim",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " (",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a ∧ b → b",
     "name": "And.right",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.right",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ (q ∨ r)", "name": "h", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "h",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": ")",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n    ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "q → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "q → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "intro",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": {"type": "q", "name": "hq", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hq",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "q → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left.h",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p ∧ q",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a → a ∨ b",
     "name": "Or.inl",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "Or.inl",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "q → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left.h.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"},
   {"name": "mp.left.h.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a → b → a ∧ b",
     "name": "And.intro",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.intro",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "q → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left.h.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left.h.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"},
   {"name": "mp.left.h.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses": [],
    "conclusion": "Goals accomplished! 🐙",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "exact",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a ∧ b → a",
     "name": "And.left",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.left",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ (q ∨ r)", "name": "h", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "h",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "q → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left.h.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.left.h.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "q", "names": ["hq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses": [],
    "conclusion": "Goals accomplished! 🐙",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "exact",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": {"type": "q", "name": "hq", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hq",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) → p ∧ q ∨ p ∧ r",
    "_type": "goal"},
   {"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n    ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "intro",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": {"type": "r", "name": "hr", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hr",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right.h",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, b → a ∨ b",
     "name": "Or.inr",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "Or.inr",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right.h.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"},
   {"name": "mp.right.h.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a → b → a ∧ b",
     "name": "And.intro",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.intro",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right.h.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right.h.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"},
   {"name": "mp.right.h.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses": [],
    "conclusion": "Goals accomplished! 🐙",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "exact",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a ∧ b → a",
     "name": "And.left",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.left",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ (q ∨ r)", "name": "h", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "h",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "r → p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right.h.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mp.right.h.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ (q ∨ r)", "names": ["h"], "body": "", "_type": "hypothesis"},
     {"type": "r", "names": ["hr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses": [],
    "conclusion": "Goals accomplished! 🐙",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "exact",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": {"type": "r", "name": "hr", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hr",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r) ↔ p ∧ q ∨ p ∧ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n  ",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "intro",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ q ∨ p ∧ r", "name": "h", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "h",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n    ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q → p ∧ (q ∨ r)",
    "_type": "goal"},
   {"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c",
     "name": "Or.elim",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "Or.elim",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ q ∨ p ∧ r", "name": "h", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "h",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n    ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q → p ∧ (q ∨ r)",
    "_type": "goal"},
   {"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "intro",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ q", "name": "hpq", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hpq",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q → p ∧ (q ∨ r)",
    "_type": "goal"},
   {"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"},
   {"name": "mpr.left.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a → b → a ∧ b",
     "name": "And.intro",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.intro",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q → p ∧ (q ∨ r)",
    "_type": "goal"},
   {"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"},
   {"name": "mpr.left.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses": [],
    "conclusion": "Goals accomplished! 🐙",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "exact",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a ∧ b → a",
     "name": "And.left",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.left",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ q", "name": "hpq", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hpq",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q → p ∧ (q ∨ r)",
    "_type": "goal"},
   {"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left.right.h",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a → a ∨ b",
     "name": "Or.inl",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "Or.inl",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.left.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q", "names": ["hpq"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n        ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses": [],
    "conclusion": "Goals accomplished! 🐙",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "exact",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a ∧ b → b",
     "name": "And.right",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.right",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ q", "name": "hpq", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hpq",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ q ∨ p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n    ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "intro",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "Introduce one or more hypotheses, optionally naming and/or pattern-matching them.\nFor each hypothesis to be introduced, the remaining main goal's target type must be a `let` or function type.\n* `intro` by itself introduces one anonymous hypothesis, which can be accessed by e.g. `assumption`.\n* `intro x y` introduces two hypotheses and names them. Individual hypotheses can be anonymized via `_`,\n  or matched against a pattern:\n  ```lean\n  -- ... ⊢ α × β → ...\n  intro (a, b)\n  -- ..., a : α, b : β ⊢ ...\n  ```\n* Alternatively, `intro` can be combined with pattern matching much like `fun`:\n  ```lean\n  intro\n  | n + 1, 0 => tac\n  | ...\n  ```\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ r", "name": "hpr", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hpr",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"},
   {"name": "mpr.right.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a → b → a ∧ b",
     "name": "And.intro",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.intro",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right.left",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "p",
    "_type": "goal"},
   {"name": "mpr.right.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses": [],
    "conclusion": "Goals accomplished! 🐙",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "exact",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a ∧ b → a",
     "name": "And.left",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.left",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ r", "name": "hpr", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hpr",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"}],
    "conclusion": "p ∧ r → p ∧ (q ∨ r)",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n      ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": ".",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right.right.h",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "apply",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`apply e` tries to match the current goal against the conclusion of `e`'s type.\nIf it succeeds, then the tactic returns as many subgoals as the number of premises that\nhave not been fixed by type inference or type class resolution.\nNon-dependent premises are added before dependent ones.\n\nThe `apply` tactic uses higher-order pattern matching, type class resolution, and first-order unification with dependent types.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, b → a ∨ b",
     "name": "Or.inr",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "Or.inr",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "mpr.right.right",
    "hypotheses":
    [{"type": "Prop",
      "names": ["p", "q", "r"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ q ∨ p ∧ r",
      "names": ["h"],
      "body": "",
      "_type": "hypothesis"},
     {"type": "p ∧ r", "names": ["hpr"], "body": "", "_type": "hypothesis"}],
    "conclusion": "q ∨ r",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": null,
    "raw": "\n        ",
    "link": null,
    "docstring":
    "`· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. ",
    "_type": "token"}],
  "_type": "sentence"},
 {"messages": [],
  "goals":
  [{"name": "",
    "hypotheses": [],
    "conclusion": "Goals accomplished! 🐙",
    "_type": "goal"}],
  "contents":
  [{"typeinfo": null,
    "semanticType": "Keyword",
    "raw": "exact",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo":
    {"type": "∀ {a b : Prop}, a ∧ b → b",
     "name": "And.right",
     "_type": "typeinfo"},
    "semanticType": null,
    "raw": "And.right",
    "link": null,
    "docstring": null,
    "_type": "token"},
   {"typeinfo": null,
    "semanticType": null,
    "raw": " ",
    "link": null,
    "docstring":
    "`exact e` closes the main goal if its target type matches that of `e`.\n",
    "_type": "token"},
   {"typeinfo": {"type": "p ∧ r", "name": "hpr", "_type": "typeinfo"},
    "semanticType": "Name.Variable",
    "raw": "hpr",
    "link": null,
    "docstring": null,
    "_type": "token"}],
  "_type": "sentence"},
 {"contents": [], "_type": "text"}]