[GOAL]
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A
r : R
⊢ (fun r => r • 1) r = x ↔ ↑(algebraMap R A) r = x
[PROOFSTEP]
rw [algebraMap_eq_smul_one]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ 1 ≤ 1.toAddSubmonoid
[PROOFSTEP]
rintro x ⟨n, rfl⟩
[GOAL]
case intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
⊢ ↑(Nat.castAddMonoidHom A) n ∈ 1.toAddSubmonoid
[PROOFSTEP]
exact ⟨n, map_natCast (algebraMap R A) n⟩
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ 1 = span R {1}
[PROOFSTEP]
apply Submodule.ext
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ ∀ (x : A), x ∈ 1 ↔ x ∈ span R {1}
[PROOFSTEP]
intro a
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n a : A
⊢ a ∈ 1 ↔ a ∈ span R {1}
[PROOFSTEP]
simp only [mem_one, mem_span_singleton, Algebra.smul_def, mul_one]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ 1 ≤ P ↔ 1 ∈ P
[PROOFSTEP]
simp only [one_eq_span, span_le, Set.singleton_subset_iff, SetLike.mem_coe]
[GOAL]
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ map (AlgHom.toLinearMap f) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
x✝ : A'
⊢ x✝ ∈ map (AlgHom.toLinearMap f) 1 ↔ x✝ ∈ 1
[PROOFSTEP]
simp
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ map (↑(opLinearEquiv R)) 1 = 1
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
x : Aᵐᵒᵖ
⊢ x ∈ map (↑(opLinearEquiv R)) 1 ↔ x ∈ 1
[PROOFSTEP]
induction x using MulOpposite.rec'
[GOAL]
case h.h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n X✝ : A
⊢ op X✝ ∈ map (↑(opLinearEquiv R)) 1 ↔ op X✝ ∈ 1
[PROOFSTEP]
simp
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ comap (↑(opLinearEquiv R)) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n x✝ : A
⊢ x✝ ∈ comap (↑(opLinearEquiv R)) 1 ↔ x✝ ∈ 1
[PROOFSTEP]
simp
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ map (↑(LinearEquiv.symm (opLinearEquiv R))) 1 = 1
[PROOFSTEP]
rw [← comap_equiv_eq_map_symm, comap_op_one]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ comap (↑(LinearEquiv.symm (opLinearEquiv R))) 1 = 1
[PROOFSTEP]
rw [← map_equiv_eq_comap_symm, map_op_one]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R A
⊢ (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid
[PROOFSTEP]
dsimp [HMul.hMul, Mul.mul]
  --porting note: added `hMul`
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R A
⊢ (map₂ (LinearMap.mul R A) M N).toAddSubmonoid =
    ⨆ (s : { x // x ∈ M.toAddSubmonoid }), AddSubmonoid.map (AddMonoidHom.mulLeft ↑s) N.toAddSubmonoid
[PROOFSTEP]
rw [map₂, iSup_toAddSubmonoid]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R A
⊢ ⨆ (i : { x // x ∈ M }), (map (↑(LinearMap.mul R A) ↑i) N).toAddSubmonoid =
    ⨆ (s : { x // x ∈ M.toAddSubmonoid }), AddSubmonoid.map (AddMonoidHom.mulLeft ↑s) N.toAddSubmonoid
[PROOFSTEP]
rfl
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
C : A → Prop
r : A
hr : r ∈ M * N
hm : ∀ (m : A), m ∈ M → ∀ (n : A), n ∈ N → C (m * n)
ha : ∀ (x y : A), C x → C y → C (x + y)
⊢ C r
[PROOFSTEP]
rw [← mem_toAddSubmonoid, mul_toAddSubmonoid] at hr 
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
C : A → Prop
r : A
hr : r ∈ M.toAddSubmonoid * N.toAddSubmonoid
hm : ∀ (m : A), m ∈ M → ∀ (n : A), n ∈ N → C (m * n)
ha : ∀ (x y : A), C x → C y → C (x + y)
⊢ C r
[PROOFSTEP]
exact AddSubmonoid.mul_induction_on hr hm ha
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
C : (r : A) → r ∈ M * N → Prop
hm : ∀ (m : A) (x : m ∈ M) (n : A) (x_1 : n ∈ N), C (m * n) (_ : m * n ∈ M * N)
ha : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) (_ : x + y ∈ M * N)
r : A
hr : r ∈ M * N
⊢ C r hr
[PROOFSTEP]
refine' Exists.elim _ fun (hr : r ∈ M * N) (hc : C r hr) => hc
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
C : (r : A) → r ∈ M * N → Prop
hm : ∀ (m : A) (x : m ∈ M) (n : A) (x_1 : n ∈ N), C (m * n) (_ : m * n ∈ M * N)
ha : ∀ (x : A) (hx : x ∈ M * N) (y : A) (hy : y ∈ M * N), C x hx → C y hy → C (x + y) (_ : x + y ∈ M * N)
r : A
hr : r ∈ M * N
⊢ ∃ x, C r x
[PROOFSTEP]
exact
  Submodule.mul_induction_on hr (fun x hx y hy => ⟨_, hm _ hx _ hy⟩) fun x y ⟨_, hx⟩ ⟨_, hy⟩ => ⟨_, ha _ _ _ _ hx hy⟩
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ 1 * M = M
[PROOFSTEP]
conv_lhs => rw [one_eq_span, ← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
| 1 * M
[PROOFSTEP]
rw [one_eq_span, ← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
| 1 * M
[PROOFSTEP]
rw [one_eq_span, ← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
| 1 * M
[PROOFSTEP]
rw [one_eq_span, ← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ span R {1} * span R ↑M = M
[PROOFSTEP]
erw [span_mul_span, one_mul, span_eq]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ M * 1 = M
[PROOFSTEP]
conv_lhs => rw [one_eq_span, ← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
| M * 1
[PROOFSTEP]
rw [one_eq_span, ← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
| M * 1
[PROOFSTEP]
rw [one_eq_span, ← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
| M * 1
[PROOFSTEP]
rw [one_eq_span, ← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ span R ↑M * span R {1} = M
[PROOFSTEP]
erw [span_mul_span, mul_one, span_eq]
[GOAL]
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ ⨆ (i : { x // x ∈ M }), map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N) =
    map (AlgHom.toLinearMap f) M * map (AlgHom.toLinearMap f) N
[PROOFSTEP]
apply congr_arg sSup
[GOAL]
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
⊢ (range fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) =
    range fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)
[PROOFSTEP]
ext S
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ (S ∈ range fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) ↔
    S ∈ range fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ (S ∈ range fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) →
    S ∈ range fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case h.mpr
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
⊢ (S ∈ range fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) →
    S ∈ range fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)
[PROOFSTEP]
rintro ⟨y, hy⟩
[GOAL]
case h.mp.intro
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ M }
hy : (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) y = S
⊢ S ∈ range fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)
[PROOFSTEP]
use⟨f y, mem_map.mpr ⟨y.1, y.2, rfl⟩⟩
    -- porting note: added `⟨⟩`
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ M }
hy : (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) y = S
⊢ (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N))
      { val := ↑f ↑y, property := (_ : ↑f ↑y ∈ map (AlgHom.toLinearMap f) M) } =
    S
[PROOFSTEP]
refine' Eq.trans _ hy
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ M }
hy : (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) y = S
⊢ (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N))
      { val := ↑f ↑y, property := (_ : ↑f ↑y ∈ map (AlgHom.toLinearMap f) M) } =
    (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) y
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ M }
hy : (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) y = S
x✝ : A'
⊢ x✝ ∈
      (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N))
        { val := ↑f ↑y, property := (_ : ↑f ↑y ∈ map (AlgHom.toLinearMap f) M) } ↔
    x✝ ∈ (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) y
[PROOFSTEP]
simp
[GOAL]
case h.mpr.intro
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ map (AlgHom.toLinearMap f) M }
hy : (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y = S
⊢ S ∈ range fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)
[PROOFSTEP]
obtain ⟨y', hy', fy_eq⟩ := mem_map.mp y.2
[GOAL]
case h.mpr.intro.intro.intro
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ map (AlgHom.toLinearMap f) M }
hy : (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : ↑(AlgHom.toLinearMap f) y' = ↑y
⊢ S ∈ range fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)
[PROOFSTEP]
use⟨y', hy'⟩
    -- porting note: added `⟨⟩`
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ map (AlgHom.toLinearMap f) M }
hy : (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : ↑(AlgHom.toLinearMap f) y' = ↑y
⊢ (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) { val := y', property := hy' } = S
[PROOFSTEP]
refine' Eq.trans _ hy
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ map (AlgHom.toLinearMap f) M }
hy : (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : ↑(AlgHom.toLinearMap f) y' = ↑y
⊢ (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) { val := y', property := hy' } =
    (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y
[PROOFSTEP]
rw [f.toLinearMap_apply] at fy_eq 
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ map (AlgHom.toLinearMap f) M }
hy : (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : ↑f y' = ↑y
⊢ (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) { val := y', property := hy' } =
    (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : Semiring A
inst✝² : Algebra R A
S✝ T : Set A
M N P Q : Submodule R A
m n : A
A' : Type u_1
inst✝¹ : Semiring A'
inst✝ : Algebra R A'
f : A →ₐ[R] A'
S : Submodule R A'
y : { x // x ∈ map (AlgHom.toLinearMap f) M }
hy : (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y = S
y' : A
hy' : y' ∈ M
fy_eq : ↑f y' = ↑y
x✝ : A'
⊢ x✝ ∈ (fun i => map (AlgHom.toLinearMap f) (map (↑(LinearMap.mul R A) ↑i) N)) { val := y', property := hy' } ↔
    x✝ ∈ (fun s => map (↑(LinearMap.mul R A') ↑s) (map (AlgHom.toLinearMap f) N)) y
[PROOFSTEP]
simp [fy_eq]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ map (↑(opLinearEquiv R)) (M * N) = map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ map (↑(opLinearEquiv R)) (M * N) ≤ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M
[PROOFSTEP]
simp_rw [map_le_iff_le_comap]
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ M * N ≤ comap (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M)
[PROOFSTEP]
refine' mul_le.2 fun m hm n hn => _
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m✝ n✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ m * n ∈ comap (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M)
[PROOFSTEP]
rw [mem_comap, map_equiv_eq_comap_symm, map_equiv_eq_comap_symm]
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m✝ n✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ ↑↑(opLinearEquiv R) (m * n) ∈
    comap (↑(LinearEquiv.symm (opLinearEquiv R))) N * comap (↑(LinearEquiv.symm (opLinearEquiv R))) M
[PROOFSTEP]
show op n * op m ∈ _
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m✝ n✝ m : A
hm : m ∈ M
n : A
hn : n ∈ N
⊢ op n * op m ∈ comap (↑(LinearEquiv.symm (opLinearEquiv R))) N * comap (↑(LinearEquiv.symm (opLinearEquiv R))) M
[PROOFSTEP]
exact mul_mem_mul hn hm
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ map (↑(opLinearEquiv R)) N * map (↑(opLinearEquiv R)) M ≤ map (↑(opLinearEquiv R)) (M * N)
[PROOFSTEP]
refine' mul_le.2 (MulOpposite.rec' fun m hm => MulOpposite.rec' fun n hn => _)
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m✝ n✝ m : A
hm : op m ∈ map (↑(opLinearEquiv R)) N
n : A
hn : op n ∈ map (↑(opLinearEquiv R)) M
⊢ op m * op n ∈ map (↑(opLinearEquiv R)) (M * N)
[PROOFSTEP]
rw [Submodule.mem_map_equiv] at hm hn ⊢
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m✝ n✝ m : A
hm : ↑(LinearEquiv.symm (opLinearEquiv R)) (op m) ∈ N
n : A
hn : ↑(LinearEquiv.symm (opLinearEquiv R)) (op n) ∈ M
⊢ ↑(LinearEquiv.symm (opLinearEquiv R)) (op m * op n) ∈ M * N
[PROOFSTEP]
exact mul_mem_mul hn hm
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ comap (↑(LinearEquiv.symm (opLinearEquiv R))) (M * N) =
    comap (↑(LinearEquiv.symm (opLinearEquiv R))) N * comap (↑(LinearEquiv.symm (opLinearEquiv R))) M
[PROOFSTEP]
simp_rw [← map_equiv_eq_comap_symm, map_op_mul]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ↑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R)) (map (↑(LinearEquiv.symm (opLinearEquiv R))) (M * N)) =
    map (↑(opLinearEquiv R))
      (map (↑(LinearEquiv.symm (opLinearEquiv R))) N * map (↑(LinearEquiv.symm (opLinearEquiv R))) M)
[PROOFSTEP]
rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe, LinearEquiv.symm_trans_self,
  LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N✝ P Q : Submodule R A
m n : A
M N : Submodule R Aᵐᵒᵖ
⊢ comap (↑(opLinearEquiv R)) (M * N) = comap (↑(opLinearEquiv R)) N * comap (↑(opLinearEquiv R)) M
[PROOFSTEP]
simp_rw [comap_equiv_eq_map_symm, map_unop_mul]
[GOAL]
ι : Sort uι
R✝ : Type u
inst✝⁶ : CommSemiring R✝
A✝ : Type v
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
S✝ T : Set A✝
M N P Q : Submodule R✝ A✝
m n : A✝
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
⊢ ∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')
[PROOFSTEP]
obtain ⟨U, h, hU⟩ := mem_span_finite_of_mem_span hx
[GOAL]
case intro.intro
ι : Sort uι
R✝ : Type u
inst✝⁶ : CommSemiring R✝
A✝ : Type v
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
S✝ T : Set A✝
M N P Q : Submodule R✝ A✝
m n : A✝
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
⊢ ∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')
[PROOFSTEP]
obtain ⟨T, T', hS, hS', h⟩ := Finset.subset_mul h
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Sort uι
R✝ : Type u
inst✝⁶ : CommSemiring R✝
A✝ : Type v
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
S✝ T✝ : Set A✝
M N P Q : Submodule R✝ A✝
m n : A✝
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h✝ : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
T T' : Finset A
hS : ↑T ⊆ S
hS' : ↑T' ⊆ S'
h : U ⊆ T * T'
⊢ ∃ T T', ↑T ⊆ S ∧ ↑T' ⊆ S' ∧ x ∈ span R (↑T * ↑T')
[PROOFSTEP]
use T, T', hS, hS'
[GOAL]
case right
ι : Sort uι
R✝ : Type u
inst✝⁶ : CommSemiring R✝
A✝ : Type v
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
S✝ T✝ : Set A✝
M N P Q : Submodule R✝ A✝
m n : A✝
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h✝ : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
T T' : Finset A
hS : ↑T ⊆ S
hS' : ↑T' ⊆ S'
h : U ⊆ T * T'
⊢ x ∈ span R (↑T * ↑T')
[PROOFSTEP]
have h' : (U : Set A) ⊆ T * T' := by assumption_mod_cast
[GOAL]
ι : Sort uι
R✝ : Type u
inst✝⁶ : CommSemiring R✝
A✝ : Type v
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
S✝ T✝ : Set A✝
M N P Q : Submodule R✝ A✝
m n : A✝
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h✝ : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
T T' : Finset A
hS : ↑T ⊆ S
hS' : ↑T' ⊆ S'
h : U ⊆ T * T'
⊢ ↑U ⊆ ↑T * ↑T'
[PROOFSTEP]
assumption_mod_cast
[GOAL]
case right
ι : Sort uι
R✝ : Type u
inst✝⁶ : CommSemiring R✝
A✝ : Type v
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
S✝ T✝ : Set A✝
M N P Q : Submodule R✝ A✝
m n : A✝
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h✝ : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
T T' : Finset A
hS : ↑T ⊆ S
hS' : ↑T' ⊆ S'
h : U ⊆ T * T'
h' : ↑U ⊆ ↑T * ↑T'
⊢ x ∈ span R (↑T * ↑T')
[PROOFSTEP]
have h'' := span_mono h' hU
[GOAL]
case right
ι : Sort uι
R✝ : Type u
inst✝⁶ : CommSemiring R✝
A✝ : Type v
inst✝⁵ : Semiring A✝
inst✝⁴ : Algebra R✝ A✝
S✝ T✝ : Set A✝
M N P Q : Submodule R✝ A✝
m n : A✝
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : AddCommMonoid A
inst✝¹ : Mul A
inst✝ : Module R A
S S' : Set A
x : A
hx : x ∈ span R (S * S')
U : Finset A
h✝ : ↑U ⊆ S * S'
hU : x ∈ span R ↑U
T T' : Finset A
hS : ↑T ⊆ S
hS' : ↑T' ⊆ S'
h : U ⊆ T * T'
h' : ↑U ⊆ ↑T * ↑T'
h'' : x ∈ span R (↑T * ↑T')
⊢ x ∈ span R (↑T * ↑T')
[PROOFSTEP]
assumption
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P✝ Q✝ : Submodule R A
m n : A
P Q : Submodule R A
x : A
hx : x ∈ P * Q
⊢ x ∈ span R (↑P * ↑Q)
[PROOFSTEP]
rwa [← Submodule.span_eq P, ← Submodule.span_eq Q, Submodule.span_mul_span] at hx 
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n x y : A
⊢ x ∈ span R {y} * P ↔ ∃ z, z ∈ P ∧ y * z = x
[PROOFSTEP]
simp_rw [(· * ·), Mul.mul, map₂_span_singleton_eq_map]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n x y : A
⊢ x ∈ map (↑(LinearMap.mul R A) y) P ↔ ∃ z, z ∈ P ∧ Mul.mul y z = x
[PROOFSTEP]
rfl
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n x y : A
⊢ x ∈ P * span R {y} ↔ ∃ z, z ∈ P ∧ z * y = x
[PROOFSTEP]
simp_rw [(· * ·), Mul.mul, map₂_span_singleton_eq_map_flip]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n x y : A
⊢ x ∈ map (↑(LinearMap.flip (LinearMap.mul R A)) y) P ↔ ∃ z, z ∈ P ∧ Mul.mul z y = x
[PROOFSTEP]
rfl
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
src✝² : Semigroup (Submodule R A) :=
  Function.Injective.semigroup toAddSubmonoid (_ : Function.Injective toAddSubmonoid)
    (_ : ∀ (m n : Submodule R A), (m * n).toAddSubmonoid = m.toAddSubmonoid * n.toAddSubmonoid)
src✝¹ : AddMonoidWithOne (Submodule R A) := AddMonoidWithOne.unary
src✝ : AddCommMonoid (Submodule R A) := pointwiseAddCommMonoid
⊢ Lattice (Submodule R A)
[PROOFSTEP]
infer_instance
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
s : Set A
⊢ span R s ^ 0 = span R (s ^ 0)
[PROOFSTEP]
rw [pow_zero, pow_zero, one_eq_span_one_set]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
s : Set A
n : ℕ
⊢ span R s ^ (n + 1) = span R (s ^ (n + 1))
[PROOFSTEP]
rw [pow_succ, pow_succ, span_pow s n, span_mul_span]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
⊢ M ^ n = span R (↑M ^ n)
[PROOFSTEP]
rw [← span_pow, span_eq]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
h : n ≠ 0
⊢ (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
h✝ : n ≠ 0
h : Nat.zero ≠ 0
⊢ (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid ^ Nat.zero
[PROOFSTEP]
exact (h rfl).elim
[GOAL]
case succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
n✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : Nat.succ n ≠ 0
⊢ (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, pow_succ, mul_toAddSubmonoid]
[GOAL]
case succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
n✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : Nat.succ n ≠ 0
⊢ M.toAddSubmonoid * (M ^ n).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ n
[PROOFSTEP]
cases n with
| zero => rw [pow_zero, pow_zero, mul_one, ← mul_toAddSubmonoid, mul_one]
| succ n => rw [ih n.succ_ne_zero]
[GOAL]
case succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
n✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : n ≠ 0 → (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n
h : Nat.succ n ≠ 0
⊢ M.toAddSubmonoid * (M ^ n).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ n
[PROOFSTEP]
cases n with
| zero => rw [pow_zero, pow_zero, mul_one, ← mul_toAddSubmonoid, mul_one]
| succ n => rw [ih n.succ_ne_zero]
[GOAL]
case succ.zero
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
h✝ : n ≠ 0
ih : Nat.zero ≠ 0 → (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid ^ Nat.zero
h : Nat.succ Nat.zero ≠ 0
⊢ M.toAddSubmonoid * (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ Nat.zero
[PROOFSTEP]

| zero => rw [pow_zero, pow_zero, mul_one, ← mul_toAddSubmonoid, mul_one]
[GOAL]
case succ.zero
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
h✝ : n ≠ 0
ih : Nat.zero ≠ 0 → (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid ^ Nat.zero
h : Nat.succ Nat.zero ≠ 0
⊢ M.toAddSubmonoid * (M ^ Nat.zero).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ Nat.zero
[PROOFSTEP]
rw [pow_zero, pow_zero, mul_one, ← mul_toAddSubmonoid, mul_one]
[GOAL]
case succ.succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
n✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : Nat.succ n ≠ 0 → (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid ^ Nat.succ n
h : Nat.succ (Nat.succ n) ≠ 0
⊢ M.toAddSubmonoid * (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ Nat.succ n
[PROOFSTEP]

| succ n => rw [ih n.succ_ne_zero]
[GOAL]
case succ.succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
n✝ : ℕ
h✝ : n✝ ≠ 0
n : ℕ
ih : Nat.succ n ≠ 0 → (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid ^ Nat.succ n
h : Nat.succ (Nat.succ n) ≠ 0
⊢ M.toAddSubmonoid * (M ^ Nat.succ n).toAddSubmonoid = M.toAddSubmonoid * M.toAddSubmonoid ^ Nat.succ n
[PROOFSTEP]
rw [ih n.succ_ne_zero]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
[PROOFSTEP]
obtain rfl | hn := Decidable.eq_or_ne n 0
[GOAL]
case inl
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ M.toAddSubmonoid ^ 0 ≤ (M ^ 0).toAddSubmonoid
[PROOFSTEP]
rw [pow_zero, pow_zero]
[GOAL]
case inl
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
⊢ 1 ≤ 1.toAddSubmonoid
[PROOFSTEP]
exact le_one_toAddSubmonoid
[GOAL]
case inr
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
hn : n ≠ 0
⊢ M.toAddSubmonoid ^ n ≤ (M ^ n).toAddSubmonoid
[PROOFSTEP]
exact (pow_toAddSubmonoid M hn).ge
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → C (Nat.succ i) (m * x) (_ : m * x ∈ M * npowRec i M)
n : ℕ
x : A
hx : x ∈ M ^ n
⊢ C n x hx
[PROOFSTEP]
induction' n with n n_ih generalizing x
[GOAL]
case zero
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → C (Nat.succ i) (m * x) (_ : m * x ∈ M * npowRec i M)
n : ℕ
x✝ : A
hx✝ : x✝ ∈ M ^ n
x : A
hx : x ∈ M ^ Nat.zero
⊢ C Nat.zero x hx
[PROOFSTEP]
rw [pow_zero] at hx 
[GOAL]
case zero
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → C (Nat.succ i) (m * x) (_ : m * x ∈ M * npowRec i M)
n : ℕ
x✝ : A
hx✝¹ : x✝ ∈ M ^ n
x : A
hx✝ : x ∈ M ^ Nat.zero
hx : x ∈ 1
⊢ C Nat.zero x hx✝
[PROOFSTEP]
obtain ⟨r, rfl⟩ := hx
[GOAL]
case zero.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → C (Nat.succ i) (m * x) (_ : m * x ∈ M * npowRec i M)
n : ℕ
x : A
hx✝ : x ∈ M ^ n
r : R
hx : ↑(Algebra.linearMap R A) r ∈ M ^ Nat.zero
⊢ C Nat.zero (↑(Algebra.linearMap R A) r) hx
[PROOFSTEP]
exact hr r
[GOAL]
case succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → C (Nat.succ i) (m * x) (_ : m * x ∈ M * npowRec i M)
n✝ : ℕ
x✝ : A
hx✝ : x✝ ∈ M ^ n✝
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx : x ∈ M ^ Nat.succ n
⊢ C (Nat.succ n) x hx
[PROOFSTEP]
exact
  Submodule.mul_induction_on' (fun m hm x ih => hmul _ hm _ _ _ (n_ih ih)) (fun x hx y hy Cx Cy => hadd _ _ _ _ _ Cx Cy)
    hx
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n : ℕ
x : A
hx : x ∈ M ^ n
⊢ C n x hx
[PROOFSTEP]
induction' n with n n_ih generalizing x
[GOAL]
case zero
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n : ℕ
x✝ : A
hx✝ : x✝ ∈ M ^ n
x : A
hx : x ∈ M ^ Nat.zero
⊢ C Nat.zero x hx
[PROOFSTEP]
rw [pow_zero] at hx 
[GOAL]
case zero
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n : ℕ
x✝ : A
hx✝¹ : x✝ ∈ M ^ n
x : A
hx✝ : x ∈ M ^ Nat.zero
hx : x ∈ 1
⊢ C Nat.zero x hx✝
[PROOFSTEP]
obtain ⟨r, rfl⟩ := hx
[GOAL]
case zero.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n : ℕ
x : A
hx✝ : x ∈ M ^ n
r : R
hx : ↑(Algebra.linearMap R A) r ∈ M ^ Nat.zero
⊢ C Nat.zero (↑(Algebra.linearMap R A) r) hx
[PROOFSTEP]
exact hr r
[GOAL]
case succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n✝ : ℕ
x✝ : A
hx✝ : x✝ ∈ M ^ n✝
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx : x ∈ M ^ Nat.succ n
⊢ C (Nat.succ n) x hx
[PROOFSTEP]
revert hx
[GOAL]
case succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n✝ : ℕ
x✝ : A
hx : x✝ ∈ M ^ n✝
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx : x ∈ M ^ Nat.succ n), C (Nat.succ n) x hx
[PROOFSTEP]
suffices h_lean4_1926 : ∀ (hx' : x ∈ M ^ n * M), C (Nat.succ n) x (by rwa [pow_succ']) from fun hx =>
  h_lean4_1926
    (by rwa [← pow_succ'])
      -- porting note: end workaround
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n✝ : ℕ
x✝ : A
hx : x✝ ∈ M ^ n✝
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx' : x ∈ M ^ n * M
⊢ x ∈ M ^ Nat.succ n
[PROOFSTEP]
rwa [pow_succ']
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n✝ : ℕ
x✝ : A
hx✝ : x✝ ∈ M ^ n✝
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
h_lean4_1926 : ∀ (hx' : x ∈ M ^ n * M), C (Nat.succ n) x (_ : x ∈ M ^ Nat.succ n)
hx : x ∈ M ^ Nat.succ n
⊢ x ∈ M ^ n * M
[PROOFSTEP]
rwa [← pow_succ']
[GOAL]
case succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n✝ : ℕ
x✝ : A
hx : x✝ ∈ M ^ n✝
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
⊢ ∀ (hx' : x ∈ M ^ n * M), C (Nat.succ n) x (_ : x ∈ M ^ Nat.succ n)
[PROOFSTEP]
intro hx
[GOAL]
case succ
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝¹ : A
C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop
hr : ∀ (r : R), C 0 (↑(algebraMap R A) r) (_ : ↑(algebraMap R A) r ∈ 1)
hadd : ∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) (_ : x + y ∈ M ^ i)
hmul :
  ∀ (i : ℕ) (x : A) (hx : x ∈ M ^ i),
    C i x hx → ∀ (m : A) (hm : m ∈ M), C (Nat.succ i) (x * m) (_ : x * m ∈ M ^ (i + 1))
n✝ : ℕ
x✝ : A
hx✝ : x✝ ∈ M ^ n✝
n : ℕ
n_ih : ∀ {x : A} (hx : x ∈ M ^ n), C n x hx
x : A
hx : x ∈ M ^ n * M
⊢ C (Nat.succ n) x (_ : x ∈ M ^ Nat.succ n)
[PROOFSTEP]
exact
  Submodule.mul_induction_on' (fun m hm x ih => hmul _ _ hm (n_ih _) _ ih) (fun x hx y hy Cx Cy => hadd _ _ _ _ _ Cx Cy)
    hx
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
p q : Submodule R Aᵐᵒᵖ
⊢ Equiv.toFun
      { toFun := fun p => op (comap (↑(opLinearEquiv R)) p),
        invFun := fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p),
        left_inv :=
          (_ :
            ∀ (p : Submodule R Aᵐᵒᵖ),
              (fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p))
                  ((fun p => op (comap (↑(opLinearEquiv R)) p)) p) =
                p),
        right_inv :=
          (_ :
            ∀ (p : (Submodule R A)ᵐᵒᵖ),
              (fun p => op (comap (↑(opLinearEquiv R)) p))
                  ((fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p)) p) =
                p) }
      (p + q) =
    Equiv.toFun
        { toFun := fun p => op (comap (↑(opLinearEquiv R)) p),
          invFun := fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p),
          left_inv :=
            (_ :
              ∀ (p : Submodule R Aᵐᵒᵖ),
                (fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p))
                    ((fun p => op (comap (↑(opLinearEquiv R)) p)) p) =
                  p),
          right_inv :=
            (_ :
              ∀ (p : (Submodule R A)ᵐᵒᵖ),
                (fun p => op (comap (↑(opLinearEquiv R)) p))
                    ((fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p)) p) =
                  p) }
        p +
      Equiv.toFun
        { toFun := fun p => op (comap (↑(opLinearEquiv R)) p),
          invFun := fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p),
          left_inv :=
            (_ :
              ∀ (p : Submodule R Aᵐᵒᵖ),
                (fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p))
                    ((fun p => op (comap (↑(opLinearEquiv R)) p)) p) =
                  p),
          right_inv :=
            (_ :
              ∀ (p : (Submodule R A)ᵐᵒᵖ),
                (fun p => op (comap (↑(opLinearEquiv R)) p))
                    ((fun p => comap (↑(LinearEquiv.symm (opLinearEquiv R))) (unop p)) p) =
                  p) }
        q
[PROOFSTEP]
simp [comap_equiv_eq_map_symm, ← op_add]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n✝ : A
n : ℕ
⊢ map (↑(opLinearEquiv R)) (M ^ n) = map (↑(opLinearEquiv R)) M ^ n
[PROOFSTEP]
rw [map_equiv_eq_comap_symm, map_equiv_eq_comap_symm, comap_unop_pow]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M✝ N P Q : Submodule R A
m n✝ : A
n : ℕ
M : Submodule R Aᵐᵒᵖ
⊢ map (↑(LinearEquiv.symm (opLinearEquiv R))) (M ^ n) = map (↑(LinearEquiv.symm (opLinearEquiv R))) M ^ n
[PROOFSTEP]
rw [← comap_equiv_eq_map_symm, ← comap_equiv_eq_map_symm, comap_op_pow]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
s t : SetSemiring A
⊢ OneHom.toFun { toFun := fun s => span R (↑SetSemiring.down s), map_one' := (_ : span R {1} = 1) } (s * t) =
    OneHom.toFun { toFun := fun s => span R (↑SetSemiring.down s), map_one' := (_ : span R {1} = 1) } s *
      OneHom.toFun { toFun := fun s => span R (↑SetSemiring.down s), map_one' := (_ : span R {1} = 1) } t
[PROOFSTEP]
dsimp only
  -- porting note: new, needed due to new-style structures
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Set A
M N P Q : Submodule R A
m n : A
s t : SetSemiring A
⊢ span R (↑SetSemiring.down (s * t)) = span R (↑SetSemiring.down s) * span R (↑SetSemiring.down t)
[PROOFSTEP]
rw [SetSemiring.down_mul, span_mul_span, ← image_mul_prod]
[GOAL]
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
⊢ ∏ i in s, span R (M i) = span R (∏ i in s, M i)
[PROOFSTEP]
letI := Classical.decEq ι
[GOAL]
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i in s, span R (M i) = span R (∏ i in s, M i)
[PROOFSTEP]
refine' Finset.induction_on s _ _
[GOAL]
case refine'_1
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∏ i in ∅, span R (M i) = span R (∏ i in ∅, M i)
[PROOFSTEP]
simp [one_eq_span, Set.singleton_one]
[GOAL]
case refine'_2
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ ⦃a : ι⦄ {s : Finset ι},
    ¬a ∈ s →
      ∏ i in s, span R (M i) = span R (∏ i in s, M i) →
        ∏ i in insert a s, span R (M i) = span R (∏ i in insert a s, M i)
[PROOFSTEP]
intro _ _ H ih
[GOAL]
case refine'_2
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
M : ι → Set A
this : DecidableEq ι := Classical.decEq ι
a✝ : ι
s✝ : Finset ι
H : ¬a✝ ∈ s✝
ih : ∏ i in s✝, span R (M i) = span R (∏ i in s✝, M i)
⊢ ∏ i in insert a✝ s✝, span R (M i) = span R (∏ i in insert a✝ s✝, M i)
[PROOFSTEP]
rw [Finset.prod_insert H, Finset.prod_insert H, ih, span_mul_span]
[GOAL]
ι✝ : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
ι : Type u_1
s : Finset ι
x : ι → A
⊢ ∏ i in s, span R {x i} = span R {∏ i in s, x i}
[PROOFSTEP]
rw [prod_span, Set.finset_prod_singleton]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
⊢ 1 • P = P
[PROOFSTEP]
simp_rw [HSMul.hSMul, SetSemiring.down_one, ← one_eq_span_one_set, one_mul]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
⊢ (s * t) • P = s • t • P
[PROOFSTEP]
simp_rw [HSMul.hSMul, SetSemiring.down_mul, ← mul_assoc, span_mul_span]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
s t : SetSemiring A
P : Submodule R A
⊢ (s + t) • P = s • P + t • P
[PROOFSTEP]
simp_rw [HSMul.hSMul, SetSemiring.down_add, span_union, sup_mul, add_eq_sup]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
P : Submodule R A
⊢ 0 • P = 0
[PROOFSTEP]
simp_rw [HSMul.hSMul, SetSemiring.down_zero, span_empty, bot_mul, bot_eq_zero]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ ↑Set.up {a} • M = map (LinearMap.mulLeft R a) M
[PROOFSTEP]
conv_lhs => rw [← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
| ↑Set.up {a} • M
[PROOFSTEP]
rw [← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
| ↑Set.up {a} • M
[PROOFSTEP]
rw [← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
| ↑Set.up {a} • M
[PROOFSTEP]
rw [← span_eq M]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ ↑Set.up {a} • span R ↑M = map (LinearMap.mulLeft R a) M
[PROOFSTEP]
change span _ _ * span _ _ = _
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a})) * span R ↑M = map (LinearMap.mulLeft R a) M
[PROOFSTEP]
rw [span_mul_span]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M) = map (LinearMap.mulLeft R a) M
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M) ≤ map (LinearMap.mulLeft R a) M
[PROOFSTEP]
rw [span_le]
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ ↑SetSemiring.down (↑Set.up {a}) * ↑M ⊆ ↑(map (LinearMap.mulLeft R a) M)
[PROOFSTEP]
rintro _ ⟨b, m, hb, hm, rfl⟩
[GOAL]
case a.intro.intro.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
b m : A
hb : b ∈ ↑SetSemiring.down (↑Set.up {a})
hm : m ∈ ↑M
⊢ (fun x x_1 => x * x_1) b m ∈ ↑(map (LinearMap.mulLeft R a) M)
[PROOFSTEP]
rw [SetLike.mem_coe, mem_map, Set.mem_singleton_iff.mp hb]
[GOAL]
case a.intro.intro.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
b m : A
hb : b ∈ ↑SetSemiring.down (↑Set.up {a})
hm : m ∈ ↑M
⊢ ∃ y, y ∈ M ∧ ↑(LinearMap.mulLeft R a) y = (fun x x_1 => x * x_1) a m
[PROOFSTEP]
exact ⟨m, hm, rfl⟩
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m n a : A
M : Submodule R A
⊢ map (LinearMap.mulLeft R a) M ≤ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M)
[PROOFSTEP]
rintro _ ⟨m, hm, rfl⟩
[GOAL]
case a.intro.intro
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M✝ N : Submodule R A
m✝ n a : A
M : Submodule R A
m : A
hm : m ∈ ↑M
⊢ ↑(LinearMap.mulLeft R a) m ∈ span R (↑SetSemiring.down (↑Set.up {a}) * ↑M)
[PROOFSTEP]
exact subset_span ⟨a, m, Set.mem_singleton a, hm, rfl⟩
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a✝ b✝ : A
ha : a✝ ∈ {x | ∀ (y : A), y ∈ J → x * y ∈ I}
hb : b✝ ∈ {x | ∀ (y : A), y ∈ J → x * y ∈ I}
y : A
hy : y ∈ J
⊢ (a✝ + b✝) * y ∈ I
[PROOFSTEP]
rw [add_mul]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
a✝ b✝ : A
ha : a✝ ∈ {x | ∀ (y : A), y ∈ J → x * y ∈ I}
hb : b✝ ∈ {x | ∀ (y : A), y ∈ J → x * y ∈ I}
y : A
hy : y ∈ J
⊢ a✝ * y + b✝ * y ∈ I
[PROOFSTEP]
exact Submodule.add_mem _ (ha _ hy) (hb _ hy)
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
y : A
x✝ : y ∈ J
⊢ 0 * y ∈ I
[PROOFSTEP]
rw [zero_mul]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
y : A
x✝ : y ∈ J
⊢ 0 ∈ I
[PROOFSTEP]
apply Submodule.zero_mem
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ∀ (y : A), y ∈ J → x * y ∈ I},
              add_mem' :=
                (_ :
                  ∀ {a b : A},
                    a ∈ {x | ∀ (y : A), y ∈ J → x * y ∈ I} →
                      b ∈ {x | ∀ (y : A), y ∈ J → x * y ∈ I} → ∀ (y : A), y ∈ J → (a + b) * y ∈ I) },
          zero_mem' := (_ : ∀ (y : A), y ∈ J → 0 * y ∈ I) }.toAddSubsemigroup.carrier
y : A
hy : y ∈ J
⊢ r • x * y ∈ I
[PROOFSTEP]
rw [Algebra.smul_mul_assoc]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J : Submodule R A
r : R
x : A
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {x | ∀ (y : A), y ∈ J → x * y ∈ I},
              add_mem' :=
                (_ :
                  ∀ {a b : A},
                    a ∈ {x | ∀ (y : A), y ∈ J → x * y ∈ I} →
                      b ∈ {x | ∀ (y : A), y ∈ J → x * y ∈ I} → ∀ (y : A), y ∈ J → (a + b) * y ∈ I) },
          zero_mem' := (_ : ∀ (y : A), y ∈ J → 0 * y ∈ I) }.toAddSubsemigroup.carrier
y : A
hy : y ∈ J
⊢ r • (x * y) ∈ I
[PROOFSTEP]
exact Submodule.smul_mem _ _ (hx _ hy)
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 => x • x_1) y' = y
⊢ y ∈ ↑I
[PROOFSTEP]
rw [← xy'_eq_y]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 => x • x_1) y' = y
⊢ (fun x_1 => x • x_1) y' ∈ ↑I
[PROOFSTEP]
apply h
[GOAL]
case a
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n x : A
I J : Submodule R A
h : x ∈ I / J
y : A
x✝ : y ∈ x • ↑J
y' : A
hy' : y' ∈ ↑J
xy'_eq_y : (fun x_1 => x • x_1) y' = y
⊢ y' ∈ J
[PROOFSTEP]
assumption
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I J K : Submodule R A
⊢ I ≤ J / K ↔ I * K ≤ J
[PROOFSTEP]
rw [le_div_iff, mul_le]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ 1 ≤ 1 / I ↔ I ≤ 1
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ 1 ≤ 1 / I → I ≤ 1
case mpr
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ I ≤ 1 → 1 ≤ 1 / I
[PROOFSTEP]
all_goals intro hI
[GOAL]
case mp
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ 1 ≤ 1 / I → I ≤ 1
[PROOFSTEP]
intro hI
[GOAL]
case mpr
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ I ≤ 1 → 1 ≤ 1 / I
[PROOFSTEP]
intro hI
[GOAL]
case mp
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
hI : 1 ≤ 1 / I
⊢ I ≤ 1
[PROOFSTEP]
rwa [le_div_iff_mul_le, one_mul] at hI 
[GOAL]
case mpr
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
hI : I ≤ 1
⊢ 1 ≤ 1 / I
[PROOFSTEP]
rwa [le_div_iff_mul_le, one_mul]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
hI : I ≤ 1
⊢ I ≤ I * (1 / I)
[PROOFSTEP]
refine
  (mul_one I).symm.trans_le
    ?_
      -- porting note: drop `rw {occs := _}` in favor of `refine`
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
hI : I ≤ 1
⊢ I * 1 ≤ I * (1 / I)
[PROOFSTEP]
apply mul_le_mul_right (one_le_one_div.mpr hI)
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ I * (1 / I) ≤ 1
[PROOFSTEP]
rw [Submodule.mul_le]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m n : A
I : Submodule R A
⊢ ∀ (m : A), m ∈ I → ∀ (n : A), n ∈ 1 / I → m * n ∈ 1
[PROOFSTEP]
intro m hm n hn
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : n ∈ 1 / I
⊢ m * n ∈ 1
[PROOFSTEP]
rw [Submodule.mem_div_iff_forall_mul_mem] at hn 
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ (y : A), y ∈ I → n * y ∈ 1
⊢ m * n ∈ 1
[PROOFSTEP]
rw [mul_comm]
[GOAL]
ι : Sort uι
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
M N : Submodule R A
m✝ n✝ : A
I : Submodule R A
m : A
hm : m ∈ I
n : A
hn : ∀ (y : A), y ∈ I → n * y ∈ 1
⊢ n * m ∈ 1
[PROOFSTEP]
exact hn m hm
[GOAL]
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
⊢ map (AlgEquiv.toLinearMap h) (I / J) = map (AlgEquiv.toLinearMap h) I / map (AlgEquiv.toLinearMap h) J
[PROOFSTEP]
ext x
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ x ∈ map (AlgEquiv.toLinearMap h) (I / J) ↔ x ∈ map (AlgEquiv.toLinearMap h) I / map (AlgEquiv.toLinearMap h) J
[PROOFSTEP]
simp only [mem_map, mem_div_iff_forall_mul_mem]
[GOAL]
case h
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ (∃ y, (∀ (y_1 : A), y_1 ∈ J → y * y_1 ∈ I) ∧ ↑(AlgEquiv.toLinearMap h) y = x) ↔
    ∀ (y : B),
      (∃ y_1, y_1 ∈ J ∧ ↑(AlgEquiv.toLinearMap h) y_1 = y) → ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = x * y
[PROOFSTEP]
constructor
[GOAL]
case h.mp
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ (∃ y, (∀ (y_1 : A), y_1 ∈ J → y * y_1 ∈ I) ∧ ↑(AlgEquiv.toLinearMap h) y = x) →
    ∀ (y : B),
      (∃ y_1, y_1 ∈ J ∧ ↑(AlgEquiv.toLinearMap h) y_1 = y) → ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = x * y
[PROOFSTEP]
rintro ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
[GOAL]
case h.mp.intro.intro.intro.intro
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : A
hx : ∀ (y : A), y ∈ J → x * y ∈ I
y : A
hy : y ∈ J
⊢ ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = ↑(AlgEquiv.toLinearMap h) x * ↑(AlgEquiv.toLinearMap h) y
[PROOFSTEP]
exact ⟨x * y, hx _ hy, h.map_mul x y⟩
[GOAL]
case h.mpr
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
⊢ (∀ (y : B),
      (∃ y_1, y_1 ∈ J ∧ ↑(AlgEquiv.toLinearMap h) y_1 = y) → ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = x * y) →
    ∃ y, (∀ (y_1 : A), y_1 ∈ J → y * y_1 ∈ I) ∧ ↑(AlgEquiv.toLinearMap h) y = x
[PROOFSTEP]
rintro hx
[GOAL]
case h.mpr
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx :
  ∀ (y : B),
    (∃ y_1, y_1 ∈ J ∧ ↑(AlgEquiv.toLinearMap h) y_1 = y) → ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = x * y
⊢ ∃ y, (∀ (y_1 : A), y_1 ∈ J → y * y_1 ∈ I) ∧ ↑(AlgEquiv.toLinearMap h) y = x
[PROOFSTEP]
refine' ⟨h.symm x, fun z hz => _, h.apply_symm_apply x⟩
[GOAL]
case h.mpr
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx :
  ∀ (y : B),
    (∃ y_1, y_1 ∈ J ∧ ↑(AlgEquiv.toLinearMap h) y_1 = y) → ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = x * y
z : A
hz : z ∈ J
⊢ ↑(AlgEquiv.symm h) x * z ∈ I
[PROOFSTEP]
obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩
[GOAL]
case h.mpr.intro.intro
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx :
  ∀ (y : B),
    (∃ y_1, y_1 ∈ J ∧ ↑(AlgEquiv.toLinearMap h) y_1 = y) → ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : ↑(AlgEquiv.toLinearMap h) xz = x * ↑h z
⊢ ↑(AlgEquiv.symm h) x * z ∈ I
[PROOFSTEP]
convert xz_mem
[GOAL]
case h.e'_4
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx :
  ∀ (y : B),
    (∃ y_1, y_1 ∈ J ∧ ↑(AlgEquiv.toLinearMap h) y_1 = y) → ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : ↑(AlgEquiv.toLinearMap h) xz = x * ↑h z
⊢ ↑(AlgEquiv.symm h) x * z = xz
[PROOFSTEP]
apply h.injective
[GOAL]
case h.e'_4.a
ι : Sort uι
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
M N : Submodule R A
m n : A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
x : B
hx :
  ∀ (y : B),
    (∃ y_1, y_1 ∈ J ∧ ↑(AlgEquiv.toLinearMap h) y_1 = y) → ∃ y_1, y_1 ∈ I ∧ ↑(AlgEquiv.toLinearMap h) y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : ↑(AlgEquiv.toLinearMap h) xz = x * ↑h z
⊢ ↑h (↑(AlgEquiv.symm h) x * z) = ↑h xz
[PROOFSTEP]
erw [h.map_mul, h.apply_symm_apply, hxz]
