awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.ClosedSubmodule (goal)
Goal:
ι : Sort u_1
R : Type u_2
M : Type u_3
N : Type u_4
O : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : TopologicalSpace M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : TopologicalSpace N
inst_6 : Module R N
inst_7 : AddCommMonoid O
inst_8 : TopologicalSpace O
inst_9 : Module R O
𝕜 : Type u_6
H : Type u_7
inst_10 : Semiring 𝕜
inst_11 : AddCommMonoid H
inst_12 : UniformSpace H
inst_13 : Module 𝕜 H
inst_14 : CompleteSpace H
K : ClosedSubmodule 𝕜 H
⊢ CompleteSpace.{u_7} ↥K
have a : IsComplete (↑K : Set H)
Tactic: apply IsComplete.completeSpace_coe
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Compact (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
hN : N.FG
⊢ IsCompact (↑N : Set M)
have obtain : ∀ (s : Finset M) (hs : span R (↑s : Set M) = N), IsCompact (↑N : Set M)
Tactic: obtain ⟨s, hs⟩ := hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Compact (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
⊢ IsCompact (↑N : Set M)
have this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
Tactic: have : LinearMap.range (Fintype.linearCombination R (α := s) Subtype.val) = N := by
    simp [hs]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Compact (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
⊢ IsCompact (↑N : Set M)
have rw : IsCompact
  (↑(LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) : Set M)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Compact (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
⊢ IsCompact
    (↑(LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) : Set M)
have refine : Continuous (X := ↥s → R) (Y := M)
  (⇑(Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s → R) → M)
Tactic: refine isCompact_range ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Compact (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : TopologicalSpace R
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : TopologicalSpace M
inst_5 : ContinuousAdd M
inst_6 : ContinuousSMul R M
inst_7 : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R (↑s : Set M) = N
this : LinearMap.range (M := ↥s → R) (Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) = N
⊢ Continuous (X := ↥s → R) (Y := M)
    (⇑(Fintype.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))) : (a : ↥s → R) → M)
have simp : Continuous (Y := M) fun (f : ↥s → R) ↦ ∑ i ∈ s.attach, f i • (↑i : M)
Tactic: simp only [Fintype.linearCombination, Finset.univ_eq_attach, LinearMap.coe_mk,
    AddHom.coe_mk]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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
⊢ IsTopCompl p q ↔ Continuous[inst_1, instTopologicalSpaceSubtype] (⇑(p.projectionOnto q h) : (a : M) → ↥p)
have 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))
Tactic: rw [h.isTopCompl_iff, IsInducing.subtypeVal.continuous_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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] (⇑(q.projection p ⋯) : (a : M) → M)
have rw : Continuous[inst_1, inst_1] (⇑(LinearMap.id - p.projection q sorry) : (a : M) → M)
Tactic: rw [projection_eq_id_sub_projection h.isCompl]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (hypothesis)
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
⊢ IsTopCompl.{u_1, u_2} (R := R) (M := M) ⊥ ⊤
have this : IsIdempotentElem.{u_2} (M := M →L[R] M) 0
Tactic: have : IsIdempotentElem (0 : M →L[R] M) := .zero
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (hypothesis)
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
⊢ IsTopCompl.{u_1, u_2} (R := R) (M := M) ⊤ ⊥
have this : IsIdempotentElem (M := M →L[R] M) (ContinuousLinearMap.id R M)
Tactic: have : IsIdempotentElem (.id R M : M →L[R] M) := .one
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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₂
⊢ IsIdempotentElem p
have h₁ : ∀ (x : N), Eq (α := N) ((p * p : (a : N) → N) x : N) ((p : (a : N) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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
⊢ (q.projectionL p ⋯ : (a : M) → M) x = HSub.hSub (β := M) x ((p.projectionL q h : (a : M) → M) x : M)
have rw : HAdd.hAdd (α := M) (β := M) ((q.projectionL p sorry : (a : M) → M) x : M) ((p.projectionL q h : (a : M) → M) x : M) = x
Tactic: rw [eq_sub_iff_add_eq, projectionL_add_projectionL_eq_self]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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
⊢ (q.projectionL p ⋯ : (a : M) → M) x = HSub.hSub (β := M) x ((p.projectionL q h : (a : M) → M) x : M)
have rw₁ : x = x
Tactic: rw [eq_sub_iff_add_eq, projectionL_add_projectionL_eq_self]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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] (↑q : Set M)
have rw : IsClosed[inst_1] (↑(↑(p.projectionOntoL q h) : M →ₗ[R] ↥p).ker : Set M)
Tactic: rw [← ker_projectionOntoL h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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}
have rw : IsClosed[inst_1] (Set.preimage (β := ↥p) (⇑(p.projectionOntoL q h) : (a : M) → ↥p) {0})
Tactic: rw [← (isQuotientMap_projectionOntoL h).isClosed_preimage]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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[inst_1] (Set.preimage (β := ↥p) (⇑(p.projectionOntoL q h) : (a : M) → ↥p) {0})
have 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})
Tactic: rwa [← ker_projectionOntoL h] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (hypothesis)
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)
⊢ T3Space.{u_2} ↥p
have this : IsClosed[instTopologicalSpaceSubtype] {0}
Tactic: have : IsClosed ({0} : Set p) := by
    rw [← (isQuotientMap_projectionOntoL h).isClosed_preimage]
    rwa [← ker_projectionOntoL h] at hq
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (hypothesis)
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}
⊢ T3Space.{u_2} ↥p
have this₁ : T1Space.{u_2} ↥p
Tactic: have : T1Space p := IsTopologicalAddGroup.t1Space _ this
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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
⊢ T3Space.{u_2} ↥p
have rw : T0Space.{u_2} ↥p
Tactic: rw [RegularSpace.t3Space_iff_t0Space]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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 (α := ↥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)
have fst : (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).1 :
    M) =
  (↑(x, 0).1 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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)
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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 (α := ↥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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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)
⊢ 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)
have snd : (↑((ContinuousLinearEquiv.equivOfRightInverse f p.subtypeL hf : (a : M) → ↥p × ↥(↑f : M →ₗ[R] ↥p).ker) (↑x : M)).2 :
    M) =
  (↑(0, x).2 : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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 ↔ IsHomeomorph (X := ↥p × ↥q) (Y := M) (⇑(p.prodEquivOfIsCompl q h) : (a : ↥p × ↥q) → M)
have rw : Continuous[instTopologicalSpaceProd, inst_1] (⇑(p.prodEquivOfIsCompl q h) : (a : ↥p × ↥q) → M)
Tactic: rw [(p.prodEquivOfIsCompl q h).isHomeomorph_iff,
    isTopCompl_iff_continuous_symm_prodEquivOfIsCompl, and_iff_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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)
have 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 sorry : (a : M) → ↥q) x : ↥q)
Tactic: funext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (hypothesis)
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[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype]
      (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q)
