awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
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
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : 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)
lj : 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)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : li = 3 * lj
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    li
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
have hk₁ : 3 * P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ lj = 0
Tactic: simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
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
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : 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)
lj : 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)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : li = 3 * lj
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    lj
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    li
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
have hk₁ : P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂ ∨ lj = 0
Tactic: simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
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
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : 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)
lj : 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)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : li = 3 * lj
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    lj
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
have hk₁ : P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ lj = 0
Tactic: simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
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
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : 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)
lj : 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)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : lj = 3 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    li
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    li
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
have hk₁ : P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ li = 0
Tactic: simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
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
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : 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)
lj : 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)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : lj = 3 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    li
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
have hk₁ : P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂ ∨ li = 0
Tactic: simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
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
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : 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)
lj : 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)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : lj = 3 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    lj
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    li
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
have hk₁ : 3 * P.pairing k₂ k₁ = P.pairing k₁ k₂ ∨ li = 0
Tactic: simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas (hypothesis)
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
inst_9 : P.IsReduced
inst_10 : P.IsIrreducible
this : Fintype ι
B : P.InvariantForm
i j : ι
li : 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)
lj : 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)
hij : li ≠ lj
key :
  ∀ (k : ι),
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        li ∨
      (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k : M) =
        lj
k₁ k₂ : ι
hk :
  HMul.hMul (β := R) (P.pairing k₂ k₁)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₁ : M) :
        R) =
    HMul.hMul (β := R) (P.pairing k₁ k₂)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) k₂ : M) :
        R)
h₀ : lj = 3 * li
h₁ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₁) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₁ : M) =
    lj
h₂ :
  (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) k₂) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) k₂ : M) =
    lj
⊢ P.pairing k₁ k₂ = P.pairing k₂ k₁ ∨ P.pairing k₁ k₂ = 3 * P.pairing k₂ k₁ ∨ P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂
have hk₁ : 3 * P.pairing k₂ k₁ = 3 * P.pairing k₁ k₂ ∨ li = 0
Tactic: simp only [h₁, h₂, h₀, ← mul_assoc, mul_comm, mul_eq_mul_right_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := N) (m * m * P.pairing i j + m * n * (P.pairing i j * P.pairing j i) + n * n * P.pairing j i)
      ((P.coroot : (a : ι) → N) k : N) =
    m • HSMul.hSMul (β := N) (P.pairing i j) ((P.coroot : (a : ι) → N) i : N) +
      n • HSMul.hSMul (β := N) (P.pairing j i) ((P.coroot : (a : ι) → N) j : N)
have hlsq : ∀ (i : ι),
  lsq i =
    (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
Tactic: have hlsq (i : ι) : lsq i = P.RootForm (P.root i) (P.root i) := rfl
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (β := N) (lsq k) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m • lsq i) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n • lsq j) ((P.coroot : (a : ι) → N) j : N)
have simp : HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
  HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (β := N) m ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) +
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (β := N) n ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
Tactic: simp only [hlsq, smul_assoc, P.rootForm_self_smul_coroot, smul_comm _ 2]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
    HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (β := N) m ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) +
      HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (β := N) n ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
have rw : HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
  HSMul.hSMul (α := ℕ) (β := N) 2
      ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M)) : N) +
    HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (β := N) n ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
Tactic: rw [← map_smul _ m, ← map_smul _ n, ← nsmul_add, ← map_add, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
rw :
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2
        ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M)) : N) +
      HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (β := N) n ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
⊢ HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
    HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (β := N) m ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) +
      HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (β := N) n ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
have rw₁ : HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
  HSMul.hSMul (α := ℕ) (β := N) 2
      ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M)) : N) +
    HSMul.hSMul (α := ℕ) (β := N) 2
      ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M)) : N)
Tactic: rw [← map_smul _ m, ← map_smul _ n, ← nsmul_add, ← map_add, hk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : CommRing R
inst_4 : Module R M
inst_5 : Module R N
P : RootPairing ι R M N
inst_6 : P.IsAnisotropic
inst_7 : IsDomain R
inst_8 : IsTorsionFree R N
i j k : ι
m n : R
hk :
  HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M) + HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M) =
    (P.root : (a : ι) → M) k
B : P.InvariantForm := P.toInvariantForm
lsq : (i : ι) → R :=
  fun (i : ι) ↦
    (((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M)
hlsq :
  ∀ (i : ι),
    lsq i =
      (((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M)
rw :
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2
        ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M)) : N) +
      HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (β := N) n ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
rw₁ :
  HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
    HSMul.hSMul (α := ℕ) (β := N) 2
        ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M)) : N) +
      HSMul.hSMul (α := ℕ) (β := N) 2
        ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M)) : N)
⊢ HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
    HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (β := N) m ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) i : M) : N)) +
      HSMul.hSMul (α := ℕ) 2
        (HSMul.hSMul (β := N) n ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) j : M) : N))
have rw₂ : HSMul.hSMul (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : M) : N) =
  HSMul.hSMul (α := ℕ) 2
    (HAdd.hAdd (α := N) (β := N)
      ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) m ((P.root : (a : ι) → M) i : M)) : N)
      ((P.Polarization : (a : M) → N) (HSMul.hSMul (β := M) n ((P.root : (a : ι) → M) j : M)) : N))
Tactic: rw [← map_smul _ m, ← map_smul _ n, ← nsmul_add, ← map_add, hk]