-- Mathlib/LinearAlgebra/Dual.lean
theorem _root_.FiniteDimensional.mem_span_of_iInf_ker_le_ker [FiniteDimensional 𝕜 E]
    {L : ι → E →ₗ[𝕜] 𝕜} {K : E →ₗ[𝕜] 𝕜}
    (h : ⨅ i, LinearMap.ker (L i) ≤ ker K) : K ∈ span 𝕜 (range L)

Proof state:
case intro.intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
⊢ False

Tactic:
have : K φs = 0 := by
  refine h <| (Submodule.mem_iInf _).2 fun i ↦ (mem_bot 𝕜).1 ?_
  rw [← hφ, Submodule.mem_map]
  exact ⟨L i, Submodule.subset_span ⟨i, rfl⟩, (apply_evalEquiv_symm_apply 𝕜 E _ φ).symm⟩

Result:
case intro.intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
this : K φs = 0
⊢ False

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
i : ι
⊢ (L i) φs ∈ ⊥

Tactic:
rw [← hφ, Submodule.mem_map]

Result:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
i : ι
⊢ ∃ y ∈ span 𝕜 (Set.range L), φ y = (L i) φs

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
⊢ K φs = 0

Tactic:
refine h <| (Submodule.mem_iInf _).2 fun i ↦ (mem_bot 𝕜).1 ?_

Result:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
i : ι
⊢ (L i) φs ∈ ⊥

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
by_contra hK

Result:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
⊢ False

Proof state:
case intro.intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
⊢ False

Tactic:
let φs := (Module.evalEquiv 𝕜 E).symm φ

Result:
case intro.intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
⊢ False

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
⊢ False

Tactic:
rcases exists_dual_map_eq_bot_of_nmem hK inferInstance with ⟨φ, φne, hφ⟩

Result:
case intro.intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
⊢ False

Proof state:
case intro.intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
this : K φs = 0
⊢ False

Tactic:
simp only [apply_evalEquiv_symm_apply, φs, φne] at this

Result:
no goals

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : φ K ≠ 0
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (evalEquiv 𝕜 E).symm φ
i : ι
⊢ ∃ y ∈ span 𝕜 (Set.range L), φ y = (L i) φs

Tactic:
exact ⟨L i, Submodule.subset_span ⟨i, rfl⟩, (apply_evalEquiv_symm_apply 𝕜 E _ φ).symm⟩

Result:
no goals