liftMetaTactic code before video

MetaExamples/RewriteIneq.lean

@@ -98,3 +98,56 @@ example (x y z : Nat) (h₁ : x ≤ y) (h₂ : y ≤ z) : x ≤ z :=
 example (x y z : Nat) (h₁ : x ≤ y) (h₂ : y ≤ z) : x ≤ y :=
   by
     rw_le h₁
+
+#check MVarId.getType
+
+
+elab "rw_leq" t:term : tactic => do
+  let h ← elabTerm t none
+  liftMetaTactic fun goal =>
+  goal.withContext do
+    let hType ← inferType h
+    let target ← goal.getType
+    match ← matchLe hType, ← matchLe target with
+    | some (a, b), some (c, d) =>
+      let firstEq ← isDefEq a c
+      let secondEq ← isDefEq b d
+      if firstEq && secondEq then
+        goal.assign h
+        return []
+      else
+      if firstEq then
+        -- have `a = c`, so `h` is `c ≤ b` and we need `b ≤ d`
+        let newTarget ← mkAppM ``Nat.le #[b, d]
+        let newGoal ← mkFreshExprMVar newTarget
+        let proof ← mkAppM ``Nat.le_trans #[h, newGoal]
+        goal.assign proof
+        return [newGoal.mvarId!]
+      else
+      if secondEq then
+        -- have `b = d`, so `h` is `a ≤ d` and we need `c ≤ a`
+        let newTarget ← mkAppM ``Nat.le #[c, a]
+        let newGoal ← mkFreshExprMVar newTarget
+        let proof ← mkAppM ``Nat.le_trans #[newGoal, h]
+        goal.assign proof
+        return [newGoal.mvarId!]
+      else
+        throwError "Neither ends matched"
+    | _, _ =>
+      throwError "Did not get inequalities"
+
+
+example (x y z : Nat) (h₁ : x ≤ y) (h₂ : y ≤ z) : x ≤ z :=
+  by
+    rw_leq h₁
+    exact h₂
+
+example (x y z : Nat) (h₁ : x ≤ y) (h₂ : y ≤ z) : x ≤ z :=
+  by
+    rw_le h₂
+    exact h₁
+
+
+example (x y z : Nat) (h₁ : x ≤ y) (h₂ : y ≤ z) : x ≤ y :=
+  by
+    rw_leq h₁