Algebra · hard

Statement, exactly as the model and Lean see it

theorem lg_target {ι : Type u_1} {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [_root_.Module K M] [Finite ι] [Infinite K] (f : ι → Module.Dual K M) (h : ∀ (i : ι), ∃ x, (f i) x ≠ 0) : ∃ x, ∀ (i : ι), (f i) x ≠ 0 := by

Mathlib declaration: Module.Dual.exists_forall_ne_zero_of_forall_exists
Held-out module: Mathlib.Algebra.Module.Submodule.Union
Banned modules (itself + downstream): 9
Reference proof premises (reachable / held-out): 2 / 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.00009

Attempts

sample 0 · round 0Lean 3 syntax2.9 s model time

Proof

let S := {i | ∃ x, (f i) x ≠ 0}
have hS : Set.univ = S := by rw [h]
obtain ⟨x, hx⟩ := (Set.finite.exists_maximal {i | ∃ x, (f i) x ≠ 0} (λ i j h1 h2, (Module.linear_map.ker_eq_bot_iff _).mp (Set.eq_of_subset_of_le h1 h2)))
apply hx

What Lean printed (this is all the model sees on repair)

6:82: error: unexpected token ','; expected '↦', '=>'
5:35: error: Invalid rewrite argument: Expected an equality or iff proof or definition name, but `h ?i` is a proof of
  ∃ x, (f ?i) x ≠ 0
6:21: error: Unknown constant `Set.finite.exists_maximal`

Reference proof

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

lemma Module.Dual.exists_forall_ne_zero_of_forall_exists
    (f : ι → Dual K M) (h : ∀ i, ∃ x, f i x ≠ 0) :
    ∃ x, ∀ i, f i x ≠ 0 := by
  let p i := LinearMap.ker (f i)
  replace h i : p i ≠ ⊤ := by specialize h i; aesop
  obtain ⟨x, hx⟩ := Submodule.exists_forall_notMem_of_forall_ne_top p h
  exact ⟨x, by simpa [p] using hx⟩