awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ (↑f : M →ₗ[R] M).ker ∈ Module.End.invtSubmodule (↑T : M →ₗ[R] M) ↔ f ∘SL T ∘SL f = f ∘SL T

Tactic:
simpa [← ContinuousLinearMap.coe_comp] using
    LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff (T := T) hf.toLinearMap

Premises used: ContinuousLinearMap.IsIdempotentElem.toLinearMap, LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff, ContinuousLinearMap.coe_comp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
f T : M →L[R] M
hf : IsIdempotentElem f
⊢ Commute f T ↔
    (↑f : M →ₗ[R] M).range ∈ Module.End.invtSubmodule (↑T : M →ₗ[R] M) ∧
      (↑f : M →ₗ[R] M).ker ∈ Module.End.invtSubmodule (↑T : M →ₗ[R] M)

Tactic:
simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← coe_comp] using
    LinearMap.IsIdempotentElem.commute_iff (T := T) hf.toLinearMap

Premises used: LinearMap.IsIdempotentElem.commute_iff, Module.End.mul_eq_comp, ContinuousLinearMap.IsIdempotentElem.toLinearMap, SemiconjBy, Commute, ContinuousLinearMap.coe_comp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTopologicalAddGroup M
f T : M →L[R] M
hT : IsUnit T
hf : IsIdempotentElem f
⊢ IsUnit (M := M →ₗ[R] M) ((toLinearMapRingHom : (a : M →L[R] M) → M →ₗ[R] M) T : M →ₗ[R] M)

Tactic:
have := hT.map ContinuousLinearMap.toLinearMapRingHom
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTopologicalAddGroup M
f T : M →L[R] M
hT : IsUnit T
hf : IsIdempotentElem f
this : IsUnit (M := M →ₗ[R] M) ((toLinearMapRingHom : (a : M →L[R] M) → M →ₗ[R] M) T : M →ₗ[R] M)
⊢ IsUnit T

Tactic:
hT
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTopologicalAddGroup M
f T : M →L[R] M
hT : IsUnit T
hf : IsIdempotentElem f
this : IsUnit (M := M →ₗ[R] M) ((toLinearMapRingHom : (a : M →L[R] M) → M →ₗ[R] M) T : M →ₗ[R] M)
lift :
  ∀ (T : (M →L[R] M)ˣ)
    (this : IsUnit (M := M →ₗ[R] M) ((toLinearMapRingHom : (a : M →L[R] M) → M →ₗ[R] M) (↑T : M →L[R] M) : M →ₗ[R] M)),
    Commute f (↑T : M →L[R] M) ↔
      Submodule.map (↑(↑T : M →L[R] M) : M →ₗ[R] M) (↑f : M →ₗ[R] M).range = (↑f : M →ₗ[R] M).range ∧
        Submodule.map (↑(↑T : M →L[R] M) : M →ₗ[R] M) (↑f : M →ₗ[R] M).ker = (↑f : M →ₗ[R] M).ker
⊢ Commute f T ↔
    Submodule.map (↑T : M →ₗ[R] M) (↑f : M →ₗ[R] M).range = (↑f : M →ₗ[R] M).range ∧
      Submodule.map (↑T : M →ₗ[R] M) (↑f : M →ₗ[R] M).ker = (↑f : M →ₗ[R] M).ker

Tactic:
lift T to (M →L[R] M)ˣ using hT

Premises used: ContinuousLinearMap, RingHom.id
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTopologicalAddGroup M
f : M →L[R] M
hf : IsIdempotentElem f
T : (M →L[R] M)ˣ
this : IsUnit (M := M →ₗ[R] M) ((toLinearMapRingHom : (a : M →L[R] M) → M →ₗ[R] M) (↑T : M →L[R] M) : M →ₗ[R] M)
⊢ Commute f (↑T : M →L[R] M) ↔
    Submodule.map (↑(↑T : M →L[R] M) : M →ₗ[R] M) (↑f : M →ₗ[R] M).range = (↑f : M →ₗ[R] M).range ∧
      Submodule.map (↑(↑T : M →L[R] M) : M →ₗ[R] M) (↑f : M →ₗ[R] M).ker = (↑f : M →ₗ[R] M).ker

Tactic:
simpa [Commute, SemiconjBy, Module.End.mul_eq_comp, ← ContinuousLinearMap.coe_comp] using
    LinearMap.IsIdempotentElem.commute_iff_of_isUnit this hf.toLinearMap

