awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : ι, c i • L i
have h₁ : ∀ (i : ι), c i • p.liftQ (L i) sorry ∘ₗ p.mkQ
Tactic: enter [2]; intro i; rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : ι, c i • L i = K
have conv_lhs : ∑ i : ι, c i • p.liftQ (L i) sorry ∘ₗ p.mkQ = K
Tactic: conv_lhs => enter [2]; intro i; rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = K
have rw : ∑ i : ι, c i • p.liftQ (L i) sorry ∘ₗ p.mkQ = p.liftQ K h ∘ₗ p.mkQ
Tactic: rw [← p.liftQ_mkQ K h]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 : ι, c i • p.liftQ (L i) ⋯ ∘ₗ p.mkQ = p.liftQ K h ∘ₗ p.mkQ
have h₁ : ∀ (x_1 : E),
  Eq.{u_4 + 1} (α := 𝕜) ((∑ i : ι, c i • p.liftQ (L i) sorry ∘ₗ p.mkQ : (a : E) → 𝕜) x_1 : 𝕜)
    ((p.liftQ K h ∘ₗ p.mkQ : (a : E) → 𝕜) x_1 : 𝕜)
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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 • p.liftQ (L i) ⋯ ∘ₗ p.mkQ : (a : E) → 𝕜) x : 𝕜)
    ((p.liftQ K h ∘ₗ p.mkQ : (a : E) → 𝕜) x : 𝕜)
have h₁ : Eq.{u_4 + 1} (α := 𝕜) ((∑ i : ι, c i • p.liftQ (L i) sorry ∘ₗ p.mkQ : (a : E) → 𝕜) x : 𝕜)
  ((∑ i : ι, c i • L' i : (a : E ⧸ p) → 𝕜) ((p.mkQ : (a : E) → E ⧸ p) x : E ⧸ p) : 𝕜)
Tactic: convert! LinearMap.congr_fun hK' (p.mkQ x)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ (dualAnnihilator W).dualCoannihilator = W
have refine : ∀ v ∉ W, v ∉ (dualAnnihilator W).dualCoannihilator
Tactic: refine le_antisymm (fun v ↦ Function.mtr ?_) (le_dualAnnihilator_dualCoannihilator _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
⊢ v ∉ W → v ∉ (dualAnnihilator W).dualCoannihilator
have simp : v ∉ W →
  ¬∀ (φ : Dual K V),
      (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) →
        Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
Tactic: simp only [mem_dualAnnihilator, mem_dualCoannihilator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
⊢ v ∉ W →
    ¬∀ (φ : Dual K V),
        (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) →
          Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
have rw : (¬∀ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
      Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
  ¬∀ (φ : Dual K V),
      (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) →
        Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
Tactic: rw [← Quotient.mk_eq_zero W, ← Module.forall_dual_apply_eq_zero_iff K]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
⊢ (¬∀ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
        Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
    ¬∀ (φ : Dual K V),
        (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) →
          Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
have push : (∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
    Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
  ∃ (φ : Dual K V),
    (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) ∧
      Ne.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
Tactic: push Not
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
⊢ (∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
      Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
    ∃ (φ : Dual K V),
      (∀ w ∈ W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) w : K) (0 : K)) ∧
        Ne.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
have refine : (∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)),
    Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) →
  ∀ (φ : Dual.{u_1, u_2} K (V ⧸ W))
    (hφ : Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)) (w : V) (hw : w ∈ W),
    Eq.{u_1 + 1} (α := K) ((φ ∘ₗ mkQ W : (a : V) → K) w : K) (0 : K)
Tactic: refine fun ⟨φ, hφ⟩ ↦ ⟨φ.comp W.mkQ, fun w hw ↦ ?_, hφ⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
h :
  ∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)), Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
φ : Dual.{u_1, u_2} K (V ⧸ W)
hφ : Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
w : V
hw : w ∈ W
⊢ Eq.{u_1 + 1} (α := K) ((φ ∘ₗ mkQ W : (a : V) → K) w : K) (0 : K)
have rw : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) ((mkQ W : (a : V) → V ⧸ W) w : V ⧸ W) : K) (0 : K)
Tactic: rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
h :
  ∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)), Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
