-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma infinite_of_linInd_coxeterWeight_four [NeZero (2 : R)] [NoZeroSMulDivisors ℤ M]
    (hl : LinearIndependent R ![P.root i, P.root j]) (hc : P.coxeterWeight i j = 4) :
    Infinite ι

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 : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ Infinite ι

Tactic:
refine (infinite_range_iff (Embedding.injective P.root)).mp (Infinite.mono ?_
  ((infinite_range_reflection_reflection_iterate_iff (P.coroot_root_two i)
  (P.coroot_root_two j) ?_).mpr ?_))

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 : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ (range fun n => (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[n] (P.root j)) ⊆ range ⇑P.root

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 : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ (P.toLin.flip (P.coroot i)) (P.root j) * (P.toLin.flip (P.coroot j)) (P.root i) = 4

case refine_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
i j : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hl : LinearIndependent R ![P.root i, P.root j]
hc : P.coxeterWeight i j = 4
⊢ (P.toLin.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j

Proof state:
case refine_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
i j : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hc : P.coxeterWeight i j = 4
hl : ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
⊢ ¬P.pairing j i • P.root i + -(2 • P.root j) = 0

Tactic:
exact hl

Result:
no goals

Proof state:
case refine_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
i j : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hc : P.coxeterWeight i j = 4
hl : ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
⊢ (P.toLin.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j

Tactic:
rw [ne_eq, coroot_root_eq_pairing, ← sub_eq_zero, sub_eq_add_neg]

Result:
case refine_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
i j : ι
inst✝¹ : NeZero 2
inst✝ : NoZeroSMulDivisors ℤ M
hc : P.coxeterWeight i j = 4
hl : ¬P.pairing j i • P.root i + -(2 • P.root j) = 0
⊢ ¬P.pairing j i • P.root i + -(2 • P.root j) = 0