awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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 K v'
have hv₄ : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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))
⊢ Subtype.val (p := fun (x : M) ↦ x ∈ v) = (⇑M'.subtype : (a : ↥M') → M) ∘ v'
have h : ∀ (x : { x : M // x ∈ v }), (↑x : M) = ((⇑M'.subtype : (a : ↥M') → M) ∘ v') x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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 v'
have hv₄ : LinearIndependent K (M := M) ((⇑M'.subtype : (a : ↥M') → M) ∘ v')
Tactic: rw [show ((↑) : v → M) = M'.subtype ∘ v' by ext; simp [v']] at hv₃
Cleared hypotheses: hv₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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) ⋯
⊢ ∃ (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)
have hv' : LinearIndependent K v'
Tactic: have hv' : LinearIndependent K v' := by
    replace hv₃ := hv₃.restrict_scalars (R := K) <| by
      simp_rw [← Algebra.algebraMap_eq_smul_one]
      exact FaithfulSMul.algebraMap_injective K L
    rw [show ((↑) : v → M) = M'.subtype ∘ v' by ext; simp [v']] at hv₃
    exact hv₃.of_comp
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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'
this : Eq (α := Submodule K ↥M') (span K (Set.range v')) ⊤
e : { x : M // x ∈ v } ≃ Fin (Nat.card.{u_3} { x : M // x ∈ v }) := Finite.equivFin { x : M // x ∈ v }
⊢ LE.le (α := Submodule K ↥M') ⊤ (span K (Set.range v'))
have rw : LE.le.{u_3} (α := Submodule K ↥M') ⊤ ⊤
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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'
⊢ ∃ (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)
have suffices : Eq (α := Submodule K ↥M') (span K (Set.range v')) ⊤
Tactic: suffices span K (Set.range v') = ⊤ by
    let e := (Module.Finite.finite_basis b).equivFin
    let b' : Basis _ K M' := Basis.mk hv' (by rw [this])
    exact ⟨_, b.reindex e, b'.reindex e, fun i ↦ by simp [b, b', v']⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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'
this : span K v = M'
⊢ Eq (α := Submodule K ↥M') (span K (Set.range v')) ⊤
have a : Submodule.map M'.subtype (span K (Set.range v')) = Submodule.map M'.subtype ⊤
Tactic: apply Submodule.map_injective_of_injective M'.injective_subtype
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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'
this : span K v = M'
⊢ Submodule.map M'.subtype (span K (Set.range v')) = Submodule.map M'.subtype ⊤
have a : span K ((fun (x : (↑v : Type u_3)) ↦ (M'.subtype : (a : ↥M') → M) (v' x)) '' univ) = Submodule.map M'.subtype ⊤
Tactic: rw [Submodule.map_span, ← Set.image_univ, Set.image_image]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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'
⊢ Eq (α := Submodule K ↥M') (span K (Set.range v')) ⊤
have suffices : span K v = M'
Tactic: suffices span K v = M' by
    apply Submodule.map_injective_of_injective M'.injective_subtype
    rw [Submodule.map_span, ← Set.image_univ, Set.image_image]
    simpa [v']
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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'
⊢ span K v = M'
have refine : ∀ (m : M) (hm : m ∈ M'), Membership.mem (γ := Submodule K M) (span K v) m
Tactic: refine le_antisymm (Submodule.span_le.mpr hv₁) fun m hm ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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'
⊢ Membership.mem (γ := Submodule K M) (span K v) m
have obtain : ∀ (w : Set N) (hw₁ : w ⊆ (↑N' : Set N)) (hw₂ : Eq (α := Submodule L N) (span L w) (span L (↑N' : Set N)))
  (hw₃ : LinearIndependent.{u_4, u_2, u_4} (ι := { x : N // x ∈ w }) L (Subtype.val (p := fun (x : N) ↦ x ∈ w))),
  Membership.mem (γ := Submodule K M) (span K v) m
Tactic: obtain ⟨w, hw₁, hw₂, hw₃⟩ := exists_linearIndependent L (N' : Set N)
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (hypothesis)
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) (span L (↑N' : Set N))
hw₃ : LinearIndependent.{u_4, u_2, u_4} (ι := { x : N // x ∈ w }) L (Subtype.val (p := fun (x : N) ↦ x ∈ w))
⊢ Membership.mem (γ := Submodule K M) (span K v) m
have hw₄ : Eq (α := Submodule L N) (span L w) ⊤
Tactic: rw [hN] at hw₂
Cleared hypotheses: hw₂, hw₃
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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))
⊢ LE.le.{u_4} (α := Submodule L N) ⊤
    (span L (Set.range (ι := { x : N // x ∈ w }) (Subtype.val (p := fun (x : N) ↦ x ∈ w))))
have 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))))
Tactic: rw [← hw₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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))))
⊢ LE.le.{u_4} (α := Submodule L N) ⊤
    (span L (Set.range (ι := { x : N // x ∈ w }) (Subtype.val (p := fun (x : N) ↦ x ∈ w))))
have rw₁ : LE.le (α := Submodule L N) (span L w) (span L {x : N | x ∈ w})
Tactic: rw [← hw₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.PerfectPairing.Restrict (goal)
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})
⊢ LE.le.{u_4} (α := Submodule L N) ⊤
    (span L (Set.range (ι := { x : N // x ∈ w }) (Subtype.val (p := fun (x : N) ↦ x ∈ w))))
have rw₂ : LE.le (α := Submodule L N) (span L w) (span L w)
Tactic: rw [← hw₂, Subtype.range_coe_subtype, Set.setOf_mem_eq]