awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ 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.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)
α : Type u_6
f : α → ι
x y : (i : ι) → φ i
h :
  ∀ (x_1 : α),
    (x + y) (f x_1) =
      HAdd.hAdd (α := (i : α) → φ (f i)) (β := (i : α) → φ (f i)) (fun (i : α) ↦ x (f i)) (fun (i : α) ↦ y (f i)) x_1
⊢ (fun (i : α) ↦ (x + y) (f i)) = HAdd.hAdd (α := (i : α) → φ (f i)) (fun (i : α) ↦ x (f i)) fun (i : α) ↦ y (f i)

Tactic:
ext
-- 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)
α : Type u_6
f : α → ι
x y : (i : ι) → φ i
x_1 : α
⊢ (x + y) (f x_1) =
    HAdd.hAdd (α := (i : α) → φ (f i)) (β := (i : α) → φ (f i)) (fun (i : α) ↦ x (f i)) (fun (i : α) ↦ y (f i)) x_1

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₂
ι : 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)
α : Type u_6
f : α → ι
m : R
x : (i : ι) → φ i
h :
  ∀ (x_1 : α),
    (m • x) (f x_1) =
      HSMul.hSMul (α := R) (β := (i : α) → φ (f i)) ((RingHom.id R : (a : R) → R) m : R) (fun (i : α) ↦ x (f i)) x_1
⊢ (fun (i : α) ↦ (m • x) (f i)) =
    HSMul.hSMul (α := R) (β := (i : α) → φ (f i)) ((RingHom.id R : (a : R) → R) m : R) fun (i : α) ↦ x (f i)

Tactic:
ext
-- 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)
α : Type u_6
f : α → ι
m : R
x : (i : ι) → φ i
x_1 : α
⊢ (m • x) (f x_1) =
    HSMul.hSMul (α := R) (β := (i : α) → φ (f i)) ((RingHom.id R : (a : R) → R) m : R) (fun (i : α) ↦ x (f i)) x_1

