F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
⊢ x ≤ upperBound hc
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
⊢ ∀ (a : Lifts F E K), a ∈ c → a ≤ upperBound hc
intro x hx
case left
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
⊢ x.fst ≤ (upperBound hc).fst

case right
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
⊢ ∀ (s : { x_1 // x_1 ∈ x.fst }) (t : { x // x ∈ (upperBound hc).fst }), ↑s = ↑t → ↑x.snd s = ↑(upperBound hc).snd t
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
⊢ x ≤ upperBound hc
constructor
no goals
case left
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
⊢ x.fst ≤ (upperBound hc).fst
exact fun s hs => ⟨x, Set.mem_insert_of_mem ⊥ hx, hs⟩
case right
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
s : { x_1 // x_1 ∈ x.fst }
t : { x // x ∈ (upperBound hc).fst }
hst : ↑s = ↑t
⊢ ↑x.snd s = ↑(upperBound hc).snd t
case right
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
⊢ ∀ (s : { x_1 // x_1 ∈ x.fst }) (t : { x // x ∈ (upperBound hc).fst }), ↑s = ↑t → ↑x.snd s = ↑(upperBound hc).snd t
intro s t hst
case right
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
s : { x_1 // x_1 ∈ x.fst }
t : { x // x ∈ (upperBound hc).fst }
hst : ↑s = ↑t
⊢ ↑x.snd s =
    ↑(Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).snd
      { val := ↑t, property := (_ : ↑t ∈ (Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).fst) }
case right
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
s : { x_1 // x_1 ∈ x.fst }
t : { x // x ∈ (upperBound hc).fst }
hst : ↑s = ↑t
⊢ ↑x.snd s = ↑(upperBound hc).snd t
change x.2 s = (Classical.choose t.mem).2 ⟨t, (Classical.choose_spec t.mem).2⟩
case right.intro.intro.intro
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
s : { x_1 // x_1 ∈ x.fst }
t : { x // x ∈ (upperBound hc).fst }
hst : ↑s = ↑t
z : Lifts F E K
left✝ : z ∈ insert ⊥ c
hxz : x ≤ z
hyz : Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst) ≤ z
⊢ ↑x.snd s =
    ↑(Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).snd
      { val := ↑t, property := (_ : ↑t ∈ (Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).fst) }
case right
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
s : { x_1 // x_1 ∈ x.fst }
t : { x // x ∈ (upperBound hc).fst }
hst : ↑s = ↑t
⊢ ↑x.snd s =
    ↑(Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).snd
      { val := ↑t, property := (_ : ↑t ∈ (Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).fst) }
obtain ⟨z, _, hxz, hyz⟩ :=
  Lifts.exists_max_two hc (Set.mem_insert_of_mem ⊥ hx) (Classical.choose_spec t.mem).1
case right.intro.intro.intro
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
s : { x_1 // x_1 ∈ x.fst }
t : { x // x ∈ (upperBound hc).fst }
hst : ↑s = ↑t
z : Lifts F E K
left✝ : z ∈ insert ⊥ c
hxz : x ≤ z
hyz : Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst) ≤ z
⊢ ↑z.snd { val := ↑s, property := (_ : ↑s ∈ z.fst) } =
    ↑z.snd
      { val := ↑{ val := ↑t, property := (_ : ↑t ∈ (Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).fst) },
        property :=
          (_ : ↑{ val := ↑t, property := (_ : ↑t ∈ (Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).fst) } ∈ z.fst) }
case right.intro.intro.intro
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
s : { x_1 // x_1 ∈ x.fst }
t : { x // x ∈ (upperBound hc).fst }
hst : ↑s = ↑t
z : Lifts F E K
left✝ : z ∈ insert ⊥ c
hxz : x ≤ z
hyz : Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst) ≤ z
⊢ ↑x.snd s =
    ↑(Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).snd
      { val := ↑t, property := (_ : ↑t ∈ (Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).fst) }
rw [Lifts.eq_of_le hxz, Lifts.eq_of_le hyz]
no goals
case right.intro.intro.intro
F : Type u_3
E : Type u_2
K : Type u_1
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
S : Set E
c : Set (Lifts F E K)
hc : IsChain (fun x x_1 => x ≤ x_1) c
x : Lifts F E K
hx : x ∈ c
s : { x_1 // x_1 ∈ x.fst }
t : { x // x ∈ (upperBound hc).fst }
hst : ↑s = ↑t
z : Lifts F E K
left✝ : z ∈ insert ⊥ c
hxz : x ≤ z
hyz : Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst) ≤ z
⊢ ↑z.snd { val := ↑s, property := (_ : ↑s ∈ z.fst) } =
    ↑z.snd
      { val := ↑{ val := ↑t, property := (_ : ↑t ∈ (Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).fst) },
        property :=
          (_ : ↑{ val := ↑t, property := (_ : ↑t ∈ (Classical.choose (_ : ↑t ∈ ↑(upperBound hc).fst)).fst) } ∈ z.fst) }
exact congr_arg z.2 (Subtype.ext hst)