awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
K_1 : Type uK
V_1 : Type uV
inst : CommSemiring K_1
inst_1 : AddCommMonoid V_1
inst_2 : Module K_1 V_1
inst_3 : Projective K_1 V_1
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
K : Type u_4
V : Type u_5
inst_10 : Field K
inst_11 : AddCommGroup V
inst_12 : Module K V
inst_13 : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
this : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
heq : lift.{max u_5 u_4, u_5} (Module.rank K V) = lift.{u_5, max u_5 u_4} (Module.rank K (Dual K (Dual K V)))
⊢ False
have this₁ : Module.rank K (Dual K (Dual K V)) < Module.rank K (Dual K (Dual K V))
Tactic: rw [← lift_umax, heq, lift_id'] at this
Cleared hypotheses: this, heq
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K_1 : Type uK
V_1 : Type uV
inst : CommSemiring K_1
inst_1 : AddCommMonoid V_1
inst_2 : Module K_1 V_1
inst_3 : Projective K_1 V_1
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
K : Type u_4
V : Type u_5
inst_10 : Field K
inst_11 : AddCommGroup V
inst_12 : Module K V
inst_13 : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
⊢ False
have suffices : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
Tactic: suffices lift (Module.rank K V) < Module.rank K (Dual K (Dual K V)) by
    have heq := lift_rank_eq_of_equiv_equiv (R := K) (R' := K) (M := V) (M' := Dual K (Dual K V))
      (ZeroHom.id K) (evalEquiv K V) bijective_id (fun r v ↦ (evalEquiv K V).map_smul _ _)
    rw [← lift_umax, heq, lift_id'] at this
    exact lt_irrefl _ this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
K_1 : Type uK
V_1 : Type uV
inst : CommSemiring K_1
inst_1 : AddCommMonoid V_1
inst_2 : Module K_1 V_1
inst_3 : Projective K_1 V_1
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
K : Type u_4
V : Type u_5
inst_10 : Field K
inst_11 : AddCommGroup V
inst_12 : Module K V
inst_13 : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
⊢ lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
have h₁ : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K V)
Tactic: have h₁ : lift (Module.rank K V) < Module.rank K (Dual K V) := lift_rank_lt_rank_dual contra
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K_1 : Type uK
V_1 : Type uV
inst : CommSemiring K_1
inst_1 : AddCommMonoid V_1
inst_2 : Module K_1 V_1
inst_3 : Projective K_1 V_1
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
K : Type u_4
V : Type u_5
inst_10 : Field K
inst_11 : AddCommGroup V
inst_12 : Module K V
inst_13 : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
h₁ : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K V)
⊢ Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V))
have h : Module.rank K (Dual K V) = lift.{u_4, max u_4 u_5} (Module.rank K (Dual K V))
Tactic: convert! lift_rank_lt_rank_dual <| le_trans (by simpa) h₁.le
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
K_1 : Type uK
V_1 : Type uV
inst : CommSemiring K_1
inst_1 : AddCommMonoid V_1
inst_2 : Module K_1 V_1
inst_3 : Projective K_1 V_1
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
K : Type u_4
V : Type u_5
inst_10 : Field K
inst_11 : AddCommGroup V
inst_12 : Module K V
inst_13 : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
h₁ : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K V)
⊢ Module.rank K (Dual K V) = lift.{u_4, max u_4 u_5} (Module.rank K (Dual K V))
have h : Module.rank K (Dual K V) = Module.rank K (Dual K V)
Tactic: rw [lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
K_1 : Type uK
V_1 : Type uV
inst : CommSemiring K_1
inst_1 : AddCommMonoid V_1
inst_2 : Module K_1 V_1
inst_3 : Projective K_1 V_1
R : Type u_1
M : Type u_2
N : Type u_3
inst_4 : CommSemiring R
inst_5 : AddCommMonoid M
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R N
inst_9 : IsReflexive R M
K : Type u_4
V : Type u_5
inst_10 : Field K
inst_11 : AddCommGroup V
inst_12 : Module K V
inst_13 : IsReflexive K V
contra : ℵ₀ ≤ Module.rank K V
h₁ : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K V)
⊢ lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
have h₂ : Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V))
Tactic: have h₂ : Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V)) := by
    convert! lift_rank_lt_rank_dual <| le_trans (by simpa) h₁.le
    rw [lift_id']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Projective R M
⊢ Eq.{u_2 + 1} (α := Submodule R M) (dualCoannihilator ⊤) ⊥
have rw : Eq (α := Submodule R M) (comap (Dual.eval R M) (dualAnnihilator ⊤)) ⊥
Tactic: rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Projective R M
rw : Eq (α := Submodule R M) (comap (Dual.eval R M) (dualAnnihilator ⊤)) ⊥
⊢ Eq.{u_2 + 1} (α := Submodule R M) (dualCoannihilator ⊤) ⊥
have rw₁ : Eq (α := Submodule R M) (comap (Dual.eval R M) ⊥) ⊥
Tactic: rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Projective R M
rw : Eq (α := Submodule R M) (comap (Dual.eval R M) (dualAnnihilator ⊤)) ⊥
rw₁ : Eq (α := Submodule R M) (comap (Dual.eval R M) ⊥) ⊥
⊢ Eq.{u_2 + 1} (α := Submodule R M) (dualCoannihilator ⊤) ⊥
have rw₂ : Eq (α := Submodule R M) (LinearMap.ker (Dual.eval R M)) ⊥
Tactic: rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Projective R M
rw : Eq (α := Submodule R M) (comap (Dual.eval R M) (dualAnnihilator ⊤)) ⊥
rw₁ : Eq (α := Submodule R M) (comap (Dual.eval R M) ⊥) ⊥
rw₂ : Eq (α := Submodule R M) (LinearMap.ker (Dual.eval R M)) ⊥
⊢ Eq.{u_2 + 1} (α := Submodule R M) (dualCoannihilator ⊤) ⊥
have rw₃ : Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊥
Tactic: rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective.{u_3, u_4} R (M ⧸ p)
this :
  ∃ (f : Dual.{u_3, u_4} R (M ⧸ p)),
    Ne.{u_3 + 1} (α := R) ((f : (a : M ⧸ p) → R) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) : R) (0 : R)
