-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma neg_mem_range_root_iff {x : M} :
    -x ∈ range P.root ↔ x ∈ range P.root

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
x : M
this : ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root
⊢ -x ∈ range ⇑P.root ↔ x ∈ range ⇑P.root

Tactic:
refine ⟨this x, fun h ↦ ?_⟩

Result:
ι : 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 : M
this : ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root
h : x ∈ range ⇑P.root
⊢ -x ∈ range ⇑P.root

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
x : M
this : ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root
h : - -x ∈ range ⇑P.root
⊢ -x ∈ range ⇑P.root

Tactic:
exact this (-x) h

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
x : M
⊢ -x ∈ range ⇑P.root ↔ x ∈ range ⇑P.root

Tactic:
suffices ∀ x : M, -x ∈ range P.root → x ∈ range P.root by
  refine ⟨this x, fun h ↦ ?_⟩
  rw [← neg_neg x] at h
  exact this (-x) h

Result:
ι : 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 : M
⊢ ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root

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
x : M
⊢ ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root

Tactic:
intro y ⟨i, hi⟩

Result:
ι : 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 y : M
i : ι
hi : P.root i = -y
⊢ y ∈ range ⇑P.root

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
x y : M
i : ι
hi : P.root i = -y
⊢ P.root ((P.reflection_perm i) i) = y

Tactic:
simp [neg_eq_iff_eq_neg.mpr hi]

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
x y : M
i : ι
hi : P.root i = -y
⊢ y ∈ range ⇑P.root

Tactic:
exact ⟨P.reflection_perm i i, by simp [neg_eq_iff_eq_neg.mpr hi]⟩

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
x : M
this : ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root
h : x ∈ range ⇑P.root
⊢ -x ∈ range ⇑P.root

Tactic:
rw [← neg_neg x] at h

Result:
ι : 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 : M
this : ∀ (x : M), -x ∈ range ⇑P.root → x ∈ range ⇑P.root
h : - -x ∈ range ⇑P.root
⊢ -x ∈ range ⇑P.root