awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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₂ :
  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
h₁ :
  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)
⊢ HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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 i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)

Tactic:
simp only [h₄] at h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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₂ :
  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
h₁ :
  HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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 i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)
a :
  Eq.{u_4 + 1} (α := N)
    ((fun (x : N) ↦ lsq j • x)
      (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)))
    ((fun (x : N) ↦ lsq j • x)
      (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)))
⊢ 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)

Tactic:
apply smul_right_injective _ (r := lsq j) (RootPairing.IsAnisotropic.rootForm_root_ne_zero j)

Premises used: RootPairing.IsAnisotropic.rootForm_root_ne_zero, smul_right_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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₂ :
  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
h₁ :
  HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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 i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)
⊢ HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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 i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)

Tactic:
h₁
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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₂ :
  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
h₁ :
  HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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 i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)
h :
  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) =
    HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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)
h₅ :
  lsq j •
      (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)) =
    HSMul.hSMul (β := N) (m * (P.pairing i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : 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) =
    lsq j •
      (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))

Tactic:
convert! h₁ using 1
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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₂ :
  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
h₁ :
  HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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 i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : 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) =
    HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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)

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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₂ :
  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
h₁ :
  HSMul.hSMul (β := N) (m * m * (P.pairing i j * lsq j)) ((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 i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)
⊢ lsq j •
      (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)) =
    HSMul.hSMul (β := N) (m * (P.pairing i j * lsq j)) ((P.coroot : (a : ι) → N) i : N) +
      HSMul.hSMul (β := N) (n * (P.pairing j i * lsq j)) ((P.coroot : (a : ι) → N) j : N)

Tactic:
module
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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
S : Type u_5
inst_6 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsAnisotropic
apply :
  finrank.{u_5, u_4} S ↥(P.corootSpan S) ≤
    finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S))
⊢ finrank.{u_5, u_4} S ↥(LinearMap.range (M := ↥(P.rootSpan S)) (P.PolarizationIn S)) =
    finrank.{u_5, u_4} S ↥(P.corootSpan S)

Tactic:
apply (Submodule.finrank_mono (P.range_polarizationIn_le_span_coroot S)).antisymm

Premises used: LE.le.antisymm, Submodule.finrank_mono, RootPairing.range_polarizationIn_le_span_coroot
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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
S : Type u_5
inst_6 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsAnisotropic
⊢ IsReflexive R N

Tactic:
have : IsReflexive R N := .of_isPerfPair P.flip.toLinearMap
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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
S : Type u_5
inst_6 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsAnisotropic
this : IsReflexive R N
⊢ IsTorsionFree S N

Tactic:
have : Module.IsTorsionFree S N := .trans_faithfulSMul S R N
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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
S : Type u_5
inst_6 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsAnisotropic
this_1 : IsReflexive R N
this : IsTorsionFree S N
⊢ Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0

Tactic:
Finset.prod_ne_zero_iff.mpr fun i _ h ↦ ?_

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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
S : Type u_5
inst_6 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsAnisotropic
this_1 : IsReflexive R N
this : IsTorsionFree S N
refine :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      ∀
        (h :
          Eq.{u_5 + 1} (α := S)
            ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                    LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
                  (a : ↥(P.rootSpan S)) → S)
                (P.rootSpanMem S i) :
              S)
            (0 : S)),
        False
⊢ Ne.{u_5 + 1} (α := S)
    (∏ i : ι,
      (((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i))
    0

Tactic:
refine Finset.prod_ne_zero_iff.mpr fun i _ h ↦ ?_

Premises used: Iff.mpr, Finset.prod_ne_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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
S : Type u_5
inst_6 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsAnisotropic
this_1 : IsReflexive R N
this : IsTorsionFree S N
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h :
  Eq.{u_5 + 1} (α := S)
    ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) :
      S)
    (0 : S)
⊢ Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
              (a : ↥(P.rootSpan S)) → S)
            (P.rootSpanMem S i) :
          S) :
      R)
    (0 : R)

Tactic:
have := (FaithfulSMul.algebraMap_eq_zero_iff S R).mpr h
-- Module: Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
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
S : Type u_5
inst_6 : CommRing S
inst_7 : IsDomain R
inst_8 : IsDomain S
inst_9 : Algebra S R
inst_10 : FaithfulSMul S R
inst_11 : P.IsValuedIn S
inst_12 : Module S M
inst_13 : IsScalarTower S R M
inst_14 : Module S N
inst_15 : IsScalarTower S R N
inst_16 : P.IsAnisotropic
this_1 : IsReflexive R N
this_2 : IsTorsionFree S N
i : ι
h_1 : Membership.mem (γ := Finset ι) Finset.univ i
h :
  Eq.{u_5 + 1} (α := S)
    ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
            LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
          (a : ↥(P.rootSpan S)) → S)
        (P.rootSpanMem S i) :
      S)
    (0 : S)
this :
  Eq.{u_2 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((P.RootFormIn S : (a : ↥(P.rootSpan S)) → ↥(P.rootSpan S) →ₗ[S] S) (P.rootSpanMem S i) :
                LinearMap.{u_5, u_5, u_3, u_5} (RingHom.id S) (↥(P.rootSpan S)) S) :
              (a : ↥(P.rootSpan S)) → S)
            (P.rootSpanMem S i) :
          S) :
      R)
    (0 : R)
⊢ Eq.{u_2 + 1} (α := R)
    ((((P.RootForm : (a : M) → M →ₗ[R] R) (↑(P.rootSpanMem S i) : M) : M →ₗ[R] R) : (a : M) → R)
        (↑(P.rootSpanMem S i) : M) :
      R)
    (0 : R)

Tactic:
rw [algebraMap_rootFormIn] at this

Premises used: RootPairing.algebraMap_rootFormIn