awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
h₁ : P.pairing i j = 1
⊢ (P.root : (a : ι) → M) ((P.reflectionPerm j : (a : ι) → ι) i : ι) =
    HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)

Tactic:
simpa [h₁] using P.reflection_apply_root j i

Premises used: RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
h₁ : P.pairing i j = 1
⊢ 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))

Tactic:
exact ⟨P.reflectionPerm j i, by simpa [h₁] using P.reflection_apply_root j i⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
h₁ : P.pairingIn ℤ j i = 1
⊢ P.pairing j i = 1

Tactic:
simpa [← P.algebraMap_pairingIn ℤ]

Premises used: RootPairing.algebraMap_pairingIn, Int
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
h₁ : P.pairingIn ℤ j i = 1
⊢ P.pairing j i = 1

Tactic:
replace h₁ : P.pairing j i = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
h₁ : P.pairing j i = 1
inr :
  Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M))
⊢ 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))

Tactic:
rw [← neg_mem_range_root_iff, neg_sub]

Premises used: neg_sub, RootPairing.neg_mem_range_root_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
h₁ : P.pairing j i = 1
⊢ (P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) j : ι) =
    HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M)

Tactic:
simpa [h₁] using P.reflection_apply_root i j

Premises used: RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
h₁ : P.pairing j i = 1
⊢ Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) j : M) ((P.root : (a : ι) → M) i : M))

Tactic:
exact ⟨P.reflectionPerm i j, by simpa [h₁] using P.reflection_apply_root i j⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
pos : P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
⊢ 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))

Tactic:
suffices P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1 by
      rcases this with h₁ | h₁
      · replace h₁ : P.pairing i j = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
        exact ⟨P.reflectionPerm j i, by simpa [h₁] using P.reflection_apply_root j i⟩
      · replace h₁ : P.pairing j i = 1 := by simpa [← P.algebraMap_pairingIn ℤ]
        rw [← neg_mem_range_root_iff, neg_sub]
        exact ⟨P.reflectionPerm i j, by simpa [h₁] using P.reflection_apply_root i j⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
⊢ Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)

Tactic:
have aux₁ := P.coxeterWeightIn_mem_set_of_isCrystallographic i j
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
aux₁ : Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
⊢ P.coxeterWeightIn ℤ i j ≠ 4

Tactic:
have aux₂ := (linearIndependent_iff_coxeterWeightIn_ne_four P ℤ).mp hli
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
aux₁ : Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
aux₂ : P.coxeterWeightIn ℤ i j ≠ 4
⊢ P.coxeterWeightIn ℤ i j ≠ 0

Tactic:
simpa only [ne_eq, P.coxeterWeightIn_eq_zero_iff] using h.ne'

Premises used: RootPairing.coxeterWeightIn_eq_zero_iff, ne_eq, LT.lt.ne'
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
aux₁ : Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
aux₂ : P.coxeterWeightIn ℤ i j ≠ 4
⊢ P.coxeterWeightIn ℤ i j ≠ 0

Tactic:
have aux₃ : P.coxeterWeightIn ℤ i j ≠ 0 := by
        simpa only [ne_eq, P.coxeterWeightIn_eq_zero_iff] using h.ne'
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
aux₁ : Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (P.coxeterWeightIn ℤ i j)
aux₂ : P.coxeterWeightIn ℤ i j ≠ 4
aux₃ : P.coxeterWeightIn ℤ i j ≠ 0
⊢ Membership.mem (γ := Set ℤ) {1, 2, 3} (P.coxeterWeightIn ℤ i j)

Tactic:
simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  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)
⊢ Membership.mem (γ := Set ℤ) {1, 2, 3} (P.coxeterWeightIn ℤ i j)

Tactic:
have : P.coxeterWeightIn ℤ i j ∈ ({1, 2, 3} : Set _) := by
      have aux₁ := P.coxeterWeightIn_mem_set_of_isCrystallographic i j
      have aux₂ := (linearIndependent_iff_coxeterWeightIn_ne_four P ℤ).mp hli
      have aux₃ : P.coxeterWeightIn ℤ i j ≠ 0 := by
        simpa only [ne_eq, P.coxeterWeightIn_eq_zero_iff] using h.ne'
      simp_all
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
hli :
  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)
