awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
j : ι
hj :
  HSMul.hSMul (α := ℤ) (β := M) 1 ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul (α := ℤ) (β := M) (↑n : ℤ) ((P.root : (a : ι) → M) j : M)
⊢ Eq (α := ℤ) (↑n : ℤ) 1

Tactic:
rw [(smul_left_injective ℤ <| P.ne_zero j).eq_iff, eq_comm] at hj

Premises used: RootPairing.ne_zero, Function.Injective.eq_iff, smul_left_injective, Int, eq_comm
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
j : ι
hj : Eq (α := ℤ) (↑n : ℤ) 1
⊢ 2 ≤ n

Tactic:
have : 2 ≤ n := Nat.AtLeastTwo.prop
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
j : ι
hj : Eq (α := ℤ) (↑n : ℤ) 1
this : 2 ≤ n
⊢ False

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)
this : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) j : M) (-(P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (α := ℤ) (β := M) (-1) ((P.root : (a : ι) → M) i : M)

Tactic:
rw [← one_smul ℤ (P.root i), ← neg_smul, hj] at this

Premises used: neg_smul, Int, one_smul, RootPairing.root, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)
this :
  HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (α := ℤ) (β := M) (-1) ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (α := ℤ) (β := M) (↑n : ℤ) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (α := ℤ) (β := M) (-1) ((P.root : (a : ι) → M) i : M)

Tactic:
simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)
this :
  HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (α := ℤ) (β := M) (-1) ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (α := ℤ) (β := M) (↑n : ℤ) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (α := ℤ) (β := M) (-1) ((P.root : (a : ι) → M) i : M)

Tactic:
replace this : (n : ℤ) • P.root i = -1 • P.root i := by simpa
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)
this :
  HSMul.hSMul (α := ℤ) (β := M) (↑n : ℤ) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (α := ℤ) (β := M) (-1) ((P.root : (a : ι) → M) i : M)
⊢ Eq (α := ℤ) (↑n : ℤ) (-1)

Tactic:
rw [(smul_left_injective ℤ <| P.ne_zero i).eq_iff] at this

Premises used: RootPairing.ne_zero, Function.Injective.eq_iff, smul_left_injective, Int
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
n : ℕ
inst_8 : n.AtLeastTwo
i j : ι
hj : (P.root : (a : ι) → M) j = HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) i : M)
this : Eq (α := ℤ) (↑n : ℤ) (-1)
⊢ False

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
IsReduced.linearIndependent P (fun hij ↦ ?_) (fun hij ↦ P.zero_notMem_range_root ?_)

Premises used: RootPairing.zero_notMem_range_root, RootPairing.IsReduced.linearIndependent
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
refine_1 : ∀ (hij : i = j), False
refine_2 :
  ∀ (hij : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) 0
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
refine IsReduced.linearIndependent P (fun hij ↦ ?_) (fun hij ↦ P.zero_notMem_range_root ?_)

Premises used: RootPairing.zero_notMem_range_root, RootPairing.IsReduced.linearIndependent
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
hij : i = j
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) j : M))

Tactic:
rw [hij, ← two_smul (R := ℕ)] at h

Premises used: two_smul, Nat
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
hij : i = j
h₁ :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) j : M))
⊢ i = j

Tactic:
rw [hij, ← two_smul (R := ℕ)] at h

Premises used: two_smul, Nat
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) j : M))
hij : i = j
⊢ False

Tactic:
P.nsmul_notMem_range_root h

Premises used: RootPairing.nsmul_notMem_range_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSMul.hSMul (α := ℕ) (β := M) 2 ((P.root : (a : ι) → M) j : M))
hij : i = j
⊢ False

Tactic:
exact P.nsmul_notMem_range_root h

Premises used: RootPairing.nsmul_notMem_range_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
hij : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
refine_2 :
  ∀
    (h :
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
        (HAdd.hAdd (α := M) (β := M) (-(P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) j : M)))
    (hij : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) 0
refine_2₁ refine_2₂ refine_2₃ refine_2₄ :
  ∀ (h : Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) 0)
    (hij : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)),
    Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) 0
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) 0

Tactic:
rwa [hij, neg_add_cancel] at h

Premises used: neg_add_cancel
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
this :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι)] :
      Fin (Nat.succ 0).succ → M)
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
simpa using this
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
suffices :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι)] :
      Fin (Nat.succ 0).succ → M)
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
suffices LinearIndependent R ![P.root i, P.root (P.reflectionPerm j j)] by simpa using this
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
apply :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M)
      ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M))
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι)] :
      Fin (Nat.succ 0).succ → M)

Tactic:
apply P.linearIndependent_of_add_mem_range_root

Premises used: RootPairing.linearIndependent_of_add_mem_range_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsAddTorsionFree M
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M)
      ((P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) j : ι) : M))

