assumption discharger for DifferentiableAt

SciLean/FunctionSpaces/Differentiable/Basic.lean

@@ -236,18 +236,26 @@ theorem Prod.mk.arg_fstsnd.Differentiable_comp
   := Differentiable.prod hg hf
 
 
-
 -- Prod.fst --------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
+@[differentiable, fprop_rule]
+theorem Prod.fst.arg_self.Differentiable_comp 
+  (f : X → Y×Z) (hf : Differentiable R f)
+  : Differentiable R (fun x => (f x).1)
+  := Differentiable.fst hf
+
+
+-- Prod.snd --------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
 @[differentiable, fprop_rule]
 theorem Prod.snd.arg_self.Differentiable_comp 
   (f : X → Y×Z) (hf : Differentiable R f)
   : Differentiable R (fun x => (f x).2)
   := Differentiable.snd hf
 
 
-
 -- Function.comp ---------------------------------------------------------------
 --------------------------------------------------------------------------------
 

SciLean/FunctionSpaces/Differentiable/Tactic.lean

@@ -4,7 +4,7 @@ import SciLean.Tactic.FProp.Notation
 import SciLean.FunctionSpaces.Differentiable.Basic
 
 set_option profiler true
-set_option profiler.threshold 10 true
+set_option profiler.threshold 10
 
 example : Differentiable ℝ (fun x : ℝ => x) := by fprop
 
@@ -97,7 +97,9 @@ example : Differentiable ℝ (fun x : ℝ =>
   let x2 := x1
   let x3 := x2
   let x4 := x3
-  x4) := by fprop
+  let x5 := x4
+  let x6 := x5
+  x6) := by fprop
 
 
 example : Differentiable ℝ (fun x : ℝ => 

SciLean/FunctionSpaces/Differentiable/Test.lean

@@ -47,7 +47,7 @@ example
   (x : R) (f : R → K) (g : R → K) 
   (hf : DifferentiableAt R f x) (hg : DifferentiableAt R g x) (hx : g x ≠ 0)
   : DifferentiableAt R (fun x => f x / g x) x 
-  := by differentiable
+  := by fprop
 
 
 example
@@ -56,7 +56,7 @@ example
   (x : R) (k : K) (g : R → K) 
    (hg : DifferentiableAt R g x) (hx : g x ≠ 0)
   : DifferentiableAt R (fun x => k / g x) x 
-  := by differentiable
+  := by fprop
 
 
 example
@@ -65,5 +65,5 @@ example
   (x : R) (f : R → K) (k : K)
   (hf : DifferentiableAt R f x) (hx : k ≠ 0)
   : DifferentiableAt R (fun x => f x / k) x 
-  := by differentiable
+  := by fprop
 

SciLean/FunctionSpaces/DifferentiableAt/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Analysis.Calculus.Deriv.Inv
 
 import SciLean.FunctionSpaces.Differentiable.Init
 import SciLean.Tactic.FProp.Basic
+import SciLean.Tactic.FProp.Notation
 
 
 namespace SciLean
@@ -65,8 +66,6 @@ theorem pi_rule
   := by apply differentiableAt_pi.2 hf
 
 
-
-
 end SciLean.DifferentiableAt
 
 
@@ -164,7 +163,9 @@ def DifferentiableAt.fpropExt : FPropExt where
     }
     FProp.tryTheorem? e thm (fun _ => pure none)
 
-  discharger _ := return none
+  discharger e := 
+    FProp.tacticToDischarge (Syntax.mkLit ``Lean.Parser.Tactic.assumption "assumption") e
+
 
 -- register fderiv
 #eval show Lean.CoreM Unit from do

SciLean/Tactic/FProp/Basic.lean

@@ -4,6 +4,31 @@ open Lean Meta Qq
 
 namespace SciLean.FProp
 
+open Elab Term in
+def tacticToDischarge (tacticCode : Syntax) : Expr → MetaM (Option Expr) := fun e => do
+    let mvar ← mkFreshExprSyntheticOpaqueMVar e `simp.discharger
+    let runTac? : TermElabM (Option Expr) :=
+      try
+        /- We must only save messages and info tree changes. Recall that `simp` uses temporary metavariables (`withNewMCtxDepth`).
+           So, we must not save references to them at `Term.State`. -/
+        withoutModifyingStateWithInfoAndMessages do
+          instantiateMVarDeclMVars mvar.mvarId!
+
+          let goals ←
+            withSynthesize (mayPostpone := false) do Tactic.run mvar.mvarId! (Tactic.evalTactic tacticCode *> Tactic.pruneSolvedGoals)
+
+          let result ← instantiateMVars mvar
+          if result.hasExprMVar then
+            return none
+          else
+            return some result
+      catch _ =>
+        return none
+    let (result?, _) ← runTac?.run {} {} 
+
+    return result?
+
+
 /-- Takes lambda function `fun x => b` and splits it into composition of two functions. 
 
   Example:
@@ -159,11 +184,7 @@ mutual
       else
 
         trace[Meta.Tactic.fprop.step] "fvar app case: decomposed into `({← ppExpr f}) ∘ ({← ppExpr g})`"
-
-        let fg ← mkAppM ``Function.comp #[f,g]
-        let e' := ext.replaceFPropFun e fg
-
-        fprop e' -- are we abusing `Function.comp` defeq here?
+        ext.compRule e f g
 
   partial def applyTheorems (e : Expr) (discharge? : Expr → FPropM (Option Expr)) : FPropM (Option Expr) := do
     let .some (fpropName, ext, f) ← getFProp? e