this : Membership.mem (γ := Set ℤ) {1, 2, 3} (P.coxeterWeightIn ℤ i j)
⊢ P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
        P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 1 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
            P.pairingIn ℤ i j = -2 ∧ P.pairingIn ℤ j i = -1 ∨
              P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
                P.pairingIn ℤ i j = 3 ∧ P.pairingIn ℤ j i = 1 ∨
                  P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -3 ∧ P.pairingIn ℤ j i = -1

Tactic:
simp_rw [coxeterWeightIn, Int.mul_mem_one_two_three_iff, mem_insert_iff, mem_singleton_iff,
      Prod.mk.injEq] at this

Premises used: Set.mem_singleton_iff, Int.mul_mem_one_two_three_iff, Prod.mk.injEq, RootPairing.coxeterWeightIn, Set.mem_insert_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
hli :
  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)
this :
  P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 1 ∨
    P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -1 ∨
      P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 2 ∨
        P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 1 ∨
          P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -2 ∨
            P.pairingIn ℤ i j = -2 ∧ P.pairingIn ℤ j i = -1 ∨
              P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 3 ∨
                P.pairingIn ℤ i j = 3 ∧ P.pairingIn ℤ j i = 1 ∨
                  P.pairingIn ℤ i j = -1 ∧ P.pairingIn ℤ j i = -3 ∨ P.pairingIn ℤ i j = -3 ∧ P.pairingIn ℤ j i = -1
⊢ P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  ¬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)
⊢ Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
hli :
  ¬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)
this :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
⊢ P.pairingIn ℤ i j * P.pairingIn ℤ j i = 4

Tactic:
replace hli : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 4 :=
        (P.coxeterWeightIn_eq_four_iff_not_linearIndependent ℤ).mpr hli
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
this :
  Membership.mem (γ := Set (ℤ × ℤ))
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
      (-4, -1), (-1, -4), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
hli : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 4
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(1, 4), (2, 2), (4, 1)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  ¬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)
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(1, 4), (2, 2), (4, 1)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
have : (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ ({(1, 4), (2, 2), (4, 1)} : Set _) := by
      have := P.pairingIn_pairingIn_mem_set_of_isCrystallographic i j
      replace hli : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 4 :=
        (P.coxeterWeightIn_eq_four_iff_not_linearIndependent ℤ).mpr hli
      aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
hli :
  ¬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)
this : Membership.mem (γ := Set (ℤ × ℤ)) {(1, 4), (2, 2), (4, 1)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
⊢ P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4 ∨
    P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 2 ∨ P.pairingIn ℤ i j = 4 ∧ P.pairingIn ℤ j i = 1

Tactic:
simp only [mem_insert_iff, mem_singleton_iff, Prod.mk.injEq] at this

Premises used: Set.mem_singleton_iff, Prod.mk.injEq, Set.mem_insert_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this_3 : IsAddTorsionFree M
hli :
  ¬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)
this :
  P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4 ∨
    P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 2 ∨ P.pairingIn ℤ i j = 4 ∧ P.pairingIn ℤ j i = 1
neg :
  ∀ (hij : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4),
    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))
neg₁ :
  ∀ (hij : P.pairingIn ℤ i j = 2 ∧ P.pairingIn ℤ j i = 2),
    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))
neg₂ :
  ∀ (hij : P.pairingIn ℤ i j = 4 ∧ P.pairingIn ℤ j i = 1),
    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))
    (HSub.hSub («α» := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M))

Tactic:
rcases this with hij | hij | hij
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
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 : Finite ι
inst_6 : CharZero R
inst_7 : P.IsCrystallographic
i j : ι
inst_8 : IsDomain R
h : 0 < P.pairingIn ℤ i j
h' : i ≠ j
this_1 : Module.IsReflexive R M
this_2 : Module.IsReflexive R N
this : IsAddTorsionFree M
hli :
  ¬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)
hij : P.pairingIn ℤ i j = 1 ∧ P.pairingIn ℤ j i = 4
neg :
  Membership.mem.{u_3, u_3} («α» := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    (-(P.root : (a : ι) → M) i : M)
⊢ 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))

Tactic:
rw [(P.pairingIn_one_four_iff ℤ i j).mp hij, two_smul, sub_add_cancel_right]

Premises used: two_smul, Int, RootPairing.pairingIn_one_four_iff, Iff.mp, sub_add_cancel_right