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' : 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)
obtain : ∀ (n : ℕ) (b' : Basis.{0, u_1, u_3} (Fin n) K ↥i.range), FiniteDimensional K M'
⊢ FiniteDimensional K M'

Tactic:
obtain ⟨n, -, b', -⟩ := p.exists_basis_basis_of_span_eq_top_of_mem_algebraMap _ _ hM hN <| by
    rintro - ⟨m, rfl⟩ - ⟨n, rfl⟩
    exact hp m n

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' : 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)
n : ℕ
b' : Basis.{0, u_1, u_3} (Fin n) K ↥i.range
⊢ FiniteDimensional.{u_1, u_3} K ↥i.range

Tactic:
have : FiniteDimensional K (LinearMap.range i) := b'.finiteDimensional_of_finite
-- 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)
n : ℕ
b' : Basis.{0, u_1, u_3} (Fin n) K ↥i.range
this : FiniteDimensional.{u_1, u_3} K ↥i.range
⊢ FiniteDimensional K M'

Tactic:
Finite.equiv (LinearEquiv.ofInjective i hi).symm

Premises used: LinearEquiv.symm, LinearEquiv.ofInjective, Module.Finite.equiv
-- 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)
n : ℕ
b' : Basis.{0, u_1, u_3} (Fin n) K ↥i.range
this : FiniteDimensional.{u_1, u_3} K ↥i.range
⊢ FiniteDimensional K M'

Tactic:
exact Finite.equiv (LinearEquiv.ofInjective i hi).symm

Premises used: LinearEquiv.symm, LinearEquiv.ofInjective, Module.Finite.equiv
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
⊢ Injective.{u_3 + 1, u_3 + 1} (α := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (β := M)
    (⇑(Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) :
      (a : ↥(span L (Set.range (⇑i : (a : M') → M)))) → M)

Tactic:
simp
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
⊢ Injective.{u_4 + 1, u_4 + 1} (α := ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))) (β := N)
    (⇑(Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))) :
      (a : ↥(span L (Set.range (⇑j : (a : N') → N)))) → N)

Tactic:
simp
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
⊢ p.IsPerfectCompl
    (range (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))))
    (range (M := ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))

Tactic:
simpa
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
⊢ IsPerfPair (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (N :=
    ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (p.compl₁₂ (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))

Tactic:
have : (p.compl₁₂ (span L <| .range i).subtype (span L <| .range j).subtype).IsPerfPair :=
    .restrict _ _ _ (by simp) (by simp) (by simpa)
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
this :
  IsPerfPair (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (N :=
    ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (p.compl₁₂ (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))
⊢ Injective.{u_5 + 1, u_3 + 1} (α := M') (β := ↥i.range) (⇑i.rangeRestrict : (a : M') → ↥i.range)

Tactic:
simpa
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
this :
  IsPerfPair (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (N :=
    ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (p.compl₁₂ (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))
⊢ Injective.{u_6 + 1, u_4 + 1} (α := N') (β := ↥j.range) (⇑j.rangeRestrict : (a : N') → ↥j.range)

Tactic:
simpa
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
this :
  IsPerfPair (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (N :=
    ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (p.compl₁₂ (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))
rw :
  Eq (α := Submodule L ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
    (span L (↑(range (Submodule.inclusionSpan L i.range)) : Set ↥(span L (Set.range (⇑i : (a : M') → M))))) ⊤
⊢ Eq (α := Submodule L ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
    (span L
      (↑(range (Submodule.inclusionSpan L i.range ∘ₗ i.rangeRestrict)) : Set ↥(span L (Set.range (⇑i : (a : M') → M)))))
    ⊤

Tactic:
rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]

Premises used: LinearMap.range_comp_of_range_eq_top, LinearMap.range_rangeRestrict
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
this :
  IsPerfPair (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (N :=
    ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (p.compl₁₂ (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))
⊢ Eq (α := Submodule L ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
    (span L (↑(range (Submodule.inclusionSpan L i.range)) : Set ↥(span L (Set.range (⇑i : (a : M') → M))))) ⊤

Tactic:
(LinearMap.range i).span_range_inclusionSpan L

Premises used: Set.Mem, setOf, LinearMap.range, Set.range, Submodule.span_range_inclusionSpan
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
this :
  IsPerfPair (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (N :=
    ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (p.compl₁₂ (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))
⊢ Eq (α := Submodule L ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
    (span L (↑(range (Submodule.inclusionSpan L i.range)) : Set ↥(span L (Set.range (⇑i : (a : M') → M))))) ⊤

Tactic:
exact (LinearMap.range i).span_range_inclusionSpan L

Premises used: LinearMap.range, Submodule.span_range_inclusionSpan
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
this :
  IsPerfPair (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (N :=
    ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (p.compl₁₂ (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))
rw :
  Eq (α := Submodule L ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (span L (↑(range (Submodule.inclusionSpan L j.range)) : Set ↥(span L (Set.range (⇑j : (a : N') → N))))) ⊤
⊢ Eq (α := Submodule L ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (span L
      (↑(range (Submodule.inclusionSpan L j.range ∘ₗ j.rangeRestrict)) : Set ↥(span L (Set.range (⇑j : (a : N') → N)))))
    ⊤

Tactic:
rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]

Premises used: LinearMap.range_comp_of_range_eq_top, LinearMap.range_rangeRestrict
-- 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)
hij : p.IsPerfectCompl (span L (↑i.range : Set M)) (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)
this :
  IsPerfPair (M := ↥(span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M)))) (N :=
    ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (p.compl₁₂ (Submodule.subtype (span L (Set.range.{u_3, u_5 + 1} (ι := M') (⇑i : (a : M') → M))))
      (Submodule.subtype (span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N)))))
⊢ Eq (α := Submodule L ↥(span L (Set.range.{u_4, u_6 + 1} (ι := N') (⇑j : (a : N') → N))))
    (span L (↑(range (Submodule.inclusionSpan L j.range)) : Set ↥(span L (Set.range (⇑j : (a : N') → N))))) ⊤

Tactic:
(LinearMap.range j).span_range_inclusionSpan L

Premises used: Set.Mem, setOf, LinearMap.range, Set.range, Submodule.span_range_inclusionSpan