Premises used: Module.End.mul_eq_comp, ContinuousLinearMap.IsIdempotentElem.toLinearMap, SemiconjBy, Commute, ContinuousLinearMap.coe_comp, LinearMap.IsIdempotentElem.commute_iff_of_isUnit
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsTopologicalAddGroup M
inst_5 : T1Space M
p : M →L[R] M
hp : IsIdempotentElem p
⊢ IsClosed (↑(↑p : M →ₗ[R] M).range : Set M)

Tactic:
LinearMap.IsIdempotentElem.range_eq_ker hp.toLinearMap ▸ isClosed_ker (.id R M - p)

Premises used: LinearMap.IsIdempotentElem.range_eq_ker, ContinuousLinearMap.IsIdempotentElem.toLinearMap, Eq.rec, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f₁ : M₁ →L[R] M₂
f₂ : M₁ →L[R] M₃
⊢ (↑(f₁.prod f₂) : M₁ →ₗ[R] M₂ × M₃) = (↑f₁ : M₁ →ₗ[R] M₂).prod (↑f₂ : M₁ →ₗ[R] M₃)

Tactic:
rfl

Premises used: LinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f₁ : M₁ →L[R] M₂
f₂ : M₁ →L[R] M₃
x : M₁
⊢ Eq (α := M₂ × M₃) ((f₁.prod f₂ : (a : M₁) → M₂ × M₃) x : M₂ × M₃)
    (((f₁ : (a : M₁) → M₂) x, (f₂ : (a : M₁) → M₃) x) : M₂ × M₃)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
x : M₁
⊢ Eq (α := M₁ × M₂) ((inl R M₁ M₂ : (a : M₁) → M₁ × M₂) x : M₁ × M₂) ((x, 0) : M₁ × M₂)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
x : M₂
⊢ Eq (α := M₁ × M₂) ((inr R M₁ M₂ : (a : M₂) → M₁ × M₂) x : M₁ × M₂) ((0, x) : M₁ × M₂)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₁ →ₗ[R] M₁ × M₂) (↑(inl R M₁ M₂) : M₁ →ₗ[R] M₁ × M₂) (LinearMap.inl R M₁ M₂)

Tactic:
rfl

Premises used: LinearMap.inl, LinearMap.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₂ →ₗ[R] M₁ × M₂) (↑(inr R M₁ M₂) : M₂ →ₗ[R] M₁ × M₂) (LinearMap.inr R M₁ M₂)

Tactic:
rfl

Premises used: LinearMap.prod, LinearMap.inr, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
L : M₁ × M₂ →L[R] M₃
v : M₁ × M₂
⊢ HAdd.hAdd (α := M₃) (β := M₃) ((L ∘SL inl R M₁ M₂ : (a : M₁) → M₃) v.1 : M₃)
      ((L ∘SL inr R M₁ M₂ : (a : M₂) → M₃) v.2 : M₃) =
    (L : (a : M₁ × M₂) → M₃) v

Tactic:
simp [← map_add]

Premises used: map_add
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f : M₁ →L[R] M₂
g : M₁ →L[R] M₃
⊢ (↑(f.prod g) : M₁ →ₗ[R] M₂ × M₃).ker = (↑f : M₁ →ₗ[R] M₂).ker ⊓ (↑g : M₁ →ₗ[R] M₃).ker

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₁ × M₂ →ₗ[R] M₁) (↑(fst R M₁ M₂) : M₁ × M₂ →ₗ[R] M₁) (LinearMap.fst R M₁ M₂)

Tactic:
rfl

Premises used: LinearMap.fst, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := (a : M₁ × M₂) → M₁) (⇑(fst R M₁ M₂) : (a : M₁ × M₂) → M₁) Prod.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₁ × M₂ →ₗ[R] M₂) (↑(snd R M₁ M₂) : M₁ × M₂ →ₗ[R] M₂) (LinearMap.snd R M₁ M₂)

Tactic:
rfl

Premises used: LinearMap.snd, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := (a : M₁ × M₂) → M₂) (⇑(snd R M₁ M₂) : (a : M₁ × M₂) → M₂) Prod.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₁ × M₂ →L[R] M₁ × M₂) (ContinuousLinearMap.prod (fst R M₁ M₂) (snd R M₁ M₂))
    (ContinuousLinearMap.id R (M₁ × M₂))

Tactic:
ext fun ⟨_x, _y⟩ => rfl