Tactic:
simpa [sub_eq_add_neg] using h

Premises used: sub_eq_add_neg
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  have : IsAddTorsionFree M := .of_isTorsionFree R M
  P.linearIndependent_of_add_mem_range_root h

Premises used: RootPairing.toLinearMap, RootPairing.linearIndependent_of_add_mem_range_root, Module.IsReflexive.of_isPerfPair, IsAddTorsionFree.of_isTorsionFree
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : CharZero R
inst_6 : IsDomain R
inst_7 : P.IsReduced
i j : ι
h :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))
⊢ LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)

Tactic:
have : IsReflexive R M := .of_isPerfPair P.toLinearMap
  have : IsAddTorsionFree M := .of_isTorsionFree R M
  P.linearIndependent_of_sub_mem_range_root h

Premises used: RootPairing.toLinearMap, Module.IsReflexive.of_isPerfPair, IsAddTorsionFree.of_isTorsionFree, RootPairing.linearIndependent_of_sub_mem_range_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
hc : P.coxeterWeight i j = 4
⊢ Infinite ι

Tactic:
(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 ?_))

Premises used: Iff.mpr, Set.Infinite.mono, Set.infinite_range_iff, Module.infinite_range_reflection_reflection_iterate_iff, RootPairing.coroot_root_two, RootPairing.root, Iff.mp, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
hc : P.coxeterWeight i j = 4
refine_1 :
  Subset.{u_3} (α := Set M)
    (range fun (n : ℕ) ↦ (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯) : (a : M) → M)^[n] ((P.root : (a : ι) → M) j))
    (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
refine_2 :
  HMul.hMul (α := R) (β := R)
      ((((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
      ((((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) i : M) :
        R) =
    4
refine_3 :
  HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M)
      ((((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
      ((P.root : (a : ι) → M) i : M) ≠
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ 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 ?_))

Premises used: Iff.mpr, Set.Infinite.mono, Set.infinite_range_iff, Module.infinite_range_reflection_reflection_iterate_iff, RootPairing.coroot_root_two, RootPairing.root, Iff.mp, Function.Embedding.injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
hc : P.coxeterWeight i j = 4
refine_1 :
  ∀ (y : ℕ),
    Membership.mem (α := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
      ((⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯) : (a : M) → M)^[y] ((P.root : (a : ι) → M) j) : M)
⊢ Subset.{u_3} (α := Set M)
    (range fun (n : ℕ) ↦ (⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯) : (a : M) → M)^[n] ((P.root : (a : ι) → M) j))
    (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))

Tactic:
rw [range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
hc : P.coxeterWeight i j = 4
n : ℕ
refine_1 :
  Membership.mem (α := M) (γ := Set M)
    ((comp (β := M) (⇑(Module.reflection ⋯) : (a : M) → M) (⇑(Module.reflection ⋯) : (a : M) → M))^[n] ''
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    ((⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯) : (a : M) → M)^[n] ((P.root : (a : ι) → M) j) : M)
⊢ Membership.mem (α := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    ((⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯) : (a : M) → M)^[n] ((P.root : (a : ι) → M) j) : M)

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]

Premises used: Module.bijOn_reflection_of_mapsTo, RootPairing.mapsTo_reflection_root, Set.BijOn.comp, Set.BijOn.image_eq, RootPairing.coroot_root_two, Function.IsFixedPt.image_iterate
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
hc : P.coxeterWeight i j = 4
n : ℕ
⊢ Membership.mem (α := M) (γ := Set M)
    ((comp (β := M) (⇑(Module.reflection ⋯) : (a : M) → M) (⇑(Module.reflection ⋯) : (a : M) → M))^[n] ''
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    ((⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯) : (a : M) → M)^[n] ((P.root : (a : ι) → M) j) : M)

Tactic:
mem_image_of_mem _ (mem_range_self j)

Premises used: Set.mem_range_self, Set.Mem, Set.mem_image_of_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.Reduced
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
i j : ι
inst_5 : NeZero.{u_2} (R := R) 2
inst_6 : IsAddTorsionFree M
hl :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i, (P.root : (a : ι) → M) j] : Fin (Nat.succ 0).succ → M)
hc : P.coxeterWeight i j = 4
n : ℕ
⊢ Membership.mem (α := M) (γ := Set M)
    ((comp (β := M) (⇑(Module.reflection ⋯) : (a : M) → M) (⇑(Module.reflection ⋯) : (a : M) → M))^[n] ''
      range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    ((⇑(Module.reflection ⋯ ≪≫ₗ Module.reflection ⋯) : (a : M) → M)^[n] ((P.root : (a : ι) → M) j) : M)

Tactic:
exact mem_image_of_mem _ (mem_range_self j)

Premises used: Set.mem_range_self, Set.mem_image_of_mem