-- Module: Mathlib.Algebra.Star.Subalgebra
Goal:
R : Type u_2
A : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : Algebra R A
inst_4 : StarRing A
inst_5 : StarModule R A
s : Set A
p :
  (x y : A) →
    Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x →
      Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both :
  ∀ (r₁ r₂ : R), p ((Algebra.algebraMap R A : (a : R) → A) r₁) ((Algebra.algebraMap R A : (a : R) → A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((Algebra.algebraMap R A : (a : R) → A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((Algebra.algebraMap R A : (a : R) → A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y)
    (hz : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) z), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
star_left :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p (Star.star x) y ⋯ hy
star_right :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y), p x y hx hy → p x (Star.star y) hx ⋯
a b : A
ha : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) a
hb : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) b
mem : ∀ (z : A) (hz : z ∈ s), p a z ha ⋯
algebraMap : ∀ (r : R), p a ((Algebra.algebraMap R A : (a : R) → A) r) ha ⋯
mul :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y) (h₁ : p a x ha hx) (h₂ : p a y ha hy),
    p a (x * y) ha ⋯
add :
  ∀ (x y : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x)
    (hy : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) y) (h₁ : p a x ha hx) (h₂ : p a y ha hy),
    p a (x + y) ha ⋯
star :
  ∀ (x : A) (hx : Membership.mem (γ := StarSubalgebra R A) (adjoin R s) x) (h : p a x ha hx), p a (Star.star x) ha ⋯
⊢ p a b ha hb

Tactic:
induction hb using adjoin_induction with
  | mem z hz => induction ha using adjoin_induction with
    | mem _ h => exact mem_mem _ _ h hz
    | algebraMap _ => exact algebraMap_left _ _ hz
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | star _ _ h => exact star_left _ _ _ _ h
  | algebraMap r =>
    induction ha using adjoin_induction with
    | mem _ h => exact algebraMap_right _ _ h
    | algebraMap _ => exact algebraMap_both _ _
    | mul _ _ _ _ h₁ h₂ => exact mul_left _ _ _ _ _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add_left _ _ _ _ _ _ h₁ h₂
    | star _ _ h => exact star_left _ _ _ _ h
  | mul _ _ _ _ h₁ h₂ => exact mul_right _ _ _ _ _ _ h₁ h₂
  | add _ _ _ _ h₁ h₂ => exact add_right _ _ _ _ _ _ h₁ h₂
  | star _ _ h => exact star_right _ _ _ _ h

Premises used: Algebra.algebraMap, Star.star