fix: simp at hypotheses and using hypotheses

src/Lean/Elab/Tactic/Simp.lean

@@ -30,7 +30,8 @@ def simpLocalDeclFVarId (simpLemmas : SimpLemmas) (fvarId : FVarId) : TacticM Un
     let localDecl ← getLocalDecl fvarId
     let r ← simp localDecl.type simpLemmas
     match r.proof? with
-    | some proof => setGoals ((← replaceLocalDecl g fvarId r.expr proof).mvarId :: gs)
+    | some proof =>
+      setGoals ((← replaceLocalDecl g fvarId r.expr proof).mvarId :: gs)
     | none => setGoals ((← changeLocalDecl g fvarId r.expr (checkDefEq := false)) :: gs)
 
 def simpLocalDecl (simpLemmas : SimpLemmas) (userName : Name) : TacticM Unit :=
@@ -80,7 +81,7 @@ where
       let (g, _) ← getMainGoal
       withMVarContext g do
         let mut lemmas := lemmas
-        for simpLemma in stx[1].getArgs do
+        for simpLemma in stx[1].getSepArgs do
           let post :=
             if simpLemma[0].isNone then
               true

src/Lean/Meta/Tactic/Replace.lean

@@ -82,7 +82,7 @@ def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkD
           throwTacticEx `changeHypothesis mvarId m!"given type{indentExpr typeNew}\nis not definitionally equal to{indentExpr typeOld}"
     let finalize (targetNew : Expr) : MetaM MVarId := do
       let mvarId ← replaceTargetDefEq mvarId targetNew
-      let (_, mvarId) ← introNP mvarId (numReverted-1)
+      let (_, mvarId) ← introNP mvarId numReverted
       pure mvarId
     match target with
     | Expr.forallE n d b c => do check d; finalize (mkForall n c.binderInfo typeNew b)

tests/lean/run/simp4.lean

@@ -12,3 +12,21 @@ theorem ex1 (x : Nat) (h : q x) : q x ∧ q (f x) := by
 
 theorem ex2 (x : Nat) : q (f x) ∨ r (f x) := by
   simp
+
+@[simp] axiom ax5 (x : Nat) : 0 + x = x
+
+theorem ex3 (h : 0 + x = y) : f x = f y := by
+  simp at h
+  simp [h]
+
+theorem ex4 (x y z : Nat) (h : (x, z).1 = y) : f x = f y := by
+  simp at h
+  simp [h]
+
+theorem ex5
+    (f  : Nat → Nat → Nat)
+    (g  : Nat → Nat)
+    (h₁ : ∀ x, f x x = x)
+    (h₂ : ∀ x, g (g x) = x)
+    : f (g (g x)) (f x x) = x :=
+  by simp [h₁, h₂]