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)
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:
exact (LinearMap.range j).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)))))
x : M'
y : N'
⊢ ∀ x ∈ (↑i.range : Set M),
    ∀ y ∈ (↑j.range : Set N),
      Membership.mem (α := L) (γ := Submodule K L) (range (Algebra.linearMap K L))
        ((((restrictScalarsₗ K L N L K ∘ₗ
                      (↑K :
                          {S : Type u_2} →
                            {M : Type u_3} →
                              {M₂ : Type (max u_2 u_4)} →
                                [inst : Semiring K] →
                                  [inst_16 : Semiring S] →
                                    [inst_17 : AddCommMonoid M] →
                                      [inst_18 : AddCommMonoid M₂] →
                                        [inst_19 : Module K M] →
                                          [inst_20 : Module K M₂] →
                                            [inst_21 : Module S M] →
                                              [inst_22 : Module S M₂] →
                                                [CompatibleSMul M M₂ K S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[K] M₂)
                        p :
                    (a : M) → N →ₗ[K] L)
                  x :
                N →ₗ[K] L) :
              (a : N) → L)
            y :
          L)

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)))))
x : M'
y : N'
⊢ Membership.mem (α := M) (↑i.range : Set M) ((i : (a : M') → M) x : 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)
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)))))
x : M'
y : N'
⊢ Membership.mem (α := N) (↑j.range : Set N) ((j : (a : N') → N) y : 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)
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)))))
⊢ (i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp).IsPerfPair

Tactic:
exact restrictScalars_field_aux
    (p.compl₁₂ (span L <| .range i).subtype (span L <| .range j).subtype)
    ((LinearMap.range i).inclusionSpan L ∘ₗ i.rangeRestrict)
    ((LinearMap.range j).inclusionSpan L ∘ₗ j.rangeRestrict)
    (((LinearMap.range i).injective_inclusionSpan L).comp (by simpa))
    (((LinearMap.range j).injective_inclusionSpan L).comp (by simpa))
    (by rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
        exact (LinearMap.range i).span_range_inclusionSpan L)
    (by rw [LinearMap.range_comp_of_range_eq_top _ (LinearMap.range_rangeRestrict _)]
        exact (LinearMap.range j).span_range_inclusionSpan L)
    fun x y ↦ LinearMap.BilinMap.apply_apply_mem_of_mem_span
      (LinearMap.range <| Algebra.linearMap K L) (range i) (range j)
      ((LinearMap.restrictScalarsₗ K L _ _ _).comp (p.restrictScalars K))
      (by simpa) (i x) (j y) (subset_span <| by simp) (subset_span <| by simp)

Premises used: LinearMap.restrictScalars, Submodule.injective_inclusionSpan, LinearMap.BilinMap.apply_apply_mem_of_mem_span, LinearMap.range, Algebra.linearMap, LinearMap.rangeRestrict, LinearMap.comp, SetLike.coe, Function.Injective.comp, Submodule.inclusionSpan, Submodule.span, Submodule.subtype, _private.0.LinearMap.restrictScalars_field_aux, LinearMap.restrictScalarsₗ, Submodule.subset_span, Set.range, LinearMap.compl₁₂, DFunLike.coe
-- 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
M' : Type u_5
N' : Type u_6
inst_10 : AddCommGroup M'
inst_11 : AddCommGroup N'
inst_12 : Module K M'
inst_13 : Module K N'
inst_14 : IsScalarTower K L N
i : M' →ₗ[K] M
j : N' →ₗ[K] 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)
x : M'
y : N'
⊢ Eq.{u_2 + 1} (α := L)
    ((algebraMap K L : (a : K) → L)
        ((((i.restrictScalarsRange₂ j (Algebra.linearMap K L) ⋯ p hp : (a : M') → N' →ₗ[K] K) x : N' →ₗ[K] K) :
              (a : N') → K)
            y :
          K) :
      L)
    ((((p : (a : M) → N →ₗ[L] L) ((i : (a : M') → M) x) : N →ₗ[L] L) : (a : N) → L) ((j : (a : N') → N) y : N) : L)

Tactic:
LinearMap.restrictScalarsRange₂_apply i j (Algebra.linearMap K L)
    (FaithfulSMul.algebraMap_injective K L) p hp x y

Premises used: LinearMap.restrictScalarsRange₂_apply, Algebra.linearMap, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.LinearAlgebra.Pi
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)
c : M₂
i : ι
⊢ Eq.{i + 1} (α := φ i) ((pi (φ := φ) f : (a : M₂) → (i : ι) → φ i) c i : φ i) ((f i : (a : M₂) → φ i) c : φ i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
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)
h : ∀ (c : M₂), c ∈ (pi (φ := φ) f).ker ↔ Membership.mem (γ := Submodule R M₂) (⨅ (i : ι), (f i).ker) c
⊢ (pi (φ := φ) f).ker = ⨅ (i : ι), (f i).ker

Tactic:
ext c
-- Module: Mathlib.LinearAlgebra.Pi
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)
c : M₂
⊢ c ∈ (pi (φ := φ) f).ker ↔ Membership.mem (γ := Submodule R M₂) (⨅ (i : ι), (f i).ker) c

Tactic:
simp [funext_iff]

Premises used: funext_iff
-- Module: Mathlib.LinearAlgebra.Pi
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)
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)
⊢ pi (φ := φ) f = 0 ↔ ∀ (i : ι), f i = 0

Tactic:
simp only [LinearMap.ext_iff, pi_apply, funext_iff]

Premises used: funext_iff, LinearMap.pi_apply, LinearMap.ext_iff
-- Module: Mathlib.LinearAlgebra.Pi
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)
⊢ (∀ (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:
⟨fun h a b => h b a, fun h a b => h b a⟩

Premises used: Iff.intro
-- Module: Mathlib.LinearAlgebra.Pi
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)
⊢ (∀ (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:
exact ⟨fun h a b => h b a, fun h a b => h b a⟩
-- Module: Mathlib.LinearAlgebra.Pi
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)
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)
⊢ Eq (α := M₂ →ₗ[R] (i : ι) → φ i) (pi (φ := φ) fun (x : ι) ↦ 0) 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Pi
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)
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:
rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
M₃ : Type y
ι : 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 : (i : ι) → LinearMap.{u, u, w, i} (RingHom.id R) M₂ (φ i)
g : M₃ →ₗ[R] M₂
⊢ pi (φ := φ) f ∘ₗ g = pi (φ := φ) fun (i : ι) ↦ f i ∘ₗ g

Tactic:
rfl

Premises used: LinearMap.pi, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
M₂ : Type w
ι : Type x
inst : Semiring R
inst_1 : AddCommMonoid M₂
inst_2 : Module R M₂
x : M₂
⊢ (const : (a : M₂) → ι → M₂) x = Function.const ι x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
i : ι
⊢ Eq (α := (a : (i : ι) → φ i) → φ i) (⇑(proj (φ := φ) i) : (a : (i : ι) → φ i) → φ i) (eval (β := φ) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
i : ι
⊢ Eq (α := ((i : ι) → φ i) →+ φ i) (toAddMonoidHom (R := R) (modM₁ := Pi.module ι φ R) (proj (φ := φ) i))
    (Pi.evalAddMonoidHom φ i)

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, Pi.evalAddMonoidHom, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
i : ι
b : (i : ι) → φ i
⊢ (proj (φ := φ) i : (a : (i : ι) → φ i) → φ i) b = b i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
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)
i : ι
⊢ proj (φ := φ) i ∘ₗ pi (φ := φ) f = f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
⊢ Eq (α := ((i : ι) → φ i) →ₗ[R] (i : ι) → φ i) (pi (φ := φ) (proj (φ := φ))) id

Tactic:
rfl

Premises used: LinearMap.pi, rfl
-- Module: Mathlib.LinearAlgebra.Pi
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 : M₂ →ₗ[R] (i : ι) → φ i
⊢ (pi (φ := fun (x : ι) ↦ φ x) fun (x : ι) ↦ proj (φ := φ) x ∘ₗ f) = f

Tactic:
rfl

Premises used: LinearMap.pi, rfl
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
i : ι
⊢ Surjective (α := (i : ι) → φ i) (β := φ i) (⇑(proj (φ := φ) i) : (a : (i : ι) → φ i) → φ i)

Tactic:
surjective_eval i

Premises used: Function.surjective_eval
-- Module: Mathlib.LinearAlgebra.Pi
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
⊢ ∀ (i : ι), a i = 0

Tactic:
simp only [mem_iInf, mem_ker, proj_apply] at h

Premises used: Submodule.mem_iInf, LinearMap.proj_apply, LinearMap.mem_ker
-- Module: Mathlib.LinearAlgebra.Pi
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 : ∀ (i : ι), a i = 0
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) ⊥ a

