Theorem: Ideal.IsBasis.toRingSubgroupsBasis (DividedPowers/ForMathlib/Topology/LinearTopology.lean)

State before:
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
i : ι
u : α
⊢ u ∈ ↑(Submodule.toAddSubgroup (B i)) * ↑(Submodule.toAddSubgroup (B i)) → u ∈ ↑(Submodule.toAddSubgroup (B i))
Tactic:
rintro ⟨x, _, _, hy, rfl⟩
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
i : ι
x : α
left✝ : x ∈ ↑(Submodule.toAddSubgroup (B i))
w✝ : α
hy : w✝ ∈ ↑(Submodule.toAddSubgroup (B i))
⊢ (fun x x_1 => x * x_1) x w✝ ∈ ↑(Submodule.toAddSubgroup (B i))

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝ : Ring α
ι : Type u_2
B : ι → Ideal α
hB : IsBasis B
i : ι
x : α
left✝ : x ∈ ↑(Submodule.toAddSubgroup (B i))
w✝ : α
hy : w✝ ∈ ↑(Submodule.toAddSubgroup (B i))
⊢ (fun x x_1 => x * x_1) x w✝ ∈ ↑(Submodule.toAddSubgroup (B i))
Tactic:
exact Ideal.mul_mem_left _ _ hy
State after:
no goals