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

State before:
α✝ : Type u_1
inst✝² : Ring α✝
α : Type u_2
inst✝¹ : CommRing α
ι : Type u_3
inst✝ : Nonempty ι
B : ι → Ideal α
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
i : ι
a r : α
h : a ∈ B i
⊢ a * r ∈ B i
Tactic:
rw [mul_comm]
State after:
α✝ : Type u_1
inst✝² : Ring α✝
α : Type u_2
inst✝¹ : CommRing α
ι : Type u_3
inst✝ : Nonempty ι
B : ι → Ideal α
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
i : ι
a r : α
h : a ∈ B i
⊢ r * a ∈ B i

State before:
α✝ : Type u_1
inst✝² : Ring α✝
α : Type u_2
inst✝¹ : CommRing α
ι : Type u_3
inst✝ : Nonempty ι
B : ι → Ideal α
inter : ∀ (i j : ι), ∃ k, B k ≤ B i ⊓ B j
i : ι
a r : α
h : a ∈ B i
⊢ r * a ∈ B i
Tactic:
refine' Ideal.mul_mem_left (B i) r h
State after:
no goals