-- Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
theorem submodulesRingBasis : SubmodulesRingBasis
    (fun (r : R⁰) ↦ Submodule.span (R_hat R K) {((r : R) : FiniteAdeleRing R K)}) where
  inter i j := ⟨i * j, by
    push_cast
    simp only [le_inf_iff, Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]
    exact ⟨⟨((j : R) : R_hat R K), by rw [mul_comm]; rfl⟩, ⟨((i : R) : R_hat R K), rfl⟩⟩⟩
  leftMul a r

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
⊢ a • Submodule.span (R_hat R K) {↑↑(r * b)} ≤ Submodule.span (R_hat R K) {↑↑r}

Tactic:
rintro x ⟨m, hm, rfl⟩

Result:
case h.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
m : FiniteAdeleRing R K
hm : m ∈ ↑(Submodule.span (R_hat R K) {↑↑(r * b)})
⊢ (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m ∈ Submodule.span (R_hat R K) {↑↑r}

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
r : ↥R⁰
m n : R_hat R K
⊢ (m * n * ↑↑r) • ↑↑r = m • ↑↑r * n • ↑↑r

Tactic:
simp only [Algebra.smul_def', map_mul]

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
r : ↥R⁰
m n : R_hat R K
⊢ Algebra.algebraMap m * Algebra.algebraMap n * Algebra.algebraMap ↑↑r * ↑↑r =
    Algebra.algebraMap m * ↑↑r * (Algebra.algebraMap n * ↑↑r)

Proof state:
case intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
⊢ ∃ j, a • Submodule.span (R_hat R K) {↑↑j} ≤ Submodule.span (R_hat R K) {↑↑r}

Tactic:
use r * b

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
⊢ a • Submodule.span (R_hat R K) {↑↑(r * b)} ≤ Submodule.span (R_hat R K) {↑↑r}

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
i j : ↥R⁰
⊢ Submodule.span (R_hat R K) {↑↑i * ↑↑j} ≤ Submodule.span (R_hat R K) {↑↑i} ⊓ Submodule.span (R_hat R K) {↑↑j}

Tactic:
simp only [le_inf_iff, Submodule.span_singleton_le_iff_mem, Submodule.mem_span_singleton]

Result:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
i j : ↥R⁰
⊢ (∃ a, a • ↑↑i = ↑↑i * ↑↑j) ∧ ∃ a, a • ↑↑j = ↑↑i * ↑↑j

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ Algebra.algebraMap (n * c) * ↑↑r = Algebra.algebraMap n * ↑c * ↑↑r

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ (n * c) • ↑↑r = n • (a * (↑↑r * ↑↑b))

Tactic:
rw [mul_left_comm, h, mul_comm _ (c : FiniteAdeleRing R K),
  Algebra.smul_def', Algebra.smul_def', ← mul_assoc]

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ Algebra.algebraMap (n * c) * ↑↑r = Algebra.algebraMap n * ↑c * ↑↑r

Proof state:
case intro.intro.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
r : ↥R⁰
a : FiniteAdeleRing R K
ha : a ∈ ↑(Submodule.span (R_hat R K) {↑↑r})
b : FiniteAdeleRing R K
hb : b ∈ ↑(Submodule.span (R_hat R K) {↑↑r})
⊢ a * b ∈ ↑(Submodule.span (R_hat R K) {↑↑r})

Tactic:
simp only [SetLike.mem_coe, Submodule.mem_span_singleton] at ha hb ⊢

Result:
case intro.intro.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
r : ↥R⁰
a b : FiniteAdeleRing R K
ha : ∃ a_1, a_1 • ↑↑r = a
hb : ∃ a, a • ↑↑r = b
⊢ ∃ a_1, a_1 • ↑↑r = a * b

Proof state:
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
i j : ↥R⁰
⊢ (∃ a, a • ↑↑i = ↑↑i * ↑↑j) ∧ ∃ a, a • ↑↑j = ↑↑i * ↑↑j

Tactic:
exact ⟨⟨((j : R) : R_hat R K), by rw [mul_comm]; rfl⟩, ⟨((i : R) : R_hat R K), rfl⟩⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
r : ↥R⁰
b : FiniteAdeleRing R K
hb : ∃ a, a • ↑↑r = b
m : R_hat R K
⊢ ∃ a, a • ↑↑r = m • ↑↑r * b

Tactic:
rcases hb with ⟨n, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
r : ↥R⁰
m n : R_hat R K
⊢ ∃ a, a • ↑↑r = m • ↑↑r * n • ↑↑r

Proof state:
case h.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
m : FiniteAdeleRing R K
hm : m ∈ Submodule.span (R_hat R K) {↑(↑r * ↑b)}
⊢ (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m ∈ Submodule.span (R_hat R K) {↑↑r}

Tactic:
rw [Submodule.mem_span_singleton] at hm ⊢

Result:
case h.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
m : FiniteAdeleRing R K
hm : ∃ a, a • ↑(↑r * ↑b) = m
⊢ ∃ a_1, a_1 • ↑↑r = (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m

Proof state:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ (n * c) • ↑↑r = n • (a * ↑(↑r * ↑b))

Tactic:
push_cast

Result:
case h
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ (n * c) • ↑↑r = n • (a * (↑↑r * ↑↑b))

Proof state:
case h.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
m : FiniteAdeleRing R K
hm : m ∈ ↑(Submodule.span (R_hat R K) {↑↑(r * b)})
⊢ (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m ∈ Submodule.span (R_hat R K) {↑↑r}

Tactic:
simp only [Submonoid.coe_mul, SetLike.mem_coe] at hm

Result:
case h.intro.intro
R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
m : FiniteAdeleRing R K
hm : m ∈ Submodule.span (R_hat R K) {↑(↑r * ↑b)}
⊢ (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m ∈ Submodule.span (R_hat R K) {↑↑r}