awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
s : Set (M →ₗ[R] R)
inst_4 : Projective R (HasQuotient.Quotient (M →ₗ[R] R) (B := Submodule R (M →ₗ[R] R)) (span R s))
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) z : R) (0 : R)
hn : Ne (α := Submodule R (M →ₗ[R] R)) (span R s) ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) φ
this : ∀ (f : M →ₗ[R] R) (hf : f ∈ s), Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) φs : R) (0 : R)
obtain : ∀ (x : M →ₗ[R] R) (xs : x ∈ s) (hx : Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) φs : R) (0 : R)), False
⊢ False

Tactic:
obtain ⟨x, xs, hx⟩ := h φs (by simp [φne, φs])
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
s : Set (M →ₗ[R] R)
inst_4 : Projective R (HasQuotient.Quotient (M →ₗ[R] R) (B := Submodule R (M →ₗ[R] R)) (span R s))
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) z : R) (0 : R)
hn : Ne (α := Submodule R (M →ₗ[R] R)) (span R s) ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) φ
this : ∀ (f : M →ₗ[R] R) (hf : f ∈ s), Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) φs : R) (0 : R)
x : M →ₗ[R] R
xs : x ∈ s
hx : Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) φs : R) (0 : R)
⊢ False

Tactic:
hx <| this x xs
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsReflexive R M
s : Set (M →ₗ[R] R)
inst_4 : Projective R (HasQuotient.Quotient (M →ₗ[R] R) (B := Submodule R (M →ₗ[R] R)) (span R s))
h : ∀ (z : M), z ≠ 0 → ∃ f ∈ s, Ne.{u_1 + 1} (α := R) ((f : (a : M) → R) z : R) (0 : R)
hn : Ne (α := Submodule R (M →ₗ[R] R)) (span R s) ⊤
φ : Dual R (M →ₗ[R] R)
φne : φ ≠ 0
hφ : map φ (span R s) = ⊥
φs : M := (LinearEquiv.symm (evalEquiv R M) : (a : Dual R (Dual R M)) → M) φ
this : ∀ (f : M →ₗ[R] R) (hf : f ∈ s), Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) φs : R) (0 : R)
x : M →ₗ[R] R
xs : x ∈ s
hx : Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) φs : R) (0 : R)
⊢ False

Tactic:
exact hx <| this x xs
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
by_contra : ∀ (hK : K ∉ span 𝕜 (Set.range L)), False
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K

Tactic:
by_contra hK
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
rcases :
  ∀ (φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)) (φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜))
    (hφ : map φ (span 𝕜 (Set.range L)) = ⊥), False
⊢ False

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

Premises used: inferInstance, Submodule.exists_dual_map_eq_bot_of_notMem
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜)
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (LinearEquiv.symm (evalEquiv 𝕜 E) : (a : Dual 𝕜 (Dual 𝕜 E)) → E) φ
⊢ Eq.{u_4 + 1} (α := 𝕜) ((K : (a : E) → 𝕜) φs : 𝕜) (0 : 𝕜)

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

Premises used: Iff.mpr, Submodule.mem_iInf, Set.Mem, Submodule.mem_bot, setOf, Set.preimage, Set.singleton, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜)
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (LinearEquiv.symm (evalEquiv 𝕜 E) : (a : Dual 𝕜 (Dual 𝕜 E)) → E) φ
refine : ∀ (i : ι), Membership.mem.{u_4, u_4} (α := 𝕜) (γ := Submodule 𝕜 𝕜) ⊥ ((L i : (a : E) → 𝕜) φs : 𝕜)
⊢ Eq.{u_4 + 1} (α := 𝕜) ((K : (a : E) → 𝕜) φs : 𝕜) (0 : 𝕜)

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

Premises used: Iff.mpr, Submodule.mem_iInf
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜)
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (LinearEquiv.symm (evalEquiv 𝕜 E) : (a : Dual 𝕜 (Dual 𝕜 E)) → E) φ
i : ι
rw :
  ∃ (y : E →ₗ[𝕜] 𝕜),
    Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) y ∧
      Eq.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) y : 𝕜) ((L i : (a : E) → 𝕜) φs : 𝕜)
⊢ Membership.mem.{u_4, u_4} (α := 𝕜) (γ := Submodule 𝕜 𝕜) ⊥ ((L i : (a : E) → 𝕜) φs : 𝕜)

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

Premises used: Submodule.mem_map
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜)
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (LinearEquiv.symm (evalEquiv 𝕜 E) : (a : Dual 𝕜 (Dual 𝕜 E)) → E) φ
i : ι
⊢ ∃ (y : E →ₗ[𝕜] 𝕜),
    Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) y ∧
      Eq.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) y : 𝕜) ((L i : (a : E) → 𝕜) φs : 𝕜)

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

Premises used: Module.apply_evalEquiv_symm_apply, And.intro, Exists.intro, Submodule.subset_span, Eq.symm, rfl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜)
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (LinearEquiv.symm (evalEquiv 𝕜 E) : (a : Dual 𝕜 (Dual 𝕜 E)) → E) φ
i : ι
⊢ ∃ (y : E →ₗ[𝕜] 𝕜),
    Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) y ∧
      Eq.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) y : 𝕜) ((L i : (a : E) → 𝕜) φs : 𝕜)

