R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
⊢ FG ↑I
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
⊢ FG ↑I
have : (1 : A) ∈ (I * ↑I⁻¹ : Submodule R A) := by
  rw [I.mul_inv]
  exact one_le.mp le_rfl
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ FG ↑I
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
⊢ FG ↑I
obtain ⟨T, T', hT, hT', one_mem⟩ := mem_span_mul_finite_of_mem_mul this
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑I ≤ span R ↑T
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ FG ↑I
refine' ⟨T, span_eq_of_le _ hT _⟩
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑(1 * I) ≤ span R ↑T * 1
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑I ≤ span R ↑T
rw [← one_mul I, ← mul_one (span R (T : Set A))]
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑(1 * I) ≤ span R ↑T * ↑I⁻¹ * ↑I
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑(1 * I) ≤ span R ↑T * 1
conv_rhs => rw [← I.inv_mul, ← mul_assoc]
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑1 ≤ span R ↑T * span R ↑T'
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑(1 * I) ≤ span R ↑T * ↑I⁻¹ * ↑I
refine' mul_le_mul_left (le_trans _ <| mul_le_mul_right <| span_le.mpr hT')
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ 1 ≤ span R (↑T * ↑T')
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ ↑1 ≤ span R ↑T * span R ↑T'
simp only [Units.val_one, span_mul_span]
no goals
case intro.intro.intro.intro
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
this : 1 ∈ ↑I * ↑I⁻¹
T T' : Finset A
hT : ↑T ⊆ ↑↑I
hT' : ↑T' ⊆ ↑↑I⁻¹
one_mem : 1 ∈ span R (↑T * ↑T')
⊢ 1 ≤ span R (↑T * ↑T')
rwa [one_le]
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
⊢ 1 ∈ 1
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
⊢ 1 ∈ ↑I * ↑I⁻¹
rw [I.mul_inv]
no goals
R✝ : Type ?u.75765
M : Type ?u.75768
inst✝⁵ : Semiring R✝
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R✝ M
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
I : (Submodule R A)ˣ
⊢ 1 ∈ 1
exact one_le.mp le_rfl