-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_div {B : Type*} [CommSemiring B] [Algebra R B] (I J : Submodule R A)
    (h : A ≃ₐ[R] B) : (I / J).map h.toLinearMap = I.map h.toLinearMap / J.map h.toLinearMap

Proof state:
case h.e'_5.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h.toLinearMap xz = x * h z
⊢ x * h z = h xz

Tactic:
simp only [AlgEquiv.toLinearMap_apply] at hxz

Result:
case h.e'_5.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h xz = x * h z
⊢ x * h z = h xz

Proof state:
case h.mp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x) →
    ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y

Tactic:
rintro ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩

Result:
case h.mp.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, x * y ∈ I
y : A
hy : y ∈ J
⊢ ∃ y_1 ∈ I, h.toLinearMap y_1 = h.toLinearMap x * h.toLinearMap y

Proof state:
case h.mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
⊢ h.symm x * z ∈ I

Tactic:
obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩

Result:
case h.mpr.intro.intro
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h.toLinearMap xz = x * h z
⊢ h.symm x * z ∈ I

Proof state:
case h.mp.intro.intro.intro.intro
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, x * y ∈ I
y : A
hy : y ∈ J
⊢ ∃ y_1 ∈ I, h.toLinearMap y_1 = h.toLinearMap x * h.toLinearMap y

Tactic:
exact ⟨x * y, hx _ hy, map_mul h x y⟩

Result:
no goals

Proof state:
case h.e'_5.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h.toLinearMap xz = x * h z
⊢ h (h.symm x * z) = h xz

Tactic:
rw [map_mul, h.apply_symm_apply]

Result:
case h.e'_5.a
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h.toLinearMap xz = x * h z
⊢ x * h z = h xz

Proof state:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x) ↔
    ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y

Tactic:
constructor

Result:
case h.mp
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x) →
    ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y

case h.mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y) →
    ∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x

Proof state:
case h.mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y) →
    ∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x

Tactic:
rintro hx

Result:
case h.mpr
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
⊢ ∃ y, (∀ y_1 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x

Proof state:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 h.toLinearMap (I / J) ↔ x ∈ map h.toLinearMap I / map h.toLinearMap J

Tactic:
simp only [mem_map, mem_div_iff_forall_mul_mem]

Result:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, y * y_1 ∈ I) ∧ h.toLinearMap y = x) ↔
    ∀ (y : B), (∃ y_1 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y

Proof state:
case h.mpr.intro.intro
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h.toLinearMap xz = x * h z
⊢ h.symm x * z ∈ I

Tactic:
convert xz_mem

Result:
case h.e'_5
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 ∈ J, h.toLinearMap y_1 = y) → ∃ y_1 ∈ I, h.toLinearMap y_1 = x * y
z : A
hz : z ∈ J
xz : A
xz_mem : xz ∈ I
hxz : h.toLinearMap xz = x * h z
⊢ h.symm x * z = xz

Proof state:
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R A
B : Type u_1
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
I J : Submodule R A
h : A ≃ₐ[R] B
⊢ map h.toLinearMap (I / J) = map h.toLinearMap I / map h.toLinearMap J

Tactic:
ext x

Result:
case h
R : Type u
inst✝⁴ : CommSemiring R
A : Type v
inst✝³ : CommSemiring A
inst✝² : Algebra R 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 h.toLinearMap (I / J) ↔ x ∈ map h.toLinearMap I / map h.toLinearMap J