awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p : Submodule R M
h : p.ClosedComplemented
⊢ IsCompl p h.complement

Tactic:
h.isTopCompl_complement.isCompl

Premises used: Submodule.ClosedComplemented.isTopCompl_complement, Submodule.IsTopCompl.isCompl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p : Submodule R M
inst_4 : T1Space.{u_2} ↥p
h : p.ClosedComplemented
⊢ IsClosed[inst_1] (↑h.complement : Set M)

Tactic:
h.isTopCompl_complement.isClosed'

Premises used: Submodule.ClosedComplemented.isTopCompl_complement, Submodule.IsTopCompl.isClosed'
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
inst_4 : ContinuousSub M
inst_5 : T1Space M
p : Submodule R M
h : p.ClosedComplemented
⊢ IsClosed[inst_1] (↑p : Set M)

Tactic:
h.isTopCompl_complement.isClosed

Premises used: Submodule.ClosedComplemented.isTopCompl_complement, Submodule.IsTopCompl.isClosed
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
⊢ ClosedComplemented.{u_1, u_2} (R := R) (M := M) ⊥

Tactic:
isTopCompl_bot_top.closedComplemented

Premises used: Submodule.isTopCompl_bot_top, Submodule.IsTopCompl.closedComplemented
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
⊢ ClosedComplemented.{u_1, u_2} (R := R) (M := M) ⊤

Tactic:
isTopCompl_top_bot.closedComplemented

Premises used: Submodule.isTopCompl_top_bot, Submodule.IsTopCompl.closedComplemented
-- Module: Mathlib.Topology.Algebra.Module.Complement
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
f₁ : M →L[R] N
f₂ : N →L[R] M
h : LeftInverse.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f₂ : (a : N) → M) (⇑f₁ : (a : M) → N)
⊢ (↑f₁ : M →ₗ[R] N).range.ClosedComplemented

Tactic:
f₁.isTopCompl_range_ker_of_leftInverse f₂ h |>.closedComplemented

Premises used: ContinuousLinearMap.isTopCompl_range_ker_of_leftInverse, Submodule.IsTopCompl.closedComplemented
-- Module: Mathlib.Topology.Algebra.Module.Complement
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
N : Type u_3
inst_1 : TopologicalSpace M
inst_2 : TopologicalSpace N
inst_3 : AddCommGroup M
inst_4 : AddCommGroup N
inst_5 : Module R M
inst_6 : Module R N
inst_7 : ContinuousSub M
f₁ : M →L[R] N
f₂ : N →L[R] M
h : RightInverse.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f₂ : (a : N) → M) (⇑f₁ : (a : M) → N)
⊢ (↑f₁ : M →ₗ[R] N).ker.ClosedComplemented

Tactic:
f₂.isTopCompl_range_ker_of_leftInverse f₁ h.leftInverse |>.symm.closedComplemented

Premises used: Submodule.IsTopCompl.symm, ContinuousLinearMap.isTopCompl_range_ker_of_leftInverse, Submodule.IsTopCompl.closedComplemented, Function.RightInverse.leftInverse
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
inst_4 : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), (f : (a : M) → ↥p) (↑x : M) = x
x : ↥p
fst :
  (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).1 :
      M) =
    (↑(x, 0).1 : M)
snd :
  Eq (α := M)
    (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).2 :
      M)
    (↑(x, 0).2 : M)
⊢ Eq (α := ↥p × ↥(↑f : M →ₗ[R] ↥p).ker)
    ((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M) :
      ↥p × ↥(↑f : M →ₗ[R] ↥p).ker)
    ((x, 0) : ↥p × ↥(↑f : M →ₗ[R] ↥p).ker)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
inst_4 : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), (f : (a : M) → ↥p) (↑x : M) = x
x : ↥p
⊢ (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).1 :
      M) =
    (↑(x, 0).1 : M)

Tactic:
simp [hf]
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
inst_4 : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), (f : (a : M) → ↥p) (↑x : M) = x
x : ↥p
⊢ Eq (α := M)
    (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).2 :
      M)
    (↑(x, 0).2 : M)