φ : Dual.{u_1, u_2} K (V ⧸ W)
hφ : Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
w : V
hw : w ∈ W
rw : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) ((mkQ W : (a : V) → V ⧸ W) w : V ⧸ W) : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((φ ∘ₗ mkQ W : (a : V) → K) w : K) (0 : K)
have rw₁ : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk w) : K) (0 : K)
Tactic: rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
h :
  ∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)), Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
φ : Dual.{u_1, u_2} K (V ⧸ W)
hφ : Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
w : V
hw : w ∈ W
rw : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) ((mkQ W : (a : V) → V ⧸ W) w : V ⧸ W) : K) (0 : K)
rw₁ : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk w) : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((φ ∘ₗ mkQ W : (a : V) → K) w : K) (0 : K)
have rw₂ : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) 0 : K) (0 : K)
Tactic: rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
h :
  ∃ (φ : Dual.{u_1, u_2} K (V ⧸ W)), Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
φ : Dual.{u_1, u_2} K (V ⧸ W)
hφ : Ne.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk v) : K) (0 : K)
w : V
hw : w ∈ W
rw : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) ((mkQ W : (a : V) → V ⧸ W) w : V ⧸ W) : K) (0 : K)
rw₁ : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) (Submodule.Quotient.mk w) : K) (0 : K)
rw₂ : Eq.{u_1 + 1} (α := K) ((φ : (a : V ⧸ W) → K) 0 : K) (0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((φ ∘ₗ mkQ W : (a : V) → K) w : K) (0 : K)
have rw₃ : Eq.{u_1 + 1} (α := K) 0 0
Tactic: rw [comp_apply, mkQ_apply, (Quotient.mk_eq_zero W).mpr hw, φ.map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
⊢ (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)) ↔ v ∈ W
have rw : (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)) ↔
  v ∈ (dualAnnihilator W).dualCoannihilator
Tactic: rw [← SetLike.ext_iff.mp dualAnnihilator_dualCoannihilator_eq v, mem_dualCoannihilator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
v : V
rw :
  (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)) ↔
    v ∈ (dualAnnihilator W).dualCoannihilator
⊢ (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)) ↔ v ∈ W
have rw₁ : (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)) ↔
  ∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) v : K) (0 : K)
Tactic: rw [← SetLike.ext_iff.mp dualAnnihilator_dualCoannihilator_eq v, mem_dualCoannihilator]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator = W
have h : ∀ (x : V), x ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator ↔ x ∈ W
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
x : V
⊢ x ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator ↔ x ∈ W
have h : (∀ φ ∈ dualAnnihilator W, Eq.{u_1 + 1} (α := K) ((φ : (a : V) → K) x : K) (0 : K)) ↔
  x ∈ comap (Dual.eval K V) (dualAnnihilator W).dualAnnihilator
