-- Mathlib/Algebra/Algebra/Hom.lean
lemma algebraMapSubmonoid_map_eq (f : A →ₐ[R] B) :
    (algebraMapSubmonoid A M).map f = algebraMapSubmonoid B M

Proof state:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ Submonoid.map f (algebraMapSubmonoid A M) ↔ x ∈ algebraMapSubmonoid B M

Tactic:
constructor

Result:
case h.mp
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ Submonoid.map f (algebraMapSubmonoid A M) → x ∈ algebraMapSubmonoid B M

case h.mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)

Proof state:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R A) r ∈ algebraMapSubmonoid A M ∧ f ((algebraMap R A) r) = (algebraMap R B) r

Tactic:
simp only [AlgHom.commutes, and_true]

Result:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R A) r ∈ algebraMapSubmonoid A M

Proof state:
case h.mpr.intro.intro
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ ∃ x ∈ algebraMapSubmonoid A M, f x = (algebraMap R B) r

Tactic:
use (algebraMap R A r)

Result:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R A) r ∈ algebraMapSubmonoid A M ∧ f ((algebraMap R A) r) = (algebraMap R B) r

Proof state:
case h.mpr.intro.intro
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R B) r ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
simp only [Submonoid.mem_map]

Result:
case h.mpr.intro.intro
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ ∃ x ∈ algebraMapSubmonoid A M, f x = (algebraMap R B) r

Proof state:
case h.mp.intro.intro.intro.intro
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ f ((algebraMap R A) r) ∈ algebraMapSubmonoid B M

Tactic:
simp only [AlgHom.commutes]

Result:
case h.mp.intro.intro.intro.intro
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R B) r ∈ algebraMapSubmonoid B M

Proof state:
case h.mp
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ Submonoid.map f (algebraMapSubmonoid A M) → x ∈ algebraMapSubmonoid B M

Tactic:
rintro ⟨a, ⟨r, hr, rfl⟩, rfl⟩

Result:
case h.mp.intro.intro.intro.intro
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ f ((algebraMap R A) r) ∈ algebraMapSubmonoid B M

Proof state:
case h.mpr
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ algebraMapSubmonoid B M → x ∈ Submonoid.map f (algebraMapSubmonoid A M)

Tactic:
rintro ⟨r, hr, rfl⟩

Result:
case h.mpr.intro.intro
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R B) r ∈ Submonoid.map f (algebraMapSubmonoid A M)

Proof state:
case h.mp.intro.intro.intro.intro
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R B) r ∈ algebraMapSubmonoid B M

Tactic:
use r

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ Submonoid.map f (algebraMapSubmonoid A M) = algebraMapSubmonoid B M

Tactic:
ext x

Result:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
x : B
⊢ x ∈ Submonoid.map f (algebraMapSubmonoid A M) ↔ x ∈ algebraMapSubmonoid B M

Proof state:
case h
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : CommRing B
inst✝ : Algebra R B
f : A →ₐ[R] B
r : R
hr : r ∈ ↑M
⊢ (algebraMap R A) r ∈ algebraMapSubmonoid A M

Tactic:
use r

Result:
no goals