awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Complement
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
F : Type u_3
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : IsTopologicalAddGroup E
inst_5 : TopologicalSpace F
inst_6 : AddCommGroup F
inst_7 : Module R F
inst_8 : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ₁ φ₂ : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ₁ ψ₂ : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
x : E
⊢ Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) : (a : E) → F) x : F)
    ((ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂ : (a : E) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Complement
Goal:
R : Type u_1
inst : Ring R
E : Type u_2
F : Type u_3
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module R E
inst_4 : IsTopologicalAddGroup E
inst_5 : TopologicalSpace F
inst_6 : AddCommGroup F
inst_7 : Module R F
inst_8 : ContinuousAdd F
p q : Submodule R E
h : IsTopCompl p q
φ : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥p) F
ψ : ContinuousLinearMap.{u_1, u_1, u_2, u_3} (RingHom.id R) (↥q) F
⊢ (↑(ofIsTopCompl h φ ψ) : E →ₗ[R] F).range = (↑φ : ↥p →ₗ[R] F).range ⊔ (↑ψ : ↥q →ₗ[R] F).range

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f g : M₁ →SL[σ₁₂] M₂
H : (↑f : M₁ →ₛₗ[σ₁₂] M₂) = (↑g : M₁ →ₛₗ[σ₁₂] M₂)
mk :
  ∀ (toLinearMap : M₁ →ₛₗ[σ₁₂] M₂) (cont : Continuous[inst_2, inst_4] toLinearMap.toFun)
    (H : (↑{ toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂) = (↑g : M₁ →ₛₗ[σ₁₂] M₂)),
    { toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
g : M₁ →SL[σ₁₂] M₂
toLinearMap : M₁ →ₛₗ[σ₁₂] M₂
cont : Continuous[inst_2, inst_4] toLinearMap.toFun
H : (↑{ toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂) = (↑g : M₁ →ₛₗ[σ₁₂] M₂)
mk :
  ∀ (toLinearMap_1 : M₁ →ₛₗ[σ₁₂] M₂) (cont_1 : Continuous[inst_2, inst_4] toLinearMap_1.toFun)
    (H :
      (↑{ toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂) =
        (↑{ toLinearMap := toLinearMap_1, cont := cont_1 : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂)),
    { toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } = { toLinearMap := toLinearMap_1, cont := cont_1 }
⊢ { toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } = g

Tactic:
cases g
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
toLinearMap : M₁ →ₛₗ[σ₁₂] M₂
cont : Continuous[inst_2, inst_4] toLinearMap.toFun
toLinearMap_1 : M₁ →ₛₗ[σ₁₂] M₂
cont_1 : Continuous[inst_2, inst_4] toLinearMap_1.toFun
H :
  (↑{ toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂) =
    (↑{ toLinearMap := toLinearMap_1, cont := cont_1 : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂)
⊢ { toLinearMap := toLinearMap, cont := cont : M₁ →SL[σ₁₂] M₂ } = { toLinearMap := toLinearMap_1, cont := cont_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
h : Continuous[inst_2, inst_4] f.toFun
⊢ (↑{ toLinearMap := f, cont := h : M₁ →SL[σ₁₂] M₂ } : M₁ →ₛₗ[σ₁₂] M₂) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
h : Continuous[inst_2, inst_4] f.toFun
⊢ Eq (α := (a : M₁) → M₂) (⇑{ toLinearMap := f, cont := h : M₁ →SL[σ₁₂] M₂ } : (a : M₁) → M₂) (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ Continuous[inst_2, inst_4] (⇑f : (a : M₁) → M₂)

Tactic:
f.2

Premises used: ContinuousLinearMap.cont
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ Continuous[inst_2, inst_4] (⇑(↑f : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂)

Tactic:
f.2

Premises used: ContinuousLinearMap.cont
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
E₁ : Type u_9
E₂ : Type u_10
inst_2 : UniformSpace E₁
inst_3 : UniformSpace E₂
inst_4 : AddCommGroup E₁
inst_5 : AddCommGroup E₂
inst_6 : Module R₁ E₁
inst_7 : Module R₂ E₂
inst_8 : IsUniformAddGroup E₁
inst_9 : IsUniformAddGroup E₂
f : E₁ →SL[σ₁₂] E₂
⊢ UniformContinuous.{u_9, u_10} (α := E₁) (β := E₂) (⇑f : (a : E₁) → E₂)

Tactic:
uniformContinuous_addMonoidHom_of_continuous f.continuous

Premises used: ContinuousLinearMap.continuous, uniformContinuous_addMonoidHom_of_continuous
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f g : M₁ →SL[σ₁₂] M₂
⊢ (↑f : M₁ →ₛₗ[σ₁₂] M₂) = (↑g : M₁ →ₛₗ[σ₁₂] M₂) ↔ f = g

Tactic:
coe_injective.eq_iff

Premises used: Function.Injective.eq_iff, ContinuousLinearMap.coe_injective
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
⊢ Function.Injective (α := M₁ →SL[σ₁₂] M₂) (β := M₁ → M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
⊢ Function.Injective (α := M₁ →SL[σ₁₂] M₂) (β := M₁ →ₜ+ M₂) ContinuousAddMonoidHom.toContinuousAddMonoidHom

Tactic:
(DFunLike.coe_injective.of_comp_iff _).1 DFunLike.coe_injective

Premises used: DFunLike.coe_injective, Iff.mp, Function.Injective.of_comp_iff
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f g : M₁ →SL[σ₁₂] M₂
⊢ Eq (α := M₁ →ₜ+ M₂) (↑f : M₁ →ₜ+ M₂) (↑g : M₁ →ₜ+ M₂) ↔ f = g

Tactic:
toContinuousAddMonoidHom_injective.eq_iff

Premises used: Function.Injective.eq_iff, ContinuousLinearMap.toContinuousAddMonoidHom_injective
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f g : M₁ →SL[σ₁₂] M₂
h : ∀ (x : M₁), Eq.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) x : M₂) ((g : (a : M₁) → M₂) x : M₂)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ Eq (α := (a : M₁) → M₂) (⇑(↑f : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂) (⇑f : (a : M₁) → M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
f' : M₁ → M₂
h : f' = (⇑f : (a : M₁) → M₂)
⊢ (⇑(f.copy f' h) : (a : M₁) → M₂) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
f' : M₁ → M₂
h : f' = (⇑f : (a : M₁) → M₂)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
h :
  ∀ (f : (a : M₁) → M₂),
    Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
        f ↔
      Membership.mem (γ := Set ((a : M₁) → M₂))
        ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
          Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
        f
⊢ Eq (α := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
    ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
      Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))

Tactic:
ext f
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : (a : M₁) → M₂
h :
  Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f →
    Membership.mem (γ := Set ((a : M₁) → M₂))
      ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
        Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f
h₁ :
  Membership.mem (γ := Set ((a : M₁) → M₂))
      ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
        Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f →
    Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f
⊢ Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f ↔
    Membership.mem (γ := Set ((a : M₁) → M₂))
      ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
        Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
      f

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ Membership.mem (γ := Set ((a : M₁) → M₂))
    ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
      Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
    (⇑f : (a : M₁) → M₂)

Tactic:
⟨f.continuous, f, rfl⟩

Premises used: Set.Mem, setOf, ContinuousLinearMap.toLinearMap, Set.inter, ContinuousLinearMap.continuous, And.intro, Exists.intro, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ Membership.mem (γ := Set ((a : M₁) → M₂))
    ({f : M₁ → M₂ | Continuous[inst_2, inst_4] f} ∩
      Set.range (ι := M₁ →ₛₗ[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
    (⇑f : (a : M₁) → M₂)

Tactic:
exact ⟨f.continuous, f, rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hfc : Membership.mem (γ := Set (M₁ → M₂)) {f : M₁ → M₂ | Continuous[inst_2, inst_4] f} (⇑f : (a : M₁) → M₂)
⊢ Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
    (⇑f : (a : M₁) → M₂)

Tactic:
⟨⟨f, hfc⟩, rfl⟩

Premises used: Set.Mem, ContinuousLinearMap.mk, setOf, Exists.intro, Set.range, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →ₛₗ[σ₁₂] M₂
hfc : Membership.mem (γ := Set (M₁ → M₂)) {f : M₁ → M₂ | Continuous[inst_2, inst_4] f} (⇑f : (a : M₁) → M₂)
⊢ Membership.mem (γ := Set ((a : M₁) → M₂)) (Set.range (ι := M₁ →SL[σ₁₂] M₂) (DFunLike.coe (β := fun (x : M₁) ↦ M₂)))
    (⇑f : (a : M₁) → M₂)

Tactic:
exact ⟨⟨f, hfc⟩, rfl⟩
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ Eq.{u_6 + 1} (α := Set M₂) (Set.range.{u_6, u_4 + 1} (ι := M₁) (⇑(↑f : M₁ →ₛₗ[σ₁₂] M₂) : (a : M₁) → M₂))
    (Set.range.{u_6, u_4 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
⊢ Eq.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) 0 : M₂) (0 : M₂)

Tactic:
map_zero f

Premises used: map_zero
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
x y : M₁
⊢ (f : (a : M₁) → M₂) (x + y) = HAdd.hAdd (α := M₂) (β := M₂) ((f : (a : M₁) → M₂) x : M₂) ((f : (a : M₁) → M₂) y : M₂)

Tactic:
map_add f x y

Premises used: map_add
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
c : R₁
x : M₁
⊢ (f : (a : M₁) → M₂) (c • x) =
    HSMul.hSMul.{u_2, u_6, u_6} (α := R₂) (β := M₂) ((σ₁₂ : (a : R₁) → R₂) c : R₂) ((f : (a : M₁) → M₂) x : M₂)

Tactic:
(toLinearMap _).map_smulₛₗ _ _

Premises used: ContinuousLinearMap.toLinearMap, LinearMap.map_smulₛₗ
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
M₂ : Type u_6
inst_3 : TopologicalSpace M₂
inst_4 : AddCommMonoid M₂
inst_5 : Module R₁ M₁
inst_6 : Module R₁ M₂
f : M₁ →L[R₁] M₂
c : R₁
x : M₁
⊢ (f : (a : M₁) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M₁) → M₂) x : M₂)

Tactic:
simp only [RingHom.id_apply, map_smulₛₗ]

Premises used: RingHom.id_apply, MulActionSemiHomClass.map_smulₛₗ
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
M₁ : Type u_4
inst : TopologicalSpace M₁
inst_1 : AddCommMonoid M₁
M₂ : Type u_6
inst_2 : TopologicalSpace M₂
inst_3 : AddCommMonoid M₂
R : Type u_9
S : Type u_10
inst_4 : Semiring S
inst_5 : SMul R M₁
inst_6 : Module S M₁
inst_7 : SMul R M₂
inst_8 : Module S M₂
inst_9 : LinearMap.CompatibleSMul M₁ M₂ R S
f : M₁ →L[S] M₂
c : R
x : M₁
⊢ (f : (a : M₁) → M₂) (c • x) = HSMul.hSMul (β := M₂) c ((f : (a : M₁) → M₂) x : M₂)

Tactic:
LinearMap.CompatibleSMul.map_smul (f : M₁ →ₗ[S] M₂) c x

Premises used: ContinuousLinearMap.toLinearMap, LinearMap.CompatibleSMul.map_smul
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
f g : R₁ →L[R₁] M₁
h : Eq.{u_4 + 1} (α := M₁) ((f : (a : R₁) → M₁) 1 : M₁) ((g : (a : R₁) → M₁) 1 : M₁)
⊢ f = g

Tactic:
coe_inj.1 <| LinearMap.ext_ring h

Premises used: ContinuousLinearMap.coe_inj, LinearMap.ext_ring, Iff.mp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
x : ↥(↑f : M₁ →ₛₗ[σ₁₂] M₂).ker
⊢ Eq.{u_6 + 1} (α := M₂) ((f : (a : M₁) → M₂) (↑x : M₁) : M₂) (0 : M₂)

Tactic:
x.2

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Subtype.property
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : T2Space M₂
s : Set M₁
f g : M₁ →SL[σ₁₂] M₂
h : Set.EqOn.{u_4, u_6} (β := M₂) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₁) → M₂) s
⊢ Set.EqOn.{u_4, u_6} (β := M₂) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₁) → M₂)
    (closure[inst_2] (↑(Submodule.span R₁ s) : Set M₁))

Tactic:
(LinearMap.eqOn_span' h).closure f.continuous g.continuous

Premises used: LinearMap.eqOn_span', Set.EqOn.closure, ContinuousLinearMap.continuous
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : T2Space M₂
s : Set M₁
hs : Dense (↑(Submodule.span R₁ s) : Set M₁)
f g : M₁ →SL[σ₁₂] M₂
h : Set.EqOn.{u_4, u_6} (β := M₂) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₁) → M₂) s
⊢ f = g

Tactic:
ext fun x => eqOn_closure_span h (hs x)

Premises used: ContinuousLinearMap.eqOn_closure_span, ContinuousLinearMap.ext
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
M₂ : Type u_6
inst_4 : TopologicalSpace M₂
inst_5 : AddCommMonoid M₂
inst_6 : Module R₁ M₁
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
inst_9 : TopologicalSpace R₁
inst_10 : TopologicalSpace R₂
inst_11 : ContinuousSMul R₁ M₁
inst_12 : ContinuousAdd M₁
inst_13 : ContinuousSMul R₂ M₂
inst_14 : ContinuousAdd M₂
f : M₁ →SL[σ₁₂] M₂
s : Submodule R₁ M₁
⊢ Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s.topologicalClosure ≤ (Submodule.map (↑f : M₁ →ₛₗ[σ₁₂] M₂) s).topologicalClosure

Tactic:
image_closure_subset_closure_image f.continuous

Premises used: Set.Mem, setOf, Set.Subset, ContinuousLinearMap.continuous, closure, image_closure_subset_closure_image, Set.image, Set.sInter
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
inst_6 : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
s : Submodule R₁ M₁
hs : s ∈ Module.End.invtSubmodule (↑f : M₁ →ₗ[R₁] M₁)
rw :
  ∀ (hs : Submodule.map (↑f : M₁ →ₗ[R₁] M₁) s ≤ s),
    Submodule.map (↑f : M₁ →ₗ[R₁] M₁) s.topologicalClosure ≤ s.topologicalClosure
⊢ s.topologicalClosure ∈ Module.End.invtSubmodule (↑f : M₁ →ₗ[R₁] M₁)

Tactic:
rw [Module.End.mem_invtSubmodule_iff_map_le] at hs ⊢

Premises used: Module.End.mem_invtSubmodule_iff_map_le
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
inst_6 : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
s : Submodule R₁ M₁
hs : Submodule.map (↑f : M₁ →ₗ[R₁] M₁) s ≤ s
⊢ Submodule.map (↑f : M₁ →ₗ[R₁] M₁) s.topologicalClosure ≤ s.topologicalClosure

Tactic:
(s.topologicalClosure_map f).trans (Submodule.topologicalClosure_mono hs)

Premises used: Submodule.topologicalClosure_map, Submodule.topologicalClosure_mono, LE.le.trans
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Goal:
R₁ : Type u_1
inst : Semiring R₁
M₁ : Type u_4
inst_1 : TopologicalSpace M₁
inst_2 : AddCommMonoid M₁
inst_3 : Module R₁ M₁
inst_4 : TopologicalSpace R₁
inst_5 : ContinuousSMul R₁ M₁
inst_6 : ContinuousAdd M₁
f : M₁ →L[R₁] M₁
s : Submodule R₁ M₁
hs : Submodule.map (↑f : M₁ →ₗ[R₁] M₁) s ≤ s
⊢ Submodule.map (↑f : M₁ →ₗ[R₁] M₁) s.topologicalClosure ≤ s.topologicalClosure

Tactic:
exact (s.topologicalClosure_map f).trans (Submodule.topologicalClosure_mono hs)

Premises used: Submodule.topologicalClosure_map, Submodule.topologicalClosure_mono, LE.le.trans