-- Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean
theorem toRing_subgroups_basis (hB : SubmodulesRingBasis B) :
    RingSubgroupsBasis fun i => (B i).toAddSubgroup

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
⊢ RingSubgroupsBasis fun i => (B i).toAddSubgroup

Tactic:
apply RingSubgroupsBasis.of_comm (fun i => (B i).toAddSubgroup) hB.inter hB.mul

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
⊢ ∀ (x : A) (i : ι), ∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => x * y) ⁻¹' ↑(B i).toAddSubgroup

Proof state:
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup

Tactic:
rintro b (b_in : b ∈ B j)

Result:
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
b : A
b_in : b ∈ B j
⊢ b ∈ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup

Proof state:
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
b : A
b_in : b ∈ B j
⊢ b ∈ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup

Tactic:
exact hj ⟨b, b_in, rfl⟩

Result:
no goals

Proof state:
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup

Tactic:
use j

Result:
case h
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i : ι
⊢ ∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup

Tactic:
rcases hB.leftMul a i with ⟨j, hj⟩

Result:
case intro
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i j : ι
hj : a • B j ≤ B i
⊢ ∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
⊢ ∀ (x : A) (i : ι), ∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => x * y) ⁻¹' ↑(B i).toAddSubgroup

Tactic:
intro a i

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
B : ι → Submodule R A
hB : SubmodulesRingBasis B
a : A
i : ι
⊢ ∃ j, ↑(B j).toAddSubgroup ⊆ (fun y => a * y) ⁻¹' ↑(B i).toAddSubgroup