-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem sSup_toSubsemiring (S : Set (Subalgebra R A)) (hS : S.Nonempty) :
    (sSup S).toSubsemiring = sSup (toSubsemiring '' S)

Proof state:
case e_s.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ ∃ a ∈ S, (algebraMap R A) x ∈ a

Tactic:
exact ⟨y, hy, algebraMap_mem y x⟩

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)

Tactic:
rw [h, sSup_image, ← Subsemiring.closure_sUnion, sSup_def, adjoin_toSubsemiring]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S)) =
    Subsemiring.closure (⋃₀ (SetLike.coe '' S))

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
⊢ Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S)) =
    Subsemiring.closure (⋃₀ (SetLike.coe '' S))

Tactic:
congr 1

Result:
case e_s
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
⊢ Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)

Proof state:
case e_s
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
⊢ Set.range ⇑(algebraMap R A) ∪ ⋃₀ (SetLike.coe '' S) = ⋃₀ (SetLike.coe '' S)

Tactic:
rw [Set.union_eq_right]

Result:
case e_s
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
⊢ Set.range ⇑(algebraMap R A) ⊆ ⋃₀ (SetLike.coe '' S)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ toSubsemiring '' S = (fun x => Subsemiring.closure ↑x) '' S

Tactic:
congr! with x

Result:
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
x : Subalgebra R A
a✝ : x ∈ S
⊢ x.toSubsemiring = Subsemiring.closure ↑x

Proof state:
case h
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
x : Subalgebra R A
a✝ : x ∈ S
⊢ x.toSubsemiring = Subsemiring.closure ↑x

Tactic:
exact x.toSubsemiring.closure_eq.symm

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)

Tactic:
rw [Set.image_image]

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ toSubsemiring '' S = (fun x => Subsemiring.closure ↑x) '' S

Proof state:
case e_s.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ (algebraMap R A) x ∈ ⋃₀ (SetLike.coe '' S)

Tactic:
simp only [Set.mem_sUnion, Set.mem_image, exists_exists_and_eq_and, SetLike.mem_coe]

Result:
case e_s.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ ∃ a ∈ S, (algebraMap R A) x ∈ a

Proof state:
case e_s.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
x : R
⊢ (algebraMap R A) x ∈ ⋃₀ (SetLike.coe '' S)

Tactic:
obtain ⟨y, hy⟩ := hS

Result:
case e_s.intro.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
x : R
y : Subalgebra R A
hy : y ∈ S
⊢ (algebraMap R A) x ∈ ⋃₀ (SetLike.coe '' S)

Proof state:
case e_s
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
⊢ Set.range ⇑(algebraMap R A) ⊆ ⋃₀ (SetLike.coe '' S)

Tactic:
rintro _ ⟨x, rfl⟩

Result:
case e_s.intro
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
x : R
⊢ (algebraMap R A) x ∈ ⋃₀ (SetLike.coe '' S)

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)

Tactic:
have h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S) := by
  rw [Set.image_image]
  congr! with x
  exact x.toSubsemiring.closure_eq.symm

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
hS : S.Nonempty
h : toSubsemiring '' S = Subsemiring.closure '' (SetLike.coe '' S)
⊢ (sSup S).toSubsemiring = sSup (toSubsemiring '' S)