awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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 : P.IsRootSystem
⊢ Eq (α := Submodule R (Dual R N)) (span R (range P.root')) ⊤

Tactic:
simp [← rootSpan_map_toPerfPair]

Premises used: RootPairing.rootSpan_map_toPerfPair
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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 : P.IsRootSystem
⊢ Eq (α := Submodule R (Dual R M)) (span R (range P.coroot')) ⊤

Tactic:
span_root'_eq_top P.flip

Premises used: RootPairing.flip, RootPairing.span_root'_eq_top
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_7
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : FaithfulSMul S R
inst_8 : P.IsValuedIn S
inst_9 : IsDomain R
inst_10 : IsTorsionFree R M
inst_11 : NeZero.{u_2} (R := R) 2
i j : ι
⊢ P.pairingIn S i j = 0 ↔ P.pairingIn S j i = 0

Tactic:
simpa only [← FaithfulSMul.algebraMap_eq_zero_iff S R, algebraMap_pairingIn] using
    P.pairing_eq_zero_iff

Premises used: RootPairing.pairing_eq_zero_iff, RootPairing.algebraMap_pairingIn, FaithfulSMul.algebraMap_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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 : ι
S : Type u_7
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : P.IsValuedIn S
rw :
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairing j i) ((P.root : (a : ι) → M) i : M)) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
rw₁ :
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := M) ((algebraMap S R : (a : S) → R) (P.pairingIn S j i) : R)
        ((P.root : (a : ι) → M) i : M)) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
rw₂ rw₃ :
  HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M)) =
    HSub.hSub (α := M) ((P.root : (a : ι) → M) j : M)
      (HSMul.hSMul (β := M) (P.pairingIn S j i) ((P.root : (a : ι) → M) i : M))
⊢ (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.pairingIn S j i) ((P.root : (a : ι) → M) i : M))

Tactic:
rw [reflection_apply_root, ← P.algebraMap_pairingIn S, algebraMap_smul]

Premises used: RootPairing.algebraMap_pairingIn, algebraMap_smul, RootPairing.reflection_apply_root
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_7
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : P.IsValuedIn S
i j : ι
⊢ (algebraMap S R : (a : S) → R) (P.coxeterWeightIn S i j) = P.coxeterWeight i j

Tactic:
simp [coxeterWeightIn, coxeterWeight]

