awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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))
⊢ 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) +
          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)
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))
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) +
            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 (α := ℕ) (β := N) 2 ((P.Polarization : (a : M) → N) ((P.root : (a : ι) → M) k : 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 (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)
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) (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 h₁ : 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)
Tactic: have h₁ : lsq k • P.coroot k = (m • lsq i) • P.coroot i + (n • lsq j) • P.coroot j := by
    simp only [hlsq, smul_assoc, P.rootForm_self_smul_coroot, smul_comm _ 2]
    rw [← map_smul _ m, ← map_smul _ n, ← nsmul_add, ← map_add, 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)
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)
h₁ :
  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)
⊢ lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R) +
      n * n * lsq j
have aux : Eq.{u_2 + 1} (α := R)
  ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) i : M) :
    R)
  ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
      ((P.root : (a : ι) → M) j : M) :
    R)
Tactic: have aux : P.RootForm (P.root j) (P.root i) = B.form (P.root i) (P.root j) :=
      P.rootForm_symmetric.eq (P.root j) (P.root i)
-- 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)
h₁ :
  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)
aux :
  Eq.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) i : M) :
      R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R)
⊢ lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R) +
      n * n * lsq j
have simp : m *
      (HMul.hMul (β := R) m
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) i : M) :
            R) +
        HMul.hMul (β := R) n
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R)) +
    n *
      (HMul.hMul (β := R) m
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R) +
        HMul.hMul (β := R) n
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R)) =
  HMul.hMul (β := R) (m * m)
        ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
            ((P.root : (a : ι) → M) i : M) :
          R) +
      m * n *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R) +
    HMul.hMul (β := R) (n * n)
      ((((P.RootForm : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) j) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R)
Tactic: simp [hlsq, ← hk, aux, B]
-- 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)
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)
h₁ :
  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)
⊢ 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 h₂ : lsq k =
  m * m * lsq i +
      m * n *
        HMul.hMul (α := R) (β := R) (2 : R)
          ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
              ((P.root : (a : ι) → M) j : M) :
            R) +
    n * n * lsq j
Tactic: have h₂ :
      lsq k = (m * m) * lsq i + (m * n) * (2 * B.form (P.root i) (P.root j)) + (n * n) * lsq j := by
    have aux : P.RootForm (P.root j) (P.root i) = B.form (P.root i) (P.root j) :=
      P.rootForm_symmetric.eq (P.root j) (P.root i)
    simp [hlsq, ← hk, aux, B]
    ring
-- 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)
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)
h₁ :
  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)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R) +
      n * n * lsq j
⊢ 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 h₃ : HMul.hMul (α := R) (β := R) (2 : R)
    ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
        ((P.root : (a : ι) → M) j : M) :
      R) =
  P.pairing i j * lsq j
Tactic: have h₃ : 2 * B.form (P.root i) (P.root j) = P.pairing i j * lsq j :=
    B.two_mul_apply_root_root i j
-- 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)
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)
h₁ :
  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)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    P.pairing i j * lsq j
⊢ 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 h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
Tactic: have h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j := B.pairing_mul_eq_pairing_mul_swap i j
-- 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)
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)
h₁ :
  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)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
⊢ HSMul.hSMul (β := N) (m * m * (P.pairing j i * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (m * n * (P.pairing j i * P.pairing i j * lsq j)) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (n * n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m * (P.pairing j i * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)
have h₅ : HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
    ((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)
Tactic: rw [h₂, h₃] at h₁
Cleared hypotheses: h₁, h₂, h₃, h₄
-- 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)
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)
h₁ :
  HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
      ((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)
h₂ :
  lsq k =
    m * m * lsq i +
        m * n *
          HMul.hMul (α := R) (β := R) (2 : R)
            ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
                ((P.root : (a : ι) → M) j : M) :
              R) +
      n * n * lsq j
h₃ :
  HMul.hMul (α := R) (β := R) (2 : R)
      ((((B.form : (a : M) → M →ₗ[R] R) ((P.root : (a : ι) → M) i) : M →ₗ[R] R) : (a : M) → R)
          ((P.root : (a : ι) → M) j : M) :
        R) =
    P.pairing i j * lsq j
h₄ : P.pairing j i * lsq i = P.pairing i j * lsq j
⊢ HSMul.hSMul (β := N) (m * m * (P.pairing j i * lsq i)) ((P.coroot : (a : ι) → N) k : N) +
        HSMul.hSMul (β := N) (m * n * (P.pairing j i * P.pairing i j * lsq j)) ((P.coroot : (a : ι) → N) k : N) +
      HSMul.hSMul (β := N) (n * n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) k : N) =
    HSMul.hSMul (β := N) (m * (P.pairing j i * lsq i)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)
have h₅ : Eq.{u_4 + 1} (α := N)
  ((fun (n : N) ↦ P.pairing j i • n)
    (HSMul.hSMul (β := N) (m * m * lsq i + m * n * (P.pairing i j * lsq j) + n * n * lsq j)
      ((P.coroot : (a : ι) → N) k : N)))
  ((fun (n : N) ↦ P.pairing j i • 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)))
Tactic: replace h₁ := congr_arg (fun n ↦ P.pairing j i • n) h₁
Cleared hypotheses: h₁