-- 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
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)

Tactic:
rw [mul_mul_mul_comm, 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
r : ↥R⁰
m n : R_hat R K
⊢ Algebra.algebraMap m * Algebra.algebraMap n * (Algebra.algebraMap ↑↑r * ↑↑r) =
    Algebra.algebraMap m * Algebra.algebraMap n * (↑↑r * ↑↑r)

Proof state:
case h.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
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ ∃ a_1, a_1 • ↑↑r = (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) (n • ↑(↑r * ↑b))

Tactic:
simp only [LinearMapClass.map_smul, DistribMulAction.toLinearMap_apply, smul_eq_mul]

Result:
case h.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
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ ∃ a_1, a_1 • ↑↑r = n • (a * ↑(↑r * ↑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
r : ↥R⁰
x : FiniteAdeleRing R K
hx : ∃ x_1 ∈ ↑(Submodule.span (R_hat R K) {↑↑r}), ∃ y ∈ ↑(Submodule.span (R_hat R K) {↑↑r}), x_1 * y = x
⊢ x ∈ ↑(Submodule.span (R_hat R K) {↑↑r})

Tactic:
rcases hx with ⟨a, ha, b, hb, rfl⟩

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 : 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})

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 : ∃ a, a • ↑(↑r * ↑b) = m
⊢ ∃ a_1, a_1 • ↑↑r = (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) m

Tactic:
rcases hm with ⟨n, rfl⟩

Result:
case h.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
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ ∃ a_1, a_1 • ↑↑r = (DistribMulAction.toLinearMap (R_hat R K) (FiniteAdeleRing R K) a) (n • ↑(↑r * ↑b))

Proof state:
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

Tactic:
use m * n * (r : R)

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
⊢ (m * n * ↑↑r) • ↑↑r = m • ↑↑r * n • ↑↑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⁰
⊢ ↑↑j • ↑↑i = ↑↑i * ↑↑j

Tactic:
rw [mul_comm]

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⁰
⊢ ↑↑j • ↑↑i = ↑↑j * ↑↑i

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
⊢ Algebra.algebraMap m * Algebra.algebraMap n * (Algebra.algebraMap ↑↑r * ↑↑r) =
    Algebra.algebraMap m * Algebra.algebraMap n * (↑↑r * ↑↑r)

Tactic:
rfl

Result:
no goals

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⁰
⊢ ↑↑j • ↑↑i = ↑↑j * ↑↑i

Tactic:
rfl

Result:
no goals

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
r : ↥R⁰
x : FiniteAdeleRing R K
hx : x ∈ ↑(Submodule.span (R_hat R K) {↑↑r}) * ↑(Submodule.span (R_hat R K) {↑↑r})
⊢ x ∈ ↑(Submodule.span (R_hat R K) {↑↑r})

Tactic:
rw [mem_mul] at hx

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
r : ↥R⁰
x : FiniteAdeleRing R K
hx : ∃ x_1 ∈ ↑(Submodule.span (R_hat R K) {↑↑r}), ∃ y ∈ ↑(Submodule.span (R_hat R K) {↑↑r}), x_1 * y = x
⊢ x ∈ ↑(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
r : ↥R⁰
⊢ ↑(Submodule.span (R_hat R K) {↑↑r}) * ↑(Submodule.span (R_hat R K) {↑↑r}) ⊆ ↑(Submodule.span (R_hat R K) {↑↑r})

Tactic:
intro x hx

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
r : ↥R⁰
x : FiniteAdeleRing R K
hx : x ∈ ↑(Submodule.span (R_hat R K) {↑↑r}) * ↑(Submodule.span (R_hat R K) {↑↑r})
⊢ x ∈ ↑(Submodule.span (R_hat R K) {↑↑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 b : FiniteAdeleRing R K
ha : ∃ a_1, a_1 • ↑↑r = a
hb : ∃ a, a • ↑↑r = b
⊢ ∃ a_1, a_1 • ↑↑r = a * b

Tactic:
rcases ha with ⟨m, rfl⟩

Result:
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

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
a : FiniteAdeleRing R K
r : ↥R⁰
⊢ ∃ j, a • Submodule.span (R_hat R K) {↑↑j} ≤ Submodule.span (R_hat R K) {↑↑r}

Tactic:
rcases mul_nonZeroDivisor_mem_finiteIntegralAdeles a with ⟨b, c, h⟩

Result:
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}

Proof state:
case h.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
a : FiniteAdeleRing R K
r b : ↥R⁰
c : R_hat R K
h : a * ↑↑b = ↑c
n : R_hat R K
⊢ ∃ a_1, a_1 • ↑↑r = n • (a * ↑(↑r * ↑b))

Tactic:
use n * c

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))