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 q : Submodule R M
h : IsCompl p q
rw :
  Continuous[inst_1, inst_1] (⇑(p.projection q h) : (a : M) → M) ↔
    Continuous[inst_1, inst_1]
      (Function.comp (β := { x : M // x ∈ (↑p : Set M) }) (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M)))
        (⇑(p.projectionOnto q h) : (a : M) → ↥p))
⊢ IsTopCompl p q ↔ Continuous[inst_1, instTopologicalSpaceSubtype] (⇑(p.projectionOnto q h) : (a : M) → ↥p)

Tactic:
rw [h.isTopCompl_iff, IsInducing.subtypeVal.continuous_iff]

Premises used: Topology.IsInducing.continuous_iff, Submodule.IsCompl.isTopCompl_iff, Topology.IsInducing.subtypeVal
-- 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
h : IsCompl p q
⊢ Continuous[inst_1, inst_1] (⇑(p.projection q h) : (a : M) → M) ↔
    Continuous[inst_1, inst_1]
      (Function.comp (β := { x : M // x ∈ (↑p : Set M) }) (Subtype.val (p := fun (x : M) ↦ x ∈ (↑p : Set M)))
        (⇑(p.projectionOnto q h) : (a : M) → ↥p))

Tactic:
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
h : IsTopCompl p q
⊢ Continuous[inst_1, instTopologicalSpaceSubtype] (⇑(p.projectionOnto q ⋯) : (a : M) → ↥p)

Tactic:
h.isCompl.isTopCompl_iff_projectionOnto.mp h

Premises used: Submodule.IsCompl.isTopCompl_iff_projectionOnto, Submodule.IsTopCompl.isCompl, Iff.mp
-- 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 : ContinuousSub M
h : IsTopCompl p q
rw : Continuous[inst_1, inst_1] (⇑(LinearMap.id - p.projection q ⋯) : (a : M) → M)
⊢ Continuous[inst_1, inst_1] (⇑(q.projection p ⋯) : (a : M) → M)

Tactic:
rw [projection_eq_id_sub_projection h.isCompl]

Premises used: Submodule.projection_eq_id_sub_projection, 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 : ContinuousSub M
h : IsTopCompl p q
⊢ Continuous[inst_1, inst_1] (⇑(LinearMap.id - p.projection q ⋯) : (a : M) → M)

Tactic:
continuous_id.sub h.continuous_projection

Premises used: Submodule.IsTopCompl.continuous_projection, continuous_id, Continuous.sub
-- 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 : ContinuousSub M
h : IsTopCompl p q
⊢ Continuous[inst_1, inst_1] (⇑(LinearMap.id - p.projection q ⋯) : (a : M) → M)

Tactic:
exact continuous_id.sub h.continuous_projection

Premises used: Submodule.IsTopCompl.continuous_projection, continuous_id, Continuous.sub
-- 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 : ContinuousSub M
⊢ IsTopCompl p q ↔ IsTopCompl q p

Tactic:
⟨IsTopCompl.symm, IsTopCompl.symm⟩

Premises used: Submodule.IsTopCompl.symm, Iff.intro
-- 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
⊢ IsIdempotentElem.{u_2} (M := M →L[R] M) 0

Tactic:
have : IsIdempotentElem (0 : M →L[R] M) := .zero
-- 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
this : IsIdempotentElem.{u_2} (M := M →L[R] M) 0
⊢ IsTopCompl.{u_1, u_2} (R := R) (M := M) ⊥ ⊤

Tactic:
simpa using this.isTopCompl

Premises used: ContinuousLinearMap.IsIdempotentElem.isTopCompl
-- 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
⊢ IsIdempotentElem (M := M →L[R] M) (ContinuousLinearMap.id R M)

Tactic:
have : IsIdempotentElem (.id R M : M →L[R] M) := .one
-- 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
this : IsIdempotentElem (M := M →L[R] M) (ContinuousLinearMap.id R M)
⊢ IsTopCompl.{u_1, u_2} (R := R) (M := M) ⊤ ⊥

Tactic:
simpa using this.isTopCompl

Premises used: ContinuousLinearMap.IsIdempotentElem.isTopCompl
-- 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)
p : N →L[R] N := f₁ ∘SL f₂
h₁ : ∀ (x : N), Eq (α := N) ((p * p : (a : N) → N) x : N) ((p : (a : N) → N) x : N)
⊢ IsIdempotentElem p

Tactic:
ext x
-- 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)
p : N →L[R] N := f₁ ∘SL f₂
x : N
⊢ Eq (α := N) ((p * p : (a : N) → N) x : N) ((p : (a : N) → N) x : N)

Tactic:
simp [p, h (f₂ x)]

Premises used: DFunLike.coe
-- 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
f : M →L[R] ↥p
hf : ∀ (x : ↥p), (f : (a : M) → ↥p) (↑x : M) = x
⊢ IsTopCompl p (↑f : M →ₗ[R] ↥p).ker

Tactic:
simpa using p.subtypeL.isTopCompl_range_ker_of_leftInverse f hf

Premises used: Submodule.subtypeL, ContinuousLinearMap.isTopCompl_range_ker_of_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
p q : Submodule R M
h : IsTopCompl p q
⊢ (↑(p.projectionOntoL q h) : M →ₗ[R] ↥p) = p.projectionOnto q ⋯

Tactic:
rfl

Premises used: Submodule.projectionOnto, 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
h : IsTopCompl p q
x : ↥p
⊢ (p.projectionOntoL q h : (a : M) → ↥p) (↑x : M) = x

Tactic:
projectionOnto_apply_left h.isCompl x

Premises used: Submodule.IsTopCompl.isCompl, Submodule.projectionOnto_apply_left
-- 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
h : IsTopCompl p q
⊢ (↑(p.projectionOntoL q h) : M →ₗ[R] ↥p).range = ⊤

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
h : IsTopCompl p q
⊢ Surjective (α := M) (β := ↥p) (⇑(p.projectionOntoL q h) : (a : M) → ↥p)

Tactic:
projectionOnto_surjective h.isCompl

Premises used: Submodule.IsTopCompl.isCompl, Submodule.projectionOnto_surjective
-- 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
h : IsTopCompl p q
x : M
⊢ Eq (α := ↥p) ((p.projectionOntoL q h : (a : M) → ↥p) x : ↥p) (0 : ↥p) ↔ x ∈ q

Tactic:
projectionOnto_apply_eq_zero_iff h.isCompl

Premises used: Submodule.projectionOnto_apply_eq_zero_iff, 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
h : IsTopCompl p q
x : ↥q
⊢ Eq (α := ↥p) ((p.projectionOntoL q h : (a : M) → ↥p) (↑x : M) : ↥p) (0 : ↥p)

Tactic:
projectionOntoL_apply_eq_zero_of_mem_right h x.2

Premises used: Submodule.projectionOntoL_apply_eq_zero_of_mem_right, Subtype.property
-- 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
h : IsTopCompl p q
⊢ (↑(p.projectionOntoL q h) : M →ₗ[R] ↥p).ker = 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
h : IsTopCompl p q
⊢ IsQuotientMap (X := M) (Y := ↥p) (⇑(p.projectionOntoL q h) : (a : M) → ↥p)

Tactic:
.of_inverse continuous_subtype_val (p.projectionOntoL q h).continuous
    (projectionOntoL_apply_left h)

Premises used: continuous_subtype_val, Submodule.projectionOntoL_apply_left, ContinuousLinearMap.continuous, Submodule.projectionOntoL, Topology.IsQuotientMap.of_inverse
-- 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
h : IsTopCompl p q
⊢ (↑(p.projectionL q h) : M →ₗ[R] M) = p.projection q ⋯

Tactic:
rfl

Premises used: Submodule.projection, 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
h : IsTopCompl p q
x : M
⊢ Eq (α := M) ((p.projectionL q h : (a : M) → M) x : M) ((↑((p.projectionOntoL q h : (a : M) → ↥p) x) : M) : 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
h : IsTopCompl p q
x : M
⊢ Eq (α := M) ((↑((p.projectionOntoL q h : (a : M) → ↥p) x) : M) : M) ((p.projectionL q h : (a : M) → M) x : 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
h : IsTopCompl p q
x : M
⊢ Membership.mem (α := M) p ((p.projectionL q h : (a : M) → M) x : M)

Tactic:
SetLike.coe_mem _

Premises used: SetLike.coe_mem, Set.Mem
-- 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
h : IsTopCompl p q
x : ↥p
⊢ (p.projectionL q h : (a : M) → M) (↑x : M) = (↑x : M)

Tactic:
projection_apply_left h.isCompl x

Premises used: Submodule.projection_apply_left, 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
h : IsTopCompl p q
⊢ (↑(p.projectionL q h) : M →ₗ[R] M).range = p

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
h : IsTopCompl p q
x : M
⊢ Eq (α := M) ((p.projectionL q h : (a : M) → M) x : M) (0 : M) ↔ x ∈ q

Tactic:
projection_apply_eq_zero_iff h.isCompl

Premises used: Submodule.IsTopCompl.isCompl, Submodule.projection_apply_eq_zero_iff
-- 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
h : IsTopCompl p q
x : ↥q
⊢ Eq (α := M) ((p.projectionL q h : (a : M) → M) (↑x : M) : M) (0 : M)

Tactic:
projectionL_apply_eq_zero_of_mem_right h x.2

Premises used: Submodule.projectionL_apply_eq_zero_of_mem_right, Subtype.property
-- 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
h : IsTopCompl p q
⊢ (↑(p.projectionL q h) : M →ₗ[R] M).ker = 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
h : IsTopCompl p q
⊢ IsIdempotentElem (p.projectionL q h)

Tactic:
simp [← isIdempotentElem_toLinearMap_iff]

Premises used: ContinuousLinearMap.isIdempotentElem_toLinearMap_iff
-- 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 : ContinuousSub M
h : IsTopCompl p q
x : M
⊢ HAdd.hAdd (α := M) (β := M) ((p.projectionL q h : (a : M) → M) x : M) ((q.projectionL p ⋯ : (a : M) → M) x : M) = x

Tactic:
projection_add_projection_eq_self h.isCompl x

Premises used: Submodule.IsTopCompl.isCompl, Submodule.projection_add_projection_eq_self
-- 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.projectionL q h + q.projectionL p ⋯ = ContinuousLinearMap.id R M

Tactic:
ContinuousLinearMap.ext <| projectionL_add_projectionL_eq_self h

Premises used: Submodule.projectionL_add_projectionL_eq_self, ContinuousLinearMap.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
p q : Submodule R M
inst_4 : ContinuousSub M
h : IsTopCompl p q
x : M
rw : HAdd.hAdd (α := M) (β := M) ((q.projectionL p ⋯ : (a : M) → M) x : M) ((p.projectionL q h : (a : M) → M) x : M) = x
rw₁ rw₂ : x = x
⊢ (q.projectionL p ⋯ : (a : M) → M) x = HSub.hSub (β := M) x ((p.projectionL q h : (a : M) → M) x : M)

Tactic:
rw [eq_sub_iff_add_eq, projectionL_add_projectionL_eq_self]

Premises used: eq_sub_iff_add_eq, Submodule.projectionL_add_projectionL_eq_self
-- 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
⊢ q.projectionL p ⋯ = ContinuousLinearMap.id R M - p.projectionL q h

Tactic:
ContinuousLinearMap.ext <| projectionL_eq_self_sub_projectionL h

Premises used: Submodule.projectionL_eq_self_sub_projectionL, ContinuousLinearMap.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
p q : Submodule R M
inst_4 : ContinuousSub M
h : IsTopCompl p q
x : M
⊢ (p.projectionL q h : (a : M) → M) x = x ↔ x ∈ p

Tactic:
projection_eq_self_iff h.isCompl x

Premises used: Submodule.IsTopCompl.isCompl, Submodule.projection_eq_self_iff
-- 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
f : M →L[R] M
hf : IsIdempotentElem f
⊢ f = (↑f : M →ₗ[R] M).range.projectionL (↑f : M →ₗ[R] M).ker ⋯

Tactic:
coe_inj.mp <| LinearMap.IsIdempotentElem.eq_projection hf.toLinearMap

Premises used: ContinuousLinearMap.coe_inj, ContinuousLinearMap.IsIdempotentElem.toLinearMap, LinearMap.IsIdempotentElem.eq_projection, Iff.mp
-- 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
f : M →L[R] M
⊢ IsIdempotentElem f ↔
    ∃ (h : IsTopCompl (↑f : M →ₗ[R] M).range (↑f : M →ₗ[R] M).ker),
      f = (↑f : M →ₗ[R] M).range.projectionL (↑f : M →ₗ[R] M).ker h

Tactic:
⟨fun h ↦ ⟨_, h.eq_projectionL⟩, fun ⟨hf, h⟩ ↦ h.symm ▸ isIdempotentElem_projectionL hf⟩

Premises used: Eq.rec, ContinuousLinearMap.IsIdempotentElem.eq_projectionL, ContinuousLinearMap.IsIdempotentElem.isTopCompl, IsIdempotentElem, _private.0.ContinuousLinearMap.isIdempotentElem_iff_eq_projectionL_range_ker.match_1, Iff.intro, Exists.intro, Eq.symm, Submodule.isIdempotentElem_projectionL
-- 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
h : IsTopCompl p q
⊢ p.ClosedComplemented

Tactic:
⟨p.projectionOntoL q h, projectionOntoL_apply_left h⟩

Premises used: Submodule.projectionOntoL_apply_left, Submodule.ClosedComplemented, Submodule.projectionOntoL, Exists.intro
-- 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 : T1Space.{u_2} ↥p
h : IsTopCompl p q
rw : IsClosed[inst_1] (↑(↑(p.projectionOntoL q h) : M →ₗ[R] ↥p).ker : Set M)
⊢ IsClosed[inst_1] (↑q : Set M)

Tactic:
rw [← ker_projectionOntoL h]

Premises used: Submodule.ker_projectionOntoL
-- 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 : T1Space.{u_2} ↥p
h : IsTopCompl p q
⊢ IsClosed[inst_1] (↑(↑(p.projectionOntoL q h) : M →ₗ[R] ↥p).ker : Set M)

Tactic:
isClosed_ker _

Premises used: ContinuousLinearMap.isClosed_ker
-- 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 : T1Space.{u_2} ↥p
h : IsTopCompl p q
⊢ IsClosed[inst_1] (↑(↑(p.projectionOntoL q h) : M →ₗ[R] ↥p).ker : Set M)

Tactic:
exact isClosed_ker _

Premises used: ContinuousLinearMap.isClosed_ker
-- 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 : T1Space.{u_2} ↥q
inst_5 : ContinuousSub M
h : IsTopCompl p q
⊢ IsClosed[inst_1] (↑p : Set M)

Tactic:
h.symm.isClosed'

Premises used: Submodule.IsTopCompl.symm, 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
p q : Submodule R M
inst_4 : IsTopologicalAddGroup M
h : IsTopCompl p q
hq : IsClosed[inst_1] (↑q : Set M)
rw : IsClosed[inst_1] (Set.preimage (β := ↥p) (⇑(p.projectionOntoL q h) : (a : M) → ↥p) {0})
⊢ IsClosed[instTopologicalSpaceSubtype] {0}

Tactic:
rw [← (isQuotientMap_projectionOntoL h).isClosed_preimage]

Premises used: Topology.IsCoinducing.isClosed_preimage, Topology.IsQuotientMap.isCoinducing, Submodule.isQuotientMap_projectionOntoL
-- 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
hq : IsClosed[inst_1] (↑q : Set M)
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hq : IsClosed[inst_1] (↑(↑(p.projectionOntoL q h) : M →ₗ[R] ↥p).ker : Set M)),
    IsClosed[inst_1] (Set.preimage (β := ↥p) (⇑(p.projectionOntoL q h) : (a : M) → ↥p) {0})
⊢ IsClosed[inst_1] (Set.preimage (β := ↥p) (⇑(p.projectionOntoL q h) : (a : M) → ↥p) {0})

Tactic:
rwa [← ker_projectionOntoL h] at hq

Premises used: Submodule.ker_projectionOntoL
-- 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
hq : IsClosed[inst_1] (↑q : Set M)
⊢ IsClosed[instTopologicalSpaceSubtype] {0}

Tactic:
have : IsClosed ({0} : Set p) := by
    rw [← (isQuotientMap_projectionOntoL h).isClosed_preimage]
    rwa [← ker_projectionOntoL h] at hq
-- 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
hq : IsClosed[inst_1] (↑q : Set M)
this : IsClosed[instTopologicalSpaceSubtype] {0}
⊢ T1Space.{u_2} ↥p

Tactic:
have : T1Space p := IsTopologicalAddGroup.t1Space _ this
-- 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
hq : IsClosed[inst_1] (↑q : Set M)
this_1 : IsClosed[instTopologicalSpaceSubtype] {0}
this : T1Space.{u_2} ↥p
rw : T0Space.{u_2} ↥p
⊢ T3Space.{u_2} ↥p

Tactic:
rw [RegularSpace.t3Space_iff_t0Space]

Premises used: RegularSpace.t3Space_iff_t0Space
-- 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
hq : IsClosed[inst_1] (↑q : Set M)
this_1 : IsClosed[instTopologicalSpaceSubtype] {0}
this : T1Space.{u_2} ↥p
⊢ T0Space.{u_2} ↥p

Tactic:
infer_instance
-- 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
hq : IsClosed[inst_1] (↑q : Set M)
⊢ T2Space.{u_2} ↥p

Tactic:
have := h.t3Space hq
  inferInstance

Premises used: Submodule.IsTopCompl.t3Space, inferInstance
-- 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
⊢ ∃ (q : Submodule R M), IsTopCompl p q

Tactic:
Exists.elim h fun f hf => ⟨_, f.isTopCompl_of_proj hf⟩

Premises used: LinearMap.ker, ContinuousLinearMap.toLinearMap, Exists.intro, ContinuousLinearMap.isTopCompl_of_proj, Exists.elim
-- 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
⊢ p.ClosedComplemented ↔ ∃ (q : Submodule R M), IsTopCompl p q

Tactic:
⟨ClosedComplemented.exists_isTopCompl, fun H ↦ H.elim fun _ hq ↦ hq.closedComplemented⟩

Premises used: Iff.intro, Submodule.IsTopCompl.closedComplemented, Submodule.ClosedComplemented.exists_isTopCompl, Exists.elim
-- 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
⊢ ∃ (q : Submodule R M), IsClosed[inst_1] (↑q : Set M) ∧ IsCompl p q

Tactic:
Exists.elim h.exists_isTopCompl fun q hq => ⟨q, hq.isClosed', hq.isCompl⟩

Premises used: Submodule.IsTopCompl.isCompl, And.intro, Exists.intro, Submodule.ClosedComplemented.exists_isTopCompl, Exists.elim, 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
p : Submodule R M
h : p.ClosedComplemented
⊢ IsTopCompl p h.complement

Tactic:
Classical.choose_spec h.exists_isTopCompl

Premises used: Submodule.ClosedComplemented.complement, Classical.choose_spec, Submodule.ClosedComplemented.exists_isTopCompl