Premises used: ContinuousLinearMap.id, ContinuousLinearMap.snd, ContinuousLinearMap.prod, _private.0.ContinuousLinearMap.fst_prod_snd.match_1, ContinuousLinearMap.fst, Prod, Eq, DFunLike.coe, ContinuousLinearMap.ext, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f : M₁ →L[R] M₂
g : M₁ →L[R] M₃
⊢ fst R M₂ M₃ ∘SL f.prod g = f

Tactic:
ext fun _x => rfl

Premises used: ContinuousLinearMap.ext, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f : M₁ →L[R] M₂
g : M₁ →L[R] M₃
⊢ snd R M₂ M₃ ∘SL f.prod g = g

Tactic:
ext fun _x => rfl

Premises used: ContinuousLinearMap.ext, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₁ →L[R] M₁) (fst R M₁ M₂ ∘SL inl R M₁ M₂) (ContinuousLinearMap.id R M₁)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.id, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₂ →L[R] M₁) (fst R M₁ M₂ ∘SL inr R M₁ M₂) 0

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₁ →L[R] M₂) (snd R M₁ M₂ ∘SL inl R M₁ M₂) 0

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₂ →L[R] M₂) (snd R M₁ M₂ ∘SL inr R M₁ M₂) (ContinuousLinearMap.id R M₂)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.id, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
M₄ : Type u_5
inst_10 : TopologicalSpace M₄
inst_11 : AddCommMonoid M₄
inst_12 : Module R M₄
f₁ : M₁ →L[R] M₂
f₂ : M₃ →L[R] M₄
⊢ (↑(f₁.prodMap f₂) : M₁ × M₃ →ₗ[R] M₂ × M₄) = (↑f₁ : M₁ →ₗ[R] M₂).prodMap (↑f₂ : M₃ →ₗ[R] M₄)

Tactic:
rfl

Premises used: LinearMap.prod, rfl, LinearMap.prodMap
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₁ : Type u_2
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R M₁
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
M₄ : Type u_5
inst_10 : TopologicalSpace M₄
inst_11 : AddCommMonoid M₄
inst_12 : Module R M₄
f₁ : M₁ →L[R] M₂
f₂ : M₃ →L[R] M₄
⊢ Eq (α := (a : M₁ × M₃) → M₂ × M₄) (⇑(f₁.prodMap f₂) : (a : M₁ × M₃) → M₂ × M₄)
    (Prod.map (⇑f₁ : (a : M₁) → M₂) (⇑f₂ : (a : M₃) → M₄))

Tactic:
rfl

Premises used: Prod.map, Function.prod, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)
⊢ Eq (α := (a : M) → (i : ι) → φ i) (⇑(pi (φ := φ) f) : (a : M) → (i : ι) → φ i) fun (c : M) (i : ι) ↦
    (f i : (a : M) → φ i) c

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)
⊢ (↑(pi (φ := φ) f) : M →ₗ[R] (i : ι) → φ i) = LinearMap.pi (φ := φ) fun (i : ι) ↦ (↑(f i) : M →ₗ[R] φ i)

Tactic:
rfl

Premises used: LinearMap.pi, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)
c : M
i : ι
⊢ Eq.{u_5 + 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.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)
simp :
  (∀ (x : M) (x_1 : ι),
      Eq.{u_5 + 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.{u_5 + 1} (α := φ i) ((f i : (a : M) → φ i) x : φ i)
        (((0 : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)) : (a : M) → φ i) x : φ i)
⊢ pi (φ := φ) f = 0 ↔ ∀ (i : ι), f i = 0

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

Premises used: ContinuousLinearMap.pi_apply, funext_iff, ContinuousLinearMap.ext_iff
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)
⊢ (∀ (x : M) (x_1 : ι),
      Eq.{u_5 + 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.{u_5 + 1} (α := φ i) ((f i : (a : M) → φ i) x : φ i)
        (((0 : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)) : (a : M) → φ i) x : φ i)

Tactic:
forall_comm

Premises used: forall_comm
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)
⊢ (∀ (x : M) (x_1 : ι),
      Eq.{u_5 + 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.{u_5 + 1} (α := φ i) ((f i : (a : M) → φ i) x : φ i)
        (((0 : ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)) : (a : M) → φ i) x : φ i)

Tactic:
exact forall_comm

Premises used: forall_comm
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
⊢ Eq (α := M →L[R] (i : ι) → φ i) (pi (φ := φ) fun (x : ι) ↦ 0) 0

Tactic:
ext fun _ => rfl

Premises used: ContinuousLinearMap.ext, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommMonoid M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_7 : (i : ι) → TopologicalSpace (φ i)
inst_8 : (i : ι) → AddCommMonoid (φ i)
inst_9 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_2, u_5} (RingHom.id R) M (φ i)
g : M₂ →L[R] M
⊢ pi (φ := φ) f ∘SL g = pi (φ := φ) fun (i : ι) ↦ f i ∘SL g

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.pi, LinearMap.pi, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
φ : ι → Type u_5
inst_1 : (i : ι) → TopologicalSpace (φ i)
inst_2 : (i : ι) → AddCommMonoid (φ i)
inst_3 : (i : ι) → Module.{u_1, u_5} R (φ i)
i : ι
b : (i : ι) → φ i
⊢ (proj (φ := φ) i : (a : (i : ι) → φ i) → φ i) b = b i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₂ : Type u_3
inst_1 : TopologicalSpace M₂
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_3, u_5} (RingHom.id R) M₂ (φ i)
i : ι
⊢ proj (φ := φ) i ∘SL pi (φ := φ) f = f i

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
φ : ι → Type u_5
inst_1 : (i : ι) → TopologicalSpace (φ i)
inst_2 : (i : ι) → AddCommMonoid (φ i)
inst_3 : (i : ι) → Module.{u_1, u_5} R (φ i)
i : ι
⊢ Eq (α := ((i : ι) → φ i) →ₗ[R] φ i) (↑(proj (φ := φ) i) : ((i : ι) → φ i) →ₗ[R] φ i) (LinearMap.proj (φ := φ) i)

