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)) ⊤
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)
⊢ Membership.mem (γ := Submodule K M) (span K v) m
have h_span : 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]
-- 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)) ⊤
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)))
⊢ Membership.mem (γ := Submodule K M) (span K v) m
have rw : ∀ (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: rw [h_span, Basis.mem_span_iff_repr_mem, ← Basis.toMatrix_mulVec_repr bM b m]
-- 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)
⊢ finrank.{u_1, u_3} K ↥M' = finrank L M
have 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
Tactic: obtain ⟨n, b, b', hb⟩ := exists_basis_basis_of_span_eq_top_of_mem_algebraMap p M' N' hM hN hp
-- 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)
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
have rw : finrank.{u_1, u_3} K ↥M' = Fintype.card (Fin n)
Tactic: rw [finrank_eq_card_basis b, finrank_eq_card_basis b']
-- 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)
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)
⊢ finrank.{u_1, u_3} K ↥M' = finrank L M
have rw₁ : Fintype.card (Fin n) = Fintype.card (Fin n)
Tactic: rw [finrank_eq_card_basis b, finrank_eq_card_basis b']
-- 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' : 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)
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair
have suffices : FiniteDimensional K M'
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))
-- 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' : 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)
⊢ FiniteDimensional K M'
have obtain : ∀ (n : ℕ) (b' : Basis.{0, u_1, u_3} (Fin n) K ↥i.range), 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
-- 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' : 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 K M'
have this : FiniteDimensional.{u_1, u_3} K ↥i.range
Tactic: have : FiniteDimensional K (LinearMap.range i) := b'.finiteDimensional_of_finite
-- 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' : 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)
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair
have 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)))))
Tactic: have : (p.compl₁₂ (span L <| .range i).subtype (span L <| .range j).subtype).IsPerfPair :=
    .restrict _ _ _ (by simp) (by simp) (by simpa)
-- 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' : 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 ∘ₗ i.rangeRestrict)) : Set ↥(span L (Set.range (⇑i : (a : M') → M)))))
    ⊤
have 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))))) ⊤
Tactic: rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
-- 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' : 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 ∘ₗ j.rangeRestrict)) : Set ↥(span L (Set.range (⇑j : (a : N') → N)))))
    ⊤
have 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))))) ⊤
Tactic: rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
φ : ι → Type i
inst_3 : (i : ι) → AddCommMonoid (φ i)
inst_4 : (i : ι) → Module.{u, i} R (φ i)
f : (i : ι) → LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
⊢ (pi (φ := φ) f).ker = ⨅ (i : ι), (f i).ker
have h : ∀ (c : M₂), c ∈ (pi (φ := φ) f).ker ↔ Membership.mem (γ := Submodule R M₂) (⨅ (i : ι), (f i).ker) c
Tactic: ext c
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
φ : ι → Type i
inst_3 : (i : ι) → AddCommMonoid (φ i)
inst_4 : (i : ι) → Module.{u, i} R (φ i)
f : (i : ι) → LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
⊢ pi (φ := φ) f = 0 ↔ ∀ (i : ι), f i = 0
have simp : (∀ (x : M₂) (x_1 : ι),
    Eq.{i + 1} (α := φ x_1) ((f x_1 : (a : M₂) → φ x_1) x : φ x_1) ((0 : (a : M₂) → (i : ι) → φ i) x x_1 : φ x_1)) ↔
  ∀ (i : ι) (x : M₂),
    Eq.{i + 1} (α := φ i) ((f i : (a : M₂) → φ i) x : φ i)
      (((0 : LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)) : (a : M₂) → φ i) x : φ i)
