-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem mem_adjoin_of_map_mul {s} {x : A} {f : A →ₗ[R] B} (hf : ∀ a₁ a₂, f (a₁ * a₂) = f a₁ * f a₂)
    (h : x ∈ adjoin R s) : f x ∈ adjoin R (f '' (s ∪ {1}))

Proof state:
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
h : x ∈ adjoin R s
⊢ f x ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
induction h using adjoin_induction with
| mem a ha => exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩
| algebraMap r =>
  have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
    subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
  convert Subalgebra.smul_mem (adjoin R (f '' (s ∪ {1}))) this r
  rw [algebraMap_eq_smul_one]
  exact f.map_smul _ _
| add y z _ _ hy hz => simpa [hy, hz] using Subalgebra.add_mem _ hy hz
| mul y z _ _ hy hz => simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz

Result:
no goals

Proof state:
case algebraMap
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
⊢ f ((algebraMap R A) r) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
  subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩

Result:
case algebraMap
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f ((algebraMap R A) r) ∈ adjoin R (⇑f '' (s ∪ {1}))

Proof state:
case algebraMap
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f ((algebraMap R A) r) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
convert Subalgebra.smul_mem (adjoin R (f '' (s ∪ {1}))) this r

Result:
case h.e'_5
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f ((algebraMap R A) r) = r • f 1

Proof state:
case h.e'_5
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f ((algebraMap R A) r) = r • f 1

Tactic:
rw [algebraMap_eq_smul_one]

Result:
case h.e'_5
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f (r • 1) = r • f 1

Proof state:
case mul
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : f y ∈ adjoin R (⇑f '' (s ∪ {1}))
hz : f z ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f (y * z) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
simpa [hf, hy, hz] using Subalgebra.mul_mem _ hy hz

Result:
no goals

Proof state:
case h.e'_5
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
this : f 1 ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f (r • 1) = r • f 1

Tactic:
exact f.map_smul _ _

Result:
no goals

Proof state:
case mem
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
a : A
ha : a ∈ s
⊢ f a ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
exact subset_adjoin ⟨a, ⟨Set.subset_union_left ha, rfl⟩⟩

Result:
no goals

Proof state:
case add
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
y z : A
hx✝ : y ∈ adjoin R s
hy✝ : z ∈ adjoin R s
hy : f y ∈ adjoin R (⇑f '' (s ∪ {1}))
hz : f z ∈ adjoin R (⇑f '' (s ∪ {1}))
⊢ f (y + z) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
simpa [hy, hz] using Subalgebra.add_mem _ hy hz

Result:
no goals