awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
      Fin (Nat.succ 0).succ → M)
rw rw₁ :
  P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
⊢ HSub.hSub (α := ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ) =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i

Tactic:
rw [P.chainBotCoeff_sub_chainTopCoeff h]

Premises used: RootPairing.chainBotCoeff_sub_chainTopCoeff
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
h :
  LinearIndependent.{0, u_2, u_3} (ι := Fin (Nat.succ 0).succ) R (M := M)
    (![(P.root : (a : ι) → M) i,
        (P.root : (a : ι) → M) (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)] :
      Fin (Nat.succ 0).succ → M)
calc :
  HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ)
calc₁ :
  (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
          (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
      ℤ) =
    HSub.hSub (α := ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
calc₂ :
  HSub.hSub (α := ℤ)
      (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i
            (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j)) :
        ℤ) =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i
⊢ HAdd.hAdd (α := ℤ) (↑(chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ)
      (↑(chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) : ℤ) =
    P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i

Tactic:
calc (P.chainBotCoeff i j + P.chainTopCoeff i j : ℤ)
    _ = P.chainBotCoeff i (P.chainTopIdx i j) := by simp
    _ = P.chainBotCoeff i (P.chainTopIdx i j) - P.chainTopCoeff i (P.chainTopIdx i j) := by simp
    _ = P.pairingIn ℤ (P.chainTopIdx i j) i := by rw [P.chainBotCoeff_sub_chainTopCoeff h]

Premises used: RootPairing.chainTopIdx, RootPairing.pairingIn, RootPairing.chainBotCoeff, Int, Nat.cast, RootPairing.chainTopCoeff, HAdd.hAdd
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
pos :
  ∀
    (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)),
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
      3
neg :
  ∀
    (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)),
    chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
        chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
      3
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    3

Tactic:
by_cases h : LinearIndependent R ![P.root i, P.root j]

Premises used: RootPairing.root, LinearIndependent, Matrix.vecEmpty, DFunLike.coe, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
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)
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    3

Tactic:
simp [chainTopCoeff_of_not_linearIndependent, chainBotCoeff_of_not_linearIndependent, h]

Premises used: RootPairing.chainTopCoeff_of_not_linearIndependent, RootPairing.chainBotCoeff_of_not_linearIndependent
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
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)
pos : P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i ≤ 3
⊢ chainBotCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j +
      chainTopCoeff.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j ≤
    3

Tactic:
rw [← Int.ofNat_le, Nat.cast_add, Nat.cast_ofNat,
    chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx h]

Premises used: Nat.cast_ofNat, RootPairing.chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx, Nat.cast_add, Int.ofNat_le
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
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)
⊢ 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), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j),
      P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i)

Tactic:
have := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed i (P.chainTopIdx i j)
-- Module: Mathlib.LinearAlgebra.RootSystem.Chain
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
inst_1 : CommRing R
inst_2 : CharZero R
inst_3 : IsDomain R
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : AddCommGroup N
inst_7 : Module R N
P : RootPairing ι R M N
inst_8 : P.IsCrystallographic
i j : ι
inst_9 : P.IsReduced
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)
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), (2, 2), (-2, -2)}
    (P.pairingIn ℤ i (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j),
      P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i)
⊢ P.pairingIn ℤ (chainTopIdx.{u_1, u_2, u_3, u_4} (R := R) (M := M) (N := N) (P := P) i j) i ≤ 3

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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
⊢ P.flip.flip = P

Tactic:
rfl

Premises used: RootPairing.flip, LinearMap.mk₂'ₛₗ, LinearMap.flip, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
inst_5 : NeZero.{u_2} (R := R) 2
h : Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)
⊢ Eq.{u_2 + 1} (α := R) 0 2

Tactic:
simpa [h] using P.root_coroot_two i

Premises used: RootPairing.root_coroot_two
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
inst_5 : NeZero.{u_2} (R := R) 2
⊢ Ne.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N) (0 : N)

Tactic:
P.flip.ne_zero i

Premises used: RootPairing.ne_zero, RootPairing.flip
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : NeZero.{u_2} (R := R) 2
⊢ 0 ∉ range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)

Tactic:
simpa only [mem_range, not_exists] using fun i ↦ P.ne_zero i

Premises used: Set.mem_range, RootPairing.ne_zero, not_exists
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : NeZero.{u_2} (R := R) 2
⊢ 0 ∉ range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)

Tactic:
P.flip.zero_notMem_range_root

Premises used: RootPairing.zero_notMem_range_root, Set.Mem, RootPairing.flip
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
obtain : ∀ (i : ι), ∃ (i : ι), Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)
⊢ ∃ (i : ι), Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)

Tactic:
obtain ⟨i⟩ := (inferInstance : Nonempty ι)

Premises used: inferInstance
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
i : ι
⊢ ∃ (i : ι), Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)

Tactic:
⟨i, P.ne_zero i⟩

Premises used: RootPairing.ne_zero, Exists.intro
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
i : ι
⊢ ∃ (i : ι), Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)

Tactic:
exact ⟨i, P.ne_zero i⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
⊢ ∃ (i : ι), Ne.{u_4 + 1} (α := N) ((P.coroot : (a : ι) → N) i : N) (0 : N)

Tactic:
P.flip.exists_ne_zero

