Theorems / mh_sets_4267d0
Mathlib held-out
Sets · medium
theorem lg_target {α : Type u} {β : Type v} (f : Set (α → β)) (s : Set α) [Finite ↑f] [Finite ↑s] : Finite ↑(f.seq s) := by- Mathlib declaration
- Finite.Set.finite_seq
- Held-out module
- Mathlib.Data.Set.Finite.Monad
- Banned modules (itself + downstream)
- 1
- Reference proof premises (reachable / held-out)
- 3 / 0
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.00010
Attempts
- sample 0 · round 0Wrong tactic7.2 s model time
Proof intro h_finite h_s_finite apply Finite.mk obtain ⟨f_list, f_list_finite⟩ := h_finite obtain ⟨s_list, s_list_finite⟩ := h_s_finite let f_seq_list := List.map (fun f => f <$> s_list) f_list let f_seq_set := Set.ofList f_seq_list use f_seq_set apply Set.finite_of_list apply List.finite_map apply List.finite_map_iff.1 f_list_finite apply List.finite_of_list apply List.finite_map apply List.finite_map_iff.1 s_list_finite
What Lean printed (this is all the model sees on repair) 4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce α : Type u β : Type v f : Set (α → β) s : Set α inst✝¹ : Finite ↑f inst✝ : Finite ↑s ⊢ Finite ↑(f.seq s)
Reference proof
Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.
instance finite_seq (f : Set (α → β)) (s : Set α) [Finite f] [Finite s] : Finite (f.seq s) := by rw [seq_def] infer_instance