-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma reflection_perm_eq_reflection_perm_iff_of_span :
    P.reflection_perm i = P.reflection_perm j ↔
    ∀ x ∈ span R (range P.root), P.reflection i x = P.reflection j x

Proof state:
case refine_2.H.a
ι : 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
i j : ι
h : ∀ x ∈ span R (range ⇑P.root), (P.reflection i) x = (P.reflection j) x
k : ι
⊢ P.root ((P.reflection_perm i) k) = P.root ((P.reflection_perm j) k)

Tactic:
simp [h (P.root k) (Submodule.subset_span <| mem_range_self k)]

Result:
no goals

Proof state:
case refine_1.smul
ι : 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
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x✝ : M
t : R
x : M
hx✝ : x ∈ span R (range ⇑P.root)
hx : (P.reflection i) x = (P.reflection j) x
⊢ (P.reflection i) (t • x) = (P.reflection j) (t • x)

Tactic:
simp [hx]

Result:
no goals

Proof state:
case refine_2.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
i j : ι
h : ∀ x ∈ span R (range ⇑P.root), (P.reflection i) x = (P.reflection j) x
k : ι
⊢ (P.reflection_perm i) k = (P.reflection_perm j) k

Tactic:
apply P.root.injective

Result:
case refine_2.H.a
ι : 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
i j : ι
h : ∀ x ∈ span R (range ⇑P.root), (P.reflection i) x = (P.reflection j) x
k : ι
⊢ P.root ((P.reflection_perm i) k) = P.root ((P.reflection_perm j) k)

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
i j : ι
⊢ P.reflection_perm i = P.reflection_perm j ↔ ∀ x ∈ span R (range ⇑P.root), (P.reflection i) x = (P.reflection j) x

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

Result:
case refine_1
ι : 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
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x : M
hx : x ∈ span R (range ⇑P.root)
⊢ (P.reflection i) x = (P.reflection j) x

case refine_2
ι : 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
i j : ι
h : ∀ x ∈ span R (range ⇑P.root), (P.reflection i) x = (P.reflection j) x
⊢ P.reflection_perm i = P.reflection_perm j

Proof state:
case refine_1.mem
ι : 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
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x✝ x : M
hx : x ∈ range ⇑P.root
⊢ (P.reflection i) x = (P.reflection j) x

Tactic:
obtain ⟨k, rfl⟩ := hx

Result:
case refine_1.mem.intro
ι : 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
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x : M
k : ι
⊢ (P.reflection i) (P.root k) = (P.reflection j) (P.root k)

Proof state:
case refine_1.zero
ι : 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
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.reflection i) 0 = (P.reflection j) 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.add
ι : 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
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x✝ x y : M
hx✝ : x ∈ span R (range ⇑P.root)
hy✝ : y ∈ span R (range ⇑P.root)
hx : (P.reflection i) x = (P.reflection j) x
hy : (P.reflection i) y = (P.reflection j) y
⊢ (P.reflection i) (x + y) = (P.reflection j) (x + y)

Tactic:
simp [hx, hy]

Result:
no goals

Proof state:
case refine_1.mem.intro
ι : 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
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x : M
k : ι
⊢ (P.reflection i) (P.root k) = (P.reflection j) (P.root k)

Tactic:
simp only [← root_reflection_perm, h]

Result:
no goals

Proof state:
case refine_2
ι : 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
i j : ι
h : ∀ x ∈ span R (range ⇑P.root), (P.reflection i) x = (P.reflection j) x
⊢ P.reflection_perm i = P.reflection_perm j

Tactic:
ext k

Result:
case refine_2.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
i j : ι
h : ∀ x ∈ span R (range ⇑P.root), (P.reflection i) x = (P.reflection j) x
k : ι
⊢ (P.reflection_perm i) k = (P.reflection_perm j) k

Proof state:
case refine_1
ι : 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
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x : M
hx : x ∈ span R (range ⇑P.root)
⊢ (P.reflection i) x = (P.reflection j) x

Tactic:
induction hx using Submodule.span_induction with
| mem x hx =>
  obtain ⟨k, rfl⟩ := hx
  simp only [← root_reflection_perm, h]
| zero => simp
| add x y _ _ hx hy => simp [hx, hy]
| smul t x _ hx => simp [hx]

Result:
no goals