Tactic:
simp
-- 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
f : α → ι
v : (i : ι) → φ i
i : α
⊢ Eq.{u_5 + 1} (α := φ (f i)) ((Pi.compRightL R φ f : (a : (i : ι) → φ i) → (i : α) → φ (f i)) v i : φ (f i))
    (v (f i) : φ (f 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)
inst_7 : Fintype ι
inst_8 : DecidableEq ι
L : ((i : ι) → φ i) →L[R] M
v : (i : ι) → φ i
⊢ Eq.{u_2 + 1} (α := M) (∑ i : ι, (L ∘SL single R φ i : (a : φ i) → M) (v i) : M) ((L : (a : (i : ι) → φ i) → M) v : M)

Tactic:
simp [← map_sum, LinearMap.sum_single_apply]

Premises used: map_sum, LinearMap.sum_single_apply
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
inst_9 : Module R M₃
f : M →L[R] M₂
g : M →L[R] M₃
h : (↑f : M →ₗ[R] M₂).ker ⊔ (↑g : M →ₗ[R] M₃).ker = ⊤
⊢ (↑(f.prod g) : M →ₗ[R] M₂ × M₃).range = (↑f : M →ₗ[R] M₂).range.prod (↑g : M →ₗ[R] M₃).range

Tactic:
LinearMap.range_prod_eq h

Premises used: LinearMap.range_prod_eq, LinearMap.prod
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
M₂ : Type u_3
inst_4 : TopologicalSpace M₂
inst_5 : AddCommGroup M₂
inst_6 : Module R M₂
M₃ : Type u_4
inst_7 : TopologicalSpace M₃
inst_8 : AddCommGroup M₃
inst_9 : Module R M₃
f : M →L[R] M₃
g : M₂ →L[R] M₃
⊢ (↑f : M →ₗ[R] M₃).ker.prod (↑g : M₂ →ₗ[R] M₃).ker ≤ ((↑f : M →ₗ[R] M₃).coprod (↑g : M₂ →ₗ[R] M₃)).ker

Tactic:
LinearMap.ker_prod_ker_le_ker_coprod f.toLinearMap g.toLinearMap

Premises used: Set.Mem, LinearMap.ker_prod_ker_le_ker_coprod, ContinuousLinearMap.toLinearMap
-- 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 g : M × M₂ →L[R] M₃
simp :
  (↑f : M × M₂ →ₗ[R] M₃) ∘ₗ LinearMap.inl R M M₂ = (↑g : M × M₂ →ₗ[R] M₃) ∘ₗ LinearMap.inl R M M₂ ∧
      (↑f : M × M₂ →ₗ[R] M₃) ∘ₗ LinearMap.inr R M M₂ = (↑g : M × M₂ →ₗ[R] M₃) ∘ₗ LinearMap.inr R M M₂ ↔
    (↑(f ∘SL inl R M M₂) : M →ₗ[R] M₃) = (↑(g ∘SL inl R M M₂) : M →ₗ[R] M₃) ∧
      (↑(f ∘SL inr R M M₂) : M₂ →ₗ[R] M₃) = (↑(g ∘SL inr R M M₂) : M₂ →ₗ[R] M₃)
⊢ f = g ↔ f ∘SL inl R M M₂ = g ∘SL inl R M M₂ ∧ f ∘SL inr R M M₂ = g ∘SL inr R M M₂

Tactic:
simp only [← coe_inj, LinearMap.prod_ext_iff]

Premises used: ContinuousLinearMap.coe_inj, LinearMap.prod_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
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 g : M × M₂ →L[R] M₃
⊢ (↑f : M × M₂ →ₗ[R] M₃) ∘ₗ LinearMap.inl R M M₂ = (↑g : M × M₂ →ₗ[R] M₃) ∘ₗ LinearMap.inl R M M₂ ∧
      (↑f : M × M₂ →ₗ[R] M₃) ∘ₗ LinearMap.inr R M M₂ = (↑g : M × M₂ →ₗ[R] M₃) ∘ₗ LinearMap.inr R M M₂ ↔
    (↑(f ∘SL inl R M M₂) : M →ₗ[R] M₃) = (↑(g ∘SL inl R M M₂) : M →ₗ[R] M₃) ∧
      (↑(f ∘SL inr R M M₂) : M₂ →ₗ[R] M₃) = (↑(g ∘SL inr R M M₂) : M₂ →ₗ[R] M₃)

Tactic:
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 g : M × M₂ →L[R] M₃
hl : f ∘SL inl R M M₂ = g ∘SL inl R M M₂
hr : f ∘SL inr R M M₂ = g ∘SL inr R M M₂
⊢ f = g

Tactic:
prod_ext_iff.2 ⟨hl, hr⟩

Premises used: Iff.mpr, ContinuousLinearMap.prod_ext_iff, And.intro
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
hl :
  ∀ (x : M₁),
    Eq.{u_3 + 1} (α := M) (((f₁ + g₁).coprod (f₂ + g₂) ∘SL inl R M₁ M₂ : (a : M₁) → M) x : M)
      (((f₁.coprod f₂ + g₁.coprod g₂) ∘SL inl R M₁ M₂ : (a : M₁) → M) x : M)
hr :
  ∀ (x : M₂),
    Eq.{u_3 + 1} (α := M) (((f₁ + g₁).coprod (f₂ + g₂) ∘SL inr R M₁ M₂ : (a : M₂) → M) x : M)
      (((f₁.coprod f₂ + g₁.coprod g₂) ∘SL inr R M₁ M₂ : (a : M₂) → M) x : M)
⊢ (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
x : M₁
⊢ Eq.{u_3 + 1} (α := M) (((f₁ + g₁).coprod (f₂ + g₂) ∘SL inl R M₁ M₂ : (a : M₁) → M) x : M)
    (((f₁.coprod f₂ + g₁.coprod g₂) ∘SL inl R M₁ M₂ : (a : M₁) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
f₁ g₁ : M₁ →L[R] M
f₂ g₂ : M₂ →L[R] M
x : M₂
⊢ Eq.{u_3 + 1} (α := M) (((f₁ + g₁).coprod (f₂ + g₂) ∘SL inr R M₁ M₂ : (a : M₂) → M) x : M)
    (((f₁.coprod f₂ + g₁.coprod g₂) ∘SL inr R M₁ M₂ : (a : M₂) → M) x : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
f₁ : M₁ →L[R] M
f₂ : M₂ →L[R] M
⊢ (↑(f₁.coprod f₂) : M₁ × M₂ →ₗ[R] M).range = (↑f₁ : M₁ →ₗ[R] M).range ⊔ (↑f₂ : M₂ →ₗ[R] M).range

Tactic:
LinearMap.range_coprod ..

Premises used: LinearMap.coprod, LinearMap.range_coprod
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
f₁ : M₁ →L[R] M
f₂ : M₂ →L[R] M
⊢ f₁ ∘SL fst R M₁ M₂ + f₂ ∘SL snd R M₁ M₂ = f₁.coprod f₂

Tactic:
rfl

Premises used: LinearMap.coprod, ContinuousLinearMap.coprod, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : TopologicalSpace M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : ContinuousAdd M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : ContinuousAdd N
inst_11 : AddCommMonoid M₁
inst_12 : Module R M₁
inst_13 : AddCommMonoid M₂
inst_14 : Module R M₂
f : M →L[R] N
g₁ : M₁ →L[R] M
g₂ : M₂ →L[R] M
⊢ f ∘SL g₁.coprod g₂ = (f ∘SL g₁).coprod (f ∘SL g₂)

Tactic:
coe_injective <| LinearMap.comp_coprod ..

Premises used: ContinuousLinearMap.coe_injective, LinearMap.comp_coprod
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
f₁ : M₁ →L[R] M
f₂ : M₂ →L[R] M
⊢ f₁.coprod f₂ ∘SL inl R M₁ M₂ = f₁

Tactic:
coe_injective <| LinearMap.coprod_inl ..

Premises used: LinearMap.coprod_inl, ContinuousLinearMap.coe_injective
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
f₁ : M₁ →L[R] M
f₂ : M₂ →L[R] M
⊢ f₁.coprod f₂ ∘SL inr R M₁ M₂ = f₂

Tactic:
coe_injective <| LinearMap.coprod_inr ..

Premises used: LinearMap.coprod_inr, ContinuousLinearMap.coe_injective
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
N : Type u_4
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : ContinuousAdd M
inst_6 : AddCommMonoid N
inst_7 : Module R N
inst_8 : ContinuousAdd N
⊢ Eq (α := M × N →L[R] M × N) (coprod (inl R M N) (inr R M N)) (ContinuousLinearMap.id R (M × N))

Tactic:
coe_injective <| LinearMap.coprod_inl_inr

Premises used: LinearMap.coprod_inl_inr, ContinuousLinearMap.coe_injective
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommMonoid M₂
inst_10 : Module R M₂
inst_11 : ContinuousAdd M₁
inst_12 : ContinuousAdd M₂
f : M × M₁ →L[R] M₂
rw : f ∘SL coprod (inl R M M₁) (inr R M M₁) = f
rw₁ : f ∘SL ContinuousLinearMap.id R (M × M₁) = f
rw₂ rw₃ : f = f
⊢ (f ∘SL inl R M M₁).coprod (f ∘SL inr R M M₁) = f

Tactic:
rw [← ContinuousLinearMap.comp_coprod, coprod_inl_inr, comp_id]

Premises used: ContinuousLinearMap.comp_coprod, ContinuousLinearMap.comp_id, ContinuousLinearMap.coprod_inl_inr
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : TopologicalSpace M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : ContinuousAdd M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : ContinuousAdd N
inst_11 : AddCommMonoid M₁
inst_12 : Module R M₁
inst_13 : AddCommMonoid M₂
inst_14 : Module R M₂
inst_15 : ContinuousAdd M₁
inst_16 : ContinuousAdd M₂
inst_17 : Semiring S
inst_18 : Module S M
inst_19 : ContinuousConstSMul S M
inst_20 : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
dsimp : (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2
⊢ (r • a).1.coprod (r • a).2 = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) (a.1.coprod a.2)

Tactic:
dsimp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : TopologicalSpace M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : ContinuousAdd M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : ContinuousAdd N
inst_11 : AddCommMonoid M₁
inst_12 : Module R M₁
inst_13 : AddCommMonoid M₂
inst_14 : Module R M₂
inst_15 : ContinuousAdd M₁
inst_16 : ContinuousAdd M₂
inst_17 : Semiring S
inst_18 : Module S M
inst_19 : ContinuousConstSMul S M
inst_20 : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
hl :
  ∀ (x : M₁),
    Eq.{u_3 + 1} (α := M) (((r • a.1).coprod (r • a.2) ∘SL inl R M₁ M₂ : (a : M₁) → M) x : M)
      (((r • a.1.coprod a.2) ∘SL inl R M₁ M₂ : (a : M₁) → M) x : M)
hr :
  ∀ (x : M₂),
    Eq.{u_3 + 1} (α := M) (((r • a.1).coprod (r • a.2) ∘SL inr R M₁ M₂ : (a : M₂) → M) x : M)
      (((r • a.1.coprod a.2) ∘SL inr R M₁ M₂ : (a : M₂) → M) x : M)
⊢ (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : TopologicalSpace M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : ContinuousAdd M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : ContinuousAdd N
inst_11 : AddCommMonoid M₁
inst_12 : Module R M₁
inst_13 : AddCommMonoid M₂
inst_14 : Module R M₂
inst_15 : ContinuousAdd M₁
inst_16 : ContinuousAdd M₂
inst_17 : Semiring S
inst_18 : Module S M
inst_19 : ContinuousConstSMul S M
inst_20 : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
x : M₁
⊢ Eq.{u_3 + 1} (α := M) (((r • a.1).coprod (r • a.2) ∘SL inl R M₁ M₂ : (a : M₁) → M) x : M)
    (((r • a.1.coprod a.2) ∘SL inl R M₁ M₂ : (a : M₁) → M) x : M)

Tactic:
simp [smul_apply]

Premises used: ContinuousLinearMap.smul_apply
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : TopologicalSpace M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : ContinuousAdd M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : ContinuousAdd N
inst_11 : AddCommMonoid M₁
inst_12 : Module R M₁
inst_13 : AddCommMonoid M₂
inst_14 : Module R M₂
inst_15 : ContinuousAdd M₁
inst_16 : ContinuousAdd M₂
inst_17 : Semiring S
inst_18 : Module S M
inst_19 : ContinuousConstSMul S M
inst_20 : SMulCommClass R S M
r : S
a : (M₁ →L[R] M) × (M₂ →L[R] M)
x : M₂
⊢ Eq.{u_3 + 1} (α := M) (((r • a.1).coprod (r • a.2) ∘SL inr R M₁ M₂ : (a : M₂) → M) x : M)
    (((r • a.1.coprod a.2) ∘SL inr R M₁ M₂ : (a : M₂) → M) x : M)

Tactic:
simp [smul_apply]

Premises used: ContinuousLinearMap.smul_apply
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : TopologicalSpace M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : ContinuousAdd M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : ContinuousAdd N
inst_11 : AddCommMonoid M₁
inst_12 : Module R M₁
inst_13 : AddCommMonoid M₂
inst_14 : Module R M₂
inst_15 : ContinuousAdd M₁
inst_16 : ContinuousAdd M₂
inst_17 : Semiring S
inst_18 : Module S M
inst_19 : ContinuousConstSMul S M
inst_20 : SMulCommClass R S M
f : (M₁ →L[R] M) × (M₂ →L[R] M)
⊢ (fun (f : M₁ × M₂ →L[R] M) ↦ (f ∘SL inl R M₁ M₂, f ∘SL inr R M₁ M₂))
      ((fun (f : (M₁ →L[R] M) × (M₂ →L[R] M)) ↦ f.1.coprod f.2) f) =
    f

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : TopologicalSpace M₁
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M
inst_6 : Module R M
inst_7 : ContinuousAdd M
inst_8 : AddCommMonoid N
inst_9 : Module R N
inst_10 : ContinuousAdd N
inst_11 : AddCommMonoid M₁
inst_12 : Module R M₁
inst_13 : AddCommMonoid M₂
inst_14 : Module R M₂
inst_15 : ContinuousAdd M₁
inst_16 : ContinuousAdd M₂
inst_17 : Semiring S
inst_18 : Module S M
inst_19 : ContinuousConstSMul S M
inst_20 : SMulCommClass R S M
f : M₁ × M₂ →L[R] M
⊢ (fun (f : (M₁ →L[R] M) × (M₂ →L[R] M)) ↦ f.1.coprod f.2)
      ((fun (f : M₁ × M₂ →L[R] M) ↦ (f ∘SL inl R M₁ M₂, f ∘SL inr R M₁ M₂)) f) =
    f

Tactic:
simp [← comp_coprod f (.inl R M₁ M₂)]

Premises used: ContinuousLinearMap.comp_coprod, ContinuousLinearMap.inl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
Goal:
R : Type u_1
M : Type u_3
M₁ : Type u_5
M₂ : Type u_6
inst : Semiring R
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace M₁
inst_3 : TopologicalSpace M₂
inst_4 : AddCommGroup M
inst_5 : Module R M
inst_6 : ContinuousAdd M
inst_7 : AddCommMonoid M₁
inst_8 : Module R M₁
inst_9 : AddCommGroup M₂
inst_10 : Module R M₂
f₁ : M₁ →L[R] M
f₂ : M₂ →L[R] M
hf : Disjoint (↑f₁ : M₁ →ₗ[R] M).range (↑f₂ : M₂ →ₗ[R] M).range
⊢ (↑(f₁.coprod f₂) : M₁ × M₂ →ₗ[R] M).ker = (↑f₁ : M₁ →ₗ[R] M).ker.prod (↑f₂ : M₂ →ₗ[R] M).ker

Tactic:
LinearMap.ker_coprod_of_disjoint_range f₁.toLinearMap f₂.toLinearMap hf

Premises used: LinearMap.ker_coprod_of_disjoint_range, LinearMap.coprod, ContinuousLinearMap.toLinearMap
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
S : Submodule R M
⊢ (↑S.mkQL : M →ₗ[R] M ⧸ S) = S.mkQ

Tactic:
rfl

Premises used: Submodule.mkQ, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
S : Submodule R M
⊢ Eq (α := (a : M) → M ⧸ S) (⇑S.mkQL : (a : M) → M ⧸ S) (⇑S.mkQ : (a : M) → M ⧸ S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
S : Submodule R M
x : M
⊢ Eq (α := M ⧸ S) ((S.mkQL : (a : M) → M ⧸ S) x : M ⧸ S) ((S.mkQ : (a : M) → M ⧸ S) x : M ⧸ S)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
S : Submodule R M
⊢ IsQuotientMap (X := M) (Y := M ⧸ S) (⇑S.mkQL : (a : M) → M ⧸ S)

Tactic:
isQuotientMap_quot_mk

Premises used: Submodule.Quotient.mk, Quotient, Quotient.mk', isQuotientMap_quot_mk
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Goal:
R : Type u_1
inst : Ring R
M : Type u_3
inst_1 : TopologicalSpace M
inst_2 : AddCommGroup M
inst_3 : Module R M
S : Submodule R M
inst_4 : ContinuousAdd M
⊢ IsOpenQuotientMap (X := M) (Y := M ⧸ S) (⇑S.mkQL : (a : M) → M ⧸ S)

Tactic:
S.isOpenQuotientMap_mkQ

Premises used: Submodule.isOpenQuotientMap_mkQ
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Goal:
R : Type u_1
R₂ : Type u_2
inst : Ring R
inst_1 : Ring R₂
σ : R →+* R₂
M : Type u_3
M₂ : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module R₂ M₂
S : Submodule R M
f : M →SL[σ] M₂
h : S ≤ (↑f : M →ₛₗ[σ] M₂).ker
⊢ (↑(S.liftQL f h) : M ⧸ S →ₛₗ[σ] M₂) = S.liftQ (↑f : M →ₛₗ[σ] M₂) h

Tactic:
rfl

Premises used: Submodule.liftQ, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Goal:
R : Type u_1
R₂ : Type u_2
inst : Ring R
inst_1 : Ring R₂
σ : R →+* R₂
M : Type u_3
M₂ : Type u_4
inst_2 : TopologicalSpace M
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : TopologicalSpace M₂
inst_6 : AddCommGroup M₂
inst_7 : Module R₂ M₂
S : Submodule R M
f : M →SL[σ] M₂
h : S ≤ (↑f : M →ₛₗ[σ] M₂).ker
⊢ Eq (α := (a : M ⧸ S) → M₂) (⇑(S.liftQL f h) : (a : M ⧸ S) → M₂) (⇑(S.liftQ (↑f : M →ₛₗ[σ] M₂) h) : (a : M ⧸ S) → M₂)

Tactic:
rfl

Premises used: rfl