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
ι : 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
ext x
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
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
simp only [mem_map, mem_div_iff_forall_mul_mem]
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

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
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
constructor
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
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
rintro ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
no goals
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
exact ⟨x * y, hx _ hy, h.map_mul x y⟩
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
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
rintro hx
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
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
refine' ⟨h.symm x, fun z hz => _, h.apply_symm_apply x⟩
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
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
obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩
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
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
convert xz_mem
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
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
apply h.injective
no goals
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
erw [h.map_mul, h.apply_symm_apply, hxz]