awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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
by_contra! : ∀ (contra : ℵ₀ ≤ Module.rank K V), False
⊢ Module.rank K V < ℵ₀

Tactic:
by_contra! contra
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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))
⊢ 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)))

Tactic:
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 _ _)
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)))
⊢ 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

Premises used: Cardinal.lift_id', Cardinal.lift_umax
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)))
this₁ : Module.rank K (Dual K (Dual K V)) < Module.rank K (Dual K (Dual K V))
⊢ 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)))

Tactic:
rw [← lift_umax, heq, lift_id'] at this

Premises used: Cardinal.lift_id', Cardinal.lift_umax
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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 : Module.rank K (Dual K (Dual 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

Tactic:
lt_irrefl _ this

Premises used: lt_irrefl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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 : Module.rank K (Dual K (Dual 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

Tactic:
exact lt_irrefl _ this

Premises used: lt_irrefl
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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
suffices : lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))
⊢ False

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
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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 V)

Tactic:
have h₁ : lift (Module.rank K V) < Module.rank K (Dual K V) := lift_rank_lt_rank_dual contra
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
h : Module.rank K (Dual K V) = lift.{u_4, max u_4 u_5} (Module.rank K (Dual K V))
⊢ Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V))

Tactic:
convert! lift_rank_lt_rank_dual <| le_trans (by simpa) h₁.le

Premises used: LT.lt.le, lift_rank_lt_rank_dual, le_trans
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
h h₂ : Module.rank K (Dual 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))

Tactic:
rw [lift_id']

Premises used: Cardinal.lift_id'
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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))

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']
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
h₂ : Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V))
⊢ lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))

Tactic:
lt_trans h₁ h₂

Premises used: lt_trans
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
h₂ : Module.rank K (Dual K V) < Module.rank K (Dual K (Dual K V))
⊢ lift.{u_4, u_5} (Module.rank K V) < Module.rank K (Dual K (Dual K V))

Tactic:
exact lt_trans h₁ h₂

Premises used: lt_trans
-- 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 : 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)) ⊥
rw₃ rw₄ : Eq.{u_2 + 1} (α := Submodule R M) ⊥ ⊥
⊢ Eq.{u_2 + 1} (α := Submodule R M) (dualCoannihilator ⊤) ⊥

Tactic:
rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]

Premises used: Submodule.dualCoannihilator, Module.eval_ker, Submodule.dualAnnihilator_top, Submodule.comap_bot
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
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 = ⊥
⊢ ∃ (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
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
hf : Ne.{u_3 + 1} (α := R) ((f : (a : M ⧸ p) → R) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) : R) (0 : R)
⊢ map (f ∘ₗ p.mkQ) p = ⊥

Tactic:
simp [Submodule.map_comp]

Premises used: Submodule.map_comp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
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:
exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
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)
⊢ ∃ (f : Dual R M), Ne.{u_3 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R) ∧ map f p = ⊥

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]⟩
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
⊢ ¬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

Premises used: Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
hx₁ : ¬Eq (α := M ⧸ p) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) (0 : M ⧸ p)
⊢ Projective.{u_3, u_4} R (M ⧸ p)

Tactic:
rw [← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply] at hx

Premises used: Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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 : ¬Eq (α := M ⧸ p) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) (0 : M ⧸ 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)

Tactic:
Projective.exists_dual_ne_zero R hx

Premises used: Module.Projective.exists_dual_ne_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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 : ¬Eq (α := M ⧸ p) ((p.mkQ : (a : M) → M ⧸ p) x : M ⧸ p) (0 : M ⧸ 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)

Tactic:
exact Projective.exists_dual_ne_zero R hx

Premises used: Module.Projective.exists_dual_ne_zero
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
⊢ p ≠ ⊤

Tactic:
rw [lt_top_iff_ne_top] at hp

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
hp₁ : p ≠ ⊤
⊢ Projective.{u_3, u_4} R (M ⧸ p)

Tactic:
rw [lt_top_iff_ne_top] at hp

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
contrapose! : ∀ (hp : ∀ (x : M), x ∈ p), p = ⊤
⊢ ∃ (x : M), x ∉ p

Tactic:
contrapose! hp
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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
h : ∀ (x : M), x ∈ p ↔ Membership.mem (γ := Submodule R M) ⊤ x
⊢ p = ⊤

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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
x : M
⊢ x ∈ p ↔ Membership.mem (γ := Submodule R M) ⊤ x

Tactic:
simp [hp]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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)
obtain : ∀ (x : M) (hx : x ∉ p), ∃ (f : Dual R M), f ≠ 0 ∧ map f 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]
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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
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 = ⊥
⊢ ∃ (f : Dual R M), f ≠ 0 ∧ map f p = ⊥

Tactic:
obtain ⟨f, hf, hf'⟩ := p.exists_dual_map_eq_bot_of_notMem hx hp'

Premises used: Submodule.exists_dual_map_eq_bot_of_notMem
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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
hf : Ne.{u_3 + 1} (α := R) ((f : (a : M) → R) x : R) (0 : R)
hf' : map f p = ⊥
⊢ f ≠ 0

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Dual.Lemmas
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
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:
exact ⟨f, by aesop, hf'⟩
-- 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)
by_contra! : ∀ (hn : Ne (α := Submodule R (M →ₗ[R] R)) (span R s) ⊤), False
⊢ Eq (α := Submodule R (M →ₗ[R] R)) (span R s) ⊤

Tactic:
by_contra! hn
-- 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) ⊤
obtain : ∀ (φ : Dual R (M →ₗ[R] R)) (φne : φ ≠ 0) (hφ : map φ (span R s) = ⊥), False
⊢ False

Tactic:
obtain ⟨φ, φne, hφ⟩ := exists_dual_map_eq_bot_of_lt_top hn.lt_top inferInstance

Premises used: inferInstance, Submodule.exists_dual_map_eq_bot_of_lt_top, Ne.lt_top
-- 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) φ
f : M →ₗ[R] R
hf : f ∈ s
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)
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : M) → R) φs : R) (0 : R)

Tactic:
rw [← mem_bot R, ← hφ, mem_map]

Premises used: Submodule.mem_bot, Submodule.mem_map
-- 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) φ
f : M →ₗ[R] R
hf : f ∈ s
⊢ ∃ (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:
⟨f, subset_span hf, (apply_evalEquiv_symm_apply R M f φ).symm⟩

Premises used: Module.apply_evalEquiv_symm_apply, And.intro, Exists.intro, Submodule.subset_span, Eq.symm
-- 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) φ
f : M →ₗ[R] R
hf : f ∈ s
⊢ ∃ (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:
exact ⟨f, subset_span hf, (apply_evalEquiv_symm_apply R M f φ).symm⟩
-- 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) φ
⊢ ∀ (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⟩
-- 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)
⊢ φs ≠ 0

Tactic:
simp [φne, φs]