Tactic:
(mem_bot _).2 (funext fun i => h i)

Premises used: Iff.mpr, Set.Mem, Submodule.mem_bot, funext
-- Module: Mathlib.LinearAlgebra.Pi
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 : ∀ (i : ι), a i = 0
⊢ Membership.mem (γ := Submodule R ((i : ι) → φ i)) ⊥ a

Tactic:
exact (mem_bot _).2 (funext fun i => h i)

Premises used: Iff.mpr, Submodule.mem_bot, funext
-- Module: Mathlib.LinearAlgebra.Pi
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
h : ∀ (i : ι), (f : (a : M) → ι → N) (r • m) i = HSMul.hSMul (β := ι → N) r ((f : (a : M) → ι → N) m : ι → N) i
⊢ (f : (a : M) → ι → N) (r • m) = HSMul.hSMul (β := ι → N) r ((f : (a : M) → ι → N) m : ι → N)

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Pi
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
i : ι
⊢ (f : (a : M) → ι → N) (r • m) i = HSMul.hSMul (β := ι → N) r ((f : (a : M) → ι → N) m : ι → N) i

Tactic:
apply ((LinearMap.proj i).comp f).map_smul_of_tower

Premises used: LinearMap.proj, LinearMap.comp, LinearMap.map_smul_of_tower
-- Module: Mathlib.LinearAlgebra.Pi
Goal:
R : Type u
ι : Type x
inst : Semiring R
φ : ι → Type i
inst_1 : (i : ι) → AddCommMonoid (φ i)
inst_2 : (i : ι) → Module.{u, i} R (φ i)
ψ : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (ψ i)
inst_4 : (i : ι) → Module.{u, u_1} R (ψ i)
f : (i : ι) → LinearMap.{u, u, i, u_1} (RingHom.id R) (φ i) (ψ i)
⊢ Eq (α := (a : (i : ι) → φ i) → (i : ι) → ψ i) (⇑(piMap (φ := φ) (ψ := ψ) f) : (a : (i : ι) → φ i) → (i : ι) → ψ i)
    (Pi.map (α := φ) (β := ψ) fun (i : ι) ↦ (⇑(f i) : (a : φ i) → ψ i))

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.LinearAlgebra.Pi
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₂
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
⊢ (⇑f : (a : M₂) → M₃) ∘ (c • h) =
    HSMul.hSMul (α := R) (β := I → M₃) ((RingHom.id R : (a : R) → R) c : R) ((⇑f : (a : M₂) → M₃) ∘ h)

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.Pi
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₂
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:
f.map_smul' c (h x)

Premises used: LinearMap.map_smul'