Tactic: simp only [LinearMap.ext_iff, pi_apply, funext_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
φ : ι → Type i
inst_3 : (i : ι) → AddCommMonoid (φ i)
inst_4 : (i : ι) → Module.{u, i} R (φ i)
⊢ Eq (α := M₂ →ₗ[R] (i : ι) → φ i) (pi (φ := φ) fun (x : ι) ↦ 0) 0
have h : ∀ (x : M₂) (x_1 : ι),
  Eq.{i + 1} (α := φ x_1) ((pi (φ := φ) fun (x : ι) ↦ 0 : (a : M₂) → (i : ι) → φ i) x x_1 : φ x_1)
    ((0 : (a : M₂) → (i : ι) → φ i) x x_1 : φ x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (hypothesis)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
a : (i : ι) → φ i
h : Membership.mem (γ := Submodule R ((i : ι) → φ i)) (⨅ (i : ι), ker (proj (φ := φ) i)) a
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) ⊥ a
have h₁ : ∀ (i : ι), a i = 0
Tactic: simp only [mem_iInf, mem_ker, proj_apply] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R_1 : Type u
K : Type u'
M_1 : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι_1 : Type x
ι' : Type x'
inst : Semiring R_1
inst_1 : AddCommMonoid M₂
inst_2 : Module R_1 M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R_1 M₃
φ : ι_1 → Type i
inst_5 : (i : ι_1) → AddCommMonoid (φ i)
inst_6 : (i : ι_1) → Module.{u, i} R_1 (φ i)
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
inst_7 : Semiring S
inst_8 : AddCommMonoid M
inst_9 : AddCommMonoid N
inst_10 : SMul R M
inst_11 : SMul R N
inst_12 : Module S M
inst_13 : Module S N
inst_14 : CompatibleSMul M N R S
f : M →ₗ[S] ι → N
r : R
m : M
⊢ (f : (a : M) → ι → N) (r • m) = HSMul.hSMul (β := ι → N) r ((f : (a : M) → ι → N) m : ι → N)
have h : ∀ (i : ι), (f : (a : M) → ι → N) (r • m) i = HSMul.hSMul (β := ι → N) r ((f : (a : M) → ι → N) m : ι → N) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
K : Type u'
M : Type v
V : Type v'
M₂ : Type w
V₂ : Type w'
M₃ : Type y
V₃ : Type y'
M₄ : Type z
ι : Type x
ι' : Type x'
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
inst_3 : AddCommMonoid M₃
inst_4 : Module R M₃
φ : ι → Type i
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u, i} R (φ i)
f : M₂ →ₗ[R] M₃
I : Type u_1
c : R
h : I → M₂
⊢ (⇑f : (a : M₂) → M₃) ∘ (c • h) =
    HSMul.hSMul (α := R) (β := I → M₃) ((RingHom.id R : (a : R) → R) c : R) ((⇑f : (a : M₂) → M₃) ∘ h)
have h₁ : ∀ (x : I),
  ((⇑f : (a : M₂) → M₃) ∘ (c • h)) x =
    HSMul.hSMul (α := R) (β := I → M₃) ((RingHom.id R : (a : R) → R) c : R) ((⇑f : (a : M₂) → M₃) ∘ h) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
ι : Type x
φ : ι → Type i
inst : (i : ι) → AddCommMonoid (φ i)
inst_1 : Fintype ι
inst_2 : DecidableEq ι
v : (i : ι) → φ i
⊢ ∑ i : ι, Pi.single (M := φ) i (v i) = v
have h : ∀ (x : ι), (∑ i : ι, Pi.single (M := φ) i (v i)) x = v x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ LE.le (α := Submodule R ((i : ι) → φ i)) (⨆ i ∈ I, range (single R φ i)) (⨅ i ∈ J, ker (proj (φ := φ) i))
have refine : ∀ (i : ι) (hi : i ∈ I), Eq (α := Submodule R (φ i)) (comap (single R φ i) (⨅ i ∈ J, ker (proj (φ := φ) i))) ⊤
Tactic: refine iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Pi (goal)
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
inst_3 : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ Eq (α := Submodule R (φ i)) (comap (single R φ i) (⨅ i ∈ J, ker (proj (φ := φ) i))) ⊤
have simp : ∀ ⦃x : φ i⦄,
  Membership.mem (γ := Submodule R (φ i)) ⊤ x →
    ∀ (i_1 : ι) (i_2 : i_1 ∈ J),
      Eq (α := φ i_1) ((proj (φ := φ) i_1 ∘ₗ single R φ i : (a : φ i) → φ i_1) x : φ i_1) (0 : φ i_1)
Tactic: simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]