awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_3 : 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 v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ (↑N' : Set N)
hw₂ : Eq (α := Submodule L N) (span L w) ⊤
hw₃ : LinearIndependent.{u_4, u_2, u_4} (ι := { x : N // x ∈ w }) L (Subtype.val (p := fun (x : N) ↦ x ∈ w))
bN : Basis { x : N // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype (↑w : Type u_4)
e : Equiv.{u_3 + 1, u_4 + 1} (↑v : Type u_3) (↑w : Type u_4)
bM : Basis.{u_4, u_2, u_3} { x : N // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM :
  ∀ (j : (↑w : Type u_4)) (x : M) (hx : x ∈ M'),
    Eq.{u_2 + 1} (α := L)
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) x : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
      ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) (↑j : N) : L)
hj :
  ∀ (j : (↑w : Type u_4)),
    Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) m : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
⊢ ∀ (i : (↑w : Type u_4)) (j : (↑v : Type u_3)),
    Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L))
      ((bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b : (a : { x : M // x ∈ v }) → M) i j)

Tactic:
replace hp (i : w) (j : v) :
      (bN.dualBasis.map p.toPerfPair.symm).toMatrix b i j ∈ (algebraMap K L).fieldRange := by
    simp only [Basis.toMatrix, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
      Basis.dualBasis_repr]
    exact hp (b j) (by simpa [b] using hv₁ j.2) (bN i) (by simpa [bN] using hw₁ i.2)
-- 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)) ⊤
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_3 : 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 v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ (↑N' : Set N)
hw₂ : Eq (α := Submodule L N) (span L w) ⊤
hw₃ : LinearIndependent.{u_4, u_2, u_4} (ι := { x : N // x ∈ w }) L (Subtype.val (p := fun (x : N) ↦ x ∈ w))
bN : Basis { x : N // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype (↑w : Type u_4)
e : Equiv.{u_3 + 1, u_4 + 1} (↑v : Type u_3) (↑w : Type u_4)
bM : Basis.{u_4, u_2, u_3} { x : N // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM :
  ∀ (j : (↑w : Type u_4)) (x : M) (hx : x ∈ M'),
    Eq.{u_2 + 1} (α := L)
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) x : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
      ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) (↑j : N) : L)
hj :
  ∀ (j : (↑w : Type u_4)),
    Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) m : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
hp :
  ∀ (i : (↑w : Type u_4)) (j : (↑v : Type u_3)),
    Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L))
      ((bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b : (a : { x : M // x ∈ v }) → M) i j)
i : { x : M // x ∈ v }
j : { x : N // x ∈ w }
⊢ HMul.hMul (α := Matrix.{u_3, u_4, u_2} (↑v : Type u_3) (↑w : Type u_4) L) (β :=
      Matrix.{u_4, u_3, u_2} (↑w : Type u_4) (↑v : Type u_3) L) (b.toMatrix (⇑bM : (a : { x : N // x ∈ w }) → M))
      ((bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b : (a : { x : M // x ∈ v }) → M)) =
    1

Tactic:
simp [bM]
-- 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)) ⊤
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_3 : 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 v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ (↑N' : Set N)
hw₂ : Eq (α := Submodule L N) (span L w) ⊤
hw₃ : LinearIndependent.{u_4, u_2, u_4} (ι := { x : N // x ∈ w }) L (Subtype.val (p := fun (x : N) ↦ x ∈ w))
bN : Basis { x : N // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype (↑w : Type u_4)
e : Equiv.{u_3 + 1, u_4 + 1} (↑v : Type u_3) (↑w : Type u_4)
bM : Basis.{u_4, u_2, u_3} { x : N // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM :
  ∀ (j : (↑w : Type u_4)) (x : M) (hx : x ∈ M'),
    Eq.{u_2 + 1} (α := L)
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) x : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
      ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) (↑j : N) : L)
hj :
  ∀ (j : (↑w : Type u_4)),
    Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) m : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
hp :
  ∀ (i : (↑w : Type u_4)) (j : (↑v : Type u_3)),
    Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L))
      ((bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b : (a : { x : M // x ∈ v }) → M) i j)
⊢ ∀ (i : { x : M // x ∈ v }) (j : { x : N // x ∈ w }),
    Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      (b.toMatrix (⇑bM : (a : { x : N // x ∈ w }) → M) i j)

Tactic:
have hA (i j) : b.toMatrix bM i j ∈ (algebraMap K L).range :=
    Matrix.mem_subfield_of_mul_eq_one_of_mem_subfield_left e _ (by simp [bM]) hp i j
-- 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)) ⊤
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_3 : 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 v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ (↑N' : Set N)
hw₂ : Eq (α := Submodule L N) (span L w) ⊤
hw₃ : LinearIndependent.{u_4, u_2, u_4} (ι := { x : N // x ∈ w }) L (Subtype.val (p := fun (x : N) ↦ x ∈ w))
bN : Basis { x : N // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype (↑w : Type u_4)
e : Equiv.{u_3 + 1, u_4 + 1} (↑v : Type u_3) (↑w : Type u_4)
bM : Basis.{u_4, u_2, u_3} { x : N // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM :
  ∀ (j : (↑w : Type u_4)) (x : M) (hx : x ∈ M'),
    Eq.{u_2 + 1} (α := L)
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) x : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
      ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) (↑j : N) : L)
hj :
  ∀ (j : (↑w : Type u_4)),
    Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) m : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
hp :
  ∀ (i : (↑w : Type u_4)) (j : (↑v : Type u_3)),
    Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L))
      ((bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b : (a : { x : M // x ∈ v }) → M) i j)
hA :
  ∀ (i : { x : M // x ∈ v }) (j : { x : N // x ∈ w }),
    Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      (b.toMatrix (⇑bM : (a : { x : N // x ∈ w }) → M) i j)
⊢ Eq (α := Submodule K M) (span K v) (span K (Set.range (ι := { x : M // x ∈ v }) (⇑b : (a : { x : M // x ∈ v }) → M)))

Tactic:
simp [b]
-- 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)) ⊤
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_3 : 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 v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ (↑N' : Set N)
hw₂ : Eq (α := Submodule L N) (span L w) ⊤
hw₃ : LinearIndependent.{u_4, u_2, u_4} (ι := { x : N // x ∈ w }) L (Subtype.val (p := fun (x : N) ↦ x ∈ w))
bN : Basis { x : N // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype (↑w : Type u_4)
e : Equiv.{u_3 + 1, u_4 + 1} (↑v : Type u_3) (↑w : Type u_4)
bM : Basis.{u_4, u_2, u_3} { x : N // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM :
  ∀ (j : (↑w : Type u_4)) (x : M) (hx : x ∈ M'),
    Eq.{u_2 + 1} (α := L)
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) x : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
      ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) (↑j : N) : L)
hj :
  ∀ (j : (↑w : Type u_4)),
    Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) m : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
hp :
  ∀ (i : (↑w : Type u_4)) (j : (↑v : Type u_3)),
    Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L))
      ((bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b : (a : { x : M // x ∈ v }) → M) i j)
hA :
  ∀ (i : { x : M // x ∈ v }) (j : { x : N // x ∈ w }),
    Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      (b.toMatrix (⇑bM : (a : { x : N // x ∈ w }) → M) i j)
⊢ Eq (α := Submodule K M) (span K v) (span K (Set.range (ι := { x : M // x ∈ v }) (⇑b : (a : { x : M // x ∈ v }) → M)))

Tactic:
have h_span : span K v = span K (Set.range b) := by simp [b]
-- 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)) ⊤
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_3 : 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 v'
m : M
hm : m ∈ M'
w : Set N
hw₁ : w ⊆ (↑N' : Set N)
hw₂ : Eq (α := Submodule L N) (span L w) ⊤
hw₃ : LinearIndependent.{u_4, u_2, u_4} (ι := { x : N // x ∈ w }) L (Subtype.val (p := fun (x : N) ↦ x ∈ w))
bN : Basis { x : N // x ∈ w } L N := Basis.mk hw₃ ⋯
this : Fintype (↑w : Type u_4)
e : Equiv.{u_3 + 1, u_4 + 1} (↑v : Type u_3) (↑w : Type u_4)
bM : Basis.{u_4, u_2, u_3} { x : N // x ∈ w } L M := bN.dualBasis.map p.toPerfPair.symm
hbM :
  ∀ (j : (↑w : Type u_4)) (x : M) (hx : x ∈ M'),
    Eq.{u_2 + 1} (α := L)
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) x : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
      ((((p : (a : M) → N →ₗ[L] L) x : N →ₗ[L] L) : (a : N) → L) (↑j : N) : L)
hj :
  ∀ (j : (↑w : Type u_4)),
    Membership.mem.{u_2, u_2} (α := L) (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      ((((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) m : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
            (a : { x : N // x ∈ w }) → L)
          j :
        L)
hp :
  ∀ (i : (↑w : Type u_4)) (j : (↑v : Type u_3)),
    Membership.mem (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L))
      ((bN.dualBasis.map p.toPerfPair.symm).toMatrix (⇑b : (a : { x : M // x ∈ v }) → M) i j)
hA :
  ∀ (i : { x : M // x ∈ v }) (j : { x : N // x ∈ w }),
    Membership.mem (γ := Subring L) (RingHom.range.{u_1, u_2} (R := K) (algebraMap K L))
      (b.toMatrix (⇑bM : (a : { x : N // x ∈ w }) → M) i j)
h_span :
  Eq (α := Submodule K M) (span K v) (span K (Set.range (ι := { x : M // x ∈ v }) (⇑b : (a : { x : M // x ∈ v }) → M)))
⊢ ∀ (i : { x : M // x ∈ v }),
    Membership.mem (γ := Set L) (Set.range.{u_2, u_1 + 1} (ι := K) (⇑(algebraMap K L) : (a : K) → L))
      (Matrix.mulVec.{u_2, u_3, u_4} (n := { x : N // x ∈ w }) (b.toMatrix (⇑bM : (a : { x : N // x ∈ w }) → M))
        (⇑((bM.repr : (a : M) → { x : N // x ∈ w } →₀ L) m : Finsupp.{u_4, u_2} { x : N // x ∈ w } L) :
          (a : { x : N // x ∈ w }) → L)
        i)

Tactic:
exact fun i ↦ Subring.sum_mem _ fun j _ ↦ Subring.mul_mem _ (hA i j) (hj j)

Premises used: Algebra.algebraMap, RingHom.range, Subring.sum_mem, Subring.mul_mem
-- 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)
obtain :
  ∀ (n : ℕ) (b : Basis (Fin n) L M) (b' : Basis.{0, u_1, u_3} (Fin n) K ↥M')
    (hb : ∀ (i : Fin n), Eq.{u_3 + 1} (α := M) ((b : (a : Fin n) → M) i : M) ((↑((b' : (a : Fin n) → ↥M') i) : M) : M)),
    finrank.{u_1, u_3} K ↥M' = finrank L M
⊢ finrank.{u_1, u_3} K ↥M' = finrank L M

Tactic:
obtain ⟨n, b, b', hb⟩ := exists_basis_basis_of_span_eq_top_of_mem_algebraMap p M' N' hM hN hp

Premises used: LinearMap.exists_basis_basis_of_span_eq_top_of_mem_algebraMap
-- 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)
n : ℕ
b : Basis (Fin n) L M
b' : Basis.{0, u_1, u_3} (Fin n) K ↥M'
hb : ∀ (i : Fin n), Eq.{u_3 + 1} (α := M) ((b : (a : Fin n) → M) i : M) ((↑((b' : (a : Fin n) → ↥M') i) : M) : M)
rw : finrank.{u_1, u_3} K ↥M' = Fintype.card (Fin n)
rw₁ rw₂ : Fintype.card (Fin n) = Fintype.card (Fin n)
⊢ finrank.{u_1, u_3} K ↥M' = finrank L M

Tactic:
rw [finrank_eq_card_basis b, finrank_eq_card_basis b']

Premises used: Module.finrank_eq_card_basis
-- 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' : Type u_5
N' : Type u_6
inst_11 : AddCommGroup M'
inst_12 : AddCommGroup N'
inst_13 : Module K M'
inst_14 : Module K N'
inst_15 : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective.{u_5 + 1, u_3 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_6 + 1, u_4 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hM : Eq (α := Submodule L M) (span L (↑i.range : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : 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) ((i : (a : M') → M) m) : N →ₗ[L] L) : (a : N) → L) ((j : (a : N') → N) n : N) : L)
suffices : FiniteDimensional K M'
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair

Tactic:
suffices FiniteDimensional K M' from .of_injective (p.restrictScalars_injective_aux i j hi hN hp)
    (p.flip.restrictScalars_injective_aux j i hj hM (fun m n ↦ hp n m))
-- 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' : Type u_5
N' : Type u_6
inst_11 : AddCommGroup M'
inst_12 : AddCommGroup N'
inst_13 : Module K M'
inst_14 : Module K N'
inst_15 : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective.{u_5 + 1, u_3 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_6 + 1, u_4 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hM : Eq (α := Submodule L M) (span L (↑i.range : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : 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) ((i : (a : M') → M) m) : N →ₗ[L] L) : (a : N) → L) ((j : (a : N') → N) n : N) : L)
m : M'
n : 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) ((i : (a : M') → M) m) : N →ₗ[L] L) : (a : N) → L) ((j : (a : N') → N) n : N) : L)

Tactic:
hp m n

Premises used: Set.Mem
-- 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' : Type u_5
N' : Type u_6
inst_11 : AddCommGroup M'
inst_12 : AddCommGroup N'
inst_13 : Module K M'
inst_14 : Module K N'
inst_15 : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] N
hi : Injective.{u_5 + 1, u_3 + 1} (α := M') (β := M) (⇑i : (a : M') → M)
hj : Injective.{u_6 + 1, u_4 + 1} (α := N') (β := N) (⇑j : (a : N') → N)
hM : Eq (α := Submodule L M) (span L (↑i.range : Set M)) ⊤
hN : Eq (α := Submodule L N) (span L (↑j.range : Set N)) ⊤
hp :
  ∀ (m : M') (n : 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) ((i : (a : M') → M) m) : N →ₗ[L] L) : (a : N) → L) ((j : (a : N') → N) n : N) : L)
m : M'
n : 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) ((i : (a : M') → M) m) : N →ₗ[L] L) : (a : N) → L) ((j : (a : N') → N) n : N) : L)

Tactic:
exact hp m n