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
i j : ι
inst_5 : Finite ι
inst_6 : NeZero.{u_2} (R := R) 2
inst_7 : 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)
contra : P.coxeterWeight i j = 4
⊢ Infinite ι

Tactic:
have := P.infinite_of_linearIndependent_coxeterWeight_four hl contra
-- 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 : Finite ι
inst_6 : NeZero.{u_2} (R := R) 2
inst_7 : 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)
contra : P.coxeterWeight i j = 4
this : Infinite ι
⊢ False

Tactic:
not_finite ι

Premises used: not_finite
-- 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 : Finite ι
inst_6 : NeZero.{u_2} (R := R) 2
inst_7 : 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)
contra : P.coxeterWeight i j = 4
this : Infinite ι
⊢ False

Tactic:
exact not_finite ι

Premises used: not_finite
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree 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) ↔
    P.coxeterWeight i j ≠ 4

Tactic:
⟨coxeterWeight_ne_four_of_linearIndependent P, fun h ↦ ?_⟩

Premises used: RootPairing.coxeterWeight_ne_four_of_linearIndependent, Iff.intro
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
refine :
  ∀ (h : P.coxeterWeight i j ≠ 4),
    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)
⊢ 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) ↔
    P.coxeterWeight i j ≠ 4

Tactic:
refine ⟨coxeterWeight_ne_four_of_linearIndependent P, fun h ↦ ?_⟩
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h : P.coxeterWeight i j ≠ 4
contrapose :
  ∀
    (h :
      ¬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)),
    P.coxeterWeight i j = 4
⊢ 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:
contrapose h
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬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)
⊢ HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)

Tactic:
have h₁ := P.pairing_smul_root_eq_of_not_linearIndependent h
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬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₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)

Tactic:
rw [LinearIndependent.pair_symm_iff] at h

Premises used: LinearIndependent.pair_symm_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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬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₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
h₂ :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
⊢ HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)

Tactic:
rw [LinearIndependent.pair_symm_iff] at h

Premises used: LinearIndependent.pair_symm_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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)

Tactic:
have h₂ := P.pairing_smul_root_eq_of_not_linearIndependent h
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
suffices :
  HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
⊢ P.coxeterWeight i j = 4

Tactic:
suffices P.coxeterWeight i j • P.root i = (4 : R) • P.root i from
    smul_left_injective R (P.ne_zero i) 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M)

Tactic:
rfl
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
rw :
  P.pairing i j • HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
rw₁ rw₂ :
  P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M) =
    P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
⊢ HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)

Tactic:
rw [mul_smul, h₁]

Premises used: SemigroupAction.mul_smul
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
rw :
  HSMul.hSMul (β := M) (HMul.hMul (α := R) 2 2) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
⊢ P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)

Tactic:
rw [smul_comm, h₂, ← mul_smul]

Premises used: SMulCommClass.smul_comm, SemigroupAction.mul_smul
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := M) (HMul.hMul (α := R) 2 2) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)

Tactic:
norm_num
-- 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 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
this : IsAddTorsionFree M
h :
  ¬LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
      (![(P.root : (a : ι) → M) j, (P.root : (a : ι) → M) i] : Fin (Nat.succ 0).succ → M)
h₁ :
  HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
h₂ :
  HSMul.hSMul (β := M) (P.pairing i j) ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) i : M)
calc :
  HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M)
calc₁ :
  HSMul.hSMul (β := M) (P.pairing i j * P.pairing j i) ((P.root : (a : ι) → M) i : M) =
    P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M)
calc₂ :
  P.pairing i j • HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 2 ((P.root : (a : ι) → M) j : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := M) (P.coxeterWeight i j) ((P.root : (a : ι) → M) i : M) =
    HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) 4 ((P.root : (a : ι) → M) i : M)

Tactic:
calc P.coxeterWeight i j • P.root i
      = (P.pairing i j * P.pairing j i) • P.root i := by rfl
    _ = P.pairing i j • (2 : R) • P.root j := by rw [mul_smul, h₁]
    _ = (4 : R) • P.root i := by rw [smul_comm, h₂, ← mul_smul]; norm_num

Premises used: RootPairing.coxeterWeight, RootPairing.pairing, HMul.hMul, RootPairing.root, OfNat.ofNat, 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
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
rw : P.coxeterWeight i j = 4 ↔ ¬P.coxeterWeight i j ≠ 4
rw₁ rw₂ : P.coxeterWeight i j = 4 ↔ P.coxeterWeight i j = 4
⊢ P.coxeterWeight i j = 4 ↔
    ¬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:
rw [P.linearIndependent_iff_coxeterWeight_ne_four, not_not]

Premises used: Classical.not_not, RootPairing.linearIndependent_iff_coxeterWeight_ne_four
-- 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
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
⊢ P.flip.IsReduced

Tactic:
⟨fun i j h ↦ ?_⟩

Premises used: RootPairing.IsReduced.mk
-- 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
S : Type u_5
i j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
refine :
  ∀ (i j : ι)
    (h :
      ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
          (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)),
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
      Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
⊢ P.flip.IsReduced

Tactic:
refine ⟨fun i j h ↦ ?_⟩
-- 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
S : Type u_5
i_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)
inl :
  ∀
    (h :
      ¬LinearIndependent.{0, u_2, u_4} R (M := N)
          (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) i] : Fin (Nat.succ 0).succ → N)),
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) i : N) ∨
      Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) i : N)
inr :
  ∀ (hij : i ≠ j),
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
      Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)

Tactic:
rcases eq_or_ne i j with rfl | hij

Premises used: eq_or_ne, rfl
-- 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
S : Type u_5
i_1 j : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) i] : Fin (Nat.succ 0).succ → N)
inl inl₁ :
  ¬Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) i : N) →
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) i : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) i : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) i : N)

Tactic:
tauto
-- 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
S : Type u_5
i_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)
hij : i ≠ j
inr : Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)
⊢ Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) ((P.flip.root : (a : ι) → N) j : N) ∨
    Eq.{u_4 + 1} (α := N) ((P.flip.root : (a : ι) → N) i : N) (-(P.flip.root : (a : ι) → N) j : N)

Tactic:
right
-- 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
S : Type u_5
i_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)
hij : i ≠ j
⊢ ¬(i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))

Tactic:
rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight_flip,
    coxeterWeight_eq_four_iff_not_linearIndependent, IsReduced.linearIndependent_iff] at h

Premises used: RootPairing.coxeterWeight_flip, RootPairing.IsReduced.linearIndependent_iff, RootPairing.coxeterWeight_eq_four_iff_not_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
S : Type u_5
i_1 j_1 : ι
inst_5 : Finite ι
inst_6 : CharZero R
inst_7 : IsDomain R
inst_8 : IsTorsionFree R M
inst_9 : P.IsReduced
inst_10 : IsTorsionFree R N
i j : ι
h :
  ¬LinearIndependent.{0, u_2, u_4} (ι := Fin (Nat.succ 0).succ) R (M := N)
      (![(P.flip.root : (a : ι) → N) i, (P.flip.root : (a : ι) → N) j] : Fin (Nat.succ 0).succ → N)
hij : i ≠ j
h₁ : ¬(i ≠ j ∧ Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M))
⊢ i ≠ j

Tactic:
rw [← coxeterWeight_eq_four_iff_not_linearIndependent, coxeterWeight_flip,
    coxeterWeight_eq_four_iff_not_linearIndependent, IsReduced.linearIndependent_iff] at h

Premises used: RootPairing.coxeterWeight_flip, RootPairing.IsReduced.linearIndependent_iff, RootPairing.coxeterWeight_eq_four_iff_not_linearIndependent