Tactic: rw [Iff.comm, ← forall_mem_dualAnnihilator_apply_eq_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
⊢ dualRestrict W ∘ₗ W.dualLift = 1
have h : ∀ (φ : Dual.{u_1, u_2} K ↥W) (x : ↥W),
  Eq.{u_1 + 1} (α := K)
    ((((dualRestrict W ∘ₗ W.dualLift : (a : Dual K ↥W) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)
    ((((1 : (a : Dual K ↥W) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)
Tactic: ext φ x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
x : Dual.{u_1, u_2} K ↥W
⊢ (dualRestrict W : (a : Dual K V) → Dual K ↥W) ((W.dualLift : (a : Dual K ↥W) → Dual K V) x) = x
have rw : (dualRestrict W ∘ₗ W.dualLift : (a : Dual K ↥W) → Dual K ↥W) x = x
Tactic: rw [← LinearMap.comp_apply, dualRestrict_comp_dualLift, End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
x : Dual.{u_1, u_2} K ↥W
rw : (dualRestrict W ∘ₗ W.dualLift : (a : Dual K ↥W) → Dual K ↥W) x = x
⊢ (dualRestrict W : (a : Dual K V) → Dual K ↥W) ((W.dualLift : (a : Dual K ↥W) → Dual K V) x) = x
have rw₁ : (1 : (a : Dual K ↥W) → Dual K ↥W) x = x
Tactic: rw [← LinearMap.comp_apply, dualRestrict_comp_dualLift, End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
x : Dual.{u_1, u_2} K ↥W
rw : (dualRestrict W ∘ₗ W.dualLift : (a : Dual K ↥W) → Dual K ↥W) x = x
rw₁ : (1 : (a : Dual K ↥W) → Dual K ↥W) x = x
⊢ (dualRestrict W : (a : Dual K V) → Dual K ↥W) ((W.dualLift : (a : Dual K ↥W) → Dual K V) x) = x
have rw₂ : x = x
Tactic: rw [← LinearMap.comp_apply, dualRestrict_comp_dualLift, End.one_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
W : Subspace K V
φ : Dual K V
⊢ Eq (α := Dual.{u_1, u_2} K ↥W)
    ((W.quotAnnihilatorEquiv : (a : Dual K V ⧸ dualAnnihilator W) → Dual K ↥W) (Submodule.Quotient.mk φ) :
      Dual.{u_1, u_2} K ↥W)
    ((dualRestrict W : (a : Dual K V) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W)
have h : ∀ (x : ↥W),
  Eq.{u_1 + 1} (α := K)
    ((((W.quotAnnihilatorEquiv : (a : Dual K V ⧸ dualAnnihilator W) → Dual K ↥W) (Submodule.Quotient.mk φ) :
            Dual.{u_1, u_2} K ↥W) :
          (a : ↥W) → K)
        x :
      K)
    ((((dualRestrict W : (a : Dual K V) → Dual K ↥W) φ : Dual.{u_1, u_2} K ↥W) : (a : ↥W) → K) x : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
⊢ finrank K (Dual K V) = finrank K V
have pos : ∀ (h : FiniteDimensional K V), finrank K (Dual K V) = finrank K V
Tactic: by_cases h : FiniteDimensional K V
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
pos : ∀ (h : FiniteDimensional K V), finrank K (Dual K V) = finrank K V
⊢ finrank K (Dual K V) = finrank K V
have neg : ∀ (h : ¬FiniteDimensional K V), finrank K (Dual K V) = finrank K V
Tactic: by_cases h : FiniteDimensional K V
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ¬FiniteDimensional K V
⊢ finrank K (Dual K V) = finrank K V
have neg : ∀ (s : Finset V) (a : Basis (↑(↑s : Set V) : Type u_2) K V), False
Tactic: rw [finrank_eq_zero_of_basis_imp_false, finrank_eq_zero_of_basis_imp_false]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
h : ¬FiniteDimensional K V
neg : ∀ (s : Finset V) (a : Basis (↑(↑s : Set V) : Type u_2) K V), False
⊢ finrank K (Dual K V) = finrank K V
have neg₁ : ∀ (s : Finset (Dual K V)) (a : Basis (↑(↑s : Set (Dual K V)) : Type (max u_1 u_2)) K (Dual K V)), False
Tactic: rw [finrank_eq_zero_of_basis_imp_false, finrank_eq_zero_of_basis_imp_false]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V : (a : Submodule K V) → Submodule K (Dual K (Dual K V))) W
have this : (dualAnnihilator W).dualCoannihilator = W
Tactic: have : _ = W := Subspace.dualAnnihilator_dualCoannihilator_eq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
this : (dualAnnihilator W).dualCoannihilator = W
⊢ (dualAnnihilator W).dualAnnihilator = (mapEvalEquiv K V : (a : Submodule K V) → Submodule K (Dual K (Dual K V))) W
have this₁ : (OrderIso.symm (mapEvalEquiv K V) : (a : Submodule K (Dual K (Dual K V))) → Submodule K V)
    (dualAnnihilator W).dualAnnihilator =
  W
Tactic: rw [dualCoannihilator, ← Module.mapEvalEquiv_symm_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
⊢ finrank.{u_1, u_2} K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
have rw : finrank.{u_1, u_2} K ↥W + finrank.{u_1, u_2} K (V ⧸ W) = finrank K V
Tactic: rw [← W.quotEquivAnnihilator.finrank_eq, add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
rw : finrank.{u_1, u_2} K ↥W + finrank.{u_1, u_2} K (V ⧸ W) = finrank K V
⊢ finrank.{u_1, u_2} K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
have rw₁ : finrank.{u_1, u_2} K (V ⧸ W) + finrank.{u_1, u_2} K ↥W = finrank K V
Tactic: rw [← W.quotEquivAnnihilator.finrank_eq, add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K V
rw : finrank.{u_1, u_2} K ↥W + finrank.{u_1, u_2} K (V ⧸ W) = finrank K V
rw₁ : finrank.{u_1, u_2} K (V ⧸ W) + finrank.{u_1, u_2} K ↥W = finrank K V
⊢ finrank.{u_1, u_2} K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
have rw₂ : finrank K V = finrank K V
Tactic: rw [← W.quotEquivAnnihilator.finrank_eq, add_comm, Submodule.finrank_quotient_add_finrank]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K (Dual K V)
⊢ finrank K ↥W + finrank.{u_1, u_2} K ↥(dualCoannihilator W) = finrank K V
have rw : finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
Tactic: rw [finrank_dualCoannihilator_eq, finrank_add_finrank_dualAnnihilator_eq, dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K (Dual K V)
rw : finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
⊢ finrank K ↥W + finrank.{u_1, u_2} K ↥(dualCoannihilator W) = finrank K V
have rw₁ : finrank K (Dual K V) = finrank K V
Tactic: rw [finrank_dualCoannihilator_eq, finrank_add_finrank_dualAnnihilator_eq, dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
W : Subspace K (Dual K V)
rw : finrank K ↥W + finrank K ↥(dualAnnihilator W) = finrank K V
rw₁ : finrank K (Dual K V) = finrank K V
⊢ finrank K ↥W + finrank.{u_1, u_2} K ↥(dualCoannihilator W) = finrank K V
have rw₂ : finrank K V = finrank K V
Tactic: rw [finrank_dualCoannihilator_eq, finrank_add_finrank_dualAnnihilator_eq, dual_finrank_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
w : M
hw : w ∈ W
⊢ w ∈ W.dualAnnihilator.subtype.flip.ker
have h : ∀ (φ : Dual R M) (hφ : φ ∈ W.dualAnnihilator),
  Eq.{u_1 + 1} (α := R)
    ((((W.dualAnnihilator.subtype.flip : (a : M) → ↥W.dualAnnihilator →ₗ[R] R) w : ↥W.dualAnnihilator →ₗ[R] R) :
          (a : ↥W.dualAnnihilator) → R)
        (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ) :
      R)
    ((0 : (a : ↥W.dualAnnihilator) → R) (Subtype.mk (p := fun (x : Dual R M) ↦ x ∈ W.dualAnnihilator) φ hφ) : R)
Tactic: ext ⟨φ, hφ⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
h :
  Eq (α := (a : M) → R) ((fun (φ : ↥W.dualAnnihilator) ↦ ((⇑(↑φ : Dual R M) : (a : M) → R) : (a : M) → R)) φ)
    ((fun (φ : ↥W.dualAnnihilator) ↦ ((⇑(↑φ : Dual R M) : (a : M) → R) : (a : M) → R)) ψ)
⊢ φ = ψ
have a : ∀ (x : M), Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup M'
inst_4 : Module R M'
W : Submodule R M
φ ψ : ↥W.dualAnnihilator
h :
  Eq (α := (a : M) → R) ((fun (φ : ↥W.dualAnnihilator) ↦ ((⇑(↑φ : Dual R M) : (a : M) → R) : (a : M) → R)) φ)
    ((fun (φ : ↥W.dualAnnihilator) ↦ ((⇑(↑φ : Dual R M) : (a : M) → R) : (a : M) → R)) ψ)
x : M
⊢ Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)
have h₁ : ∀ (x : M), Eq.{u_1 + 1} (α := R) (((↑φ : Dual R M) : (a : M) → R) x : R) (((↑ψ : Dual R M) : (a : M) → R) x : R)
Tactic: simp only [funext_iff] at h
Cleared hypotheses: h