⊢ ∃ (f : Dual R M), Ne.{u_3 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R) ∧ map f p = ⊥
have obtain : ∀ (f : Dual.{u_3, u_4} R (M ⧸ p))
  (hf : Ne.{u_3 + 1} (α := R) ((f : (a : M ⧸ p) → R) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) : R) (0 : R)),
  ∃ (f : Dual R M), Ne.{u_3 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R) ∧ map f p = ⊥
Tactic: obtain ⟨f, hf⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective.{u_3, u_4} R (M ⧸ p)
⊢ ∃ (f : Dual R M), Ne.{u_3 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R) ∧ map f p = ⊥
have suffices : ∃ (f : Dual.{u_3, u_4} R (M ⧸ p)),
  Ne.{u_3 + 1} (α := R) ((f : (a : M ⧸ p) → R) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) : R) (0 : R)
Tactic: suffices ∃ f : Dual R (M ⧸ p), f (p.mkQ x) ≠ 0 by
    obtain ⟨f, hf⟩ := this; exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective.{u_3, u_4} R (M ⧸ p)
⊢ ∃ (f : Dual.{u_3, u_4} R (M ⧸ p)),
    Ne.{u_3 + 1} (α := R) ((f : (a : M ⧸ p) → R) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) : R) (0 : R)
have hx₁ : ¬Eq (α := M ⧸ p) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) (0 : M ⧸ p)
Tactic: rw [← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply] at hx
Cleared hypotheses: hx, hp'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Projective.{u_3, u_4} R (M ⧸ p)
⊢ ∃ (x : M), x ∉ p
have hp₁ : p ≠ ⊤
Tactic: rw [lt_top_iff_ne_top] at hp
Cleared hypotheses: hp, hp'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
hp : p ≠ ⊤
hp' : Projective.{u_3, u_4} R (M ⧸ p)
⊢ ∃ (x : M), x ∉ p
have contrapose! : ∀ (hp : ∀ (x : M), x ∈ p), p = ⊤
Tactic: contrapose! hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
hp' : Projective.{u_3, u_4} R (M ⧸ p)
hp : ∀ (x : M), x ∈ p
⊢ p = ⊤
have h : ∀ (x : M), x ∈ p ↔ Membership.mem (γ := Submodule R M) ⊤ x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Projective.{u_3, u_4} R (M ⧸ p)
⊢ ∃ (f : Dual R M), f ≠ 0 ∧ map f p = ⊥
have obtain : ∀ (x : M) (hx : x ∉ p), ∃ (f : Dual R M), f ≠ 0 ∧ map f p = ⊥
Tactic: obtain ⟨x, hx⟩ : ∃ x : M, x ∉ p := by rw [lt_top_iff_ne_top] at hp; contrapose! hp; ext; simp [hp]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Projective.{u_3, u_4} R (M ⧸ p)
x : M
hx : x ∉ p
⊢ ∃ (f : Dual R M), f ≠ 0 ∧ map f p = ⊥
have obtain : ∀ (f : Dual R M) (hf : Ne.{u_3 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)) (hf' : map f p = ⊥),
  ∃ (f : Dual R M), f ≠ 0 ∧ map f p = ⊥
Tactic: obtain ⟨f, hf, hf'⟩ := p.exists_dual_map_eq_bot_of_notMem hx hp'
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ Eq (α := Submodule R (M →ₗ[R] R)) (span R s) ⊤
have by_contra! : ∀ (hn : Ne (α := Submodule R (M →ₗ[R] R)) (span R s) ⊤), False
Tactic: by_contra! hn
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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) ⊤
⊢ False
have obtain : ∀ (φ : Dual R (M →ₗ[R] R)) (φne : φ ≠ 0) (hφ : map φ (span R s) = ⊥), False
Tactic: obtain ⟨φ, φne, hφ⟩ := exists_dual_map_eq_bot_of_lt_top hn.lt_top inferInstance
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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) φ
f : M →ₗ[R] R
hf : f ∈ s
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) φs : R) (0 : R)
have rw : ∃ (y : M →ₗ[R] R),
  Membership.mem (γ := Submodule R (M →ₗ[R] R)) (span R s) y ∧
    Eq.{u_1 + 1} (α := R) ((φ : (a : M →ₗ[R] R) → R) y : R) ((f : (a : M) → R) φs : R)
