awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
h :
  ∀ (g : Dual S N'),
    ∃ (m : M'),
      Eq (α := N' →ₗ[S] R)
        ((↑S :
              {S_1 : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_1} →
                    [inst : Semiring S] →
                      [inst_19 : Semiring S_1] →
                        [inst_20 : AddCommMonoid M] →
                          [inst_21 : AddCommMonoid M₂] →
                            [inst_22 : Module S M] →
                              [inst_23 : Module S M₂] →
                                [inst_24 : Module S_1 M] →
                                  [inst_25 : Module S_1 M₂] →
                                    [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (S := R) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m)) ∘ₗ
          j)
        (Algebra.linearMap S R ∘ₗ g)
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
g : Dual S N'
m : M'
hm :
  Eq (α := N' →ₗ[S] R)
    ((↑S :
          {S_1 : Type u_1} →
            {M : Type u_3} →
              {M₂ : Type u_1} →
                [inst : Semiring S] →
                  [inst_19 : Semiring S_1] →
                    [inst_20 : AddCommMonoid M] →
                      [inst_21 : AddCommMonoid M₂] →
                        [inst_22 : Module S M] →
                          [inst_23 : Module S M₂] →
                            [inst_24 : Module S_1 M] →
                              [inst_25 : Module S_1 M₂] →
                                [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (S := R) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m)) ∘ₗ
      j)
    (Algebra.linearMap S R ∘ₗ g)
n : N'
h₁ :
  Eq.{u_1 + 1} (α := R)
    ((algebraMap S R : (a : S) → R)
        ((((i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp : (a : M') → N' →ₗ[S] S) m : N' →ₗ[S] S) :
              (a : N') → S)
            n :
          S) :
      R)
    ((algebraMap S R : (a : S) → R) ((g : (a : N') → S) n : S) : R)
⊢ Eq.{u_4 + 1} (α := S)
    ((((i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp : (a : M') → N' →ₗ[S] S) m : N' →ₗ[S] S) :
          (a : N') → S)
        n :
      S)
    ((g : (a : N') → S) n : S)

Tactic:
apply FaithfulSMul.algebraMap_injective S R

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
p : M →ₗ[R] N →ₗ[R] R
inst_5 : p.IsPerfPair
S : Type u_4
M' : Type u_5
N' : Type u_6
inst_6 : CommRing S
inst_7 : IsDomain S
inst_8 : Algebra S R
inst_9 : Module S M
inst_10 : Module S N
inst_11 : IsScalarTower S R M
inst_12 : IsScalarTower S R N
inst_13 : IsTorsionFree S R
inst_14 : Nontrivial R
inst_15 : AddCommGroup M'
inst_16 : Module S M'
inst_17 : AddCommGroup N'
inst_18 : Module S N'
i : M' →ₗ[S] M
j : N' →ₗ[S] N
h :
  ∀ (g : Dual S N'),
    ∃ (m : M'),
      Eq (α := N' →ₗ[S] R)
        ((↑S :
              {S_1 : Type u_1} →
                {M : Type u_3} →
                  {M₂ : Type u_1} →
                    [inst : Semiring S] →
                      [inst_19 : Semiring S_1] →
                        [inst_20 : AddCommMonoid M] →
                          [inst_21 : AddCommMonoid M₂] →
                            [inst_22 : Module S M] →
                              [inst_23 : Module S M₂] →
                                [inst_24 : Module S_1 M] →
                                  [inst_25 : Module S_1 M₂] →
                                    [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
            (S := R) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m)) ∘ₗ
          j)
        (Algebra.linearMap S R ∘ₗ g)
hp :
  ∀ (m : M') (n : N'),
    Membership.mem.{u_1, u_1} (α := R) (γ := Subring R) (RingHom.range.{u_4, u_1} (R := S) (algebraMap S R))
      ((((p : (a : M) → N →ₗ[R] R) ((i : (a : M') → M) m) : N →ₗ[R] R) : (a : N) → R) ((j : (a : N') → N) n : N) : R)
g : Dual S N'
m : M'
hm :
  Eq (α := N' →ₗ[S] R)
    ((↑S :
          {S_1 : Type u_1} →
            {M : Type u_3} →
              {M₂ : Type u_1} →
                [inst : Semiring S] →
                  [inst_19 : Semiring S_1] →
                    [inst_20 : AddCommMonoid M] →
                      [inst_21 : AddCommMonoid M₂] →
                        [inst_22 : Module S M] →
                          [inst_23 : Module S M₂] →
                            [inst_24 : Module S_1 M] →
                              [inst_25 : Module S_1 M₂] →
                                [CompatibleSMul M M₂ S S_1] → (fₗ : M →ₗ[S_1] M₂) → M →ₗ[S] M₂)
        (S := R) ((p.toPerfPair : (a : M) → Dual R N) ((i : (a : M') → M) m)) ∘ₗ
      j)
    (Algebra.linearMap S R ∘ₗ g)
n : N'
⊢ Eq.{u_1 + 1} (α := R)
    ((Algebra.linearMap S R : (a : S) → R)
        ((((i.restrictScalarsRange₂ j (Algebra.linearMap S R) ⋯ p hp : (a : M') → N' →ₗ[S] S) m : N' →ₗ[S] S) :
              (a : N') → S)
            n :
          S) :
      R)
    ((algebraMap S R : (a : S) → R) ((g : (a : N') → S) n : S) : R)

Tactic:
simpa using LinearMap.congr_fun hm n

Premises used: LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
⊢ IsReflexive L M

Tactic:
have : IsReflexive L M := .of_isPerfPair p
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this : IsReflexive L M
⊢ IsReflexive L N

Tactic:
have : IsReflexive L N := .of_isPerfPair p.flip
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this : IsReflexive L N
obtain :
  ∀ (v : Set M) (hv₁ : v ⊆ (↑M' : Set M)) (hv₂ : Eq (α := Submodule L M) (span L v) (span L (↑M' : Set M)))
    (hv₃ : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))),
    ∃ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis.{0, u_1, u_3} (Fin n) K ↥M'),
      ∀ (i : Fin n), Eq.{u_3 + 1} (α := M) ((b : (a : Fin n) → M) i : M) ((↑((b' : (a : Fin n) → ↥M') i) : M) : M)
⊢ ∃ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis.{0, u_1, u_3} (Fin n) K ↥M'),
    ∀ (i : Fin n), Eq.{u_3 + 1} (α := M) ((b : (a : Fin n) → M) i : M) ((↑((b' : (a : Fin n) → ↥M') i) : M) : M)

Tactic:
obtain ⟨v, hv₁, hv₂, hv₃⟩ := exists_linearIndependent L (M' : Set M)

Premises used: exists_linearIndependent, SetLike.coe
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) (span L (↑M' : Set M))
hv₃ : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
⊢ Eq (α := Submodule L M) (span L v) ⊤

Tactic:
rw [hM] at hv₂
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) (span L (↑M' : Set M))
hv₃ : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
hv₄ : Eq (α := Submodule L M) (span L v) ⊤
⊢ LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))

Tactic:
rw [hM] at hv₂
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃ : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
rw :
  LE.le (α := Submodule L M) (span L v)
    (span L (Set.range (ι := { x : M // x ∈ v }) (Subtype.val (p := fun (x : M) ↦ x ∈ v))))
rw₁ : LE.le (α := Submodule L M) (span L v) (span L {x : M | x ∈ v})
rw₂ rw₃ : LE.le (α := Submodule L M) (span L v) (span L v)
⊢ LE.le.{u_3} (α := Submodule L M) ⊤
    (span L (Set.range (ι := { x : M // x ∈ v }) (Subtype.val (p := fun (x : M) ↦ x ∈ v))))

Tactic:
rw [← hv₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]

Premises used: Subtype.range_coe_subtype, Set.setOf_mem_eq
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this_2 : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃ : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
b : Basis { x : M // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype (↑v : Type u_3)
v' : (↑v : Type u_3) → ↥M' := fun (i : (↑v : Type u_3)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ M') (↑i : M) ⋯
simp_rw : Injective.{u_1 + 1, u_2 + 1} (β := L) fun (r : K) ↦ (algebraMap K L : (a : K) → L) r
⊢ Injective.{u_1 + 1, u_2 + 1} (β := L) fun (r : K) ↦ HSMul.hSMul (β := L) r 1

Tactic:
simp_rw [← Algebra.algebraMap_eq_smul_one]

Premises used: Algebra.algebraMap_eq_smul_one
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this_2 : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃ : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
b : Basis { x : M // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype (↑v : Type u_3)
v' : (↑v : Type u_3) → ↥M' := fun (i : (↑v : Type u_3)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ M') (↑i : M) ⋯
⊢ Injective.{u_1 + 1, u_2 + 1} (β := L) fun (r : K) ↦ (algebraMap K L : (a : K) → L) r

Tactic:
FaithfulSMul.algebraMap_injective K L

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this_2 : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃ : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
b : Basis { x : M // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype (↑v : Type u_3)
v' : (↑v : Type u_3) → ↥M' := fun (i : (↑v : Type u_3)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ M') (↑i : M) ⋯
⊢ Injective.{u_1 + 1, u_2 + 1} (β := L) fun (r : K) ↦ (algebraMap K L : (a : K) → L) r

Tactic:
exact FaithfulSMul.algebraMap_injective K L

Premises used: FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this_2 : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃ : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
b : Basis { x : M // x ∈ v } L M := Basis.mk hv₃ ⋯
this : Fintype (↑v : Type u_3)
v' : (↑v : Type u_3) → ↥M' := fun (i : (↑v : Type u_3)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ M') (↑i : M) ⋯
⊢ LinearIndependent.{u_3, u_1, u_3} (ι := { x : M // x ∈ v }) K (Subtype.val (p := fun (x : M) ↦ x ∈ v))

Tactic:
replace hv₃ := hv₃.restrict_scalars (R := K) <| by
      simp_rw [← Algebra.algebraMap_eq_smul_one]
      exact FaithfulSMul.algebraMap_injective K L
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this_2 : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃_1 : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
b : Basis { x : M // x ∈ v } L M := Basis.mk hv₃_1 ⋯
this : Fintype (↑v : Type u_3)
v' : (↑v : Type u_3) → ↥M' := fun (i : (↑v : Type u_3)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ M') (↑i : M) ⋯
hv₃ : LinearIndependent.{u_3, u_1, u_3} (ι := { x : M // x ∈ v }) K (Subtype.val (p := fun (x : M) ↦ x ∈ v))
h : ∀ (x : { x : M // x ∈ v }), (↑x : M) = ((⇑M'.subtype : (a : ↥M') → M) ∘ v') x
⊢ Subtype.val (p := fun (x : M) ↦ x ∈ v) = (⇑M'.subtype : (a : ↥M') → M) ∘ v'

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this_2 : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃_1 : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
b : Basis { x : M // x ∈ v } L M := Basis.mk hv₃_1 ⋯
this : Fintype (↑v : Type u_3)
v' : (↑v : Type u_3) → ↥M' := fun (i : (↑v : Type u_3)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ M') (↑i : M) ⋯
hv₃ : LinearIndependent.{u_3, u_1, u_3} (ι := { x : M // x ∈ v }) K (Subtype.val (p := fun (x : M) ↦ x ∈ v))
x : { x : M // x ∈ v }
⊢ (↑x : M) = ((⇑M'.subtype : (a : ↥M') → M) ∘ v') x

Tactic:
simp [v']
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this_2 : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃_1 : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
b : Basis { x : M // x ∈ v } L M := Basis.mk hv₃_1 ⋯
this : Fintype (↑v : Type u_3)
v' : (↑v : Type u_3) → ↥M' := fun (i : (↑v : Type u_3)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ M') (↑i : M) ⋯
hv₃ : LinearIndependent.{u_3, u_1, u_3} (ι := { x : M // x ∈ v }) K (Subtype.val (p := fun (x : M) ↦ x ∈ v))
⊢ LinearIndependent K (M := M) ((⇑M'.subtype : (a : ↥M') → M) ∘ v')

Tactic:
rw [show ((↑) : v → M) = M'.subtype ∘ v' by ext; simp [v']] at hv₃
-- Module: Mathlib.LinearAlgebra.PerfectPairing.Restrict
Goal:
K : Type u_1
L : Type u_2
M : Type u_3
N : Type u_4
inst : Field K
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
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
p : M →ₗ[L] N →ₗ[L] L
inst_10 : p.IsPerfPair
M' : Submodule K M
N' : Submodule K N
hM : Eq (α := Submodule L M) (span L (↑M' : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑N' : Set N)) ⊤
hp :
  ∀ x ∈ M',
    ∀ y ∈ N',
      Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
        ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) y : L)
this_1 : IsReflexive L M
this_2 : IsReflexive L N
v : Set M
hv₁ : v ⊆ (↑M' : Set M)
hv₂ : Eq (α := Submodule L M) (span L v) ⊤
hv₃_1 : LinearIndependent.{u_3, u_2, u_3} (ι := { x : M // x ∈ v }) L (Subtype.val (p := fun (x : M) ↦ x ∈ v))
b : Basis { x : M // x ∈ v } L M := Basis.mk hv₃_1 ⋯
this : Fintype (↑v : Type u_3)
v' : (↑v : Type u_3) → ↥M' := fun (i : (↑v : Type u_3)) ↦ Subtype.mk (p := fun (x : M) ↦ x ∈ M') (↑i : M) ⋯
hv₃ : LinearIndependent K (M := M) ((⇑M'.subtype : (a : ↥M') → M) ∘ v')
⊢ LinearIndependent K v'

Tactic:
hv₃.of_comp

Premises used: LinearIndependent.of_comp