-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma coe_rootSpan_dualAnnihilator_map :
    P.rootSpan.dualAnnihilator.map P.toDualRight.symm = {x | ∀ i, P.root' i x = 0}

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : N
⊢ x ∈ ⇑P.toDualRight.toEquiv.symm '' {f | range ⇑P.root ⊆ ↑(LinearMap.ker f)} ↔ x ∈ {x | ∀ (i : ι), (P.root' i) x = 0}

Tactic:
rw [← Equiv.setOf_apply_symm_eq_image_setOf, Equiv.symm_symm]

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : N
⊢ x ∈ {b | range ⇑P.root ⊆ ↑(LinearMap.ker (P.toDualRight.toEquiv b))} ↔ x ∈ {x | ∀ (i : ι), (P.root' i) x = 0}

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : N
⊢ x ∈ ↑(Submodule.map P.toDualRight.symm P.rootSpan.dualAnnihilator) ↔ x ∈ {x | ∀ (i : ι), (P.root' i) x = 0}

Tactic:
rw [rootSpan, Submodule.map_coe, Submodule.coe_dualAnnihilator_span]

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : N
⊢ x ∈ ⇑P.toDualRight.symm '' {f | range ⇑P.root ⊆ ↑(LinearMap.ker f)} ↔ x ∈ {x | ∀ (i : ι), (P.root' i) x = 0}

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : N
⊢ x ∈ ⇑P.toDualRight.symm '' {f | range ⇑P.root ⊆ ↑(LinearMap.ker f)} ↔ x ∈ {x | ∀ (i : ι), (P.root' i) x = 0}

Tactic:
change x ∈ P.toDualRight.toEquiv.symm '' _ ↔ _

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : N
⊢ x ∈ ⇑P.toDualRight.toEquiv.symm '' {f | range ⇑P.root ⊆ ↑(LinearMap.ker f)} ↔ x ∈ {x | ∀ (i : ι), (P.root' i) x = 0}

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : N
⊢ x ∈ {b | range ⇑P.root ⊆ ↑(LinearMap.ker (P.toDualRight.toEquiv b))} ↔ x ∈ {x | ∀ (i : ι), (P.root' i) x = 0}

Tactic:
simp [Set.range_subset_iff]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
⊢ ↑(Submodule.map P.toDualRight.symm P.rootSpan.dualAnnihilator) = {x | ∀ (i : ι), (P.root' i) x = 0}

Tactic:
ext x

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
x : N
⊢ x ∈ ↑(Submodule.map P.toDualRight.symm P.rootSpan.dualAnnihilator) ↔ x ∈ {x | ∀ (i : ι), (P.root' i) x = 0}