-- Mathlib/LinearAlgebra/Dual.lean
theorem range_dualMap_eq_dualAnnihilator_ker_of_subtype_range_surjective (f : M →ₗ[R] M')
    (hf : Function.Surjective f.range.subtype.dualMap) :
    LinearMap.range f.dualMap = f.ker.dualAnnihilator

Proof state:
case h.e'_3.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ ker f = ker f.rangeRestrict

Tactic:
exact (ker_rangeRestrict f).symm

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
⊢ range f.dualMap = (ker f).dualAnnihilator

Tactic:
have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj

Result:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range f.dualMap = (ker f).dualAnnihilator

Proof state:
case h.e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range f.dualMap = range f.rangeRestrict.dualMap

Tactic:
calc
  _ = range ((range f).subtype.comp f.rangeRestrict).dualMap := by simp
  _ = _ := ?_

Result:
case h.e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range ((range f).subtype ∘ₗ f.rangeRestrict).dualMap = range f.rangeRestrict.dualMap

Proof state:
case h.e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range ((range f).subtype ∘ₗ f.rangeRestrict).dualMap = range f.rangeRestrict.dualMap

Tactic:
rw [← dualMap_comp_dualMap, range_comp_of_range_eq_top]

Result:
case h.e'_2.hf
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range (range f).subtype.dualMap = ⊤

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
⊢ range f.dualMap = (ker f).dualAnnihilator

Tactic:
have rr_surj : Function.Surjective f.rangeRestrict := by
  rw [← range_eq_top, range_rangeRestrict]

Result:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
⊢ range f.dualMap = (ker f).dualAnnihilator

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
⊢ Function.Surjective ⇑f.rangeRestrict

Tactic:
rw [← range_eq_top, range_rangeRestrict]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range f.dualMap = range ((range f).subtype ∘ₗ f.rangeRestrict).dualMap

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range f.dualMap = (ker f).dualAnnihilator

Tactic:
convert this using 1

Result:
case h.e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range f.dualMap = range f.rangeRestrict.dualMap

case h.e'_3
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ (ker f).dualAnnihilator = (ker f.rangeRestrict).dualAnnihilator

Proof state:
case h.e'_2.hf
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ range (range f).subtype.dualMap = ⊤

Tactic:
rwa [range_eq_top]

Result:
no goals

Proof state:
case h.e'_3
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ (ker f).dualAnnihilator = (ker f.rangeRestrict).dualAnnihilator

Tactic:
apply congr_arg

Result:
case h.e'_3.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ⇑(range f).subtype.dualMap
rr_surj : Function.Surjective ⇑f.rangeRestrict
this : range f.rangeRestrict.dualMap = (ker f.rangeRestrict).dualAnnihilator
⊢ ker f = ker f.rangeRestrict