ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<VAR>b₂ : α<VAR>b₂J : b₂ ∈ J<VAR>cba₂ : c₂ ≤ b₂ ⊔ a₂<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<VAR>b₂ : α<VAR>b₂J : b₂ ∈ J<VAR>cba₂ : c₂ ≤ b₂ ⊔ a₂<VAR>b : α := b₁ ⊔ b₂<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<VAR>b₂ : α<VAR>b₂J : b₂ ∈ J<VAR>cba₂ : c₂ ≤ b₂ ⊔ a₂<VAR>b : α := b₁ ⊔ b₂<VAR>bJ : b ∈ J<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<VAR>b₂ : α<VAR>b₂J : b₂ ∈ J<VAR>cba₂ : c₂ ≤ b₂ ⊔ a₂<VAR>b : α := b₁ ⊔ b₂<VAR>bJ : b ∈ J<VAR>ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>JF : Disjoint (↑F) Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<VAR>b₂ : α<VAR>b₂J : b₂ ∈ J<VAR>cba₂ : c₂ ≤ b₂ ⊔ a₂<VAR>b : α := b₁ ⊔ b₂<VAR>bJ : b ∈ J<VAR>ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂<VAR>ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F<GOAL>a₁ ⊓ a₂ ∉ J
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<VAR>b₂ : α<VAR>b₂J : b₂ ∈ J<VAR>cba₂ : c₂ ≤ b₂ ⊔ a₂<VAR>b : α := b₁ ⊔ b₂<VAR>bJ : b ∈ J<VAR>ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂<VAR>ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F<VAR>ha₁a₂ : a₁ ⊓ a₂ ∈ J<GOAL>¬Disjoint (↑F) Jset
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<VAR>b₂ : α<VAR>b₂J : b₂ ∈ J<VAR>cba₂ : c₂ ≤ b₂ ⊔ a₂<VAR>b : α := b₁ ⊔ b₂<VAR>bJ : b ∈ J<VAR>ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂<VAR>ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F<VAR>ha₁a₂ : a₁ ⊓ a₂ ∈ J<GOAL>∃ x ∈ ↑F, x ∈ Jset
<VAR>α : Type u_1<VAR>inst✝¹ : DistribLattice α<VAR>inst✝ : BoundedOrder α<VAR>F : PFilter α<VAR>I : Ideal α<VAR>hFI : Disjoint ↑F ↑I<VAR>S : Set (Set α) := {J | IsIdeal J ∧ ↑I ≤ J ∧ Disjoint (↑F) J}<VAR>Jset : Set α<VAR>Jidl : IsIdeal Jset<VAR>IJ : ↑I ≤ Jset<VAR>left✝ : ↑I ⊆ Jset<VAR>Jmax : ∀ a ∈ S, Jset ⊆ a → a = Jset<VAR>J : Ideal α := Jidl.toIdeal<VAR>IJ' : I ≤ J<VAR>Jpr : J.IsProper<VAR>a₁ a₂ : α<VAR>ha₁ : a₁ ∉ J<VAR>ha₂ : a₂ ∉ J<VAR>J₁ : Ideal α := J ⊔ principal a₁<VAR>J₂ : Ideal α := J ⊔ principal a₂<VAR>a₁J₁ : a₁ ∈ J₁<VAR>a₂J₂ : a₂ ∈ J₂<VAR>J₁J : ↑J₁ ≠ Jset<VAR>J₂J : ↑J₂ ≠ Jset<VAR>J₁S : ↑J₁ ∉ S<VAR>J₂S : ↑J₂ ∉ S<VAR>J₁F : ¬Disjoint ↑F ↑J₁<VAR>J₂F : ¬Disjoint ↑F ↑J₂<VAR>c₁ : α<VAR>c₁F : c₁ ∈ ↑F<VAR>c₁J₁ : c₁ ∈ ↑J₁<VAR>c₂ : α<VAR>c₂F : c₂ ∈ ↑F<VAR>c₂J₂ : c₂ ∈ ↑J₂<VAR>b₁ : α<VAR>b₁J : b₁ ∈ J<VAR>cba₁ : c₁ ≤ b₁ ⊔ a₁<VAR>b₂ : α<VAR>b₂J : b₂ ∈ J<VAR>cba₂ : c₂ ≤ b₂ ⊔ a₂<VAR>b : α := b₁ ⊔ b₂<VAR>bJ : b ∈ J<VAR>ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂<VAR>ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F<VAR>ha₁a₂ : a₁ ⊓ a₂ ∈ J<GOAL>b ⊔ a₁ ⊓ a₂ ∈ ↑F ∧ b ⊔ a₁ ⊓ a₂ ∈ Jset
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>r : α → β → Prop<VAR>s : Multiset (Multiset α)<VAR>t : Multiset (Multiset β)<VAR>h : Rel (Rel r) s t<GOAL>Rel r s.join t.join
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>(D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j) ≫ (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) = D.diagramOverOpenπ U j ≫ (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j ≫ (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) = D.diagramOverOpenπ U j ≫ (componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).map (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ { pt := (D.U i).presheaf.obj (op U), π := { app := fun j => D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app (op (WalkingMultispan.left (i, j))) ≫ 𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j)))) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫ 𝟙 ((componentwiseDiagram D.diagram.multispan (⋯.functor.obj U)).obj (op (WalkingMultispan.left (i, j))))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ { pt := (D.U i).presheaf.obj (op U), π := { app := fun j => D.ιInvAppπApp U (unop j), naturality := ⋯ } }.π.app (op (WalkingMultispan.left (i, j))) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ ((D.f i i).c.app (op U) ≫ (D.t i i).c.app ((Opens.map (D.f i i).base).op.obj (op U)) ≫ invApp (D.f i i) (unop (op ((Opens.map (D.t i i).base).toPrefunctor.1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ≫ (D.U i).presheaf.map (eqToHom ⋯).op) ≫ (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ ((D.f i i).c.app (op U) ≫ ((D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U))) ≫ (D.V (i, i)).presheaf.map (eqToHom ⋯)) ≫ invApp (D.f i i) (unop (op ((Opens.map (D.t i i).base).toPrefunctor.1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))))) ≫ (D.U i).presheaf.map (eqToHom ⋯).op) ≫ (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ (D.f i i).c.app (op U) ≫ (D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U))) ≫ (D.V (i, i)).presheaf.map (eqToHom ⋯) ≫ invApp (D.f i i) ((Opens.map (D.t i i).base).toPrefunctor.1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))) ≫ (D.U i).presheaf.map (eqToHom ⋯).op ≫ (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ (D.f i i).c.app (op U) ≫ (D.V (i, i)).presheaf.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯) ≫ invApp (D.f i i) ((Opens.map (D.t i i).base).toPrefunctor.1 (unop ((Opens.map (D.f i i).base).op.obj (op U)))) ≫ (D.U i).presheaf.map (eqToHom ⋯).op ≫ (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ (D.U i).presheaf.map (homOfLE ⋯).op ≫ (D.U i).presheaf.map ((opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫ (D.U i).presheaf.map (eqToHom ⋯).op ≫ (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ (D.U i).presheaf.map ((((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫ (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫ (eqToHom ⋯).op) ≫ (D.f i j).c.app (op ((Opens.map (D.ι i).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ (D.f i j).c.app (op ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U))) ≫ ((TopCat.Presheaf.pushforward C (D.f i j).base).obj (D.V (i, j)).presheaf).map ((((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫ (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫ (eqToHom ⋯).op) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : GlueData C<VAR>inst✝ : HasLimits C<VAR>i j : D.J<VAR>U : Opens ↑↑(D.U i)<GOAL>D.diagramOverOpenπ U i ≫ (D.f i j).c.app (op ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.right i)))).base).obj (⋯.functor.obj U))) ≫ (D.V (i, j)).presheaf.map ((Opens.map (D.f i j).base).op.map ((((eqToIso ⋯).inv ≫ (homOfLE ⋯).op) ≫ (opensFunctor (D.f i i)).op.map (𝟙 ((Opens.map (D.f i i).base).op.obj (op U)) ≫ eqToHom ⋯)) ≫ (eqToHom ⋯).op) ≫ eqToHom ⋯) = limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j)))
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f g : α → β → α<VAR>a : α<VAR>l : List β<VAR>H : ∀ (a : α) (b : β), b ∈ l → f a b = g a b<GOAL>foldl f a l = foldl g a l
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n<VAR>a : α<VAR>x✝ : ∃ n, a ∈ f n<VAR>n : ℕ<VAR>h : a ∈ f n<GOAL>a ∈ rfindOpt f
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n<VAR>a : α<VAR>x✝ : ∃ n, a ∈ f n<VAR>n : ℕ<VAR>h : a ∈ f n<VAR>h' : (rfindOpt f).Dom<GOAL>a ∈ rfindOpt f
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n<VAR>a : α<VAR>x✝ : ∃ n, a ∈ f n<VAR>n : ℕ<VAR>h : a ∈ f n<VAR>h' : (rfindOpt f).Dom<VAR>k : ℕ<VAR>hk : (rfindOpt f).get h' ∈ f k<GOAL>a ∈ rfindOpt f
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n<VAR>a : α<VAR>x✝ : ∃ n, a ∈ f n<VAR>n : ℕ<VAR>h : a ∈ f n<VAR>h' : (rfindOpt f).Dom<VAR>k : ℕ<VAR>hk : (rfindOpt f).get h' ∈ f k<VAR>this : Option.some a = Option.some ((rfindOpt f).get h')<GOAL>a ∈ rfindOpt f
<VAR>α : Type u_1<VAR>f : ℕ → Option α<VAR>H : ∀ {a : α} {m n : ℕ}, m ≤ n → a ∈ f m → a ∈ f n<VAR>a : α<VAR>x✝ : ∃ n, a ∈ f n<VAR>n : ℕ<VAR>h : a ∈ f n<VAR>h' : (rfindOpt f).Dom<VAR>k : ℕ<VAR>hk : (rfindOpt f).get h' ∈ f k<VAR>this : a = (rfindOpt f).get h'<GOAL>a ∈ rfindOpt f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝² : LinearOrder R<VAR>inst✝¹ : LinearOrder S<VAR>inst✝ : F.NeBot<VAR>t : R<VAR>ht : ∀ (a : R), (∀ᶠ (x : R) in F, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) t a<VAR>tbot : ¬IsBot t<GOAL>∃ l, ∃ᶠ (x : R) in F, l ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝² : LinearOrder R<VAR>inst✝¹ : LinearOrder S<VAR>inst✝ : F.NeBot<VAR>t : R<VAR>ht : ∀ (a : R), (∀ᶠ (x : R) in F, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) t a<VAR>tbot : ¬IsBot t<VAR>t' : R<VAR>ht' : t' < t<GOAL>∃ l, ∃ᶠ (x : R) in F, l ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝² : LinearOrder R<VAR>inst✝¹ : LinearOrder S<VAR>inst✝ : F.NeBot<VAR>t : R<VAR>ht : ∀ (a : R), (∀ᶠ (x : R) in F, (fun x x_1 => x ≤ x_1) x a) → (fun x x_1 => x ≤ x_1) t a<VAR>tbot : ¬IsBot t<VAR>t' : R<VAR>ht' : t' < t<VAR>ev : ∀ᶠ (x : R) in F, ¬(fun x => t' ≤ x) x<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>F : Filter R<VAR>inst✝² : LinearOrder R<VAR>inst✝¹ : LinearOrder S<VAR>inst✝ : F.NeBot<VAR>t : R<VAR>tbot : ¬IsBot t<VAR>t' : R<VAR>ht' : t' < t<VAR>ev : ∀ᶠ (x : R) in F, ¬(fun x => t' ≤ x) x<VAR>ht : t ≤ t'<GOAL>False
<VAR>R✝ : Type u_1<VAR>inst✝¹⁸ : CommRing R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝¹⁷ : CommRing S✝<VAR>inst✝¹⁶ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K✝ : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>R : Type u_6<VAR>S : Type u_7<VAR>K : Type u_8<VAR>L : Type u_9<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing L<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsFractionRing S L<VAR>inst✝ : Algebra.IsIntegral R S<VAR>x : L<GOAL>IsAlgebraic K x
<VAR>R✝ : Type u_1<VAR>inst✝¹⁸ : CommRing R✝<VAR>M : Submonoid R✝<VAR>S✝ : Type u_2<VAR>inst✝¹⁷ : CommRing S✝<VAR>inst✝¹⁶ : Algebra R✝ S✝<VAR>P : Type u_3<VAR>inst✝¹⁵ : CommRing P<VAR>A : Type u_4<VAR>K✝ : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>R : Type u_6<VAR>S : Type u_7<VAR>K : Type u_8<VAR>L : Type u_9<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing L<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsFractionRing S L<VAR>inst✝ : Algebra.IsIntegral R S<VAR>x : S<VAR>s : ↥S⁰<GOAL>IsAlgebraic K (mk' L x s)