Tactic:
simp [hf]
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
inst_4 : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), (f : (a : M) → ↥p) (↑x : M) = x
x : ↥(↑f : M →ₗ[R] ↥p).ker
fst :
  Eq (α := M)
    (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).1 :
      M)
    (↑(0, x).1 : M)
snd :
  (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).2 :
      M) =
    (↑(0, x).2 : M)
⊢ Eq (α := ↥p × ↥(↑f : M →ₗ[R] ↥p).ker)
    ((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M) :
      ↥p × ↥(↑f : M →ₗ[R] ↥p).ker)
    ((0, x) : ↥p × ↥(↑f : M →ₗ[R] ↥p).ker)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
inst_4 : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), (f : (a : M) → ↥p) (↑x : M) = x
x : ↥(↑f : M →ₗ[R] ↥p).ker
⊢ Eq (α := M)
    (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).1 :
      M)
    (↑(0, x).1 : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
inst_4 : IsTopologicalAddGroup M
p : Submodule R M
hp : p.ClosedComplemented
f : M →L[R] ↥p
hf : ∀ (x : ↥p), (f : (a : M) → ↥p) (↑x : M) = x
x : ↥(↑f : M →ₗ[R] ↥p).ker
⊢ (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).2 :
      M) =
    (↑(0, x).2 : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
⊢ IsTopCompl p q ↔ Continuous[inst_1, instTopologicalSpaceProd] (⇑(p.prodEquivOfIsCompl q h).symm : (a : M) → ↥p × ↥q)

Tactic:
⟨fun hTop ↦ ((p.projectionOntoL q hTop).prod (q.projectionOntoL p hTop.symm)).continuous.congr
    fun x ↦ (prodEquivOfIsCompl_symm_apply h x).symm,
  fun hCont ↦ ⟨h, continuous_subtype_val.comp <| continuous_fst.comp hCont⟩⟩

Premises used: continuous_subtype_val, Continuous.comp, continuous_fst, Submodule.prodEquivOfIsCompl_symm_apply, Submodule.IsTopCompl.symm, Continuous.congr, Submodule.IsTopCompl.mk, ContinuousLinearMap.continuous, Submodule.projectionOntoL, Iff.intro, ContinuousLinearMap.prod, Eq.symm
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
⊢ Continuous[instTopologicalSpaceProd, inst_1] (⇑(p.prodEquivOfIsCompl q h) : (a : ↥p × ↥q) → M)

Tactic:
(continuous_subtype_val.comp continuous_fst).add (continuous_subtype_val.comp continuous_snd)

Premises used: continuous_subtype_val, Continuous.comp, continuous_snd, continuous_fst, Continuous.add
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
rw : Continuous[instTopologicalSpaceProd, inst_1] (⇑(p.prodEquivOfIsCompl q h) : (a : ↥p × ↥q) → M)
⊢ IsTopCompl p q ↔ IsHomeomorph (X := ↥p × ↥q) (Y := M) (⇑(p.prodEquivOfIsCompl q h) : (a : ↥p × ↥q) → M)

Tactic:
rw [(p.prodEquivOfIsCompl q h).isHomeomorph_iff,
    isTopCompl_iff_continuous_symm_prodEquivOfIsCompl, and_iff_right]

Premises used: Submodule.prodEquivOfIsCompl, and_iff_right, LinearEquiv.isHomeomorph_iff, Submodule.IsCompl.isTopCompl_iff_continuous_symm_prodEquivOfIsCompl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
⊢ Continuous[instTopologicalSpaceProd, inst_1] (⇑(p.prodEquivOfIsCompl q h) : (a : ↥p × ↥q) → M)

Tactic:
continuous_prodEquivOfIsCompl h

Premises used: Submodule.continuous_prodEquivOfIsCompl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
⊢ Continuous[instTopologicalSpaceProd, inst_1] (⇑(p.prodEquivOfIsCompl q h) : (a : ↥p × ↥q) → M)

Tactic:
exact continuous_prodEquivOfIsCompl h

Premises used: Submodule.continuous_prodEquivOfIsCompl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsTopCompl p q
⊢ (↑(p.prodEquivOfIsTopCompl q h) : (↥p × ↥q) ≃ₗ[R] M) = p.prodEquivOfIsCompl q ⋯

Tactic:
rfl

Premises used: Submodule.prodEquivOfIsCompl, LinearEquiv.trans, rfl, LinearEquiv.ofBijective
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsTopCompl p q
x : ↥p × ↥q
⊢ (p.prodEquivOfIsTopCompl q h : (a : ↥p × ↥q) → M) x = (↑x.1 : M) + (↑x.2 : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsTopCompl p q
x : M
⊢ Eq (α := ↥p × ↥q) (((p.prodEquivOfIsTopCompl q h).symm : (a : M) → ↥p × ↥q) x : ↥p × ↥q)
    (((p.projectionOntoL q h : (a : M) → ↥p) x, (q.projectionOntoL p ⋯ : (a : M) → ↥q) x) : ↥p × ↥q)

Tactic:
prodEquivOfIsCompl_symm_apply h.isCompl x

Premises used: Submodule.prodEquivOfIsCompl_symm_apply, Submodule.IsTopCompl.isCompl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
h₁ :
  ∀ (x : M),
    Eq (α := ↥q)
      (Function.comp (β := M ⧸ p) (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q) (⇑p.mkQ : (a : M) → M ⧸ p) x :
        ↥q)
      ((q.projectionOnto p ⋯ : (a : M) → ↥q) x : ↥q)
⊢ Eq (α := M → ↥q)
    (Function.comp (β := M ⧸ p) (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q) (⇑p.mkQ : (a : M) → M ⧸ p))
    (⇑(q.projectionOnto p ⋯) : (a : M) → ↥q)

Tactic:
funext
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
x : M
⊢ Eq (α := ↥q)
    (Function.comp (β := M ⧸ p) (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q) (⇑p.mkQ : (a : M) → M ⧸ p) x : ↥q)
    ((q.projectionOnto p ⋯ : (a : M) → ↥q) x : ↥q)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
⊢ Eq (α := M → ↥q)
    (Function.comp (β := M ⧸ p) (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q) (⇑p.mkQ : (a : M) → M ⧸ p))
    (⇑(q.projectionOnto p ⋯) : (a : M) → ↥q)

Tactic:
have hproj : ⇑(p.quotientEquivOfIsCompl q h) ∘ ⇑p.mkQ = ⇑(q.projectionOnto p h.symm) := by
    funext; simp
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsCompl p q
hproj :
  Eq (α := M → ↥q)
    (Function.comp (β := M ⧸ p) (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q) (⇑p.mkQ : (a : M) → M ⧸ p))
    (⇑(q.projectionOnto p ⋯) : (a : M) → ↥q)
rw :
  IsTopCompl p q ↔
    Continuous[inst_1, instTopologicalSpaceSubtype]
      (Function.comp (β := M ⧸ p) (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q) (⇑p.mkQL : (a : M) → M ⧸ p))
rw₁ :
  IsTopCompl p q ↔
    Continuous[inst_1, instTopologicalSpaceSubtype]
      (Function.comp (β := M ⧸ p) (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q) (⇑p.mkQ : (a : M) → M ⧸ p))
rw₂ : IsTopCompl p q ↔ Continuous[inst_1, instTopologicalSpaceSubtype] (⇑(q.projectionOnto p ⋯) : (a : M) → ↥q)
rw₃ : IsTopCompl p q ↔ IsTopCompl q p
rw₄ rw₅ : IsTopCompl q p ↔ IsTopCompl q p
⊢ IsTopCompl p q ↔
    Continuous[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype]
      (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q)

Tactic:
rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto,
    isTopCompl_comm]

Premises used: Submodule.coe_mkQL, Submodule.IsCompl.isTopCompl_iff_projectionOnto, Submodule.isQuotientMap_mkQL, Topology.IsQuotientMap.continuous_iff, Submodule.isTopCompl_comm, IsCompl.symm
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsTopCompl p q
⊢ (↑(p.quotientEquivOfIsTopCompl q h) : (M ⧸ p) ≃ₗ[R] ↥q) = p.quotientEquivOfIsCompl q ⋯

Tactic:
rfl

Premises used: LinearEquiv.ofLinear, Submodule.quotientEquivOfIsCompl, rfl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsTopCompl p q
x : M ⧸ p
⊢ Eq (α := ↥q) ((p.quotientEquivOfIsTopCompl q h : (a : M ⧸ p) → ↥q) x : ↥q)
    ((p.quotientEquivOfIsCompl q ⋯ : (a : M ⧸ p) → ↥q) x : ↥q)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsTopCompl p q
y : ↥q
⊢ Eq (α := M ⧸ p) (((p.quotientEquivOfIsTopCompl q h).symm : (a : ↥q) → M ⧸ p) y : M ⧸ p)
    ((p.mkQ : (a : M) → M ⧸ p) (↑y : M) : M ⧸ p)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- Module: Mathlib.Topology.Algebra.Module.Complement
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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsTopCompl p q
x : M
⊢ Eq (α := ↥q) ((p.quotientEquivOfIsTopCompl q h : (a : M ⧸ p) → ↥q) (Quotient.mk x) : ↥q)
    ((q.projectionOnto p ⋯ : (a : M) → ↥q) x : ↥q)

Tactic:
quotientEquivOfIsCompl_apply_mk h.isCompl x

Premises used: Submodule.quotientEquivOfIsCompl_apply_mk, Submodule.IsTopCompl.isCompl
-- 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
h₁ :
  ∀ (x : E),
    Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h φ ψ : (a : E) → F) x : F)
      ((φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯ : (a : E) → F) x : F)
