my assumption

my_assumption.lean

import Lean

open Lean Meta Tactic

def myAssumption (mvarId : MVarId) : Elab.Tactic.TacticM PUnit := do
  -- Check that `mvarId` is not already assigned.
  mvarId.checkNotAssigned `myAssumption
  -- Use the local context of `mvarId`.
  mvarId.withContext do
    -- The target is the type of `mvarId`.
    let target ← mvarId.getType
    -- For each hypothesis in the local context:
    for ldecl in ← getLCtx do
      -- If the hypothesis is an implementation detail, skip it.
      if ldecl.isImplementationDetail then
        continue
      -- If the type of the hypothesis is definitionally equal to the target
      -- type:
      if ← isDefEq ldecl.type target then
        -- Use the local hypothesis to prove the goal.
        mvarId.assign ldecl.toExpr
        -- Stop and return true.
        return ()
    -- If we have not found any suitable local hypothesis, return false.
    return ()

elab "my_assumption" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    myAssumption goal

example : P -> P ∧ Q := by 
  intro h
  constructor
  · my_assumption
  · my_assumption; sorry