Premises used: RootPairing.flip, RootPairing.exists_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
obtain : ∀ (i : ι) (hi : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)), Nontrivial M
⊢ Nontrivial M

Tactic:
obtain ⟨i, hi⟩ := P.exists_ne_zero

Premises used: RootPairing.exists_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
i : ι
hi : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)
⊢ Nontrivial M

Tactic:
⟨P.root i, 0, hi⟩

Premises used: Nontrivial.mk, RootPairing.root, Exists.intro, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
i : ι
hi : Ne.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) i : M) (0 : M)
⊢ Nontrivial M

Tactic:
exact ⟨P.root i, 0, hi⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : Nonempty ι
inst_6 : NeZero.{u_2} (R := R) 2
⊢ Nontrivial N

Tactic:
P.flip.nontrivial

Premises used: RootPairing.flip, RootPairing.nontrivial
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ P.flip.pairing i j = P.pairing j i

Tactic:
rfl

Premises used: RootPairing.pairing, RootPairing.flip, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (((P.toLinearMap : (a : M) → N →ₗ[R] R) ((P.root : (a : ι) → M) i) : N →ₗ[R] R) : (a : N) → R)
      ((P.coroot : (a : ι) → N) j : N) =
    P.pairing i j

Tactic:
rfl

Premises used: RootPairing.pairing, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (P.root' i : (a : N) → R) ((P.coroot : (a : ι) → N) j : N) = P.pairing i j

Tactic:
rfl

Premises used: RootPairing.pairing, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (P.coroot' i : (a : M) → R) ((P.root : (a : ι) → M) j : M) = P.pairing j i

Tactic:
rfl

Premises used: RootPairing.pairing, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) j : M) =
    P.pairing j i

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ P.pairing i i = 2

Tactic:
P.root_coroot_two i

Premises used: RootPairing.root_coroot_two, RootPairing.pairing
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 k l : ι
h : (P.root : (a : ι) → M) k = HAdd.hAdd (α := M) (β := M) ((P.root : (a : ι) → M) i : M) ((P.root : (a : ι) → M) j : M)
⊢ P.pairing k l = P.pairing i l + P.pairing j l

Tactic:
simp only [← root_coroot_eq_pairing, h, map_add, LinearMap.add_apply]

Premises used: RootPairing.root_coroot_eq_pairing, LinearMap.add_apply, map_add
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 k l : ι
x y : R
h :
  (P.root : (a : ι) → M) k =
    HSMul.hSMul (β := M) x ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) y ((P.root : (a : ι) → M) l : M)
⊢ P.pairing k j = x • P.pairing i j + y • P.pairing l j

Tactic:
simp only [← root_coroot_eq_pairing, h, map_add, map_smul, LinearMap.add_apply,
    LinearMap.smul_apply, smul_eq_mul]

Premises used: RootPairing.root_coroot_eq_pairing, LinearMap.smul_apply, LinearMap.add_apply, map_add, smul_eq_mul, map_smul
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.flip : (a : N) → M →ₗ[R] R) ((P.coroot : (a : ι) → N) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    (2 : R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) ((P.reflectionPerm i : (a : ι) → ι) j : ι) : M)
    ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M)

Tactic:
(P.reflectionPerm_root i j).symm

Premises used: RootPairing.reflectionPerm_root, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ Membership.mem (α := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M)

Tactic:
P.root_reflectionPerm i j ▸ mem_range_self (P.reflectionPerm i j)

Premises used: Set.mem_range_self, Eq.rec, RootPairing.reflectionPerm, DFunLike.coe, RootPairing.root_reflectionPerm
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ Membership.mem (α := M) (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))
    ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) : M)

Tactic:
exact P.root_reflectionPerm i j ▸ mem_range_self (P.reflectionPerm i j)
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
x : M
⊢ (P.reflection i : (a : M) → M) x =
    x - HSMul.hSMul.{u_2, u_3, u_3} (α := R) (β := M) ((P.coroot' i : (a : M) → R) x : R) ((P.root : (a : ι) → M) i : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) j : M) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M))

Tactic:
rfl

Premises used: RootPairing.pairing, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ Eq (α := M) ((P.reflection i : (a : M) → M) ((P.root : (a : ι) → M) i : M) : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
Module.reflection_apply_self (P.coroot_root_two i)

Premises used: Module.reflection_apply_self, RootPairing.coroot_root_two
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
x : M
⊢ (P.reflection i : (a : M) → M) ((P.reflection i : (a : M) → M) x : M) = x

Tactic:
Module.involutive_reflection (P.coroot_root_two i) x

Premises used: Module.involutive_reflection, RootPairing.coroot_root_two
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ (P.reflection i)⁻¹ = P.reflection i

Tactic:
rfl

Premises used: LinearEquiv.symm, Module.preReflection, RootPairing.reflection, Module.reflection, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
⊢ HPow.hPow (β := ℕ) (P.reflection i) 2 = 1

Tactic:
mul_eq_one_iff_eq_inv.mpr rfl

Premises used: Iff.mpr, mul_eq_one_iff_eq_inv, npowRec, LinearEquiv.trans, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.Defs
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 : ι
H : ∀ (j : ι), Eq (α := ι) ((HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 : (a : ι) → ι) j : ι) ((1 : (a : ι) → ι) j : ι)
⊢ HPow.hPow (β := ℕ) (P.reflectionPerm i) 2 = 1

Tactic:
ext j