Theorems / mh_prob_ed4cc9

Mathlib held-out

Probability · easy

Statement, exactly as the model and Lean see it
theorem lg_target : LawfulFunctor PMF := by
Mathlib declaration
PMF.instLawfulFunctor
Held-out module
Mathlib.Probability.ProbabilityMassFunction.Constructions
Banned modules (itself + downstream)
4
Reference proof premises (reachable / held-out)
1 / 1

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00007

Attempts

  1. sample 0 · round 0Wrong tactic2.4 s model time
    Proof
    intros F G f g η ϵ
constructor
· intros X
  dsimp [PMF.map]
  simp [η, ϵ]
  ext x
  simp [η, ϵ]
· intros X Y Z f g
  dsimp [PMF.map]
  simp [η, ϵ]
  ext x
  simp [η, ϵ]
    What Lean printed (this is all the model sees on repair)
    4:2: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

⊢ LawfulFunctor PMF

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

instance : LawfulFunctor PMF where
  map_const := rfl
  id_map := bind_pure
  comp_map _ _ _ := (map_comp _ _ _).symm