-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
@[elab_as_elim]
lemma iSup_induction {ι : Sort*} (S : ι → Subalgebra R A) {motive : A → Prop}
    {x : A} (mem : x ∈ ⨆ i, S i)
    (basic : ∀ i, ∀ a ∈ S i, motive a)
    (zero : motive 0) (one : motive 1)
    (add : ∀ a b, motive a → motive b → motive (a + b))
    (mul : ∀ a b, motive a → motive b → motive (a * b))
    (algebraMap : ∀ r, motive (algebraMap R A r)) : motive x

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
zero : motive 0
one : motive 1
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((_root_.algebraMap R A) r)
T : Subalgebra R A :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := one, add_mem' := ⋯, zero_mem' := zero,
    algebraMap_mem' := algebraMap }
⊢ iSup S ≤ T

Tactic:
rwa [iSup_le_iff]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
zero : motive 0
one : motive 1
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((_root_.algebraMap R A) r)
T : Subalgebra R A :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := one, add_mem' := ⋯, zero_mem' := zero,
    algebraMap_mem' := algebraMap }
⊢ motive x

Tactic:
suffices iSup S ≤ T from this mem

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
zero : motive 0
one : motive 1
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((_root_.algebraMap R A) r)
T : Subalgebra R A :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := one, add_mem' := ⋯, zero_mem' := zero,
    algebraMap_mem' := algebraMap }
⊢ iSup S ≤ T

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
zero : motive 0
one : motive 1
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((_root_.algebraMap R A) r)
⊢ motive x

Tactic:
let T : Subalgebra R A :=
{ carrier := {x | motive x}
  mul_mem' {a b} := mul a b
  one_mem' := one
  add_mem' {a b} := add a b
  zero_mem' := zero
  algebraMap_mem' := algebraMap }

Result:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
ι : Sort u_1
S : ι → Subalgebra R A
motive : A → Prop
x : A
mem : x ∈ ⨆ i, S i
basic : ∀ (i : ι), ∀ a ∈ S i, motive a
zero : motive 0
one : motive 1
add : ∀ (a b : A), motive a → motive b → motive (a + b)
mul : ∀ (a b : A), motive a → motive b → motive (a * b)
algebraMap : ∀ (r : R), motive ((_root_.algebraMap R A) r)
T : Subalgebra R A :=
  { carrier := {x | motive x}, mul_mem' := ⋯, one_mem' := one, add_mem' := ⋯, zero_mem' := zero,
    algebraMap_mem' := algebraMap }
⊢ motive x