R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
⊢ φ = ψ
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
⊢ Function.Injective ↑(dualMap f)
intro φ ψ h
case h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
x : M₂
⊢ ↑φ x = ↑ψ x
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
⊢ φ = ψ
ext x
case h.intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
y : M₁
⊢ ↑φ (↑f y) = ↑ψ (↑f y)
case h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
x : M₂
⊢ ↑φ x = ↑ψ x
obtain ⟨y, rfl⟩ := hf x
no goals
case h.intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
y : M₁
⊢ ↑φ (↑f y) = ↑ψ (↑f y)
exact congr_arg (fun g : Module.Dual R M₁ => g y) h