Module: Mathlib.Topology.Algebra.LinearTopology

Goal state before:
pp: R : Type u_1
R' : Type u_2
M : Type u_3
inst✝⁸ : Ring R
inst✝⁷ : Ring R'
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : Module R' M
inst✝³ : SMulCommClass R R' M
inst✝² : TopologicalSpace M
inst✝¹ : IsLinearTopology R M
inst✝ : IsLinearTopology R' M
⊢ (𝓝 0).HasBasis (fun I ↦ ↑I ∈ 𝓝 0 ∧ (∀ (r : R), ∀ x ∈ I, r • x ∈ I) ∧ ∀ (r' : R'), ∀ x ∈ I, r' • x ∈ I) fun I ↦ ↑I

Tactic:
by
  -- Start from a neighborhood `V`. It contains some open sub-`R`-module `I`.
  refine IsLinearTopology.hasBasis_submodule R |>.to_hasBasis (fun I hI ↦ ?_)
    (fun I hI ↦ ⟨{I with smul_mem' := fun r x hx ↦ hI.2.1 r x hx}, hI.1, subset_rfl⟩)
  -- `I` itself is a neighborhood of zero, so it contains some open sub-`R'`-module `J`.
  rcases (hasBasis_submodule R').mem_iff.mp hI with ⟨J, hJ, J_sub_I⟩
  set uR : Set R := univ -- Convenient to avoid type ascriptions
  set uR' : Set R' := univ
  have hRR : uR * uR ⊆ uR := subset_univ _
  have hRI : uR • (I : Set M) ⊆ I := smul_subset_iff.mpr fun x _ i hi ↦ I.smul_mem x hi
  have hR'J : uR' • (J : Set M) ⊆ J := smul_subset_iff.mpr fun x _ j hj ↦ J.smul_mem x hj
  have hRJ : uR • (J : Set M) ⊆ I := subset_trans (smul_subset_smul_left J_sub_I) hRI
  -- Note that, on top of the obvious `R • I ⊆ I` and `R' • J ⊆ J`, we have `R • J ⊆ R • I ⊆ I`.
  -- Now set `S := J ∪ (R • J)`. We have:
  -- 1. `R • S = (R • J) ∪ (R • R • J) ⊆ R • J ⊆ S`.
  -- 2. `R' • S = (R' • J) ∪ (R' • R • J) ⊆ J ∪ (R • R' • J) ⊆ J ∪ (R • J) = S`.
  -- Hence the subgroup `A` generated by `S` is a sub-`(R, R')`-bimodule,
  -- which we claim is open and contained in `I`.
  -- Indeed, we have `J ⊆ S ⊆ I`, hence `J ⊆ A ⊆ I`, and `J` is open by hypothesis.
  set S : Set M := J ∪ uR • J
  have S_sub_I : S ⊆ I := union_subset J_sub_I hRJ
  have hRS : uR • S ⊆ S := calc
    uR • S = uR • (J : Set M) ∪ (uR * uR) • (J : Set M) := by simp_rw [S, smul_union, mul_smul]
    _ ⊆ uR • (J : Set M) ∪ uR • (J : Set M) := by gcongr
    _ = uR • (J : Set M) := union_self _
    _ ⊆ S := subset_union_right
  have hR'S : uR' • S ⊆ S := calc
    uR' • S = uR' • (J : Set M) ∪ uR • uR' • (J : Set M) := by simp_rw [S, smul_union, smul_comm]
    _ ⊆ J ∪ uR • J := by gcongr
    _ = S := rfl
  set A : AddSubgroup M := .closure S
  have hRA : ∀ r : R, ∀ i ∈ A, r • i ∈ A := fun r i hi ↦ by
    refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
    case base => exact AddSubgroup.subset_closure <| hRS <| Set.smul_mem_smul trivial hx
    case zero => simp_rw [smul_zero]; exact zero_mem _
    case add => simp_rw [smul_add]; exact add_mem hx hy
    case neg => simp_rw [smul_neg]; exact neg_mem hx
  have hR'A : ∀ r' : R', ∀ i ∈ A, r' • i ∈ A := fun r' i hi ↦ by
    refine AddSubgroup.closure_induction (fun x hx => ?base) ?zero (fun x y _ _ hx hy ↦ ?add)
      (fun x _ hx ↦ ?neg) hi
    case base => exact AddSubgroup.subset_closure <| hR'S <| Set.smul_mem_smul trivial hx
    case zero => simp_rw [smul_zero]; exact zero_mem _
    case add => simp_rw [smul_add]; exact add_mem hx hy
    case neg => simp_rw [smul_neg]; exact neg_mem hx
  have A_sub_I : (A : Set M) ⊆ I := I.toAddSubgroup.closure_le.mpr S_sub_I
  have J_sub_A : (J : Set M) ⊆ A := subset_trans subset_union_left AddSubgroup.subset_closure
  exact ⟨A, ⟨mem_of_superset hJ J_sub_A, hRA, hR'A⟩, A_sub_I⟩

Goal state after: