R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = AlgHom.comp (f j) (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : { x // x ∈ T }
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
      (_ :
        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
          (fun i x => ↑(f i) x) i { val := x, property := hxi } = (fun i x => ↑(f i) x) j { val := x, property := hxj })
      ↑T (_ : ↑T ⊆ ⋃ (i : ι), ↑(K i)) x =
    ↑(f i) { val := ↑x, property := hx }
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = AlgHom.comp (f j) (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : { x // x ∈ T }
hx : ↑x ∈ K i
⊢ ↑(iSupLift K dir f hf T hT) x = ↑(f i) { val := ↑x, property := hx }
dsimp [iSupLift, inclusion]
no goals
R : Type u
A : Type v
B : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Subalgebra R A
ι : Type u_1
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x x_1 => x ≤ x_1) K
f : (i : ι) → { x // x ∈ K i } →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = AlgHom.comp (f j) (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : { x // x ∈ T }
hx : ↑x ∈ K i
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => ↑(f i) x)
      (_ :
        ∀ (i j : ι) (x : A) (hxi : x ∈ (fun i => ↑(K i)) i) (hxj : x ∈ (fun i => ↑(K i)) j),
          (fun i x => ↑(f i) x) i { val := x, property := hxi } = (fun i x => ↑(f i) x) j { val := x, property := hxj })
      ↑T (_ : ↑T ⊆ ⋃ (i : ι), ↑(K i)) x =
    ↑(f i) { val := ↑x, property := hx }
rw [Set.iUnionLift_of_mem]