Tactic: rw [← mem_bot R, ← hφ, mem_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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) φ
⊢ False
have this : ∀ (f : M →ₗ[R] R) (hf : f ∈ s), Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) φs : R) (0 : R)
Tactic: have this f (hf : f ∈ s) : f φs = 0 := by
    rw [← mem_bot R, ← hφ, mem_map]
    exact ⟨f, subset_span hf, (apply_evalEquiv_symm_apply R M f φ).symm⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (goal)
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)
⊢ False
have obtain : ∀ (x : M →ₗ[R] R) (xs : x ∈ s) (hx : Ne.{u_1 + 1} (α := R) ((x : (a : M) → R) φs : R) (0 : R)), False
Tactic: obtain ⟨x, xs, hx⟩ := h φs (by simp [φne, φs])
-- 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 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K
have by_contra : ∀ (hK : K ∉ span 𝕜 (Set.range L)), False
Tactic: by_contra hK
-- 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 : FiniteDimensional 𝕜 E
L : ι → E →ₗ[𝕜] 𝕜
K : E →ₗ[𝕜] 𝕜
h : ⨅ (i : ι), (L i).ker ≤ K.ker
hK : K ∉ span 𝕜 (Set.range L)
⊢ False
have rcases : ∀ (φ : Dual 𝕜 (E →ₗ[𝕜] 𝕜)) (φne : Ne.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) K : 𝕜) (0 : 𝕜))
  (hφ : map φ (span 𝕜 (Set.range L)) = ⊥), False
Tactic: rcases exists_dual_map_eq_bot_of_notMem hK inferInstance with ⟨φ, φne, 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 : 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 : 𝕜)
have refine : ∀ (i : ι), Membership.mem.{u_4, u_4} (α := 𝕜) (γ := Submodule 𝕜 𝕜) ⊥ ((L i : (a : E) → 𝕜) φs : 𝕜)
Tactic: refine h <| (Submodule.mem_iInf _).2 fun i ↦ (mem_bot 𝕜).1 ?_
-- 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 : 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 : ι
⊢ Membership.mem.{u_4, u_4} (α := 𝕜) (γ := Submodule 𝕜 𝕜) ⊥ ((L i : (a : E) → 𝕜) φs : 𝕜)
have rw : ∃ (y : E →ₗ[𝕜] 𝕜),
  Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) y ∧
    Eq.{u_4 + 1} (α := 𝕜) ((φ : (a : E →ₗ[𝕜] 𝕜) → 𝕜) y : 𝕜) ((L i : (a : E) → 𝕜) φs : 𝕜)
Tactic: rw [← hφ, Submodule.mem_map]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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) φ
⊢ False
have this : 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⟩
-- 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
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K
have have : ∀ (x : Fintype ι), Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K
Tactic: have _ := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K
have p_eq : p = φ.ker
Tactic: have p_eq : p = ker φ := (ker_pi L).symm
-- 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
⊢ ⨅ (i : ι), (L' i).ker ≤ K'.ker
have simp_rw : ⊥ ≤ (liftQ (⨅ (i : ι), (L i).ker) K h).ker
Tactic: simp_rw +zetaDelta [← ker_pi, pi_liftQ_eq_liftQ_pi, ker_liftQ_eq_bot' p φ p_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Dual.Lemmas (hypothesis)
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
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K
have this : ⨅ (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
-- 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
⊢ Membership.mem (γ := Submodule 𝕜 (E →ₗ[𝕜] 𝕜)) (span 𝕜 (Set.range L)) K
have obtain : ∀ (c : ι → 𝕜) (hK' : ∑ i : ι, c i • L' i = 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)
-- 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 enter : fun (i : ι) ↦ c i • L i
Tactic: enter [2]
-- 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₁ : c i • p.liftQ (L i) sorry ∘ₗ p.mkQ
Tactic: rw [← p.liftQ_mkQ (L i) (iInf_le _ i)]