-- 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:
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

Tactic:
rw [range_subset_iff]

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
⊢ ∀ (y : ℕ), (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[y] (P.root j) ∈ range ⇑P.root

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 : ι
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

Tactic:
rw [coroot_root_eq_pairing, coroot_root_eq_pairing, ← hc, mul_comm, coxeterWeight]

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
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

Tactic:
rw [LinearIndependent.pair_iff] at hl

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
hl : ∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
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_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
⊢ ∀ (y : ℕ), (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[y] (P.root j) ∈ range ⇑P.root

Tactic:
intro n

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
n : ℕ
⊢ (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[n] (P.root j) ∈ range ⇑P.root

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

Tactic:
exact mem_image_of_mem _ (mem_range_self j)

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.pairing j i = 0 ∧ -2 = 0
⊢ (P.toLin.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j

Tactic:
simp only [neg_smul, neg_eq_zero, two_ne_zero (α := R), and_false, imp_false] at hl

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.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
hl : ∀ (s t : R), s • P.root i + t • P.root j = 0 → s = 0 ∧ t = 0
hc : P.coxeterWeight i j = 4
⊢ (P.toLin.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j

Tactic:
specialize hl (P.pairing j i) (-2)

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 = 0 ∧ -2 = 0
⊢ (P.toLin.flip (P.coroot i)) (P.root j) • P.root i ≠ 2 • P.root j

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

Tactic:
rw [← IsFixedPt.image_iterate ((bijOn_reflection_of_mapsTo (P.coroot_root_two i)
  (P.mapsTo_reflection_root i)).comp (bijOn_reflection_of_mapsTo (P.coroot_root_two j)
  (P.mapsTo_reflection_root j))).image_eq n]

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
n : ℕ
⊢ (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯))^[n] (P.root j) ∈
    (⇑(Module.reflection ⋯) ∘ ⇑(Module.reflection ⋯))^[n] '' range ⇑P.root