awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
x : M ⧸ S
⊢ Eq.{u_4 + 1} (α := M₂) ((S.liftQL f h : (a : M ⧸ S) → M₂) x : M₂)
    ((S.liftQ (↑f : M →ₛₗ[σ] M₂) h : (a : M ⧸ S) → M₂) x : M₂)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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
p : Submodule R M
⊢ (↑p.subtypeL : ↥p →ₗ[R] M) = p.subtype

Tactic:
rfl

Premises used: Submodule.subtype, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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
p : Submodule R M
⊢ Eq (α := (a : ↥p) → M) (⇑p.subtypeL : (a : ↥p) → M) (⇑p.subtype : (a : ↥p) → M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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
p : Submodule R M
x : ↥p
⊢ (p.subtypeL : (a : ↥p) → M) x = (↑x : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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
p : Submodule R M
⊢ (↑p.subtypeL : ↥p →ₗ[R] M).range = p

Tactic:
Submodule.range_subtype _

Premises used: Submodule.subtype, Submodule.range_subtype
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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
p : Submodule R M
⊢ (↑p.subtypeL : ↥p →ₗ[R] M).ker = ⊥

Tactic:
Submodule.ker_subtype _

Premises used: Submodule.ker_subtype, Submodule.subtype
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₁ M₁
⊢ (↑(f.domRestrict p) : ↥p →ₛₗ[σ₁₂] M₂) = (↑f : M₁ →ₛₗ[σ₁₂] M₂).domRestrict p

Tactic:
rfl

Premises used: LinearMap.domRestrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₁ M₁
⊢ Eq (α := (a : ↥p) → M₂) ((⇑(f.domRestrict p) : (a : ↥p) → M₂) : (a : ↥p) → M₂)
    ((↑p : Set M₁).restrict (π := fun (a : M₁) ↦ M₂) (⇑f : (a : M₁) → M₂) : (a : (↑(↑p : Set M₁) : Type u_4)) → M₂)

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₂ M₂
h : ∀ (x : M₁), Membership.mem (α := M₂) p ((f : (a : M₁) → M₂) x : M₂)
⊢ (↑(f.codRestrict p h) : M₁ →ₛₗ[σ₁₂] ↥p) = LinearMap.codRestrict p (↑f : M₁ →ₛₗ[σ₁₂] M₂) h

Tactic:
rfl

Premises used: LinearMap.codRestrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₂ M₂
h : ∀ (x : M₁), Membership.mem (α := M₂) p ((f : (a : M₁) → M₂) x : M₂)
⊢ (⇑(f.codRestrict p h) : (a : M₁) → ↥p) = Set.codRestrict (⇑f : (a : M₁) → M₂) (↑p : Set M₂) h

Tactic:
rfl

Premises used: Set.codRestrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₂ M₂
h : ∀ (x : M₁), Membership.mem (α := M₂) p ((f : (a : M₁) → M₂) x : M₂)
x : M₁
⊢ Eq.{u_5 + 1} (α := M₂) ((↑((f.codRestrict p h : (a : M₁) → ↥p) x) : M₂) : M₂) ((f : (a : M₁) → M₂) x : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₂ M₂
h : ∀ (x : M₁), Membership.mem (α := M₂) p ((f : (a : M₁) → M₂) x : M₂)
⊢ (↑(f.codRestrict p h) : M₁ →ₛₗ[σ₁₂] ↥p).ker = (↑f : M₁ →ₛₗ[σ₁₂] M₂).ker

Tactic:
f.toLinearMap.ker_codRestrict p h

Premises used: LinearMap.ker_codRestrict, ContinuousLinearMap.toLinearMap, LinearMap.codRestrict
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
inst_9 : Module R₂ M₂
inst_10 : TopologicalSpace M₃
inst_11 : AddCommMonoid M₃
inst_12 : Module R₃ M₃
g : M₂ →SL[σ₂₃] M₃
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₂ M₂
h : ∀ (x : M₁), Membership.mem (α := M₂) p ((f : (a : M₁) → M₂) x : M₂)
⊢ g.domRestrict p ∘SL f.codRestrict p h = g ∘SL f

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.domRestrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
f : M₁ →SL[σ₁₂] M₂
⊢ Eq (α := LinearMap.{u_1, u_2, u_4, u_5} σ₁₂ M₁ ↥(↑f : M₁ →ₛₗ[σ₁₂] M₂).range)
    (↑f.rangeRestrict : M₁ →ₛₗ[σ₁₂] ↥(↑f : M₁ →ₛₗ[σ₁₂] M₂).range) (↑f : M₁ →ₛₗ[σ₁₂] M₂).rangeRestrict

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
inst_8 : RingHomSurjective σ₁₂
f : M₁ →SL[σ₁₂] M₂
⊢ Eq (α := (a : M₁) → ↥(↑f : M₁ →ₛₗ[σ₁₂] M₂).range) (⇑f.rangeRestrict : (a : M₁) → ↥(↑f : M₁ →ₛₗ[σ₁₂] M₂).range)
    (Set.rangeFactorization (⇑f : (a : M₁) → M₂))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.range, Set.rangeFactorization, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₁ M₁
q : Submodule R₂ M₂
h : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M₁) → M₂) x : M₂)
⊢ (↑(f.restrict h) : ↥p →ₛₗ[σ₁₂] ↥q) = (↑f : M₁ →ₛₗ[σ₁₂] M₂).restrict h