Premises used: RootPairing.coxeterWeight, RootPairing.coxeterWeightIn
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
R : Type u_2
M : Type u_4
N : Type u_5
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
S : Type u_6
inst_5 : CommRing S
inst_6 : Algebra S R
inst_7 : P.IsValuedIn S
inst_8 : Module S M
inst_9 : Module S N
inst_10 : IsScalarTower S R M
inst_11 : IsScalarTower S R N
x : M
hx : Membership.mem (γ := Submodule S M) (P.rootSpan S) x
y : N
hy : Membership.mem (γ := Submodule S N) (P.corootSpan S) y
⊢ ∀ (x : M),
    Membership.mem (γ := Set M) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) x →
      ∀ (y : N),
        Membership.mem (γ := Set N) (range.{u_5, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) y →
          Membership.mem (α := R) (γ := Submodule S R) (LinearMap.range (Algebra.linearMap S R))
            ((((LinearMap.restrictScalarsₗ S R N R S ∘ₗ
                          (↑S :
                              {S_1 : Type u_2} →
                                {M : Type u_4} →
                                  {M₂ : Type (max u_2 u_5)} →
                                    [inst : Semiring S] →
                                      [inst_12 : Semiring S_1] →
                                        [inst_13 : AddCommMonoid M] →
                                          [inst_14 : AddCommMonoid M₂] →
                                            [inst_15 : Module S M] →
                                              [inst_16 : Module S M₂] →
                                                [inst_17 : Module S_1 M] →
                                                  [inst_18 : Module S_1 M₂] →
                                                    [LinearMap.CompatibleSMul M M₂ S S_1] →
                                                      (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
                            P.toLinearMap :
                        (a : M) → N →ₗ[S] R)
                      x :
                    N →ₗ[S] R) :
                  (a : N) → R)
                y :
              R)

Tactic:
simpa using RootPairing.exists_value

Premises used: RootPairing.exists_value
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
hM : Eq (α := Submodule L M) (span L (↑(Q.rootSpan K) : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑(Q.corootSpan K) : Set N)) ⊤
hp :
  ∀ (x : M),
    Membership.mem (γ := Submodule K M) (Q.rootSpan K) x →
      ∀ (y : N),
        Membership.mem (γ := Submodule K N) (Q.corootSpan K) y →
          Membership.mem.{u_8, u_8} (α := L) (γ := Subring L) (RingHom.range.{u_7, u_8} (R := K) (algebraMap K L))
            ((((Q.toLinearMap : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
⊢ finrank.{u_7, u_4} K ↥(Q.rootSpan K) = finrank L M

Tactic:
rw [LinearMap.finrank_eq_of_isPerfPair Q.toLinearMap (Q.rootSpan K) (Q.corootSpan K)]

Premises used: RootPairing.toLinearMap, RootPairing.rootSpan, RootPairing.corootSpan, LinearMap.finrank_eq_of_isPerfPair
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
⊢ Eq (α := Submodule L M) (span L (↑(Q.rootSpan K) : Set M)) ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
⊢ Eq (α := Submodule L N) (span L (↑(Q.corootSpan K) : Set N)) ⊤

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
⊢ ∀ (x : M),
    Membership.mem (γ := Submodule K M) (Q.rootSpan K) x →
      ∀ (y : N),
        Membership.mem (γ := Submodule K N) (Q.corootSpan K) y →
          Membership.mem.{u_8, u_8} (α := L) (γ := Subring L) (RingHom.range.{u_7, u_8} (R := K) (algebraMap K L))
            ((((Q.toLinearMap : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)

Tactic:
Q.toLinearMap_apply_apply_mem_range_algebraMap K

Premises used: Set.Mem, RootPairing.toLinearMap_apply_apply_mem_range_algebraMap
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
⊢ ∀ (x : M),
    Membership.mem (γ := Submodule K M) (Q.rootSpan K) x →
      ∀ (y : N),
        Membership.mem (γ := Submodule K N) (Q.corootSpan K) y →
          Membership.mem.{u_8, u_8} (α := L) (γ := Subring L) (RingHom.range.{u_7, u_8} (R := K) (algebraMap K L))
            ((((Q.toLinearMap : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)

Tactic:
exact Q.toLinearMap_apply_apply_mem_range_algebraMap K

Premises used: RootPairing.toLinearMap_apply_apply_mem_range_algebraMap
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
K : Type u_7
L : Type u_8
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra K L
inst_5 : Module L M
inst_6 : Module L N
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
Q : RootPairing ι L M N
inst_11 : Q.IsRootSystem
inst_12 : Q.IsValuedIn K
⊢ finrank.{u_7, u_5} K ↥(Q.corootSpan K) = finrank L N

Tactic:
finrank_rootSpanIn K Q.flip

Premises used: Set.Mem, RootPairing.flip, setOf, RootPairing.finrank_rootSpanIn
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
L : Type u_8
inst_2 : Field L
inst_3 : Module L M
inst_4 : Module L N
Q : RootPairing ι L M N
inst_5 : Q.IsRootSystem
inst_6 : Finite ι
inst_7 : CharZero L
inst_8 : Q.IsCrystallographic
_i_1 : Module ℚ M := compHom M (algebraMap ℚ L)
_i : Module ℚ N := compHom N (algebraMap ℚ L)
⊢ IsAddTorsionFree M

Tactic:
have _i : IsAddTorsionFree M := .of_isTorsionFree L M
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
L : Type u_8
inst_2 : Field L
inst_3 : Module L M
inst_4 : Module L N
Q : RootPairing ι L M N
inst_5 : Q.IsRootSystem
inst_6 : Finite ι
inst_7 : CharZero L
inst_8 : Q.IsCrystallographic
_i_1 : Module ℚ M := compHom M (algebraMap ℚ L)
_i_2 : Module ℚ N := compHom N (algebraMap ℚ L)
_i : IsAddTorsionFree M
rw : finrank.{0, u_4} ℚ ↥(span ℚ (range.{u_4, u_1 + 1} (ι := ι) (⇑Q.root : (a : ι) → M))) = finrank L M
rw₁ rw₂ :
  finrank.{0, u_4} ℚ ↥(span ℚ (range.{u_4, u_1 + 1} (ι := ι) (⇑Q.root : (a : ι) → M))) =
    finrank.{0, u_4} ℚ ↥(Q.rootSpan ℚ)
⊢ finrank.{0, u_4} ℤ ↥(Q.rootSpan ℤ) = finrank L M

Tactic:
rw [← Submodule.finrank_span_eq_finrank_span ℤ ℚ, ← Q.finrank_rootSpanIn ℚ]

Premises used: Rat, Int, Submodule.finrank_span_eq_finrank_span, RootPairing.finrank_rootSpanIn
-- Module: Mathlib.LinearAlgebra.RootSystem.IsValuedIn
Goal:
ι : Type u_1
M : Type u_4
N : Type u_5
inst : AddCommGroup M
inst_1 : AddCommGroup N
L : Type u_8
inst_2 : Field L
inst_3 : Module L M
inst_4 : Module L N
Q : RootPairing ι L M N
inst_5 : Q.IsRootSystem
inst_6 : Finite ι
inst_7 : CharZero L
inst_8 : Q.IsCrystallographic
⊢ finrank.{0, u_5} ℤ ↥(Q.corootSpan ℤ) = finrank L N

Tactic:
Q.flip.finrank_rootSpanIn_int

Premises used: Set.Mem, RootPairing.finrank_rootSpanIn_int, RootPairing.flip, setOf
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
inst_3 : IsCancelMulZero R
inst_4 : NeZero.{u_1} (R := R) 2
hx : Dvd.dvd.{u_1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (2 : R)
contra : Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (0 : R)
⊢ False

Tactic:
simp [contra, two_ne_zero (α := R)] at hx

Premises used: two_ne_zero
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
a b : M
⊢ Exists.choose (p := fun (c : R) ↦
      HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (a + b) : R) =
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
      ⋯ =
    Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯ +
      Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) b : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯

Tactic:
hx.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
a b : M
refine :
  Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (a + b) : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯))
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯ +
        Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) b : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯))
⊢ Exists.choose (p := fun (c : R) ↦
      HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (a + b) : R) =
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
      ⋯ =
    Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯ +
      Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) b : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯

Tactic:
refine hx.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
r : R
a : M
⊢ Exists.choose (p := fun (c : R) ↦
      HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
      ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯)

Tactic:
hx.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
r : R
a : M
refine :
  Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯))
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
        (Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)))
⊢ Exists.choose (p := fun (c : R) ↦
      HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
        HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
      ⋯ =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
      (Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯)

Tactic:
refine hx.1.1 ?_

Premises used: LinearMap.IsReflective.regular, IsRegular.left
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
r : R
a : M
simp :
  HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      (Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯) =
    HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      (r •
        Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)
⊢ Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (Exists.choose (p := fun (c : R) ↦
        HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) (r • a) : R) =
          HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
        ⋯))
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      (HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) r : R)
        (Exists.choose (p := fun (c : R) ↦
          HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) a : R) =
            HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) c)
          ⋯)))

