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

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
let ψ : (E ⧸ p) →ₗ[𝕜] ι → 𝕜 := p.liftQ φ p_eq.le

Result:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
⊢ K ∈ span 𝕜 (Set.range L)

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
have : ⨅ i, ker (L' i) ≤ ker K' := by
  simp_rw +zetaDelta [← ker_pi, pi_liftQ_eq_liftQ_pi, ker_liftQ_eq_bot' p φ p_eq]
  exact bot_le

Result:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, ker (L' i) ≤ ker K'
⊢ K ∈ span 𝕜 (Set.range L)

Proof state:
case h.e'_2
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, ker (L' i) ≤ ker K'
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
x : E
⊢ (∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ) x = (∑ i : ι, c i • L' i) (p.mkQ x)

Tactic:
simp only [L',coeFn_sum, Finset.sum_apply, smul_apply, coe_comp, Function.comp_apply,
  smul_eq_mul]

Result:
no goals

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

Tactic:
let φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L

Result:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
⊢ K ∈ span 𝕜 (Set.range L)

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
have _ : FiniteDimensional 𝕜 (E ⧸ p) := of_injective ψ (ker_eq_bot.1 (ker_liftQ_eq_bot' p φ p_eq))

Result:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
⊢ K ∈ span 𝕜 (Set.range L)

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

Tactic:
have _ := Fintype.ofFinite ι

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

Proof state:
case intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, ker (L' i) ≤ ker K'
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
⊢ ∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = p.liftQ K h ∘ₗ p.mkQ

Tactic:
ext x

Result:
case intro.h
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, ker (L' i) ≤ ker K'
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
x : E
⊢ (∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ) x = (p.liftQ K h ∘ₗ p.mkQ) x

Proof state:
case intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, ker (L' i) ≤ ker K'
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
⊢ ∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = K

Tactic:
rw [← p.liftQ_mkQ K h]

Result:
case intro
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
K' : E ⧸ p →ₗ[𝕜] 𝕜 := p.liftQ K h
this : ⨅ i, ker (L' i) ≤ ker K'
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
⊢ ∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = p.liftQ K h ∘ₗ p.mkQ

Proof state:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
⊢ K ∈ span 𝕜 (Set.range L)

Tactic:
let L' i : (E ⧸ p) →ₗ[𝕜] 𝕜 := p.liftQ (L i) (iInf_le _ i)

Result:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst✝³ : Field 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ i, ker (L i) ≤ ker K
x✝¹ : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi L
p : Submodule 𝕜 E := ⨅ i, ker (L i)
p_eq : p = ker φ
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := p.liftQ φ ⋯
x✝ : FiniteDimensional 𝕜 (E ⧸ p)
L' : ι → E ⧸ p →ₗ[𝕜] 𝕜 := fun i => p.liftQ (L i) ⋯
⊢ K ∈ span 𝕜 (Set.range L)