awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i : ι
rw : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑2 : K) : L) (2 : L)
rw₁ : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) (↑2 : K) : L) ((↑2 : L) : L)
rw₂ rw₃ : Eq.{u_2 + 1} (α := L) (↑2 : L) (↑2 : L)
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) 2 : L) (2 : L)

Tactic:
rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]

Premises used: Int.cast_two, map_intCast
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i : ι
⊢ Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) 2 : L) (2 : L)

Tactic:
have : algebraMap K L 2 = 2 := by
      rw [← Int.cast_two (R := K), ← Int.cast_two (R := L), map_intCast]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i : ι
this : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) 2 : L) (2 : L)
⊢ Eq.{u_2 + 1} (α := L)
    ((algebraMap K L : (a : K) → L)
        ((((LinearMap.restrictScalarsRange₂
                      (Submodule.subtype (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
                      (Submodule.subtype (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
                      (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯ :
                    (a : ↥(span K (range (⇑P.root : (a : ι) → M)))) →
                      ↥(span K (range (⇑P.coroot : (a : ι) → N))) →ₗ[K] K)
                  (({
                        toFun := fun (i : ι) ↦
                          Subtype.mk (p := fun (x : M) ↦
                            Membership.mem (γ := Submodule K M)
                              (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                            ((P.root : (a : ι) → M) i) ⋯,
                        inj' := ⋯ } :
                      (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
                    i) :
                LinearMap.{u_5, u_5, u_4, u_5} (RingHom.id K)
                  (↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) K) :
              (a : ↥(span K (range (⇑P.coroot : (a : ι) → N)))) → K)
            (({
                    toFun := fun (i : ι) ↦
                      Subtype.mk (p := fun (x : N) ↦
                        Membership.mem (γ := Submodule K N)
                          (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x)
                        ((P.coroot : (a : ι) → N) i) ⋯,
                    inj' := ⋯ } :
                  (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))
                i :
              ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) :
          K) :
      L)
    ((algebraMap K L : (a : K) → L) 2 : L)

Tactic:
simp [this]
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i : ι
this : Eq.{u_2 + 1} (α := L) ((algebraMap K L : (a : K) → L) 2 : L) (2 : L)
⊢ Eq.{u_5 + 1} (α := K)
    ((((LinearMap.restrictScalarsRange₂
                  (Submodule.subtype (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
                  (Submodule.subtype (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
                  (Algebra.linearMap K L) ⋯ P.toLinearMap ⋯ :
                (a : ↥(span K (range (⇑P.root : (a : ι) → M)))) → ↥(span K (range (⇑P.coroot : (a : ι) → N))) →ₗ[K] K)
              (({
                    toFun := fun (i : ι) ↦
                      Subtype.mk (p := fun (x : M) ↦
                        Membership.mem (γ := Submodule K M)
                          (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x)
                        ((P.root : (a : ι) → M) i) ⋯,
                    inj' := ⋯ } :
                  (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
                i) :
            LinearMap.{u_5, u_5, u_4, u_5} (RingHom.id K)
              (↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) K) :
          (a : ↥(span K (range (⇑P.coroot : (a : ι) → N)))) → K)
        (({
                toFun := fun (i : ι) ↦
                  Subtype.mk (p := fun (x : N) ↦
                    Membership.mem (γ := Submodule K N)
                      (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x)
                    ((P.coroot : (a : ι) → N) i) ⋯,
                inj' := ⋯ } :
              (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))
            i :
          ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) :
      K)
    (2 : K)

Tactic:
exact FaithfulSMul.algebraMap_injective K L <| by simp [this]

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
rw :
  Eq.{u_3 + 1} (α := Submodule K ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span K
      (range.{u_3, u_1 + 1} (ι := ι)
        (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))))
    (span K
      {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)})
⊢ Eq.{u_3 + 1} (α := Submodule K ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span K
      (range.{u_3, u_1 + 1} (ι := ι)
        (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))))
    ⊤

Tactic:
rw [← span_setOf_mem_eq_top]

Premises used: Submodule.span_setOf_mem_eq_top
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
e_s :
  Eq.{u_3 + 1} (α := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (range.{u_3, u_1 + 1} (ι := ι)
      (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
        (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M)))))
    {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)}
⊢ Eq.{u_3 + 1} (α := Submodule K ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (span K
      (range.{u_3, u_1 + 1} (ι := ι)
        (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))))
    (span K
      {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)})

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
e_s :
  ∀ (x : M)
    (hx : Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x),
    Membership.mem (γ := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
        (range.{u_3, u_1 + 1} (ι := ι)
          (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
            (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M)))))
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x
          hx) ↔
      Membership.mem (γ := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
        {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
          Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)}
        (Subtype.mk (p := fun (x : M) ↦
          Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x hx)
⊢ Eq.{u_3 + 1} (α := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
    (range.{u_3, u_1 + 1} (ι := ι)
      (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
        (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M)))))
    {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
      Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)}

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
x : M
hx : Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x
⊢ Membership.mem (γ := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
      (range.{u_3, u_1 + 1} (ι := ι)
        (⇑(root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M)))))
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x hx) ↔
    Membership.mem (γ := Set ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))))
      {x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) |
        Membership.mem (γ := Set M) (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)) (↑x : M)}
      (Subtype.mk (p := fun (x : M) ↦
        Membership.mem (γ := Submodule K M) (span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M))) x) x hx)

Tactic:
simp [restrictScalars']

Premises used: RootPairing.restrictScalars'
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
rw :
  Eq.{u_4 + 1} (α := Submodule K ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    (span K
      (range.{u_4, u_1 + 1} (ι := ι)
        (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))))
    (span K
      {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
        Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)})
⊢ Eq.{u_4 + 1} (α := Submodule K ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    (span K
      (range.{u_4, u_1 + 1} (ι := ι)
        (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))))
    ⊤

Tactic:
rw [← span_setOf_mem_eq_top]

Premises used: Submodule.span_setOf_mem_eq_top
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
e_s :
  Eq.{u_4 + 1} (α := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    (range.{u_4, u_1 + 1} (ι := ι)
      (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
        (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N)))))
    {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
      Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)}
⊢ Eq.{u_4 + 1} (α := Submodule K ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    (span K
      (range.{u_4, u_1 + 1} (ι := ι)
        (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))))
    (span K
      {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
        Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)})

Tactic:
congr
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
e_s :
  ∀ (x : N)
    (hx : Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x),
    Membership.mem (γ := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
        (range.{u_4, u_1 + 1} (ι := ι)
          (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
            (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N)))))
        (Subtype.mk (p := fun (x : N) ↦
          Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x) x
          hx) ↔
      Membership.mem (γ := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
        {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
          Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)}
        (Subtype.mk (p := fun (x : N) ↦
          Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x) x
          hx)