Tactic:
simp only [RingHom.id_apply]

Premises used: RingHom.id_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
y : M
⊢ HMul.hMul (α := R) (β := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R)
      ((coroot B hx : (a : M) → R) y : R) =
    HMul.hMul (α := R) (β := R) (2 : R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
(hx.dvd_two_mul y).choose_spec.symm

Premises used: Exists.choose_spec, LinearMap.IsReflective.dvd_two_mul, Classical.choose, Eq.symm
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
h :
  ∀ (y : M),
    Eq.{u_1 + 1} (α := R)
      ((HSMul.hSMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (coroot B hx) :
            (a : M) → R)
          y :
        R)
      ((HSMul.hSMul (α := ℕ) (β := M →ₗ[R] R) 2 ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)
⊢ HSMul.hSMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (coroot B hx) =
    HSMul.hSMul (α := ℕ) (β := M →ₗ[R] R) 2 ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R)

Tactic:
ext y
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
y : M
⊢ Eq.{u_1 + 1} (α := R)
    ((HSMul.hSMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) (coroot B hx) :
          (a : M) → R)
        y :
      R)
    ((HSMul.hSMul (α := ℕ) (β := M →ₗ[R] R) 2 ((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R)

Tactic:
simp [smul_apply, smul_eq_mul, nsmul_eq_mul, Nat.cast_ofNat, apply_self_mul_coroot_apply]

Premises used: Nat.cast_ofNat, LinearMap.IsReflective.apply_self_mul_coroot_apply, LinearMap.smul_apply, nsmul_eq_mul, smul_eq_mul
-- Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
B : M →ₗ[R] M →ₗ[R] R
x : M
hx : B.IsReflective x
⊢ Eq.{u_1 + 1} (α := R)
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1)
      ((coroot B hx : (a : M) → R) x))
    ((fun (x_1 : R) ↦ HMul.hMul (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) x : R) x_1) 2)

Tactic:
simp [mul_comm _ (B x x)]

Premises used: mul_comm, DFunLike.coe