⊢ ofIsTopCompl h φ ψ = φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯

Tactic:
ext
-- 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)
    ((φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯ : (a : E) → F) x : F)

Tactic:
simp [ofIsTopCompl]

Premises used: ContinuousLinearMap.ofIsTopCompl
-- 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) = LinearMap.ofIsCompl ⋯ (↑φ : ↥p →ₗ[R] F) (↑ψ : ↥q →ₗ[R] F)

Tactic:
rfl

Premises used: LinearMap.ofIsCompl, rfl
-- 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)
    ((LinearMap.ofIsCompl ⋯ (↑φ : ↥p →ₗ[R] F) (↑ψ : ↥q →ₗ[R] F) : (a : E) → F) x : F)

Tactic:
rfl

Premises used: rfl
-- 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 : ↥p
⊢ Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h φ ψ : (a : E) → F) (↑x : E) : F) ((φ : (a : ↥p) → 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
x : ↥q
⊢ Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h φ ψ : (a : E) → F) (↑x : E) : F) ((ψ : (a : ↥q) → 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
χ : E →L[R] F
hφ : ∀ (u : ↥p), Eq.{u_3 + 1} (α := F) ((φ : (a : ↥p) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
hψ : ∀ (u : ↥q), Eq.{u_3 + 1} (α := F) ((ψ : (a : ↥q) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h φ ψ : (a : E) → F) x : F) ((χ : (a : E) → F) x : F)
⊢ ofIsTopCompl h φ ψ = χ

Tactic:
ext
-- 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
χ : E →L[R] F
hφ : ∀ (u : ↥p), Eq.{u_3 + 1} (α := F) ((φ : (a : ↥p) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
hψ : ∀ (u : ↥q), Eq.{u_3 + 1} (α := F) ((ψ : (a : ↥q) → F) u : F) ((χ : (a : E) → F) (↑u : E) : F)
x : E
⊢ Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h φ ψ : (a : E) → F) x : F) ((χ : (a : E) → F) x : F)

Tactic:
simp [LinearMap.ofIsCompl_eq h.isCompl hφ, hψ]

Premises used: Submodule.IsTopCompl.isCompl, LinearMap.ofIsCompl_eq
-- 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
h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h 0 0 : (a : E) → F) x : F) ((0 : (a : E) → F) x : F)
⊢ Eq (α := E →L[R] F) (ofIsTopCompl h 0 0) 0

Tactic:
ext
-- 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
x : E
⊢ Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h 0 0 : (a : E) → F) x : F) ((0 : (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
h₁ :
  ∀ (x : E),
    Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) : (a : E) → F) x : F)
      ((ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂ : (a : E) → F) x : F)
⊢ ofIsTopCompl h (φ₁ + φ₂) (ψ₁ + ψ₂) = ofIsTopCompl h φ₁ ψ₁ + ofIsTopCompl h φ₂ ψ₂

Tactic:
ext