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 : 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))
rw :
  LE.le (α := Submodule L N) (span L w)
    (span L (Set.range (ι := { x : N // x ∈ w }) (Subtype.val (p := fun (x : N) ↦ x ∈ w))))
rw₁ : LE.le (α := Submodule L N) (span L w) (span L {x : N | x ∈ w})
rw₂ rw₃ : LE.le (α := Submodule L N) (span L w) (span L w)
⊢ LE.le.{u_4} (α := Submodule L N) ⊤
    (span L (Set.range (ι := { x : N // x ∈ w }) (Subtype.val (p := fun (x : N) ↦ x ∈ w))))

Tactic:
rw [← hw₂, 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) ⋯
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₃ ⋯
have : ∀ (this : Fintype (↑w : Type u_4)), Membership.mem (γ := Submodule K M) (span K v) m
⊢ Membership.mem (γ := Submodule K M) (span K v) m

Tactic:
have : Fintype w := Set.Finite.fintype <| Module.Finite.finite_basis bN
-- 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)
rw : finrank L M = Fintype.card.{u_4} (↑w : Type u_4)
rw₁ : finrank L M = finrank L N
rw₂ rw₃ : finrank L N = finrank L N
⊢ Fintype.card.{u_3} (↑v : Type u_3) = Fintype.card.{u_4} (↑w : Type u_4)

Tactic:
rw [← Module.finrank_eq_card_basis b,
    ← Module.finrank_eq_card_basis bN, Module.finrank_of_isPerfPair p]

Premises used: Module.finrank_of_isPerfPair, 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' : 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)
have :
  ∀ (e : Equiv.{u_3 + 1, u_4 + 1} (↑v : Type u_3) (↑w : Type u_4)), Membership.mem (γ := Submodule K M) (span K v) m
⊢ Membership.mem (γ := Submodule K M) (span K v) m

Tactic:
have e : v ≃ w := Fintype.equivOfCardEq <| by rw [← Module.finrank_eq_card_basis b,
    ← Module.finrank_eq_card_basis bN, Module.finrank_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_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
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)

Tactic:
simp [bM, bN]
-- 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
⊢ ∀ (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)

Tactic:
have hbM (j : w) (x : M) (hx : x ∈ M') : bM.repr x j = p x (j : N) := by simp [bM, bN]
-- 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)
⊢ ∀ (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)

Tactic:
have hj (j : w) : bM.repr m j ∈ (algebraMap K L).range := (hbM _ _ hm) ▸ hp m hm j (hw₁ j.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)) ⊤
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)
simp :
  Membership.mem.{u_2, u_2} (α := L) (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L))
    ((((p.toPerfPair : (a : M) → Dual L N) ((b : (a : { x : M // x ∈ v }) → M) j) : Dual L N) : (a : N) → L)
        ((bN : (a : { x : N // x ∈ w }) → N) i : N) :
      L)
⊢ 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:
simp only [Basis.toMatrix, Basis.map_repr, LinearEquiv.symm_symm, LinearEquiv.trans_apply,
      Basis.dualBasis_repr]

Premises used: Module.Basis.map_repr, LinearEquiv.trans_apply, Module.Basis.toMatrix, LinearEquiv.symm_symm, Module.Basis.dualBasis_repr
-- 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 (α := M) M' ((b : (a : { x : M // x ∈ v }) → M) j : M)

Tactic:
simpa [b] using hv₁ j.2

Premises used: Subtype.property
-- 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 (α := N) N' ((bN : (a : { x : N // x ∈ w }) → N) i : N)

Tactic:
simpa [bN] using hw₁ i.2

Premises used: Subtype.property
-- 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.{u_2, u_2} (α := L) (γ := Subfield L) (RingHom.fieldRange.{u_1, u_2} (K := K) (algebraMap K L))
    ((((p.toPerfPair : (a : M) → Dual L N) ((b : (a : { x : M // x ∈ v }) → M) j) : Dual L N) : (a : N) → L)
        ((bN : (a : { x : N // x ∈ w }) → N) i : N) :
      L)

Tactic:
exact hp (b j) (by simpa [b] using hv₁ j.2) (bN i) (by simpa [bN] using hw₁ i.2)

Premises used: DFunLike.coe