import Lean

open Lean Meta MVarId Elab Tactic Term in
/-- A tactic to reduce the main goal, up to definitional equality. -/
elab "reduceGoal" : tactic: Parser.Category
tactic => do
  let goal: ?m.125
goal ← Lean.Elab.Tactic.getMainGoal: TacticM MVarId
Lean.Elab.Tactic.getMainGoal
  withContext: {n : Type → Type ?u.127} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → MVarId → n α → n α
withContext goal: ?m.125
goal do
    let goalDecl: ?m.383
goalDecl ← getDecl: MVarId → MetaM MetavarDecl
getDecl goal: ?m.125
goal
    let goalType: ?m.386
goalType := goalDecl: ?m.383
goalDecl.type: MetavarDecl → Expr
type
    let reducedGoalType: ?m.690
reducedGoalType ← Meta.withTransparency: {n : Type → Type ?u.424} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → TransparencyMode → n α → n α
Meta.withTransparency TransparencyMode.reducible: TransparencyMode
TransparencyMode.reducible <|
       reduce: Expr → optParam Bool true → optParam Bool true → optParam Bool true → MetaM Expr
reduce (skipTypes := false: Bool
false) (skipProofs := false: Bool
false) goalType: ?m.386
goalType
    let goal': ?m.750
goal' ← MVarId.replaceTargetDefEq: MVarId → Expr → MetaM MVarId
MVarId.replaceTargetDefEq goal: ?m.125
goal reducedGoalType: ?m.690
reducedGoalType
    replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal [goal': ?m.750
goal']