have 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 sorry) : (a : M) → ↥q)
Tactic: have hproj : ⇑(p.quotientEquivOfIsCompl q h) ∘ ⇑p.mkQ = ⇑(q.projectionOnto p h.symm) := by
    funext; simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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)
⊢ IsTopCompl p q ↔
    Continuous[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype]
      (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q)
have 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))
Tactic: rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto,
    isTopCompl_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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))
⊢ IsTopCompl p q ↔
    Continuous[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype]
      (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q)
have 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))
Tactic: rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto,
    isTopCompl_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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))
⊢ IsTopCompl p q ↔
    Continuous[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype]
      (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q)
have rw₂ : IsTopCompl p q ↔ Continuous[inst_1, instTopologicalSpaceSubtype] (⇑(q.projectionOnto p sorry) : (a : M) → ↥q)
Tactic: rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto,
    isTopCompl_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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)
⊢ IsTopCompl p q ↔
    Continuous[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype]
      (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q)
have rw₃ : IsTopCompl p q ↔ IsTopCompl q p
Tactic: rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto,
    isTopCompl_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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
⊢ IsTopCompl p q ↔
    Continuous[QuotientModule.Quotient.topologicalSpace p, instTopologicalSpaceSubtype]
      (⇑(p.quotientEquivOfIsCompl q h) : (a : M ⧸ p) → ↥q)
have rw₄ : IsTopCompl q p ↔ IsTopCompl q p
Tactic: rw [p.isQuotientMap_mkQL.continuous_iff, coe_mkQL, hproj, ← h.symm.isTopCompl_iff_projectionOnto,
    isTopCompl_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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 φ ψ = φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p ⋯
have h₁ : ∀ (x : E),
  Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h φ ψ : (a : E) → F) x : F)
    ((φ ∘SL p.projectionOntoL q h + ψ ∘SL q.projectionOntoL p sorry : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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)
⊢ ofIsTopCompl h φ ψ = χ
have h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h φ ψ : (a : E) → F) x : F) ((χ : (a : E) → F) x : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Complement (goal)
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
⊢ Eq (α := E →L[R] F) (ofIsTopCompl h 0 0) 0
have h₁ : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((ofIsTopCompl h 0 0 : (a : E) → F) x : F) ((0 : (a : E) → F) x : F)
Tactic: ext