Tactic:
rfl

Premises used: LinearMap.restrict, LinearMap.codRestrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₁ M₁
q : Submodule R₂ M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M₁) → M₂) x : M₂)
x : ↥p
⊢ Eq.{u_5 + 1} (α := M₂) ((↑((f.restrict hf : (a : ↥p) → ↥q) x) : M₂) : M₂) ((f : (a : M₁) → M₂) (↑x : M₁) : M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₁ M₁
q : Submodule R₂ M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M₁) → M₂) x : M₂)
x : ↥p
⊢ Eq.{u_5 + 1} (α := ↥q) ((f.restrict hf : (a : ↥p) → ↥q) x : ↥q)
    (Subtype.mk (p := fun (x : M₂) ↦ x ∈ q) ((f : (a : M₁) → M₂) (↑x : M₁)) ⋯ : ↥q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
M₁ : Type u_4
M₂ : Type u_5
M₃ : Type u_6
inst_4 : TopologicalSpace M₁
inst_5 : AddCommMonoid M₁
inst_6 : Module R₁ M₁
inst_7 : TopologicalSpace M₂
inst_8 : AddCommMonoid M₂
inst_9 : Module R₂ M₂
inst_10 : TopologicalSpace M₃
inst_11 : AddCommMonoid M₃
inst_12 : Module R₃ M₃
p : Submodule R₁ M₁
p₂ : Submodule R₂ M₂
p₃ : Submodule R₃ M₃
f : M₁ →SL[σ₁₂] M₂
g : M₂ →SL[σ₂₃] M₃
hf : MapsTo (⇑f : (a : M₁) → M₂) (↑p : Set M₁) (↑p₂ : Set M₂)
hg : MapsTo (⇑g : (a : M₂) → M₃) (↑p₂ : Set M₂) (↑p₃ : Set M₃)
hfg : MapsTo (⇑(g ∘SL f) : (a : M₁) → M₃) (↑p : Set M₁) (↑p₃ : Set M₃)
⊢ (g ∘SL f).restrict hfg = g.restrict hg ∘SL f.restrict hf

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.codRestrict, LinearMap.codRestrict, ContinuousLinearMap.restrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₁ M₁
q : Submodule R₂ M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M₁) → M₂) x : M₂)
⊢ q.subtypeL ∘SL f.restrict hf = f.domRestrict p

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, Submodule.subtypeL, Submodule.subtype, ContinuousLinearMap.domRestrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₁ M₁
q : Submodule R₂ M₂
hf : ∀ x ∈ p, Membership.mem (α := M₂) q ((f : (a : M₁) → M₂) x : M₂)
⊢ f.restrict hf = (f.domRestrict p).codRestrict q ⋯

Tactic:
rfl

Premises used: ContinuousLinearMap.restrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
inst : Semiring R₁
inst_1 : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
M₂ : Type u_5
inst_2 : TopologicalSpace M₁
inst_3 : AddCommMonoid M₁
inst_4 : Module R₁ M₁
inst_5 : TopologicalSpace M₂
inst_6 : AddCommMonoid M₂
inst_7 : Module R₂ M₂
f : M₁ →SL[σ₁₂] M₂
p : Submodule R₁ M₁
q : Submodule R₂ M₂
hf : ∀ (x : M₁), Membership.mem (α := M₂) q ((f : (a : M₁) → M₂) x : M₂)
⊢ f.restrict ⋯ = (f.codRestrict q hf).domRestrict p

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.codRestrict, LinearMap.codRestrict, ContinuousLinearMap.domRestrict, ContinuousLinearMap.restrict, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Goal:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
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 : M₁
⊢ Membership.mem (α := M₁) (↑f₁ : M₁ →ₛₗ[σ₁₂] M₂).ker
    ((ContinuousLinearMap.id R₁ M₁ - f₂ ∘SL f₁ : (a : M₁) → M₁) x : M₁)

Tactic:
simp [h (f₁ x)]

