-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem iSupLift_of_mem {i : ι} (x : T) (hx : (x : A) ∈ K i) :
    iSupLift K dir f hf T hT x = f i ⟨x, hx⟩

Proof state:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ x = (f i) ⟨↑x, hx⟩

Tactic:
apply Set.iUnionLift_of_mem

Result:
no goals

Proof state:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf (iSup K) ⋯) x = (f i) ⟨↑x, hx⟩

Tactic:
dsimp [iSupLift]

Result:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑(iSup K) ⋯ x = (f i) ⟨↑x, hx⟩

Proof state:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : NonUnitalStarSubalgebra R A
hT : T = iSup K
i : ι
x : ↥T
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf T hT) x = (f i) ⟨↑x, hx⟩

Tactic:
subst hT

Result:
R : Type u
A : Type v
B : Type w
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : NonUnitalSemiring A
inst✝⁹ : StarRing A
inst✝⁸ : Module R A
inst✝⁷ : NonUnitalSemiring B
inst✝⁶ : StarRing B
inst✝⁵ : Module R B
ι : Type u_1
inst✝⁴ : StarRing R
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : StarModule R A
inst✝ : Nonempty ι
K : ι → NonUnitalStarSubalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →⋆ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i : ι
x : ↥(iSup K)
hx : ↑x ∈ K i
⊢ (iSupLift K dir f hf (iSup K) ⋯) x = (f i) ⟨↑x, hx⟩