apply?

apply? は，カレントゴールを apply や refine で変形することができないか，ライブラリから検索して提案してくれるタクティクです． 複数の候補が提案されたときは，どれを選ぶとゴールが何に変わるのか表示されるので，その中から好ましいものを選ぶと良いでしょう．

import Mathlib.Algebra.Algebra.Basic -- 群を使うのに必要
import Mathlib.Tactic.Says -- `says` を使うのに必要

set_option says.verify true

variable (G H : Type)

/-- 群順同型が積を保つという定理 -/
example [Group G] [Group H] (f : G →* H) (a b : G) :
    f (a * b) = f a * f b := by
  -- `exact MonoidHom.map_mul f a b` を提案してくれる
  apply? says exact MonoidHom.map_mul f a b

補足

apply? はあくまで証明を書くときに補助として使うものです． sorry と同じように，清書した証明に残してはいけません． sorry と同じと言いましたが，実際 apply? は sorryAx を裏で使用します．

theorem T (x y : Nat) (_: x ≤ y) : 8 ^ x ≤ 16 ^ y := by
  apply?

  -- `apply?` しただけで `done` が通り，示せているように見える
  done

/-- info: 'T' depends on axioms: [propext, sorryAx] -/
#guard_msgs in #print axioms T