Premises used: DFunLike.coe
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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 : M₁
⊢ (↑((f₁.projKerOfRightInverse f₂ h : (a : M₁) → ↥(↑f₁ : M₁ →ₛₗ[σ₁₂] M₂).ker) x) : M₁) =
    HSub.hSub (β := M₁) x ((f₂ : (a : M₂) → M₁) ((f₁ : (a : M₁) → M₂) x : M₂) : M₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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
a : (↑((f₁.projKerOfRightInverse f₂ h : (a : M₁) → ↥(↑f₁ : M₁ →ₛₗ[σ₁₂] M₂).ker) (↑x : M₁)) : M₁) = (↑x : M₁)
⊢ (f₁.projKerOfRightInverse f₂ h : (a : M₁) → ↥(↑f₁ : M₁ →ₛₗ[σ₁₂] M₂).ker) (↑x : M₁) = x

Tactic:
ext1
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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₁)) : M₁) = (↑x : M₁)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
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₂)
y : M₂
⊢ Eq.{u_4 + 1} (α := M₁)
    (↑((f₁.projKerOfRightInverse f₂ h : (a : M₁) → ↥(↑f₁ : M₁ →ₛₗ[σ₁₂] M₂).ker) ((f₂ : (a : M₂) → M₁) y)) : M₁)
    (↑0 : M₁)

