From 27663315e6fda6c11aa321685b75bdcb12046558 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Fri, 29 Mar 2024 09:26:42 -0400
Subject: [PATCH] ...

---
 SciLean/Data/ArrayType/Notation.lean | 58 ++++++++++++++--------------
 SciLean/Tactic/DeduceBy.lean         |  5 +++
 2 files changed, 34 insertions(+), 29 deletions(-)

diff --git a/SciLean/Data/ArrayType/Notation.lean b/SciLean/Data/ArrayType/Notation.lean
index e4050bef..fd71212d 100644
--- a/SciLean/Data/ArrayType/Notation.lean
+++ b/SciLean/Data/ArrayType/Notation.lean
@@ -91,35 +91,35 @@ def unexpandArrayToArrayType : Lean.PrettyPrinter.Unexpander
 
 namespace ArrayType.PowerNotation
 
-class SHPow {α : Sort u} {β : Sort v} {γ : outParam (Sort w)} (a :α) (b : β) (c : outParam γ)
-def SHPow.pow {α β γ} (a : α) (b : β) {c : γ} [SHPow a b c] := c
-
-instance {Cont Idx Elem} [ArrayTypeNotation Cont Idx Elem] : SHPow Elem Idx (arrayTypeCont Idx Elem)  := ⟨⟩
-instance {α β γ} (x : α) (y : β) [HPow α β γ] : SHPow x y (HPow.hPow x y):= ⟨⟩
-open Lean Elab Term Meta in
-elab:40 (priority:=high) x:term:41 " ^ " y:term:42 : term => withFreshMacroScope do
-  let x ← elabTerm (← `(SHPow.pow $x $y)) none
-  return x.getArg! 5
-
-/- #check K ^ (κ×ι)
-#eval 2 ^ 3
-
- -/
-
-/- open Lean Elab Term in
-elab:40 (priority:=high) x:term:41 " ^ " y:term:42 : term =>
-  try
-    let y ← elabTerm y none
-    let x ← elabTerm x none
-    let z ← Meta.mkAppOptM ``arrayTypeCont #[y,x,none,none]
-    return z
-  catch _ => do
-    return ← elabTerm (← `(HPow.hPow $x $y)) none
- -/
-@[app_unexpander arrayTypeCont] def unexpandArrayTypeCont : Lean.PrettyPrinter.Unexpander
-  | `($(_) $I $X) =>
-    `($X ^ $I)
-  | _  => throw ()
+-- class SHPow {α : Sort u} {β : Sort v} {γ : outParam (Sort w)} (a :α) (b : β) (c : outParam γ)
+-- def SHPow.pow {α β γ} (a : α) (b : β) {c : γ} [SHPow a b c] := c
+
+-- instance {Cont Idx Elem} [ArrayTypeNotation Cont Idx Elem] : SHPow Elem Idx (arrayTypeCont Idx Elem)  := ⟨⟩
+-- instance {α β γ} (x : α) (y : β) [HPow α β γ] : SHPow x y (HPow.hPow x y):= ⟨⟩
+-- open Lean Elab Term Meta in
+-- elab:40 (priority:=high) x:term:41 " ^ " y:term:42 : term => withFreshMacroScope do
+--   let x ← elabTerm (← `(SHPow.pow $x $y)) none
+--   return x.getArg! 5
+
+-- /- #check K ^ (κ×ι)
+-- #eval 2 ^ 3
+
+--  -/
+
+-- /- open Lean Elab Term in
+-- elab:40 (priority:=high) x:term:41 " ^ " y:term:42 : term =>
+--   try
+--     let y ← elabTerm y none
+--     let x ← elabTerm x none
+--     let z ← Meta.mkAppOptM ``arrayTypeCont #[y,x,none,none]
+--     return z
+--   catch _ => do
+--     return ← elabTerm (← `(HPow.hPow $x $y)) none
+--  -/
+-- @[app_unexpander arrayTypeCont] def unexpandArrayTypeCont : Lean.PrettyPrinter.Unexpander
+--   | `($(_) $I $X) =>
+--     `($X ^ $I)
+--   | _  => throw ()
 
 
 -- Notation: Float^[10,20] --
diff --git a/SciLean/Tactic/DeduceBy.lean b/SciLean/Tactic/DeduceBy.lean
index 32203043..2f737a6a 100644
--- a/SciLean/Tactic/DeduceBy.lean
+++ b/SciLean/Tactic/DeduceBy.lean
@@ -57,6 +57,11 @@ partial def deduceByTactic : Tactic
   let goal ← getMainGoal
   let .some (_,lhs,rhs) := Expr.eq? (← goal.getType) | throwError "expected `?m = e`, got {← ppExpr (← goal.getType)}"
 
+  if ¬lhs.hasMVar ∨ ¬rhs.hasMVar then
+    let prf ← elabTerm (← `(by (conv => ($t;$t)); try simp)) (← goal.getType)
+    goal.assign prf
+    return ()
+
   -- if ¬lhs.isMVar then
   --   throwError "lhs is not mvar"