-- Mathlib/Algebra/Module/CharacterModule.lean
lemma surjective_of_dual_injective (f : A →ₗ[R] A') (hf : Function.Injective (dual f)) :
    Function.Surjective f

Proof state:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
a : A' ⧸ LinearMap.range f
c : CharacterModule (A' ⧸ LinearMap.range f)
⊢ c a = 0

Tactic:
obtain ⟨b, rfl⟩ := QuotientAddGroup.mk'_surjective _ a

Result:
case intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ LinearMap.range f)
b : A'
⊢ c ((QuotientAddGroup.mk' (LinearMap.range f).toAddSubgroup) b) = 0

Proof state:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
⊢ Function.Surjective ⇑f

Tactic:
rw [← LinearMap.range_eq_top, ← Submodule.unique_quotient_iff_eq_top]

Result:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
⊢ Nonempty (Unique (A' ⧸ LinearMap.range f))

Proof state:
case intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ LinearMap.range f)
b : A'
⊢ (dual (LinearMap.range f).mkQ) c = 0

Tactic:
refine hf ?_

Result:
case intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ LinearMap.range f)
b : A'
⊢ (dual f) ((dual (LinearMap.range f).mkQ) c) = (dual f) 0

Proof state:
case intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ LinearMap.range f)
b : A'
⊢ c ((QuotientAddGroup.mk' (LinearMap.range f).toAddSubgroup) b) = 0

Tactic:
suffices eq : dual (Submodule.mkQ _) c = 0 from congr($eq b)

Result:
case intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ LinearMap.range f)
b : A'
⊢ (dual (LinearMap.range f).mkQ) c = 0

Proof state:
case intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
c : CharacterModule (A' ⧸ LinearMap.range f)
b : A'
⊢ (dual f) ((dual (LinearMap.range f).mkQ) c) = (dual f) 0

Tactic:
rw [← LinearMap.comp_apply, ← dual_comp, LinearMap.range_mkQ_comp, dual_zero,
  LinearMap.zero_apply, dual_apply, AddMonoidHom.zero_comp]

Result:
no goals

Proof state:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
⊢ Nonempty (Unique (A' ⧸ LinearMap.range f))

Tactic:
refine ⟨Unique.mk inferInstance fun a ↦ eq_zero_of_character_apply fun c ↦ ?_⟩

Result:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
A' : Type u_1
inst✝² : AddCommGroup A'
inst✝¹ : Module R A
inst✝ : Module R A'
f : A →ₗ[R] A'
hf : Function.Injective ⇑(dual f)
a : A' ⧸ LinearMap.range f
c : CharacterModule (A' ⧸ LinearMap.range f)
⊢ c a = 0