Tactic:
simp [h y]
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
Goal:
A : Type u_1
M₁ : Type u_2
M₂ : Type u_3
R : Type u_4
inst : Semiring A
inst_1 : Semiring R
inst_2 : AddCommMonoid M₁
inst_3 : Module A M₁
inst_4 : Module R M₁
inst_5 : TopologicalSpace M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module A M₂
inst_8 : Module R M₂
inst_9 : TopologicalSpace M₂
inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A
f : M₁ →L[A] M₂
⊢ Eq (α := M₁ →ₗ[R] M₂) (↑(restrictScalars R f) : M₁ →ₗ[R] M₂)
    ((↑R :
        {S : Type u_1} →
          {M : Type u_2} →
            {M₂ : Type u_3} →
              [inst : Semiring R] →
                [inst_11 : Semiring S] →
                  [inst_12 : AddCommMonoid M] →
                    [inst_13 : AddCommMonoid M₂] →
                      [inst_14 : Module R M] →
                        [inst_15 : Module R M₂] →
                          [inst_16 : Module S M] →
                            [inst_17 : Module S M₂] →
                              [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (↑f : M₁ →ₗ[A] M₂))

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
Goal:
A : Type u_1
M₁ : Type u_2
M₂ : Type u_3
R : Type u_4
inst : Semiring A
inst_1 : Semiring R
inst_2 : AddCommMonoid M₁
inst_3 : Module A M₁
inst_4 : Module R M₁
inst_5 : TopologicalSpace M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module A M₂
inst_8 : Module R M₂
inst_9 : TopologicalSpace M₂
inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A
f : M₁ →L[A] M₂
⊢ Eq (α := M₁ →ₜ+ M₂) (↑(restrictScalars R f) : M₁ →ₜ+ M₂) (↑f : M₁ →ₜ+ M₂)

Tactic:
rfl

Premises used: ContinuousAddMonoidHom.toContinuousAddMonoidHom, ContinuousLinearMap.restrictScalars, AddMonoidHomClass.toAddMonoidHom, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
Goal:
A : Type u_1
M₁ : Type u_2
M₂ : Type u_3
R : Type u_4
inst : Semiring A
inst_1 : Semiring R
inst_2 : AddCommMonoid M₁
inst_3 : Module A M₁
inst_4 : Module R M₁
inst_5 : TopologicalSpace M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module A M₂
inst_8 : Module R M₂
inst_9 : TopologicalSpace M₂
inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A
⊢ Eq (α := M₁ →L[R] M₂) (restrictScalars.{u_1, u_2, u_3, u_4} (A := A) R 0) 0

Tactic:
rfl

Premises used: LinearMap.restrictScalars, ContinuousLinearMap.restrictScalars, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
Goal:
A : Type u_1
M₁ : Type u_2
M₂ : Type u_3
R : Type u_4
inst : Semiring A
inst_1 : Semiring R
inst_2 : AddCommMonoid M₁
inst_3 : Module A M₁
inst_4 : Module R M₁
inst_5 : TopologicalSpace M₁
inst_6 : AddCommMonoid M₂
inst_7 : Module A M₂
inst_8 : Module R M₂
inst_9 : TopologicalSpace M₂
inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A
inst_11 : ContinuousAdd M₂
f g : M₁ →L[A] M₂
⊢ restrictScalars R (f + g) = HAdd.hAdd (α := M₁ →L[R] M₂) (restrictScalars R f) (restrictScalars R g)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, ContinuousLinearMap.restrictScalars, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
Goal:
A : Type u_1
M₁ : Type u_2
M₂ : Type u_3
R : Type u_4
S : Type u_5
inst : Semiring A
inst_1 : Semiring R
inst_2 : Semiring S
inst_3 : AddCommMonoid M₁
inst_4 : Module A M₁
inst_5 : Module R M₁
inst_6 : TopologicalSpace M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module A M₂
inst_9 : Module R M₂
inst_10 : TopologicalSpace M₂
inst_11 : LinearMap.CompatibleSMul M₁ M₂ R A
inst_12 : Module S M₂
inst_13 : ContinuousConstSMul S M₂
inst_14 : SMulCommClass A S M₂
inst_15 : SMulCommClass R S M₂
c : S
f : M₁ →L[A] M₂
⊢ restrictScalars R (c • f) = HSMul.hSMul (β := M₁ →L[R] M₂) c (restrictScalars R f)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, ContinuousLinearMap.restrictScalars, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
Goal:
A : Type u_1
M₁ : Type u_2
M₂ : Type u_3
R : Type u_4
S : Type u_5
inst : Semiring A
inst_1 : Semiring R
inst_2 : Semiring S
inst_3 : AddCommMonoid M₁
inst_4 : Module A M₁
inst_5 : Module R M₁
inst_6 : TopologicalSpace M₁
inst_7 : AddCommMonoid M₂
inst_8 : Module A M₂
inst_9 : Module R M₂
inst_10 : TopologicalSpace M₂
inst_11 : LinearMap.CompatibleSMul M₁ M₂ R A
inst_12 : Module S M₂
inst_13 : ContinuousConstSMul S M₂
inst_14 : SMulCommClass A S M₂
inst_15 : SMulCommClass R S M₂
inst_16 : ContinuousAdd M₂
⊢ Eq (α := (a : M₁ →L[A] M₂) → M₁ →L[R] M₂) (⇑(restrictScalarsₗ A M₁ M₂ R S) : (a : M₁ →L[A] M₂) → M₁ →L[R] M₂)
    (restrictScalars R)

Tactic:
rfl

Premises used: ContinuousLinearMap.restrictScalars, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
Goal:
A : Type u_1
R : Type u_2
M₁ : Type u_4
M₂ : Type u_5
inst : Ring A
inst_1 : Ring R
inst_2 : AddCommGroup M₁
inst_3 : Module A M₁
inst_4 : Module R M₁
inst_5 : TopologicalSpace M₁
inst_6 : AddCommGroup M₂
inst_7 : Module A M₂
inst_8 : Module R M₂
inst_9 : TopologicalSpace M₂
inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A
inst_11 : IsTopologicalAddGroup M₂
f g : M₁ →L[A] M₂
⊢ restrictScalars R (f - g) = HSub.hSub (α := M₁ →L[R] M₂) (restrictScalars R f) (restrictScalars R g)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, ContinuousLinearMap.restrictScalars, rfl
-- Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.RestrictScalars
Goal:
A : Type u_1
R : Type u_2
M₁ : Type u_4
M₂ : Type u_5
inst : Ring A
inst_1 : Ring R
inst_2 : AddCommGroup M₁
inst_3 : Module A M₁
inst_4 : Module R M₁
inst_5 : TopologicalSpace M₁
inst_6 : AddCommGroup M₂
inst_7 : Module A M₂
inst_8 : Module R M₂
inst_9 : TopologicalSpace M₂
inst_10 : LinearMap.CompatibleSMul M₁ M₂ R A
inst_11 : IsTopologicalAddGroup M₂
f : M₁ →L[A] M₂
⊢ Eq (α := M₁ →L[R] M₂) (restrictScalars R (-f)) (-restrictScalars R f)

Tactic:
rfl

Premises used: LinearMap.restrictScalars, ContinuousLinearMap.restrictScalars, rfl
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : AddCommMonoid M
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R M
inst_9 : Module S M₂
inst_10 : EquivLike F M M₂
s : ContinuousSemilinearEquivClass F σ M M₂
⊢ ContinuousSemilinearMapClass F σ M M₂

Tactic:
{ s with }

Premises used: ContinuousSemilinearMapClass.mk
-- Module: Mathlib.Topology.Algebra.Module.Equiv
Goal:
F : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
σ' : S →+* R
inst_2 : RingHomInvPair σ σ'
inst_3 : RingHomInvPair σ' σ
M : Type u_4
inst_4 : TopologicalSpace M
inst_5 : AddCommMonoid M
M₂ : Type u_5
inst_6 : TopologicalSpace M₂
inst_7 : AddCommMonoid M₂
inst_8 : Module R M
inst_9 : Module S M₂
inst_10 : EquivLike F M M₂
s : ContinuousSemilinearEquivClass F σ M M₂
⊢ HomeomorphClass F M M₂

Tactic:
{ s with }

Premises used: ContinuousSemilinearEquivClass.map_continuous, ContinuousSemilinearEquivClass.inv_continuous, HomeomorphClass.mk