-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma smul_coroot_eq_of_root_eq_smul [Finite ι] [NoZeroSMulDivisors ℤ N] (i j : ι) (t : R)
    (h : P.root j = t • P.root i) :
    t • P.coroot j = P.coroot i

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
⊢ (P.root' i) (P.coroot i) = 2

Tactic:
simp

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
⊢ MapsTo (⇑(preReflection (t • P.coroot j) (P.root' i))) (range ⇑P.coroot) (range ⇑P.coroot)

Tactic:
convert P.mapsTo_coreflection_coroot j

Result:
case h.e'_3
ι : 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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
⊢ ⇑(preReflection (t • P.coroot j) (P.root' i)) = ⇑(P.coreflection j)

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
⊢ t • P.coroot j = P.coroot i

Tactic:
have hij : t * P.pairing i j = 2 := by simpa using ((P.coroot' j).congr_arg h).symm

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
⊢ t • P.coroot j = P.coroot i

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
⊢ t * P.pairing i j = 2

Tactic:
simpa using ((P.coroot' j).congr_arg h).symm

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x : N
⊢ P.root' j = t • P.root' i

Tactic:
ext

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x x✝ : N
⊢ (P.root' j) x✝ = (t • P.root' i) x✝

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
⊢ t • P.coroot j = P.coroot i

Tactic:
refine Module.eq_of_mapsTo_reflection_of_mem (f := P.root' i) (g := P.root' i)
  (finite_range P.coroot) (by simp [hij]) (by simp) (by simp [hij]) (by simp) ?_
  (P.mapsTo_coreflection_coroot i) (mem_range_self i)

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
⊢ MapsTo (⇑(preReflection (t • P.coroot j) (P.root' i))) (range ⇑P.coroot) (range ⇑P.coroot)

Proof state:
case h.e'_3.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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x : N
⊢ (preReflection (t • P.coroot j) (P.root' i)) x = (P.coreflection j) x

Tactic:
replace h : P.root' j = t • P.root' i := by ext; simp [h, root']

Result:
case h.e'_3.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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
hij : t * P.pairing i j = 2
x : N
h : P.root' j = t • P.root' i
⊢ (preReflection (t • P.coroot j) (P.root' i)) x = (P.coreflection j) x

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
⊢ (P.root' i) (t • P.coroot j) = 2

Tactic:
simp [hij]

Result:
no goals

Proof state:
case h.e'_3
ι : 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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
⊢ ⇑(preReflection (t • P.coroot j) (P.root' i)) = ⇑(P.coreflection j)

Tactic:
ext x

Result:
case h.e'_3.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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x : N
⊢ (preReflection (t • P.coroot j) (P.root' i)) x = (P.coreflection j) x

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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
h : P.root j = t • P.root i
hij : t * P.pairing i j = 2
x x✝ : N
⊢ (P.root' j) x✝ = (t • P.root' i) x✝

Tactic:
simp [h, root']

Result:
no goals

Proof state:
case h.e'_3.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
inst✝¹ : Finite ι
inst✝ : NoZeroSMulDivisors ℤ N
i j : ι
t : R
hij : t * P.pairing i j = 2
x : N
h : P.root' j = t • P.root' i
⊢ (preReflection (t • P.coroot j) (P.root' i)) x = (P.coreflection j) x

Tactic:
simp [Module.preReflection_apply, coreflection_apply, h, smul_comm _ t, mul_smul]

Result:
no goals