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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = 3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 3
⊢ B.rootLength j < B.rootLength i

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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = -4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i

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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : -1 * B.rootLength i = 4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = -1
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i

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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -3
⊢ B.rootLength j < B.rootLength i

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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -2
⊢ B.rootLength j < B.rootLength i

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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 2 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 2
⊢ B.rootLength j < B.rootLength i

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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 3 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 3
⊢ B.rootLength j < B.rootLength i

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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = -4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = -4
⊢ B.rootLength j < B.rootLength i

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
inst_8 : IsDomain R
B : RootPositiveForm ℤ P
i j : ι
hne : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
hne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
hij : P.pairingIn ℤ i j ∉ {-1, 0, 1}
aux₂ : 1 * B.rootLength i = 4 * B.rootLength j
hi : 0 < B.rootLength i
hji : P.pairingIn ℤ j i = 1
hij' : P.pairingIn ℤ i j = 4
⊢ B.rootLength j < B.rootLength i

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
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
simp : P.pairing i j = P.pairing j i
⊢ P.pairingIn ℤ i j = P.pairingIn ℤ j i

Tactic:
simp only [← (FaithfulSMul.algebraMap_injective ℤ R).eq_iff, algebraMap_pairingIn]

Premises used: Function.Injective.eq_iff, RootPairing.algebraMap_pairingIn, Int, FaithfulSMul.algebraMap_injective
-- 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
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ P.pairing i j = P.pairing j i

Tactic:
mul_right_cancel₀ (B.ne_zero j) (len_eq ▸ B.pairing_mul_eq_pairing_mul_swap j i)

Premises used: RootPairing.InvariantForm.ne_zero, mul_right_cancel₀
-- 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
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ P.pairing i j = P.pairing j i

Tactic:
exact mul_right_cancel₀ (B.ne_zero j) (len_eq ▸ B.pairing_mul_eq_pairing_mul_swap j i)

Premises used: RootPairing.InvariantForm.ne_zero, mul_right_cancel₀
-- 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
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ P.pairingIn ℤ i j = P.pairingIn ℤ j i

Tactic:
replace len_eq : P.pairingIn ℤ i j = P.pairingIn ℤ j i := by
    simp only [← (FaithfulSMul.algebraMap_injective ℤ R).eq_iff, algebraMap_pairingIn]
    exact mul_right_cancel₀ (B.ne_zero j) (len_eq ▸ B.pairing_mul_eq_pairing_mul_swap 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
B : P.InvariantForm
len_eq : P.pairingIn ℤ i j = P.pairingIn ℤ j i
⊢ 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
B : P.InvariantForm
len_eq : P.pairingIn ℤ i j = P.pairingIn ℤ j i
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)
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)} (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
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
ne : i ≠ j
ne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
ne : i ≠ j
ne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this : Module.IsReflexive R M
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_length_eq len_eq
-- 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
B : P.InvariantForm
len_eq :
  Eq.{u_2 + 1} («α» := R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
ne : i ≠ j
ne' : Ne.{u_3 + 1} («α» := M) ((P.root : (a : ι) → M) i : M) (-(P.root : (a : ι) → M) j : M)
this_1 : Module.IsReflexive R M
this :
  Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)
⊢ Membership.mem (γ := Set (ℤ × ℤ)) {(0, 0), (1, 1), (-1, -1)} (P.pairingIn ℤ i j, P.pairingIn ℤ j i)

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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.pairingIn ℤ i j = 0
rw : P.pairingIn ℤ i j * P.pairingIn ℤ j i = 0
rw₁ : 0 * P.pairingIn ℤ j i = 0
rw₂ rw₃ : Eq («α» := ℤ) 0 0
⊢ P.coxeterWeightIn ℤ i j = 0

Tactic:
rw [coxeterWeightIn, h, zero_mul]

Premises used: MulZeroClass.zero_mul, RootPairing.coxeterWeightIn
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
refine : ∀ (h : P.coxeterWeightIn ℤ i j = 0), P.pairingIn ℤ i j = 0
⊢ P.coxeterWeightIn ℤ i j = 0 ↔ P.pairingIn ℤ i j = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [coxeterWeightIn, h, zero_mul]⟩
-- 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 : CharZero R
inst_6 : P.IsCrystallographic
i j : ι
inst_7 : IsDomain R
h : P.coxeterWeightIn ℤ i j = 0
rwa :
  ∀
    (h :
      Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R)
        ((algebraMap ℤ R : (a : ℤ) → R) 0 : R)),
    P.pairingIn ℤ i j = 0
rwa₁ :
  ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.coxeterWeightIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
rwa₂ : ∀ (h : P.coxeterWeight i j = 0), P.pairingIn ℤ i j = 0
rwa₃ : ∀ (h : P.IsOrthogonal i j), P.pairingIn ℤ i j = 0
rwa₄ : ∀ (h : P.pairing i j = 0 ∧ P.pairing j i = 0), P.pairingIn ℤ i j = 0
rwa₅ : ∀ (h : P.pairing i j = 0 ∧ P.pairing i j = 0), P.pairingIn ℤ i j = 0
rwa₆ : ∀ (h : P.pairing i j = 0), P.pairingIn ℤ i j = 0
rwa₇ : ∀ (h : Eq («α» := R) ((algebraMap ℤ R : (a : ℤ) → R) (P.pairingIn ℤ i j) : R) (0 : R)), P.pairingIn ℤ i j = 0
rwa₈ rwa₉ rwa₁₀ rwa₁₁ : ∀ (h : P.pairingIn ℤ i j = 0), P.pairingIn ℤ i j = 0
⊢ P.pairingIn ℤ i j = 0

Tactic:
rwa [← (algebraMap_injective ℤ R).eq_iff, map_zero, algebraMap_coxeterWeightIn,
    RootPairing.coxeterWeight_zero_iff_isOrthogonal, IsOrthogonal,
    P.pairing_eq_zero_iff' (i := j) (j := i), and_self, ← P.algebraMap_pairingIn ℤ,
    FaithfulSMul.algebraMap_eq_zero_iff] at h

Premises used: and_self, RootPairing.pairing_eq_zero_iff', Function.Injective.eq_iff, map_zero, RootPairing.algebraMap_coxeterWeightIn, RootPairing.algebraMap_pairingIn, RootPairing.coxeterWeight_zero_iff_isOrthogonal, Int, FaithfulSMul.algebraMap_injective, RootPairing.IsOrthogonal, FaithfulSMul.algebraMap_eq_zero_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
⊢ Module.IsReflexive R M

Tactic:
have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
-- 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 : Module.IsReflexive R M
⊢ Module.IsReflexive R N

Tactic:
have : Module.IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- 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 : Module.IsReflexive R N
⊢ IsAddTorsionFree M

Tactic:
have : IsAddTorsionFree M := .of_isTorsionFree R M
-- 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
pos :
  ∀
    (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 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 :
  ∀
    (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 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:
by_cases hli : LinearIndependent R ![α 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 : P.pairingIn ℤ i j = 1 ∨ P.pairingIn ℤ j i = 1
inl :
  ∀ (h₁ : P.pairingIn ℤ 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))
inr :
  ∀ (h₁ : 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 h₁ | h₁
-- 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 ℤ i j = 1
⊢ P.pairing i j = 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 ℤ i j = 1
⊢ P.pairing i j = 1

Tactic:
replace h₁ : P.pairing i j = 1 := by simpa [← P.algebraMap_pairingIn ℤ]