⊢ Eq.{u_4 + 1} (α := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
    (range.{u_4, u_1 + 1} (ι := ι)
      (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
        (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N)))))
    {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
      Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)}

Tactic:
ext ⟨x, hx⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
x : N
hx : Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x
⊢ Membership.mem (γ := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
      (range.{u_4, u_1 + 1} (ι := ι)
        (⇑(coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K)) :
          (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N)))))
      (Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x) x
        hx) ↔
    Membership.mem (γ := Set ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))))
      {x : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) |
        Membership.mem (γ := Set N) (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)) (↑x : N)}
      (Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Submodule K N) (span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N))) x) x hx)

Tactic:
simp [restrictScalars']

Premises used: RootPairing.restrictScalars'
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
x : ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))
y : ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))
⊢ Eq.{u_2 + 1} (α := L)
    ((algebraMap K L : (a : K) → L)
        ((((toLinearMap (P.restrictScalars' K) :
                    (a : ↥(span K (range (⇑P.root : (a : ι) → M)))) →
                      ↥(span K (range (⇑P.coroot : (a : ι) → N))) →ₗ[K] K)
                  x :
                LinearMap.{u_5, u_5, u_4, u_5} (RingHom.id K)
                  (↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) K) :
              (a : ↥(span K (range (⇑P.coroot : (a : ι) → N)))) → K)
            y :
          K) :
      L)
    ((((P.toLinearMap : (a : M) → N →ₗ[L] L) (↑x : M) : N →ₗ[L] L) : (a : N) → L) (↑y : N) : L)

Tactic:
simp [restrictScalars']

Premises used: RootPairing.restrictScalars'
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i : ι
⊢ Eq.{u_3 + 1} (α := M)
    ((↑(((root (N := ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K) :
                Embedding.{u_1 + 1, u_3 + 1} ι ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) :
              (a : ι) → ↥(span K (range (⇑P.root : (a : ι) → M))))
            i) :
        M) :
      M)
    ((P.root : (a : ι) → M) i : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i : ι
⊢ Eq.{u_4 + 1} (α := N)
    ((↑(((coroot (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (P.restrictScalars' K) :
                Embedding.{u_1 + 1, u_4 + 1} ι ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) :
              (a : ι) → ↥(span K (range (⇑P.coroot : (a : ι) → N))))
            i) :
        N) :
      N)
    ((P.coroot : (a : ι) → N) i : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseChange
Goal:
ι : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field L
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module L M
inst_4 : Module L N
P : RootPairing ι L M N
K : Type u_5
inst_5 : Field K
inst_6 : Algebra K L
inst_7 : Module K M
inst_8 : Module K N
inst_9 : IsScalarTower K L M
inst_10 : IsScalarTower K L N
inst_11 : P.IsBalanced
inst_12 : P.IsValuedIn K
i j : ι
⊢ (algebraMap K L : (a : K) → L)
      (pairing (M := ↥(span K (range.{u_3, u_1 + 1} (ι := ι) (⇑P.root : (a : ι) → M)))) (N :=
        ↥(span K (range.{u_4, u_1 + 1} (ι := ι) (⇑P.coroot : (a : ι) → N)))) (P.restrictScalars' K) i j) =
    P.pairing i j

Tactic:
simp only [pairing, restrictScalars_toLinearMap_apply_apply, restrictScalars_coe_root,
    restrictScalars_coe_coroot]

Premises used: RootPairing.restrictScalars_coe_coroot, RootPairing.pairing, RootPairing.restrictScalars_coe_root, RootPairing.restrictScalars_toLinearMap_apply_apply
-- Module: Mathlib.LinearAlgebra.RootSystem.BaseExists
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : Finite ι
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 : LinearOrder S
inst_7 : AddCommGroup S
inst_8 : IsOrderedAddMonoid S
f : M →+ S
inst_9 : CharZero R
inst_10 : IsDomain R
inst_11 : P.IsCrystallographic
hf : ∀ (i : ι), Ne.{u_5 + 1} (α := S) ((f : (a : M) → S) ((P.root : (a : ι) → M) i : M) : S) (0 : S)
_i : InvolutiveNeg ι := P.indexNeg
i : ι
hi : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) i
j : ι
hj : Membership.mem (γ := Set ι) (baseOf (⇑P.root : (a : ι) → M) f) j
hne : i ≠ j
⊢ ∀ (i : ι), Eq.{u_3 + 1} (α := M) ((P.root : (a : ι) → M) (-i) : M) (-(P.root : (a : ι) → M) i : M)

Tactic:
simp