Tactic:
exact ⟨L i, Submodule.subset_span ⟨i, rfl⟩, (apply_evalEquiv_symm_apply 𝕜 E _ φ).symm⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜)
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (LinearEquiv.symm (evalEquiv 𝕜 E) : (a : Dual 𝕜 (Dual 𝕜 E)) → E) φ
⊢ Eq.{u_4 + 1} (α := 𝕜) ((K : (a : E) → 𝕜) φs : 𝕜) (0 : 𝕜)

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⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)
φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜)
hφ : map φ (span 𝕜 (Set.range L)) = ⊥
φs : E := (LinearEquiv.symm (evalEquiv 𝕜 E) : (a : Dual 𝕜 (Dual 𝕜 E)) → E) φ
this : Eq.{u_4 + 1} (α := 𝕜) ((K : (a : E) → 𝕜) φs : 𝕜) (0 : 𝕜)
⊢ False

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

Premises used: Module.apply_evalEquiv_symm_apply
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
have : ∀ (x : Fintype ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K

Tactic:
have _ := Fintype.ofFinite ι
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
⊢ p = φ.ker

Tactic:
have p_eq : p = ker φ := (ker_pi L).symm
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
simp_rw : ⊥ ≤ (liftQ (⨅ (i : ι), (L i).ker) K h).ker
⊢ ⨅ (i : ι), (L' i).ker ≤ K'.ker

Tactic:
simp_rw +zetaDelta [← ker_pi, pi_liftQ_eq_liftQ_pi, ker_liftQ_eq_bot' p φ p_eq]

Premises used: LinearMap.ker_pi, Submodule.ker_liftQ_eq_bot', Submodule.pi_liftQ_eq_liftQ_pi
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
⊢ ⊥ ≤ (liftQ (⨅ (i : ι), (L i).ker) K h).ker

Tactic:
bot_le

Premises used: Set.Mem, bot_le
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
⊢ ⊥ ≤ (liftQ (⨅ (i : ι), (L i).ker) K h).ker

Tactic:
exact bot_le

Premises used: bot_le
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
⊢ ⨅ (i : ι), (L' i).ker ≤ K'.ker

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
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
obtain :
  ∀ (c : ι → 𝕜) (hK' : ∑ i : ι, c i • L' i = K'), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K

Tactic:
obtain ⟨c, hK'⟩ :=
    (mem_span_range_iff_exists_fun 𝕜).1 (FiniteDimensional.mem_span_of_iInf_ker_le_ker this)

Premises used: FiniteDimensional.mem_span_of_iInf_ker_le_ker, Submodule.mem_span_range_iff_exists_fun, Iff.mp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K

Tactic:
(mem_span_range_iff_exists_fun 𝕜).2 ⟨c, ?_⟩

Premises used: Iff.mpr, Submodule.mem_span_range_iff_exists_fun, Exists.intro
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
enter : fun (i : ι) ↦ c i • L i
| ∑ i : ι, c i • L i

Tactic:
enter [2]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
i : ι
h₁ : c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ
| c i • L i

Tactic:
rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]

Premises used: Submodule.liftQ_mkQ, iInf_le
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
h₁ : ∀ (i : ι), c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ
| ∑ i : ι, c i • L i

Tactic:
enter [2]; intro i; rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
conv_lhs : ∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = K
⊢ ∑ i : ι, c i • L i = K

Tactic:
conv_lhs => enter [2]; intro i; rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
rw : ∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = p.liftQ K h ∘ₗ p.mkQ
⊢ ∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = K

Tactic:
rw [← p.liftQ_mkQ K h]

Premises used: Submodule.liftQ_mkQ
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
h₁ :
  ∀ (x_1 : E),
    Eq.{u_4 + 1} (α := 𝕜) ((∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ : (a : E) → 𝕜) x_1 : 𝕜)
      ((p.liftQ K h ∘ₗ p.mkQ : (a : E) → 𝕜) x_1 : 𝕜)
⊢ ∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = p.liftQ K h ∘ₗ p.mkQ

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x_1 : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
x : E
⊢ Eq.{u_4 + 1} (α := 𝕜) ((∑ i : ι, c i • L' i : (a : E ⧸ p) → 𝕜) ((p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p) : 𝕜)
    ((K' : (a : E ⧸ p) → 𝕜) ((p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p) : 𝕜)

Tactic:
LinearMap.congr_fun hK' (p.mkQ x)

Premises used: LinearMap.congr_fun, Submodule.mkQ, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
Goal:
ι : Type u_3
𝕜 : Type u_4
E : Type u_5
inst : Field 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Finite ι
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
x_1 : Fintype ι
φ : E →ₗ[𝕜] ι → 𝕜 := LinearMap.pi (φ := fun (a : ι) ↦ 𝕜) L
p : Submodule 𝕜 E := ⨅ (i : ι), (L i).ker
p_eq : p = φ.ker
ψ : E ⧸ p →ₗ[𝕜] ι → 𝕜 := failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h_1 : FiniteDimensional.{u_4, u_5} 𝕜 (E ⧸ p)
L' : (i : ι) → LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := fun (i : ι) ↦ p.liftQ (L i) ⋯
K' : LinearMap.{u_4, u_4, u_5, u_4} (RingHom.id 𝕜) (E ⧸ p) 𝕜 := p.liftQ K h
this : ⨅ (i : ι), (L' i).ker ≤ K'.ker
c : ι → 𝕜
hK' : ∑ i : ι, c i • L' i = K'
x : E
h₁ :
  Eq.{u_4 + 1} (α := 𝕜) ((∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ : (a : E) → 𝕜) x : 𝕜)
    ((∑ i : ι, c i • L' i : (a : E ⧸ p) → 𝕜) ((p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p) : 𝕜)
⊢ Eq.{u_4 + 1} (α := 𝕜) ((∑ i : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ : (a : E) → 𝕜) x : 𝕜)
    ((p.liftQ K h ∘ₗ p.mkQ : (a : E) → 𝕜) x : 𝕜)

Tactic:
convert! LinearMap.congr_fun hK' (p.mkQ x)

Premises used: LinearMap.congr_fun, Submodule.mkQ, DFunLike.coe