Tactic:
rfl

Premises used: LinearMap.proj, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
φ : ι → Type u_5
inst_1 : (i : ι) → TopologicalSpace (φ i)
inst_2 : (i : ι) → AddCommMonoid (φ i)
inst_3 : (i : ι) → Module.{u_1, u_5} R (φ i)
⊢ Eq (α := ((i : ι) → φ i) →L[R] (i : ι) → φ i) (pi (φ := φ) (proj (φ := φ))) (ContinuousLinearMap.id R ((i : ι) → φ i))

Tactic:
rfl

Premises used: ContinuousLinearMap.pi, ContinuousLinearMap.id, LinearMap.pi, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
M₂ : Type u_3
inst_1 : TopologicalSpace M₂
inst_2 : AddCommMonoid M₂
inst_3 : Module R M₂
ι : Type u_4
φ : ι → Type u_5
inst_4 : (i : ι) → TopologicalSpace (φ i)
inst_5 : (i : ι) → AddCommMonoid (φ i)
inst_6 : (i : ι) → Module.{u_1, u_5} R (φ i)
f : M₂ →L[R] (i : ι) → φ i
⊢ (pi (φ := fun (x : ι) ↦ φ x) fun (x : ι) ↦ proj (φ := φ) x ∘SL f) = f

Tactic:
rfl

Premises used: ContinuousLinearMap.pi, LinearMap.pi, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
φ : ι → Type u_5
inst_1 : (i : ι) → TopologicalSpace (φ i)
inst_2 : (i : ι) → AddCommMonoid (φ i)
inst_3 : (i : ι) → Module.{u_1, u_5} R (φ i)
⊢ Eq (α := Submodule R ((i : ι) → φ i)) (⨅ (i : ι), LinearMap.ker (↑(proj (φ := φ) i) : ((i : ι) → φ i) →ₗ[R] φ i)) ⊥

Tactic:
LinearMap.iInf_ker_proj

Premises used: LinearMap.iInf_ker_proj, LinearMap.proj
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Semiring R
ι : Type u_4
φ : ι → Type u_5
inst_1 : (i : ι) → TopologicalSpace (φ i)
inst_2 : (i : ι) → AddCommMonoid (φ i)
inst_3 : (i : ι) → Module.{u_1, u_5} R (φ i)
ψ : ι → Type u_6
inst_4 : (i : ι) → TopologicalSpace (ψ i)
inst_5 : (i : ι) → AddCommMonoid (ψ i)
inst_6 : (i : ι) → Module.{u_1, u_6} R (ψ i)
f : (i : ι) → ContinuousLinearMap.{u_1, u_1, u_5, u_6} (RingHom.id R) (φ i) (ψ i)
⊢ (↑(piMap (φ := φ) (ψ := ψ) f) : ((i : ι) → φ i) →ₗ[R] (i : ι) → ψ i) =
    LinearMap.piMap (φ := φ) (ψ := ψ) fun (i : ι) ↦ (↑(f i) : φ i →ₗ[R] ψ i)

Tactic:
rfl

Premises used: LinearMap.pi, LinearMap.piMap, rfl