awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid U
inst_2 : Module R U
inst_3 : TopologicalSpace U
inst_4 : AddCommMonoid V
inst_5 : Module R V
inst_6 : TopologicalSpace V
inst_7 : ContinuousAdd V
inst_8 : ContinuousConstSMul R V
inst_9 : AddCommMonoid W
inst_10 : Module R W
inst_11 : TopologicalSpace W
inst_12 : ContinuousAdd W
inst_13 : ContinuousConstSMul R W
x x_1 : U →L[R] V
⊢ lcomp W (x + x_1) = HAdd.hAdd (α := (V →L[R] W) →ₗ[R] U →L[R] W) (lcomp W x) (lcomp W x_1)
have h : ∀ (x_2 : V →L[R] W) (x_3 : U),
  Eq.{u_4 + 1} (α := W) ((((lcomp W (x + x_1) : (a : V →L[R] W) → U →L[R] W) x_2 : U →L[R] W) : (a : U) → W) x_3 : W)
    ((((HAdd.hAdd (α := (V →L[R] W) →ₗ[R] U →L[R] W) (lcomp W x) (lcomp W x_1) : (a : V →L[R] W) → U →L[R] W) x_2 :
            U →L[R] W) :
          (a : U) → W)
        x_3 :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
U : Type u_2
V : Type u_3
W : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid U
inst_2 : Module R U
inst_3 : TopologicalSpace U
inst_4 : AddCommMonoid V
inst_5 : Module R V
inst_6 : TopologicalSpace V
inst_7 : ContinuousAdd V
inst_8 : ContinuousConstSMul R V
inst_9 : AddCommMonoid W
inst_10 : Module R W
inst_11 : TopologicalSpace W
inst_12 : ContinuousAdd W
inst_13 : ContinuousConstSMul R W
x : R
x_1 : U →L[R] V
⊢ lcomp W (x • x_1) =
    HSMul.hSMul (α := R) (β := (V →L[R] W) →ₗ[R] U →L[R] W) ((RingHom.id R : (a : R) → R) x : R) (lcomp W x_1)
have h : ∀ (x_2 : V →L[R] W) (x_3 : U),
  Eq.{u_4 + 1} (α := W) ((((lcomp W (x • x_1) : (a : V →L[R] W) → U →L[R] W) x_2 : U →L[R] W) : (a : U) → W) x_3 : W)
    ((((HSMul.hSMul (α := R) (β := (V →L[R] W) →ₗ[R] U →L[R] W) ((RingHom.id R : (a : R) → R) x : R) (lcomp W x_1) :
                (a : V →L[R] W) → U →L[R] W)
              x_2 :
            U →L[R] W) :
          (a : U) → W)
        x_3 :
      W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module S M
inst_5 : SMulCommClass R S M
inst_6 : TopologicalSpace M
inst_7 : ContinuousAdd M
inst_8 : ContinuousConstSMul S M
inst_9 : TopologicalSpace R
inst_10 : ContinuousSMul R M
f : R →L[R] M
⊢ toSpanSingleton R ((fun (f : R →L[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) = f
have h : Eq.{u_3 + 1} (α := M) ((toSpanSingleton R ((fun (f : R →L[R] M) ↦ ((f : (a : R) → M) 1 : M)) f) : (a : R) → M) 1 : M)
  ((f : (a : R) → M) 1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
x y : M₂
⊢ c.smulRight (x + y) = HAdd.hAdd (α := M →L[R] M₂) (c.smulRight x) (c.smulRight y)
have h : ∀ (e : M),
  Eq.{u_5 + 1} (α := M₂) ((c.smulRight (x + y) : (a : M) → M₂) e : M₂)
    ((HAdd.hAdd (α := M →L[R] M₂) (c.smulRight x) (c.smulRight y) : (a : M) → M₂) e : M₂)
Tactic: ext e
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
⊢ c.smulRight (a • x) = HSMul.hSMul (α := T) (β := M →L[R] M₂) ((RingHom.id T : (a : T) → T) a : T) (c.smulRight x)
have h : ∀ (e : M),
  Eq.{u_5 + 1} (α := M₂) ((c.smulRight (a • x) : (a : M) → M₂) e : M₂)
    ((HSMul.hSMul (α := T) (β := M →L[R] M₂) ((RingHom.id T : (a : T) → T) a : T) (c.smulRight x) : (a : M) → M₂) e :
      M₂)
Tactic: ext e
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
M : Type u_4
M₂ : Type u_5
inst : Semiring R
inst_1 : Semiring S
inst_2 : Semiring T
inst_3 : Module R S
inst_4 : AddCommMonoid M₂
inst_5 : Module R M₂
inst_6 : Module S M₂
inst_7 : IsScalarTower R S M₂
inst_8 : TopologicalSpace S
inst_9 : TopologicalSpace M₂
inst_10 : ContinuousSMul S M₂
inst_11 : TopologicalSpace M
inst_12 : AddCommMonoid M
inst_13 : Module R M
inst_14 : ContinuousAdd M₂
inst_15 : Module T M₂
inst_16 : ContinuousConstSMul T M₂
inst_17 : SMulCommClass R T M₂
inst_18 : SMulCommClass S T M₂
c : M →L[R] S
a : T
x : M₂
e : M
⊢ Eq.{u_5 + 1} (α := M₂) ((c.smulRight (a • x) : (a : M) → M₂) e : M₂)
    ((HSMul.hSMul (α := T) (β := M →L[R] M₂) ((RingHom.id T : (a : T) → T) a : T) (c.smulRight x) : (a : M) → M₂) e :
      M₂)
have h : HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((c : (a : M) → S) e : S) (a • x) =
  a • HSMul.hSMul.{u_2, u_5, u_5} (α := S) ((c : (a : M) → S) e : S) x
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent (hypothesis)
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
⊢ 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
have this : IsUnit (M := M →ₗ[R] M) ((toLinearMapRingHom : (a : M →L[R] M) → M →ₗ[R] M) T : M →ₗ[R] M)
Tactic: have := hT.map ContinuousLinearMap.toLinearMapRingHom
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent (goal)
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)
⊢ 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
have 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
Tactic: lift T to (M →L[R] M)ˣ using hT
Cleared hypotheses: T, hT, this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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 = 0 ↔ ∀ (i : ι), f i = 0
have 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)
Tactic: simp only [ContinuousLinearMap.ext_iff, pi_apply, funext_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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
⊢ (fun (i : α) ↦ (x + y) (f i)) = HAdd.hAdd (α := (i : α) → φ (f i)) (fun (i : α) ↦ x (f i)) fun (i : α) ↦ y (f i)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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
⊢ (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)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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 = 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₂
have 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₃)
Tactic: simp only [← coe_inj, LinearMap.prod_ext_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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
⊢ (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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)
⊢ (f₁ + g₁).coprod (f₂ + g₂) = f₁.coprod f₂ + g₁.coprod g₂
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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₂
⊢ (f ∘SL inl R M M₁).coprod (f ∘SL inr R M M₁) = f
have rw : f ∘SL coprod (inl R M M₁) (inr R M M₁) = f
Tactic: rw [← ContinuousLinearMap.comp_coprod, coprod_inl_inr, comp_id]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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
⊢ (f ∘SL inl R M M₁).coprod (f ∘SL inr R M M₁) = f
have rw₁ : f ∘SL ContinuousLinearMap.id R (M × M₁) = f
Tactic: rw [← ContinuousLinearMap.comp_coprod, coprod_inl_inr, comp_id]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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
⊢ (f ∘SL inl R M M₁).coprod (f ∘SL inr R M M₁) = f
have rw₂ : f = f
Tactic: rw [← ContinuousLinearMap.comp_coprod, coprod_inl_inr, comp_id]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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)
⊢ (r • a).1.coprod (r • a).2 = HSMul.hSMul (α := S) ((RingHom.id S : (a : S) → S) r : S) (a.1.coprod a.2)
have dsimp : (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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)
⊢ (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd (goal)
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)
⊢ (r • a.1).coprod (r • a.2) = r • a.1.coprod a.2
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict (goal)
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Ring R₁
inst_1 : Ring R₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
inst_2 : RingHomInvPair σ₁₂ σ₂₁
M₁ : Type u_4
M₂ : Type u_5
inst_3 : TopologicalSpace M₁
inst_4 : AddCommGroup M₁
inst_5 : Module R₁ M₁
inst_6 : TopologicalSpace M₂
inst_7 : AddCommGroup M₂
inst_8 : Module R₂ M₂
inst_9 : IsTopologicalAddGroup M₁
f₁ : M₁ →SL[σ₁₂] M₂
f₂ : M₂ →SL[σ₂₁] M₁
h : Function.RightInverse.{u_4 + 1, u_5 + 1} (α := M₁) (β := M₂) (⇑f₂ : (a : M₂) → M₁) (⇑f₁ : (a : M₁) → M₂)
x : ↥(↑f₁ : M₁ →ₛₗ[σ₁₂] M₂).ker
⊢ (f₁.projKerOfRightInverse f₂ h : (a : M₁) → ↥(↑f₁ : M₁ →ₛₗ[σ₁₂] M₂).ker) (↑x : M₁) = x
have a : (↑((f₁.projKerOfRightInverse f₂ h : (a : M₁) → ↥(↑f₁ : M₁ →ₛₗ[σ₁₂] M₂).ker) (↑x : M₁)) : M₁) = (↑x : M₁)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (LinearMap.pi (φ := φ) fun (i : ι) ↦
          if h : i ∈ I then
            LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
          else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → (i : ι) → φ i)
      a i
have dsimp : Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
  (if h : i ∈ I then
        LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
      else 0 :
      (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
    a
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (if h : i ∈ I then
          LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
        else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a
have pos : ∀ (h : i ∈ I),
  Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
pos :
  ∀ (h : i ∈ I),
    Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
      (LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) :
          (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
        a
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (if h : i ∈ I then
          LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
        else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a
have neg : i ∉ I →
  Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (0 : (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i) a
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
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)
I J : Set ι
inst_10 : DecidablePred fun (i : ι) ↦ i ∈ I
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
i : ι
⊢ Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (if h : i ∈ I then
          LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h)
        else 0 :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a
have pos : ∀ (h : i ∈ I),
  Continuous[Pi.topologicalSpace, inst_7 i] fun (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) ↦
    (LinearMap.proj (φ := fun (i : (↑I : Type u_4)) ↦ φ (↑i : ι)) (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) :
        (a : (i : (↑I : Type u_4)) → φ (↑i : ι)) → φ i)
      a
Tactic: split_ifs <;> [apply continuous_apply; exact continuous_zero]